Library Machabstr2concr

Simulation between the two semantics for the Mach language.





Require Import Coqlib.

Require Import Maps.

Require Import AST.

Require Import Integers.

Require Import Values.

Require Import Mem.

Require Import Events.

Require Import Globalenvs.

Require Import Smallstep.

Require Import Op.

Require Import Locations.

Require Import Mach.

Require Import Machtyping.

Require Import Machabstr.

Require Import Machconcr.

Require Import Asmgenretaddr.

Two semantics were defined for the Mach intermediate language:

The concrete semantics (file Mach), where the whole activation record resides in memory and the Mgetstack, Msetstack and Mgetparent are interpreted as sp-relative memory accesses.
The abstract semantics (file Machabstr), where the activation record is split in two parts: the Cminor stack data, resident in memory, and the frame information, residing not in memory but in additional evaluation environments.

In this file, we show a simulation result between these semantics: if a program executes with some behaviour beh in the abstract semantics, it also executes with the same behaviour in the concrete semantics. This result bridges the correctness proof in file Stackingproof (which uses the abstract Mach semantics as output) and that in file Asmgenproof (which uses the concrete Mach semantics as input).





Remark size_type_chunk:

  forall ty, size_chunk (chunk_of_type ty) = AST.typesize ty.

Agreement between frames and memory-resident activation records

Agreement for one frame





Section FRAME_MATCH.




Variable f: function.

Hypothesis wt_f: wt_function f.

The core idea of the simulation proof is that for all active functions, the memory-allocated activation record, in the concrete semantics, contains the same data as the Cminor stack block (at positive offsets) and the frame of the function (at negative offsets) in the abstract semantics

This intuition (activation record = Cminor stack data + frame) is formalized by the following predicate frame_match fr sp base mm ms. fr is a frame and mm the current memory state in the abstract semantics. ms is the current memory state in the concrete semantics. The stack pointer is Vptr sp base in both semantics.





Inductive frame_match (fr: frame)

                      (sp: block) (base: int) 

                      (mm ms: mem) : Prop :=

  frame_match_intro:

    valid_block ms sp ->

    low_bound mm sp = 0 ->

    low_bound ms sp = -f.(fn_framesize) ->

    high_bound ms sp >= 0 ->

    base = Int.repr (-f.(fn_framesize)) ->

    (forall ty ofs,

       -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 -> (4 | ofs) ->

       load (chunk_of_type ty) ms sp ofs = Some(fr ty ofs)) ->

    frame_match fr sp base mm ms.

The following two innocuous-looking lemmas are the key results showing that sp-relative memory accesses in the concrete semantics behave like the direct frame accesses in the abstract semantics. First, a value v that has type ty is preserved when stored in memory with chunk chunk_of_type ty, then read back with the same chunk. The typing hypothesis is crucial here: for instance, a float value reads back as Vundef when stored and load with chunk Mint32.





Lemma load_result_ty:

  forall v ty,

  Val.has_type v ty -> Val.load_result (chunk_of_type ty) v = v.

Second, computations of sp-relative offsets using machine arithmetic (as done in the concrete semantics) never overflows and behaves identically to the offset computations using exact arithmetic (as done in the abstract semantics).





Lemma int_add_no_overflow:

  forall x y,

  Int.min_signed <= Int.signed x + Int.signed y <= Int.max_signed ->

  Int.signed (Int.add x y) = Int.signed x + Int.signed y.

Given matching frames and activation records, loading from the activation record (in the concrete semantics) behaves identically to reading the corresponding slot from the frame (in the abstract semantics).





Lemma frame_match_load_stack:

  forall fr sp base mm ms ty ofs,

  frame_match fr sp base mm ms ->

  0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) ->

  (4 | Int.signed ofs) ->

  load_stack ms (Vptr sp base) ty ofs = 

  Some (fr ty (Int.signed ofs - f.(fn_framesize))).






Lemma frame_match_get_slot:

  forall fr sp base mm ms ty ofs v,

  frame_match fr sp base mm ms ->

  get_slot f fr ty (Int.signed ofs) v ->

  load_stack ms (Vptr sp base) ty ofs = Some v.

