Library Stackingproof

Correctness proof for the translation from Linear to Mach.

This file proves semantic preservation for the Stacking pass. For the target language Mach, we use the abstract semantics given in file Machabstr, where a part of the activation record is not resident in memory. Combined with the semantic equivalence result between the two Mach semantics (see file Machabstr2concr), the proof in this file also shows semantic preservation with respect to the concrete Mach semantics.





Require Import Coqlib.

Require Import Maps.

Require Import Errors.

Require Import AST.

Require Import Integers.

Require Import Values.

Require Import Op.

Require Import Mem.

Require Import Events.

Require Import Globalenvs.

Require Import Smallstep.

Require Import Locations.

Require Import Linear.

Require Import Lineartyping.

Require Import Mach.

Require Import Machabstr.

Require Import Bounds.

Require Import Conventions.

Require Import Stacklayout.

Require Import Stacking.

Properties of frames and frame accesses

``Good variable'' properties for frame accesses.





Lemma typesize_typesize:

  forall ty, AST.typesize ty = 4 * Locations.typesize ty.






Section PRESERVATION.




Variable prog: Linear.program.

Variable tprog: Mach.program.

Hypothesis TRANSF: transf_program prog = OK tprog.

Let ge := Genv.globalenv prog.

Let tge := Genv.globalenv tprog.




Section FRAME_PROPERTIES.




Variable stack: list Machabstr.stackframe.

Variable f: Linear.function.

Let b := function_bounds f.

Let fe := make_env b.

Variable tf: Mach.function.

Hypothesis TRANSF_F: transf_function f = OK tf.




Lemma unfold_transf_function:

  tf = Mach.mkfunction

         f.(Linear.fn_sig)

         (transl_body f fe)

         f.(Linear.fn_stacksize)

         fe.(fe_size)

         (Int.repr fe.(fe_ofs_link))

         (Int.repr fe.(fe_ofs_retaddr)).






Lemma size_no_overflow: fe.(fe_size) <= -Int.min_signed.

A frame index is valid if it lies within the resource bounds of the current function.





Definition index_valid (idx: frame_index) :=

  match idx with

  | FI_link => True

  | FI_retaddr => True

  | FI_local x Tint => 0 <= x < b.(bound_int_local)

  | FI_local x Tfloat => 0 <= x < b.(bound_float_local)

  | FI_arg x ty => 0 <= x /\ x + typesize ty <= b.(bound_outgoing)

  | FI_saved_int x => 0 <= x < b.(bound_int_callee_save)

  | FI_saved_float x => 0 <= x < b.(bound_float_callee_save)

  end.




Definition type_of_index (idx: frame_index) :=

  match idx with

  | FI_link => Tint

  | FI_retaddr => Tint

  | FI_local x ty => ty

  | FI_arg x ty => ty

  | FI_saved_int x => Tint

  | FI_saved_float x => Tfloat

  end.

Non-overlap between the memory areas corresponding to two frame indices.





Definition index_diff (idx1 idx2: frame_index) : Prop :=

  match idx1, idx2 with

  | FI_link, FI_link => False

  | FI_retaddr, FI_retaddr => False

  | FI_local x1 ty1, FI_local x2 ty2 =>

      x1 <> x2 \/ ty1 <> ty2

  | FI_arg x1 ty1, FI_arg x2 ty2 =>

      x1 + typesize ty1 <= x2 \/ x2 + typesize ty2 <= x1

  | FI_saved_int x1, FI_saved_int x2 => x1 <> x2

  | FI_saved_float x1, FI_saved_float x2 => x1 <> x2

  | _, _ => True

  end.




Ltac AddPosProps :=

  generalize (bound_int_local_pos b); intro;

  generalize (bound_float_local_pos b); intro;

  generalize (bound_int_callee_save_pos b); intro;

  generalize (bound_float_callee_save_pos b); intro;

  generalize (bound_outgoing_pos b); intro;

  generalize (align_float_part b); intro.




Lemma size_pos: fe.(fe_size) >= 0.






Opaque function_bounds.




Lemma offset_of_index_disj:

  forall idx1 idx2,

  index_valid idx1 -> index_valid idx2 ->

  index_diff idx1 idx2 ->

  offset_of_index fe idx1 + 4 * typesize (type_of_index idx1) <= offset_of_index fe idx2 \/

  offset_of_index fe idx2 + 4 * typesize (type_of_index idx2) <= offset_of_index fe idx1.






