diff options
| -rw-r--r-- | aarch64/Conventions1.v | 5 | ||||
| -rw-r--r-- | arm/Conventions1.v | 6 | ||||
| -rw-r--r-- | cfrontend/Cshmgen.v | 37 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 133 | ||||
| -rw-r--r-- | powerpc/Conventions1.v | 6 | ||||
| -rw-r--r-- | riscV/Conventions1.v | 6 | ||||
| -rw-r--r-- | x86/Conventions1.v | 14 |
7 files changed, 174 insertions, 33 deletions
diff --git a/aarch64/Conventions1.v b/aarch64/Conventions1.v index 575d058d..b1b3badd 100644 --- a/aarch64/Conventions1.v +++ b/aarch64/Conventions1.v @@ -377,3 +377,8 @@ Proof. unfold loc_arguments; reflexivity. Qed. +(** ** Normalization of function results *) + +(** No normalization needed. *) + +Definition return_value_needs_normalization (t: rettype) := false. diff --git a/arm/Conventions1.v b/arm/Conventions1.v index 45008bff..7016c1ee 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -641,3 +641,9 @@ Proof. unfold loc_arguments. destruct Archi.abi; reflexivity. Qed. + +(** ** Normalization of function results *) + +(** No normalization needed. *) + +Definition return_value_needs_normalization (t: rettype) := false. diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index ee135dcd..5bd12d00 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -23,6 +23,7 @@ Require Import Coqlib Maps Errors Integers Floats. Require Import AST Linking. Require Import Ctypes Cop Clight Cminor Csharpminor. +Require Import Conventions1. Local Open Scope string_scope. Local Open Scope error_monad_scope. @@ -558,6 +559,34 @@ Fixpoint typlist_of_arglist (al: list Clight.expr) (tyl: typelist) typ_of_type (default_argument_conversion (typeof a1)) :: typlist_of_arglist a2 Tnil end. +(** Translate a function call. + Depending on the ABI, it may be necessary to normalize the value + returned by casting it to the return type of the function. + For example, in the x86 ABI, a return value of type "char" is + returned in register AL, leaving the top 24 bits of EAX + unspecified. Hence, a cast to type "char" is needed to sign- or + zero-extend the returned integer before using it. *) + +Definition make_normalization (t: type) (a: expr) := + match t with + | Tint IBool _ _ => Eunop Ocast8unsigned a + | Tint I8 Signed _ => Eunop Ocast8signed a + | Tint I8 Unsigned _ => Eunop Ocast8unsigned a + | Tint I16 Signed _ => Eunop Ocast16signed a + | Tint I16 Unsigned _ => Eunop Ocast16unsigned a + | _ => a + end. + +Definition make_funcall (x: option ident) (tres: type) (sg: signature) + (fn: expr) (args: list expr): stmt := + match x, return_value_needs_normalization sg.(sig_res) with + | Some id, true => + Sseq (Scall x sg fn args) + (Sset id (make_normalization tres (Evar id))) + | _, _ => + Scall x sg fn args + end. + (** * Translation of statements *) (** [transl_statement nbrk ncnt s] returns a Csharpminor statement @@ -601,10 +630,10 @@ Fixpoint transl_statement (ce: composite_env) (tyret: type) (nbrk ncnt: nat) | fun_case_f args res cconv => do tb <- transl_expr ce b; do tcl <- transl_arglist ce cl args; - OK(Scall x {| sig_args := typlist_of_arglist cl args; - sig_res := rettype_of_type res; - sig_cc := cconv |} - tb tcl) + let sg := {| sig_args := typlist_of_arglist cl args; + sig_res := rettype_of_type res; + sig_cc := cconv |} in + OK (make_funcall x res sg tb tcl) | _ => Error(msg "Cshmgen.transl_stmt(call)") end | Clight.Sbuiltin x ef tyargs bl => diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 09e31cb2..1ceb8e4d 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -15,7 +15,7 @@ Require Import Coqlib Errors Maps Integers Floats. Require Import AST Linking. Require Import Values Events Memory Globalenvs Smallstep. -Require Import Ctypes Cop Clight Cminor Csharpminor. +Require Import Ctypes Ctyping Cop Clight Cminor Csharpminor. Require Import Cshmgen. (** * Relational specification of the transformation *) @@ -996,6 +996,26 @@ Proof. eapply make_memcpy_correct with (b := b) (v := Vptr b' ofs'); eauto. Qed. +Lemma make_normalization_correct: + forall e le m a v t, + eval_expr ge e le m a v -> + wt_val v t -> + eval_expr ge e le m (make_normalization t a) v. +Proof. + intros. destruct t; simpl; auto. inv H0. +- destruct i; simpl in H3. + + destruct s; econstructor; eauto; simpl; congruence. + + destruct s; econstructor; eauto; simpl; congruence. + + auto. + + econstructor; eauto; simpl; congruence. +- auto. +- destruct i. + + destruct s; econstructor; eauto. + + destruct s; econstructor; eauto. + + auto. + + econstructor; eauto. +Qed. + End CONSTRUCTORS. (** * Basic preservation invariants *) @@ -1360,7 +1380,16 @@ Inductive match_cont: composite_env -> type -> nat -> nat -> Clight.cont -> Csha match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk' ncnt' k tk -> match_cont ce tyret nbrk ncnt (Clight.Kcall id f e le k) - (Kcall id tf te le tk). + (Kcall id tf te le tk) + | match_Kcall_normalize: forall ce tyret nbrk ncnt nbrk' ncnt' f e k id a tf te le tk cu, + linkorder cu prog -> + transl_function cu.(prog_comp_env) f = OK tf -> + match_env e te -> + match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk' ncnt' k tk -> + (forall v e le m, wt_val v tyret -> le!id = Some v -> eval_expr tge e le m a v) -> + match_cont ce tyret nbrk ncnt + (Clight.Kcall (Some id) f e le k) + (Kcall (Some id) tf te le (Kseq (Sset id a) tk)). Inductive match_states: Clight.state -> Csharpminor.state -> Prop := | match_state: @@ -1377,14 +1406,15 @@ Inductive match_states: Clight.state -> Csharpminor.state -> Prop := forall fd args k m tfd tk targs tres cconv cu ce (LINK: linkorder cu prog) (TR: match_fundef cu fd tfd) - (MK: match_cont ce Tvoid 0%nat 0%nat k tk) + (MK: match_cont ce tres 0%nat 0%nat k tk) (ISCC: Clight.is_call_cont k) (TY: type_of_fundef fd = Tfunction targs tres cconv), match_states (Clight.Callstate fd args k m) (Callstate tfd args tk m) | match_returnstate: - forall res k m tk ce - (MK: match_cont ce Tvoid 0%nat 0%nat k tk), + forall res tres k m tk ce + (MK: match_cont ce tres 0%nat 0%nat k tk) + (WT: wt_val res tres), match_states (Clight.Returnstate res k m) (Returnstate res tk m). @@ -1442,7 +1472,9 @@ Proof. - (* set *) auto. - (* call *) - simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. auto. + simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. + unfold make_funcall. + destruct o; auto; destruct Conventions1.return_value_needs_normalization; auto. - (* builtin *) auto. - (* seq *) @@ -1500,24 +1532,26 @@ End FIND_LABEL. (** Properties of call continuations *) Lemma match_cont_call_cont: - forall ce' tyret' nbrk' ncnt' ce tyret nbrk ncnt k tk, + forall ce' nbrk' ncnt' ce tyret nbrk ncnt k tk, match_cont ce tyret nbrk ncnt k tk -> - match_cont ce' tyret' nbrk' ncnt' (Clight.call_cont k) (call_cont tk). + match_cont ce' tyret nbrk' ncnt' (Clight.call_cont k) (call_cont tk). Proof. induction 1; simpl; auto. - constructor. - econstructor; eauto. +- apply match_Kstop. +- eapply match_Kcall; eauto. +- eapply match_Kcall_normalize; eauto. Qed. Lemma match_cont_is_call_cont: - forall ce tyret nbrk ncnt k tk ce' tyret' nbrk' ncnt', + forall ce tyret nbrk ncnt k tk ce' nbrk' ncnt', match_cont ce tyret nbrk ncnt k tk -> Clight.is_call_cont k -> - match_cont ce' tyret' nbrk' ncnt' k tk /\ is_call_cont tk. + match_cont ce' tyret nbrk' ncnt' k tk /\ is_call_cont tk. Proof. intros. inv H; simpl in H0; try contradiction; simpl. - split; auto; constructor. - split; auto; econstructor; eauto. + split; auto; apply match_Kstop. + split; auto; eapply match_Kcall; eauto. + split; auto; eapply match_Kcall_normalize; eauto. Qed. (** The simulation proof *) @@ -1549,19 +1583,44 @@ Proof. - (* call *) revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence. - intros targs tres cc CF TR. monadInv TR. inv MTR. + intros targs tres cc CF TR. monadInv TR. exploit functions_translated; eauto. intros (cu' & tfd & FIND & TFD & LINK'). rewrite H in CF. simpl in CF. inv CF. - econstructor; split. - apply plus_one. econstructor; eauto. - eapply transl_expr_correct with (cunit := cu); eauto. - eapply transl_arglist_correct with (cunit := cu); eauto. - erewrite typlist_of_arglist_eq by eauto. - eapply transl_fundef_sig1; eauto. - rewrite H3. auto. - econstructor; eauto. - eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto. - simpl. auto. + set (sg := {| sig_args := typlist_of_arglist al targs; + sig_res := rettype_of_type tres; + sig_cc := cc |}) in *. + assert (SIG: funsig tfd = sg). + { unfold sg; erewrite typlist_of_arglist_eq by eauto. + eapply transl_fundef_sig1; eauto. rewrite H3; auto. } + assert (EITHER: tk' = tk /\ ts' = Scall optid sg x x0 + \/ exists id, optid = Some id /\ + tk' = tk /\ ts' = Sseq (Scall optid sg x x0) + (Sset id (make_normalization tres (Evar id)))). + { unfold make_funcall in MTR. + destruct optid. destruct Conventions1.return_value_needs_normalization. + inv MTR. right; exists i; auto. + inv MTR; auto. + inv MTR; auto. } + destruct EITHER as [(EK & ES) | (id & EI & EK & ES)]; rewrite EK, ES. + + (* without normalization of return value *) + econstructor; split. + apply plus_one. eapply step_call; eauto. + eapply transl_expr_correct with (cunit := cu); eauto. + eapply transl_arglist_correct with (cunit := cu); eauto. + econstructor; eauto. + eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto. + exact I. + + (* with normalization of return value *) + subst optid. + econstructor; split. + eapply plus_two. apply step_seq. eapply step_call; eauto. + eapply transl_expr_correct with (cunit := cu); eauto. + eapply transl_arglist_correct with (cunit := cu); eauto. + traceEq. + econstructor; eauto. + eapply match_Kcall_normalize with (ce := prog_comp_env cu') (cu := cu); eauto. + intros. eapply make_normalization_correct; eauto. constructor; eauto. + exact I. - (* builtin *) monadInv TR. inv MTR. @@ -1658,6 +1717,7 @@ Proof. eapply match_env_free_blocks; eauto. eapply match_returnstate with (ce := prog_comp_env cu); eauto. eapply match_cont_call_cont. eauto. + constructor. - (* return some *) monadInv TR. inv MTR. @@ -1667,6 +1727,7 @@ Proof. eapply match_env_free_blocks; eauto. eapply match_returnstate with (ce := prog_comp_env cu); eauto. eapply match_cont_call_cont. eauto. + apply wt_val_casted. eapply cast_val_is_casted; eauto. - (* skip call *) monadInv TR. inv MTR. @@ -1675,6 +1736,7 @@ Proof. apply plus_one. apply step_skip_call. auto. eapply match_env_free_blocks; eauto. eapply match_returnstate with (ce := prog_comp_env cu); eauto. + constructor. - (* switch *) monadInv TR. @@ -1738,20 +1800,33 @@ Proof. simpl. econstructor; eauto. unfold transl_function. rewrite EQ; simpl. rewrite EQ1; simpl. auto. constructor. + replace (fn_return f) with tres. eassumption. + simpl in TY. unfold type_of_function in TY. congruence. - (* external function *) inv TR. exploit match_cont_is_call_cont; eauto. intros [A B]. econstructor; split. - apply plus_one. constructor. eauto. + apply plus_one. constructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved. eapply match_returnstate with (ce := ce); eauto. + apply has_rettype_wt_val. + replace (rettype_of_type tres0) with (sig_res (ef_sig ef)). + eapply external_call_well_typed_gen; eauto. + rewrite H5. simpl. simpl in TY. congruence. - (* returnstate *) inv MK. - econstructor; split. - apply plus_one. constructor. - econstructor; eauto. simpl; reflexivity. constructor. + + (* without normalization *) + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl; reflexivity. constructor. + + (* with normalization *) + econstructor; split. + eapply plus_three. econstructor. econstructor. constructor. + simpl. apply H13. eauto. apply PTree.gss. + traceEq. + simpl. rewrite PTree.set2. econstructor; eauto. simpl; reflexivity. constructor. Qed. Lemma transl_initial_states: diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 7c1b2750..25d9c081 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -463,3 +463,9 @@ Lemma loc_arguments_main: Proof. reflexivity. Qed. + +(** ** Normalization of function results *) + +(** No normalization needed. *) + +Definition return_value_needs_normalization (t: rettype) := false. diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v index 09cbbb44..27d09d94 100644 --- a/riscV/Conventions1.v +++ b/riscV/Conventions1.v @@ -438,3 +438,9 @@ Lemma loc_arguments_main: Proof. reflexivity. Qed. + +(** ** Normalization of function results *) + +(** No normalization needed. *) + +Definition return_value_needs_normalization (t: rettype) := false. diff --git a/x86/Conventions1.v b/x86/Conventions1.v index 595cb721..01b15e98 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -471,3 +471,17 @@ Lemma loc_arguments_main: Proof. unfold loc_arguments; destruct Archi.ptr64; reflexivity. Qed. + +(** ** Normalization of function results *) + +(** In the x86 ABI, a return value of type "char" is returned in + register AL, leaving the top 24 bits of EAX unspecified. + Likewise, a return value of type "short" is returned in register + AH, leaving the top 16 bits of EAX unspecified. Hence, return + values of small integer types need re-normalization after calls. *) + +Definition return_value_needs_normalization (t: rettype) : bool := + match t with + | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true + | _ => false + end. |