diff options
Diffstat (limited to 'cfrontend/Cshmgenproof3.v')
| -rw-r--r-- | cfrontend/Cshmgenproof3.v | 52 |
1 files changed, 42 insertions, 10 deletions
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v index c8b9caf..10f48f6 100644 --- a/cfrontend/Cshmgenproof3.v +++ b/cfrontend/Cshmgenproof3.v @@ -67,7 +67,11 @@ Proof. assumption. Qed. -(** ** Matching between environments *) +(** * Matching between environments *) + +(** In this section, we define a matching relation between + a Clight local environment and a Csharpminor local environment, + parameterized by an assignment of types to the Clight variables. *) Definition match_var_kind (ty: type) (vk: var_kind) : Prop := match access_mode ty with @@ -114,6 +118,10 @@ Proof. intros chunk AM. generalize (var_kind_by_value _ _ AM). congruence. Qed. +(** The following lemmas establish the [match_env] invariant at + the beginning of a function invocation, after allocation of + local variables and initialization of the parameters. *) + Lemma match_env_alloc_variables: forall e1 m1 vars e2 m2 lb, Csem.alloc_variables e1 m1 vars e2 m2 lb -> @@ -214,6 +222,10 @@ Proof. intros. apply A. apply List.in_or_app. auto. Qed. +(** The following lemmas establish the matching property + between the global environments constructed at the beginning + of program execution. *) + Definition globvarenv (gv: gvarenv) (vars: list (ident * list init_data * var_kind)) := @@ -290,7 +302,9 @@ Proof. unfold transl_program in TRANSL. monadInv TRANSL. auto. Qed. -(** ** Variable accessors *) +(* ** Correctness of variable accessors *) + +(** Correctness of the code generated by [var_get]. *) Lemma var_get_correct: forall e m id ty loc ofs v tyenv code te le, @@ -339,6 +353,8 @@ Proof. intros. rewrite H1 in H0; discriminate. Qed. +(** Correctness of the code generated by [var_set]. *) + Lemma var_set_correct: forall e m id ty m1 loc ofs t1 m2 v t2 m3 tyenv code te rhs, Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) t1 m1 loc ofs -> @@ -374,9 +390,27 @@ Proof. intros. rewrite H1 in H0; discriminate. Qed. -(** ** Proof of semantic simulation *) - -(** Inductive properties *) +(** * Proof of semantic simulation *) + +(** The proof of semantic preservation for this compiler pass relies + on simulation diagrams of the following form: +<< + e, m1, a ------------------- te, m1, ta + | | + t| |t + | | + v v + e, m2, v ------------------- te, m2, v +>> + Left: evaluation of expression [a] in Clight. + Right: evaluation of its translation [ta] in Csharpminor. + Top (precondition): matching between environments [e], [te], + plus well-typedness of expression [a]. + Bottom (postcondition): the result values [v] and final memory states [m2] + are identical in both evaluations. + + We state these diagrams as the following properties, parameterized + by the Clight evaluation. *) Definition eval_expr_prop (e: Csem.env) (m1: mem) (a: Csyntax.expr) (t: trace) (m2: mem) (v: val) : Prop := @@ -442,11 +476,9 @@ Definition eval_funcall_prop (TR: transl_fundef f = OK tf), Csharpminor.eval_funcall tprog m1 tf params t m2 res. -(* -Set Printing Depth 100. -Check (Csem.eval_funcall_ind6 ge eval_expr_prop eval_lvalue_prop - eval_exprlist_prop exec_stmt_prop exec_lblstmts_prop eval_funcall_prop). -*) +(** The proof of semantic preservation is by induction on the Clight + evaluation derivation. Since this proof is large, we break it + into one lemma for each Clight evaluation rule. *) Lemma transl_Econst_int_correct: (forall (e : Csem.env) (m : mem) (i : int) (ty : type), |