From 8539759095f95f2fbb680efc7633d868099114c8 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 29 Dec 2012 16:55:38 +0000 Subject: Merge of the clightgen branch: - Alternate semantics for Clight where function parameters are temporaries, not variables - New pass SimplLocals that turns non-addressed local variables into temporaries - Simplified Csharpminor, Cshmgen and Cminorgen accordingly - SimplExpr starts its temporaries above variable names, therefoe Cminorgen no longer needs to encode variable names and temps names. - Simplified Cminor parser & printer, as well as Errors, accordingly. - New tool clightgen to produce Clight AST in Coq-parsable .v files. - Removed side condition "return type is void" on rules skip_seq in the semantics of CompCert C, Clight, C#minor, Cminor. - Adapted RTLgenproof accordingly (now uses a memory extension). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2083 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgenproof.v | 386 ++++++++++------------------------------------- 1 file changed, 76 insertions(+), 310 deletions(-) (limited to 'cfrontend/Cshmgenproof.v') diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 2f319d0..42eae5d 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -32,24 +32,11 @@ Require Import Cshmgen. (** * Properties of operations over types *) -Remark type_of_kind_of_type: - forall t k, - var_kind_of_type t = OK k -> type_of_kind k = typ_of_type t. -Proof. - intros. destruct t; try (monadInv H); auto. - destruct i; destruct s; monadInv H; auto. - destruct f; monadInv H; auto. -Qed. - Remark transl_params_types: - forall p tp, - transl_vars p = OK tp -> - map type_of_kind (map variable_kind tp) = typlist_of_typelist (type_of_params p). + forall params, + map typ_of_type (map snd params) = typlist_of_typelist (type_of_params params). Proof. - induction p; simpl; intros. - inv H. auto. - destruct a as [id ty]. destruct (var_kind_of_type ty) as []_eqn; monadInv H. - simpl. f_equal; auto. apply type_of_kind_of_type; auto. + induction params; simpl. auto. destruct a as [id ty]; simpl. f_equal; auto. Qed. Lemma transl_fundef_sig1: @@ -60,8 +47,8 @@ Lemma transl_fundef_sig1: Proof. intros. destruct f; simpl in *. monadInv H. monadInv EQ. simpl. inversion H0. - unfold fn_sig; simpl. unfold signature_of_type. f_equal. - apply transl_params_types; auto. + unfold signature_of_function, signature_of_type. + f_equal. apply transl_params_types. destruct (list_typ_eq (sig_args (ef_sig e)) (typlist_of_typelist t)); simpl in H. destruct (opt_typ_eq (sig_res (ef_sig e)) (opttyp_of_type t0)); simpl in H. inv H. simpl. destruct (ef_sig e); simpl in *. inv H0. @@ -80,6 +67,7 @@ Proof. rewrite H0; reflexivity. Qed. +(* Lemma var_kind_by_value: forall ty chunk, access_mode ty = By_value chunk -> @@ -113,7 +101,8 @@ Proof. destruct ty; try (destruct i; try destruct s); try (destruct f); simpl; intro EQ; inversion EQ; subst vk; auto. Qed. - +*) +(**** Remark cast_int_int_normalized: forall sz si a chunk n, access_mode (Tint sz si a) = By_value chunk -> @@ -212,58 +201,13 @@ Proof. split. exists v1; exists (typeof a); auto. eauto. Qed. -(** * Properties of the translation functions *) - -Lemma transl_vars_names: - forall vars tvars, - transl_vars vars = OK tvars -> - List.map variable_name tvars = var_names vars. -Proof. - induction vars; simpl; intros. - monadInv H. auto. - destruct a as [id ty]. destruct (var_kind_of_type ty); monadInv H. - simpl. decEq; auto. -Qed. - -Lemma transl_names_norepet: - forall params vars sg tparams tvars temps body, - list_norepet (var_names params ++ var_names vars) -> - transl_vars params = OK tparams -> - transl_vars vars = OK tvars -> - let f := Csharpminor.mkfunction sg tparams tvars temps body in - list_norepet (fn_params_names f ++ fn_vars_names f). -Proof. - intros. unfold fn_params_names, fn_vars_names; simpl. - rewrite (transl_vars_names _ _ H0). - rewrite (transl_vars_names _ _ H1). - auto. -Qed. +*******) -Lemma transl_vars_append: - forall l1 l2 tl1 tl2, - transl_vars l1 = OK tl1 -> transl_vars l2 = OK tl2 -> - transl_vars (l1 ++ l2) = OK (tl1 ++ tl2). -Proof. - induction l1; simpl; intros. - inv H. auto. - destruct a as [id ty]. destruct (var_kind_of_type ty); monadInv H. - erewrite IHl1; eauto. simpl. auto. -Qed. - -Lemma transl_fn_variables: - forall params vars sg tparams tvars temps body, - transl_vars params = OK tparams -> - transl_vars vars = OK tvars -> - let f := Csharpminor.mkfunction sg tparams tvars temps body in - transl_vars (params ++ vars) = OK (fn_variables f). -Proof. - intros. - rewrite (transl_vars_append _ _ _ _ H H0). - reflexivity. -Qed. +(** * Properties of the translation functions *) (** Transformation of expressions and statements. *) +(* Lemma is_variable_correct: forall a id, is_variable a = Some id -> @@ -272,29 +216,28 @@ Proof. intros until id. unfold is_variable; destruct a; intros; try discriminate. simpl. congruence. Qed. +*) Lemma transl_expr_lvalue: forall ge e le m a loc ofs ta, Clight.eval_lvalue ge e le m a loc ofs -> transl_expr a = OK ta -> - (exists id, exists ty, a = Clight.Evar id ty /\ var_get id ty = OK ta) \/ - (exists tb, transl_lvalue a = OK tb /\ - make_load tb (typeof a) = OK ta). + (exists tb, transl_lvalue a = OK tb /\ make_load tb (typeof a) = OK ta). Proof. - intros until ta; intros EVAL TR. inv EVAL. + intros until ta; intros EVAL TR. inv EVAL; simpl in TR. (* var local *) - left; exists id; exists ty; auto. + exists (Eaddrof id); auto. (* var global *) - left; exists id; exists ty; auto. + exists (Eaddrof id); auto. (* deref *) - monadInv TR. right. exists x; split; auto. + monadInv TR. exists x; auto. (* field struct *) - simpl in TR. rewrite H0 in TR. monadInv TR. - right. econstructor; split. simpl. rewrite H0. + rewrite H0 in TR. monadInv TR. + econstructor; split. simpl. rewrite H0. rewrite EQ; rewrite EQ1; simpl; eauto. auto. (* field union *) - simpl in TR. rewrite H0 in TR. monadInv TR. - right. econstructor; split. simpl. rewrite H0. rewrite EQ; simpl; eauto. auto. + rewrite H0 in TR. monadInv TR. + econstructor; split. simpl. rewrite H0. rewrite EQ; simpl; eauto. auto. Qed. (** Properties of labeled statements *) @@ -806,34 +749,20 @@ Record match_env (e: Clight.env) (te: Csharpminor.env) : Prop := mk_match_env { me_local: forall id b ty, - e!id = Some (b, ty) -> - exists vk, var_kind_of_type ty = OK vk /\ te!id = Some (b, vk); + e!id = Some (b, ty) -> te!id = Some(b, sizeof ty); me_local_inv: - forall id b vk, - te!id = Some (b, vk) -> exists ty, e!id = Some(b, ty) + forall id b sz, + te!id = Some (b, sz) -> exists ty, e!id = Some(b, ty) }. Lemma match_env_globals: - forall e te id l ty, + forall e te id, match_env e te -> e!id = None -> - Genv.find_symbol ge id = Some l -> - type_of_global ge l = Some ty -> - te!id = None /\ - (forall chunk, access_mode ty = By_value chunk -> - exists gv, Genv.find_var_info tge l = Some gv /\ gvar_info gv = Vscalar chunk). + te!id = None. Proof. - intros. - case_eq (te!id). intros [b' vk] EQ. - exploit me_local_inv; eauto. intros [ty' EQ']. congruence. - intros. split; auto; intros. - revert H2; unfold type_of_global. - case_eq (Genv.find_var_info ge l). intros. inv H5. - exploit var_info_translated; eauto. intros [gv [A B]]. monadInv B. unfold transl_globvar in EQ. - econstructor; split. eauto. simpl. - exploit var_kind_by_value; eauto. congruence. - intros. destruct (Genv.find_funct_ptr ge l); intros; inv H5. - destruct f; simpl in H4; discriminate. + intros. destruct (te!id) as [[b sz] | ]_eqn; auto. + exploit me_local_inv; eauto. intros [ty EQ]. congruence. Qed. Lemma match_env_same_blocks: @@ -842,29 +771,25 @@ Lemma match_env_same_blocks: blocks_of_env te = Clight.blocks_of_env e. Proof. intros. - set (R := fun (x: (block * type)) (y: (block * var_kind)) => + set (R := fun (x: (block * type)) (y: (block * Z)) => match x, y with - | (b1, ty), (b2, vk) => b2 = b1 /\ var_kind_of_type ty = OK vk + | (b1, ty), (b2, sz) => b2 = b1 /\ sz = sizeof ty end). assert (list_forall2 (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y)) (PTree.elements e) (PTree.elements te)). apply PTree.elements_canonical_order. - intros id [b ty] GET. exploit me_local; eauto. intros [vk [A B]]. - exists (b, vk); split; auto. red. auto. - intros id [b vk] GET. - exploit me_local_inv; eauto. intros [ty A]. - exploit me_local; eauto. intros [vk' [B C]]. - assert (vk' = vk) by congruence. subst vk'. - exists (b, ty); split; auto. red. auto. + intros id [b ty] GET. exists (b, sizeof ty); split. eapply me_local; eauto. red; auto. + intros id [b sz] GET. exploit me_local_inv; eauto. intros [ty EQ]. + exploit me_local; eauto. intros EQ1. + exists (b, ty); split. auto. red; split; congruence. unfold blocks_of_env, Clight.blocks_of_env. generalize H0. induction 1. auto. simpl. f_equal; auto. unfold block_of_binding, Clight.block_of_binding. - destruct a1 as [id1 [blk1 ty1]]. destruct b1 as [id2 [blk2 vk2]]. - simpl in *. destruct H1 as [A [B C]]. subst blk2 id2. f_equal. - apply sizeof_var_kind_of_type. auto. + destruct a1 as [id1 [blk1 ty1]]. destruct b1 as [id2 [blk2 sz2]]. + simpl in *. destruct H1 as [A [B C]]. congruence. Qed. Lemma match_env_free_blocks: @@ -881,8 +806,8 @@ Lemma match_env_empty: Proof. unfold Clight.empty_env, Csharpminor.empty_env. constructor. - intros until b. repeat rewrite PTree.gempty. congruence. - intros until vk. rewrite PTree.gempty. congruence. + intros until ty. repeat rewrite PTree.gempty. congruence. + intros until sz. rewrite PTree.gempty. congruence. Qed. (** The following lemmas establish the [match_env] invariant at @@ -892,177 +817,42 @@ Qed. Lemma match_env_alloc_variables: forall e1 m1 vars e2 m2, Clight.alloc_variables e1 m1 vars e2 m2 -> - forall te1 tvars, + forall te1, match_env e1 te1 -> - transl_vars vars = OK tvars -> exists te2, - Csharpminor.alloc_variables te1 m1 tvars te2 m2 + Csharpminor.alloc_variables te1 m1 (map transl_var vars) te2 m2 /\ match_env e2 te2. Proof. - induction 1; intros. - monadInv H0. + induction 1; intros; simpl. exists te1; split. constructor. auto. - generalize H2. simpl. - caseEq (var_kind_of_type ty); simpl; [intros vk VK | congruence]. - caseEq (transl_vars vars); simpl; [intros tvrs TVARS | congruence]. - intro EQ; inversion EQ; subst tvars; clear EQ. - set (te2 := PTree.set id (b1, vk) te1). - assert (match_env (PTree.set id (b1, ty) e) te2). - inversion H1. unfold te2. constructor. + exploit (IHalloc_variables (PTree.set id (b1, sizeof ty) te1)). + constructor. (* me_local *) - intros until ty0. simpl. repeat rewrite PTree.gsspec. - destruct (peq id0 id); intros. - inv H3. exists vk; intuition. - auto. + intros until ty0. repeat rewrite PTree.gsspec. + destruct (peq id0 id); intros. congruence. eapply me_local; eauto. (* me_local_inv *) - intros until vk0. repeat rewrite PTree.gsspec. - destruct (peq id0 id); intros. exists ty; congruence. eauto. - destruct (IHalloc_variables _ _ H3 TVARS) as [te3 [ALLOC MENV]]. - exists te3; split. - econstructor; eauto. - rewrite (sizeof_var_kind_of_type _ _ VK). eauto. - auto. + intros until sz. repeat rewrite PTree.gsspec. + destruct (peq id0 id); intros. exists ty; congruence. eapply me_local_inv; eauto. + intros [te2 [ALLOC MENV]]. + exists te2; split. econstructor; eauto. auto. Qed. -Lemma bind_parameters_match: - forall e m1 vars vals m2, - Clight.bind_parameters e m1 vars vals m2 -> - forall te tvars, - val_casted_list vals (type_of_params vars) -> - match_env e te -> - transl_vars vars = OK tvars -> - Csharpminor.bind_parameters tge te m1 tvars vals m2. -Proof. - induction 1; intros. -(* base case *) - monadInv H1. constructor. -(* inductive case *) - simpl in H2. destruct H2. - simpl in H4. destruct (var_kind_of_type ty) as [vk|]_eqn; monadInv H4. - inv H0. - (* scalar case *) - assert (vk = Vscalar chunk). exploit var_kind_by_value; eauto. congruence. - subst vk. - apply bind_parameters_scalar with b m1. - exploit me_local; eauto. intros [vk [A B]]. congruence. - eapply val_casted_normalized; eauto. - assumption. - apply IHbind_parameters; auto. - (* struct case *) - exploit var_kind_by_reference; eauto. intros; subst vk. - apply bind_parameters_array with b m1. - exploit me_local; eauto. intros [vk [A B]]. congruence. - econstructor; eauto. - apply alignof_1248. - apply sizeof_pos. - apply sizeof_alignof_compat. - apply IHbind_parameters; auto. -Qed. - Lemma create_undef_temps_match: forall temps, - create_undef_temps (List.map (@fst ident type) temps) = Clight.create_undef_temps temps. + create_undef_temps (map fst temps) = Clight.create_undef_temps temps. Proof. induction temps; simpl. auto. destruct a as [id ty]. simpl. decEq. auto. Qed. -(* ** Correctness of variable accessors *) - -(** Correctness of the code generated by [var_get]. *) - -Lemma var_get_correct: - forall e le m id ty loc ofs v code te, - Clight.eval_lvalue ge e le m (Clight.Evar id ty) loc ofs -> - deref_loc ty m loc ofs v -> - var_get id ty = OK code -> - match_env e te -> - eval_expr tge te le m code v. -Proof. - unfold var_get; intros. - inv H0. - (* access mode By_value *) - rewrite H3 in H1. inv H1. inv H. - (* local variable *) - exploit me_local; eauto. intros [vk [A B]]. - assert (vk = Vscalar chunk). - exploit var_kind_by_value; eauto. congruence. - subst vk. - eapply eval_Evar. - eapply eval_var_ref_local. eauto. assumption. - (* global variable *) - exploit match_env_globals; eauto. intros [A B]. - exploit B; eauto. intros [gv [C D]]. - eapply eval_Evar. - eapply eval_var_ref_global. auto. - rewrite symbols_preserved. eauto. - eauto. eauto. - assumption. - (* access mode By_reference *) - rewrite H3 in H1. inv H1. inv H. - (* local variable *) - exploit me_local; eauto. intros [vk [A B]]. - eapply eval_Eaddrof. - eapply eval_var_addr_local. eauto. - (* global variable *) - exploit match_env_globals; eauto. intros [A B]. - eapply eval_Eaddrof. - eapply eval_var_addr_global. auto. - rewrite symbols_preserved. eauto. - (* access mode By_copy *) - rewrite H3 in H1. inv H1. inv H. - (* local variable *) - exploit me_local; eauto. intros [vk [A B]]. - eapply eval_Eaddrof. - eapply eval_var_addr_local. eauto. - (* global variable *) - exploit match_env_globals; eauto. intros [A B]. - eapply eval_Eaddrof. - eapply eval_var_addr_global. auto. - rewrite symbols_preserved. eauto. -Qed. - -(** Correctness of the code generated by [var_set]. *) - -Lemma var_set_correct: - forall e le m id ty loc ofs v m' code te rhs f k, - Clight.eval_lvalue ge e le m (Clight.Evar id ty) loc ofs -> - val_casted v ty -> - assign_loc ty m loc ofs v m' -> - var_set id ty rhs = OK code -> - match_env e te -> - eval_expr tge te le m rhs v -> - step tge (State f code k te le m) E0 (State f Sskip k te le m'). +Lemma bind_parameter_temps_match: + forall vars vals le1 le2, + Clight.bind_parameter_temps vars vals le1 = Some le2 -> + bind_parameters (map fst vars) vals le1 = Some le2. Proof. - intros. unfold var_set in H2. - inversion H1; subst; rewrite H5 in H2; inv H2. - (* scalar, non volatile *) - inv H. - (* local variable *) - exploit me_local; eauto. intros [vk [A B]]. - assert (vk = Vscalar chunk). - exploit var_kind_by_value; eauto. congruence. - subst vk. - eapply step_assign. eauto. - econstructor. eapply eval_var_ref_local. eauto. - eapply val_casted_normalized; eauto. assumption. - (* global variable *) - exploit match_env_globals; eauto. intros [A B]. - exploit B; eauto. intros [gv [C D]]. - eapply step_assign. eauto. - econstructor. eapply eval_var_ref_global. auto. - rewrite symbols_preserved. eauto. - eauto. eauto. - eapply val_casted_normalized; eauto. assumption. - (* struct *) - assert (eval_expr tge te le m (Eaddrof id) (Vptr loc ofs)). - inv H. - exploit me_local; eauto. intros [vk [A B]]. - constructor. eapply eval_var_addr_local; eauto. - exploit match_env_globals; eauto. intros [A B]. - constructor. eapply eval_var_addr_global; eauto. - rewrite symbols_preserved. eauto. - eapply make_memcpy_correct; eauto. + induction vars; simpl; intros. + destruct vals; inv H. auto. + destruct a as [id ty]. destruct vals; try discriminate. auto. Qed. (** * Proof of semantic preservation *) @@ -1123,19 +913,14 @@ Proof. (* cast *) eapply make_cast_correct; eauto. (* rvalue out of lvalue *) - exploit transl_expr_lvalue; eauto. - intros [[id [ty [EQ VARGET]]] | [tb [TRLVAL MKLOAD]]]. - (* Case a is a variable *) - subst a. eapply var_get_correct; eauto. - (* Case a is another lvalue *) + exploit transl_expr_lvalue; eauto. intros [tb [TRLVAL MKLOAD]]. eapply make_load_correct; eauto. (* var local *) - exploit (me_local _ _ MENV); eauto. - intros [vk [A B]]. + exploit (me_local _ _ MENV); eauto. intros EQ. econstructor. eapply eval_var_addr_local. eauto. (* var global *) - exploit match_env_globals; eauto. intros [A B]. - econstructor. eapply eval_var_addr_global. eauto. + econstructor. eapply eval_var_addr_global. + eapply match_env_globals; eauto. rewrite symbols_preserved. auto. (* deref *) simpl in TR. eauto. @@ -1261,8 +1046,7 @@ Inductive match_states: Clight.state -> Csharpminor.state -> Prop := (TR: transl_fundef fd = OK tfd) (MK: match_cont Tvoid 0%nat 0%nat k tk) (ISCC: Clight.is_call_cont k) - (TY: type_of_fundef fd = Tfunction targs tres) - (VCAST: val_casted_list args targs), + (TY: type_of_fundef fd = Tfunction targs tres), match_states (Clight.Callstate fd args k m) (Callstate tfd args tk m) | match_returnstate: @@ -1318,10 +1102,6 @@ Proof. (* skip *) auto. (* assign *) - simpl in TR. - destruct (is_variable e); monadInv TR. - unfold var_set, make_memcpy in EQ0. - destruct (access_mode (typeof e)); inv EQ0; auto. unfold make_store, make_memcpy in EQ2. destruct (access_mode (typeof e)); inv EQ2; auto. (* set *) @@ -1405,26 +1185,14 @@ Qed. (** The simulation proof *) Lemma transl_step: - forall S1 t S2, Clight.step ge S1 t S2 -> + forall S1 t S2, Clight.step2 ge S1 t S2 -> forall T1, match_states S1 T1 -> exists T2, plus step tge T1 t T2 /\ match_states S2 T2. Proof. induction 1; intros T1 MST; inv MST. (* assign *) - simpl in TR. - destruct (is_variable a1) as []_eqn; monadInv TR. - (* a variable *) - assert (SAME: ts' = ts /\ tk' = tk). - inversion MTR. auto. - subst ts. unfold var_set, make_memcpy in EQ0. destruct (access_mode (typeof a1)); congruence. - destruct SAME; subst ts' tk'. - exploit is_variable_correct; eauto. intro EQ1. rewrite EQ1 in H. - econstructor; split. - apply plus_one. eapply var_set_correct; eauto. exists v2; exists (typeof a2); auto. - eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. - eapply match_states_skip; eauto. - (* not a variable *) + monadInv TR. assert (SAME: ts' = ts /\ tk' = tk). inversion MTR. auto. subst ts. unfold make_store, make_memcpy in EQ2. destruct (access_mode (typeof a1)); congruence. @@ -1454,7 +1222,6 @@ Proof. econstructor; eauto. econstructor; eauto. simpl. auto. - eapply eval_exprlist_casted; eauto. (* builtin *) monadInv TR. inv MTR. @@ -1569,7 +1336,6 @@ Proof. exploit match_cont_is_call_cont; eauto. intros [A B]. econstructor; split. apply plus_one. apply step_skip_call. auto. - monadInv TRF. simpl. rewrite H0. auto. eapply match_env_free_blocks; eauto. constructor. eauto. @@ -1608,7 +1374,7 @@ Proof. (* goto *) monadInv TR. inv MTR. generalize TRF. unfold transl_function. intro TRF'. monadInv TRF'. - exploit (transl_find_label lbl). eexact EQ0. eapply match_cont_call_cont. eauto. + exploit (transl_find_label lbl). eexact EQ. eapply match_cont_call_cont. eauto. rewrite H. intros [ts' [tk'' [nbrk' [ncnt' [A [B C]]]]]]. econstructor; split. @@ -1616,20 +1382,20 @@ Proof. econstructor; eauto. constructor. (* internal function *) - monadInv TR. monadInv EQ. + inv H. monadInv TR. monadInv EQ. exploit match_cont_is_call_cont; eauto. intros [A B]. exploit match_env_alloc_variables; eauto. apply match_env_empty. - eapply transl_fn_variables; eauto. intros [te1 [C D]]. econstructor; split. - apply plus_one. econstructor. - eapply transl_names_norepet; eauto. - eexact C. eapply bind_parameters_match; eauto. - simpl in TY. unfold type_of_function in TY. congruence. - simpl. rewrite (create_undef_temps_match (Clight.fn_temps f)). - econstructor; eauto. - unfold transl_function. rewrite EQ0; simpl. rewrite EQ; simpl. rewrite EQ1; auto. + apply plus_one. eapply step_internal_function. + simpl. rewrite list_map_compose. simpl. assumption. + simpl. auto. + simpl. auto. + simpl. eauto. + simpl. rewrite create_undef_temps_match. eapply bind_parameter_temps_match; eauto. + simpl. econstructor; eauto. + unfold transl_function. rewrite EQ0; simpl. auto. constructor. (* external function *) @@ -1667,7 +1433,7 @@ Proof. eapply transl_fundef_sig2; eauto. econstructor; split. econstructor; eauto. eapply Genv.init_mem_transf_partial2; eauto. - econstructor; eauto. constructor; auto. exact I. red; auto. + econstructor; eauto. constructor; auto. exact I. Qed. Lemma transl_final_states: @@ -1678,7 +1444,7 @@ Proof. Qed. Theorem transl_program_correct: - forward_simulation (Clight.semantics prog) (Csharpminor.semantics tprog). + forward_simulation (Clight.semantics2 prog) (Csharpminor.semantics tprog). Proof. eapply forward_simulation_plus. eexact symbols_preserved. -- cgit v1.2.3