Library Cminorgenproof

Correctness proof for Cminor generation.





Require Import FSets.

Require Import Coqlib.

Require Import Errors.

Require Import Maps.

Require Import AST.

Require Import Integers.

Require Import Floats.

Require Import Values.

Require Import Mem.

Require Import Events.

Require Import Globalenvs.

Require Import Smallstep.

Require Import Csharpminor.

Require Import Op.

Require Import Cminor.

Require Import Cminorgen.




Open Local Scope error_monad_scope.




Section TRANSLATION.




Variable prog: Csharpminor.program.

Variable tprog: program.

Hypothesis TRANSL: transl_program prog = OK tprog.

Let ge : Csharpminor.genv := Genv.globalenv prog.

Let gvare : gvarenv := global_var_env prog.

Let gve := (ge, gvare).

Let gce : compilenv := build_global_compilenv prog.

Let tge: genv := Genv.globalenv tprog.




Lemma symbols_preserved:

  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.

Proof (Genv.find_symbol_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL).




Lemma function_ptr_translated:

  forall (b: block) (f: Csharpminor.fundef),

  Genv.find_funct_ptr ge b = Some f ->

  exists tf,

  Genv.find_funct_ptr tge b = Some tf /\ transl_fundef gce f = OK tf.

Proof (Genv.find_funct_ptr_transf_partial2 (transl_fundef gce) transl_globvar TRANSL).




Lemma functions_translated:

  forall (v: val) (f: Csharpminor.fundef),

  Genv.find_funct ge v = Some f ->

  exists tf,

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

Proof (Genv.find_funct_transf_partial2 (transl_fundef gce) transl_globvar TRANSL).




Lemma sig_preserved_body:

  forall f tf cenv size,

  transl_funbody cenv size f = OK tf -> 

  tf.(fn_sig) = f.(Csharpminor.fn_sig).






Lemma sig_preserved:

  forall f tf,

  transl_fundef gce f = OK tf -> 

  Cminor.funsig tf = Csharpminor.funsig f.






Definition global_compilenv_match (ce: compilenv) (gv: gvarenv) : Prop :=

  forall id,

  match ce!!id with

  | Var_global_scalar chunk => gv!id = Some (Vscalar chunk)

  | Var_global_array => True

  | _ => False

  end.




Lemma global_compilenv_charact:

  global_compilenv_match gce gvare.

Correspondence between Csharpminor's and Cminor's environments and memory states

In Csharpminor, every variable is stored in a separate memory block. In the corresponding Cminor code, some of these variables reside in the local variable environment; others are sub-blocks of the stack data block. We capture these changes in memory via a memory injection f:

f b = None means that the Csharpminor block b no longer exist in the execution of the generated Cminor code. This corresponds to a Csharpminor local variable translated to a Cminor local variable.
f b = Some(b', ofs) means that Csharpminor block b corresponds to a sub-block of Cminor block b at offset ofs.

A memory injection f defines a relation val_inject f between values and a relation mem_inject f between memory states. These relations, defined in file Memory, will be used intensively in our proof of simulation between Csharpminor and Cminor executions.

In the remainder of this section, we define relations between Csharpminor and Cminor environments and call stacks.

Matching for a Csharpminor variable id.

If this variable is mapped to a Cminor local variable, the corresponding Csharpminor memory block b must no longer exist in Cminor (f b = None). Moreover, the content of block b must match the value of id found in the Cminor local environment te.
If this variable is mapped to a sub-block of the Cminor stack data at offset ofs, the address of this variable in Csharpminor Vptr b Int.zero must match the address of the sub-block Vptr sp (Int.repr ofs).





Inductive match_var (f: meminj) (id: ident)

                    (e: Csharpminor.env) (m: mem) (te: env) (sp: block) : 

                    var_info -> Prop :=

  | match_var_local:

      forall chunk b v v',

      PTree.get id e = Some (b, Vscalar chunk) ->

      Mem.load chunk m b 0 = Some v ->

      f b = None ->

      PTree.get id te = Some v' ->

      val_inject f v v' ->

      match_var f id e m te sp (Var_local chunk)

  | match_var_stack_scalar:

      forall chunk ofs b,

      PTree.get id e = Some (b, Vscalar chunk) ->

      val_inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) ->

      match_var f id e m te sp (Var_stack_scalar chunk ofs)

  | match_var_stack_array:

      forall ofs sz b,

      PTree.get id e = Some (b, Varray sz) ->

      val_inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) ->

      match_var f id e m te sp (Var_stack_array ofs)

  | match_var_global_scalar:

      forall chunk,

      PTree.get id e = None ->

      PTree.get id gvare = Some (Vscalar chunk) ->

      match_var f id e m te sp (Var_global_scalar chunk)

  | match_var_global_array:

      PTree.get id e = None ->

      match_var f id e m te sp (Var_global_array).

Matching between a Csharpminor environment e and a Cminor environment te. The lo and hi parameters delimit the range of addresses for the blocks referenced from te.





Record match_env (f: meminj) (cenv: compilenv)

                 (e: Csharpminor.env) (m: mem) (te: env) (sp: block)

                 (lo hi: Z) : Prop :=

  mk_match_env {

Each variable mentioned in the compilation environment must match as defined above.


    me_vars:

      forall id, match_var f id e m te sp (PMap.get id cenv);

The range lo, hi must not be empty.


    me_low_high:

      lo <= hi;

Every block appearing in the Csharpminor environment e must be in the range lo, hi.


    me_bounded:

      forall id b lv, PTree.get id e = Some(b, lv) -> lo <= b < hi;

Distinct Csharpminor local variables must be mapped to distinct blocks.


    me_inj:

      forall id1 b1 lv1 id2 b2 lv2,

      PTree.get id1 e = Some(b1, lv1) ->

      PTree.get id2 e = Some(b2, lv2) ->

      id1 <> id2 -> b1 <> b2;

All blocks mapped to sub-blocks of the Cminor stack data must be images of variables from the Csharpminor environment e


    me_inv:

      forall b delta,

      f b = Some(sp, delta) ->

      exists id, exists lv, PTree.get id e = Some(b, lv);

All Csharpminor blocks below lo (i.e. allocated before the blocks referenced from e) must map to blocks that are below sp (i.e. allocated before the stack data for the current Cminor function).


    me_incr:

      forall b tb delta,

      f b = Some(tb, delta) -> b < lo -> tb < sp

  }.