Remark aligned_4_4x: forall x, (4 | 4 * x).






Remark aligned_4_8x: forall x, (4 | 8 * x).






Remark aligned_4_align8: forall x, (4 | align x 8).






Hint Resolve Zdivide_0 Zdivide_refl Zdivide_plus_r

             aligned_4_4x aligned_4_8x aligned_4_align8: align_4.




Hint Extern 4 (?X | ?Y) => (exists (Y/X); reflexivity) : align_4.




Lemma offset_of_index_aligned:

  forall idx, (4 | offset_of_index fe idx).






Lemma frame_size_aligned:

  (4 | fe_size fe).

The following lemmas give sufficient conditions for indices of various kinds to be valid.





Lemma index_local_valid:

  forall ofs ty,

  slot_within_bounds f b (Local ofs ty) ->

  index_valid (FI_local ofs ty).






Lemma index_arg_valid:

  forall ofs ty,

  slot_within_bounds f b (Outgoing ofs ty) ->

  index_valid (FI_arg ofs ty).






Lemma index_saved_int_valid:

  forall r,

  In r int_callee_save_regs ->

  index_int_callee_save r < b.(bound_int_callee_save) ->

  index_valid (FI_saved_int (index_int_callee_save r)).






Lemma index_saved_float_valid:

  forall r,

  In r float_callee_save_regs ->

  index_float_callee_save r < b.(bound_float_callee_save) ->

  index_valid (FI_saved_float (index_float_callee_save r)).






Hint Resolve index_local_valid index_arg_valid

             index_saved_int_valid index_saved_float_valid: stacking.

The offset of a valid index lies within the bounds of the frame.





Lemma offset_of_index_valid:

  forall idx,

  index_valid idx ->

  0 <= offset_of_index fe idx /\

  offset_of_index fe idx + 4 * typesize (type_of_index idx) <= fe.(fe_size).

Offsets for valid index are representable as signed machine integers without loss of precision.





Lemma offset_of_index_no_overflow:

  forall idx,

  index_valid idx ->

  Int.signed (Int.repr (offset_of_index fe idx)) = offset_of_index fe idx.

Characterization of the get_slot and set_slot operations in terms of the following index_val and set_index_val frame access functions.





Definition index_val (idx: frame_index) (fr: frame) :=

  fr (type_of_index idx) (offset_of_index fe idx - tf.(fn_framesize)).




Definition set_index_val (idx: frame_index) (v: val) (fr: frame) :=

  update (type_of_index idx) (offset_of_index fe idx - tf.(fn_framesize)) v fr.




Lemma slot_valid_index:

  forall idx,

  index_valid idx -> idx <> FI_link -> idx <> FI_retaddr ->

  slot_valid tf (type_of_index idx) (offset_of_index fe idx).






Lemma get_slot_index:

  forall fr idx ty v,

  index_valid idx -> idx <> FI_link -> idx <> FI_retaddr ->

  ty = type_of_index idx ->

  v = index_val idx fr ->

  get_slot tf fr ty (Int.signed (Int.repr (offset_of_index fe idx))) v.






Lemma set_slot_index:

  forall fr idx v,

  index_valid idx -> idx <> FI_link -> idx <> FI_retaddr ->

  set_slot tf fr (type_of_index idx) (Int.signed (Int.repr (offset_of_index fe idx)))

                 v (set_index_val idx v fr).

``Good variable'' properties for index_val and set_index_val.





Lemma get_set_index_val_same:

  forall fr idx v,

  index_val idx (set_index_val idx v fr) = v.






Lemma get_set_index_val_other:

  forall fr idx idx' v,

  index_valid idx -> index_valid idx' -> index_diff idx idx' ->

  index_val idx' (set_index_val idx v fr) = index_val idx' fr.






Lemma get_set_index_val_overlap:

  forall ofs1 ty1 ofs2 ty2 v fr,

  S (Outgoing ofs1 ty1) <> S (Outgoing ofs2 ty2) ->

  Loc.overlap (S (Outgoing ofs1 ty1)) (S (Outgoing ofs2 ty2)) = true ->

  index_val (FI_arg ofs2 ty2) (set_index_val (FI_arg ofs1 ty1) v fr) = Vundef.