Assigning a value to a frame slot (in the abstract semantics) corresponds to storing this value in the activation record (in the concrete semantics). Moreover, agreement between frames and activation records is preserved.





Lemma frame_match_store_stack:

  forall fr sp base mm ms ty ofs v,

  frame_match fr sp base mm ms ->

  0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) ->

  (4 | Int.signed ofs) ->

  Val.has_type v ty ->

  Mem.extends mm ms ->

  exists ms',

    store_stack ms (Vptr sp base) ty ofs v = Some ms' /\

    frame_match (update ty (Int.signed ofs - f.(fn_framesize)) v fr) sp base mm ms' /\

    Mem.extends mm ms'.






Lemma frame_match_set_slot:

  forall fr sp base mm ms ty ofs v fr',

  frame_match fr sp base mm ms ->

  set_slot f fr ty (Int.signed ofs) v fr' ->

  Val.has_type v ty ->

  Mem.extends mm ms ->

  exists ms',

    store_stack ms (Vptr sp base) ty ofs v = Some ms' /\

    frame_match fr' sp base mm ms' /\

    Mem.extends mm ms'.

Agreement is preserved by stores within blocks other than the one pointed to by sp.





Lemma frame_match_store_other:

  forall fr sp base mm ms chunk b ofs v ms',

  frame_match fr sp base mm ms ->

  store chunk ms b ofs v = Some ms' ->

  sp <> b ->

  frame_match fr sp base mm ms'.

Agreement is preserved by parallel stores in the Machabstr and the Machconcr semantics.





Lemma frame_match_store:

  forall fr sp base mm ms chunk b ofs v mm' ms',

  frame_match fr sp base mm ms ->

  store chunk mm b ofs v = Some mm' ->

  store chunk ms b ofs v = Some ms' ->

  frame_match fr sp base mm' ms'.

Memory allocation of the Cminor stack data block (in the abstract semantics) and of the whole activation record (in the concrete semantics) return memory states that agree according to frame_match. Moreover, frame_match relations over already allocated blocks remain true.





Lemma frame_match_new:

  forall mm ms mm' ms' sp sp',

  mm.(nextblock) = ms.(nextblock) ->

  alloc mm 0 f.(fn_stacksize) = (mm', sp) ->

  alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms', sp') ->

  sp = sp' /\

  frame_match empty_frame sp (Int.repr (-f.(fn_framesize))) mm' ms'.






Lemma frame_match_alloc:

  forall mm ms fr sp base lom him los his mm' ms' bm bs,

  mm.(nextblock) = ms.(nextblock) ->

  frame_match fr sp base mm ms ->

  alloc mm lom him = (mm', bm) ->

  alloc ms los his = (ms', bs) ->

  frame_match fr sp base mm' ms'.

frame_match relations are preserved by freeing a block other than the one pointed to by sp.





Lemma frame_match_free:

  forall fr sp base mm ms b,

  frame_match fr sp base mm ms ->

  sp <> b ->

  frame_match fr sp base (free mm b) (free ms b).






End FRAME_MATCH.

Accounting for the return address and back link





Section EXTEND_FRAME.




Variable f: function.

Hypothesis wt_f: wt_function f.

Variable cs: list Machconcr.stackframe.




Definition extend_frame (fr: frame) : frame :=

  update Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize)) (parent_ra cs)

    (update Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize)) (parent_sp cs)

      fr).




Lemma get_slot_extends:

  forall fr ty ofs v,

  get_slot f fr ty ofs v ->

  get_slot f (extend_frame fr) ty ofs v.






Lemma update_commut:

  forall ty1 ofs1 v1 ty2 ofs2 v2 fr,

  ofs1 + AST.typesize ty1 <= ofs2 \/

  ofs2 + AST.typesize ty2 <= ofs1 ->

  update ty1 ofs1 v1 (update ty2 ofs2 v2 fr) =

  update ty2 ofs2 v2 (update ty1 ofs1 v1 fr).