Global environments match if the memory injection f leaves unchanged the references to global symbols and functions.





Record match_globalenvs (f: meminj) : Prop := 

  mk_match_globalenvs {

    mg_symbols:

      forall id b,

      Genv.find_symbol ge id = Some b ->

      f b = Some (b, 0) /\ Genv.find_symbol tge id = Some b;

    mg_functions:

      forall b, b < 0 -> f b = Some(b, 0)

  }.

Call stacks represent abstractly the execution state of the current Csharpminor and Cminor functions, as well as the states of the calling functions. A call stack is a list of frames, each frame collecting information on the current execution state of a Csharpminor function and its Cminor translation.





Record frame : Type :=

  mkframe {

    fr_cenv: compilenv;

    fr_e: Csharpminor.env;

    fr_te: env;

    fr_sp: block;

    fr_low: Z;

    fr_high: Z

  }.




Definition callstack : Type := list frame.

Matching of call stacks imply matching of environments for each of the frames, plus matching of the global environments, plus disjointness conditions over the memory blocks allocated for local variables and Cminor stack data.





Inductive match_callstack: meminj -> callstack -> Z -> Z -> mem -> Prop :=

  | mcs_nil:

      forall f bound tbound m,

      match_globalenvs f ->

      match_callstack f nil bound tbound m

  | mcs_cons:

      forall f cenv e te sp lo hi cs bound tbound m,

      hi <= bound ->

      sp < tbound ->

      match_env f cenv e m te sp lo hi ->

      match_callstack f cs lo sp m ->

      match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m.

The remainder of this section is devoted to showing preservation of the match_callstack invariant under various assignments and memory stores. First: preservation by memory stores to ``mapped'' blocks (block that have a counterpart in the Cminor execution).





Lemma match_env_store_mapped:

  forall f cenv e m1 m2 te sp lo hi chunk b ofs v,

  f b <> None ->

  store chunk m1 b ofs v = Some m2 ->

  match_env f cenv e m1 te sp lo hi ->

  match_env f cenv e m2 te sp lo hi.






Lemma match_callstack_mapped:

  forall f cs bound tbound m1,

  match_callstack f cs bound tbound m1 ->

  forall chunk b ofs v m2,

  f b <> None ->

  store chunk m1 b ofs v = Some m2 ->

  match_callstack f cs bound tbound m2.

Preservation by assignment to a Csharpminor variable that is translated to a Cminor local variable. The value being assigned must be normalized with respect to the memory chunk of the variable, in the following sense.





Lemma match_env_store_local:

  forall f cenv e m1 m2 te sp lo hi id b chunk v tv,

  e!id = Some(b, Vscalar chunk) ->

  val_inject f (Val.load_result chunk v) tv ->

  store chunk m1 b 0 v = Some m2 ->

  match_env f cenv e m1 te sp lo hi ->

  match_env f cenv e m2 (PTree.set id tv te) sp lo hi.






Lemma match_env_store_above:

  forall f cenv e m1 m2 te sp lo hi chunk b v,

  store chunk m1 b 0 v = Some m2 ->

  hi <= b ->

  match_env f cenv e m1 te sp lo hi ->

  match_env f cenv e m2 te sp lo hi.






Lemma match_callstack_store_above:

  forall f cs bound tbound m1,

  match_callstack f cs bound tbound m1 ->

  forall chunk b v m2,

  store chunk m1 b 0 v = Some m2 ->

  bound <= b ->

  match_callstack f cs bound tbound m2.






Lemma match_callstack_store_local:

  forall f cenv e te sp lo hi cs bound tbound m1 m2 id b chunk v tv,

  e!id = Some(b, Vscalar chunk) ->

  val_inject f (Val.load_result chunk v) tv ->

  store chunk m1 b 0 v = Some m2 ->

  match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m1 ->

  match_callstack f (mkframe cenv e (PTree.set id tv te) sp lo hi :: cs) bound tbound m2.

A variant of match_callstack_store_local where the Cminor environment te already associates to id a value that matches the assigned value. In this case, match_callstack is preserved even if no assignment takes place on the Cminor side.





Lemma match_env_extensional:

  forall f cenv e m te1 sp lo hi,

  match_env f cenv e m te1 sp lo hi ->

  forall te2,

  (forall id, te2!id = te1!id) ->

  match_env f cenv e m te2 sp lo hi.






Lemma match_callstack_store_local_unchanged:

  forall f cenv e te sp lo hi cs bound tbound m1 m2 id b chunk v tv,

  e!id = Some(b, Vscalar chunk) ->

  val_inject f (Val.load_result chunk v) tv ->

  store chunk m1 b 0 v = Some m2 ->

  te!id = Some tv ->

  match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m1 ->

  match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m2.

Preservation of match_callstack by freeing all blocks allocated for local variables at function entry (on the Csharpminor side).





Lemma match_callstack_incr_bound:

  forall f cs bound tbound m,

  match_callstack f cs bound tbound m ->

  forall bound' tbound',

  bound <= bound' -> tbound <= tbound' ->

  match_callstack f cs bound' tbound' m.






