aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--aarch64/Conventions1.v16
-rw-r--r--arm/Conventions1.v3
-rw-r--r--cfrontend/SimplLocals.v13
-rw-r--r--cfrontend/SimplLocalsproof.v40
-rw-r--r--powerpc/Conventions1.v3
-rw-r--r--riscV/Conventions1.v3
-rw-r--r--x86/Conventions1.v7
7 files changed, 58 insertions, 27 deletions
diff --git a/aarch64/Conventions1.v b/aarch64/Conventions1.v
index cfcbcbf1..7edb16dd 100644
--- a/aarch64/Conventions1.v
+++ b/aarch64/Conventions1.v
@@ -343,16 +343,19 @@ Proof.
unfold loc_arguments; reflexivity.
Qed.
-(** ** Normalization of function results *)
+(** ** Normalization of function results and parameters *)
(** According to the AAPCS64 ABI specification, "padding bits" in the return
- value of a function have unpredictable values and must be ignored.
- Consequently, we force normalization of return values of small integer
- types (8- and 16-bit integers), so that the top bits (the "padding bits")
- are proper sign- or zero-extensions of the small integer value.
+ value of a function or in a function parameter have unpredictable
+ values and must be ignored. Consequently, we force normalization
+ of return values and of function parameters when they have small
+ integer types (8- and 16-bit integers), so that the top bits (the
+ "padding bits") are proper sign- or zero-extensions of the small
+ integer value.
The Apple variant of the AAPCS64 requires the callee to return a normalized
- value, hence no normalization is needed in the caller.
+ value, and the caller to pass normalized parameters, hence no
+ normalization is needed.
*)
Definition return_value_needs_normalization (t: rettype) : bool :=
@@ -365,3 +368,4 @@ Definition return_value_needs_normalization (t: rettype) : bool :=
end
end.
+Definition parameter_needs_normalization := return_value_needs_normalization.
diff --git a/arm/Conventions1.v b/arm/Conventions1.v
index 3bd2b553..b94ce9ef 100644
--- a/arm/Conventions1.v
+++ b/arm/Conventions1.v
@@ -436,8 +436,9 @@ Proof.
destruct Archi.abi; reflexivity.
Qed.
-(** ** Normalization of function results *)
+(** ** Normalization of function results and parameters *)
(** No normalization needed. *)
Definition return_value_needs_normalization (t: rettype) := false.
+Definition parameter_needs_normalization (t: rettype) := false.
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:
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v
index 045eb471..56beffe8 100644
--- a/powerpc/Conventions1.v
+++ b/powerpc/Conventions1.v
@@ -349,8 +349,9 @@ Proof.
reflexivity.
Qed.
-(** ** Normalization of function results *)
+(** ** Normalization of function results and parameters *)
(** No normalization needed. *)
Definition return_value_needs_normalization (t: rettype) := false.
+Definition parameter_needs_normalization (t: rettype) := false.
diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index 6cb06c61..eeaae3c4 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -413,8 +413,9 @@ Proof.
reflexivity.
Qed.
-(** ** Normalization of function results *)
+(** ** Normalization of function results and parameters *)
(** No normalization needed. *)
Definition return_value_needs_normalization (t: rettype) := false.
+Definition parameter_needs_normalization (t: rettype) := false.
diff --git a/x86/Conventions1.v b/x86/Conventions1.v
index 803d162a..e3c51f60 100644
--- a/x86/Conventions1.v
+++ b/x86/Conventions1.v
@@ -431,7 +431,7 @@ Proof.
unfold loc_arguments; destruct Archi.ptr64; auto; destruct Archi.win64; auto.
Qed.
-(** ** Normalization of function results *)
+(** ** Normalization of function results and parameters *)
(** In the x86 ABI, a return value of type "char" is returned in
register AL, leaving the top 24 bits of EAX unspecified.
@@ -444,3 +444,8 @@ Definition return_value_needs_normalization (t: rettype) : bool :=
| Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true
| _ => false
end.
+
+(** Function parameters are passed in normalized form and do not need
+ to be re-normalized at function entry. *)
+
+Definition parameter_needs_normalization (t: rettype) := false.
generated by cgit (git 2.34.1) at 2024-05-19 17:42:40 +0000