Accessing stack-based arguments in the caller's frame.





Definition get_parent_slot (cs: list stackframe) (ofs: Z) (ty: typ) (v: val) : Prop :=

  get_slot (parent_function cs) (parent_frame cs)

           ty (Int.signed (Int.repr (fe_ofs_arg + 4 * ofs))) v.

Agreement between location sets and Mach environments

The following agree predicate expresses semantic agreement between:

on the Linear side, the current location set ls and the location set of the caller ls0;
on the Mach side, a register set rs, a frame fr and a call stack cs.





Record agree (ls ls0: locset) (rs: regset) (fr: frame) (cs: list stackframe): Prop :=

  mk_agree {

Machine registers have the same values on the Linear and Mach sides.


    agree_reg:

      forall r, ls (R r) = rs r;

Machine registers outside the bounds of the current function have the same values they had at function entry. In other terms, these registers are never assigned.


    agree_unused_reg:

      forall r, ~(mreg_within_bounds b r) -> rs r = ls0 (R r);

Local and outgoing stack slots (on the Linear side) have the same values as the one loaded from the current Mach frame at the corresponding offsets.


    agree_locals:

      forall ofs ty, 

      slot_within_bounds f b (Local ofs ty) ->

      ls (S (Local ofs ty)) = index_val (FI_local ofs ty) fr;

    agree_outgoing:

      forall ofs ty, 

      slot_within_bounds f b (Outgoing ofs ty) ->

      ls (S (Outgoing ofs ty)) = index_val (FI_arg ofs ty) fr;

Incoming stack slots (on the Linear side) have the same values as the one loaded from the parent Mach frame at the corresponding offsets.


    agree_incoming:

      forall ofs ty,

      In (S (Incoming ofs ty)) (loc_parameters f.(Linear.fn_sig)) ->

      get_parent_slot cs ofs ty (ls (S (Incoming ofs ty)));

The areas of the frame reserved for saving used callee-save registers always contain the values that those registers had on function entry.


    agree_saved_int:

      forall r,

      In r int_callee_save_regs ->

      index_int_callee_save r < b.(bound_int_callee_save) ->

      index_val (FI_saved_int (index_int_callee_save r)) fr = ls0 (R r);

    agree_saved_float:

      forall r,

      In r float_callee_save_regs ->

      index_float_callee_save r < b.(bound_float_callee_save) ->

      index_val (FI_saved_float (index_float_callee_save r)) fr = ls0 (R r)

  }.




Hint Resolve agree_reg agree_unused_reg 

             agree_locals agree_outgoing agree_incoming

             agree_saved_int agree_saved_float: stacking.

Values of registers and register lists.





Lemma agree_eval_reg:

  forall ls ls0 rs fr cs r,

  agree ls ls0 rs fr cs -> rs r = ls (R r).






Lemma agree_eval_regs:

  forall ls ls0 rs fr cs rl,

  agree ls ls0 rs cs fr -> rs##rl = reglist ls rl.






Hint Resolve agree_eval_reg agree_eval_regs: stacking.

Preservation of agreement under various assignments: of machine registers, of local slots, of outgoing slots.





Lemma agree_set_reg:

  forall ls ls0 rs fr cs r v,

  agree ls ls0 rs fr cs ->

  mreg_within_bounds b r ->

  agree (Locmap.set (R r) v ls) ls0 (Regmap.set r v rs) fr cs.






Lemma agree_set_local:

  forall ls ls0 rs fr cs v ofs ty,

  agree ls ls0 rs fr cs ->

  slot_within_bounds f b (Local ofs ty) ->

  exists fr',

    set_slot tf fr ty (Int.signed (Int.repr (offset_of_index fe (FI_local ofs ty)))) v fr' /\

    agree (Locmap.set (S (Local ofs ty)) v ls) ls0 rs fr' cs.






Lemma agree_set_outgoing:

  forall ls ls0 rs fr cs v ofs ty,

  agree ls ls0 rs fr cs ->

  slot_within_bounds f b (Outgoing ofs ty) ->

  exists fr',

    set_slot tf fr ty (Int.signed (Int.repr (offset_of_index fe (FI_arg ofs ty)))) v fr' /\

    agree (Locmap.set (S (Outgoing ofs ty)) v ls) ls0 rs fr' cs.