Lemma load_freelist:

  forall fbl chunk m b ofs,

  (forall b', In b' fbl -> b' <> b) -> 

  load chunk (free_list m fbl) b ofs = load chunk m b ofs.






Lemma match_env_freelist:

  forall f cenv e m te sp lo hi fbl,

  match_env f cenv e m te sp lo hi ->

  (forall b, In b fbl -> hi <= b) ->

  match_env f cenv e (free_list m fbl) te sp lo hi.






Lemma match_callstack_freelist_rec:

  forall f cs bound tbound m,

  match_callstack f cs bound tbound m ->

  forall fbl,

  (forall b, In b fbl -> bound <= b) ->

  match_callstack f cs bound tbound (free_list m fbl).






Lemma blocks_of_env_charact:

  forall b e,

  In b (blocks_of_env e) <->

  exists id, exists lv, e!id = Some(b, lv).






Lemma match_callstack_freelist:

  forall f cenv e te sp lo hi cs bound tbound m tm,

  mem_inject f m tm ->

  match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m ->

  match_callstack f cs bound tbound (free_list m (blocks_of_env e))

  /\ mem_inject f (free_list m (blocks_of_env e)) (free tm sp).

Preservation of match_callstack when allocating a block for a local variable on the Csharpminor side.





Lemma load_from_alloc_is_undef:

  forall m1 chunk m2 b,

  alloc m1 0 (size_chunk chunk) = (m2, b) ->

  load chunk m2 b 0 = Some Vundef.






Lemma match_env_alloc_same:

  forall m1 lv m2 b info f1 cenv1 e1 te sp lo id data tv,

  alloc m1 0 (sizeof lv) = (m2, b) ->

  match info with

    | Var_local chunk => data = None /\ lv = Vscalar chunk

    | Var_stack_scalar chunk pos => data = Some(sp, pos) /\ lv = Vscalar chunk

    | Var_stack_array pos => data = Some(sp, pos) /\ exists sz, lv = Varray sz

    | Var_global_scalar chunk => False

    | Var_global_array => False

  end ->

  match_env f1 cenv1 e1 m1 te sp lo m1.(nextblock) ->

  te!id = Some tv ->

  e1!id = None ->

  let f2 := extend_inject b data f1 in

  let cenv2 := PMap.set id info cenv1 in

  let e2 := PTree.set id (b, lv) e1 in

  inject_incr f1 f2 ->

  match_env f2 cenv2 e2 m2 te sp lo m2.(nextblock).






Lemma match_env_alloc_other:

  forall f1 cenv e m1 m2 te sp lo hi chunk b data,

  alloc m1 0 (sizeof chunk) = (m2, b) ->

  match data with None => True | Some (b', delta') => sp < b' end ->

  hi <= m1.(nextblock) ->

  match_env f1 cenv e m1 te sp lo hi ->

  let f2 := extend_inject b data f1 in

  inject_incr f1 f2 ->

  match_env f2 cenv e m2 te sp lo hi.






Lemma match_callstack_alloc_other:

  forall f1 cs bound tbound m1,

  match_callstack f1 cs bound tbound m1 ->

  forall lv m2 b data,

  alloc m1 0 (sizeof lv) = (m2, b) ->

  match data with None => True | Some (b', delta') => tbound <= b' end ->

  bound <= m1.(nextblock) ->

  let f2 := extend_inject b data f1 in

  inject_incr f1 f2 ->

  match_callstack f2 cs bound tbound m2.






Lemma match_callstack_alloc_left:

  forall m1 lv m2 b info f1 cenv1 e1 te sp lo id data cs tv tbound,

  alloc m1 0 (sizeof lv) = (m2, b) ->

  match info with

    | Var_local chunk => data = None /\ lv = Vscalar chunk

    | Var_stack_scalar chunk pos => data = Some(sp, pos) /\ lv = Vscalar chunk

    | Var_stack_array pos => data = Some(sp, pos) /\ exists sz, lv = Varray sz

    | Var_global_scalar chunk => False

    | Var_global_array => False

  end ->

  match_callstack f1 (mkframe cenv1 e1 te sp lo m1.(nextblock) :: cs) m1.(nextblock) tbound m1 ->

  te!id = Some tv ->

  e1!id = None ->

  let f2 := extend_inject b data f1 in

  let cenv2 := PMap.set id info cenv1 in

  let e2 := PTree.set id (b, lv) e1 in

  inject_incr f1 f2 ->

  match_callstack f2 (mkframe cenv2 e2 te sp lo m2.(nextblock) :: cs) m2.(nextblock) tbound m2.






Lemma match_callstack_alloc_right:

  forall f cs bound tm1 m tm2 lo hi b,

  alloc tm1 lo hi = (tm2, b) ->

  match_callstack f cs bound tm1.(nextblock) m ->

  match_callstack f cs bound tm2.(nextblock) m.






Lemma match_env_alloc:

  forall m1 l h m2 b tm1 tm2 tb f1 ce e te sp lo hi,

  alloc m1 l h = (m2, b) ->

  alloc tm1 l h = (tm2, tb) ->

  match_env f1 ce e m1 te sp lo hi ->

  hi <= m1.(nextblock) ->

  sp < tm1.(nextblock) ->

  let f2 := extend_inject b (Some(tb, 0)) f1 in

  inject_incr f1 f2 ->

  match_env f2 ce e m2 te sp lo hi.






Lemma match_callstack_alloc_rec:

  forall f1 cs bound tbound m1,

  match_callstack f1 cs bound tbound m1 ->

  forall l h m2 b tm1 tm2 tb,

  alloc m1 l h = (m2, b) ->

  alloc tm1 l h = (tm2, tb) ->

  bound <= m1.(nextblock) ->

  tbound <= tm1.(nextblock) ->

  let f2 := extend_inject b (Some(tb, 0)) f1 in

  inject_incr f1 f2 ->

  match_callstack f2 cs bound tbound m2.






Lemma match_callstack_alloc:

  forall f1 cs m1 tm1 l h m2 b tm2 tb,

  match_callstack f1 cs m1.(nextblock) tm1.(nextblock) m1 ->

  alloc m1 l h = (m2, b) ->

  alloc tm1 l h = (tm2, tb) ->

  let f2 := extend_inject b (Some(tb, 0)) f1 in

  inject_incr f1 f2 ->

  match_callstack f2 cs m2.(nextblock) tm2.(nextblock) m2.

match_callstack implies match_globalenvs.





Lemma match_callstack_match_globalenvs:

  forall f cs bound tbound m,

  match_callstack f cs bound tbound m ->

  match_globalenvs f.

Correctness of Cminor construction functions





Remark val_inject_val_of_bool:

  forall f b, val_inject f (Val.of_bool b) (Val.of_bool b).






Remark val_inject_eval_compare_mismatch:

  forall f c v,  

  eval_compare_mismatch c = Some v ->

  val_inject f v v.






Remark val_inject_eval_compare_null:

  forall f i c v,  

  eval_compare_null c i = Some v ->

  val_inject f v v.






Hint Resolve eval_Econst eval_Eunop eval_Ebinop eval_Eload: evalexpr.




Ltac TrivialOp :=

  match goal with

  | [ |- exists y, _ /\ val_inject _ (Vint ?x) _ ] =>

      exists (Vint x); split;

      [eauto with evalexpr | constructor]

  | [ |- exists y, _ /\ val_inject _ (Vfloat ?x) _ ] =>

      exists (Vfloat x); split;

      [eauto with evalexpr | constructor]

  | [ |- exists y, _ /\ val_inject _ (Val.of_bool ?x) _ ] =>

      exists (Val.of_bool x); split;

      [eauto with evalexpr | apply val_inject_val_of_bool]

  | [ |- exists y, Some ?x = Some y /\ val_inject _ _ _ ] =>

      exists x; split; [auto | econstructor; eauto]

  | _ => idtac

  end.

Correctness of transl_constant.





Lemma transl_constant_correct:

  forall f sp cst v,

  Csharpminor.eval_constant cst = Some v ->

  exists tv,

     eval_constant tge sp (transl_constant cst) = Some tv

  /\ val_inject f v tv.

Compatibility of eval_unop with respect to val_inject.





Lemma eval_unop_compat:

  forall f op v1 tv1 v,

  eval_unop op v1 = Some v ->

  val_inject f v1 tv1 ->

  exists tv,

     eval_unop op tv1 = Some tv

  /\ val_inject f v tv.

Compatibility of eval_binop with respect to val_inject.





Lemma eval_binop_compat:

  forall f op v1 tv1 v2 tv2 v m tm,

  Csharpminor.eval_binop op v1 v2 m = Some v ->

  val_inject f v1 tv1 ->

  val_inject f v2 tv2 ->

  mem_inject f m tm ->

  exists tv,

     Cminor.eval_binop op tv1 tv2 = Some tv

  /\ val_inject f v tv.

Correctness of make_cast. Note that the resulting Cminor value is normalized according to the given memory chunk.





Lemma make_cast_correct:

  forall f sp te tm a v tv chunk,

  eval_expr tge sp te tm a tv ->

  val_inject f v tv ->

  exists tv',

     eval_expr tge sp te tm (make_cast chunk a) tv'

  /\ val_inject f (Val.load_result chunk v) tv'.






Lemma make_stackaddr_correct:

  forall sp te tm ofs,

  eval_expr tge (Vptr sp Int.zero) te tm

            (make_stackaddr ofs) (Vptr sp (Int.repr ofs)).






Lemma make_globaladdr_correct:

  forall sp te tm id b,

  Genv.find_symbol tge id = Some b ->

  eval_expr tge (Vptr sp Int.zero) te tm

            (make_globaladdr id) (Vptr b Int.zero).

Correctness of make_store.





Lemma store_arg_content_inject:

  forall f sp te tm a v va chunk,

  eval_expr tge sp te tm a va ->

  val_inject f v va ->

  exists vb,

     eval_expr tge sp te tm (store_arg chunk a) vb

  /\ val_content_inject f chunk v vb.






Lemma make_store_correct:

  forall f sp te tm addr tvaddr rhs tvrhs chunk m vaddr vrhs m' fn k,

  eval_expr tge sp te tm addr tvaddr ->

  eval_expr tge sp te tm rhs tvrhs ->

  Mem.storev chunk m vaddr vrhs = Some m' ->

  mem_inject f m tm ->

  val_inject f vaddr tvaddr ->

  val_inject f vrhs tvrhs ->

  exists tm',

  step tge (State fn (make_store chunk addr rhs) k sp te tm)

        E0 (State fn Sskip k sp te tm')

  /\ mem_inject f m' tm'

  /\ nextblock tm' = nextblock tm.

Correctness of the variable accessors var_get, var_addr, and var_set.





Lemma var_get_correct:

  forall cenv id a f e te sp lo hi m cs tm b chunk v,

  var_get cenv id = OK a ->

  match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m ->

  mem_inject f m tm ->

  eval_var_ref gve e id b chunk ->

  load chunk m b 0 = Some v ->

  exists tv,

    eval_expr tge (Vptr sp Int.zero) te tm a tv /\

    val_inject f v tv.






Lemma var_addr_correct:

  forall cenv id a f e te sp lo hi m cs tm b,

  match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m ->

  var_addr cenv id = OK a ->

  eval_var_addr gve e id b ->

  exists tv,

    eval_expr tge (Vptr sp Int.zero) te tm a tv /\

    val_inject f (Vptr b Int.zero) tv.






Lemma var_set_correct:

  forall cenv id rhs a f e te sp lo hi m cs tm tv v m' fn k,

  var_set cenv id rhs = OK a ->

  match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m ->

  eval_expr tge (Vptr sp Int.zero) te tm rhs tv ->

  val_inject f v tv ->

  mem_inject f m tm ->

  exec_assign gve e m id v m' ->

  exists te', exists tm',

    step tge (State fn a k (Vptr sp Int.zero) te tm)

          E0 (State fn Sskip k (Vptr sp Int.zero) te' tm') /\

    mem_inject f m' tm' /\

    match_callstack f (mkframe cenv e te' sp lo hi :: cs) m'.(nextblock) tm'.(nextblock) m' /\

    (forall id', id' <> id -> te'!id' = te!id').






Lemma match_env_extensional':

  forall f cenv e m te1 sp lo hi,

  match_env f cenv e m te1 sp lo hi ->

  forall te2,

  (forall id, 

     match cenv!!id with

     | Var_local _ => te2!id = te1!id

     | _ => True

     end) ->

  match_env f cenv e m te2 sp lo hi.






Lemma match_callstack_extensional:

  forall f cenv e te1 te2 sp lo hi cs bound tbound m,

  (forall id, 

     match cenv!!id with

     | Var_local _ => te2!id = te1!id

     | _ => True

     end) ->

  match_callstack f (mkframe cenv e te1 sp lo hi :: cs) bound tbound m ->

  match_callstack f (mkframe cenv e te2 sp lo hi :: cs) bound tbound m.






Lemma var_set_self_correct:

  forall cenv id a f e te sp lo hi m cs tm tv v m' fn k,

  var_set cenv id (Evar id) = OK a ->

  match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m ->

  val_inject f v tv ->

  mem_inject f m tm ->

  exec_assign gve e m id v m' ->

  exists te', exists tm',

    step tge (State fn a k (Vptr sp Int.zero) (PTree.set id tv te) tm)

          E0 (State fn Sskip k (Vptr sp Int.zero) te' tm') /\

    mem_inject f m' tm' /\

    match_callstack f (mkframe cenv e te' sp lo hi :: cs) m'.(nextblock) tm'.(nextblock) m'.

Correctness of stack allocation of local variables

This section shows the correctness of the translation of Csharpminor local variables, either as Cminor local variables or as sub-blocks of the Cminor stack data. This is the most difficult part of the proof.





Remark array_alignment_pos:

  forall sz, array_alignment sz > 0.






Remark assign_variables_incr:

  forall atk vars cenv sz cenv' sz',

  assign_variables atk vars (cenv, sz) = (cenv', sz') -> sz <= sz'.






Remark inj_offset_aligned_array:

  forall stacksize sz,

  inj_offset_aligned (align stacksize (array_alignment sz)) sz.






Remark inj_offset_aligned_array':

  forall stacksize sz,

  inj_offset_aligned (align stacksize (array_alignment sz)) (Zmax 0 sz).






Remark inj_offset_aligned_var:

  forall stacksize chunk,

  inj_offset_aligned (align stacksize (size_chunk chunk)) (size_chunk chunk).






Lemma match_callstack_alloc_variables_rec:

  forall tm sp cenv' sz' te lo cs atk,

  valid_block tm sp ->

  low_bound tm sp = 0 ->

  high_bound tm sp = sz' ->

  sz' <= Int.max_signed ->

  forall e m vars e' m',

  alloc_variables e m vars e' m' ->

  forall f cenv sz,

  assign_variables atk vars (cenv, sz) = (cenv', sz') ->

  match_callstack f (mkframe cenv e te sp lo m.(nextblock) :: cs)

                    m.(nextblock) tm.(nextblock) m ->

  mem_inject f m tm ->

  0 <= sz ->

  (forall b delta, f b = Some(sp, delta) -> high_bound m b + delta <= sz) ->

  (forall id lv, In (id, lv) vars -> te!id <> None) ->

  list_norepet (List.map (@fst ident var_kind) vars) ->

  (forall id lv, In (id, lv) vars -> e!id = None) ->

  exists f',

     inject_incr f f'

  /\ mem_inject f' m' tm

  /\ match_callstack f' (mkframe cenv' e' te sp lo m'.(nextblock) :: cs)

                        m'.(nextblock) tm.(nextblock) m'.






Lemma set_params_defined:

  forall params args id,

  In id params -> (set_params args params)!id <> None.






Lemma set_locals_defined:

  forall e vars id,

  In id vars \/ e!id <> None -> (set_locals vars e)!id <> None.






Lemma set_locals_params_defined:

  forall args params vars id,

  In id (params ++ vars) ->

  (set_locals vars (set_params args params))!id <> None.

Preservation of match_callstack by simultaneous allocation of Csharpminor local variables and of the Cminor stack data block.





Lemma match_callstack_alloc_variables:

  forall fn cenv sz m e m' tm tm' sp f cs targs body,

  build_compilenv gce fn = (cenv, sz) ->

  sz <= Int.max_signed ->

  list_norepet (fn_params_names fn ++ fn_vars_names fn) ->

  alloc_variables Csharpminor.empty_env m (fn_variables fn) e m' ->

  Mem.alloc tm 0 sz = (tm', sp) ->

  match_callstack f cs m.(nextblock) tm.(nextblock) m ->

  mem_inject f m tm ->

  let tvars := make_vars (fn_params_names fn) (fn_vars_names fn) body in

  let te := set_locals tvars (set_params targs (fn_params_names fn)) in

  exists f',

     inject_incr f f'

  /\ mem_inject f' m' tm'

  /\ match_callstack f' (mkframe cenv e te sp m.(nextblock) m'.(nextblock) :: cs)

                        m'.(nextblock) tm'.(nextblock) m'.

Correctness of the code generated by store_parameters to store in memory the values of parameters that are stack-allocated.





Inductive vars_vals_match:

    meminj -> list (ident * memory_chunk) -> list val -> env -> Prop :=

  | vars_vals_nil:

      forall f te,

      vars_vals_match f nil nil te

  | vars_vals_cons:

      forall f te id chunk vars v vals tv,

      te!id = Some tv ->

      val_inject f v tv ->

      vars_vals_match f vars vals te ->

      vars_vals_match f ((id, chunk) :: vars) (v :: vals) te.




Lemma vars_vals_match_extensional:

  forall f vars vals te,

  vars_vals_match f vars vals te ->

  forall te',

  (forall id lv, In (id, lv) vars -> te'!id = te!id) ->

  vars_vals_match f vars vals te'.






Lemma store_parameters_correct:

  forall e m1 params vl m2,

  bind_parameters e m1 params vl m2 ->

  forall s f te1 cenv sp lo hi cs tm1 fn k,

  vars_vals_match f params vl te1 ->

  list_norepet (List.map (@fst ident memory_chunk) params) ->

  mem_inject f m1 tm1 ->

  match_callstack f (mkframe cenv e te1 sp lo hi :: cs) m1.(nextblock) tm1.(nextblock) m1 ->

  store_parameters cenv params = OK s ->

  exists te2, exists tm2,

     star step tge (State fn s k (Vptr sp Int.zero) te1 tm1)

                E0 (State fn Sskip k (Vptr sp Int.zero) te2 tm2)

  /\ mem_inject f m2 tm2

  /\ match_callstack f (mkframe cenv e te2 sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2.






Lemma vars_vals_match_holds_1:

  forall f params args targs,

  list_norepet (List.map (@fst ident memory_chunk) params) ->

  List.length params = List.length args ->

  val_list_inject f args targs ->

  vars_vals_match f params args

    (set_params targs (List.map (@fst ident memory_chunk) params)).






Lemma vars_vals_match_holds:

  forall f params args targs,

  List.length params = List.length args ->

  val_list_inject f args targs ->

  forall vars,

  list_norepet (vars ++ List.map (@fst ident memory_chunk) params) ->

  vars_vals_match f params args

    (set_locals vars (set_params targs (List.map (@fst ident memory_chunk) params))).






Lemma bind_parameters_length:

  forall e m1 params args m2,

  bind_parameters e m1 params args m2 ->

  List.length params = List.length args.






Remark identset_removelist_charact:

  forall l s x, Identset.In x (identset_removelist l s) <-> Identset.In x s /\ ~In x l.






Remark InA_In:

  forall (A: Type) (x: A) (l: list A),

  InA (fun (x y: A) => x = y) x l <-> In x l.






Remark NoDupA_norepet:

  forall (A: Type) (l: list A),

  NoDupA (fun (x y: A) => x = y) l -> list_norepet l.






Lemma make_vars_norepet:

  forall fn body,

  list_norepet (fn_params_names fn ++ fn_vars_names fn) ->

  list_norepet (make_vars (fn_params_names fn) (fn_vars_names fn) body

                ++ fn_params_names fn).

The main result in this section: the behaviour of function entry in the generated Cminor code (allocate stack data block and store parameters whose address is taken) simulates what happens at function entry in the original Csharpminor (allocate one block per local variable and initialize the blocks corresponding to function parameters).





Lemma function_entry_ok:

  forall fn m e m1 vargs m2 f cs tm cenv sz tm1 sp tvargs body s fn' k,

  alloc_variables empty_env m (fn_variables fn) e m1 ->

  bind_parameters e m1 fn.(Csharpminor.fn_params) vargs m2 ->

  match_callstack f cs m.(nextblock) tm.(nextblock) m ->

  build_compilenv gce fn = (cenv, sz) ->

  sz <= Int.max_signed ->

  Mem.alloc tm 0 sz = (tm1, sp) ->

  let vars :=

    make_vars (fn_params_names fn) (fn_vars_names fn) body in

  let te :=

    set_locals vars (set_params tvargs (fn_params_names fn)) in

  val_list_inject f vargs tvargs ->

  mem_inject f m tm ->

  list_norepet (fn_params_names fn ++ fn_vars_names fn) ->

  store_parameters cenv fn.(Csharpminor.fn_params) = OK s ->

  exists f2, exists te2, exists tm2,

     star step tge (State fn' s k (Vptr sp Int.zero) te tm1)

                E0 (State fn' Sskip k (Vptr sp Int.zero) te2 tm2)

  /\ mem_inject f2 m2 tm2

  /\ inject_incr f f2

  /\ match_callstack f2

       (mkframe cenv e te2 sp m.(nextblock) m1.(nextblock) :: cs)

       m2.(nextblock) tm2.(nextblock) m2.

Semantic preservation for the translation

The proof of semantic preservation uses simulation diagrams of the following form:

       e, m1, s ----------------- sp, te1, tm1, ts
          |                                |
         t|                                |t
          v                                v
       e, m2, out --------------- sp, te2, tm2, tout

where ts is the Cminor statement obtained by translating the Csharpminor statement s. The left vertical arrow is an execution of a Csharpminor statement. The right vertical arrow is an execution of a Cminor statement. The precondition (top vertical bar) includes a mem_inject relation between the memory states m1 and tm1, and a match_callstack relation for any callstack having e, te1, sp as top frame. The postcondition (bottom vertical bar) is the existence of a memory injection f2 that extends the injection f1 we started with, preserves the match_callstack relation for the transformed callstack at the final state, and validates a outcome_inject relation between the outcomes out and tout.

Semantic preservation for expressions





Remark bool_of_val_inject:

  forall f v tv b,

  Val.bool_of_val v b -> val_inject f v tv -> Val.bool_of_val tv b.






Lemma transl_expr_correct:

  forall f m tm cenv e te sp lo hi cs

    (MINJ: mem_inject f m tm)

    (MATCH: match_callstack f

             (mkframe cenv e te sp lo hi :: cs)

             m.(nextblock) tm.(nextblock) m),

  forall a v,

  Csharpminor.eval_expr gve e m a v ->

  forall ta

    (TR: transl_expr cenv a = OK ta),

  exists tv,

     eval_expr tge (Vptr sp Int.zero) te tm ta tv

  /\ val_inject f v tv.






Lemma transl_exprlist_correct:

  forall f m tm cenv e te sp lo hi cs

    (MINJ: mem_inject f m tm)

    (MATCH: match_callstack f

             (mkframe cenv e te sp lo hi :: cs)

             m.(nextblock) tm.(nextblock) m),

  forall a v,

  Csharpminor.eval_exprlist gve e m a v ->

  forall ta

    (TR: transl_exprlist cenv a = OK ta),

  exists tv,

     eval_exprlist tge (Vptr sp Int.zero) te tm ta tv

  /\ val_list_inject f v tv.

Semantic preservation for statements and functions





Inductive match_cont: Csharpminor.cont -> Cminor.cont -> compilenv -> exit_env -> callstack -> Prop :=

  | match_Kstop: forall cenv xenv,

      match_cont Csharpminor.Kstop Kstop cenv xenv nil

  | match_Kseq: forall s k ts tk cenv xenv cs,

      transl_stmt cenv xenv s = OK ts ->

      match_cont k tk cenv xenv cs ->

      match_cont (Csharpminor.Kseq s k) (Kseq ts tk) cenv xenv cs

  | match_Kseq2: forall s1 s2 k ts1 tk cenv xenv cs,

      transl_stmt cenv xenv s1 = OK ts1 ->

      match_cont (Csharpminor.Kseq s2 k) tk cenv xenv cs ->

      match_cont (Csharpminor.Kseq (Csharpminor.Sseq s1 s2) k)

                 (Kseq ts1 tk) cenv xenv cs

  | match_Kblock: forall k tk cenv xenv cs,

      match_cont k tk cenv xenv cs ->

      match_cont (Csharpminor.Kblock k) (Kblock tk) cenv (true :: xenv) cs

  | match_Kblock2: forall k tk cenv xenv cs,

      match_cont k tk cenv xenv cs ->

      match_cont k (Kblock tk) cenv (false :: xenv) cs

  | match_Kcall_none: forall fn e k tfn sp te tk cenv xenv lo hi cs sz cenv',

      transl_funbody cenv sz fn = OK tfn ->

      match_cont k tk cenv xenv cs ->

      match_cont (Csharpminor.Kcall None fn e k)

                 (Kcall None tfn (Vptr sp Int.zero) te tk)

                 cenv' nil

                 (mkframe cenv e te sp lo hi :: cs)

  | match_Kcall_some: forall id fn e k tfn s sp te tk cenv xenv lo hi cs sz cenv',

      transl_funbody cenv sz fn = OK tfn ->

      var_set cenv id (Evar id) = OK s ->

      match_cont k tk cenv xenv cs ->

      match_cont (Csharpminor.Kcall (Some id) fn e k)

                 (Kcall (Some id) tfn (Vptr sp Int.zero) te (Kseq s tk))

                 cenv' nil

                 (mkframe cenv e te sp lo hi :: cs).




Inductive match_states: Csharpminor.state -> Cminor.state -> Prop :=

  | match_state:

      forall fn s k e m tfn ts tk sp te tm cenv xenv f lo hi cs sz

      (TRF: transl_funbody cenv sz fn = OK tfn)

      (TR: transl_stmt cenv xenv s = OK ts)

      (MINJ: mem_inject f m tm)

      (MCS: match_callstack f

               (mkframe cenv e te sp lo hi :: cs)

               m.(nextblock) tm.(nextblock) m)

      (MK: match_cont k tk cenv xenv cs),

      match_states (Csharpminor.State fn s k e m)

                   (State tfn ts tk (Vptr sp Int.zero) te tm)

  | match_state_seq:

      forall fn s1 s2 k e m tfn ts1 tk sp te tm cenv xenv f lo hi cs sz

      (TRF: transl_funbody cenv sz fn = OK tfn)

      (TR: transl_stmt cenv xenv s1 = OK ts1)

      (MINJ: mem_inject f m tm)

      (MCS: match_callstack f

               (mkframe cenv e te sp lo hi :: cs)

               m.(nextblock) tm.(nextblock) m)

      (MK: match_cont (Csharpminor.Kseq s2 k) tk cenv xenv cs),

      match_states (Csharpminor.State fn (Csharpminor.Sseq s1 s2) k e m)

                   (State tfn ts1 tk (Vptr sp Int.zero) te tm)

  | match_callstate:

      forall fd args k m tfd targs tk tm f cs cenv

      (TR: transl_fundef gce fd = OK tfd)

      (MINJ: mem_inject f m tm)

      (MCS: match_callstack f cs m.(nextblock) tm.(nextblock) m)

      (MK: match_cont k tk cenv nil cs)

      (ISCC: Csharpminor.is_call_cont k)

      (ARGSINJ: val_list_inject f args targs),

      match_states (Csharpminor.Callstate fd args k m)

                   (Callstate tfd targs tk tm)

  | match_returnstate:

      forall v k m tv tk tm f cs cenv

      (MINJ: mem_inject f m tm)

      (MCS: match_callstack f cs m.(nextblock) tm.(nextblock) m)

      (MK: match_cont k tk cenv nil cs)

      (RESINJ: val_inject f v tv),

      match_states (Csharpminor.Returnstate v k m)

                   (Returnstate tv tk tm).




Remark nextblock_freelist:

  forall lb m, nextblock (free_list m lb) = nextblock m.






Remark val_inject_function_pointer:

  forall v fd f tv,

  Genv.find_funct tge v = Some fd ->

  match_globalenvs f ->

  val_inject f v tv ->

  tv = v.






Lemma match_call_cont:

  forall k tk cenv xenv cs,

  match_cont k tk cenv xenv cs ->

  match_cont (Csharpminor.call_cont k) (call_cont tk) cenv nil cs.






Lemma match_is_call_cont:

  forall tfn te sp tm k tk cenv xenv cs,

  match_cont k tk cenv xenv cs ->

  Csharpminor.is_call_cont k ->

  exists tk',

    star step tge (State tfn Sskip tk sp te tm)

               E0 (State tfn Sskip tk' sp te tm)

    /\ is_call_cont tk'

    /\ match_cont k tk' cenv nil cs.

Properties of switch compilation





Require Import Switch.




Remark switch_table_shift:

  forall n sl base dfl,

  switch_target n (S dfl) (switch_table sl (S base)) =

  S (switch_target n dfl (switch_table sl base)).






Remark length_switch_table:

  forall sl base1 base2,

  length (switch_table sl base1) = length (switch_table sl base2).






Inductive transl_lblstmt_cont (cenv: compilenv) (xenv: exit_env): lbl_stmt -> cont -> cont -> Prop :=

  | tlsc_default: forall s k ts,

      transl_stmt cenv (switch_env (LSdefault s) xenv) s = OK ts ->

      transl_lblstmt_cont cenv xenv (LSdefault s) k (Kblock (Kseq ts k))

  | tlsc_case: forall i s ls k ts k',

      transl_stmt cenv (switch_env (LScase i s ls) xenv) s = OK ts ->

      transl_lblstmt_cont cenv xenv ls k k' ->

      transl_lblstmt_cont cenv xenv (LScase i s ls) k (Kblock (Kseq ts k')).




Lemma switch_descent:

  forall cenv xenv k ls body s,

  transl_lblstmt cenv (switch_env ls xenv) ls body = OK s ->

  exists k',

  transl_lblstmt_cont cenv xenv ls k k'

  /\ (forall f sp e m,

      plus step tge (State f s k sp e m) E0 (State f body k' sp e m)).






Lemma switch_ascent:

  forall f n sp e m cenv xenv k ls k1,

  let tbl := switch_table ls O in

  let ls' := select_switch n ls in

  transl_lblstmt_cont cenv xenv ls k k1 ->

  exists k2,

  star step tge (State f (Sexit (switch_target n (length tbl) tbl)) k1 sp e m)

             E0 (State f (Sexit O) k2 sp e m)

  /\ transl_lblstmt_cont cenv xenv ls' k k2.






Lemma switch_match_cont:

  forall cenv xenv k cs tk ls tk',

  match_cont k tk cenv xenv cs ->

  transl_lblstmt_cont cenv xenv ls tk tk' ->

  match_cont (Csharpminor.Kseq (seq_of_lbl_stmt ls) k) tk' cenv (false :: switch_env ls xenv) cs.






Lemma transl_lblstmt_suffix:

  forall n cenv xenv ls body ts,

  transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts ->

  let ls' := select_switch n ls in

  exists body', exists ts',

  transl_lblstmt cenv (switch_env ls' xenv) ls' body' = OK ts'.






Lemma switch_match_states:

  forall fn k e m tfn ts tk sp te tm cenv xenv f lo hi cs sz ls body tk'

    (TRF: transl_funbody cenv sz fn = OK tfn)

    (TR: transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts)

    (MINJ: mem_inject f m tm)

    (MCS: match_callstack f

             (mkframe cenv e te sp lo hi :: cs)

             m.(nextblock) tm.(nextblock) m)

    (MK: match_cont k tk cenv xenv cs)

    (TK: transl_lblstmt_cont cenv xenv ls tk tk'),

  exists S,

  plus step tge (State tfn (Sexit O) tk' (Vptr sp Int.zero) te tm) E0 S

  /\ match_states (Csharpminor.State fn (seq_of_lbl_stmt ls) k e m) S.

Commutation between find_label and compilation





Section FIND_LABEL.




Variable lbl: label.

Variable cenv: compilenv.

Variable cs: callstack.




Remark find_label_var_set:

  forall id e s k,

  var_set cenv id e = OK s ->

  find_label lbl s k = None.






Lemma transl_lblstmt_find_label_context:

  forall cenv xenv ls body ts tk1 tk2 ts' tk',

  transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts ->

  transl_lblstmt_cont cenv xenv ls tk1 tk2 ->

  find_label lbl body tk2 = Some (ts', tk') ->

  find_label lbl ts tk1 = Some (ts', tk').






Lemma transl_find_label:

  forall s k xenv ts tk,

  transl_stmt cenv xenv s = OK ts ->

  match_cont k tk cenv xenv cs ->

  match Csharpminor.find_label lbl s k with

  | None => find_label lbl ts tk = None

  | Some(s', k') =>

      exists ts', exists tk', exists xenv',

        find_label lbl ts tk = Some(ts', tk')

     /\ transl_stmt cenv xenv' s' = OK ts'

     /\ match_cont k' tk' cenv xenv' cs

  end



with transl_lblstmt_find_label:

  forall ls xenv body k ts tk tk1,

  transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts ->

  match_cont k tk cenv xenv cs ->

  transl_lblstmt_cont cenv xenv ls tk tk1 ->

  find_label lbl body tk1 = None ->

  match Csharpminor.find_label_ls lbl ls k with

  | None => find_label lbl ts tk = None

  | Some(s', k') =>

      exists ts', exists tk', exists xenv',

        find_label lbl ts tk = Some(ts', tk')

     /\ transl_stmt cenv xenv' s' = OK ts'

     /\ match_cont k' tk' cenv xenv' cs

  end.






Remark find_label_store_parameters:

  forall vars s k,

  store_parameters cenv vars = OK s -> find_label lbl s k = None.






End FIND_LABEL.




Lemma transl_find_label_body:

  forall cenv xenv size f tf k tk cs lbl s' k',

  transl_funbody cenv size f = OK tf ->

  match_cont k tk cenv xenv cs ->

  Csharpminor.find_label lbl f.(Csharpminor.fn_body) (Csharpminor.call_cont k) = Some (s', k') ->

  exists ts', exists tk', exists xenv',

     find_label lbl tf.(fn_body) (call_cont tk) = Some(ts', tk')

  /\ transl_stmt cenv xenv' s' = OK ts'

  /\ match_cont k' tk' cenv xenv' cs.






Require Import Coq.Program.Equality.




Fixpoint seq_left_depth (s: Csharpminor.stmt) : nat :=

  match s with

  | Csharpminor.Sseq s1 s2 => S (seq_left_depth s1)

  | _ => O

  end.




Definition measure (S: Csharpminor.state) : nat :=

  match S with

  | Csharpminor.State fn s k e m => seq_left_depth s

  | _ => O

  end.




Lemma transl_step_correct:

  forall S1 t S2, Csharpminor.step gve S1 t S2 ->

  forall T1, match_states S1 T1 ->

  (exists T2, plus step tge T1 t T2 /\ match_states S2 T2)

  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat.






Lemma match_globalenvs_init:

  let m := Genv.init_mem prog in

  match_globalenvs (meminj_init m).






Lemma transl_initial_states:

  forall S, Csharpminor.initial_state prog S ->

  exists R, Cminor.initial_state tprog R /\ match_states S R.






Lemma transl_final_states:

  forall S R r,

  match_states S R -> Csharpminor.final_state S r -> Cminor.final_state R r.






Theorem transl_program_correct:

  forall (beh: program_behavior),

  not_wrong beh -> Csharpminor.exec_program prog beh ->

  Cminor.exec_program tprog beh.






End TRANSLATION.