Lemma set_slot_extends:

  forall fr ty ofs v fr',

  set_slot f fr ty ofs v fr' ->

  set_slot f (extend_frame fr) ty ofs v (extend_frame fr').






Lemma frame_match_load_link:

  forall fr sp base mm ms,

  frame_match f (extend_frame fr) sp base mm ms ->

  load_stack ms (Vptr sp base) Tint f.(fn_link_ofs) = Some (parent_sp cs).






Lemma frame_match_load_retaddr:

  forall fr sp base mm ms,

  frame_match f (extend_frame fr) sp base mm ms ->

  load_stack ms (Vptr sp base) Tint f.(fn_retaddr_ofs) = Some (parent_ra cs).






Lemma frame_match_function_entry:

  forall mm ms mm' ms1 sp sp',

  extends mm ms ->

  alloc mm 0 f.(fn_stacksize) = (mm', sp) ->

  alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms1, sp') ->

  Val.has_type (parent_sp cs) Tint ->

  Val.has_type (parent_ra cs) Tint ->

  let base := Int.repr (-f.(fn_framesize)) in

  exists ms2, exists ms3,

  sp = sp' /\

  store_stack ms1 (Vptr sp base) Tint f.(fn_link_ofs) (parent_sp cs) = Some ms2 /\

  store_stack ms2 (Vptr sp base) Tint f.(fn_retaddr_ofs) (parent_ra cs) = Some ms3 /\

  frame_match f (extend_frame empty_frame) sp base mm' ms3 /\

  extends mm' ms3.






End EXTEND_FRAME.

Invariant for stacks





Section SIMULATION.




Variable p: program.

Let ge := Genv.globalenv p.

The match_stacks predicate relates a Machabstr call stack with the corresponding Machconcr stack. In addition to enforcing the frame_match predicate for each stack frame, we also enforce:

Proper chaining of activation record on the Machconcr side.
Preservation of the return address stored at the bottom of the activation record.
Separation between the memory blocks holding the activation records: their addresses increase strictly from caller to callee.





Definition stack_below (ts: list Machconcr.stackframe) (b: block) : Prop :=

  match parent_sp ts with

  | Vptr sp base' => sp < b

  | _ => False

  end.




Inductive match_stacks: 

      list Machabstr.stackframe -> list Machconcr.stackframe ->

      mem -> mem -> Prop :=

  | match_stacks_nil: forall mm ms,

      match_stacks nil nil mm ms

  | match_stacks_cons: forall fb sp base c fr s f ra ts mm ms,

      Genv.find_funct_ptr ge fb = Some (Internal f) ->

      wt_function f ->

      frame_match f (extend_frame f ts fr) sp base mm ms ->

      stack_below ts sp ->

      Val.has_type ra Tint ->

      match_stacks s ts mm ms ->

      match_stacks (Machabstr.Stackframe f (Vptr sp base) c fr :: s)

                   (Machconcr.Stackframe fb (Vptr sp base) ra c :: ts)

                   mm ms.

If match_stacks holds, a lookup in the parent frame in the Machabstr semantics corresponds to two memory loads in the Machconcr semantics, one to load the pointer to the parent's activation record, the second to read within this record.





Lemma match_stacks_get_parent:

  forall s ts mm ms ty ofs v,

  match_stacks s ts mm ms ->

  get_slot (parent_function s) (parent_frame s) ty (Int.signed ofs) v ->

  load_stack ms (Machconcr.parent_sp ts) ty ofs = Some v.

Preservation of the match_stacks invariant by various kinds of memory stores.





Remark stack_below_trans:

  forall ts b b', 

  stack_below ts b -> b <= b' -> stack_below ts b'.






Lemma match_stacks_store_other:

  forall s ts ms mm,

  match_stacks s ts mm ms ->

  forall chunk b ofs v ms',

  store chunk ms b ofs v = Some ms' ->

  stack_below ts b ->

  match_stacks s ts mm ms'.






Lemma match_stacks_store_slot:

  forall s ts ms mm,

  match_stacks s ts mm ms ->

  forall ty ofs v ms' b i,

  stack_below ts b ->

  store_stack ms (Vptr b i) ty ofs v = Some ms' ->

  match_stacks s ts mm ms'.






Lemma match_stacks_store:

  forall s ts ms mm,

  match_stacks s ts mm ms ->

  forall chunk b ofs v mm' ms',

  store chunk mm b ofs v = Some mm' ->

  store chunk ms b ofs v = Some ms' ->

  match_stacks s ts mm' ms'.






Lemma match_stacks_alloc:

  forall s ts ms mm,

  match_stacks s ts mm ms ->

  forall lom him mm' bm los his ms' bs,

  mm.(nextblock) = ms.(nextblock) ->

  alloc mm lom him = (mm', bm) ->

  alloc ms los his = (ms', bs) ->

  match_stacks s ts mm' ms'.






Lemma match_stacks_free:

  forall s ts ms mm,

  match_stacks s ts mm ms ->

  forall b,

  stack_below ts b ->

  match_stacks s ts (Mem.free mm b) (Mem.free ms b).






Lemma match_stacks_function_entry:

  forall s ts mm ms lom him mm' los his ms' stk,

  match_stacks s ts mm ms ->

  alloc mm lom him = (mm', stk) ->

  alloc ms los his = (ms', stk) ->

  match_stacks s ts mm' ms' /\ stack_below ts stk.

Invariant between states.

The match_state predicate relates a Machabstr state with a Machconcr state. In addition to match_stacks between the stacks, we ask that

The Machabstr frame is properly stored in the activation record, as characterized by frame_match.
The Machconcr memory state extends the Machabstr memory state, in the sense of the Mem.extends relation defined in module Mem.





Inductive match_states:

            Machabstr.state -> Machconcr.state -> Prop :=

  | match_states_intro:

      forall s f sp base c rs fr mm ts fb ms

        (STACKS: match_stacks s ts mm ms)

        (FM: frame_match f (extend_frame f ts fr) sp base mm ms)

        (BELOW: stack_below ts sp)

        (MEXT: Mem.extends mm ms)

        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)),

      match_states (Machabstr.State s f (Vptr sp base) c rs fr mm)

                   (Machconcr.State ts fb (Vptr sp base) c rs ms)

  | match_states_call:

      forall s f rs mm ts fb ms

        (STACKS: match_stacks s ts mm ms)

        (MEXT: Mem.extends mm ms)

        (FIND: Genv.find_funct_ptr ge fb = Some f),

      match_states (Machabstr.Callstate s f rs mm)

                   (Machconcr.Callstate ts fb rs ms)

  | match_states_return:

      forall s rs mm ts ms

        (STACKS: match_stacks s ts mm ms)

        (MEXT: Mem.extends mm ms),

      match_states (Machabstr.Returnstate s rs mm)

                   (Machconcr.Returnstate ts rs ms).

The proof of simulation

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

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

The precondition is matching between the initial states st1 and st2, as usual, plus the fact that st1 is well-typed in the sense of predicate wt_state from module Machtyping. The postcondition is matching between the final states st1' and st2'. The well-typedness of st2 is not part of the postcondition, since it follows from that of st1 if the program is well-typed. (See the subject reduction property in module Machtyping.)





Lemma find_function_find_function_ptr:

  forall ros rs f',

  find_function ge ros rs = Some f' ->

  exists fb', Genv.find_funct_ptr ge fb' = Some f' /\ find_function_ptr ge ros rs = Some fb'.

Preservation of arguments to external functions.





Lemma transl_extcall_arguments:

  forall rs s sg args ts m ms,

  Machabstr.extcall_arguments (parent_function s) rs (parent_frame s) sg args ->

  match_stacks s ts m ms ->

  extcall_arguments rs ms (parent_sp ts) sg args.






Hypothesis wt_prog: wt_program p.




Theorem step_equiv:

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

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

  exists s2', Machconcr.step ge s1' t s2' /\ match_states s2 s2'.






Lemma equiv_initial_states:

  forall st1, Machabstr.initial_state p st1 ->

  exists st2, Machconcr.initial_state p st2 /\ match_states st1 st2 /\ wt_state st1.






Lemma equiv_final_states:

  forall st1 st2 r, 

  match_states st1 st2 /\ wt_state st1 -> Machabstr.final_state st1 r -> Machconcr.final_state st2 r.






Theorem exec_program_equiv:

  forall (beh: program_behavior), not_wrong beh ->

  Machabstr.exec_program p beh -> Machconcr.exec_program p beh.






End SIMULATION.