Lemma agree_return_regs:

  forall ls ls0 rs fr cs rs',

  agree ls ls0 rs fr cs ->

  (forall r,

    ~In r int_callee_save_regs -> ~In r float_callee_save_regs ->

    rs' r = rs r) ->

  (forall r,

    In r int_callee_save_regs \/ In r float_callee_save_regs ->

    rs' r = ls0 (R r)) ->

  (forall r, return_regs ls0 ls (R r) = rs' r).

Agreement over callee-save registers and stack locations





Definition agree_callee_save (ls1 ls2: locset) : Prop :=

  forall l,

  match l with

  | R r => In r int_callee_save_regs \/ In r float_callee_save_regs

  | S s => True

  end ->

  ls2 l = ls1 l.




Remark mreg_not_within_bounds:

  forall r,

  ~mreg_within_bounds b r -> In r int_callee_save_regs \/ In r float_callee_save_regs.






Lemma agree_callee_save_agree:

  forall ls ls1 ls2 rs fr cs,

  agree ls ls1 rs fr cs ->

  agree_callee_save ls1 ls2 ->

  agree ls ls2 rs fr cs.






Lemma agree_callee_save_return_regs:

  forall ls1 ls2,

  agree_callee_save (return_regs ls1 ls2) ls1.






Lemma agree_callee_save_set_result:

  forall ls1 ls2 v sg,

  agree_callee_save ls1 ls2 ->

  agree_callee_save (Locmap.set (R (Conventions.loc_result sg)) v ls1) ls2.

A variant of agree used for return frames.





Definition agree_frame (ls ls0: locset) (fr: frame) (cs: list stackframe): Prop :=

  exists rs, agree ls ls0 rs fr cs.




Lemma agree_frame_agree:

  forall ls1 ls2 rs fr cs ls0,

  agree_frame ls1 ls0 fr cs ->

  agree_callee_save ls2 ls1 ->

  (forall r, rs r = ls2 (R r)) ->

  agree ls2 ls0 rs fr cs.

Correctness of saving and restoring of callee-save registers

The following lemmas show the correctness of the register saving code generated by save_callee_save: after this code has executed, the register save areas of the current frame do contain the values of the callee-save registers used by the function.





Section SAVE_CALLEE_SAVE.




Variable bound: frame_env -> Z.

Variable number: mreg -> Z.

Variable mkindex: Z -> frame_index.

Variable ty: typ.

Variable sp: val.

Variable csregs: list mreg.




Hypothesis number_inj: 

  forall r1 r2, In r1 csregs -> In r2 csregs -> r1 <> r2 -> number r1 <> number r2.

Hypothesis mkindex_valid:

  forall r, In r csregs -> number r < bound fe -> index_valid (mkindex (number r)).

Hypothesis mkindex_not_link:

  forall z, mkindex z <> FI_link.

Hypothesis mkindex_not_retaddr:

  forall z, mkindex z <> FI_retaddr.

Hypothesis mkindex_typ:

  forall z, type_of_index (mkindex z) = ty.

Hypothesis mkindex_inj:

  forall z1 z2, z1 <> z2 -> mkindex z1 <> mkindex z2.

Hypothesis mkindex_diff:

  forall r idx,

  idx <> mkindex (number r) -> index_diff (mkindex (number r)) idx.




Lemma save_callee_save_regs_correct:

  forall l k rs fr m,

  incl l csregs ->

  list_norepet l ->

  exists fr',

    star step tge 

       (State stack tf sp

         (save_callee_save_regs bound number mkindex ty fe l k) rs fr m)

    E0 (State stack tf sp k rs fr' m)

  /\ (forall r,

       In r l -> number r < bound fe ->

       index_val (mkindex (number r)) fr' = rs r)

  /\ (forall idx,

       index_valid idx ->

       (forall r,

         In r l -> number r < bound fe -> idx <> mkindex (number r)) ->

       index_val idx fr' = index_val idx fr).






End SAVE_CALLEE_SAVE.




Lemma save_callee_save_int_correct:

  forall k sp rs fr m,

  exists fr',

    star step tge 

       (State stack tf sp

         (save_callee_save_int fe k) rs fr m)

    E0 (State stack tf sp k rs fr' m)

  /\ (forall r,

       In r int_callee_save_regs ->

       index_int_callee_save r < bound_int_callee_save b ->

       index_val (FI_saved_int (index_int_callee_save r)) fr' = rs r)

  /\ (forall idx,

       index_valid idx ->

       match idx with FI_saved_int _ => False | _ => True end ->

       index_val idx fr' = index_val idx fr).






Lemma save_callee_save_float_correct:

  forall k sp rs fr m,

  exists fr',

    star step tge 

       (State stack tf sp

         (save_callee_save_float fe k) rs fr m)

    E0 (State stack tf sp k rs fr' m)

  /\ (forall r,

       In r float_callee_save_regs ->

       index_float_callee_save r < bound_float_callee_save b ->

       index_val (FI_saved_float (index_float_callee_save r)) fr' = rs r)

  /\ (forall idx,

       index_valid idx ->

       match idx with FI_saved_float _ => False | _ => True end ->

       index_val idx fr' = index_val idx fr).






Lemma save_callee_save_correct:

  forall sp k rs m ls cs,

  (forall r, rs r = ls (R r)) ->

  (forall ofs ty,

     In (S (Outgoing ofs ty)) (loc_arguments f.(Linear.fn_sig)) ->

     get_parent_slot cs ofs ty (ls (S (Outgoing ofs ty)))) ->

  exists fr',

    star step tge

       (State stack tf sp (save_callee_save fe k) rs empty_frame m)

    E0 (State stack tf sp k rs fr' m)

  /\ agree (call_regs ls) ls rs fr' cs.

The following lemmas show the correctness of the register reloading code generated by reload_callee_save: after this code has executed, all callee-save registers contain the same values they had at function entry.





Section RESTORE_CALLEE_SAVE.




Variable bound: frame_env -> Z.

Variable number: mreg -> Z.

Variable mkindex: Z -> frame_index.

Variable ty: typ.

Variable sp: val.

Variable csregs: list mreg.

Hypothesis mkindex_valid:

  forall r, In r csregs -> number r < bound fe -> index_valid (mkindex (number r)).

Hypothesis mkindex_not_link:

  forall z, mkindex z <> FI_link.

Hypothesis mkindex_not_retaddr:

  forall z, mkindex z <> FI_retaddr.

Hypothesis mkindex_typ:

  forall z, type_of_index (mkindex z) = ty.

Hypothesis number_within_bounds:

  forall r, In r csregs ->

  (number r < bound fe <-> mreg_within_bounds b r).

Hypothesis mkindex_val:

  forall ls ls0 rs fr cs r, 

  agree ls ls0 rs fr cs -> In r csregs -> number r < bound fe ->

  index_val (mkindex (number r)) fr = ls0 (R r).




Lemma restore_callee_save_regs_correct:

  forall k fr m ls0 l ls rs cs,

  incl l csregs ->

  list_norepet l -> 

  agree ls ls0 rs fr cs ->

  exists ls', exists rs',

    star step tge

      (State stack tf sp

        (restore_callee_save_regs bound number mkindex ty fe l k) rs fr m)

   E0 (State stack tf sp k rs' fr m)

  /\ (forall r, In r l -> rs' r = ls0 (R r))

  /\ (forall r, ~(In r l) -> rs' r = rs r)

  /\ agree ls' ls0 rs' fr cs.






End RESTORE_CALLEE_SAVE.




Lemma restore_int_callee_save_correct:

  forall sp k fr m ls0 ls rs cs,

  agree ls ls0 rs fr cs ->

  exists ls', exists rs',

    star step tge

       (State stack tf sp

         (restore_callee_save_int fe k) rs fr m)

    E0 (State stack tf sp k rs' fr m)

  /\ (forall r, In r int_callee_save_regs -> rs' r = ls0 (R r))

  /\ (forall r, ~(In r int_callee_save_regs) -> rs' r = rs r)

  /\ agree ls' ls0 rs' fr cs.






Lemma restore_float_callee_save_correct:

  forall sp k fr m ls0 ls rs cs,

  agree ls ls0 rs fr cs ->

  exists ls', exists rs',

    star step tge

       (State stack tf sp

          (restore_callee_save_float fe k) rs fr m)

    E0 (State stack tf sp k rs' fr m)

  /\ (forall r, In r float_callee_save_regs -> rs' r = ls0 (R r))

  /\ (forall r, ~(In r float_callee_save_regs) -> rs' r = rs r)

  /\ agree ls' ls0 rs' fr cs.






Lemma restore_callee_save_correct:

  forall sp k fr m ls0 ls rs cs,

  agree ls ls0 rs fr cs ->

  exists rs',

    star step tge

       (State stack tf sp (restore_callee_save fe k) rs fr m)

    E0 (State stack tf sp k rs' fr m)

  /\ (forall r, 

        In r int_callee_save_regs \/ In r float_callee_save_regs -> 

        rs' r = ls0 (R r))

  /\ (forall r, 

        ~(In r int_callee_save_regs) ->

        ~(In r float_callee_save_regs) ->

        rs' r = rs r).






End FRAME_PROPERTIES.

Semantic preservation

Preservation of code labels through the translation.





Section LABELS.




Remark find_label_fold_right:

  forall (A: Type) (fn: A -> Mach.code -> Mach.code) lbl,

  (forall x k, Mach.find_label lbl (fn x k) = Mach.find_label lbl k) ->  forall (args: list A) k,

  Mach.find_label lbl (List.fold_right fn k args) = Mach.find_label lbl k.






Remark find_label_save_callee_save:

  forall fe lbl k,

  Mach.find_label lbl (save_callee_save fe k) = Mach.find_label lbl k.






Remark find_label_restore_callee_save:

  forall fe lbl k,

  Mach.find_label lbl (restore_callee_save fe k) = Mach.find_label lbl k.






Lemma find_label_transl_code:

  forall fe lbl c,

  Mach.find_label lbl (transl_code fe c) =

    option_map (transl_code fe) (Linear.find_label lbl c).






Lemma transl_find_label:

  forall f tf lbl c,

  transf_function f = OK tf ->

  Linear.find_label lbl f.(Linear.fn_code) = Some c ->

  Mach.find_label lbl tf.(Mach.fn_code) = 

    Some (transl_code (make_env (function_bounds f)) c).






End LABELS.

Code inclusion property for Linear executions.





Lemma find_label_incl:

  forall lbl c c', 

  Linear.find_label lbl c = Some c' -> incl c' c.

Preservation / translation of global symbols and functions.





Lemma symbols_preserved:

  forall id, Genv.find_symbol tge id = Genv.find_symbol ge id.






Lemma functions_translated:

  forall v f,

  Genv.find_funct ge v = Some f ->

  exists tf,

  Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.

Proof

  (Genv.find_funct_transf_partial transf_fundef TRANSF).




Lemma function_ptr_translated:

  forall v f,

  Genv.find_funct_ptr ge v = Some f ->

  exists tf,

  Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.

Proof

  (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF).




Lemma sig_preserved:

  forall f tf, transf_fundef f = OK tf -> Mach.funsig tf = Linear.funsig f.






Lemma find_function_translated:

  forall f0 tf0 ls ls0 rs fr cs ros f,

  agree f0 tf0 ls ls0 rs fr cs ->

  Linear.find_function ge ros ls = Some f ->

  exists tf,

  find_function tge ros rs = Some tf /\ transf_fundef f = OK tf.






Hypothesis wt_prog: wt_program prog.




Lemma find_function_well_typed:

  forall ros ls f,

  Linear.find_function ge ros ls = Some f -> wt_fundef f.

Correctness of stack pointer relocation in operations and addressing modes.





Definition shift_sp (tf: Mach.function) (sp: val) :=

  Val.add sp (Vint (Int.repr (-tf.(fn_framesize)))).




Remark shift_offset_sp:

  forall f tf sp n v,

  transf_function f = OK tf ->

  offset_sp sp n = Some v ->

  offset_sp (shift_sp tf sp)

    (Int.add (Int.repr (fe_size (make_env (function_bounds f)))) n) = Some v.






Lemma shift_eval_operation:

  forall f tf sp op args v,

  transf_function f = OK tf ->

  eval_operation ge sp op args = Some v ->

  eval_operation tge (shift_sp tf sp) 

                 (transl_op (make_env (function_bounds f)) op) args = Some v.






Lemma shift_eval_addressing:

  forall f tf sp addr args v,

  transf_function f = OK tf ->

  eval_addressing ge sp addr args = Some v ->

  eval_addressing tge (shift_sp tf sp) 

                 (transl_addr (make_env (function_bounds f)) addr) args =

  Some v.

Preservation of the arguments to an external call.





Section EXTERNAL_ARGUMENTS.




Variable cs: list Machabstr.stackframe.

Variable ls: locset.

Variable rs: regset.

Variable sg: signature.




Hypothesis AG1: forall r, rs r = ls (R r).

Hypothesis AG2: forall (ofs : Z) (ty : typ),

      In (S (Outgoing ofs ty)) (loc_arguments sg) ->

      get_parent_slot cs ofs ty (ls (S (Outgoing ofs ty))).




Lemma transl_external_arguments_rec:

  forall locs,

  incl locs (loc_arguments sg) ->

  extcall_args (parent_function cs) rs (parent_frame cs) locs ls##locs.






Lemma transl_external_arguments:

  extcall_arguments (parent_function cs) rs (parent_frame cs) sg (ls ## (loc_arguments sg)).






End EXTERNAL_ARGUMENTS.

The proof of semantic preservation relies on simulation diagrams of the following form:

           st1 --------------- st2
            |                   |
           t|                  +|t
            |                   |
            v                   v
           st1'--------------- st2'

Matching between source and target states is defined by match_states below. It implies:

Agreement between, on the Linear side, the location sets ls and parent_locset s of the current function and its caller, and on the Mach side the register set rs, the frame fr and the caller's frame parent_frame ts.
Inclusion between the Linear code c and the code of the function f being executed.
Well-typedness of f.





Inductive match_stacks: list Linear.stackframe -> list Machabstr.stackframe -> Prop :=

  | match_stacks_nil:

      match_stacks nil nil

  | match_stacks_cons:

      forall f sp c ls tf fr s ts,

      match_stacks s ts ->

      transf_function f = OK tf ->

      wt_function f ->

      agree_frame f tf ls (parent_locset s) fr ts ->

      incl c (Linear.fn_code f) ->

      match_stacks

       (Linear.Stackframe f sp ls c :: s)

       (Machabstr.Stackframe tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) c) fr :: ts).




Inductive match_states: Linear.state -> Machabstr.state -> Prop :=

  | match_states_intro:

      forall s f sp c ls m ts tf rs fr

        (STACKS: match_stacks s ts)

        (TRANSL: transf_function f = OK tf)

        (WTF: wt_function f)

        (AG: agree f tf ls (parent_locset s) rs fr ts)

        (INCL: incl c (Linear.fn_code f)),

      match_states (Linear.State s f sp c ls m)

                   (Machabstr.State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) c) rs fr m)

  | match_states_call:

      forall s f ls m ts tf rs

        (STACKS: match_stacks s ts)

        (TRANSL: transf_fundef f = OK tf)

        (WTF: wt_fundef f)

        (AG1: forall r, rs r = ls (R r))

        (AG2: forall ofs ty, 

                In (S (Outgoing ofs ty)) (loc_arguments (Linear.funsig f)) ->

                get_parent_slot ts ofs ty (ls (S (Outgoing ofs ty))))

        (AG3: agree_callee_save ls (parent_locset s)),

      match_states (Linear.Callstate s f ls m)

                   (Machabstr.Callstate ts tf rs m)

  | match_states_return:

      forall s ls m ts rs

        (STACKS: match_stacks s ts)

        (AG1: forall r, rs r = ls (R r))

        (AG2: agree_callee_save ls (parent_locset s)),

      match_states (Linear.Returnstate s ls m)

                   (Machabstr.Returnstate ts rs m).




Theorem transf_step_correct:

  forall s1 t s2, Linear.step ge s1 t s2 ->

  forall s1' (MS: match_states s1 s1'),

  exists s2', plus step tge s1' t s2' /\ match_states s2 s2'.






Lemma transf_initial_states:

  forall st1, Linear.initial_state prog st1 ->

  exists st2, Machabstr.initial_state tprog st2 /\ match_states st1 st2.






Lemma transf_final_states:

  forall st1 st2 r, 

  match_states st1 st2 -> Linear.final_state st1 r -> Machabstr.final_state st2 r.






Theorem transf_program_correct:

  forall (beh: program_behavior), not_wrong beh ->

  Linear.exec_program prog beh -> Machabstr.exec_program tprog beh.






End PRESERVATION.