diff options
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/SimplLocals.v | 13 | ||||
| -rw-r--r-- | cfrontend/SimplLocalsproof.v | 40 |
2 files changed, 36 insertions, 17 deletions
diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v index f54aa60d..0a164e29 100644 --- a/cfrontend/SimplLocals.v +++ b/cfrontend/SimplLocals.v @@ -18,7 +18,7 @@ Require FSetAVL. Require Import Coqlib Ordered Errors. Require Import AST Linking. Require Import Ctypes Cop Clight. -Require Compopts. +Require Compopts Conventions1. Open Scope error_monad_scope. Open Scope string_scope. @@ -157,15 +157,20 @@ with simpl_lblstmt (cenv: compilenv) (ls: labeled_statements) : res labeled_stat end. (** Function parameters that are not lifted to temporaries must be - stored in the corresponding local variable at function entry. *) + stored in the corresponding local variable at function entry. + The other function parameters may need to be normalized to their types, + to support interoperability with code generated by other C compilers. *) Fixpoint store_params (cenv: compilenv) (params: list (ident * type)) (s: statement): statement := match params with | nil => s | (id, ty) :: params' => - if VSet.mem id cenv - then store_params cenv params' s + if VSet.mem id cenv then + if Conventions1.parameter_needs_normalization (rettype_of_type ty) + then Ssequence (Sset id (make_cast (Etempvar id ty) ty)) + (store_params cenv params' s) + else store_params cenv params' s else Ssequence (Sassign (Evar id ty) (Etempvar id ty)) (store_params cenv params' s) end. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 8246a748..988988a1 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -1108,23 +1108,37 @@ Theorem store_params_correct: /\ match_envs j cenv e le m' lo hi te tle tlo thi /\ Mem.nextblock tm' = Mem.nextblock tm. Proof. +Local Opaque Conventions1.parameter_needs_normalization. induction 1; simpl; intros until targs; intros NOREPET CASTED VINJ MENV MINJ TLE LE. - (* base case *) +- (* base case *) inv VINJ. exists tle2; exists tm; split. apply star_refl. split. auto. split. auto. split. apply match_envs_temps_exten with tle1; auto. auto. - (* inductive case *) +- (* inductive case *) inv NOREPET. inv CASTED. inv VINJ. exploit me_vars; eauto. instantiate (1 := id); intros MV. - destruct (VSet.mem id cenv) eqn:?. - (* lifted to temp *) - eapply IHbind_parameters with (tle1 := PTree.set id v' tle1); eauto. - eapply match_envs_assign_lifted; eauto. - inv MV; try congruence. rewrite ENV in H; inv H. - inv H0; try congruence. - unfold Mem.storev in H2. eapply Mem.store_unmapped_inject; eauto. - intros. repeat rewrite PTree.gsspec. destruct (peq id0 id). auto. - apply TLE. intuition. - (* still in memory *) + destruct (VSet.mem id cenv) eqn:LIFTED. ++ (* lifted to temp *) + exploit (IHbind_parameters s tm (PTree.set id v' tle1) (PTree.set id v' tle2)). + eauto. eauto. eauto. + eapply match_envs_assign_lifted; eauto. + inv MV; try congruence. rewrite ENV in H; inv H. + inv H0; try congruence. + unfold Mem.storev in H2. eapply Mem.store_unmapped_inject; eauto. + intros. repeat rewrite PTree.gsspec. destruct (peq id0 id). auto. + apply TLE. intuition. + eauto. + intros (tle & tm' & U & V & X & Y & Z). + exists tle, tm'; split; [|auto]. + destruct (Conventions1.parameter_needs_normalization (rettype_of_type ty)); [|assumption]. + assert (A: tle!id = Some v'). + { erewrite bind_parameter_temps_inv by eauto. apply PTree.gss. } + eapply star_left. constructor. + eapply star_left. econstructor. eapply make_cast_correct. + constructor; eauto. apply cast_val_casted; auto. eapply val_casted_inject; eauto. + rewrite PTree.gsident by auto. + eapply star_left. constructor. eassumption. + traceEq. traceEq. traceEq. ++ (* still in memory *) inv MV; try congruence. rewrite ENV in H; inv H. exploit assign_loc_inject; eauto. intros [tm1 [A [B C]]]. @@ -1979,7 +1993,7 @@ Lemma find_label_store_params: forall s k params, find_label lbl (store_params cenv params s) k = find_label lbl s k. Proof. induction params; simpl. auto. - destruct a as [id ty]. destruct (VSet.mem id cenv); auto. + destruct a as [id ty]. destruct (VSet.mem id cenv); [destruct Conventions1.parameter_needs_normalization|]; auto. Qed. Lemma find_label_add_debug_vars: |