aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2020-03-09 13:26:35 +0100
committerCyril SIX <cyril.six@kalray.eu>2020-03-09 13:26:35 +0100
commit3ce6324ce0a461a1ec81e2b8ddce3f147920994c (patch)
tree73b56264681f7098df43beffa40be4055a6f05fd
parent7794bebc14750c5d8116f54cabe143231ef60308 (diff)
parente16fff7a60904a760f5c11b0bc700abdbdd5d467 (diff)
downloadcompcert-kvx-3ce6324ce0a461a1ec81e2b8ddce3f147920994c.tar.gz
compcert-kvx-3ce6324ce0a461a1ec81e2b8ddce3f147920994c.zip
Merge remote-tracking branch 'origin/mppa-work' into mppa-work-untested
-rw-r--r--Makefile1
-rw-r--r--aarch64/Builtins1.v2
-rw-r--r--aarch64/CSE2deps.v20
-rw-r--r--aarch64/CSE2depsproof.v128
-rw-r--r--aarch64/Conventions1.v137
-rw-r--r--arm/Builtins1.v2
-rw-r--r--arm/CSE2deps.v20
-rw-r--r--arm/CSE2depsproof.v129
-rw-r--r--arm/Conventions1.v238
-rw-r--r--backend/Allocation.v10
-rw-r--r--backend/Allocproof.v15
-rw-r--r--backend/Asmexpandaux.ml2
-rw-r--r--backend/CSE2.v20
-rw-r--r--backend/CSE2proof.v194
-rw-r--r--backend/Cminor.v20
-rw-r--r--backend/Cminortyping.v45
-rw-r--r--backend/Conventions.v67
-rw-r--r--backend/Duplicateproof.v2
-rw-r--r--backend/IRC.ml1
-rw-r--r--backend/Inliningaux.ml2
-rw-r--r--backend/OpHelpers.v20
-rw-r--r--backend/PrintAsmaux.ml6
-rw-r--r--backend/PrintCminor.ml6
-rw-r--r--backend/RTLgen.v16
-rw-r--r--backend/RTLgenspec.v12
-rw-r--r--backend/RTLtyping.v35
-rw-r--r--backend/Tailcall.v2
-rw-r--r--backend/Tailcallproof.v10
-rw-r--r--backend/ValueAnalysis.v5
-rw-r--r--backend/ValueDomain.v5
-rw-r--r--cfrontend/C2C.ml18
-rw-r--r--cfrontend/Cexec.v73
-rw-r--r--cfrontend/Cop.v4
-rw-r--r--cfrontend/Csem.v2
-rw-r--r--cfrontend/Cshmgen.v39
-rw-r--r--cfrontend/Cshmgenproof.v133
-rw-r--r--cfrontend/Csyntax.v2
-rw-r--r--cfrontend/Ctypes.v19
-rw-r--r--cfrontend/Ctyping.v87
-rw-r--r--cfrontend/PrintCsyntax.ml4
-rw-r--r--common/AST.v79
-rw-r--r--common/Builtins.v2
-rw-r--r--common/Builtins0.v64
-rw-r--r--common/Events.v131
-rw-r--r--common/Memdata.v31
-rw-r--r--common/Memory.v26
-rw-r--r--common/Memtype.v5
-rw-r--r--common/PrintAST.ml8
-rw-r--r--common/Values.v33
-rwxr-xr-xconfig_aarch64.sh1
-rwxr-xr-xconfig_arm.sh1
-rwxr-xr-xconfig_ia32.sh1
-rwxr-xr-xconfig_k1c.sh1
-rwxr-xr-xconfig_ppc.sh1
-rwxr-xr-xconfig_rv32.sh1
-rwxr-xr-xconfig_rv64.sh1
-rwxr-xr-xconfig_simple.sh6
-rwxr-xr-xconfig_x86_64.sh1
-rwxr-xr-xcoq2
-rw-r--r--cparser/Elab.ml5
-rw-r--r--cparser/Lexer.mll2
-rw-r--r--driver/Interp.ml4
-rw-r--r--exportclight/ExportClight.ml12
-rw-r--r--lib/Maps.v112
-rw-r--r--mppa_k1c/Asmblockdeps.v8
-rw-r--r--mppa_k1c/Asmblockgen.v2
-rw-r--r--mppa_k1c/Asmblockgenproof1.v6
-rw-r--r--mppa_k1c/Asmvliw.v6
-rw-r--r--mppa_k1c/Builtins1.v12
-rw-r--r--mppa_k1c/CSE2deps.v20
-rw-r--r--mppa_k1c/CSE2depsproof.v127
-rw-r--r--mppa_k1c/Conventions1.v31
-rw-r--r--mppa_k1c/PostpassSchedulingproof.v2
-rw-r--r--mppa_k1c/abstractbb/AbstractBasicBlocksDef.v2
-rw-r--r--mppa_k1c/abstractbb/ImpSimuTest.v14
-rw-r--r--mppa_k1c/abstractbb/Impure/ImpHCons.v4
-rw-r--r--mppa_k1c/abstractbb/Parallelizability.v8
-rw-r--r--mppa_k1c/abstractbb/SeqSimuTheory.v11
-rw-r--r--mppa_k1c/lib/Asmblockgenproof0.v4
-rw-r--r--mppa_k1c/lib/ForwardSimulationBlock.v6
-rw-r--r--mppa_k1c/lib/Machblockgen.v8
-rw-r--r--mppa_k1c/lib/Machblockgenproof.v20
-rw-r--r--powerpc/Archi.v4
-rw-r--r--powerpc/Asmexpand.ml2
-rw-r--r--powerpc/Builtins1.v2
-rw-r--r--powerpc/CSE2deps.v20
-rw-r--r--powerpc/CSE2depsproof.v135
-rw-r--r--powerpc/Conventions1.v177
-rw-r--r--powerpc/extractionMachdep.v3
-rw-r--r--riscV/Asmexpand.ml38
-rw-r--r--riscV/Builtins1.v2
-rw-r--r--riscV/CSE2deps.v20
-rw-r--r--riscV/CSE2depsproof.v127
-rw-r--r--riscV/Conventions1.v341
-rw-r--r--test/cse2/globals.c8
-rw-r--r--test/cse2/indexed_addr.c6
-rw-r--r--test/monniaux/cycles.h7
-rw-r--r--test/regression/Results/interop18
-rw-r--r--test/regression/interop1.c15
-rw-r--r--x86/Asmexpand.ml4
-rw-r--r--x86/Builtins1.v4
-rw-r--r--x86/CSE2deps.v24
-rw-r--r--x86/CSE2depsproof.v253
-rw-r--r--x86/Conventions1.v187
104 files changed, 2433 insertions, 1328 deletions
diff --git a/Makefile b/Makefile
index 5566cf57..2cd40800 100644
--- a/Makefile
+++ b/Makefile
@@ -86,6 +86,7 @@ BACKEND=\
ValueDomain.v ValueAOp.v ValueAnalysis.v \
ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \
CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \
+ CSE2deps.v CSE2depsproof.v \
CSE2.v CSE2proof.v \
NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \
Unusedglob.v Unusedglobproof.v \
diff --git a/aarch64/Builtins1.v b/aarch64/Builtins1.v
index f6e643d2..53c83d7e 100644
--- a/aarch64/Builtins1.v
+++ b/aarch64/Builtins1.v
@@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) :=
Definition platform_builtin_sig (b: platform_builtin) : signature :=
match b with end.
-Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
+Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
match b with end.
diff --git a/aarch64/CSE2deps.v b/aarch64/CSE2deps.v
new file mode 100644
index 00000000..90b514a2
--- /dev/null
+++ b/aarch64/CSE2deps.v
@@ -0,0 +1,20 @@
+Require Import BoolEqual Coqlib.
+Require Import AST Integers Floats.
+Require Import Values Memory Globalenvs Events.
+Require Import Op.
+
+
+Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
+ (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk))
+ && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk))
+ && ((ofsw + size_chunk chunkw <=? ofsr) ||
+ (ofsr + size_chunk chunkr <=? ofsw)).
+
+Definition may_overlap chunk addr args chunk' addr' args' :=
+ match addr, addr', args, args' with
+ | (Aindexed ofs), (Aindexed ofs'),
+ (base :: nil), (base' :: nil) =>
+ if peq base base'
+ then negb (can_swap_accesses_ofs (Int64.unsigned ofs') chunk' (Int64.unsigned ofs) chunk)
+ else true | _, _, _, _ => true
+ end.
diff --git a/aarch64/CSE2depsproof.v b/aarch64/CSE2depsproof.v
new file mode 100644
index 00000000..4aac23af
--- /dev/null
+++ b/aarch64/CSE2depsproof.v
@@ -0,0 +1,128 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Maps.
+
+Require Import Globalenvs Values.
+Require Import Linking Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import CSE2 CSE2deps.
+Require Import Lia.
+
+Lemma ptrofs_size :
+ Ptrofs.wordsize = 64%nat.
+Proof.
+ unfold Ptrofs.wordsize.
+ unfold Wordsize_Ptrofs.wordsize.
+ trivial.
+Qed.
+
+Lemma ptrofs_modulus :
+ Ptrofs.modulus = 18446744073709551616.
+Proof.
+ reflexivity.
+Qed.
+
+Section SOUNDNESS.
+ Variable F V : Type.
+ Variable genv: Genv.t F V.
+ Variable sp : val.
+
+Section MEMORY_WRITE.
+ Variable m m2 : mem.
+ Variable chunkw chunkr : memory_chunk.
+ Variable base : val.
+
+ Variable addrw addrr valw : val.
+ Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
+
+ Section INDEXED_AWAY.
+ Variable ofsw ofsr : int64.
+ Hypothesis ADDRW : eval_addressing genv sp
+ (Aindexed ofsw) (base :: nil) = Some addrw.
+ Hypothesis ADDRR : eval_addressing genv sp
+ (Aindexed ofsr) (base :: nil) = Some addrr.
+
+ Lemma load_store_away1 :
+ forall RANGEW : 0 <= Int64.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk,
+ forall RANGER : 0 <= Int64.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk,
+ forall SWAPPABLE : Int64.unsigned ofsw + size_chunk chunkw <= Int64.unsigned ofsr
+ \/ Int64.unsigned ofsr + size_chunk chunkr <= Int64.unsigned ofsw,
+ Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+ Proof.
+ intros.
+
+ pose proof (max_size_chunk chunkr) as size_chunkr_bounded.
+ pose proof (max_size_chunk chunkw) as size_chunkw_bounded.
+ unfold largest_size_chunk in *.
+
+ rewrite ptrofs_modulus in *.
+ simpl in *.
+ inv ADDRR.
+ inv ADDRW.
+
+ destruct base; try discriminate.
+ eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
+ exact STORE.
+ right.
+
+ all: unfold Ptrofs.of_int64.
+
+ all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.repr (Int64.unsigned ofsr))) as [OFSR | OFSR];
+ rewrite OFSR).
+ all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.repr (Int64.unsigned ofsw))) as [OFSW | OFSW];
+ rewrite OFSW).
+ all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 18446744073709551615; lia).
+
+ all: try rewrite ptrofs_modulus in *.
+
+ all: intuition lia.
+ Qed.
+
+ Theorem load_store_away :
+ can_swap_accesses_ofs (Int64.unsigned ofsr) chunkr (Int64.unsigned ofsw) chunkw = true ->
+ Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+ Proof.
+ intro SWAP.
+ unfold can_swap_accesses_ofs in SWAP.
+ repeat rewrite andb_true_iff in SWAP.
+ repeat rewrite orb_true_iff in SWAP.
+ repeat rewrite Z.leb_le in SWAP.
+ apply load_store_away1.
+ all: tauto.
+ Qed.
+ End INDEXED_AWAY.
+End MEMORY_WRITE.
+End SOUNDNESS.
+
+
+Section SOUNDNESS.
+ Variable F V : Type.
+ Variable genv: Genv.t F V.
+ Variable sp : val.
+
+Lemma may_overlap_sound:
+ forall m m' : mem,
+ forall chunk addr args chunk' addr' args' v a a' rs,
+ (eval_addressing genv sp addr (rs ## args)) = Some a ->
+ (eval_addressing genv sp addr' (rs ## args')) = Some a' ->
+ (may_overlap chunk addr args chunk' addr' args') = false ->
+ (Mem.storev chunk m a v) = Some m' ->
+ (Mem.loadv chunk' m' a') = (Mem.loadv chunk' m a').
+Proof.
+ intros until rs.
+ intros ADDR ADDR' OVERLAP STORE.
+ destruct addr; destruct addr'; try discriminate.
+ { (* Aindexed / Aindexed *)
+ destruct args as [ | base [ | ]]. 1,3: discriminate.
+ destruct args' as [ | base' [ | ]]. 1,3: discriminate.
+ simpl in OVERLAP.
+ destruct (peq base base'). 2: discriminate.
+ subst base'.
+ destruct (can_swap_accesses_ofs (Int64.unsigned ofs0) chunk' (Int64.unsigned ofs) chunk) eqn:SWAP.
+ 2: discriminate.
+ simpl in *.
+ eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
+ }
+Qed.
+
+End SOUNDNESS.
diff --git a/aarch64/Conventions1.v b/aarch64/Conventions1.v
index 5914e8f2..efda835d 100644
--- a/aarch64/Conventions1.v
+++ b/aarch64/Conventions1.v
@@ -102,10 +102,9 @@ Definition is_float_reg (r: mreg): bool :=
with one integer result. *)
Definition loc_result (s: signature) : rpair mreg :=
- match s.(sig_res) with
- | None => One R0
- | Some (Tint | Tlong | Tany32 | Tany64) => One R0
- | Some (Tfloat | Tsingle) => One F0
+ match proj_sig_res s with
+ | Tint | Tlong | Tany32 | Tany64 => One R0
+ | Tfloat | Tsingle => One F0
end.
(** The result registers have types compatible with that given in the signature. *)
@@ -114,7 +113,7 @@ Lemma loc_result_type:
forall sig,
subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
Proof.
- intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; auto.
+ intros. unfold loc_result. destruct (proj_sig_res sig); auto.
Qed.
(** The result locations are caller-save registers *)
@@ -124,7 +123,7 @@ Lemma loc_result_caller_save:
forall_rpair (fun r => is_callee_save r = false) (loc_result s).
Proof.
intros.
- unfold loc_result. destruct (sig_res s) as [[]|]; simpl; auto.
+ unfold loc_result. destruct (proj_sig_res s); simpl; auto.
Qed.
(** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
@@ -134,12 +133,12 @@ Lemma loc_result_pair:
match loc_result sg with
| One _ => True
| Twolong r1 r2 =>
- r1 <> r2 /\ sg.(sig_res) = Some Tlong
+ r1 <> r2 /\ proj_sig_res sg = Tlong
/\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
/\ Archi.ptr64 = false
end.
Proof.
- intros; unfold loc_result; destruct (sig_res sg) as [[]|]; exact I.
+ intros; unfold loc_result; destruct (proj_sig_res sg); exact I.
Qed.
(** The location of the result depends only on the result part of the signature *)
@@ -147,7 +146,7 @@ Qed.
Lemma loc_result_exten:
forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2.
Proof.
- intros. unfold loc_result. rewrite H; auto.
+ intros. unfold loc_result, proj_sig_res. rewrite H; auto.
Qed.
(** ** Location of function arguments *)
@@ -191,27 +190,6 @@ Fixpoint loc_arguments_rec
Definition loc_arguments (s: signature) : list (rpair loc) :=
loc_arguments_rec s.(sig_args) 0 0 0.
-(** [size_arguments s] returns the number of [Outgoing] slots used
- to call a function with signature [s]. *)
-
-Fixpoint size_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z :=
- match tyl with
- | nil => ofs
- | (Tint | Tlong | Tany32 | Tany64) :: tys =>
- match list_nth_z int_param_regs ir with
- | None => size_arguments_rec tys ir fr (ofs + 2)
- | Some ireg => size_arguments_rec tys (ir + 1) fr ofs
- end
- | (Tfloat | Tsingle) :: tys =>
- match list_nth_z float_param_regs fr with
- | None => size_arguments_rec tys ir fr (ofs + 2)
- | Some freg => size_arguments_rec tys ir (fr + 1) ofs
- end
- end.
-
-Definition size_arguments (s: signature) : Z :=
- size_arguments_rec s.(sig_args) 0 0 0.
-
(** Argument locations are either caller-save registers or [Outgoing]
stack slots at nonnegative offsets. *)
@@ -286,95 +264,22 @@ Qed.
Hint Resolve loc_arguments_acceptable: locs.
-(** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
-
-Remark size_arguments_rec_above:
- forall tyl ir fr ofs0,
- ofs0 <= size_arguments_rec tyl ir fr ofs0.
-Proof.
- induction tyl; simpl; intros.
- omega.
- assert (A: ofs0 <=
- match list_nth_z int_param_regs ir with
- | Some _ => size_arguments_rec tyl (ir + 1) fr ofs0
- | None => size_arguments_rec tyl ir fr (ofs0 + 2)
- end).
- { destruct (list_nth_z int_param_regs ir); eauto.
- apply Z.le_trans with (ofs0 + 2); auto. omega. }
- assert (B: ofs0 <=
- match list_nth_z float_param_regs fr with
- | Some _ => size_arguments_rec tyl ir (fr + 1) ofs0
- | None => size_arguments_rec tyl ir fr (ofs0 + 2)
- end).
- { destruct (list_nth_z float_param_regs fr); eauto.
- apply Z.le_trans with (ofs0 + 2); auto. omega. }
- destruct a; auto.
-Qed.
-
-Lemma size_arguments_above:
- forall s, size_arguments s >= 0.
-Proof.
- intros; unfold size_arguments. apply Z.le_ge. apply size_arguments_rec_above.
-Qed.
-
-Lemma loc_arguments_rec_bounded:
- forall ofs ty tyl ir fr ofs0,
- In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_rec tyl ir fr ofs0)) ->
- ofs + typesize ty <= size_arguments_rec tyl ir fr ofs0.
-Proof.
- induction tyl; simpl; intros.
-- contradiction.
-- assert (T: forall ty0, typesize ty0 <= 2).
- { destruct ty0; simpl; omega. }
- assert (A: forall ty0,
- In (S Outgoing ofs ty) (regs_of_rpairs
- match list_nth_z int_param_regs ir with
- | Some ireg =>
- One (R ireg) :: loc_arguments_rec tyl (ir + 1) fr ofs0
- | None => One (S Outgoing ofs0 ty0) :: loc_arguments_rec tyl ir fr (ofs0 + 2)
- end) ->
- ofs + typesize ty <=
- match list_nth_z int_param_regs ir with
- | Some _ => size_arguments_rec tyl (ir + 1) fr ofs0
- | None => size_arguments_rec tyl ir fr (ofs0 + 2)
- end).
- { intros. destruct (list_nth_z int_param_regs ir); simpl in H0; destruct H0.
- - discriminate.
- - eapply IHtyl; eauto.
- - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_rec_above.
- - eapply IHtyl; eauto. }
- assert (B: forall ty0,
- In (S Outgoing ofs ty) (regs_of_rpairs
- match list_nth_z float_param_regs fr with
- | Some ireg =>
- One (R ireg) :: loc_arguments_rec tyl ir (fr + 1) ofs0
- | None => One (S Outgoing ofs0 ty0) :: loc_arguments_rec tyl ir fr (ofs0 + 2)
- end) ->
- ofs + typesize ty <=
- match list_nth_z float_param_regs fr with
- | Some _ => size_arguments_rec tyl ir (fr + 1) ofs0
- | None => size_arguments_rec tyl ir fr (ofs0 + 2)
- end).
- { intros. destruct (list_nth_z float_param_regs fr); simpl in H0; destruct H0.
- - discriminate.
- - eapply IHtyl; eauto.
- - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_rec_above.
- - eapply IHtyl; eauto. }
- destruct a; eauto.
-Qed.
-
-Lemma loc_arguments_bounded:
- forall (s: signature) (ofs: Z) (ty: typ),
- In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) ->
- ofs + typesize ty <= size_arguments s.
-Proof.
- unfold loc_arguments, size_arguments; intros.
- eauto using loc_arguments_rec_bounded.
-Qed.
-
Lemma loc_arguments_main:
loc_arguments signature_main = nil.
Proof.
unfold loc_arguments; reflexivity.
Qed.
+(** ** Normalization of function results *)
+
+(** 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. *)
+
+Definition return_value_needs_normalization (t: rettype) : bool :=
+ match t with
+ | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true
+ | _ => false
+ end.
diff --git a/arm/Builtins1.v b/arm/Builtins1.v
index f6e643d2..53c83d7e 100644
--- a/arm/Builtins1.v
+++ b/arm/Builtins1.v
@@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) :=
Definition platform_builtin_sig (b: platform_builtin) : signature :=
match b with end.
-Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
+Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
match b with end.
diff --git a/arm/CSE2deps.v b/arm/CSE2deps.v
new file mode 100644
index 00000000..9db51bbb
--- /dev/null
+++ b/arm/CSE2deps.v
@@ -0,0 +1,20 @@
+Require Import BoolEqual Coqlib.
+Require Import AST Integers Floats.
+Require Import Values Memory Globalenvs Events.
+Require Import Op.
+
+
+Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
+ (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk))
+ && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk))
+ && ((ofsw + size_chunk chunkw <=? ofsr) ||
+ (ofsr + size_chunk chunkr <=? ofsw)).
+
+Definition may_overlap chunk addr args chunk' addr' args' :=
+ match addr, addr', args, args' with
+ | (Aindexed ofs), (Aindexed ofs'),
+ (base :: nil), (base' :: nil) =>
+ if peq base base'
+ then negb (can_swap_accesses_ofs (Int.unsigned ofs') chunk' (Int.unsigned ofs) chunk)
+ else true | _, _, _, _ => true
+ end.
diff --git a/arm/CSE2depsproof.v b/arm/CSE2depsproof.v
new file mode 100644
index 00000000..61fe5980
--- /dev/null
+++ b/arm/CSE2depsproof.v
@@ -0,0 +1,129 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Maps.
+
+Require Import Globalenvs Values.
+Require Import Linking Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import CSE2 CSE2deps.
+Require Import Lia.
+
+Lemma ptrofs_size :
+ Ptrofs.wordsize = 32%nat.
+Proof.
+ unfold Ptrofs.wordsize.
+ unfold Wordsize_Ptrofs.wordsize.
+ trivial.
+Qed.
+
+Lemma ptrofs_modulus :
+ Ptrofs.modulus = 4294967296.
+Proof.
+ unfold Ptrofs.modulus.
+ rewrite ptrofs_size.
+ destruct Archi.ptr64; reflexivity.
+Qed.
+
+Section SOUNDNESS.
+ Variable F V : Type.
+ Variable genv: Genv.t F V.
+ Variable sp : val.
+
+Section MEMORY_WRITE.
+ Variable m m2 : mem.
+ Variable chunkw chunkr : memory_chunk.
+ Variable base : val.
+
+ Variable addrw addrr valw : val.
+ Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
+
+ Section INDEXED_AWAY.
+ Variable ofsw ofsr : int.
+ Hypothesis ADDRW : eval_addressing genv sp
+ (Aindexed ofsw) (base :: nil) = Some addrw.
+ Hypothesis ADDRR : eval_addressing genv sp
+ (Aindexed ofsr) (base :: nil) = Some addrr.
+
+ Lemma load_store_away1 :
+ forall RANGEW : 0 <= Int.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk,
+ forall RANGER : 0 <= Int.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk,
+ forall SWAPPABLE : Int.unsigned ofsw + size_chunk chunkw <= Int.unsigned ofsr
+ \/ Int.unsigned ofsr + size_chunk chunkr <= Int.unsigned ofsw,
+ Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+ Proof.
+ intros.
+
+ pose proof (max_size_chunk chunkr) as size_chunkr_bounded.
+ pose proof (max_size_chunk chunkw) as size_chunkw_bounded.
+ unfold largest_size_chunk in *.
+
+ rewrite ptrofs_modulus in *.
+ simpl in *.
+ inv ADDRR.
+ inv ADDRW.
+ destruct base; try discriminate.
+ eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
+ exact STORE.
+ right.
+
+ all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int ofsr)) as [OFSR | OFSR];
+ rewrite OFSR).
+ all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int ofsw)) as [OFSW | OFSW];
+ rewrite OFSW).
+
+ all: try rewrite ptrofs_modulus in *.
+
+ all: unfold Ptrofs.of_int.
+
+ all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 4294967295; lia).
+ all: intuition lia.
+ Qed.
+
+ Theorem load_store_away :
+ can_swap_accesses_ofs (Int.unsigned ofsr) chunkr (Int.unsigned ofsw) chunkw = true ->
+ Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+ Proof.
+ intro SWAP.
+ unfold can_swap_accesses_ofs in SWAP.
+ repeat rewrite andb_true_iff in SWAP.
+ repeat rewrite orb_true_iff in SWAP.
+ repeat rewrite Z.leb_le in SWAP.
+ apply load_store_away1.
+ all: tauto.
+ Qed.
+ End INDEXED_AWAY.
+End MEMORY_WRITE.
+End SOUNDNESS.
+
+
+Section SOUNDNESS.
+ Variable F V : Type.
+ Variable genv: Genv.t F V.
+ Variable sp : val.
+
+Lemma may_overlap_sound:
+ forall m m' : mem,
+ forall chunk addr args chunk' addr' args' v a a' rs,
+ (eval_addressing genv sp addr (rs ## args)) = Some a ->
+ (eval_addressing genv sp addr' (rs ## args')) = Some a' ->
+ (may_overlap chunk addr args chunk' addr' args') = false ->
+ (Mem.storev chunk m a v) = Some m' ->
+ (Mem.loadv chunk' m' a') = (Mem.loadv chunk' m a').
+Proof.
+ intros until rs.
+ intros ADDR ADDR' OVERLAP STORE.
+ destruct addr; destruct addr'; try discriminate.
+ { (* Aindexed / Aindexed *)
+ destruct args as [ | base [ | ]]. 1,3: discriminate.
+ destruct args' as [ | base' [ | ]]. 1,3: discriminate.
+ simpl in OVERLAP.
+ destruct (peq base base'). 2: discriminate.
+ subst base'.
+ destruct (can_swap_accesses_ofs (Int.unsigned i0) chunk' (Int.unsigned i) chunk) eqn:SWAP.
+ 2: discriminate.
+ simpl in *.
+ eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
+ }
+Qed.
+
+End SOUNDNESS.
diff --git a/arm/Conventions1.v b/arm/Conventions1.v
index c5277e8d..fe49a781 100644
--- a/arm/Conventions1.v
+++ b/arm/Conventions1.v
@@ -104,13 +104,12 @@ Definition is_float_reg (r: mreg): bool :=
representation with a single LDM instruction. *)
Definition loc_result (s: signature) : rpair mreg :=
- match s.(sig_res) with
- | None => One R0
- | Some (Tint | Tany32) => One R0
- | Some (Tfloat | Tsingle | Tany64) => One F0
- | Some Tlong => if Archi.big_endian
- then Twolong R0 R1
- else Twolong R1 R0
+ match proj_sig_res s with
+ | Tint | Tany32 => One R0
+ | Tfloat | Tsingle | Tany64 => One F0
+ | Tlong => if Archi.big_endian
+ then Twolong R0 R1
+ else Twolong R1 R0
end.
(** The result registers have types compatible with that given in the signature. *)
@@ -119,7 +118,7 @@ Lemma loc_result_type:
forall sig,
subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
Proof.
- intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; destruct Archi.big_endian; auto.
+ intros. unfold loc_result. destruct (proj_sig_res sig); destruct Archi.big_endian; auto.
Qed.
(** The result locations are caller-save registers *)
@@ -129,7 +128,7 @@ Lemma loc_result_caller_save:
forall_rpair (fun r => is_callee_save r = false) (loc_result s).
Proof.
intros.
- unfold loc_result. destruct (sig_res s) as [[]|]; destruct Archi.big_endian; simpl; auto.
+ unfold loc_result. destruct (proj_sig_res s); destruct Archi.big_endian; simpl; auto.
Qed.
(** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
@@ -139,14 +138,13 @@ Lemma loc_result_pair:
match loc_result sg with
| One _ => True
| Twolong r1 r2 =>
- r1 <> r2 /\ sg.(sig_res) = Some Tlong
+ r1 <> r2 /\ proj_sig_res sg = Tlong
/\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
/\ Archi.ptr64 = false
end.
Proof.
- intros; unfold loc_result; destruct (sig_res sg) as [[]|]; destruct Archi.big_endian; auto.
- intuition congruence.
- intuition congruence.
+ intros; unfold loc_result; destruct (proj_sig_res sg); auto.
+ destruct Archi.big_endian; intuition congruence.
Qed.
(** The location of the result depends only on the result part of the signature *)
@@ -154,7 +152,7 @@ Qed.
Lemma loc_result_exten:
forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2.
Proof.
- intros. unfold loc_result. rewrite H; auto.
+ intros. unfold loc_result, proj_sig_res. rewrite H; auto.
Qed.
(** ** Location of function arguments *)
@@ -271,48 +269,6 @@ Definition loc_arguments (s: signature) : list (rpair loc) :=
else loc_arguments_hf s.(sig_args) 0 0 0
end.
-(** [size_arguments s] returns the number of [Outgoing] slots used
- to call a function with signature [s]. *)
-
-Fixpoint size_arguments_hf (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z :=
- match tyl with
- | nil => ofs
- | (Tint|Tany32) :: tys =>
- if zlt ir 4
- then size_arguments_hf tys (ir + 1) fr ofs
- else size_arguments_hf tys ir fr (ofs + 1)
- | (Tfloat|Tany64) :: tys =>
- if zlt fr 8
- then size_arguments_hf tys ir (fr + 1) ofs
- else size_arguments_hf tys ir fr (align ofs 2 + 2)
- | Tsingle :: tys =>
- if zlt fr 8
- then size_arguments_hf tys ir (fr + 1) ofs
- else size_arguments_hf tys ir fr (ofs + 1)
- | Tlong :: tys =>
- let ir := align ir 2 in
- if zlt ir 4
- then size_arguments_hf tys (ir + 2) fr ofs
- else size_arguments_hf tys ir fr (align ofs 2 + 2)
- end.
-
-Fixpoint size_arguments_sf (tyl: list typ) (ofs: Z) {struct tyl} : Z :=
- match tyl with
- | nil => Z.max 0 ofs
- | (Tint | Tsingle | Tany32) :: tys => size_arguments_sf tys (ofs + 1)
- | (Tfloat | Tlong | Tany64) :: tys => size_arguments_sf tys (align ofs 2 + 2)
- end.
-
-Definition size_arguments (s: signature) : Z :=
- match Archi.abi with
- | Archi.Softfloat =>
- size_arguments_sf s.(sig_args) (-4)
- | Archi.Hardfloat =>
- if s.(sig_cc).(cc_vararg)
- then size_arguments_sf s.(sig_args) (-4)
- else size_arguments_hf s.(sig_args) 0 0 0
- end.
-
(** Argument locations are either non-temporary registers or [Outgoing]
stack slots at nonnegative offsets. *)
@@ -473,173 +429,15 @@ Qed.
Hint Resolve loc_arguments_acceptable: locs.
-(** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
-
-Remark size_arguments_hf_above:
- forall tyl ir fr ofs0,
- ofs0 <= size_arguments_hf tyl ir fr ofs0.
-Proof.
- induction tyl; simpl; intros.
- omega.
- destruct a.
- destruct (zlt ir 4); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega.
- destruct (zlt fr 8); eauto.
- apply Z.le_trans with (align ofs0 2). apply align_le; omega.
- apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
- set (ir' := align ir 2).
- destruct (zlt ir' 4); eauto.
- apply Z.le_trans with (align ofs0 2). apply align_le; omega.
- apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
- destruct (zlt fr 8); eauto.
- apply Z.le_trans with (ofs0 + 1); eauto. omega.
- destruct (zlt ir 4); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega.
- destruct (zlt fr 8); eauto.
- apply Z.le_trans with (align ofs0 2). apply align_le; omega.
- apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
-Qed.
-
-Remark size_arguments_sf_above:
- forall tyl ofs0,
- Z.max 0 ofs0 <= size_arguments_sf tyl ofs0.
-Proof.
- induction tyl; simpl; intros.
- omega.
- destruct a; (eapply Z.le_trans; [idtac|eauto]).
- xomega.
- assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega.
- assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega.
- xomega.
- xomega.
- assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega.
-Qed.
-
-Lemma size_arguments_above:
- forall s, size_arguments s >= 0.
-Proof.
- intros; unfold size_arguments. apply Z.le_ge.
- assert (0 <= size_arguments_sf (sig_args s) (-4)).
- { change 0 with (Z.max 0 (-4)). apply size_arguments_sf_above. }
- assert (0 <= size_arguments_hf (sig_args s) 0 0 0).
- { apply size_arguments_hf_above. }
- destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; auto.
-Qed.
-
-Lemma loc_arguments_hf_bounded:
- forall ofs ty tyl ir fr ofs0,
- In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_hf tyl ir fr ofs0)) ->
- ofs + typesize ty <= size_arguments_hf tyl ir fr ofs0.
-Proof.
- induction tyl; simpl; intros.
- elim H.
- destruct a.
-- (* int *)
- destruct (zlt ir 4); destruct H.
- discriminate.
- eauto.
- inv H. apply size_arguments_hf_above.
- eauto.
-- (* float *)
- destruct (zlt fr 8); destruct H.
- discriminate.
- eauto.
- inv H. apply size_arguments_hf_above.
- eauto.
-- (* long *)
- destruct (zlt (align ir 2) 4).
- destruct H. discriminate. destruct H. discriminate. eauto.
- destruct Archi.big_endian.
- destruct H. inv H.
- eapply Z.le_trans. 2: apply size_arguments_hf_above. simpl; omega.
- destruct H. inv H.
- rewrite <- Z.add_assoc. simpl. apply size_arguments_hf_above.
- eauto.
- destruct H. inv H.
- rewrite <- Z.add_assoc. simpl. apply size_arguments_hf_above.
- destruct H. inv H.
- eapply Z.le_trans. 2: apply size_arguments_hf_above. simpl; omega.
- eauto.
-- (* float *)
- destruct (zlt fr 8); destruct H.
- discriminate.
- eauto.
- inv H. apply size_arguments_hf_above.
- eauto.
-- (* any32 *)
- destruct (zlt ir 4); destruct H.
- discriminate.
- eauto.
- inv H. apply size_arguments_hf_above.
- eauto.
-- (* any64 *)
- destruct (zlt fr 8); destruct H.
- discriminate.
- eauto.
- inv H. apply size_arguments_hf_above.
- eauto.
-Qed.
-
-Lemma loc_arguments_sf_bounded:
- forall ofs ty tyl ofs0,
- In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf tyl ofs0)) ->
- Z.max 0 (ofs + typesize ty) <= size_arguments_sf tyl ofs0.
-Proof.
- induction tyl; simpl; intros.
- elim H.
- destruct a.
-- (* int *)
- destruct H.
- destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above.
- eauto.
-- (* float *)
- destruct H.
- destruct (zlt (align ofs0 2) 0); inv H. apply size_arguments_sf_above.
- eauto.
-- (* long *)
- destruct H.
- destruct Archi.big_endian.
- destruct (zlt (align ofs0 2) 0); inv H.
- eapply Z.le_trans. 2: apply size_arguments_sf_above. simpl; xomega.
- destruct (zlt (align ofs0 2) 0); inv H.
- rewrite <- Z.add_assoc. simpl. apply size_arguments_sf_above.
- destruct H.
- destruct Archi.big_endian.
- destruct (zlt (align ofs0 2) 0); inv H.
- rewrite <- Z.add_assoc. simpl. apply size_arguments_sf_above.
- destruct (zlt (align ofs0 2) 0); inv H.
- eapply Z.le_trans. 2: apply size_arguments_sf_above. simpl; xomega.
- eauto.
-- (* float *)
- destruct H.
- destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above.
- eauto.
-- (* any32 *)
- destruct H.
- destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above.
- eauto.
-- (* any64 *)
- destruct H.
- destruct (zlt (align ofs0 2) 0); inv H. apply size_arguments_sf_above.
- eauto.
-Qed.
-
-Lemma loc_arguments_bounded:
- forall (s: signature) (ofs: Z) (ty: typ),
- In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) ->
- ofs + typesize ty <= size_arguments s.
-Proof.
- unfold loc_arguments, size_arguments; intros.
- assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf (sig_args s) (-4))) ->
- ofs + typesize ty <= size_arguments_sf (sig_args s) (-4)).
- { intros. eapply Z.le_trans. 2: eapply loc_arguments_sf_bounded; eauto. xomega. }
- assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_hf (sig_args s) 0 0 0)) ->
- ofs + typesize ty <= size_arguments_hf (sig_args s) 0 0 0).
- { intros. eapply loc_arguments_hf_bounded; eauto. }
- destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; eauto.
-Qed.
-
Lemma loc_arguments_main:
loc_arguments signature_main = nil.
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/backend/Allocation.v b/backend/Allocation.v
index 6e4fcc82..d18b07a9 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -738,11 +738,11 @@ Function add_equations_args (rl: list reg) (tyl: list typ) (ll: list (rpair loc)
(** [add_equations_res] is similar but is specialized to the case where
there is only one pseudo-register. *)
-Function add_equations_res (r: reg) (oty: option typ) (p: rpair mreg) (e: eqs) : option eqs :=
- match p, oty with
+Function add_equations_res (r: reg) (ty: typ) (p: rpair mreg) (e: eqs) : option eqs :=
+ match p, ty with
| One mr, _ =>
Some (add_equation (Eq Full r (R mr)) e)
- | Twolong mr1 mr2, Some Tlong =>
+ | Twolong mr1 mr2, Tlong =>
if Archi.ptr64 then None else
Some (add_equation (Eq Low r (R mr2)) (add_equation (Eq High r (R mr1)) e))
| _, _ =>
@@ -1088,7 +1088,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
| BStailcall sg ros args mv1 ros' =>
let args' := loc_arguments sg in
assertion (tailcall_is_possible sg);
- assertion (opt_typ_eq sg.(sig_res) f.(RTL.fn_sig).(sig_res));
+ assertion (rettype_eq sg.(sig_res) f.(RTL.fn_sig).(sig_res));
assertion (ros_compatible_tailcall ros');
do e1 <- add_equation_ros ros ros' empty_eqs;
do e2 <- add_equations_args args (sig_args sg) args' e1;
@@ -1118,7 +1118,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
track_moves env mv empty_eqs
| BSreturn (Some arg) mv =>
let arg' := loc_result (RTL.fn_sig f) in
- do e1 <- add_equations_res arg (sig_res (RTL.fn_sig f)) arg' empty_eqs;
+ do e1 <- add_equations_res arg (proj_sig_res (RTL.fn_sig f)) arg' empty_eqs;
track_moves env mv e1
end.
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 3d8fb451..b6880860 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -1301,10 +1301,10 @@ Proof.
Qed.
Lemma add_equations_res_lessdef:
- forall r oty l e e' rs ls,
- add_equations_res r oty l e = Some e' ->
+ forall r ty l e e' rs ls,
+ add_equations_res r ty l e = Some e' ->
satisf rs ls e' ->
- Val.has_type rs#r (match oty with Some ty => ty | None => Tint end) ->
+ Val.has_type rs#r ty ->
Val.lessdef rs#r (Locmap.getpair (map_rpair R l) ls).
Proof.
intros. functional inversion H; simpl.
@@ -1892,7 +1892,7 @@ Qed.
Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signature -> Prop :=
| match_stackframes_nil: forall sg,
- sg.(sig_res) = Some Tint ->
+ sg.(sig_res) = Tint ->
match_stackframes nil nil sg
| match_stackframes_cons:
forall res f sp pc rs s tf bb ls ts sg an e env
@@ -2498,13 +2498,13 @@ Proof.
(return_regs (parent_locset ts) ls1))
with (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f))) ls1).
eapply add_equations_res_lessdef; eauto.
- rewrite H13. apply WTRS.
+ rewrite <- H14. apply WTRS.
generalize (loc_result_caller_save (RTL.fn_sig f)).
destruct (loc_result (RTL.fn_sig f)); simpl.
intros A; rewrite A; auto.
intros [A B]; rewrite A, B; auto.
apply return_regs_agree_callee_save.
- unfold proj_sig_res. rewrite <- H11; rewrite H13. apply WTRS.
+ rewrite <- H11, <- H14. apply WTRS.
(* internal function *)
- monadInv FUN. simpl in *.
@@ -2536,7 +2536,8 @@ Proof.
simpl. destruct (loc_result (ef_sig ef)) eqn:RES; simpl.
rewrite Locmap.gss; auto.
generalize (loc_result_pair (ef_sig ef)); rewrite RES; intros (A & B & C & D & E).
- exploit external_call_well_typed; eauto. unfold proj_sig_res; rewrite B. intros WTRES'.
+ assert (WTRES': Val.has_type v' Tlong).
+ { rewrite <- B. eapply external_call_well_typed; eauto. }
rewrite Locmap.gss. rewrite Locmap.gso by (red; auto). rewrite Locmap.gss.
rewrite val_longofwords_eq_1 by auto. auto.
red; intros. rewrite (AG l H0).
diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index b1d822db..cc171cae 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -100,7 +100,7 @@ let translate_annot sp preg_to_dwarf annot =
| a::_ -> aux a)
let builtin_nop =
- let signature ={sig_args = []; sig_res = None; sig_cc = cc_default} in
+ let signature ={sig_args = []; sig_res = Tvoid; sig_cc = cc_default} in
let name = coqstring_of_camlstring "__builtin_nop" in
Pbuiltin(EF_builtin(name,signature),[],BR_none)
diff --git a/backend/CSE2.v b/backend/CSE2.v
index 38a46c1b..be72405b 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -6,7 +6,7 @@ David Monniaux, CNRS, VERIMAG
Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
-Require Import Memory Registers Op RTL Maps.
+Require Import Memory Registers Op RTL Maps CSE2deps.
(* Static analysis *)
@@ -265,7 +265,7 @@ Definition kill_sym_val (dst : reg) (sv : sym_val) :=
Definition kill_reg (dst : reg) (rel : RELATION.t) :=
PTree.filter1 (fun x => negb (kill_sym_val dst x))
(PTree.remove dst rel).
-
+
Definition kill_sym_val_mem (sv: sym_val) :=
match sv with
| SMove _ => false
@@ -273,16 +273,28 @@ Definition kill_sym_val_mem (sv: sym_val) :=
| SLoad _ _ _ => true
end.
+Definition kill_sym_val_store chunk addr args (sv: sym_val) :=
+ match sv with
+ | SMove _ => false
+ | SOp op _ => op_depends_on_memory op
+ | SLoad chunk' addr' args' => may_overlap chunk addr args chunk' addr' args'
+ end.
+
Definition kill_mem (rel : RELATION.t) :=
PTree.filter1 (fun x => negb (kill_sym_val_mem x)) rel.
-
Definition forward_move (rel : RELATION.t) (x : reg) : reg :=
match rel ! x with
| Some (SMove org) => org
| _ => x
end.
+Definition kill_store1 chunk addr args rel :=
+ PTree.filter1 (fun x => negb (kill_sym_val_store chunk addr args x)) rel.
+
+Definition kill_store chunk addr args rel :=
+ kill_store1 chunk addr (List.map (forward_move rel) args) rel.
+
Definition move (src dst : reg) (rel : RELATION.t) :=
PTree.set dst (SMove (forward_move rel src)) (kill_reg dst rel).
@@ -395,7 +407,7 @@ Definition apply_instr instr (rel : RELATION.t) : RB.t :=
| Inop _
| Icond _ _ _ _
| Ijumptable _ _ => Some rel
- | Istore _ _ _ _ _ => Some (kill_mem rel)
+ | Istore chunk addr args _ _ => Some (kill_store chunk addr args rel)
| Iop op args dst _ => Some (gen_oper op dst args rel)
| Iload trap chunk addr args dst _ => Some (load chunk addr dst args rel)
| Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel))
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 254cc4ce..7e1dd430 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -13,7 +13,8 @@ Require Import Memory Registers Op RTL Maps.
Require Import Globalenvs Values.
Require Import Linking Values Memory Globalenvs Events Smallstep.
Require Import Registers Op RTL.
-Require Import CSE2.
+Require Import CSE2 CSE2deps CSE2depsproof.
+Require Import Lia.
Lemma args_unaffected:
forall rs : regset,
@@ -390,6 +391,7 @@ Proof.
apply REC; auto.
Qed.
+
Lemma find_load_sound :
forall rel : RELATION.t,
forall chunk : memory_chunk,
@@ -566,6 +568,20 @@ Proof.
destruct s; congruence.
Qed.
+
+Lemma forward_move_rs:
+ forall rel arg rs,
+ sem_rel rel rs ->
+ rs # (forward_move rel arg) = rs # arg.
+Proof.
+ unfold forward_move, sem_rel, sem_reg, sem_sym_val in *.
+ intros until rs.
+ intro REL.
+ pose proof (REL arg) as RELarg.
+ destruct (rel ! arg); trivial.
+ destruct s; congruence.
+Qed.
+
Lemma oper_sound :
forall rel : RELATION.t,
forall op : operation,
@@ -984,7 +1000,40 @@ Proof.
apply op_depends_on_memory_correct; auto.
}
Qed.
-
+
+Lemma kill_store_sound :
+ forall m m' : mem,
+ forall rel : RELATION.t,
+ forall chunk addr args a v rs,
+ (eval_addressing genv sp addr (rs ## args)) = Some a ->
+ (Mem.storev chunk m a v) = Some m' ->
+ sem_rel m rel rs -> sem_rel m' (kill_store chunk addr args rel) rs.
+Proof.
+ unfold sem_rel, sem_reg.
+ intros until rs.
+ intros ADDR STORE SEM x.
+ pose proof (SEM x) as SEMx.
+ unfold kill_store, kill_store1.
+ rewrite PTree.gfilter1.
+ destruct (rel ! x) as [ sv | ].
+ 2: reflexivity.
+ destruct sv; simpl in *; trivial.
+ {
+ destruct op_depends_on_memory eqn:DEPENDS; simpl; trivial.
+ rewrite SEMx.
+ apply op_depends_on_memory_correct; auto.
+ }
+ destruct may_overlap eqn:OVERLAP; simpl; trivial.
+ destruct (eval_addressing genv sp addr0 rs ## args0) eqn:ADDR0.
+ {
+ erewrite may_overlap_sound with (args := (map (forward_move rel) args)).
+ all: try eassumption.
+
+ erewrite forward_move_map by eassumption.
+ assumption.
+ }
+ intuition congruence.
+Qed.
End SOUNDNESS.
Definition match_prog (p tp: RTL.program) :=
@@ -1072,6 +1121,7 @@ Definition fmap_sem' := fmap_sem fundef unit ge.
Definition subst_arg_ok' := subst_arg_ok fundef unit ge.
Definition subst_args_ok' := subst_args_ok fundef unit ge.
Definition kill_mem_sound' := kill_mem_sound fundef unit ge.
+Definition kill_store_sound' := kill_store_sound fundef unit ge.
Lemma sem_rel_b_ge:
forall rb1 rb2 : RB.t,
@@ -1241,9 +1291,9 @@ Proof.
{
f_equal.
symmetry.
- apply find_load_sound' with (chunk := chunk) (m := m) (a := a) (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs); trivial.
rewrite MAP in H0.
- assumption.
+ eapply find_load_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs).
+ all: eassumption.
}
unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
}
@@ -1268,36 +1318,37 @@ Proof.
apply load_sound with (a := a); auto.
}
{
- econstructor; split.
- assert (eval_addressing tge sp addr rs ## args = Some a).
- rewrite <- H0.
- apply eval_addressing_preserved. exact symbols_preserved.
- eapply exec_Iload; eauto.
- rewrite (subst_args_ok' sp m); assumption.
- constructor; auto.
-
- simpl in *.
- unfold fmap_sem', fmap_sem in *.
- destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
- destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
- apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
+ econstructor; split.
+ assert (eval_addressing tge sp addr rs ## args = Some a).
+ rewrite <- H0.
+ apply eval_addressing_preserved. exact symbols_preserved.
+ eapply exec_Iload; eauto.
+ rewrite (subst_args_ok' sp m); assumption.
+ constructor; auto.
+
+ simpl in *.
+ unfold fmap_sem', fmap_sem in *.
+ destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+ destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+ apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
+ {
+ replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
{
- replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
- {
- eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
- 2: apply apply_instr'_bot.
- simpl. tauto.
- }
- unfold apply_instr'.
- rewrite H.
- rewrite MPC.
- simpl.
- reflexivity.
+ eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+ 2: apply apply_instr'_bot.
+ simpl. tauto.
}
- apply load_sound with (a := a); assumption.
+ unfold apply_instr'.
+ rewrite H.
+ rewrite MPC.
+ simpl.
+ reflexivity.
+ }
+ apply load_sound with (a := a); assumption.
}
-- unfold transf_instr in *.
+- (* load notrap1 *)
+ unfold transf_instr in *.
destruct find_load_in_fmap eqn:FIND_LOAD.
{
unfold find_load_in_fmap, fmap_sem', fmap_sem in *.
@@ -1306,16 +1357,16 @@ Proof.
change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *.
destruct (map # pc) as [mpc | ] eqn:MPC.
2: discriminate.
-
econstructor; split.
{
eapply exec_Iop with (v := (default_notrap_load_value chunk)); eauto.
+ simpl.
rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
- { simpl.
+ {
f_equal.
- apply find_load_notrap1_sound' with (chunk := chunk) (m := m) (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs); trivial.
rewrite MAP in H0.
- assumption.
+ eapply find_load_notrap1_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs).
+ all: eassumption.
}
unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
}
@@ -1339,37 +1390,38 @@ Proof.
unfold sem_rel_b', sem_rel_b.
apply load_notrap1_sound; auto.
}
- {
- econstructor; split.
- assert (eval_addressing tge sp addr rs ## args = None).
- rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
- eapply exec_Iload_notrap1; eauto.
- rewrite subst_args_ok with (genv := ge) (sp := sp) (m := m) ; assumption.
- constructor; auto.
+ {
+ econstructor; split.
+ assert (eval_addressing tge sp addr rs ## args = None).
+ rewrite <- H0.
+ apply eval_addressing_preserved. exact symbols_preserved.
+ eapply exec_Iload_notrap1; eauto.
+ rewrite (subst_args_ok' sp m); assumption.
+ constructor; auto.
- simpl in *.
- unfold fmap_sem', fmap_sem in *.
- destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
- destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
- apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
+ simpl in *.
+ unfold fmap_sem', fmap_sem in *.
+ destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+ destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+ apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
+ {
+ replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
{
- replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
- {
- eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
- 2: apply apply_instr'_bot.
- simpl. tauto.
- }
- unfold apply_instr'.
- rewrite H.
- rewrite MPC.
- simpl.
- reflexivity.
+ eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+ 2: apply apply_instr'_bot.
+ simpl. tauto.
}
- apply load_notrap1_sound; trivial.
+ unfold apply_instr'.
+ rewrite H.
+ rewrite MPC.
+ simpl.
+ reflexivity.
+ }
+ apply load_notrap1_sound; assumption.
}
-- (* load notrap2 *)
- unfold transf_instr in *.
+(* load notrap2 *)
+- unfold transf_instr in *.
destruct find_load_in_fmap eqn:FIND_LOAD.
{
unfold find_load_in_fmap, fmap_sem', fmap_sem in *.
@@ -1385,9 +1437,9 @@ Proof.
rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
{
f_equal.
- apply find_load_notrap2_sound' with (chunk := chunk) (m := m) (a := a) (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs); trivial.
rewrite MAP in H0.
- assumption.
+ eapply find_load_notrap2_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs).
+ all: try eassumption.
}
unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
}
@@ -1411,19 +1463,20 @@ Proof.
unfold sem_rel_b', sem_rel_b.
apply load_notrap2_sound with (a := a); auto.
}
- {
+ {
econstructor; split.
assert (eval_addressing tge sp addr rs ## args = Some a).
- rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+ rewrite <- H0.
+ apply eval_addressing_preserved. exact symbols_preserved.
eapply exec_Iload_notrap2; eauto.
- rewrite subst_args_ok with (genv := ge) (sp := sp) (m := m); assumption.
+ rewrite (subst_args_ok' sp m); assumption.
constructor; auto.
simpl in *.
unfold fmap_sem', fmap_sem in *.
destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
- apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
+ apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
{
replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
{
@@ -1454,9 +1507,9 @@ Proof.
unfold fmap_sem', fmap_sem in *.
destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
- apply sem_rel_b_ge with (rb2 := Some (kill_mem mpc)); trivial.
+ apply sem_rel_b_ge with (rb2 := Some (kill_store chunk addr args mpc)); trivial.
{
- replace (Some (kill_mem mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+ replace (Some (kill_store chunk addr args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
{
eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
2: apply apply_instr'_bot.
@@ -1468,8 +1521,7 @@ Proof.
rewrite H.
reflexivity.
}
- apply (kill_mem_sound' sp m).
- assumption.
+ eapply (kill_store_sound' sp m); eassumption.
(* call *)
- econstructor; split.
@@ -1657,4 +1709,4 @@ Proof.
exact step_simulation.
Qed.
-End PRESERVATION. \ No newline at end of file
+End PRESERVATION.
diff --git a/backend/Cminor.v b/backend/Cminor.v
index ca01ad50..91a4c104 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -676,12 +676,24 @@ Definition outcome_block (out: outcome) : outcome :=
| out => out
end.
+(*
Definition outcome_result_value
- (out: outcome) (retsig: option typ) (vres: val) : Prop :=
+ (out: outcome) (retsig: rettype) (vres: val) : Prop :=
match out with
| Out_normal => vres = Vundef
| Out_return None => vres = Vundef
- | Out_return (Some v) => retsig <> None /\ vres = v
+ | Out_return (Some v) => retsig <> Tvoid /\ vres = v
+ | Out_tailcall_return v => vres = v
+ | _ => False
+ end.
+*)
+
+Definition outcome_result_value
+ (out: outcome) (vres: val) : Prop :=
+ match out with
+ | Out_normal => vres = Vundef
+ | Out_return None => vres = Vundef
+ | Out_return (Some v) => vres = v
| Out_tailcall_return v => vres = v
| _ => False
end.
@@ -711,7 +723,7 @@ Inductive eval_funcall:
Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) ->
set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
exec_stmt f (Vptr sp Ptrofs.zero) e m1 f.(fn_body) t e2 m2 out ->
- outcome_result_value out f.(fn_sig).(sig_res) vres ->
+ outcome_result_value out vres ->
outcome_free_mem out m2 sp f.(fn_stackspace) m3 ->
eval_funcall m (Internal f) vargs t m3 vres
| eval_funcall_external:
@@ -995,7 +1007,7 @@ Proof.
subst vres. replace k with (call_cont k') by congruence.
apply star_one. apply step_return_0; auto.
(* Out_return Some *)
- destruct H3. subst vres.
+ subst vres.
replace k with (call_cont k') by congruence.
apply star_one. eapply step_return_1; eauto.
(* Out_tailcall_return *)
diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v
index fccbda27..92ec45f2 100644
--- a/backend/Cminortyping.v
+++ b/backend/Cminortyping.v
@@ -130,7 +130,7 @@ Definition opt_set (e: S.typenv) (optid: option ident) (ty: typ) : res S.typenv
| Some id => S.set e id ty
end.
-Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv :=
+Fixpoint type_stmt (tret: rettype) (e: S.typenv) (s: stmt) : res S.typenv :=
match s with
| Sskip => OK e
| Sassign id a => type_assign e id a
@@ -141,7 +141,7 @@ Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv :=
do e2 <- type_exprlist e1 args sg.(sig_args);
opt_set e2 optid (proj_sig_res sg)
| Stailcall sg fn args =>
- assertion (opt_typ_eq sg.(sig_res) tret);
+ assertion (rettype_eq sg.(sig_res) tret);
do e1 <- type_expr e fn Tptr;
type_exprlist e1 args sg.(sig_args)
| Sbuiltin optid ef args =>
@@ -163,10 +163,14 @@ Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv :=
| Sswitch sz a tbl dfl =>
type_expr e a (if sz then Tlong else Tint)
| Sreturn opta =>
- match opta, tret with
- | None, _ => OK e
- | Some a, Some t => type_expr e a t
- | _, _ => Error (msg "inconsistent return")
+ match opta with
+ | None => OK e
+ | Some a => type_expr e a (proj_rettype tret)
+(*
+ if rettype_eq tret Tvoid
+ then Error (msg "inconsistent return")
+ else type_expr e a (proj_rettype tret)
+*)
end
| Slabel lbl s1 =>
type_stmt tret e s1
@@ -186,7 +190,7 @@ Definition type_function (f: function) : res typenv :=
Section SPEC.
Variable env: ident -> typ.
-Variable tret: option typ.
+Variable tret: rettype.
Inductive wt_expr: expr -> typ -> Prop :=
| wt_Evar: forall id,
@@ -205,9 +209,9 @@ Inductive wt_expr: expr -> typ -> Prop :=
wt_expr a1 Tptr ->
wt_expr (Eload chunk a1) (type_of_chunk chunk).
-Definition wt_opt_assign (optid: option ident) (optty: option typ) : Prop :=
+Definition wt_opt_assign (optid: option ident) (ty: rettype) : Prop :=
match optid with
- | Some id => match optty with Some ty => ty | None => Tint end = env id
+ | Some id => proj_rettype ty = env id
| _ => True
end.
@@ -251,8 +255,8 @@ Inductive wt_stmt: stmt -> Prop :=
wt_stmt (Sswitch sz a tbl dfl)
| wt_Sreturn_none:
wt_stmt (Sreturn None)
- | wt_Sreturn_some: forall a t,
- tret = Some t -> wt_expr a t ->
+ | wt_Sreturn_some: forall a,
+ wt_expr a (proj_rettype tret) ->
wt_stmt (Sreturn (Some a))
| wt_Slabel: forall lbl s1,
wt_stmt s1 ->
@@ -393,7 +397,7 @@ Proof.
- constructor; eauto.
- constructor.
- constructor; eauto using type_expr_sound with ty.
-- destruct tret, o; try (monadInv T); econstructor; eauto using type_expr_sound with ty.
+- destruct o; try (monadInv T); econstructor; eauto using type_expr_sound with ty.
- constructor; eauto.
- constructor.
Qed.
@@ -414,9 +418,9 @@ Definition wt_env (env: typenv) (e: Cminor.env) : Prop :=
Definition def_env (f: function) (e: Cminor.env) : Prop :=
forall id, In id f.(fn_params) \/ In id f.(fn_vars) -> exists v, e!id = Some v.
-Inductive wt_cont_call: cont -> option typ -> Prop :=
+Inductive wt_cont_call: cont -> rettype -> Prop :=
| wt_cont_Kstop:
- wt_cont_call Kstop (Some Tint)
+ wt_cont_call Kstop Tint
| wt_cont_Kcall: forall optid f sp e k tret env
(WT_FN: wt_function env f)
(WT_CONT: wt_cont env f.(fn_sig).(sig_res) k)
@@ -425,7 +429,7 @@ Inductive wt_cont_call: cont -> option typ -> Prop :=
(WT_DEST: wt_opt_assign env optid tret),
wt_cont_call (Kcall optid f sp e k) tret
-with wt_cont: typenv -> option typ -> cont -> Prop :=
+with wt_cont: typenv -> rettype -> cont -> Prop :=
| wt_cont_Kseq: forall env tret s k,
wt_stmt env tret s ->
wt_cont env tret k ->
@@ -451,7 +455,7 @@ Inductive wt_state: state -> Prop :=
(WT_CONT: wt_cont_call k (funsig f).(sig_res)),
wt_state (Callstate f args k m)
| wt_return_state: forall v k m tret
- (WT_RES: Val.has_type v (match tret with None => Tint | Some t => t end))
+ (WT_RES: Val.has_type v (proj_rettype tret))
(WT_CONT: wt_cont_call k tret),
wt_state (Returnstate v k m).
@@ -651,9 +655,8 @@ Proof.
rewrite H8; eapply call_cont_wt; eauto.
- inv WT_STMT. exploit external_call_well_typed; eauto. intros TRES.
econstructor; eauto using wt_Sskip.
- unfold proj_sig_res in TRES; red in H5.
- destruct optid. rewrite H5 in TRES. apply wt_env_assign; auto. assumption.
- destruct optid. apply def_env_assign; auto. assumption.
+ destruct optid; auto. apply wt_env_assign; auto. rewrite <- H5; auto.
+ destruct optid; auto. apply def_env_assign; auto.
- inv WT_STMT. econstructor; eauto. econstructor; eauto.
- inv WT_STMT. destruct b; econstructor; eauto.
- inv WT_STMT. econstructor; eauto. econstructor; eauto. constructor; auto.
@@ -664,7 +667,7 @@ Proof.
- econstructor; eauto using wt_Sexit.
- inv WT_STMT. econstructor; eauto using call_cont_wt. exact I.
- inv WT_STMT. econstructor; eauto using call_cont_wt.
- rewrite H2. eapply wt_eval_expr; eauto.
+ eapply wt_eval_expr; eauto.
- inv WT_STMT. econstructor; eauto.
- inversion WT_FN; subst.
assert (WT_CK: wt_cont env (sig_res (fn_sig f)) (call_cont k)).
@@ -675,7 +678,7 @@ Proof.
constructor; auto.
apply wt_env_set_locals. apply wt_env_set_params. rewrite H2; auto.
red; intros. apply def_set_locals. destruct H4; auto. left; apply def_set_params; auto.
-- exploit external_call_well_typed; eauto. unfold proj_sig_res. simpl in *. intros.
+- exploit external_call_well_typed; eauto. intros.
econstructor; eauto.
- inv WT_CONT. econstructor; eauto using wt_Sskip.
red in WT_DEST.
diff --git a/backend/Conventions.v b/backend/Conventions.v
index 6025c6b4..14ffb587 100644
--- a/backend/Conventions.v
+++ b/backend/Conventions.v
@@ -34,6 +34,73 @@ Proof.
apply IHpl; auto.
Qed.
+(** ** Stack size of function arguments *)
+
+(** [size_arguments s] returns the number of [Outgoing] slots used
+ to call a function with signature [s]. *)
+
+Definition max_outgoing_1 (accu: Z) (l: loc) : Z :=
+ match l with
+ | S Outgoing ofs ty => Z.max accu (ofs + typesize ty)
+ | _ => accu
+ end.
+
+Definition max_outgoing_2 (accu: Z) (rl: rpair loc) : Z :=
+ match rl with
+ | One l => max_outgoing_1 accu l
+ | Twolong l1 l2 => max_outgoing_1 (max_outgoing_1 accu l1) l2
+ end.
+
+Definition size_arguments (s: signature) : Z :=
+ List.fold_left max_outgoing_2 (loc_arguments s) 0.
+
+(** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
+
+Remark fold_max_outgoing_above:
+ forall l n, fold_left max_outgoing_2 l n >= n.
+Proof.
+ assert (A: forall n l, max_outgoing_1 n l >= n).
+ { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. }
+ induction l; simpl; intros.
+ - omega.
+ - eapply Zge_trans. eauto.
+ destruct a; simpl. apply A. eapply Zge_trans; eauto.
+Qed.
+
+Lemma size_arguments_above:
+ forall s, size_arguments s >= 0.
+Proof.
+ intros. apply fold_max_outgoing_above.
+Qed.
+
+Lemma loc_arguments_bounded:
+ forall (s: signature) (ofs: Z) (ty: typ),
+ In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) ->
+ ofs + typesize ty <= size_arguments s.
+Proof.
+ intros until ty.
+ assert (A: forall n l, n <= max_outgoing_1 n l).
+ { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. }
+ assert (B: forall p n,
+ In (S Outgoing ofs ty) (regs_of_rpair p) ->
+ ofs + typesize ty <= max_outgoing_2 n p).
+ { intros. destruct p; simpl in H; intuition; subst; simpl.
+ - xomega.
+ - eapply Z.le_trans. 2: apply A. xomega.
+ - xomega. }
+ assert (C: forall l n,
+ In (S Outgoing ofs ty) (regs_of_rpairs l) ->
+ ofs + typesize ty <= fold_left max_outgoing_2 l n).
+ { induction l; simpl; intros.
+ - contradiction.
+ - rewrite in_app_iff in H. destruct H.
+ + eapply Z.le_trans. eapply B; eauto.
+ apply Z.ge_le. apply fold_max_outgoing_above.
+ + apply IHl; auto.
+ }
+ apply C.
+Qed.
+
(** ** Location of function parameters *)
(** A function finds the values of its parameter in the same locations
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index a8e9b16b..466b4b75 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -378,7 +378,7 @@ Theorem step_simulation:
step tge s2 t s2'
/\ match_states s1' s2'.
Proof.
- Local Hint Resolve transf_fundef_correct.
+ Local Hint Resolve transf_fundef_correct: core.
induction 1; intros; inv MS.
(* Inop *)
- eapply dupmap_correct in DUPLIC; eauto.
diff --git a/backend/IRC.ml b/backend/IRC.ml
index 67da47da..785b0a2d 100644
--- a/backend/IRC.ml
+++ b/backend/IRC.ml
@@ -238,7 +238,6 @@ type graph = {
according to their types. A variable can be forced into class 2
by giving it a negative spill cost. *)
-
let class_of_reg r =
if Conventions1.is_float_reg r then 1 else 0
diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml
index 609b2637..d58704ca 100644
--- a/backend/Inliningaux.ml
+++ b/backend/Inliningaux.ml
@@ -16,7 +16,7 @@ open FSetAVL
open Maps
open Op
open Ordered
-open !RTL
+open! RTL
module PSet = Make(OrderedPositive)
diff --git a/backend/OpHelpers.v b/backend/OpHelpers.v
index 53414dab..b9b97903 100644
--- a/backend/OpHelpers.v
+++ b/backend/OpHelpers.v
@@ -6,16 +6,16 @@ Require Import Op CminorSel.
runtime library functions. The following type class collects
the names of these functions. *)
-Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default.
-Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default.
-Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default.
-Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default.
-Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default.
-Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default.
-Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default.
-Definition sig_ii_i := mksignature (Tint :: Tint :: nil) (Some Tint) cc_default.
-Definition sig_ff_f := mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default.
-Definition sig_ss_s := mksignature (Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default.
+Definition sig_l_l := mksignature (Tlong :: nil) Tlong cc_default.
+Definition sig_l_f := mksignature (Tlong :: nil) Tfloat cc_default.
+Definition sig_l_s := mksignature (Tlong :: nil) Tsingle cc_default.
+Definition sig_f_l := mksignature (Tfloat :: nil) Tlong cc_default.
+Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) Tlong cc_default.
+Definition sig_li_l := mksignature (Tlong :: Tint :: nil) Tlong cc_default.
+Definition sig_ii_l := mksignature (Tint :: Tint :: nil) Tlong cc_default.
+Definition sig_ii_i := mksignature (Tint :: Tint :: nil) Tint cc_default.
+Definition sig_ff_f := mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default.
+Definition sig_ss_s := mksignature (Tsingle :: Tsingle :: nil) Tsingle cc_default.
Class helper_functions := mk_helper_functions {
i64_dtos: ident; (**r float64 -> signed long *)
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 8652b2c5..d82e6f84 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -99,7 +99,7 @@ let exists_constants () =
let current_function_stacksize = ref 0l
let current_function_sig =
- ref { sig_args = []; sig_res = None; sig_cc = cc_default }
+ ref { sig_args = []; sig_res = Tvoid; sig_cc = cc_default }
(* Functions for printing of symbol names *)
let elf_symbol oc symb =
@@ -268,8 +268,8 @@ let re_asm_param_2 = Str.regexp "%\\([QR]?\\)\\([0-9]+\\)"
let print_inline_asm print_preg oc txt sg args res =
let (operands, ty_operands) =
match sg.sig_res with
- | None -> (args, sg.sig_args)
- | Some tres -> (builtin_arg_of_res res :: args, tres :: sg.sig_args) in
+ | Tvoid -> (args, sg.sig_args)
+ | tres -> (builtin_arg_of_res res :: args, proj_rettype tres :: sg.sig_args) in
let print_fragment = function
| Str.Text s ->
output_string oc s
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 8c255a65..c9a6d399 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -16,7 +16,7 @@
(** Pretty-printer for Cminor *)
open Format
-open !Camlcoq
+open! Camlcoq
open Integers
open AST
open PrintAST
@@ -193,9 +193,7 @@ let print_sig p sg =
List.iter
(fun t -> fprintf p "%s ->@ " (name_of_type t))
sg.sig_args;
- match sg.sig_res with
- | None -> fprintf p "void"
- | Some ty -> fprintf p "%s" (name_of_type ty)
+ fprintf p "%s" (name_of_rettype sg.sig_res)
let rec just_skips s =
match s with
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index a0ca0f17..2c27944a 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -410,12 +410,11 @@ Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list
a1' :: convert_builtin_args al rl1
end.
-Definition convert_builtin_res (map: mapping) (oty: option typ) (r: builtin_res ident) : mon (builtin_res reg) :=
- match r, oty with
- | BR id, _ => do r <- find_var map id; ret (BR r)
- | BR_none, None => ret BR_none
- | BR_none, Some _ => do r <- new_reg; ret (BR r)
- | _, _ => error (Errors.msg "RTLgen: bad builtin_res")
+Definition convert_builtin_res (map: mapping) (ty: rettype) (r: builtin_res ident) : mon (builtin_res reg) :=
+ match r with
+ | BR id => do r <- find_var map id; ret (BR r)
+ | BR_none => if rettype_eq ty Tvoid then ret BR_none else (do r <- new_reg; ret (BR r))
+ | _ => error (Errors.msg "RTLgen: bad builtin_res")
end.
(** Translation of an expression. [transl_expr map a rd nd]
@@ -667,10 +666,7 @@ Fixpoint reserve_labels (s: stmt) (ms: labelmap * state)
(** Translation of a CminorSel function. *)
Definition ret_reg (sig: signature) (rd: reg) : option reg :=
- match sig.(sig_res) with
- | None => None
- | Some ty => Some rd
- end.
+ if rettype_eq sig.(sig_res) Tvoid then None else Some rd.
Definition transl_fun (f: CminorSel.function) (ngoto: labelmap): mon (node * list reg) :=
do (rparams, map1) <- add_vars init_mapping f.(CminorSel.fn_params);
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index aa83da6d..92b48e2b 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -639,8 +639,8 @@ Lemma new_reg_return_ok:
map_valid map s1 ->
return_reg_ok s2 map (ret_reg sig r).
Proof.
- intros. unfold ret_reg. destruct (sig_res sig); constructor.
- eauto with rtlg. eauto with rtlg.
+ intros. unfold ret_reg.
+ destruct (rettype_eq (sig_res sig) Tvoid); constructor; eauto with rtlg.
Qed.
(** * Relational specification of the translation *)
@@ -1224,9 +1224,9 @@ Lemma convert_builtin_res_charact:
Proof.
destruct res; simpl; intros.
- monadInv TR. constructor. unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto.
-- destruct oty; monadInv TR.
-+ constructor. eauto with rtlg.
+- destruct (rettype_eq oty Tvoid); monadInv TR.
+ constructor.
++ constructor. eauto with rtlg.
- monadInv TR.
Qed.
@@ -1350,7 +1350,7 @@ Proof.
intros [C D].
eapply tr_function_intro; eauto with rtlg.
eapply transl_stmt_charact; eauto with rtlg.
- unfold ret_reg. destruct (sig_res (CminorSel.fn_sig f)).
- constructor. eauto with rtlg. eauto with rtlg.
+ unfold ret_reg. destruct (rettype_eq (sig_res (CminorSel.fn_sig f)) Tvoid).
constructor.
+ constructor; eauto with rtlg.
Qed.
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 74bfa582..857f2211 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -151,11 +151,12 @@ Inductive wt_instr : instruction -> Prop :=
list_length_z tbl * 4 <= Int.max_unsigned ->
wt_instr (Ijumptable arg tbl)
| wt_Ireturn_none:
- funct.(fn_sig).(sig_res) = None ->
+ funct.(fn_sig).(sig_res) = Tvoid ->
wt_instr (Ireturn None)
| wt_Ireturn_some:
forall arg ty,
- funct.(fn_sig).(sig_res) = Some ty ->
+ funct.(fn_sig).(sig_res) <> Tvoid ->
+ env arg = proj_sig_res funct.(fn_sig) ->
env arg = ty ->
wt_instr (Ireturn (Some arg)).
@@ -298,7 +299,7 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv :=
| Itailcall sig ros args =>
do e1 <- type_ros e ros;
do e2 <- S.set_list e1 args sig.(sig_args);
- if opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res) then
+ if rettype_eq sig.(sig_res) f.(fn_sig).(sig_res) then
if tailcall_is_possible sig
then OK e2
else Error(msg "tailcall not possible")
@@ -323,9 +324,9 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv :=
then OK e1
else Error(msg "jumptable too big")
| Ireturn optres =>
- match optres, f.(fn_sig).(sig_res) with
- | None, None => OK e
- | Some r, Some t => S.set e r t
+ match optres, rettype_eq f.(fn_sig).(sig_res) Tvoid with
+ | None, left _ => OK e
+ | Some r, right _ => S.set e r (proj_sig_res f.(fn_sig))
| _, _ => Error(msg "bad return")
end
end.
@@ -468,7 +469,7 @@ Proof.
destruct l; try discriminate. destruct l; monadInv EQ0. eauto with ty.
destruct (type_of_operation o) as [targs tres] eqn:TYOP. monadInv EQ0. eauto with ty.
- (* tailcall *)
- destruct (opt_typ_eq (sig_res s) (sig_res (fn_sig f))); try discriminate.
+ destruct (rettype_eq (sig_res s) (sig_res (fn_sig f))); try discriminate.
destruct (tailcall_is_possible s) eqn:TCIP; inv EQ2.
eauto with ty.
- (* builtin *)
@@ -477,7 +478,8 @@ Proof.
destruct (zle (list_length_z l * 4) Int.max_unsigned); inv EQ2.
eauto with ty.
- (* return *)
- simpl in H. destruct o as [r|] eqn: RET; destruct (sig_res (fn_sig f)) as [t|] eqn: RES; try discriminate.
+ simpl in H.
+ destruct o as [r|] eqn: RET; destruct (rettype_eq (sig_res (fn_sig f)) Tvoid); try discriminate.
eauto with ty.
inv H; auto with ty.
Qed.
@@ -519,7 +521,7 @@ Proof.
eapply S.set_sound; eauto with ty.
eauto with ty.
- (* tailcall *)
- destruct (opt_typ_eq (sig_res s) (sig_res (fn_sig f))); try discriminate.
+ destruct (rettype_eq (sig_res s) (sig_res (fn_sig f))); try discriminate.
destruct (tailcall_is_possible s) eqn:TCIP; inv EQ2.
constructor.
eapply type_ros_sound; eauto with ty.
@@ -543,8 +545,9 @@ Proof.
eapply check_successors_sound; eauto.
auto.
- (* return *)
- simpl in H. destruct o as [r|] eqn: RET; destruct (sig_res (fn_sig f)) as [t|] eqn: RES; try discriminate.
- econstructor. eauto. eapply S.set_sound; eauto with ty.
+ simpl in H.
+ destruct o as [r|] eqn: RET; destruct (rettype_eq (sig_res (fn_sig f)) Tvoid); try discriminate.
+ econstructor. auto. eapply S.set_sound; eauto with ty. eauto.
inv H. constructor. auto.
Qed.
@@ -721,9 +724,9 @@ Proof.
rewrite check_successor_complete by auto; simpl.
apply IHtbl0; intros; auto.
- (* return none *)
- rewrite H0. exists e; auto.
+ rewrite H0, dec_eq_true. exists e; auto.
- (* return some *)
- rewrite H0. apply S.set_complete; auto.
+ rewrite dec_eq_false by auto. apply S.set_complete; auto.
Qed.
Lemma type_code_complete:
@@ -882,7 +885,7 @@ Qed.
Inductive wt_stackframes: list stackframe -> signature -> Prop :=
| wt_stackframes_nil: forall sg,
- sg.(sig_res) = Some Tint ->
+ sg.(sig_res) = Tint ->
wt_stackframes nil sg
| wt_stackframes_cons:
forall s res f sp pc rs env sg,
@@ -978,13 +981,13 @@ Proof.
econstructor; eauto.
(* Ireturn *)
econstructor; eauto.
- inv WTI; simpl. auto. unfold proj_sig_res; rewrite H2. auto.
+ inv WTI; simpl. auto. rewrite <- H3. auto.
(* internal function *)
simpl in *. inv H5.
econstructor; eauto.
inv H1. apply wt_init_regs; auto. rewrite wt_params0. auto.
(* external function *)
- econstructor; eauto. simpl.
+ econstructor; eauto.
eapply external_call_well_typed; eauto.
(* return *)
inv H1. econstructor; eauto.
diff --git a/backend/Tailcall.v b/backend/Tailcall.v
index 939abeea..b7a62d74 100644
--- a/backend/Tailcall.v
+++ b/backend/Tailcall.v
@@ -82,7 +82,7 @@ Definition transf_instr (f: function) (pc: node) (instr: instruction) :=
| Icall sig ros args res s =>
if is_return niter f s res
&& tailcall_is_possible sig
- && opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res)
+ && rettype_eq sig.(sig_res) f.(fn_sig).(sig_res)
then Itailcall sig ros args
else instr
| _ => instr
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 5cb1b980..79a5c1cf 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -157,12 +157,10 @@ Lemma transf_instr_charact:
transf_instr_spec f instr (transf_instr f pc instr).
Proof.
intros. unfold transf_instr. destruct instr; try constructor.
- caseEq (is_return niter f n r && tailcall_is_possible s &&
- opt_typ_eq (sig_res s) (sig_res (fn_sig f))); intros.
- destruct (andb_prop _ _ H0). destruct (andb_prop _ _ H1).
- eapply transf_instr_tailcall; eauto.
- eapply is_return_charact; eauto.
- constructor.
+ destruct (is_return niter f n r && tailcall_is_possible s &&
+ rettype_eq (sig_res s) (sig_res (fn_sig f))) eqn:B.
+- InvBooleans. eapply transf_instr_tailcall; eauto. eapply is_return_charact; eauto.
+- constructor.
Qed.
Lemma transf_instr_lookup:
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 9a33768c..e25d2e5f 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -1044,9 +1044,8 @@ Proof.
red; simpl; intros. destruct (plt b (Mem.nextblock m)).
exploit RO; eauto. intros (R & P & Q).
split; auto.
- split. apply bmatch_incr with bc; auto. apply bmatch_inv with m; auto.
- intros. eapply Mem.loadbytes_unchanged_on_1. eapply external_call_readonly; eauto.
- auto. intros; red. apply Q.
+ split. apply bmatch_incr with bc; auto. apply bmatch_ext with m; auto.
+ intros. eapply external_call_readonly with (m2 := m'); eauto.
intros; red; intros; elim (Q ofs).
eapply external_call_max_perm with (m2 := m'); eauto.
destruct (j' b); congruence.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index c132ce7c..779e7bb9 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -3502,11 +3502,6 @@ Proof.
- omegaContradiction.
Qed.
-Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8.
-Proof.
- destruct chunk; simpl; omega.
-Qed.
-
Remark inval_before_contents:
forall i c chunk' av' j,
(inval_before i (i - 7) c)##j = Some (ACval chunk' av') ->
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 24e3cacf..ec5fb4dc 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -33,6 +33,7 @@ type inline_status =
type atom_info =
{ a_storage: C.storage; (* storage class *)
+ a_size: int64 option; (* size in bytes *)
a_alignment: int option; (* alignment *)
a_sections: Sections.section_name list; (* in which section to put it *)
(* 1 section for data, 3 sections (code/lit/jumptbl) for functions *)
@@ -72,9 +73,14 @@ let atom_sections a =
with Not_found ->
[]
-let atom_is_small_data a ofs =
+let atom_is_small_data a ofs =
try
- (Hashtbl.find decl_atom a).a_access = Sections.Access_near
+ let info = Hashtbl.find decl_atom a in
+ info.a_access = Sections.Access_near
+ && (match info.a_size with
+ | None -> false
+ | Some sz ->
+ let ofs = camlint64_of_ptrofs ofs in 0L <= ofs && ofs < sz)
with Not_found ->
false
@@ -376,6 +382,7 @@ let name_for_string_literal s =
Hashtbl.add decl_atom id
{ a_storage = C.Storage_static;
a_alignment = Some 1;
+ a_size = Some (Int64.of_int (String.length s + 1));
a_sections = [Sections.for_stringlit()];
a_access = Sections.Access_default;
a_inline = No_specifier;
@@ -403,9 +410,12 @@ let name_for_wide_string_literal s =
incr stringNum;
let name = Printf.sprintf "__stringlit_%d" !stringNum in
let id = intern_string name in
+ let wchar_size = Machine.((!config).sizeof_wchar) in
Hashtbl.add decl_atom id
{ a_storage = C.Storage_static;
- a_alignment = Some Machine.((!config).sizeof_wchar);
+ a_alignment = Some wchar_size;
+ a_size = Some (Int64.(mul (of_int (List.length s + 1))
+ (of_int wchar_size)));
a_sections = [Sections.for_stringlit()];
a_access = Sections.Access_default;
a_inline = No_specifier;
@@ -1247,6 +1257,7 @@ let convertFundef loc env fd =
Hashtbl.add decl_atom id'
{ a_storage = fd.fd_storage;
a_alignment = None;
+ a_size = None;
a_sections = Sections.for_function env id' fd.fd_attrib;
a_access = Sections.Access_default;
a_inline = inline;
@@ -1341,6 +1352,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) =
Hashtbl.add decl_atom id'
{ a_storage = sto;
a_alignment = Some (Z.to_int al);
+ a_size = Some (Z.to_int64 sz);
a_sections = [section];
a_access = access;
a_inline = No_specifier;
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 2942080b..b08c3ad7 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -460,6 +460,14 @@ Definition do_ef_free
check (zlt 0 (Ptrofs.unsigned sz));
do m' <- Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz);
Some(w, E0, Vundef, m')
+ | Vint n :: nil =>
+ if Int.eq_dec n Int.zero && negb Archi.ptr64
+ then Some(w, E0, Vundef, m)
+ else None
+ | Vlong n :: nil =>
+ if Int64.eq_dec n Int64.zero && Archi.ptr64
+ then Some(w, E0, Vundef, m)
+ else None
| _ => None
end.
@@ -544,45 +552,51 @@ Proof with try congruence.
- eapply do_external_function_sound; eauto.
}
destruct ef; simpl.
-(* EF_external *)
+- (* EF_external *)
eapply do_external_function_sound; eauto.
-(* EF_builtin *)
+- (* EF_builtin *)
eapply BF_EX; eauto.
-(* EF_runtime *)
+- (* EF_runtime *)
eapply BF_EX; eauto.
-(* EF_vload *)
+- (* EF_vload *)
unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs...
mydestr. destruct p as [[w'' t''] v]; mydestr.
exploit do_volatile_load_sound; eauto. intuition. econstructor; eauto.
- auto.
-(* EF_vstore *)
+- (* EF_vstore *)
unfold do_ef_volatile_store. destruct vargs... destruct v... destruct vargs... destruct vargs...
mydestr. destruct p as [[w'' t''] m'']. mydestr.
exploit do_volatile_store_sound; eauto. intuition. econstructor; eauto.
- auto.
-(* EF_malloc *)
+- (* EF_malloc *)
unfold do_ef_malloc. destruct vargs... destruct vargs... mydestr.
destruct (Mem.alloc m (- size_chunk Mptr) (Ptrofs.unsigned i)) as [m1 b] eqn:?. mydestr.
split. apply SIZE in Heqo. subst v. econstructor; eauto. constructor.
-(* EF_free *)
- unfold do_ef_free. destruct vargs... destruct v... destruct vargs...
- mydestr. split. apply SIZE in Heqo0. econstructor; eauto. congruence. omega. constructor.
-(* EF_memcpy *)
+- (* EF_free *)
+ unfold do_ef_free. destruct vargs... destruct v...
++ destruct vargs... mydestr; InvBooleans; subst i.
+ replace (Vint Int.zero) with Vnullptr. split; constructor.
+ apply negb_true_iff in H0. unfold Vnullptr; rewrite H0; auto.
++ destruct vargs... mydestr; InvBooleans; subst i.
+ replace (Vlong Int64.zero) with Vnullptr. split; constructor.
+ unfold Vnullptr; rewrite H0; auto.
++ destruct vargs... mydestr.
+ split. apply SIZE in Heqo0. econstructor; eauto. congruence. omega.
+ constructor.
+- (* EF_memcpy *)
unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs...
destruct v... destruct vargs... mydestr.
apply Decidable_sound in Heqb1. red in Heqb1.
split. econstructor; eauto; tauto. constructor.
-(* EF_annot *)
+- (* EF_annot *)
unfold do_ef_annot. mydestr.
split. constructor. apply list_eventval_of_val_sound; auto.
econstructor. constructor; eauto. constructor.
-(* EF_annot_val *)
+- (* EF_annot_val *)
unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr.
split. constructor. apply eventval_of_val_sound; auto.
econstructor. constructor; eauto. constructor.
-(* EF_inline_asm *)
+- (* EF_inline_asm *)
eapply do_inline_assembly_sound; eauto.
-(* EF_debug *)
+- (* EF_debug *)
unfold do_ef_debug. mydestr. split; constructor.
Qed.
@@ -605,37 +619,38 @@ Proof.
- eapply do_external_function_complete; eauto.
}
destruct ef; simpl in *.
-(* EF_external *)
+- (* EF_external *)
eapply do_external_function_complete; eauto.
-(* EF_builtin *)
+- (* EF_builtin *)
eapply BF_EX; eauto.
-(* EF_runtime *)
+- (* EF_runtime *)
eapply BF_EX; eauto.
-(* EF_vload *)
+- (* EF_vload *)
inv H; unfold do_ef_volatile_load.
exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto.
-(* EF_vstore *)
+- (* EF_vstore *)
inv H; unfold do_ef_volatile_store.
exploit do_volatile_store_complete; eauto. intros EQ; rewrite EQ; auto.
-(* EF_malloc *)
+- (* EF_malloc *)
inv H; unfold do_ef_malloc.
inv H0. erewrite SIZE by eauto. rewrite H1, H2. auto.
-(* EF_free *)
+- (* EF_free *)
inv H; unfold do_ef_free.
- inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. omega.
-(* EF_memcpy *)
++ inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. omega.
++ inv H0. unfold Vnullptr; destruct Archi.ptr64; auto.
+- (* EF_memcpy *)
inv H; unfold do_ef_memcpy.
inv H0. rewrite Decidable_complete. rewrite H7; rewrite H8; auto.
red. tauto.
-(* EF_annot *)
+- (* EF_annot *)
inv H; unfold do_ef_annot. inv H0. inv H6. inv H4.
rewrite (list_eventval_of_val_complete _ _ _ H1). auto.
-(* EF_annot_val *)
+- (* EF_annot_val *)
inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4.
rewrite (eventval_of_val_complete _ _ _ H1). auto.
-(* EF_inline_asm *)
+- (* EF_inline_asm *)
eapply do_inline_assembly_complete; eauto.
-(* EF_debug *)
+- (* EF_debug *)
inv H. inv H0. reflexivity.
Qed.
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index aa73abb0..143e87a3 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -140,8 +140,8 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
| Tfloat F64 _, Tfloat F32 _ => cast_case_s2f
| Tfloat F32 _, Tfloat F64 _ => cast_case_f2s
(* To pointer types *)
- | Tpointer _ _, Tint _ _ _ =>
- if Archi.ptr64 then cast_case_i2l Unsigned else cast_case_pointer
+ | Tpointer _ _, Tint _ si _ =>
+ if Archi.ptr64 then cast_case_i2l si else cast_case_pointer
| Tpointer _ _, Tlong _ _ =>
if Archi.ptr64 then cast_case_pointer else cast_case_l2i I32 Unsigned
| Tpointer _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_pointer
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index a76a14ba..6d2b470f 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -444,7 +444,7 @@ Lemma red_selection:
Proof.
intros. unfold Eselection.
set (t := typ_of_type ty).
- set (sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default).
+ set (sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default).
assert (LK: lookup_builtin_function "__builtin_sel"%string sg = Some (BI_standard (BI_select t))).
{ unfold sg, t; destruct ty as [ | ? ? ? | ? | [] ? | ? ? | ? ? ? | ? ? ? | ? ? | ? ? ];
simpl; unfold Tptr; destruct Archi.ptr64; reflexivity. }
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 792a73f9..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 := opttyp_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 =>
@@ -667,7 +696,7 @@ Definition transl_var (ce: composite_env) (v: ident * type) :=
Definition signature_of_function (f: Clight.function) :=
{| sig_args := map typ_of_type (map snd (Clight.fn_params f));
- sig_res := opttyp_of_type (Clight.fn_return f);
+ sig_res := rettype_of_type (Clight.fn_return f);
sig_cc := Clight.fn_callconv f |}.
Definition transl_function (ce: composite_env) (f: Clight.function) : res function :=
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/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index c34a5e13..e3e2c1e9 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -106,7 +106,7 @@ Definition Epreincr (id: incr_or_decr) (l: expr) (ty: type) :=
Definition Eselection (r1 r2 r3: expr) (ty: type) :=
let t := typ_of_type ty in
- let sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default in
+ let sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default in
Ebuiltin (EF_builtin "__builtin_sel"%string sg)
(Tcons type_bool (Tcons ty (Tcons ty Tnil)))
(Econs r1 (Econs r2 (Econs r3 Enil)))
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index bfc5daa9..664a60c5 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -732,8 +732,21 @@ Definition typ_of_type (t: type) : AST.typ :=
| Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tptr
end.
-Definition opttyp_of_type (t: type) : option AST.typ :=
- if type_eq t Tvoid then None else Some (typ_of_type t).
+Definition rettype_of_type (t: type) : AST.rettype :=
+ match t with
+ | Tvoid => AST.Tvoid
+ | Tint I32 _ _ => AST.Tint
+ | Tint I8 Signed _ => AST.Tint8signed
+ | Tint I8 Unsigned _ => AST.Tint8unsigned
+ | Tint I16 Signed _ => AST.Tint16signed
+ | Tint I16 Unsigned _ => AST.Tint16unsigned
+ | Tint IBool _ _ => AST.Tint8unsigned
+ | Tlong _ _ => AST.Tlong
+ | Tfloat F32 _ => AST.Tsingle
+ | Tfloat F64 _ => AST.Tfloat
+ | Tpointer _ _ => AST.Tptr
+ | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tvoid
+ end.
Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ :=
match tl with
@@ -742,7 +755,7 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ :=
end.
Definition signature_of_type (args: typelist) (res: type) (cc: calling_convention): signature :=
- mksignature (typlist_of_typelist args) (opttyp_of_type res) cc.
+ mksignature (typlist_of_typelist args) (rettype_of_type res) cc.
(** * Construction of the composite environment *)
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index b92a9bac..00fcf8ab 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -397,10 +397,10 @@ Inductive wt_rvalue : expr -> Prop :=
wt_arguments rargs tyargs ->
(* This typing rule is specialized to the builtin invocations generated
by C2C, which are either __builtin_sel or builtins returning void. *)
- (ty = Tvoid /\ sig_res (ef_sig ef) = None)
+ (ty = Tvoid /\ sig_res (ef_sig ef) = AST.Tvoid)
\/ (tyargs = Tcons type_bool (Tcons ty (Tcons ty Tnil))
/\ let t := typ_of_type ty in
- let sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default in
+ let sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default in
ef = EF_builtin "__builtin_sel"%string sg) ->
wt_rvalue (Ebuiltin ef tyargs rargs ty)
| wt_Eparen: forall r tycast ty,
@@ -521,11 +521,20 @@ Fixpoint bind_globdef (e: typenv) (l: list (ident * globdef fundef type)) : type
| (id, Gvar v) :: l => bind_globdef (PTree.set id v.(gvar_info) e) l
end.
+Inductive wt_fundef (ce: composite_env) (e: typenv) : fundef -> Prop :=
+ | wt_fundef_internal: forall f,
+ wt_function ce e f ->
+ wt_fundef ce e (Internal f)
+ | wt_fundef_external: forall ef targs tres cc,
+ (ef_sig ef).(sig_res) = rettype_of_type tres ->
+ wt_fundef ce e (External ef targs tres cc).
+
Inductive wt_program : program -> Prop :=
| wt_program_intro: forall p,
let e := bind_globdef (PTree.empty _) p.(prog_defs) in
- (forall id f, In (id, Gfun (Internal f)) p.(prog_defs) ->
- wt_function p.(prog_comp_env) e f) ->
+ (forall id fd,
+ In (id, Gfun fd) p.(prog_defs) ->
+ wt_fundef p.(prog_comp_env) e fd) ->
wt_program p.
Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty.
@@ -745,7 +754,7 @@ Definition ebuiltin (ef: external_function) (tyargs: typelist) (args: exprlist)
do x1 <- check_rvals args;
do x2 <- check_arguments args tyargs;
if type_eq tyres Tvoid
- && opt_typ_eq (sig_res (ef_sig ef)) None
+ && AST.rettype_eq (sig_res (ef_sig ef)) AST.Tvoid
then OK (Ebuiltin ef tyargs args tyres)
else Error (msg "builtin: wrong type decoration").
@@ -915,7 +924,8 @@ Definition retype_function (ce: composite_env) (e: typenv) (f: function) : res f
Definition retype_fundef (ce: composite_env) (e: typenv) (fd: fundef) : res fundef :=
match fd with
| Internal f => do f' <- retype_function ce e f; OK (Internal f')
- | External id args res cc => OK fd
+ | External ef args res cc =>
+ assertion (rettype_eq (ef_sig ef).(sig_res) (rettype_of_type res)); OK fd
end.
Definition typecheck_program (p: program) : res program :=
@@ -987,6 +997,7 @@ Proof.
classify_cast (Tint i s a) t2 <> cast_case_default).
{
unfold classify_cast. destruct t2; try congruence. destruct f; congruence.
+ destruct Archi.ptr64; congruence.
}
destruct i; auto.
Qed.
@@ -1240,7 +1251,7 @@ Lemma ebuiltin_sound:
Proof.
intros. monadInv H.
destruct (type_eq tyres Tvoid); simpl in EQ2; try discriminate.
- destruct (opt_typ_eq (sig_res (ef_sig ef)) None); inv EQ2.
+ destruct (rettype_eq (sig_res (ef_sig ef)) AST.Tvoid); inv EQ2.
econstructor; eauto. eapply check_arguments_sound; eauto.
Qed.
@@ -1372,6 +1383,14 @@ Proof.
intros. monadInv H. constructor; simpl. eapply retype_stmt_sound; eauto.
Qed.
+Lemma retype_fundef_sound:
+ forall ce e fd fd', retype_fundef ce e fd = OK fd' -> wt_fundef ce e fd'.
+Proof.
+ intros. destruct fd; monadInv H.
+- constructor; eapply retype_function_sound; eauto.
+- constructor; auto.
+Qed.
+
Theorem typecheck_program_sound:
forall p p', typecheck_program p = OK p' -> wt_program p'.
Proof.
@@ -1394,11 +1413,11 @@ Proof.
inv H1. simpl. auto.
}
rewrite ENVS.
- intros id f. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp).
+ intros id fd. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp).
induction 1; simpl; intros.
contradiction.
destruct H0; auto. subst b1; inv H. simpl in H1. inv H1.
- destruct f1; monadInv H4. eapply retype_function_sound; eauto.
+ eapply retype_fundef_sound; eauto.
Qed.
(** * Subject reduction *)
@@ -1710,6 +1729,26 @@ Proof.
inv H; auto.
Qed.
+Lemma has_rettype_wt_val:
+ forall v ty,
+ Val.has_rettype v (rettype_of_type ty) -> wt_val v ty.
+Proof.
+ unfold rettype_of_type, Val.has_rettype, Val.has_type; destruct ty; intros.
+- destruct v; contradiction || constructor.
+- destruct i.
+ + destruct s; destruct v; try contradiction; constructor; red; auto.
+ + destruct s; destruct v; try contradiction; constructor; red; auto.
+ + destruct v; try contradiction; constructor; auto.
+ + destruct v; try contradiction; constructor; red; auto.
+- destruct v; try contradiction; constructor; auto.
+- destruct f; destruct v; try contradiction; constructor.
+- unfold Tptr in *; destruct v; destruct Archi.ptr64 eqn:P64; try contradiction; constructor; auto.
+- destruct v; contradiction || constructor.
+- destruct v; contradiction || constructor.
+- destruct v; contradiction || constructor.
+- destruct v; contradiction || constructor.
+Qed.
+
Lemma wt_rred:
forall ge tenv a m t a' m',
rred ge a m t a' m' -> wt_rvalue ge tenv a -> wt_rvalue ge tenv a'.
@@ -1749,7 +1788,7 @@ Proof.
- (* builtin *) subst. destruct H7 as [(A & B) | (A & B)].
+ subst ty. auto with ty.
+ simpl in B. set (T := typ_of_type ty) in *.
- set (sg := mksignature (AST.Tint :: T :: T :: nil) (Some T) cc_default) in *.
+ set (sg := mksignature (AST.Tint :: T :: T :: nil) T cc_default) in *.
assert (LK: lookup_builtin_function "__builtin_sel"%string sg = Some (BI_standard (BI_select T))).
{ unfold sg, T; destruct ty as [ | ? ? ? | ? | [] ? | ? ? | ? ? ? | ? ? ? | ? ? | ? ? ];
simpl; unfold Tptr; destruct Archi.ptr64; reflexivity. }
@@ -1895,12 +1934,6 @@ Hypothesis WTPROG: wt_program prog.
Let ge := globalenv prog.
Let gtenv := bind_globdef (PTree.empty _) prog.(prog_defs).
-Hypothesis WT_EXTERNAL:
- forall id ef args res cc vargs m t vres m',
- In (id, Gfun (External ef args res cc)) prog.(prog_defs) ->
- external_call ef ge vargs m t vres m' ->
- wt_val vres res.
-
Inductive wt_expr_cont: typenv -> function -> cont -> Prop :=
| wt_Kdo: forall te f k,
wt_stmt_cont te f k ->
@@ -1999,12 +2032,6 @@ Proof.
induction 1; simpl; auto; econstructor; eauto.
Qed.
-Definition wt_fundef (fd: fundef) :=
- match fd with
- | Internal f => wt_function ge gtenv f
- | External ef targs tres cc => True
- end.
-
Definition fundef_return (fd: fundef) : type :=
match fd with
| Internal f => f.(fn_return)
@@ -2012,10 +2039,10 @@ Definition fundef_return (fd: fundef) : type :=
end.
Lemma wt_find_funct:
- forall v fd, Genv.find_funct ge v = Some fd -> wt_fundef fd.
+ forall v fd, Genv.find_funct ge v = Some fd -> wt_fundef ge gtenv fd.
Proof.
intros. apply Genv.find_funct_prop with (p := prog) (v := v); auto.
- intros. inv WTPROG. destruct f; simpl; auto. apply H1 with id; auto.
+ intros. inv WTPROG. apply H1 with id; auto.
Qed.
Inductive wt_state: state -> Prop :=
@@ -2031,7 +2058,7 @@ Inductive wt_state: state -> Prop :=
wt_state (ExprState f r k e m)
| wt_call_state: forall b fd vargs k m
(WTK: wt_call_cont k (fundef_return fd))
- (WTFD: wt_fundef fd)
+ (WTFD: wt_fundef ge gtenv fd)
(FIND: Genv.find_funct ge b = Some fd),
wt_state (Callstate fd vargs k m)
| wt_return_state: forall v k m ty
@@ -2088,7 +2115,6 @@ Qed.
End WT_FIND_LABEL.
-
Lemma preservation_estep:
forall S t S', estep ge S t S' -> wt_state S -> wt_state S'.
Proof.
@@ -2163,9 +2189,10 @@ Proof.
- inv WTS; eauto with ty.
- exploit wt_find_label. eexact WTB. eauto. eapply call_cont_wt'; eauto.
intros [A B]. eauto with ty.
-- simpl in WTFD; inv WTFD. econstructor; eauto. apply wt_call_cont_stmt_cont; auto.
-- exploit (Genv.find_funct_inversion prog); eauto. intros (id & A).
- econstructor; eauto.
+- inv WTFD. inv H3. econstructor; eauto. apply wt_call_cont_stmt_cont; auto.
+- inv WTFD. econstructor; eauto.
+ apply has_rettype_wt_val. simpl; rewrite <- H1.
+ eapply external_call_well_typed_gen; eauto.
- inv WTK. eauto with ty.
Qed.
@@ -2180,7 +2207,7 @@ Theorem wt_initial_state:
Proof.
intros. inv H. econstructor. constructor.
apply Genv.find_funct_ptr_prop with (p := prog) (b := b); auto.
- intros. inv WTPROG. destruct f0; simpl; auto. apply H4 with id; auto.
+ intros. inv WTPROG. apply H4 with id; auto.
instantiate (1 := (Vptr b Ptrofs.zero)). rewrite Genv.find_funct_find_funct_ptr. auto.
Qed.
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 1c9729c5..03dc5837 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -19,7 +19,7 @@ open Format
open Camlcoq
open Values
open AST
-open Ctypes
+open! Ctypes
open Cop
open Csyntax
@@ -85,7 +85,7 @@ let name_optid id =
let rec name_cdecl id ty =
match ty with
- | Tvoid ->
+ | Ctypes.Tvoid ->
"void" ^ name_optid id
| Ctypes.Tint(sz, sg, a) ->
name_inttype sz sg ^ attributes a ^ name_optid id
diff --git a/common/AST.v b/common/AST.v
index 86cab287..eb34d675 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -45,9 +45,6 @@ Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}.
Proof. decide equality. Defined.
Global Opaque typ_eq.
-Definition opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}
- := option_eq typ_eq.
-
Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2}
:= list_eq_dec typ_eq.
@@ -91,10 +88,34 @@ Fixpoint subtype_list (tyl1 tyl2: list typ) : bool :=
| _, _ => false
end.
+(** To describe the values returned by functions, we use the more precise
+ types below. *)
+
+Inductive rettype : Type :=
+ | Tret (t: typ) (**r like type [t] *)
+ | Tint8signed (**r 8-bit signed integer *)
+ | Tint8unsigned (**r 8-bit unsigned integer *)
+ | Tint16signed (**r 16-bit signed integer *)
+ | Tint16unsigned (**r 16-bit unsigned integer *)
+ | Tvoid. (**r no value returned *)
+
+Coercion Tret: typ >-> rettype.
+
+Lemma rettype_eq: forall (t1 t2: rettype), {t1=t2} + {t1<>t2}.
+Proof. generalize typ_eq; decide equality. Defined.
+Global Opaque rettype_eq.
+
+Fixpoint proj_rettype (r: rettype) : typ :=
+ match r with
+ | Tret t => t
+ | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => Tint
+ | Tvoid => Tint
+ end.
+
(** Additionally, function definitions and function calls are annotated
by function signatures indicating:
- the number and types of arguments;
-- the type of the returned value, if any;
+- the type of the returned value;
- additional information on which calling convention to use.
These signatures are used in particular to determine appropriate
@@ -117,24 +138,20 @@ Global Opaque calling_convention_eq.
Record signature : Type := mksignature {
sig_args: list typ;
- sig_res: option typ;
+ sig_res: rettype;
sig_cc: calling_convention
}.
-Definition proj_sig_res (s: signature) : typ :=
- match s.(sig_res) with
- | None => Tint
- | Some t => t
- end.
+Definition proj_sig_res (s: signature) : typ := proj_rettype s.(sig_res).
Definition signature_eq: forall (s1 s2: signature), {s1=s2} + {s1<>s2}.
Proof.
- generalize opt_typ_eq, list_typ_eq, calling_convention_eq; decide equality.
+ generalize rettype_eq, list_typ_eq, calling_convention_eq; decide equality.
Defined.
Global Opaque signature_eq.
Definition signature_main :=
- {| sig_args := nil; sig_res := Some Tint; sig_cc := cc_default |}.
+ {| sig_args := nil; sig_res := Tint; sig_cc := cc_default |}.
(** Memory accesses (load and store instructions) are annotated by
a ``memory chunk'' indicating the type, size and signedness of the
@@ -177,6 +194,28 @@ Definition type_of_chunk (c: memory_chunk) : typ :=
Lemma type_of_Mptr: type_of_chunk Mptr = Tptr.
Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed.
+(** Same, as a return type. *)
+
+Definition rettype_of_chunk (c: memory_chunk) : rettype :=
+ match c with
+ | Mint8signed => Tint8signed
+ | Mint8unsigned => Tint8unsigned
+ | Mint16signed => Tint16signed
+ | Mint16unsigned => Tint16unsigned
+ | Mint32 => Tint
+ | Mint64 => Tlong
+ | Mfloat32 => Tsingle
+ | Mfloat64 => Tfloat
+ | Many32 => Tany32
+ | Many64 => Tany64
+ end.
+
+Lemma proj_rettype_of_chunk:
+ forall chunk, proj_rettype (rettype_of_chunk chunk) = type_of_chunk chunk.
+Proof.
+ destruct chunk; auto.
+Qed.
+
(** The chunk that is appropriate to store and reload a value of
the given type, without losing information. *)
@@ -487,15 +526,15 @@ Definition ef_sig (ef: external_function): signature :=
| EF_external name sg => sg
| EF_builtin name sg => sg
| EF_runtime name sg => sg
- | EF_vload chunk => mksignature (Tptr :: nil) (Some (type_of_chunk chunk)) cc_default
- | EF_vstore chunk => mksignature (Tptr :: type_of_chunk chunk :: nil) None cc_default
- | EF_malloc => mksignature (Tptr :: nil) (Some Tptr) cc_default
- | EF_free => mksignature (Tptr :: nil) None cc_default
- | EF_memcpy sz al => mksignature (Tptr :: Tptr :: nil) None cc_default
- | EF_annot kind text targs => mksignature targs None cc_default
- | EF_annot_val kind text targ => mksignature (targ :: nil) (Some targ) cc_default
+ | EF_vload chunk => mksignature (Tptr :: nil) (rettype_of_chunk chunk) cc_default
+ | EF_vstore chunk => mksignature (Tptr :: type_of_chunk chunk :: nil) Tvoid cc_default
+ | EF_malloc => mksignature (Tptr :: nil) Tptr cc_default
+ | EF_free => mksignature (Tptr :: nil) Tvoid cc_default
+ | EF_memcpy sz al => mksignature (Tptr :: Tptr :: nil) Tvoid cc_default
+ | EF_annot kind text targs => mksignature targs Tvoid cc_default
+ | EF_annot_val kind text targ => mksignature (targ :: nil) targ cc_default
| EF_inline_asm text sg clob => sg
- | EF_debug kind text targs => mksignature targs None cc_default
+ | EF_debug kind text targs => mksignature targs Tvoid cc_default
end.
(** Whether an external function should be inlined by the compiler. *)
diff --git a/common/Builtins.v b/common/Builtins.v
index c9097e86..476b541e 100644
--- a/common/Builtins.v
+++ b/common/Builtins.v
@@ -29,7 +29,7 @@ Definition builtin_function_sig (b: builtin_function) : signature :=
| BI_platform b => platform_builtin_sig b
end.
-Definition builtin_function_sem (b: builtin_function) : builtin_sem (proj_sig_res (builtin_function_sig b)) :=
+Definition builtin_function_sem (b: builtin_function) : builtin_sem (sig_res (builtin_function_sig b)) :=
match b with
| BI_standard b => standard_builtin_sem b
| BI_platform b => platform_builtin_sem b
diff --git a/common/Builtins0.v b/common/Builtins0.v
index b78006dd..8da98314 100644
--- a/common/Builtins0.v
+++ b/common/Builtins0.v
@@ -26,8 +26,8 @@ Require Import AST Integers Floats Values Memdata.
appropriate for the target.
*)
-Definition val_opt_has_type (ov: option val) (t: typ) : Prop :=
- match ov with Some v => Val.has_type v t | None => True end.
+Definition val_opt_has_rettype (ov: option val) (t: rettype) : Prop :=
+ match ov with Some v => Val.has_rettype v t | None => True end.
Definition val_opt_inject (j: meminj) (ov ov': option val) : Prop :=
match ov, ov' with
@@ -42,10 +42,10 @@ Definition val_opt_inject (j: meminj) (ov ov': option val) : Prop :=
and be compatible with value injections.
*)
-Record builtin_sem (tret: typ) : Type := mkbuiltin {
+Record builtin_sem (tret: rettype) : Type := mkbuiltin {
bs_sem :> list val -> option val;
bs_well_typed: forall vl,
- val_opt_has_type (bs_sem vl) tret;
+ val_opt_has_rettype (bs_sem vl) tret;
bs_inject: forall j vl vl',
Val.inject_list j vl vl' -> val_opt_inject j (bs_sem vl) (bs_sem vl')
}.
@@ -60,8 +60,8 @@ Record builtin_sem (tret: typ) : Type := mkbuiltin {
Local Unset Program Cases.
Program Definition mkbuiltin_v1t
- (tret: typ) (f: val -> val)
- (WT: forall v1, Val.has_type (f v1) tret)
+ (tret: rettype) (f: val -> val)
+ (WT: forall v1, Val.has_rettype (f v1) tret)
(INJ: forall j v1 v1', Val.inject j v1 v1' -> Val.inject j (f v1) (f v1')) :=
mkbuiltin tret (fun vl => match vl with v1 :: nil => Some (f v1) | _ => None end) _ _.
Next Obligation.
@@ -72,8 +72,8 @@ Next Obligation.
Qed.
Program Definition mkbuiltin_v2t
- (tret: typ) (f: val -> val -> val)
- (WT: forall v1 v2, Val.has_type (f v1 v2) tret)
+ (tret: rettype) (f: val -> val -> val)
+ (WT: forall v1 v2, Val.has_rettype (f v1 v2) tret)
(INJ: forall j v1 v1' v2 v2',
Val.inject j v1 v1' -> Val.inject j v2 v2' ->
Val.inject j (f v1 v2) (f v1' v2')) :=
@@ -86,8 +86,8 @@ Next Obligation.
Qed.
Program Definition mkbuiltin_v3t
- (tret: typ) (f: val -> val -> val -> val)
- (WT: forall v1 v2 v3, Val.has_type (f v1 v2 v3) tret)
+ (tret: rettype) (f: val -> val -> val -> val)
+ (WT: forall v1 v2 v3, Val.has_rettype (f v1 v2 v3) tret)
(INJ: forall j v1 v1' v2 v2' v3 v3',
Val.inject j v1 v1' -> Val.inject j v2 v2' -> Val.inject j v3 v3' ->
Val.inject j (f v1 v2 v3) (f v1' v2' v3')) :=
@@ -100,8 +100,8 @@ Next Obligation.
Qed.
Program Definition mkbuiltin_v1p
- (tret: typ) (f: val -> option val)
- (WT: forall v1, val_opt_has_type (f v1) tret)
+ (tret: rettype) (f: val -> option val)
+ (WT: forall v1, val_opt_has_rettype (f v1) tret)
(INJ: forall j v1 v1',
Val.inject j v1 v1' -> val_opt_inject j (f v1) (f v1')) :=
mkbuiltin tret (fun vl => match vl with v1 :: nil => f v1 | _ => None end) _ _.
@@ -113,8 +113,8 @@ Next Obligation.
Qed.
Program Definition mkbuiltin_v2p
- (tret: typ) (f: val -> val -> option val)
- (WT: forall v1 v2, val_opt_has_type (f v1 v2) tret)
+ (tret: rettype) (f: val -> val -> option val)
+ (WT: forall v1 v2, val_opt_has_rettype (f v1 v2) tret)
(INJ: forall j v1 v1' v2 v2',
Val.inject j v1 v1' -> Val.inject j v2 v2' ->
val_opt_inject j (f v1 v2) (f v1' v2')) :=
@@ -171,7 +171,7 @@ Proof.
destruct t; intros; constructor.
Qed.
-Lemma inj_num_opt_wt: forall t x, val_opt_has_type (option_map (inj_num t) x) t.
+Lemma inj_num_opt_wt: forall t x, val_opt_has_rettype (option_map (inj_num t) x) t.
Proof.
intros. destruct x; simpl. apply inj_num_wt. auto.
Qed.
@@ -200,13 +200,13 @@ Proof.
Qed.
Lemma proj_num_opt_wt:
- forall tres t k0 k1 v,
+ forall (tres: typ) t k0 k1 v,
k0 = None \/ k0 = Some Vundef ->
- (forall x, val_opt_has_type (k1 x) tres) ->
- val_opt_has_type (proj_num t k0 v k1) tres.
+ (forall x, val_opt_has_rettype (k1 x) tres) ->
+ val_opt_has_rettype (proj_num t k0 v k1) tres.
Proof.
intros.
- assert (val_opt_has_type k0 tres). { destruct H; subst k0; exact I. }
+ assert (val_opt_has_rettype k0 tres). { destruct H; subst k0; exact I. }
destruct t; simpl; destruct v; auto.
Qed.
@@ -393,33 +393,33 @@ Definition standard_builtin_table : list (string * standard_builtin) :=
Definition standard_builtin_sig (b: standard_builtin) : signature :=
match b with
| BI_select t =>
- mksignature (Tint :: t :: t :: nil) (Some t) cc_default
+ mksignature (Tint :: t :: t :: nil) t cc_default
| BI_fabs | BI_fsqrt =>
- mksignature (Tfloat :: nil) (Some Tfloat) cc_default
+ mksignature (Tfloat :: nil) Tfloat cc_default
| BI_negl =>
- mksignature (Tlong :: nil) (Some Tlong) cc_default
+ mksignature (Tlong :: nil) Tlong cc_default
| BI_addl | BI_subl | BI_i64_umulh| BI_i64_smulh
| BI_i64_sdiv | BI_i64_udiv | BI_i64_smod | BI_i64_umod =>
- mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default
+ mksignature (Tlong :: Tlong :: nil) Tlong cc_default
| BI_mull =>
- mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default
+ mksignature (Tint :: Tint :: nil) Tlong cc_default
| BI_i32_bswap =>
- mksignature (Tint :: nil) (Some Tint) cc_default
+ mksignature (Tint :: nil) Tint cc_default
| BI_i64_bswap =>
- mksignature (Tlong :: nil) (Some Tlong) cc_default
+ mksignature (Tlong :: nil) Tlong cc_default
| BI_i16_bswap =>
- mksignature (Tint :: nil) (Some Tint) cc_default
+ mksignature (Tint :: nil) Tint cc_default
| BI_i64_shl | BI_i64_shr | BI_i64_sar =>
- mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default
+ mksignature (Tlong :: Tint :: nil) Tlong cc_default
| BI_i64_dtos | BI_i64_dtou =>
- mksignature (Tfloat :: nil) (Some Tlong) cc_default
+ mksignature (Tfloat :: nil) Tlong cc_default
| BI_i64_stod | BI_i64_utod =>
- mksignature (Tlong :: nil) (Some Tfloat) cc_default
+ mksignature (Tlong :: nil) Tfloat cc_default
| BI_i64_stof | BI_i64_utof =>
- mksignature (Tlong :: nil) (Some Tsingle) cc_default
+ mksignature (Tlong :: nil) Tsingle cc_default
end.
-Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (proj_sig_res (standard_builtin_sig b)) :=
+Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig_res (standard_builtin_sig b)) :=
match b with
| BI_select t =>
mkbuiltin t
diff --git a/common/Events.v b/common/Events.v
index 3fb84f49..28bb992a 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -623,7 +623,7 @@ Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop :=
ec_well_typed:
forall ge vargs m1 t vres m2,
sem ge vargs m1 t vres m2 ->
- Val.has_type vres (proj_sig_res sg);
+ Val.has_rettype vres sg.(sig_res);
(** The semantics is invariant under change of global environment that preserves symbols. *)
ec_symbols_preserved:
@@ -649,9 +649,12 @@ Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop :=
(** External call cannot modify memory unless they have [Max, Writable]
permissions. *)
ec_readonly:
- forall ge vargs m1 t vres m2,
+ forall ge vargs m1 t vres m2 b ofs n bytes,
sem ge vargs m1 t vres m2 ->
- Mem.unchanged_on (loc_not_writable m1) m1 m2;
+ Mem.valid_block m1 b ->
+ Mem.loadbytes m2 b ofs n = Some bytes ->
+ (forall i, ofs <= i < ofs + n -> ~Mem.perm m1 b i Max Writable) ->
+ Mem.loadbytes m1 b ofs n = Some bytes;
(** External calls must commute with memory extensions, in the
following sense. *)
@@ -771,12 +774,12 @@ Qed.
Lemma volatile_load_ok:
forall chunk,
extcall_properties (volatile_load_sem chunk)
- (mksignature (Tptr :: nil) (Some (type_of_chunk chunk)) cc_default).
+ (mksignature (Tptr :: nil) (rettype_of_chunk chunk) cc_default).
Proof.
intros; constructor; intros.
(* well typed *)
-- unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type.
- eapply Mem.load_type; eauto.
+- inv H. inv H0. apply Val.load_result_rettype.
+ eapply Mem.load_rettype; eauto.
(* symbols *)
- inv H0. constructor. eapply volatile_load_preserved; eauto.
(* valid blocks *)
@@ -784,7 +787,7 @@ Proof.
(* max perms *)
- inv H; auto.
(* readonly *)
-- inv H. apply Mem.unchanged_on_refl.
+- inv H; auto.
(* mem extends *)
- inv H. inv H1. inv H6. inv H4.
exploit volatile_load_extends; eauto. intros [v' [A B]].
@@ -833,14 +836,27 @@ Proof.
rewrite C; auto.
Qed.
+Lemma unchanged_on_readonly:
+ forall m1 m2 b ofs n bytes,
+ Mem.unchanged_on (loc_not_writable m1) m1 m2 ->
+ Mem.valid_block m1 b ->
+ Mem.loadbytes m2 b ofs n = Some bytes ->
+ (forall i, ofs <= i < ofs + n -> ~Mem.perm m1 b i Max Writable) ->
+ Mem.loadbytes m1 b ofs n = Some bytes.
+Proof.
+ intros.
+ rewrite <- H1. symmetry.
+ apply Mem.loadbytes_unchanged_on_1 with (P := loc_not_writable m1); auto.
+Qed.
+
Lemma volatile_store_readonly:
forall ge chunk1 m1 b1 ofs1 v t m2,
volatile_store ge chunk1 m1 b1 ofs1 v t m2 ->
Mem.unchanged_on (loc_not_writable m1) m1 m2.
Proof.
intros. inv H.
- apply Mem.unchanged_on_refl.
- eapply Mem.store_unchanged_on; eauto.
+- apply Mem.unchanged_on_refl.
+- eapply Mem.store_unchanged_on; eauto.
exploit Mem.store_valid_access_3; eauto. intros [P Q].
intros. unfold loc_not_writable. red; intros. elim H2.
apply Mem.perm_cur_max. apply P. auto.
@@ -922,7 +938,7 @@ Qed.
Lemma volatile_store_ok:
forall chunk,
extcall_properties (volatile_store_sem chunk)
- (mksignature (Tptr :: type_of_chunk chunk :: nil) None cc_default).
+ (mksignature (Tptr :: type_of_chunk chunk :: nil) Tvoid cc_default).
Proof.
intros; constructor; intros.
(* well typed *)
@@ -934,7 +950,7 @@ Proof.
(* perms *)
- inv H. inv H2. auto. eauto with mem.
(* readonly *)
-- inv H. eapply volatile_store_readonly; eauto.
+- inv H. eapply unchanged_on_readonly; eauto. eapply volatile_store_readonly; eauto.
(* mem extends*)
- inv H. inv H1. inv H6. inv H7. inv H4.
exploit volatile_store_extends; eauto. intros [m2' [A [B C]]].
@@ -967,7 +983,7 @@ Inductive extcall_malloc_sem (ge: Senv.t):
Lemma extcall_malloc_ok:
extcall_properties extcall_malloc_sem
- (mksignature (Tptr :: nil) (Some Tptr) cc_default).
+ (mksignature (Tptr :: nil) Tptr cc_default).
Proof.
assert (UNCHANGED:
forall (P: block -> Z -> Prop) m lo hi v m' b m'',
@@ -984,7 +1000,7 @@ Proof.
}
constructor; intros.
(* well typed *)
-- inv H. unfold proj_sig_res, Tptr; simpl. destruct Archi.ptr64; auto.
+- inv H. simpl. unfold Tptr; destruct Archi.ptr64; auto.
(* symbols preserved *)
- inv H0; econstructor; eauto.
(* valid block *)
@@ -994,7 +1010,7 @@ Proof.
rewrite dec_eq_false. auto.
apply Mem.valid_not_valid_diff with m1; eauto with mem.
(* readonly *)
-- inv H. eapply UNCHANGED; eauto.
+- inv H. eapply unchanged_on_readonly; eauto.
(* mem extends *)
- inv H. inv H1. inv H7.
assert (SZ: v2 = Vptrofs sz).
@@ -1045,38 +1061,43 @@ Qed.
Inductive extcall_free_sem (ge: Senv.t):
list val -> mem -> trace -> val -> mem -> Prop :=
- | extcall_free_sem_intro: forall b lo sz m m',
+ | extcall_free_sem_ptr: forall b lo sz m m',
Mem.load Mptr m b (Ptrofs.unsigned lo - size_chunk Mptr) = Some (Vptrofs sz) ->
Ptrofs.unsigned sz > 0 ->
Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz) = Some m' ->
- extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m'.
+ extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m'
+ | extcall_free_sem_null: forall m,
+ extcall_free_sem ge (Vnullptr :: nil) m E0 Vundef m.
Lemma extcall_free_ok:
extcall_properties extcall_free_sem
- (mksignature (Tptr :: nil) None cc_default).
+ (mksignature (Tptr :: nil) Tvoid cc_default).
Proof.
constructor; intros.
(* well typed *)
-- inv H. unfold proj_sig_res. simpl. auto.
+- inv H; simpl; auto.
(* symbols preserved *)
- inv H0; econstructor; eauto.
(* valid block *)
-- inv H. eauto with mem.
+- inv H; eauto with mem.
(* perms *)
-- inv H. eapply Mem.perm_free_3; eauto.
+- inv H; eauto using Mem.perm_free_3.
(* readonly *)
-- inv H. eapply Mem.free_unchanged_on; eauto.
- intros. red; intros. elim H3.
+- eapply unchanged_on_readonly; eauto. inv H.
++ eapply Mem.free_unchanged_on; eauto.
+ intros. red; intros. elim H6.
apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
eapply Mem.free_range_perm; eauto.
++ apply Mem.unchanged_on_refl.
(* mem extends *)
-- inv H. inv H1. inv H8. inv H6.
+- inv H.
++ inv H1. inv H8. inv H6.
exploit Mem.load_extends; eauto. intros [v' [A B]].
assert (v' = Vptrofs sz).
{ unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. }
subst v'.
exploit Mem.free_parallel_extends; eauto. intros [m2' [C D]].
- exists Vundef; exists m2'; intuition.
+ exists Vundef; exists m2'; intuition auto.
econstructor; eauto.
eapply Mem.free_unchanged_on; eauto.
unfold loc_out_of_bounds; intros.
@@ -1084,8 +1105,14 @@ Proof.
{ apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
eapply Mem.free_range_perm. eexact H4. eauto. }
tauto.
++ inv H1. inv H5. replace v2 with Vnullptr.
+ exists Vundef; exists m1'; intuition auto.
+ constructor.
+ apply Mem.unchanged_on_refl.
+ unfold Vnullptr in *; destruct Archi.ptr64; inv H3; auto.
(* mem inject *)
-- inv H0. inv H2. inv H7. inv H9.
+- inv H0.
++ inv H2. inv H7. inv H9.
exploit Mem.load_inject; eauto. intros [v' [A B]].
assert (v' = Vptrofs sz).
{ unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. }
@@ -1099,7 +1126,7 @@ Proof.
intro EQ.
exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D).
exists f, Vundef, m2'; split.
- apply extcall_free_sem_intro with (sz := sz) (m' := m2').
+ apply extcall_free_sem_ptr with (sz := sz) (m' := m2').
rewrite EQ. rewrite <- A. f_equal. omega.
auto. auto.
rewrite ! EQ. rewrite <- C. f_equal; omega.
@@ -1112,14 +1139,19 @@ Proof.
apply P. omega.
split. auto.
red; intros. congruence.
++ inv H2. inv H6. replace v' with Vnullptr.
+ exists f, Vundef, m1'; intuition auto using Mem.unchanged_on_refl.
+ constructor.
+ red; intros; congruence.
+ unfold Vnullptr in *; destruct Archi.ptr64; inv H4; auto.
(* trace length *)
- inv H; simpl; omega.
(* receptive *)
-- assert (t1 = t2). inv H; inv H0; auto. subst t2.
+- assert (t1 = t2) by (inv H; inv H0; auto). subst t2.
exists vres1; exists m1; auto.
(* determ *)
-- inv H; inv H0.
- assert (EQ1: Vptrofs sz0 = Vptrofs sz) by congruence.
+- inv H; inv H0; try (unfold Vnullptr in *; destruct Archi.ptr64; discriminate).
++ assert (EQ1: Vptrofs sz0 = Vptrofs sz) by congruence.
assert (EQ2: sz0 = sz).
{ unfold Vptrofs in EQ1; destruct Archi.ptr64 eqn:SF.
rewrite <- (Ptrofs.of_int64_to_int64 SF sz0), <- (Ptrofs.of_int64_to_int64 SF sz). congruence.
@@ -1127,6 +1159,7 @@ Proof.
}
subst sz0.
split. constructor. intuition congruence.
++ split. constructor. intuition auto.
Qed.
(** ** Semantics of [memcpy] operations. *)
@@ -1147,11 +1180,11 @@ Inductive extcall_memcpy_sem (sz al: Z) (ge: Senv.t):
Lemma extcall_memcpy_ok:
forall sz al,
extcall_properties (extcall_memcpy_sem sz al)
- (mksignature (Tptr :: Tptr :: nil) None cc_default).
+ (mksignature (Tptr :: Tptr :: nil) Tvoid cc_default).
Proof.
intros. constructor.
- (* return type *)
- intros. inv H. constructor.
+ intros. inv H. exact I.
- (* change of globalenv *)
intros. inv H0. econstructor; eauto.
- (* valid blocks *)
@@ -1159,8 +1192,9 @@ Proof.
- (* perms *)
intros. inv H. eapply Mem.perm_storebytes_2; eauto.
- (* readonly *)
- intros. inv H. eapply Mem.storebytes_unchanged_on; eauto.
- intros; red; intros. elim H8.
+ intros. inv H. eapply unchanged_on_readonly; eauto.
+ eapply Mem.storebytes_unchanged_on; eauto.
+ intros; red; intros. elim H11.
apply Mem.perm_cur_max. eapply Mem.storebytes_range_perm; eauto.
- (* extensions *)
intros. inv H.
@@ -1258,7 +1292,7 @@ Inductive extcall_annot_sem (text: string) (targs: list typ) (ge: Senv.t):
Lemma extcall_annot_ok:
forall text targs,
extcall_properties (extcall_annot_sem text targs)
- (mksignature targs None cc_default).
+ (mksignature targs Tvoid cc_default).
Proof.
intros; constructor; intros.
(* well typed *)
@@ -1271,7 +1305,7 @@ Proof.
(* perms *)
- inv H; auto.
(* readonly *)
-- inv H. apply Mem.unchanged_on_refl.
+- inv H; auto.
(* mem extends *)
- inv H.
exists Vundef; exists m1'; intuition.
@@ -1303,11 +1337,11 @@ Inductive extcall_annot_val_sem (text: string) (targ: typ) (ge: Senv.t):
Lemma extcall_annot_val_ok:
forall text targ,
extcall_properties (extcall_annot_val_sem text targ)
- (mksignature (targ :: nil) (Some targ) cc_default).
+ (mksignature (targ :: nil) targ cc_default).
Proof.
intros; constructor; intros.
(* well typed *)
-- inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto.
+- inv H. eapply eventval_match_type; eauto.
(* symbols *)
- destruct H as (A & B & C). inv H0. econstructor; eauto.
eapply eventval_match_preserved; eauto.
@@ -1316,7 +1350,7 @@ Proof.
(* perms *)
- inv H; auto.
(* readonly *)
-- inv H. apply Mem.unchanged_on_refl.
+- inv H; auto.
(* mem extends *)
- inv H. inv H1. inv H6.
exists v2; exists m1'; intuition.
@@ -1347,7 +1381,7 @@ Inductive extcall_debug_sem (ge: Senv.t):
Lemma extcall_debug_ok:
forall targs,
extcall_properties extcall_debug_sem
- (mksignature targs None cc_default).
+ (mksignature targs Tvoid cc_default).
Proof.
intros; constructor; intros.
(* well typed *)
@@ -1359,7 +1393,7 @@ Proof.
(* perms *)
- inv H; auto.
(* readonly *)
-- inv H. apply Mem.unchanged_on_refl.
+- inv H; auto.
(* mem extends *)
- inv H.
exists Vundef; exists m1'; intuition.
@@ -1396,7 +1430,8 @@ Proof.
intros. set (bsem := builtin_function_sem bf). constructor; intros.
(* well typed *)
- inv H.
- specialize (bs_well_typed _ bsem vargs). unfold val_opt_has_type, bsem; rewrite H0.
+ specialize (bs_well_typed _ bsem vargs).
+ unfold val_opt_has_rettype, bsem; rewrite H0.
auto.
(* symbols *)
- inv H0. econstructor; eauto.
@@ -1405,7 +1440,7 @@ Proof.
(* perms *)
- inv H; auto.
(* readonly *)
-- inv H. apply Mem.unchanged_on_refl.
+- inv H; auto.
(* mem extends *)
- inv H. fold bsem in H2. apply val_inject_list_lessdef in H1.
specialize (bs_inject _ bsem _ _ _ H1).
@@ -1516,7 +1551,7 @@ Proof.
apply extcall_debug_ok.
Qed.
-Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef).
+Definition external_call_well_typed_gen ef := ec_well_typed (external_call_spec ef).
Definition external_call_symbols_preserved ef := ec_symbols_preserved (external_call_spec ef).
Definition external_call_valid_block ef := ec_valid_block (external_call_spec ef).
Definition external_call_max_perm ef := ec_max_perm (external_call_spec ef).
@@ -1527,6 +1562,16 @@ Definition external_call_trace_length ef := ec_trace_length (external_call_spec
Definition external_call_receptive ef := ec_receptive (external_call_spec ef).
Definition external_call_determ ef := ec_determ (external_call_spec ef).
+(** Corollary of [external_call_well_typed_gen]. *)
+
+Lemma external_call_well_typed:
+ forall ef ge vargs m1 t vres m2,
+ external_call ef ge vargs m1 t vres m2 ->
+ Val.has_type vres (proj_sig_res (ef_sig ef)).
+Proof.
+ intros. apply Val.has_proj_rettype. eapply external_call_well_typed_gen; eauto.
+Qed.
+
(** Corollary of [external_call_valid_block]. *)
Lemma external_call_nextblock:
diff --git a/common/Memdata.v b/common/Memdata.v
index 7144d72c..a09b90f5 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -44,6 +44,13 @@ Definition size_chunk (chunk: memory_chunk) : Z :=
| Many64 => 8
end.
+Definition largest_size_chunk := 8.
+
+Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8.
+Proof.
+ destruct chunk; simpl; omega.
+Qed.
+
Lemma size_chunk_pos:
forall chunk, size_chunk chunk > 0.
Proof.
@@ -547,18 +554,26 @@ Proof.
destruct v1; auto.
Qed.
-Lemma decode_val_type:
+Lemma decode_val_rettype:
forall chunk cl,
- Val.has_type (decode_val chunk cl) (type_of_chunk chunk).
+ Val.has_rettype (decode_val chunk cl) (rettype_of_chunk chunk).
Proof.
intros. unfold decode_val.
destruct (proj_bytes cl).
- destruct chunk; simpl; auto.
-Local Opaque Val.load_result.
+- destruct chunk; simpl; rewrite ? Int.sign_ext_idem, ? Int.zero_ext_idem by omega; auto.
+- Local Opaque Val.load_result.
destruct chunk; simpl;
(exact I || apply Val.load_result_type || destruct Archi.ptr64; (exact I || apply Val.load_result_type)).
Qed.
+Lemma decode_val_type:
+ forall chunk cl,
+ Val.has_type (decode_val chunk cl) (type_of_chunk chunk).
+Proof.
+ intros. rewrite <- proj_rettype_of_chunk.
+ apply Val.has_proj_rettype. apply decode_val_rettype.
+Qed.
+
Lemma encode_val_int8_signed_unsigned:
forall v, encode_val Mint8signed v = encode_val Mint8unsigned v.
Proof.
@@ -607,11 +622,9 @@ Lemma decode_val_cast:
| _ => True
end.
Proof.
- unfold decode_val; intros; destruct chunk; auto; destruct (proj_bytes l); auto.
- unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. omega.
- unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega.
- unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. omega.
- unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega.
+ intros.
+ assert (A: Val.has_rettype v (rettype_of_chunk chunk)) by apply decode_val_rettype.
+ destruct chunk; auto; simpl in A; destruct v; try contradiction; simpl; congruence.
Qed.
(** Pointers cannot be forged. *)
diff --git a/common/Memory.v b/common/Memory.v
index 50e339e1..cd8a2001 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -728,6 +728,15 @@ Proof.
apply decode_val_type.
Qed.
+Theorem load_rettype:
+ forall m chunk b ofs v,
+ load chunk m b ofs = Some v ->
+ Val.has_rettype v (rettype_of_chunk chunk).
+Proof.
+ intros. exploit load_result; eauto; intros. rewrite H0.
+ apply decode_val_rettype.
+Qed.
+
Theorem load_cast:
forall m chunk b ofs v,
load chunk m b ofs = Some v ->
@@ -1298,6 +1307,23 @@ Proof.
}
Qed.
+Section STOREV.
+Variable chunk: memory_chunk.
+Variable m1: mem.
+Variables addr v: val.
+Variable m2: mem.
+Hypothesis STORE: storev chunk m1 addr v = Some m2.
+
+
+Theorem loadv_storev_same:
+ loadv chunk m2 addr = Some (Val.load_result chunk v).
+Proof.
+ destruct addr; simpl in *; try discriminate.
+ eapply load_store_same.
+ eassumption.
+Qed.
+End STOREV.
+
Lemma load_store_overlap:
forall chunk m1 b ofs v m2 chunk' ofs' v',
store chunk m1 b ofs v = Some m2 ->
diff --git a/common/Memtype.v b/common/Memtype.v
index 53775d8b..ca9c6f1f 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -300,6 +300,11 @@ Axiom load_type:
load chunk m b ofs = Some v ->
Val.has_type v (type_of_chunk chunk).
+Axiom load_rettype:
+ forall m chunk b ofs v,
+ load chunk m b ofs = Some v ->
+ Val.has_rettype v (rettype_of_chunk chunk).
+
(** For a small integer or float type, the value returned by [load]
is invariant under the corresponding cast. *)
Axiom load_cast:
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index baddb722..3f718428 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -27,6 +27,14 @@ let name_of_type = function
| Tany32 -> "any32"
| Tany64 -> "any64"
+let name_of_rettype = function
+ | Tret t -> name_of_type t
+ | Tvoid -> "void"
+ | Tint8signed -> "int8s"
+ | Tint8unsigned -> "int8u"
+ | Tint16signed -> "int16s"
+ | Tint16unsigned -> "int16u"
+
let name_of_chunk = function
| Mint8signed -> "int8s"
| Mint8unsigned -> "int8u"
diff --git a/common/Values.v b/common/Values.v
index 84030123..6401ba52 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -149,6 +149,23 @@ Proof.
auto.
Defined.
+Definition has_rettype (v: val) (r: rettype) : Prop :=
+ match r, v with
+ | Tret t, _ => has_type v t
+ | Tint8signed, Vint n => n = Int.sign_ext 8 n
+ | Tint8unsigned, Vint n => n = Int.zero_ext 8 n
+ | Tint16signed, Vint n => n = Int.sign_ext 16 n
+ | Tint16unsigned, Vint n => n = Int.zero_ext 16 n
+ | _, Vundef => True
+ | _, _ => False
+ end.
+
+Lemma has_proj_rettype: forall v r,
+ has_rettype v r -> has_type v (proj_rettype r).
+Proof.
+ destruct r; simpl; intros; auto; destruct v; try contradiction; exact I.
+Qed.
+
(** Truth values. Non-zero integers are treated as [True].
The integer 0 (also used to represent the null pointer) is [False].
Other values are neither true nor false. *)
@@ -1003,10 +1020,24 @@ Definition load_result (chunk: memory_chunk) (v: val) :=
| _, _ => Vundef
end.
+Lemma load_result_rettype:
+ forall chunk v, has_rettype (load_result chunk v) (rettype_of_chunk chunk).
+Proof.
+ intros. unfold has_rettype; destruct chunk; destruct v; simpl; auto.
+- rewrite Int.sign_ext_idem by omega; auto.
+- rewrite Int.zero_ext_idem by omega; auto.
+- rewrite Int.sign_ext_idem by omega; auto.
+- rewrite Int.zero_ext_idem by omega; auto.
+- destruct Archi.ptr64 eqn:SF; simpl; auto.
+- destruct Archi.ptr64 eqn:SF; simpl; auto.
+- destruct Archi.ptr64 eqn:SF; simpl; auto.
+Qed.
+
Lemma load_result_type:
forall chunk v, has_type (load_result chunk v) (type_of_chunk chunk).
Proof.
- intros. unfold has_type; destruct chunk; destruct v; simpl; auto; destruct Archi.ptr64 eqn:SF; simpl; auto.
+ intros. rewrite <- proj_rettype_of_chunk. apply has_proj_rettype.
+ apply load_result_rettype.
Qed.
Lemma load_result_same:
diff --git a/config_aarch64.sh b/config_aarch64.sh
new file mode 100755
index 00000000..ded267bf
--- /dev/null
+++ b/config_aarch64.sh
@@ -0,0 +1 @@
+exec ./config_simple.sh aarch64-linux --toolprefix aarch64-linux-gnu- "$@"
diff --git a/config_arm.sh b/config_arm.sh
new file mode 100755
index 00000000..eed55fab
--- /dev/null
+++ b/config_arm.sh
@@ -0,0 +1 @@
+exec ./config_simple.sh arm-linux --toolprefix arm-linux-gnueabihf- "$@"
diff --git a/config_ia32.sh b/config_ia32.sh
new file mode 100755
index 00000000..b40f2b39
--- /dev/null
+++ b/config_ia32.sh
@@ -0,0 +1 @@
+exec ./config_simple.sh ia32-linux "$@"
diff --git a/config_k1c.sh b/config_k1c.sh
new file mode 100755
index 00000000..20408397
--- /dev/null
+++ b/config_k1c.sh
@@ -0,0 +1 @@
+exec ./config_simple.sh k1c-cos "$@"
diff --git a/config_ppc.sh b/config_ppc.sh
new file mode 100755
index 00000000..d597cda5
--- /dev/null
+++ b/config_ppc.sh
@@ -0,0 +1 @@
+exec ./config_simple.sh ppc-linux --toolprefix powerpc-linux-gnu- "$@"
diff --git a/config_rv32.sh b/config_rv32.sh
new file mode 100755
index 00000000..654cacfa
--- /dev/null
+++ b/config_rv32.sh
@@ -0,0 +1 @@
+exec ./config_simple.sh rv32-linux --toolprefix riscv64-unknown-elf- "$@"
diff --git a/config_rv64.sh b/config_rv64.sh
new file mode 100755
index 00000000..e95f8a70
--- /dev/null
+++ b/config_rv64.sh
@@ -0,0 +1 @@
+exec ./config_simple.sh rv64-linux --toolprefix riscv64-unknown-elf- "$@"
diff --git a/config_simple.sh b/config_simple.sh
new file mode 100755
index 00000000..f02680c4
--- /dev/null
+++ b/config_simple.sh
@@ -0,0 +1,6 @@
+arch=$1
+shift
+version=`git rev-parse --short HEAD`
+branch=`git rev-parse --abbrev-ref HEAD`
+date=`date -I`
+./configure --prefix /opt/CompCert/${branch}/${date}_${version}/$arch "$@" $arch
diff --git a/config_x86_64.sh b/config_x86_64.sh
new file mode 100755
index 00000000..b18ec95b
--- /dev/null
+++ b/config_x86_64.sh
@@ -0,0 +1 @@
+exec ./config_simple.sh x86_64-linux "$@"
diff --git a/coq b/coq
index 0b04a8c7..fcf744fd 100755
--- a/coq
+++ b/coq
@@ -12,4 +12,4 @@ make -q ${1}o || {
done)
}
-"${COQBIN}coqide" $INCLUDES $1 && make ${1}o
+"${COQBIN}coqide" -async-proofs off $INCLUDES $1 && make ${1}o
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 3dbb9d45..f60e15a3 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -21,7 +21,7 @@ open Machine
open Cabs
open C
open Diagnostics
-open !Cutil
+open! Cutil
(** * Utility functions *)
@@ -452,7 +452,8 @@ let elab_constant loc = function
let (v, fk) = elab_float_constant f in
CFloat(v, fk)
| CONST_CHAR(wide, s) ->
- CInt(elab_char_constant loc wide s, IInt, "")
+ let ikind = if wide then wchar_ikind () else IInt in
+ CInt(elab_char_constant loc wide s, ikind, "")
| CONST_STRING(wide, s) ->
elab_string_literal loc wide s
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index 346477b5..e44a330f 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -177,7 +177,7 @@ let identifier_nondigit =
let identifier = identifier_nondigit (identifier_nondigit|digit)*
(* Whitespaces *)
-let whitespace_char_no_newline = [' ' '\t' '\012' '\r']
+let whitespace_char_no_newline = [' ' '\t' '\011' '\012' '\r']
(* Integer constants *)
let nonzero_digit = ['1'-'9']
diff --git a/driver/Interp.ml b/driver/Interp.ml
index a6841460..d4286779 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -15,12 +15,12 @@
open Format
open Camlcoq
open AST
-open !Integers
+open! Integers
open Values
open Memory
open Globalenvs
open Events
-open Ctypes
+open! Ctypes
open Csyntax
open Csem
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index d86e137a..c9d6fced 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -18,7 +18,7 @@
open Format
open Camlcoq
open AST
-open Ctypes
+open! Ctypes
open Cop
open Clight
@@ -221,6 +221,14 @@ let asttype p t =
| AST.Tany32 -> "AST.Tany32"
| AST.Tany64 -> "AST.Tany64")
+let astrettype p = function
+ | AST.Tret t -> asttype p t
+ | AST.Tvoid -> fprintf p "AST.Tvoid"
+ | AST.Tint8signed -> fprintf p "AST.Tint8signed"
+ | AST.Tint8unsigned -> fprintf p "AST.Tint8unsigned"
+ | AST.Tint16signed -> fprintf p "AST.Tint16signed"
+ | AST.Tint16unsigned -> fprintf p "AST.Tint16unsigned"
+
let name_of_chunk = function
| Mint8signed -> "Mint8signed"
| Mint8unsigned -> "Mint8unsigned"
@@ -236,7 +244,7 @@ let name_of_chunk = function
let signatur p sg =
fprintf p "@[<hov 2>(mksignature@ %a@ %a@ %a)@]"
(print_list asttype) sg.sig_args
- (print_option asttype) sg.sig_res
+ astrettype sg.sig_res
callconv sg.sig_cc
let assertions = ref ([]: (string * typ list) list)
diff --git a/lib/Maps.v b/lib/Maps.v
index 1dec59a2..8de3c892 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -116,6 +116,19 @@ Module Type TREE.
forall (m1: t A) (m2: t B) (i: elt),
get i (combine f m1 m2) = f (get i m1) (get i m2).
+ Parameter combine_null :
+ forall (A B C: Type) (f: A -> B -> option C),
+ t A -> t B -> t C.
+
+ Axiom gcombine_null:
+ forall (A B C: Type) (f: A -> B -> option C),
+ forall (m1: t A) (m2: t B) (i: elt),
+ get i (combine_null f m1 m2) =
+ match (get i m1), (get i m2) with
+ | (Some x1), (Some x2) => f x1 x2
+ | _, _ => None
+ end.
+
(** Enumerating the bindings of a tree. *)
Parameter elements:
forall (A: Type), t A -> list (elt * A).
@@ -151,6 +164,12 @@ Module Type TREE.
forall (A B: Type) (f: B -> A -> B) (v: B) (m: t A),
fold1 f m v =
List.fold_left (fun a p => f a (snd p)) (elements m) v.
+
+ Parameter bempty_canon :
+ forall (A : Type), t A -> bool.
+ Axiom bempty_canon_correct:
+ forall (A : Type) (tr : t A) (i : elt),
+ bempty_canon tr = true -> get i tr = None.
End TREE.
(** * The abstract signatures of maps *)
@@ -261,6 +280,12 @@ Module PTree <: TREE.
induction i; simpl; auto.
Qed.
+ Definition bempty_canon (A : Type) (tr : t A) : bool :=
+ match tr with
+ | Leaf => true
+ | _ => false
+ end.
+
Theorem gss:
forall (A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = Some x.
Proof.
@@ -269,7 +294,16 @@ Module PTree <: TREE.
Lemma gleaf : forall (A : Type) (i : positive), get i (Leaf : t A) = None.
Proof. exact gempty. Qed.
-
+
+ Lemma bempty_canon_correct:
+ forall (A : Type) (tr : t A) (i : elt),
+ bempty_canon tr = true -> get i tr = None.
+ Proof.
+ destruct tr; intros.
+ - rewrite gleaf; trivial.
+ - discriminate.
+ Qed.
+
Theorem gso:
forall (A: Type) (i j: positive) (x: A) (m: t A),
i <> j -> get i (set j x m) = get i m.
@@ -625,7 +659,81 @@ Module PTree <: TREE.
auto.
Qed.
- Fixpoint xelements (A : Type) (m : t A) (i : positive)
+ Section COMBINE_NULL.
+
+ Variables A B C: Type.
+ Variable f: A -> B -> option C.
+
+
+ Fixpoint combine_null (m1: t A) (m2: t B) {struct m1} : t C :=
+ match m1, m2 with
+ | (Node l1 o1 r1), (Node l2 o2 r2) =>
+ Node' (combine_null l1 l2)
+ (match o1, o2 with
+ | (Some x1), (Some x2) => f x1 x2
+ | _, _ => None
+ end)
+ (combine_null r1 r2)
+ | _, _ => Leaf
+ end.
+
+ Theorem gcombine_null:
+ forall (m1: t A) (m2: t B) (i: positive),
+ get i (combine_null m1 m2) =
+ match (get i m1), (get i m2) with
+ | (Some x1), (Some x2) => f x1 x2
+ | _, _ => None
+ end.
+ Proof.
+ induction m1; intros; simpl.
+ - rewrite gleaf. rewrite gleaf.
+ reflexivity.
+ - destruct m2; simpl.
+ + rewrite gleaf. rewrite gleaf.
+ destruct get; reflexivity.
+ + rewrite gnode'.
+ destruct i; simpl; try rewrite IHm1_1; try rewrite IHm1; trivial.
+ Qed.
+
+ End COMBINE_NULL.
+
+ Section REMOVE_TREE.
+
+ Variables A B: Type.
+
+ Fixpoint remove_t (m1: t A) (m2: t B) {struct m1} : t A :=
+ match m1, m2 with
+ | Leaf, _ | _, Leaf => m1
+ | (Node l1 o1 r1), (Node l2 o2 r2) =>
+ Node' (remove_t l1 l2)
+ (match o2 with
+ | Some _ => None
+ | None => o1
+ end)
+ (remove_t r1 r2)
+ end.
+
+ Theorem gremove_t:
+ forall m1 : t A,
+ forall m2 : t B,
+ forall i : positive,
+ get i (remove_t m1 m2) = match get i m2 with
+ | None => get i m1
+ | Some _ => None
+ end.
+ Proof.
+ induction m1; intros; simpl.
+ - rewrite gleaf.
+ destruct get; reflexivity.
+ - destruct m2; simpl.
+ + rewrite gleaf.
+ reflexivity.
+ + rewrite gnode'.
+ destruct i; simpl; try rewrite IHm1_1; try rewrite IHm1; trivial.
+ Qed.
+ End REMOVE_TREE.
+
+ Fixpoint xelements (A : Type) (m : t A) (i : positive)
(k: list (positive * A)) {struct m}
: list (positive * A) :=
match m with
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 02f9141b..01eda623 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -339,7 +339,7 @@ Proof.
}
destruct (Mem.load _ m1 _ _) in *; destruct (Mem.load _ m0 _ _) in *; congruence.
Qed.
-
+
Definition goto_label_deps (f: function) (lbl: label) (vpc: val) :=
match label_pos lbl 0 (fn_blocks f) with
| None => None
@@ -1005,7 +1005,7 @@ Theorem bisimu_par_wio_basic ge fn rsr rsw mr mw sr sw bi:
Proof.
(* a little tactic to automate reasoning on preg_eq *)
-Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr.
+Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr: core.
Local Ltac preg_eq_discr r rd :=
destruct (preg_eq r rd); try (subst r; rewrite assign_eq, Pregmap.gss; auto);
rewrite (assign_diff _ (#rd) (#r) _); auto;
@@ -1053,7 +1053,7 @@ Local Ltac preg_eq_discr r rd :=
preg_eq_discr r rd0. }
(* Load Octuple word *)
- + Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr.
+ + Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr: core.
unfold parexec_load_o_offset.
destruct (gpreg_o_expand rd) as [[[rd0 rd1] rd2] rd3]; destruct Ge; simpl.
rewrite H0, H.
@@ -1423,7 +1423,7 @@ Section SECT_BBLOCK_EQUIV.
Variable Ge: genv.
-Local Hint Resolve trans_state_match.
+Local Hint Resolve trans_state_match: core.
Lemma bblock_simu_reduce:
forall p1 p2 ge fn,
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 50637723..36269954 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -28,6 +28,8 @@ Require Import Chunks.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
+Import PArithCoercions.
+
(** The code generation functions take advantage of several
characteristics of the [Mach] code generated by earlier passes of the
compiler, mostly that argument and result registers are of the correct
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index ecb4629b..5b44ddaa 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -23,6 +23,8 @@ Require Import Op Locations Machblock Conventions.
Require Import Asmblock Asmblockgen Asmblockgenproof0 Asmblockprops.
Require Import Chunks.
+Import PArithCoercions.
+
(** Decomposition of integer constants. *)
Lemma make_immed32_sound:
@@ -859,7 +861,7 @@ Proof.
destruct cmp; discriminate.
Qed.
-Local Hint Resolve Val_cmpu_bool_correct Val_cmplu_bool_correct.
+Local Hint Resolve Val_cmpu_bool_correct Val_cmplu_bool_correct: core.
Lemma transl_cbranch_correct_1:
forall cond args lbl k c m ms b sp rs m' tbb,
@@ -1163,7 +1165,7 @@ Proof.
split; intros; Simpl.
Qed.
-Local Hint Resolve Val_cmpu_correct Val_cmplu_correct.
+Local Hint Resolve Val_cmpu_correct Val_cmplu_correct: core.
Lemma transl_condimm_int32u_correct:
forall cmp rd r1 n k rs m,
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index e042d95a..946007c1 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -555,6 +555,8 @@ Inductive ar_instruction : Type :=
| PArithARRI64 (i: arith_name_arri64) (rd rs: ireg) (imm: int64)
.
+Module PArithCoercions.
+
Coercion PArithR: arith_name_r >-> Funclass.
Coercion PArithRR: arith_name_rr >-> Funclass.
Coercion PArithRI32: arith_name_ri32 >-> Funclass.
@@ -569,6 +571,8 @@ Coercion PArithARR: arith_name_arr >-> Funclass.
Coercion PArithARRI32: arith_name_arri32 >-> Funclass.
Coercion PArithARRI64: arith_name_arri64 >-> Funclass.
+End PArithCoercions.
+
Inductive basic : Type :=
| PArith (i: ar_instruction)
| PLoad (i: ld_instruction)
@@ -1709,7 +1713,7 @@ Proof.
Qed.
-Local Hint Resolve parexec_bblock_write_in_order.
+Local Hint Resolve parexec_bblock_write_in_order: core.
Lemma det_parexec_write_in_order f b rs m rs' m':
det_parexec f b rs m rs' m' -> parexec_wio_bblock f b rs m = Next rs' m'.
diff --git a/mppa_k1c/Builtins1.v b/mppa_k1c/Builtins1.v
index 6186961f..3b5cd419 100644
--- a/mppa_k1c/Builtins1.v
+++ b/mppa_k1c/Builtins1.v
@@ -43,18 +43,18 @@ Definition platform_builtin_table : list (string * platform_builtin) :=
Definition platform_builtin_sig (b: platform_builtin) : signature :=
match b with
| BI_fmin | BI_fmax =>
- mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default
+ mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default
| BI_fminf | BI_fmaxf =>
- mksignature (Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default
+ mksignature (Tsingle :: Tsingle :: nil) Tsingle cc_default
| BI_fabsf =>
- mksignature (Tsingle :: nil) (Some Tsingle) cc_default
+ mksignature (Tsingle :: nil) Tsingle cc_default
| BI_fma =>
- mksignature (Tfloat :: Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default
+ mksignature (Tfloat :: Tfloat :: Tfloat :: nil) Tfloat cc_default
| BI_fmaf =>
- mksignature (Tsingle :: Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default
+ mksignature (Tsingle :: Tsingle :: Tsingle :: nil) Tsingle cc_default
end.
-Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
+Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
match b with
| BI_fmin => mkbuiltin_n2t Tfloat Tfloat Tfloat ExtFloat.min
| BI_fmax => mkbuiltin_n2t Tfloat Tfloat Tfloat ExtFloat.max
diff --git a/mppa_k1c/CSE2deps.v b/mppa_k1c/CSE2deps.v
new file mode 100644
index 00000000..8ab9242a
--- /dev/null
+++ b/mppa_k1c/CSE2deps.v
@@ -0,0 +1,20 @@
+Require Import BoolEqual Coqlib.
+Require Import AST Integers Floats.
+Require Import Values Memory Globalenvs Events.
+Require Import Op.
+
+
+Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
+ (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk))
+ && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk))
+ && ((ofsw + size_chunk chunkw <=? ofsr) ||
+ (ofsr + size_chunk chunkr <=? ofsw)).
+
+Definition may_overlap chunk addr args chunk' addr' args' :=
+ match addr, addr', args, args' with
+ | (Aindexed ofs), (Aindexed ofs'),
+ (base :: nil), (base' :: nil) =>
+ if peq base base'
+ then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk)
+ else true | _, _, _, _ => true
+ end.
diff --git a/mppa_k1c/CSE2depsproof.v b/mppa_k1c/CSE2depsproof.v
new file mode 100644
index 00000000..a3811e78
--- /dev/null
+++ b/mppa_k1c/CSE2depsproof.v
@@ -0,0 +1,127 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Maps.
+
+Require Import Globalenvs Values.
+Require Import Linking Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import CSE2 CSE2deps.
+Require Import Lia.
+
+Lemma ptrofs_size :
+ Ptrofs.wordsize = (if Archi.ptr64 then 64 else 32)%nat.
+Proof.
+ unfold Ptrofs.wordsize.
+ unfold Wordsize_Ptrofs.wordsize.
+ trivial.
+Qed.
+
+Lemma ptrofs_modulus :
+ Ptrofs.modulus = if Archi.ptr64 then 18446744073709551616 else 4294967296.
+Proof.
+ unfold Ptrofs.modulus.
+ rewrite ptrofs_size.
+ destruct Archi.ptr64; reflexivity.
+Qed.
+
+Section SOUNDNESS.
+ Variable F V : Type.
+ Variable genv: Genv.t F V.
+ Variable sp : val.
+
+Section MEMORY_WRITE.
+ Variable m m2 : mem.
+ Variable chunkw chunkr : memory_chunk.
+ Variable base : val.
+
+ Variable addrw addrr valw : val.
+ Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
+
+ Section INDEXED_AWAY.
+ Variable ofsw ofsr : ptrofs.
+ Hypothesis ADDRW : eval_addressing genv sp
+ (Aindexed ofsw) (base :: nil) = Some addrw.
+ Hypothesis ADDRR : eval_addressing genv sp
+ (Aindexed ofsr) (base :: nil) = Some addrr.
+
+ Lemma load_store_away1 :
+ forall RANGEW : 0 <= Ptrofs.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk,
+ forall RANGER : 0 <= Ptrofs.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk,
+ forall SWAPPABLE : Ptrofs.unsigned ofsw + size_chunk chunkw <= Ptrofs.unsigned ofsr
+ \/ Ptrofs.unsigned ofsr + size_chunk chunkr <= Ptrofs.unsigned ofsw,
+ Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+
+ Proof.
+ intros.
+
+ pose proof (max_size_chunk chunkr) as size_chunkr_bounded.
+ pose proof (max_size_chunk chunkw) as size_chunkw_bounded.
+ unfold largest_size_chunk in *.
+
+ rewrite ptrofs_modulus in *.
+ simpl in *.
+ inv ADDRR.
+ inv ADDRW.
+ destruct base; try discriminate.
+ eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
+ exact STORE.
+ right.
+
+ all: try (destruct (Ptrofs.unsigned_add_either i ofsr) as [OFSR | OFSR];
+ rewrite OFSR).
+ all: try (destruct (Ptrofs.unsigned_add_either i ofsw) as [OFSW | OFSW];
+ rewrite OFSW).
+ all: try rewrite ptrofs_modulus in *.
+ all: destruct Archi.ptr64.
+
+ all: intuition lia.
+ Qed.
+
+ Theorem load_store_away :
+ can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true ->
+ Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+ Proof.
+ intro SWAP.
+ unfold can_swap_accesses_ofs in SWAP.
+ repeat rewrite andb_true_iff in SWAP.
+ repeat rewrite orb_true_iff in SWAP.
+ repeat rewrite Z.leb_le in SWAP.
+ apply load_store_away1.
+ all: tauto.
+ Qed.
+ End INDEXED_AWAY.
+End MEMORY_WRITE.
+End SOUNDNESS.
+
+
+Section SOUNDNESS.
+ Variable F V : Type.
+ Variable genv: Genv.t F V.
+ Variable sp : val.
+
+Lemma may_overlap_sound:
+ forall m m' : mem,
+ forall chunk addr args chunk' addr' args' v a a' rs,
+ (eval_addressing genv sp addr (rs ## args)) = Some a ->
+ (eval_addressing genv sp addr' (rs ## args')) = Some a' ->
+ (may_overlap chunk addr args chunk' addr' args') = false ->
+ (Mem.storev chunk m a v) = Some m' ->
+ (Mem.loadv chunk' m' a') = (Mem.loadv chunk' m a').
+Proof.
+ intros until rs.
+ intros ADDR ADDR' OVERLAP STORE.
+ destruct addr; destruct addr'; try discriminate.
+ { (* Aindexed / Aindexed *)
+ destruct args as [ | base [ | ]]. 1,3: discriminate.
+ destruct args' as [ | base' [ | ]]. 1,3: discriminate.
+ simpl in OVERLAP.
+ destruct (peq base base'). 2: discriminate.
+ subst base'.
+ destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP.
+ 2: discriminate.
+ simpl in *.
+ eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
+ }
+Qed.
+
+End SOUNDNESS.
diff --git a/mppa_k1c/Conventions1.v b/mppa_k1c/Conventions1.v
index d41f1095..48346a6d 100644
--- a/mppa_k1c/Conventions1.v
+++ b/mppa_k1c/Conventions1.v
@@ -90,12 +90,17 @@ Definition is_float_reg (r: mreg) := false.
returned value. We treat a function without result as a function
with one integer result. *)
+
Definition loc_result (s: signature) : rpair mreg :=
- match s.(sig_res) with
- | None => One R0
- | Some (Tint | Tany32) => One R0
- | Some (Tfloat | Tsingle | Tany64) => One R0
- | Some Tlong => if Archi.ptr64 then One R0 else One R0
+ match s.(sig_res) with
+ | Tvoid => One R0
+ | Tint8signed => One R0
+ | Tint8unsigned => One R0
+ | Tint16signed => One R0
+ | Tint16unsigned => One R0
+ | Tint | Tany32 => One R0
+ | Tfloat | Tsingle | Tany64 => One R0
+ | Tlong => if Archi.ptr64 then One R0 else One R0
end.
(** The result registers have types compatible with that given in the signature. *)
@@ -104,8 +109,8 @@ Lemma loc_result_type:
forall sig,
subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
Proof.
- intros. unfold proj_sig_res, loc_result, mreg_type;
- destruct (sig_res sig) as [[]|]; auto; destruct Archi.ptr64; auto.
+ intros. unfold proj_sig_res, loc_result, mreg_type.
+ destruct (sig_res sig); try destruct Archi.ptr64; simpl; trivial; destruct t; trivial.
Qed.
(** The result locations are caller-save registers *)
@@ -115,7 +120,7 @@ Lemma loc_result_caller_save:
forall_rpair (fun r => is_callee_save r = false) (loc_result s).
Proof.
intros. unfold loc_result, is_callee_save;
- destruct (sig_res s) as [[]|]; simpl; auto; destruct Archi.ptr64; simpl; auto.
+ destruct (sig_res s); simpl; auto; try destruct Archi.ptr64; simpl; auto; try destruct t; simpl; auto.
Qed.
(** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
@@ -125,14 +130,15 @@ Lemma loc_result_pair:
match loc_result sg with
| One _ => True
| Twolong r1 r2 =>
- r1 <> r2 /\ sg.(sig_res) = Some Tlong
+ r1 <> r2 /\ proj_sig_res sg = Tlong
/\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
/\ Archi.ptr64 = false
end.
Proof.
intros.
- unfold loc_result; destruct (sig_res sg) as [[]|]; auto.
- unfold mreg_type; destruct Archi.ptr64; auto.
+ unfold loc_result; destruct (sig_res sg); auto;
+ unfold mreg_type; try destruct Archi.ptr64; auto;
+ destruct t; auto.
Qed.
(** The location of the result depends only on the result part of the signature *)
@@ -409,3 +415,6 @@ Lemma loc_arguments_main:
Proof.
reflexivity.
Qed.
+
+
+Definition return_value_needs_normalization (t: rettype) : bool := false.
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index fbb06c9b..3b123c75 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -567,7 +567,7 @@ Proof.
unfold builtin_alone in H0. erewrite H0; eauto.
Qed.
-Local Hint Resolve verified_schedule_nob_checks_alls_bundles.
+Local Hint Resolve verified_schedule_nob_checks_alls_bundles: core.
Lemma verified_schedule_checks_alls_bundles bb lb bundle:
verified_schedule bb = OK lb ->
diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
index 5c94d435..cf46072f 100644
--- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
+++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
@@ -403,7 +403,7 @@ Proof.
* eapply H2; eauto. intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff; auto.
* intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff, <- in_rev; auto.
Qed.
-Local Hint Resolve app_fail_allvalid_correct.
+Local Hint Resolve app_fail_allvalid_correct: core.
Lemma app_fail_correct l pt t1 t2:
match_pt t1 pt ->
diff --git a/mppa_k1c/abstractbb/ImpSimuTest.v b/mppa_k1c/abstractbb/ImpSimuTest.v
index ea55b735..7a77ec15 100644
--- a/mppa_k1c/abstractbb/ImpSimuTest.v
+++ b/mppa_k1c/abstractbb/ImpSimuTest.v
@@ -304,12 +304,12 @@ Proof.
rewrite <- EQT; eauto.
+ exploit smem_valid_set_decompose_1; eauto.
- clear DM0. unfold hsmem_post_eval, hsmem_post_eval in * |- *; simpl.
- Local Hint Resolve smem_valid_set_decompose_1.
+ Local Hint Resolve smem_valid_set_decompose_1: core.
intros; case (R.eq_dec x x0).
+ intros; subst; rewrite !Dict.set_spec_eq; simpl; eauto.
+ intros; rewrite !Dict.set_spec_diff; simpl; eauto.
Qed.
-Local Hint Resolve naive_set_correct.
+Local Hint Resolve naive_set_correct: core.
Definition equiv_hsmem ge (hd1 hd2: hsmem) :=
(forall m, allvalid ge hd1.(hpre) m <-> allvalid ge hd2.(hpre) m)
@@ -523,7 +523,7 @@ Lemma hinst_smem_correct i: forall hd hod,
WHEN hinst_smem i hd hod ~> hd' THEN
forall ge od d, smem_model ge od hod -> smem_model ge d hd -> (forall m, smem_valid ge d m -> smem_valid ge od m) -> smem_model ge (inst_smem i d od) hd'.
Proof.
- Local Hint Resolve smem_valid_set_proof.
+ Local Hint Resolve smem_valid_set_proof: core.
induction i; simpl; wlp_simplify; eauto 15 with wlp.
Qed.
Global Opaque hinst_smem.
@@ -563,7 +563,7 @@ Definition bblock_hsmem: bblock -> ?? hsmem
Lemma bblock_hsmem_correct p:
WHEN bblock_hsmem p ~> hd THEN forall ge, smem_model ge (bblock_smem p) hd.
Proof.
- Local Hint Resolve hsmem_empty_correct.
+ Local Hint Resolve hsmem_empty_correct: core.
wlp_simplify.
Qed.
Global Opaque bblock_hsmem.
@@ -775,7 +775,7 @@ Proof.
intro H; erewrite <- list_term_eval_set_hid; rewrite H. apply list_term_eval_set_hid.
Qed.
-Local Hint Resolve term_eval_set_hid_equiv list_term_eval_set_hid_equiv.
+Local Hint Resolve term_eval_set_hid_equiv list_term_eval_set_hid_equiv: core.
Program Definition bblock_simu_test (p1 p2: bblock): ?? bool :=
DO log <~ count_logger ();;
@@ -802,7 +802,7 @@ Obligation 2.
wlp_simplify.
Qed.
-Local Hint Resolve g_bblock_simu_test_correct.
+Local Hint Resolve g_bblock_simu_test_correct: core.
Theorem bblock_simu_test_correct p1 p2:
WHEN bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2.
@@ -1123,7 +1123,7 @@ Definition get {A} (d:t A) (x:R.t): option A
Definition set {A} (d:t A) (x:R.t) (v:A): t A
:= PositiveMap.add x v d.
-Local Hint Unfold PositiveMap.E.eq.
+Local Hint Unfold PositiveMap.E.eq: core.
Lemma set_spec_eq A d x (v: A):
get (set d x v) x = Some v.
diff --git a/mppa_k1c/abstractbb/Impure/ImpHCons.v b/mppa_k1c/abstractbb/Impure/ImpHCons.v
index d8002375..637116cc 100644
--- a/mppa_k1c/abstractbb/Impure/ImpHCons.v
+++ b/mppa_k1c/abstractbb/Impure/ImpHCons.v
@@ -95,7 +95,7 @@ Proof.
wlp_simplify.
Qed.
Global Opaque assert_list_incl.
-Hint Resolve assert_list_incl_correct.
+Hint Resolve assert_list_incl_correct: wlp.
End Sets.
@@ -165,7 +165,7 @@ Lemma hConsV_correct A (hasheq: A -> A -> ?? bool):
(forall x y, WHEN hasheq x y ~> b THEN b=true -> x=y) ->
forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data).
Proof.
- Local Hint Resolve f_equal2.
+ Local Hint Resolve f_equal2: core.
wlp_simplify.
exploit H; eauto.
+ wlp_simplify.
diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v
index 22809095..30904b5d 100644
--- a/mppa_k1c/abstractbb/Parallelizability.v
+++ b/mppa_k1c/abstractbb/Parallelizability.v
@@ -332,7 +332,7 @@ Fixpoint bblock_wframe(p:bblock): list R.t :=
| i::p' => (inst_wframe i)++(bblock_wframe p')
end.
-Local Hint Resolve Permutation_app_head Permutation_app_tail Permutation_app_comm.
+Local Hint Resolve Permutation_app_head Permutation_app_tail Permutation_app_comm: core.
Lemma bblock_wframe_Permutation p p':
Permutation p p' -> Permutation (bblock_wframe p) (bblock_wframe p').
@@ -620,7 +620,7 @@ Include ParallelizablityChecking L.
Section PARALLEL2.
Variable ge: genv.
-Local Hint Resolve S.empty_match_frame S.add_match_frame S.union_match_frame S.is_disjoint_match_frame.
+Local Hint Resolve S.empty_match_frame S.add_match_frame S.union_match_frame S.is_disjoint_match_frame: core.
(** Now, refinement of each operation toward parallelizable *)
@@ -659,14 +659,14 @@ Fixpoint inst_sframe (i: inst): S.t :=
| a::i' => S.add (fst a) (S.union (exp_sframe (snd a)) (inst_sframe i'))
end.
-Local Hint Resolve exp_sframe_correct.
+Local Hint Resolve exp_sframe_correct: core.
Lemma inst_sframe_correct i: S.match_frame (inst_sframe i) (inst_frame i).
Proof.
induction i as [|[y e] i']; simpl; auto.
Qed.
-Local Hint Resolve inst_wsframe_correct inst_sframe_correct.
+Local Hint Resolve inst_wsframe_correct inst_sframe_correct: core.
Fixpoint is_pararec (p: bblock) (wsframe: S.t): bool :=
match p with
diff --git a/mppa_k1c/abstractbb/SeqSimuTheory.v b/mppa_k1c/abstractbb/SeqSimuTheory.v
index 649dd083..e234883f 100644
--- a/mppa_k1c/abstractbb/SeqSimuTheory.v
+++ b/mppa_k1c/abstractbb/SeqSimuTheory.v
@@ -102,9 +102,6 @@ Fixpoint bblock_smem_rec (p: bblock) (d: smem): smem :=
let d':=inst_smem i d d in
bblock_smem_rec p' d'
end.
-(*
-Local Hint Resolve smem_eval_empty.
-*)
Definition bblock_smem: bblock -> smem
:= fun p => bblock_smem_rec p smem_empty.
@@ -124,7 +121,7 @@ Proof.
intros d a H; eapply inst_smem_pre_monotonic; eauto.
Qed.
-Local Hint Resolve inst_smem_pre_monotonic bblock_smem_pre_monotonic.
+Local Hint Resolve inst_smem_pre_monotonic bblock_smem_pre_monotonic: core.
Lemma term_eval_exp e (od:smem) m0 old:
(forall x, term_eval ge (od x) m0 = Some (old x)) ->
@@ -185,7 +182,7 @@ Lemma bblocks_smem_rec_Some_correct1 p m0: forall (m1 m2: mem) (d: smem),
(forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
forall x, term_eval ge (bblock_smem_rec p d x) m0 = Some (m2 x).
Proof.
- Local Hint Resolve inst_smem_Some_correct1.
+ Local Hint Resolve inst_smem_Some_correct1: core.
induction p as [ | i p]; simpl; intros m1 m2 d H.
- inversion_clear H; eauto.
- intros H0 x0.
@@ -299,7 +296,7 @@ Lemma block_smem_rec_valid p m0: forall (m1 m2: mem) (d:smem),
(forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
pre (bblock_smem_rec p d) ge m0.
Proof.
- Local Hint Resolve inst_valid.
+ Local Hint Resolve inst_valid: core.
induction p as [ | i p]; simpl; intros m1 d H; auto.
intros H0 H1.
destruct (inst_run ge i m1 m1) eqn: Heqov; eauto.
@@ -326,7 +323,7 @@ Theorem bblock_smem_simu p1 p2:
smem_simu (bblock_smem p1) (bblock_smem p2) ->
bblock_simu ge p1 p2.
Proof.
- Local Hint Resolve bblock_smem_valid bblock_smem_Some_correct1.
+ Local Hint Resolve bblock_smem_valid bblock_smem_Some_correct1: core.
intros (INCL & EQUIV) m DONTFAIL; unfold smem_valid in * |-.
destruct (run ge p1 m) as [m1|] eqn: RUN1; simpl; try congruence.
assert (X: forall x, term_eval ge (bblock_smem p1 x) m = Some (m1 x)); eauto.
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index 940c6563..58455ada 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -414,7 +414,7 @@ Proof.
Qed.
-Local Hint Resolve code_tail_0 code_tail_S.
+Local Hint Resolve code_tail_0 code_tail_S: core.
Lemma code_tail_next:
forall fn ofs c0,
@@ -458,7 +458,7 @@ Proof.
omega.
Qed.
-Local Hint Resolve code_tail_next.
+Local Hint Resolve code_tail_next: core.
Lemma code_tail_next_int:
forall fn ofs bi c,
diff --git a/mppa_k1c/lib/ForwardSimulationBlock.v b/mppa_k1c/lib/ForwardSimulationBlock.v
index 39dd2234..224eda0a 100644
--- a/mppa_k1c/lib/ForwardSimulationBlock.v
+++ b/mppa_k1c/lib/ForwardSimulationBlock.v
@@ -21,7 +21,7 @@ Section starN_lemma.
Variable L: semantics.
-Local Hint Resolve starN_refl starN_step Eapp_assoc.
+Local Hint Resolve starN_refl starN_step Eapp_assoc: core.
Lemma starN_split n s t s':
starN (step L) (globalenv L) n s t s' ->
@@ -93,7 +93,7 @@ Hypothesis simu_end_block:
(** Introduction d'une sémantique par bloc sur L1 appelée "memoL1" *)
-Local Hint Resolve starN_refl starN_step.
+Local Hint Resolve starN_refl starN_step: core.
Definition follows_in_block (head current: state L1): Prop :=
dist_end_block head >= dist_end_block current
@@ -164,7 +164,7 @@ Inductive is_well_memorized (s s': memostate): Prop :=
memorized s' = None ->
is_well_memorized s s'.
-Local Hint Resolve StartBloc MidBloc ExitBloc.
+Local Hint Resolve StartBloc MidBloc ExitBloc: core.
Definition memoL1 := {|
state := memostate;
diff --git a/mppa_k1c/lib/Machblockgen.v b/mppa_k1c/lib/Machblockgen.v
index a65b218f..2ba42814 100644
--- a/mppa_k1c/lib/Machblockgen.v
+++ b/mppa_k1c/lib/Machblockgen.v
@@ -105,7 +105,7 @@ Inductive is_end_block: Machblock_inst -> code -> Prop :=
| End_basic bi bh bl: header bh <> nil -> is_end_block (MB_basic bi) (bh::bl)
| End_cfi cfi bl: bl <> nil -> is_end_block (MB_cfi cfi) bl.
-Local Hint Resolve End_empty End_basic End_cfi.
+Local Hint Resolve End_empty End_basic End_cfi: core.
Inductive is_trans_code: Mach.code -> code -> Prop :=
| Tr_nil: is_trans_code nil nil
@@ -123,7 +123,7 @@ Inductive is_trans_code: Mach.code -> code -> Prop :=
header bh = nil ->
is_trans_code (i::c) (add_basic bi bh::bl).
-Local Hint Resolve Tr_nil Tr_end_block.
+Local Hint Resolve Tr_nil Tr_end_block: core.
Lemma add_to_code_is_trans_code i c bl:
is_trans_code c bl ->
@@ -145,7 +145,7 @@ Proof.
rewrite <- Heqti. eapply End_cfi. congruence.
Qed.
-Local Hint Resolve add_to_code_is_trans_code.
+Local Hint Resolve add_to_code_is_trans_code: core.
Lemma trans_code_is_trans_code_rev c1: forall c2 mbi,
is_trans_code c2 mbi ->
@@ -185,7 +185,7 @@ Proof.
exists mbi1. split; congruence.
Qed.
-Local Hint Resolve trans_code_is_trans_code.
+Local Hint Resolve trans_code_is_trans_code: core.
Theorem is_trans_code_inv c bl: is_trans_code c bl <-> bl=(trans_code c).
Proof.
diff --git a/mppa_k1c/lib/Machblockgenproof.v b/mppa_k1c/lib/Machblockgenproof.v
index 91be5e2e..0de2df52 100644
--- a/mppa_k1c/lib/Machblockgenproof.v
+++ b/mppa_k1c/lib/Machblockgenproof.v
@@ -72,7 +72,7 @@ Proof.
apply match_states_trans_state.
Qed.
-Local Hint Resolve match_states_trans_state.
+Local Hint Resolve match_states_trans_state: core.
Lemma symbols_preserved:
forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
@@ -284,7 +284,7 @@ Proof.
Qed.
Local Hint Resolve symbols_preserved senv_preserved init_mem_preserved prog_main_preserved functions_translated
- parent_sp_preserved.
+ parent_sp_preserved: core.
Definition dist_end_block_code (c: Mach.code) :=
@@ -299,8 +299,8 @@ Definition dist_end_block (s: Mach.state): nat :=
| _ => 0
end.
-Local Hint Resolve exec_nil_body exec_cons_body.
-Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exec_MBload exec_MBstore.
+Local Hint Resolve exec_nil_body exec_cons_body: core.
+Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exec_MBload exec_MBstore: core.
Lemma size_add_label l bh: size (add_label l bh) = size bh + 1.
Proof.
@@ -336,7 +336,7 @@ Proof.
omega.
Qed.
-Local Hint Resolve dist_end_block_code_simu_mid_block.
+Local Hint Resolve dist_end_block_code_simu_mid_block: core.
Lemma size_nonzero c b bl:
@@ -392,8 +392,8 @@ destruct i; congruence.
Qed.
-Local Hint Resolve Mlabel_is_not_cfi.
-Local Hint Resolve MBbasic_is_not_cfi.
+Local Hint Resolve Mlabel_is_not_cfi: core.
+Local Hint Resolve MBbasic_is_not_cfi: core.
Lemma add_to_new_block_is_label i:
header (add_to_new_bblock (trans_inst i)) <> nil -> exists l, i = Mlabel l.
@@ -408,7 +408,7 @@ Proof.
+ unfold cfi_bblock in H; simpl in H; congruence.
Qed.
-Local Hint Resolve Mlabel_is_not_basic.
+Local Hint Resolve Mlabel_is_not_basic: core.
Lemma trans_code_decompose c: forall b bl,
is_trans_code c (b::bl) ->
@@ -510,8 +510,8 @@ Proof.
rewrite Hs2, Hb2; eauto.
Qed.
-Local Hint Resolve exec_MBcall exec_MBtailcall exec_MBbuiltin exec_MBgoto exec_MBcond_true exec_MBcond_false exec_MBjumptable exec_MBreturn exec_Some_exit exec_None_exit.
-Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved find_funct_ptr_same.
+Local Hint Resolve exec_MBcall exec_MBtailcall exec_MBbuiltin exec_MBgoto exec_MBcond_true exec_MBcond_false exec_MBjumptable exec_MBreturn exec_Some_exit exec_None_exit: core.
+Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved find_funct_ptr_same: core.
Lemma match_states_concat_trans_code st f sp c rs m h:
diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index ab348c14..10f38391 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -30,6 +30,10 @@ Definition align_float64 := 8%Z.
(** Can we use the 64-bit extensions to the PowerPC architecture? *)
Parameter ppc64 : bool.
+(** Should single-precision FP arguments passed on stack be passed
+ as singles or use double FP format. *)
+Parameter single_passed_as_single : bool.
+
Definition splitlong := negb ppc64.
Lemma splitlong_ptr32: splitlong = true -> ptr64 = false.
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 704b0aba..ce88778c 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -852,7 +852,7 @@ let expand_instruction instr =
if variadic then begin
emit (Pmflr GPR0);
emit (Pbl(intern_string "__compcert_va_saveregs",
- {sig_args = []; sig_res = None; sig_cc = cc_default}));
+ {sig_args = []; sig_res = Tvoid; sig_cc = cc_default}));
emit (Pmtlr GPR0)
end;
current_function_stacksize := sz;
diff --git a/powerpc/Builtins1.v b/powerpc/Builtins1.v
index f6e643d2..53c83d7e 100644
--- a/powerpc/Builtins1.v
+++ b/powerpc/Builtins1.v
@@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) :=
Definition platform_builtin_sig (b: platform_builtin) : signature :=
match b with end.
-Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
+Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
match b with end.
diff --git a/powerpc/CSE2deps.v b/powerpc/CSE2deps.v
new file mode 100644
index 00000000..9db51bbb
--- /dev/null
+++ b/powerpc/CSE2deps.v
@@ -0,0 +1,20 @@
+Require Import BoolEqual Coqlib.
+Require Import AST Integers Floats.
+Require Import Values Memory Globalenvs Events.
+Require Import Op.
+
+
+Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
+ (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk))
+ && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk))
+ && ((ofsw + size_chunk chunkw <=? ofsr) ||
+ (ofsr + size_chunk chunkr <=? ofsw)).
+
+Definition may_overlap chunk addr args chunk' addr' args' :=
+ match addr, addr', args, args' with
+ | (Aindexed ofs), (Aindexed ofs'),
+ (base :: nil), (base' :: nil) =>
+ if peq base base'
+ then negb (can_swap_accesses_ofs (Int.unsigned ofs') chunk' (Int.unsigned ofs) chunk)
+ else true | _, _, _, _ => true
+ end.
diff --git a/powerpc/CSE2depsproof.v b/powerpc/CSE2depsproof.v
new file mode 100644
index 00000000..fdded9b6
--- /dev/null
+++ b/powerpc/CSE2depsproof.v
@@ -0,0 +1,135 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Maps.
+
+Require Import Globalenvs Values.
+Require Import Linking Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import CSE2 CSE2deps.
+Require Import Lia.
+
+Lemma ptrofs_size :
+ Ptrofs.wordsize = if Archi.ptr64 then 64%nat else 32%nat.
+Proof.
+ unfold Ptrofs.wordsize.
+ unfold Wordsize_Ptrofs.wordsize.
+ trivial.
+Qed.
+
+Lemma ptrofs_modulus :
+ Ptrofs.modulus = if Archi.ptr64 then 18446744073709551616 else 4294967296.
+Proof.
+ unfold Ptrofs.modulus.
+ rewrite ptrofs_size.
+ destruct Archi.ptr64; reflexivity.
+Qed.
+
+Lemma ptrofs_max_unsigned :
+ Ptrofs.max_unsigned = if Archi.ptr64 then 18446744073709551615 else 4294967295.
+Proof.
+ unfold Ptrofs.max_unsigned.
+ rewrite ptrofs_modulus.
+ destruct Archi.ptr64; reflexivity.
+Qed.
+
+Section SOUNDNESS.
+ Variable F V : Type.
+ Variable genv: Genv.t F V.
+ Variable sp : val.
+
+Section MEMORY_WRITE.
+ Variable m m2 : mem.
+ Variable chunkw chunkr : memory_chunk.
+ Variable base : val.
+
+ Variable addrw addrr valw : val.
+ Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
+
+ Section INDEXED_AWAY.
+ Variable ofsw ofsr : int.
+ Hypothesis ADDRW : eval_addressing genv sp
+ (Aindexed ofsw) (base :: nil) = Some addrw.
+ Hypothesis ADDRR : eval_addressing genv sp
+ (Aindexed ofsr) (base :: nil) = Some addrr.
+
+ Lemma load_store_away1 :
+ forall RANGEW : 0 <= Int.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk,
+ forall RANGER : 0 <= Int.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk,
+ forall SWAPPABLE : Int.unsigned ofsw + size_chunk chunkw <= Int.unsigned ofsr
+ \/ Int.unsigned ofsr + size_chunk chunkr <= Int.unsigned ofsw,
+ Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+ Proof.
+ intros.
+
+ pose proof (max_size_chunk chunkr) as size_chunkr_bounded.
+ pose proof (max_size_chunk chunkw) as size_chunkw_bounded.
+ unfold largest_size_chunk in *.
+
+ rewrite ptrofs_modulus in *.
+ simpl in *.
+ inv ADDRR.
+ inv ADDRW.
+ destruct base; try discriminate.
+ eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
+ exact STORE.
+ right.
+
+ all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int ofsr)) as [OFSR | OFSR];
+ rewrite OFSR).
+ all: try (destruct (Ptrofs.unsigned_add_either i (Ptrofs.of_int ofsw)) as [OFSW | OFSW];
+ rewrite OFSW).
+ all: unfold Ptrofs.of_int.
+
+ all: repeat rewrite Ptrofs.unsigned_repr by (unfold Ptrofs.max_unsigned; rewrite ptrofs_modulus; destruct Archi.ptr64; lia).
+ all: repeat rewrite ptrofs_modulus.
+ all: destruct Archi.ptr64; intuition lia.
+ Qed.
+
+ Theorem load_store_away :
+ can_swap_accesses_ofs (Int.unsigned ofsr) chunkr (Int.unsigned ofsw) chunkw = true ->
+ Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+ Proof.
+ intro SWAP.
+ unfold can_swap_accesses_ofs in SWAP.
+ repeat rewrite andb_true_iff in SWAP.
+ repeat rewrite orb_true_iff in SWAP.
+ repeat rewrite Z.leb_le in SWAP.
+ apply load_store_away1.
+ all: tauto.
+ Qed.
+ End INDEXED_AWAY.
+End MEMORY_WRITE.
+End SOUNDNESS.
+
+
+Section SOUNDNESS.
+ Variable F V : Type.
+ Variable genv: Genv.t F V.
+ Variable sp : val.
+
+Lemma may_overlap_sound:
+ forall m m' : mem,
+ forall chunk addr args chunk' addr' args' v a a' rs,
+ (eval_addressing genv sp addr (rs ## args)) = Some a ->
+ (eval_addressing genv sp addr' (rs ## args')) = Some a' ->
+ (may_overlap chunk addr args chunk' addr' args') = false ->
+ (Mem.storev chunk m a v) = Some m' ->
+ (Mem.loadv chunk' m' a') = (Mem.loadv chunk' m a').
+Proof.
+ intros until rs.
+ intros ADDR ADDR' OVERLAP STORE.
+ destruct addr; destruct addr'; try discriminate.
+ { (* Aindexed / Aindexed *)
+ destruct args as [ | base [ | ]]. 1,3: discriminate.
+ destruct args' as [ | base' [ | ]]. 1,3: discriminate.
+ simpl in OVERLAP.
+ destruct (peq base base'). 2: discriminate.
+ subst base'.
+ destruct (can_swap_accesses_ofs (Int.unsigned i0) chunk' (Int.unsigned i) chunk) eqn:SWAP.
+ 2: discriminate.
+ simpl in *.
+ eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
+ }
+Qed.
+
+End SOUNDNESS.
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v
index 1de55c1a..5c9cbd4f 100644
--- a/powerpc/Conventions1.v
+++ b/powerpc/Conventions1.v
@@ -117,18 +117,16 @@ Definition dummy_float_reg := F0. (**r Used in [Coloring]. *)
We treat a function without result as a function with one integer result. *)
Definition loc_result_32 (s: signature) : rpair mreg :=
- match s.(sig_res) with
- | None => One R3
- | Some (Tint | Tany32) => One R3
- | Some (Tfloat | Tsingle | Tany64) => One F1
- | Some Tlong => Twolong R3 R4
+ match proj_sig_res s with
+ | Tint | Tany32 => One R3
+ | Tfloat | Tsingle | Tany64 => One F1
+ | Tlong => Twolong R3 R4
end.
Definition loc_result_64 (s: signature) : rpair mreg :=
- match s.(sig_res) with
- | None => One R3
- | Some (Tint | Tlong | Tany32 | Tany64) => One R3
- | Some (Tfloat | Tsingle) => One F1
+ match proj_sig_res s with
+ | Tint | Tlong | Tany32 | Tany64 => One R3
+ | Tfloat | Tsingle => One F1
end.
Definition loc_result :=
@@ -140,8 +138,8 @@ Lemma loc_result_type:
forall sig,
subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
Proof.
- intros. unfold proj_sig_res, loc_result, loc_result_32, loc_result_64, mreg_type.
- destruct Archi.ptr64 eqn:?; destruct (sig_res sig) as [[]|]; destruct Archi.ppc64; simpl; auto.
+ intros. unfold loc_result, loc_result_32, loc_result_64, mreg_type.
+ destruct Archi.ptr64 eqn:?; destruct (proj_sig_res sig); destruct Archi.ppc64; simpl; auto.
Qed.
(** The result locations are caller-save registers *)
@@ -151,7 +149,7 @@ Lemma loc_result_caller_save:
forall_rpair (fun r => is_callee_save r = false) (loc_result s).
Proof.
intros. unfold loc_result, loc_result_32, loc_result_64, is_callee_save;
- destruct Archi.ptr64; destruct (sig_res s) as [[]|]; simpl; auto.
+ destruct Archi.ptr64; destruct (proj_sig_res s); simpl; auto.
Qed.
(** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
@@ -161,13 +159,13 @@ Lemma loc_result_pair:
match loc_result sg with
| One _ => True
| Twolong r1 r2 =>
- r1 <> r2 /\ sg.(sig_res) = Some Tlong
+ r1 <> r2 /\ proj_sig_res sg = Tlong
/\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
/\ Archi.ptr64 = false
end.
Proof.
intros; unfold loc_result, loc_result_32, loc_result_64, mreg_type;
- destruct Archi.ptr64; destruct (sig_res sg) as [[]|]; destruct Archi.ppc64; simpl; auto.
+ destruct Archi.ptr64; destruct (proj_sig_res sg); destruct Archi.ppc64; simpl; auto.
split; auto. congruence.
split; auto. congruence.
Qed.
@@ -177,7 +175,7 @@ Qed.
Lemma loc_result_exten:
forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2.
Proof.
- intros. unfold loc_result, loc_result_32, loc_result_64.
+ intros. unfold loc_result, loc_result_32, loc_result_64, proj_sig_res.
destruct Archi.ptr64; rewrite H; auto.
Qed.
@@ -210,7 +208,16 @@ Fixpoint loc_arguments_rec
| Some ireg =>
One (R ireg) :: loc_arguments_rec tys (ir + 1) fr ofs
end
- | (Tfloat | Tsingle | Tany64) as ty :: tys =>
+ | Tsingle as ty :: tys =>
+ match list_nth_z float_param_regs fr with
+ | None =>
+ let ty := if Archi.single_passed_as_single then Tsingle else Tany64 in
+ let ofs := align ofs (typesize ty) in
+ One (S Outgoing ofs ty) :: loc_arguments_rec tys ir fr (ofs + (typesize ty))
+ | Some freg =>
+ One (R freg) :: loc_arguments_rec tys ir (fr + 1) ofs
+ end
+ | (Tfloat | Tany64) as ty :: tys =>
match list_nth_z float_param_regs fr with
| None =>
let ofs := align ofs 2 in
@@ -238,33 +245,6 @@ Fixpoint loc_arguments_rec
Definition loc_arguments (s: signature) : list (rpair loc) :=
loc_arguments_rec s.(sig_args) 0 0 0.
-(** [size_arguments s] returns the number of [Outgoing] slots used
- to call a function with signature [s]. *)
-
-Fixpoint size_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z :=
- match tyl with
- | nil => ofs
- | (Tint | Tany32) :: tys =>
- match list_nth_z int_param_regs ir with
- | None => size_arguments_rec tys ir fr (ofs + 1)
- | Some ireg => size_arguments_rec tys (ir + 1) fr ofs
- end
- | (Tfloat | Tsingle | Tany64) :: tys =>
- match list_nth_z float_param_regs fr with
- | None => size_arguments_rec tys ir fr (align ofs 2 + 2)
- | Some freg => size_arguments_rec tys ir (fr + 1) ofs
- end
- | Tlong :: tys =>
- let ir := align ir 2 in
- match list_nth_z int_param_regs ir, list_nth_z int_param_regs (ir + 1) with
- | Some r1, Some r2 => size_arguments_rec tys (ir + 2) fr ofs
- | _, _ => size_arguments_rec tys ir fr (align ofs 2 + 2)
- end
- end.
-
-Definition size_arguments (s: signature) : Z :=
- size_arguments_rec s.(sig_args) 0 0 0.
-
(** Argument locations are either caller-save registers or [Outgoing]
stack slots at nonnegative offsets. *)
@@ -324,12 +304,14 @@ Opaque list_nth_z.
apply align_divides; omega. apply Z.divide_1_l. apply Z.divide_1_l.
eapply Y; eauto. omega.
- (* single *)
+ assert (ofs <= align ofs 1) by (apply align_le; omega).
assert (ofs <= align ofs 2) by (apply align_le; omega).
destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H.
subst. right. eapply list_nth_z_in; eauto.
eapply IHtyl; eauto.
- subst. split. omega. apply Z.divide_1_l.
- eapply Y; eauto. omega.
+ subst. split. destruct Archi.single_passed_as_single; simpl; omega.
+ destruct Archi.single_passed_as_single; simpl; apply Z.divide_1_l.
+ eapply Y; eauto. destruct Archi.single_passed_as_single; simpl; omega.
- (* any32 *)
destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H.
subst. left. eapply list_nth_z_in; eauto.
@@ -361,107 +343,14 @@ Qed.
Hint Resolve loc_arguments_acceptable: locs.
-(** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
-
-Remark size_arguments_rec_above:
- forall tyl ir fr ofs0,
- ofs0 <= size_arguments_rec tyl ir fr ofs0.
-Proof.
- induction tyl; simpl; intros.
- omega.
- destruct a.
- destruct (list_nth_z int_param_regs ir); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega.
- destruct (list_nth_z float_param_regs fr); eauto.
- apply Z.le_trans with (align ofs0 2). apply align_le; omega.
- apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
- set (ir' := align ir 2).
- destruct (list_nth_z int_param_regs ir'); eauto.
- destruct (list_nth_z int_param_regs (ir' + 1)); eauto.
- apply Z.le_trans with (align ofs0 2). apply align_le; omega.
- apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
- apply Z.le_trans with (align ofs0 2). apply align_le; omega.
- apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
- destruct (list_nth_z float_param_regs fr); eauto.
- apply Z.le_trans with (align ofs0 2). apply align_le; omega.
- apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
- destruct (list_nth_z int_param_regs ir); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega.
- destruct (list_nth_z float_param_regs fr); eauto.
- apply Z.le_trans with (align ofs0 2). apply align_le; omega.
- apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
-Qed.
-
-Lemma size_arguments_above:
- forall s, size_arguments s >= 0.
-Proof.
- intros; unfold size_arguments. apply Z.le_ge.
- apply size_arguments_rec_above.
-Qed.
-
-Lemma loc_arguments_bounded:
- forall (s: signature) (ofs: Z) (ty: typ),
- In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) ->
- ofs + typesize ty <= size_arguments s.
-Proof.
- intros.
- assert (forall tyl ir fr ofs0,
- In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_rec tyl ir fr ofs0)) ->
- ofs + typesize ty <= size_arguments_rec tyl ir fr ofs0).
-{
- induction tyl; simpl; intros.
- elim H0.
- destruct a.
-- (* int *)
- destruct (list_nth_z int_param_regs ir); destruct H0.
- congruence.
- eauto.
- inv H0. apply size_arguments_rec_above.
- eauto.
-- (* float *)
- destruct (list_nth_z float_param_regs fr); destruct H0.
- congruence.
- eauto.
- inv H0. apply size_arguments_rec_above. eauto.
-- (* long *)
- set (ir' := align ir 2) in *.
- assert (DFL:
- In (S Outgoing ofs ty) (regs_of_rpairs
- ((if Archi.ptr64
- then One (S Outgoing (align ofs0 2) Tlong)
- else Twolong (S Outgoing (align ofs0 2) Tint)
- (S Outgoing (align ofs0 2 + 1) Tint))
- :: loc_arguments_rec tyl ir' fr (align ofs0 2 + 2))) ->
- ofs + typesize ty <= size_arguments_rec tyl ir' fr (align ofs0 2 + 2)).
- { destruct Archi.ptr64; intros IN.
- - destruct IN. inv H1. apply size_arguments_rec_above. auto.
- - destruct IN. inv H1. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above.
- destruct H1. inv H1. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above.
- auto. }
- destruct (list_nth_z int_param_regs ir'); auto.
- destruct (list_nth_z int_param_regs (ir' + 1)); auto.
- destruct H0. congruence. destruct H0. congruence. eauto.
-- (* single *)
- destruct (list_nth_z float_param_regs fr); destruct H0.
- congruence.
- eauto.
- inv H0. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above.
- eauto.
-- (* any32 *)
- destruct (list_nth_z int_param_regs ir); destruct H0.
- congruence.
- eauto.
- inv H0. apply size_arguments_rec_above.
- eauto.
-- (* any64 *)
- destruct (list_nth_z float_param_regs fr); destruct H0.
- congruence.
- eauto.
- inv H0. apply size_arguments_rec_above. eauto.
- }
- eauto.
-Qed.
-
Lemma loc_arguments_main:
loc_arguments signature_main = nil.
Proof.
reflexivity.
Qed.
+
+(** ** Normalization of function results *)
+
+(** No normalization needed. *)
+
+Definition return_value_needs_normalization (t: rettype) := false.
diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v
index 7482435f..a3e945bf 100644
--- a/powerpc/extractionMachdep.v
+++ b/powerpc/extractionMachdep.v
@@ -34,3 +34,6 @@ Extract Constant Archi.ppc64 =>
| ""e5500"" -> true
| _ -> false
end".
+
+(* Choice of passing of single *)
+Extract Constant Archi.single_passed_as_single => "Configuration.gnu_toolchain".
diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index 1df63308..7e36abf8 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -23,7 +23,7 @@ open Asm
open Asmexpandaux
open AST
open Camlcoq
-open !Integers
+open! Integers
exception Error of string
@@ -63,44 +63,44 @@ let expand_storeind_ptr src base ofs =
let int_param_regs = [| X10; X11; X12; X13; X14; X15; X16; X17 |]
let float_param_regs = [| F10; F11; F12; F13; F14; F15; F16; F17 |]
-let rec fixup_variadic_call pos tyl =
- if pos < 8 then
+let rec fixup_variadic_call ri rf tyl =
+ if ri < 8 then
match tyl with
| [] ->
()
| (Tint | Tany32) :: tyl ->
- fixup_variadic_call (pos + 1) tyl
+ fixup_variadic_call (ri + 1) rf tyl
| Tsingle :: tyl ->
- let rs =float_param_regs.(pos)
- and rd = int_param_regs.(pos) in
+ let rs = float_param_regs.(rf)
+ and rd = int_param_regs.(ri) in
emit (Pfmvxs(rd, rs));
- fixup_variadic_call (pos + 1) tyl
+ fixup_variadic_call (ri + 1) (rf + 1) tyl
| Tlong :: tyl ->
- let pos' = if Archi.ptr64 then pos + 1 else align pos 2 + 2 in
- fixup_variadic_call pos' tyl
+ let ri' = if Archi.ptr64 then ri + 1 else align ri 2 + 2 in
+ fixup_variadic_call ri' rf tyl
| (Tfloat | Tany64) :: tyl ->
if Archi.ptr64 then begin
- let rs = float_param_regs.(pos)
- and rd = int_param_regs.(pos) in
+ let rs = float_param_regs.(rf)
+ and rd = int_param_regs.(ri) in
emit (Pfmvxd(rd, rs));
- fixup_variadic_call (pos + 1) tyl
+ fixup_variadic_call (ri + 1) (rf + 1) tyl
end else begin
- let pos = align pos 2 in
- if pos < 8 then begin
- let rs = float_param_regs.(pos)
- and rd1 = int_param_regs.(pos)
- and rd2 = int_param_regs.(pos + 1) in
+ let ri = align ri 2 in
+ if ri < 8 then begin
+ let rs = float_param_regs.(rf)
+ and rd1 = int_param_regs.(ri)
+ and rd2 = int_param_regs.(ri + 1) in
emit (Paddiw(X2, X X2, Integers.Int.neg _16));
emit (Pfsd(rs, X2, Ofsimm _0));
emit (Plw(rd1, X2, Ofsimm _0));
emit (Plw(rd2, X2, Ofsimm _4));
emit (Paddiw(X2, X X2, _16));
- fixup_variadic_call (pos + 2) tyl
+ fixup_variadic_call (ri + 2) (rf + 1) tyl
end
end
let fixup_call sg =
- if sg.sig_cc.cc_vararg then fixup_variadic_call 0 sg.sig_args
+ if sg.sig_cc.cc_vararg then fixup_variadic_call 0 0 sg.sig_args
(* Handling of annotations *)
diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v
index f6e643d2..53c83d7e 100644
--- a/riscV/Builtins1.v
+++ b/riscV/Builtins1.v
@@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) :=
Definition platform_builtin_sig (b: platform_builtin) : signature :=
match b with end.
-Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
+Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
match b with end.
diff --git a/riscV/CSE2deps.v b/riscV/CSE2deps.v
new file mode 100644
index 00000000..8ab9242a
--- /dev/null
+++ b/riscV/CSE2deps.v
@@ -0,0 +1,20 @@
+Require Import BoolEqual Coqlib.
+Require Import AST Integers Floats.
+Require Import Values Memory Globalenvs Events.
+Require Import Op.
+
+
+Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
+ (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk))
+ && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk))
+ && ((ofsw + size_chunk chunkw <=? ofsr) ||
+ (ofsr + size_chunk chunkr <=? ofsw)).
+
+Definition may_overlap chunk addr args chunk' addr' args' :=
+ match addr, addr', args, args' with
+ | (Aindexed ofs), (Aindexed ofs'),
+ (base :: nil), (base' :: nil) =>
+ if peq base base'
+ then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk)
+ else true | _, _, _, _ => true
+ end.
diff --git a/riscV/CSE2depsproof.v b/riscV/CSE2depsproof.v
new file mode 100644
index 00000000..a3811e78
--- /dev/null
+++ b/riscV/CSE2depsproof.v
@@ -0,0 +1,127 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Maps.
+
+Require Import Globalenvs Values.
+Require Import Linking Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import CSE2 CSE2deps.
+Require Import Lia.
+
+Lemma ptrofs_size :
+ Ptrofs.wordsize = (if Archi.ptr64 then 64 else 32)%nat.
+Proof.
+ unfold Ptrofs.wordsize.
+ unfold Wordsize_Ptrofs.wordsize.
+ trivial.
+Qed.
+
+Lemma ptrofs_modulus :
+ Ptrofs.modulus = if Archi.ptr64 then 18446744073709551616 else 4294967296.
+Proof.
+ unfold Ptrofs.modulus.
+ rewrite ptrofs_size.
+ destruct Archi.ptr64; reflexivity.
+Qed.
+
+Section SOUNDNESS.
+ Variable F V : Type.
+ Variable genv: Genv.t F V.
+ Variable sp : val.
+
+Section MEMORY_WRITE.
+ Variable m m2 : mem.
+ Variable chunkw chunkr : memory_chunk.
+ Variable base : val.
+
+ Variable addrw addrr valw : val.
+ Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
+
+ Section INDEXED_AWAY.
+ Variable ofsw ofsr : ptrofs.
+ Hypothesis ADDRW : eval_addressing genv sp
+ (Aindexed ofsw) (base :: nil) = Some addrw.
+ Hypothesis ADDRR : eval_addressing genv sp
+ (Aindexed ofsr) (base :: nil) = Some addrr.
+
+ Lemma load_store_away1 :
+ forall RANGEW : 0 <= Ptrofs.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk,
+ forall RANGER : 0 <= Ptrofs.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk,
+ forall SWAPPABLE : Ptrofs.unsigned ofsw + size_chunk chunkw <= Ptrofs.unsigned ofsr
+ \/ Ptrofs.unsigned ofsr + size_chunk chunkr <= Ptrofs.unsigned ofsw,
+ Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+
+ Proof.
+ intros.
+
+ pose proof (max_size_chunk chunkr) as size_chunkr_bounded.
+ pose proof (max_size_chunk chunkw) as size_chunkw_bounded.
+ unfold largest_size_chunk in *.
+
+ rewrite ptrofs_modulus in *.
+ simpl in *.
+ inv ADDRR.
+ inv ADDRW.
+ destruct base; try discriminate.
+ eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
+ exact STORE.
+ right.
+
+ all: try (destruct (Ptrofs.unsigned_add_either i ofsr) as [OFSR | OFSR];
+ rewrite OFSR).
+ all: try (destruct (Ptrofs.unsigned_add_either i ofsw) as [OFSW | OFSW];
+ rewrite OFSW).
+ all: try rewrite ptrofs_modulus in *.
+ all: destruct Archi.ptr64.
+
+ all: intuition lia.
+ Qed.
+
+ Theorem load_store_away :
+ can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true ->
+ Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+ Proof.
+ intro SWAP.
+ unfold can_swap_accesses_ofs in SWAP.
+ repeat rewrite andb_true_iff in SWAP.
+ repeat rewrite orb_true_iff in SWAP.
+ repeat rewrite Z.leb_le in SWAP.
+ apply load_store_away1.
+ all: tauto.
+ Qed.
+ End INDEXED_AWAY.
+End MEMORY_WRITE.
+End SOUNDNESS.
+
+
+Section SOUNDNESS.
+ Variable F V : Type.
+ Variable genv: Genv.t F V.
+ Variable sp : val.
+
+Lemma may_overlap_sound:
+ forall m m' : mem,
+ forall chunk addr args chunk' addr' args' v a a' rs,
+ (eval_addressing genv sp addr (rs ## args)) = Some a ->
+ (eval_addressing genv sp addr' (rs ## args')) = Some a' ->
+ (may_overlap chunk addr args chunk' addr' args') = false ->
+ (Mem.storev chunk m a v) = Some m' ->
+ (Mem.loadv chunk' m' a') = (Mem.loadv chunk' m a').
+Proof.
+ intros until rs.
+ intros ADDR ADDR' OVERLAP STORE.
+ destruct addr; destruct addr'; try discriminate.
+ { (* Aindexed / Aindexed *)
+ destruct args as [ | base [ | ]]. 1,3: discriminate.
+ destruct args' as [ | base' [ | ]]. 1,3: discriminate.
+ simpl in OVERLAP.
+ destruct (peq base base'). 2: discriminate.
+ subst base'.
+ destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP.
+ 2: discriminate.
+ simpl in *.
+ eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
+ }
+Qed.
+
+End SOUNDNESS.
diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index df7ddfd2..7f8048f6 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -105,7 +105,9 @@ Definition is_float_reg (r: mreg) :=
of function arguments), but this leaves much liberty in choosing actual
locations. To ensure binary interoperability of code generated by our
compiler with libraries compiled by another compiler, we
- implement the standard RISC-V conventions. *)
+ implement the standard RISC-V conventions as found here:
+ https://github.com/riscv/riscv-elf-psabi-doc/blob/master/riscv-elf.md
+*)
(** ** Location of function result *)
@@ -115,11 +117,10 @@ Definition is_float_reg (r: mreg) :=
with one integer result. *)
Definition loc_result (s: signature) : rpair mreg :=
- match s.(sig_res) with
- | None => One R10
- | Some (Tint | Tany32) => One R10
- | Some (Tfloat | Tsingle | Tany64) => One F10
- | Some Tlong => if Archi.ptr64 then One R10 else Twolong R11 R10
+ match proj_sig_res s with
+ | Tint | Tany32 => One R10
+ | Tfloat | Tsingle | Tany64 => One F10
+ | Tlong => if Archi.ptr64 then One R10 else Twolong R11 R10
end.
(** The result registers have types compatible with that given in the signature. *)
@@ -128,8 +129,8 @@ Lemma loc_result_type:
forall sig,
subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
Proof.
- intros. unfold proj_sig_res, loc_result, mreg_type;
- destruct (sig_res sig) as [[]|]; auto; destruct Archi.ptr64; auto.
+ intros. unfold loc_result, mreg_type;
+ destruct (proj_sig_res sig); auto; destruct Archi.ptr64; auto.
Qed.
(** The result locations are caller-save registers *)
@@ -139,7 +140,7 @@ Lemma loc_result_caller_save:
forall_rpair (fun r => is_callee_save r = false) (loc_result s).
Proof.
intros. unfold loc_result, is_callee_save;
- destruct (sig_res s) as [[]|]; simpl; auto; destruct Archi.ptr64; simpl; auto.
+ destruct (proj_sig_res s); simpl; auto; destruct Archi.ptr64; simpl; auto.
Qed.
(** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
@@ -149,13 +150,13 @@ Lemma loc_result_pair:
match loc_result sg with
| One _ => True
| Twolong r1 r2 =>
- r1 <> r2 /\ sg.(sig_res) = Some Tlong
+ r1 <> r2 /\ proj_sig_res sg = Tlong
/\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
/\ Archi.ptr64 = false
end.
Proof.
intros.
- unfold loc_result; destruct (sig_res sg) as [[]|]; auto.
+ unfold loc_result; destruct (proj_sig_res sg); auto.
unfold mreg_type; destruct Archi.ptr64; auto.
split; auto. congruence.
Qed.
@@ -165,43 +166,37 @@ Qed.
Lemma loc_result_exten:
forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2.
Proof.
- intros. unfold loc_result. rewrite H; auto.
+ intros. unfold loc_result, proj_sig_res. rewrite H; auto.
Qed.
(** ** Location of function arguments *)
-(** The RISC-V ABI states the following convention for passing arguments
+(** The RISC-V ABI states the following conventions for passing arguments
to a function:
-- Arguments are passed in registers when possible.
-
-- Up to eight integer registers (ai: int_param_regs) and up to eight
- floating-point registers (fai: float_param_regs) are used for this
- purpose.
-
-- If the arguments to a function are conceptualized as fields of a C
- struct, each with pointer alignment, the argument registers are a
- shadow of the first eight pointer-words of that struct. If argument
- i < 8 is a floating-point type, it is passed in floating-point
- register fa_i; otherwise, it is passed in integer register a_i.
-
-- When primitive arguments twice the size of a pointer-word are passed
- on the stack, they are naturally aligned. When they are passed in the
- integer registers, they reside in an aligned even-odd register pair,
- with the even register holding the least-significant bits.
-
-- Floating-point arguments to variadic functions (except those that
- are explicitly named in the parameter list) are passed in integer
- registers.
-
-- The portion of the conceptual struct that is not passed in argument
- registers is passed on the stack. The stack pointer sp points to the
- first argument not passed in a register.
-
-The bit about variadic functions doesn't quite fit CompCert's model.
-We do our best by passing the FP arguments in registers, as usual,
-and reserving the corresponding integer registers, so that fixup
-code can be introduced in the Asmexpand pass.
+- RV64, not variadic: pass the first 8 integer arguments in
+ integer registers (a1...a8: int_param_regs), the first 8 FP arguments
+ in FP registers (fa1...fa8: float_param_regs), and the remaining
+ arguments on the stack, in 8-byte slots.
+
+- RV32, not variadic: same, but arguments of 64-bit integer type
+ are passed in two consecutive integer registers (a(i), a(i+1))
+ or in a(8) and on a 32-bit word on the stack. Stack-allocated
+ arguments are aligned to their natural alignment.
+
+- RV64, variadic: pass the first 8 arguments in integer registers
+ (a1...a8), including FP arguments; pass the remaining arguments on
+ the stack, in 8-byte slots.
+
+- RV32, variadic: same, but arguments of 64-bit types (integers as well
+ as floats) are passed in two consecutive aligned integer registers
+ (a(2i), a(2i+1)).
+
+The passing of FP arguments to variadic functions in integer registers
+doesn't quite fit CompCert's model. We do our best by passing the FP
+arguments in registers, as usual, and reserving the corresponding
+integer registers, so that fixup code can be introduced in the
+Asmexpand pass.
*)
Definition int_param_regs :=
@@ -209,80 +204,84 @@ Definition int_param_regs :=
Definition float_param_regs :=
F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: F16 :: F17 :: nil.
-Definition one_arg (regs: list mreg) (rn: Z) (ofs: Z) (ty: typ)
- (rec: Z -> Z -> list (rpair loc)) :=
- match list_nth_z regs rn with
+Definition int_arg (ri rf ofs: Z) (ty: typ)
+ (rec: Z -> Z -> Z -> list (rpair loc)) :=
+ match list_nth_z int_param_regs ri with
| Some r =>
- One(R r) :: rec (rn + 1) ofs
+ One(R r) :: rec (ri + 1) rf ofs
| None =>
let ofs := align ofs (typealign ty) in
- One(S Outgoing ofs ty) :: rec rn (ofs + (if Archi.ptr64 then 2 else typesize ty))
+ One(S Outgoing ofs ty)
+ :: rec ri rf (ofs + (if Archi.ptr64 then 2 else typesize ty))
end.
-Definition two_args (regs: list mreg) (rn: Z) (ofs: Z)
- (rec: Z -> Z -> list (rpair loc)) :=
- let rn := align rn 2 in
- match list_nth_z regs rn, list_nth_z regs (rn + 1) with
- | Some r1, Some r2 =>
- Twolong (R r2) (R r1) :: rec (rn + 2) ofs
- | _, _ =>
- let ofs := align ofs 2 in
- Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) ::
- rec rn (ofs + 2)
+Definition float_arg (va: bool) (ri rf ofs: Z) (ty: typ)
+ (rec: Z -> Z -> Z -> list (rpair loc)) :=
+ match list_nth_z float_param_regs rf with
+ | Some r =>
+ if va then
+ (let ri' := (* reserve 1 or 2 aligned integer registers *)
+ if Archi.ptr64 || zeq (typesize ty) 1 then ri + 1 else align ri 2 + 2 in
+ if zle ri' 8 then
+ (* we have enough integer registers, put argument in FP reg
+ and fixup code will put it in one or two integer regs *)
+ One (R r) :: rec ri' (rf + 1) ofs
+ else
+ (* we are out of integer registers, pass argument on stack *)
+ let ofs := align ofs (typealign ty) in
+ One(S Outgoing ofs ty)
+ :: rec ri' rf (ofs + (if Archi.ptr64 then 2 else typesize ty)))
+ else
+ One (R r) :: rec ri (rf + 1) ofs
+ | None =>
+ let ofs := align ofs (typealign ty) in
+ One(S Outgoing ofs ty)
+ :: rec ri rf (ofs + (if Archi.ptr64 then 2 else typesize ty))
end.
-Definition hybrid_arg (regs: list mreg) (rn: Z) (ofs: Z) (ty: typ)
- (rec: Z -> Z -> list (rpair loc)) :=
- let rn := align rn 2 in
- match list_nth_z regs rn with
- | Some r =>
- One (R r) :: rec (rn + 2) ofs
- | None =>
+Definition split_long_arg (va: bool) (ri rf ofs: Z)
+ (rec: Z -> Z -> Z -> list (rpair loc)) :=
+ let ri := if va then align ri 2 else ri in
+ match list_nth_z int_param_regs ri, list_nth_z int_param_regs (ri + 1) with
+ | Some r1, Some r2 =>
+ Twolong (R r2) (R r1) :: rec (ri + 2) rf ofs
+ | Some r1, None =>
+ Twolong (S Outgoing ofs Tint) (R r1) :: rec (ri + 1) rf (ofs + 1)
+ | None, _ =>
let ofs := align ofs 2 in
- One (S Outgoing ofs ty) :: rec rn (ofs + 2)
+ Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) ::
+ rec ri rf (ofs + 2)
end.
Fixpoint loc_arguments_rec (va: bool)
- (tyl: list typ) (r ofs: Z) {struct tyl} : list (rpair loc) :=
+ (tyl: list typ) (ri rf ofs: Z) {struct tyl} : list (rpair loc) :=
match tyl with
| nil => nil
| (Tint | Tany32) as ty :: tys =>
- one_arg int_param_regs r ofs ty (loc_arguments_rec va tys)
+ (* pass in one integer register or on stack *)
+ int_arg ri rf ofs ty (loc_arguments_rec va tys)
| Tsingle as ty :: tys =>
- one_arg float_param_regs r ofs ty (loc_arguments_rec va tys)
+ (* pass in one FP register or on stack.
+ If vararg, reserve 1 integer register. *)
+ float_arg va ri rf ofs ty (loc_arguments_rec va tys)
| Tlong as ty :: tys =>
- if Archi.ptr64
- then one_arg int_param_regs r ofs ty (loc_arguments_rec va tys)
- else two_args int_param_regs r ofs (loc_arguments_rec va tys)
+ if Archi.ptr64 then
+ (* pass in one integer register or on stack *)
+ int_arg ri rf ofs ty (loc_arguments_rec va tys)
+ else
+ (* pass in register pair or on stack; align register pair if vararg *)
+ split_long_arg va ri rf ofs(loc_arguments_rec va tys)
| (Tfloat | Tany64) as ty :: tys =>
- if va && negb Archi.ptr64
- then hybrid_arg float_param_regs r ofs ty (loc_arguments_rec va tys)
- else one_arg float_param_regs r ofs ty (loc_arguments_rec va tys)
+ (* pass in one FP register or on stack.
+ If vararg, reserve 1 or 2 integer registers. *)
+ float_arg va ri rf ofs ty (loc_arguments_rec va tys)
end.
(** [loc_arguments s] returns the list of locations where to store arguments
when calling a function with signature [s]. *)
Definition loc_arguments (s: signature) : list (rpair loc) :=
- loc_arguments_rec s.(sig_cc).(cc_vararg) s.(sig_args) 0 0.
-
-(** [size_arguments s] returns the number of [Outgoing] slots used
- to call a function with signature [s]. *)
-
-Definition max_outgoing_1 (accu: Z) (l: loc) : Z :=
- match l with
- | S Outgoing ofs ty => Z.max accu (ofs + typesize ty)
- | _ => accu
- end.
-
-Definition max_outgoing_2 (accu: Z) (rl: rpair loc) : Z :=
- match rl with
- | One l => max_outgoing_1 accu l
- | Twolong l1 l2 => max_outgoing_1 (max_outgoing_1 accu l1) l2
- end.
-
-Definition size_arguments (s: signature) : Z :=
- List.fold_left max_outgoing_2 (loc_arguments s) 0.
+ loc_arguments_rec s.(sig_cc).(cc_vararg) s.(sig_args) 0 0 0.
(** Argument locations are either non-temporary registers or [Outgoing]
stack slots at nonnegative offsets. *)
@@ -295,15 +294,18 @@ Definition loc_argument_acceptable (l: loc) : Prop :=
end.
Lemma loc_arguments_rec_charact:
- forall va tyl rn ofs p,
+ forall va tyl ri rf ofs p,
ofs >= 0 ->
- In p (loc_arguments_rec va tyl rn ofs) -> forall_rpair loc_argument_acceptable p.
+ In p (loc_arguments_rec va tyl ri rf ofs) -> forall_rpair loc_argument_acceptable p.
Proof.
set (OK := fun (l: list (rpair loc)) =>
forall p, In p l -> forall_rpair loc_argument_acceptable p).
- set (OKF := fun (f: Z -> Z -> list (rpair loc)) =>
- forall rn ofs, ofs >= 0 -> OK (f rn ofs)).
- set (OKREGS := fun (l: list mreg) => forall r, In r l -> is_callee_save r = false).
+ set (OKF := fun (f: Z -> Z -> Z -> list (rpair loc)) =>
+ forall ri rf ofs, ofs >= 0 -> OK (f ri rf ofs)).
+ assert (CSI: forall r, In r int_param_regs -> is_callee_save r = false).
+ { decide_goal. }
+ assert (CSF: forall r, In r float_param_regs -> is_callee_save r = false).
+ { decide_goal. }
assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typealign ty) >= 0).
{ intros.
assert (ofs <= align ofs (typealign ty)) by (apply align_le; apply typealign_pos).
@@ -312,73 +314,64 @@ Proof.
{ destruct Archi.ptr64; omega. }
assert (SKK: forall ty, (if Archi.ptr64 then 2 else typesize ty) > 0).
{ intros. destruct Archi.ptr64. omega. apply typesize_pos. }
- assert (A: forall regs rn ofs ty f,
- OKREGS regs -> OKF f -> ofs >= 0 -> OK (one_arg regs rn ofs ty f)).
- { intros until f; intros OR OF OO; red; unfold one_arg; intros.
- destruct (list_nth_z regs rn) as [r|] eqn:NTH; destruct H.
- - subst p; simpl. apply OR. eapply list_nth_z_in; eauto.
+ assert (A: forall ri rf ofs ty f,
+ OKF f -> ofs >= 0 -> OK (int_arg ri rf ofs ty f)).
+ { intros until f; intros OF OO; red; unfold int_arg; intros.
+ destruct (list_nth_z int_param_regs ri) as [r|] eqn:NTH; destruct H.
+ - subst p; simpl. apply CSI. eapply list_nth_z_in; eauto.
- eapply OF; eauto.
- subst p; simpl. auto using align_divides, typealign_pos.
- eapply OF; [idtac|eauto].
generalize (AL ofs ty OO) (SKK ty); omega.
}
- assert (B: forall regs rn ofs f,
- OKREGS regs -> OKF f -> ofs >= 0 -> OK (two_args regs rn ofs f)).
- { intros until f; intros OR OF OO; unfold two_args.
- set (rn' := align rn 2).
+ assert (B: forall va ri rf ofs ty f,
+ OKF f -> ofs >= 0 -> OK (float_arg va ri rf ofs ty f)).
+ { intros until f; intros OF OO; red; unfold float_arg; intros.
+ destruct (list_nth_z float_param_regs rf) as [r|] eqn:NTH.
+ - set (ri' := if Archi.ptr64 || zeq (typesize ty) 1 then ri + 1 else align ri 2 + 2) in *.
+ destruct va; [destruct (zle ri' 8)|idtac]; destruct H.
+ + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto.
+ + eapply OF; eauto.
+ + subst p; repeat split; auto using align_divides, typealign_pos.
+ + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega.
+ + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto.
+ + eapply OF; eauto.
+ - destruct H.
+ + subst p; repeat split; auto using align_divides, typealign_pos.
+ + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega.
+ }
+ assert (C: forall va ri rf ofs f,
+ OKF f -> ofs >= 0 -> OK (split_long_arg va ri rf ofs f)).
+ { intros until f; intros OF OO; unfold split_long_arg.
+ set (ri' := if va then align ri 2 else ri).
set (ofs' := align ofs 2).
assert (OO': ofs' >= 0) by (apply (AL ofs Tlong); auto).
- assert (DFL: OK (Twolong (S Outgoing (ofs' + 1) Tint) (S Outgoing ofs' Tint)
- :: f rn' (ofs' + 2))).
- { red; simpl; intros. destruct H.
- - subst p; simpl.
- repeat split; auto using Z.divide_1_l. omega.
- - eapply OF; [idtac|eauto]. omega.
- }
- destruct (list_nth_z regs rn') as [r1|] eqn:NTH1;
- destruct (list_nth_z regs (rn' + 1)) as [r2|] eqn:NTH2;
- try apply DFL.
- red; simpl; intros; destruct H.
- - subst p; simpl. split; apply OR; eauto using list_nth_z_in.
- - eapply OF; [idtac|eauto]. auto.
- }
- assert (C: forall regs rn ofs ty f,
- OKREGS regs -> OKF f -> ofs >= 0 -> typealign ty = 1 -> OK (hybrid_arg regs rn ofs ty f)).
- { intros until f; intros OR OF OO OTY; unfold hybrid_arg; red; intros.
- set (rn' := align rn 2) in *.
- destruct (list_nth_z regs rn') as [r|] eqn:NTH; destruct H.
- - subst p; simpl. apply OR. eapply list_nth_z_in; eauto.
- - eapply OF; eauto.
- - subst p; simpl. rewrite OTY. split. apply (AL ofs Tlong OO). apply Z.divide_1_l.
- - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); simpl; omega.
+ destruct (list_nth_z int_param_regs ri') as [r1|] eqn:NTH1;
+ [destruct (list_nth_z int_param_regs (ri'+1)) as [r2|] eqn:NTH2 | idtac].
+ - red; simpl; intros; destruct H.
+ + subst p; split; apply CSI; eauto using list_nth_z_in.
+ + eapply OF; [idtac|eauto]. omega.
+ - red; simpl; intros; destruct H.
+ + subst p; split. split; auto using Z.divide_1_l. apply CSI; eauto using list_nth_z_in.
+ + eapply OF; [idtac|eauto]. omega.
+ - red; simpl; intros; destruct H.
+ + subst p; repeat split; auto using Z.divide_1_l. omega.
+ + eapply OF; [idtac|eauto]. omega.
}
- assert (D: OKREGS int_param_regs).
- { red. decide_goal. }
- assert (E: OKREGS float_param_regs).
- { red. decide_goal. }
-
- cut (forall va tyl rn ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl rn ofs)).
+ cut (forall va tyl ri rf ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl ri rf ofs)).
unfold OK. eauto.
induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl.
- red; simpl; tauto.
- destruct ty1.
+ (* int *) apply A; auto.
-+ (* float *)
- destruct (va && negb Archi.ptr64).
- apply C; auto.
- apply A; auto.
++ (* float *) apply B; auto.
+ (* long *)
destruct Archi.ptr64.
apply A; auto.
- apply B; auto.
-+ (* single *)
- apply A; auto.
-+ (* any32 *)
- apply A; auto.
-+ (* any64 *)
- destruct (va && negb Archi.ptr64).
apply C; auto.
- apply A; auto.
++ (* single *) apply B; auto.
++ (* any32 *) apply A; auto.
++ (* any64 *) apply B; auto.
Qed.
Lemma loc_arguments_acceptable:
@@ -388,54 +381,14 @@ Proof.
unfold loc_arguments; intros. eapply loc_arguments_rec_charact; eauto. omega.
Qed.
-(** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
-
-Remark fold_max_outgoing_above:
- forall l n, fold_left max_outgoing_2 l n >= n.
-Proof.
- assert (A: forall n l, max_outgoing_1 n l >= n).
- { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. }
- induction l; simpl; intros.
- - omega.
- - eapply Zge_trans. eauto.
- destruct a; simpl. apply A. eapply Zge_trans; eauto.
-Qed.
-
-Lemma size_arguments_above:
- forall s, size_arguments s >= 0.
-Proof.
- intros. apply fold_max_outgoing_above.
-Qed.
-
-Lemma loc_arguments_bounded:
- forall (s: signature) (ofs: Z) (ty: typ),
- In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) ->
- ofs + typesize ty <= size_arguments s.
-Proof.
- intros until ty.
- assert (A: forall n l, n <= max_outgoing_1 n l).
- { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. }
- assert (B: forall p n,
- In (S Outgoing ofs ty) (regs_of_rpair p) ->
- ofs + typesize ty <= max_outgoing_2 n p).
- { intros. destruct p; simpl in H; intuition; subst; simpl.
- - xomega.
- - eapply Z.le_trans. 2: apply A. xomega.
- - xomega. }
- assert (C: forall l n,
- In (S Outgoing ofs ty) (regs_of_rpairs l) ->
- ofs + typesize ty <= fold_left max_outgoing_2 l n).
- { induction l; simpl; intros.
- - contradiction.
- - rewrite in_app_iff in H. destruct H.
- + eapply Z.le_trans. eapply B; eauto. apply Z.ge_le. apply fold_max_outgoing_above.
- + apply IHl; auto.
- }
- apply C.
-Qed.
-
Lemma loc_arguments_main:
loc_arguments signature_main = nil.
Proof.
reflexivity.
Qed.
+
+(** ** Normalization of function results *)
+
+(** No normalization needed. *)
+
+Definition return_value_needs_normalization (t: rettype) := false.
diff --git a/test/cse2/globals.c b/test/cse2/globals.c
new file mode 100644
index 00000000..c6dd59cd
--- /dev/null
+++ b/test/cse2/globals.c
@@ -0,0 +1,8 @@
+int glob1, glob2;
+
+void toto() {
+ if (glob1 > 4) {
+ glob2 ++;
+ glob1 --;
+ }
+}
diff --git a/test/cse2/indexed_addr.c b/test/cse2/indexed_addr.c
new file mode 100644
index 00000000..30a7c571
--- /dev/null
+++ b/test/cse2/indexed_addr.c
@@ -0,0 +1,6 @@
+void foo(int *t) {
+ if (t[0] > 4) {
+ t[1] ++;
+ t[0] --;
+ }
+}
diff --git a/test/monniaux/cycles.h b/test/monniaux/cycles.h
index 21541145..4a87299b 100644
--- a/test/monniaux/cycles.h
+++ b/test/monniaux/cycles.h
@@ -38,6 +38,13 @@ static inline cycle_t get_cycle(void) {
return cycles;
}
+#elif defined (__ARM_ARCH) && (__ARM_ARCH >= 6)
+static inline cycle_t get_cycle(void) {
+ cycle_t cycles;
+ __asm__ volatile ("mrc p15, 0, %0, c9, c13, 0":"=r" (cycles));
+ return cycles;
+}
+
#else
static inline cycle_t get_cycle(void) { return 0; }
#endif
diff --git a/test/regression/Results/interop1 b/test/regression/Results/interop1
index 990dfe9d..6e32c1cb 100644
--- a/test/regression/Results/interop1
+++ b/test/regression/Results/interop1
@@ -1,4 +1,8 @@
--- CompCert calling native:
+si8u: 177
+si8s: -79
+si16u: 64305
+si16s: -1231
s1: { a = 'a' }
s2: { a = 'a', b = 'b' }
s3: { a = 'a', b = 'b', c = ' c' }
@@ -44,6 +48,10 @@ ru6: { a = 55555, b = 666 }
ru7: { a = -10001, b = -789, c = 'z' }
ru8: { a = 'x', b = 12345 }
--- native calling CompCert:
+si8u: 177
+si8s: -79
+si16u: 64305
+si16s: -1231
s1: { a = 'a' }
s2: { a = 'a', b = 'b' }
s3: { a = 'a', b = 'b', c = ' c' }
diff --git a/test/regression/interop1.c b/test/regression/interop1.c
index a39f449c..6836b89e 100644
--- a/test/regression/interop1.c
+++ b/test/regression/interop1.c
@@ -195,6 +195,17 @@ RETURN(ru6,U6,init_U6)
RETURN(ru7,U7,init_U7)
RETURN(ru8,U8,init_U8)
+/* Returning small integers */
+
+#define SMALLINT(name,ty) \
+extern ty THEM(name)(int); \
+ty US(name)(int x) { return x * x; }
+
+SMALLINT(si8u, unsigned char)
+SMALLINT(si8s, signed char)
+SMALLINT(si16u, unsigned short)
+SMALLINT(si16s, signed short)
+
/* Test function, calling the functions compiled by the other compiler */
#define CALLPRINT(name,ty,init) \
@@ -207,6 +218,10 @@ RETURN(ru8,U8,init_U8)
extern void THEM(test) (void);
void US(test) (void)
{
+ printf("si8u: %d\n", THEM(si8u)(12345));
+ printf("si8s: %d\n", THEM(si8s)(12345));
+ printf("si16u: %d\n", THEM(si16u)(1234567));
+ printf("si16s: %d\n", THEM(si16s)(1234567));
CALLPRINT(s1,S1,init_S1)
CALLPRINT(s2,S2,init_S2)
CALLPRINT(s3,S3,init_S3)
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index 16426ce3..b8353046 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -251,7 +251,7 @@ let expand_builtin_va_start_32 r =
invalid_arg "Fatal error: va_start used in non-vararg function";
let ofs =
Int32.(add (add !PrintAsmaux.current_function_stacksize 4l)
- (mul 4l (Z.to_int32 (Conventions1.size_arguments
+ (mul 4l (Z.to_int32 (Conventions.size_arguments
(get_current_function_sig ()))))) in
emit (Pleal (RAX, linear_addr RSP (Z.of_uint32 ofs)));
emit (Pmovl_mr (linear_addr r _0z, RAX))
@@ -506,7 +506,7 @@ let expand_instruction instr =
(* Save the registers *)
emit (Pleaq (R10, linear_addr RSP (Z.of_uint save_regs)));
emit (Pcall_s (intern_string "__compcert_va_saveregs",
- {sig_args = []; sig_res = None; sig_cc = cc_default}))
+ {sig_args = []; sig_res = Tvoid; sig_cc = cc_default}))
end;
(* Stack chaining *)
let fullsz = sz + 8 in
diff --git a/x86/Builtins1.v b/x86/Builtins1.v
index 6103cc4c..f1d60961 100644
--- a/x86/Builtins1.v
+++ b/x86/Builtins1.v
@@ -33,10 +33,10 @@ Definition platform_builtin_table : list (string * platform_builtin) :=
Definition platform_builtin_sig (b: platform_builtin) : signature :=
match b with
| BI_fmin | BI_fmax =>
- mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default
+ mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default
end.
-Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
+Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
match b with
| BI_fmin =>
mkbuiltin_n2t Tfloat Tfloat Tfloat
diff --git a/x86/CSE2deps.v b/x86/CSE2deps.v
new file mode 100644
index 00000000..f4d9e254
--- /dev/null
+++ b/x86/CSE2deps.v
@@ -0,0 +1,24 @@
+Require Import BoolEqual Coqlib.
+Require Import AST Integers Floats.
+Require Import Values Memory Globalenvs Events.
+Require Import Op.
+
+Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
+ (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk))
+ && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk))
+ && ((ofsw + size_chunk chunkw <=? ofsr) ||
+ (ofsr + size_chunk chunkr <=? ofsw)).
+
+Definition may_overlap chunk addr args chunk' addr' args' :=
+ match addr, addr', args, args' with
+ | (Aindexed ofs), (Aindexed ofs'),
+ (base :: nil), (base' :: nil) =>
+ if peq base base'
+ then negb (can_swap_accesses_ofs ofs' chunk' ofs chunk)
+ else true
+ | (Aglobal symb ofs), (Aglobal symb' ofs'), nil, nil =>
+ if peq symb symb'
+ then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk)
+ else false
+ | _, _, _, _ => true
+ end.
diff --git a/x86/CSE2depsproof.v b/x86/CSE2depsproof.v
new file mode 100644
index 00000000..1e913254
--- /dev/null
+++ b/x86/CSE2depsproof.v
@@ -0,0 +1,253 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Maps.
+
+Require Import Globalenvs Values.
+Require Import Linking Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import CSE2 CSE2deps.
+Require Import Lia.
+
+Section SOUNDNESS.
+ Variable F V : Type.
+ Variable genv: Genv.t F V.
+ Variable sp : val.
+
+Section MEMORY_WRITE.
+ Variable m m2 : mem.
+ Variable chunkw chunkr : memory_chunk.
+ Variable base : val.
+
+ Variable addrw addrr valw : val.
+ Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
+
+ Section INDEXED_AWAY.
+ Variable ofsw ofsr : Z.
+ Hypothesis ADDRW : eval_addressing genv sp
+ (Aindexed ofsw) (base :: nil) = Some addrw.
+ Hypothesis ADDRR : eval_addressing genv sp
+ (Aindexed ofsr) (base :: nil) = Some addrr.
+
+ Lemma load_store_away1 :
+ forall RANGEW : 0 <= ofsw <= Ptrofs.modulus - largest_size_chunk,
+ forall RANGER : 0 <= ofsr <= Ptrofs.modulus - largest_size_chunk,
+ forall SWAPPABLE : ofsw + size_chunk chunkw <= ofsr
+ \/ ofsr + size_chunk chunkr <= ofsw,
+ Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+ Proof.
+ intros.
+
+ pose proof (max_size_chunk chunkr) as size_chunkr_bounded.
+ pose proof (max_size_chunk chunkw) as size_chunkw_bounded.
+ try change (Ptrofs.modulus - largest_size_chunk) with 4294967288 in *.
+ try change (Ptrofs.modulus - largest_size_chunk) with 18446744073709551608 in *.
+ destruct addrr ; simpl in * ; trivial.
+ unfold eval_addressing, eval_addressing32, eval_addressing64 in *.
+ destruct Archi.ptr64 eqn:PTR64; destruct base; simpl in *; try discriminate.
+ rewrite PTR64 in *.
+
+ inv ADDRR.
+ inv ADDRW.
+ eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
+ exact STORE.
+ right.
+
+ all: try (destruct (Ptrofs.unsigned_add_either i0
+ (Ptrofs.of_int (Int.repr ofsr))) as [OFSR | OFSR];
+ rewrite OFSR).
+ all: try (destruct (Ptrofs.unsigned_add_either i0
+ (Ptrofs.of_int64 (Int64.repr ofsr))) as [OFSR | OFSR];
+ rewrite OFSR).
+ all: try (destruct (Ptrofs.unsigned_add_either i0
+ (Ptrofs.of_int (Int.repr ofsw))) as [OFSW | OFSW];
+ rewrite OFSW).
+ all: try (destruct (Ptrofs.unsigned_add_either i0
+ (Ptrofs.of_int64 (Int64.repr ofsw))) as [OFSW | OFSW];
+ rewrite OFSW).
+
+ all: unfold Ptrofs.of_int64.
+ all: unfold Ptrofs.of_int.
+
+
+ all: repeat rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia).
+ all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 4294967295; lia).
+ all: repeat rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; lia).
+ all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 18446744073709551615; lia).
+
+ all: try change Ptrofs.modulus with 4294967296.
+ all: try change Ptrofs.modulus with 18446744073709551616.
+
+ all: intuition lia.
+ Qed.
+
+ Theorem load_store_away :
+ can_swap_accesses_ofs ofsr chunkr ofsw chunkw = true ->
+ Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+ Proof.
+ intro SWAP.
+ unfold can_swap_accesses_ofs in SWAP.
+ repeat rewrite andb_true_iff in SWAP.
+ repeat rewrite orb_true_iff in SWAP.
+ repeat rewrite Z.leb_le in SWAP.
+ apply load_store_away1.
+ all: tauto.
+ Qed.
+ End INDEXED_AWAY.
+
+ Section DIFFERENT_GLOBALS.
+ Variable ofsw ofsr : ptrofs.
+ Hypothesis symw symr : ident.
+ Hypothesis ADDRW : eval_addressing genv sp
+ (Aglobal symw ofsw) nil = Some addrw.
+ Hypothesis ADDRR : eval_addressing genv sp
+ (Aglobal symr ofsr) nil = Some addrr.
+
+ Lemma ptr64_cases:
+ forall {T : Type},
+ forall b : bool,
+ forall x y : T,
+ (if b then (if b then x else y) else (if b then y else x)) = x.
+ Proof.
+ destruct b; reflexivity.
+ Qed.
+
+ (* not needed
+ Lemma bool_cases_same:
+ forall {T : Type},
+ forall b : bool,
+ forall x : T,
+ (if b then x else x) = x.
+ Proof.
+ destruct b; reflexivity.
+ Qed.
+ *)
+
+ Lemma load_store_diff_globals :
+ symw <> symr ->
+ Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+ Proof.
+ intros.
+ unfold eval_addressing in *.
+ simpl in *.
+ rewrite ptr64_cases in ADDRR.
+ rewrite ptr64_cases in ADDRW.
+ unfold Genv.symbol_address in *.
+ unfold Genv.find_symbol in *.
+ destruct ((Genv.genv_symb genv) ! symw) as [bw |] eqn:SYMW; inv ADDRW.
+ 2: simpl in STORE; discriminate.
+ destruct ((Genv.genv_symb genv) ! symr) as [br |] eqn:SYMR; inv ADDRR.
+ 2: reflexivity.
+ assert (br <> bw).
+ {
+ intro EQ.
+ subst br.
+ assert (symr = symw).
+ {
+ eapply Genv.genv_vars_inj; eauto.
+ }
+ congruence.
+ }
+ eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := bw).
+ - exact STORE.
+ - left. assumption.
+ Qed.
+ End DIFFERENT_GLOBALS.
+
+ Section SAME_GLOBALS.
+ Variable ofsw ofsr : ptrofs.
+ Hypothesis sym : ident.
+ Hypothesis ADDRW : eval_addressing genv sp
+ (Aglobal sym ofsw) nil = Some addrw.
+ Hypothesis ADDRR : eval_addressing genv sp
+ (Aglobal sym ofsr) nil = Some addrr.
+
+ Lemma load_store_glob_away1 :
+ forall RANGEW : 0 <= (Ptrofs.unsigned ofsw) <= Ptrofs.modulus - largest_size_chunk,
+ forall RANGER : 0 <= (Ptrofs.unsigned ofsr) <= Ptrofs.modulus - largest_size_chunk,
+ forall SWAPPABLE : (Ptrofs.unsigned ofsw) + size_chunk chunkw <= (Ptrofs.unsigned ofsr)
+ \/ (Ptrofs.unsigned ofsr) + size_chunk chunkr <= (Ptrofs.unsigned ofsw),
+ Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+ Proof.
+ intros.
+
+ pose proof (max_size_chunk chunkr) as size_chunkr_bounded.
+ pose proof (max_size_chunk chunkw) as size_chunkw_bounded.
+ unfold largest_size_chunk in size_chunkr_bounded, size_chunkw_bounded.
+ try change (Ptrofs.modulus - largest_size_chunk) with 4294967288 in *.
+ try change (Ptrofs.modulus - largest_size_chunk) with 18446744073709551608 in *.
+ unfold eval_addressing, eval_addressing32, eval_addressing64 in *.
+
+ rewrite ptr64_cases in ADDRR.
+ rewrite ptr64_cases in ADDRW.
+ unfold Genv.symbol_address in *.
+ inv ADDRR.
+ inv ADDRW.
+ destruct (Genv.find_symbol genv sym).
+ 2: discriminate.
+
+ eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
+ exact STORE.
+ right.
+ tauto.
+ Qed.
+
+ Lemma load_store_glob_away :
+ (can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw) = true ->
+ Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+ Proof.
+ intro SWAP.
+ unfold can_swap_accesses_ofs in SWAP.
+ repeat rewrite andb_true_iff in SWAP.
+ repeat rewrite orb_true_iff in SWAP.
+ repeat rewrite Z.leb_le in SWAP.
+ apply load_store_glob_away1.
+ all: tauto.
+ Qed.
+ End SAME_GLOBALS.
+End MEMORY_WRITE.
+End SOUNDNESS.
+
+
+Section SOUNDNESS.
+ Variable F V : Type.
+ Variable genv: Genv.t F V.
+ Variable sp : val.
+
+Lemma may_overlap_sound:
+ forall m m' : mem,
+ forall chunk addr args chunk' addr' args' v a a' rs,
+ (eval_addressing genv sp addr (rs ## args)) = Some a ->
+ (eval_addressing genv sp addr' (rs ## args')) = Some a' ->
+ (may_overlap chunk addr args chunk' addr' args') = false ->
+ (Mem.storev chunk m a v) = Some m' ->
+ (Mem.loadv chunk' m' a') = (Mem.loadv chunk' m a').
+Proof.
+ intros until rs.
+ intros ADDR ADDR' OVERLAP STORE.
+ destruct addr; destruct addr'; try discriminate.
+ { (* Aindexed / Aindexed *)
+ destruct args as [ | base [ | ]]. 1,3: discriminate.
+ destruct args' as [ | base' [ | ]]. 1,3: discriminate.
+ simpl in OVERLAP.
+ destruct (peq base base'). 2: discriminate.
+ subst base'.
+ destruct (can_swap_accesses_ofs z0 chunk' z chunk) eqn:SWAP.
+ 2: discriminate.
+ simpl in *.
+ eapply load_store_away; eassumption.
+ }
+ { (* Aglobal / Aglobal *)
+ destruct args. 2: discriminate.
+ destruct args'. 2: discriminate.
+ simpl in *.
+ destruct (peq i i1).
+ {
+ subst i1.
+ rewrite negb_false_iff in OVERLAP.
+ eapply load_store_glob_away; eassumption.
+ }
+ eapply load_store_diff_globals; eassumption.
+ }
+Qed.
+
+End SOUNDNESS.
diff --git a/x86/Conventions1.v b/x86/Conventions1.v
index 35d555f9..d9f5b8fa 100644
--- a/x86/Conventions1.v
+++ b/x86/Conventions1.v
@@ -100,22 +100,20 @@ Definition is_float_reg (r: mreg) :=
function with one integer result. *)
Definition loc_result_32 (s: signature) : rpair mreg :=
- match s.(sig_res) with
- | None => One AX
- | Some (Tint | Tany32) => One AX
- | Some (Tfloat | Tsingle) => One FP0
- | Some Tany64 => One X0
- | Some Tlong => Twolong DX AX
+ match proj_sig_res s with
+ | Tint | Tany32 => One AX
+ | Tfloat | Tsingle => One FP0
+ | Tany64 => One X0
+ | Tlong => Twolong DX AX
end.
(** In 64 bit mode, he result value of a function is passed back to
the caller in registers [AX] or [X0]. *)
Definition loc_result_64 (s: signature) : rpair mreg :=
- match s.(sig_res) with
- | None => One AX
- | Some (Tint | Tlong | Tany32 | Tany64) => One AX
- | Some (Tfloat | Tsingle) => One X0
+ match proj_sig_res s with
+ | Tint | Tlong | Tany32 | Tany64 => One AX
+ | Tfloat | Tsingle => One X0
end.
Definition loc_result :=
@@ -127,8 +125,8 @@ Lemma loc_result_type:
forall sig,
subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
Proof.
- intros. unfold proj_sig_res, loc_result, loc_result_32, loc_result_64, mreg_type;
- destruct Archi.ptr64; destruct (sig_res sig) as [[]|]; auto.
+ intros. unfold loc_result, loc_result_32, loc_result_64, mreg_type;
+ destruct Archi.ptr64; destruct (proj_sig_res sig); auto.
Qed.
(** The result locations are caller-save registers *)
@@ -138,7 +136,7 @@ Lemma loc_result_caller_save:
forall_rpair (fun r => is_callee_save r = false) (loc_result s).
Proof.
intros. unfold loc_result, loc_result_32, loc_result_64, is_callee_save;
- destruct Archi.ptr64; destruct (sig_res s) as [[]|]; simpl; auto.
+ destruct Archi.ptr64; destruct (proj_sig_res s); simpl; auto.
Qed.
(** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
@@ -148,14 +146,14 @@ Lemma loc_result_pair:
match loc_result sg with
| One _ => True
| Twolong r1 r2 =>
- r1 <> r2 /\ sg.(sig_res) = Some Tlong
+ r1 <> r2 /\ proj_sig_res sg = Tlong
/\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
/\ Archi.ptr64 = false
end.
Proof.
intros.
unfold loc_result, loc_result_32, loc_result_64, mreg_type;
- destruct Archi.ptr64; destruct (sig_res sg) as [[]|]; auto.
+ destruct Archi.ptr64; destruct (proj_sig_res sg); auto.
split; auto. congruence.
Qed.
@@ -164,7 +162,7 @@ Qed.
Lemma loc_result_exten:
forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2.
Proof.
- intros. unfold loc_result, loc_result_32, loc_result_64.
+ intros. unfold loc_result, loc_result_32, loc_result_64, proj_sig_res.
destruct Archi.ptr64; rewrite H; auto.
Qed.
@@ -223,36 +221,6 @@ Definition loc_arguments (s: signature) : list (rpair loc) :=
then loc_arguments_64 s.(sig_args) 0 0 0
else loc_arguments_32 s.(sig_args) 0.
-(** [size_arguments s] returns the number of [Outgoing] slots used
- to call a function with signature [s]. *)
-
-Fixpoint size_arguments_32
- (tyl: list typ) (ofs: Z) {struct tyl} : Z :=
- match tyl with
- | nil => ofs
- | ty :: tys => size_arguments_32 tys (ofs + typesize ty)
- end.
-
-Fixpoint size_arguments_64 (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z :=
- match tyl with
- | nil => ofs
- | (Tint | Tlong | Tany32 | Tany64) :: tys =>
- match list_nth_z int_param_regs ir with
- | None => size_arguments_64 tys ir fr (ofs + 2)
- | Some ireg => size_arguments_64 tys (ir + 1) fr ofs
- end
- | (Tfloat | Tsingle) :: tys =>
- match list_nth_z float_param_regs fr with
- | None => size_arguments_64 tys ir fr (ofs + 2)
- | Some freg => size_arguments_64 tys ir (fr + 1) ofs
- end
- end.
-
-Definition size_arguments (s: signature) : Z :=
- if Archi.ptr64
- then size_arguments_64 s.(sig_args) 0 0 0
- else size_arguments_32 s.(sig_args) 0.
-
(** Argument locations are either caller-save registers or [Outgoing]
stack slots at nonnegative offsets. *)
@@ -354,123 +322,22 @@ Qed.
Hint Resolve loc_arguments_acceptable: locs.
-(** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
-
-Remark size_arguments_32_above:
- forall tyl ofs0, ofs0 <= size_arguments_32 tyl ofs0.
+Lemma loc_arguments_main:
+ loc_arguments signature_main = nil.
Proof.
- induction tyl; simpl; intros.
- omega.
- apply Z.le_trans with (ofs0 + typesize a); auto.
- generalize (typesize_pos a); omega.
+ unfold loc_arguments; destruct Archi.ptr64; reflexivity.
Qed.
-Remark size_arguments_64_above:
- forall tyl ir fr ofs0,
- ofs0 <= size_arguments_64 tyl ir fr ofs0.
-Proof.
- induction tyl; simpl; intros.
- omega.
- assert (A: ofs0 <=
- match list_nth_z int_param_regs ir with
- | Some _ => size_arguments_64 tyl (ir + 1) fr ofs0
- | None => size_arguments_64 tyl ir fr (ofs0 + 2)
- end).
- { destruct (list_nth_z int_param_regs ir); eauto.
- apply Z.le_trans with (ofs0 + 2); auto. omega. }
- assert (B: ofs0 <=
- match list_nth_z float_param_regs fr with
- | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0
- | None => size_arguments_64 tyl ir fr (ofs0 + 2)
- end).
- { destruct (list_nth_z float_param_regs fr); eauto.
- apply Z.le_trans with (ofs0 + 2); auto. omega. }
- destruct a; auto.
-Qed.
+(** ** Normalization of function results *)
-Lemma size_arguments_above:
- forall s, size_arguments s >= 0.
-Proof.
- intros; unfold size_arguments. apply Z.le_ge.
- destruct Archi.ptr64; [apply size_arguments_64_above|apply size_arguments_32_above].
-Qed.
+(** 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. *)
-Lemma loc_arguments_32_bounded:
- forall ofs ty tyl ofs0,
- In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_32 tyl ofs0)) ->
- ofs + typesize ty <= size_arguments_32 tyl ofs0.
-Proof.
- induction tyl as [ | t l]; simpl; intros x IN.
-- contradiction.
-- rewrite in_app_iff in IN; destruct IN as [IN|IN].
-+ apply Z.le_trans with (x + typesize t); [|apply size_arguments_32_above].
- Ltac decomp :=
- match goal with
- | [ H: _ \/ _ |- _ ] => destruct H; decomp
- | [ H: S _ _ _ = S _ _ _ |- _ ] => inv H
- | [ H: False |- _ ] => contradiction
+Definition return_value_needs_normalization (t: rettype) : bool :=
+ match t with
+ | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true
+ | _ => false
end.
- destruct t; simpl in IN; decomp; simpl; omega.
-+ apply IHl; auto.
-Qed.
-
-Lemma loc_arguments_64_bounded:
- forall ofs ty tyl ir fr ofs0,
- In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_64 tyl ir fr ofs0)) ->
- ofs + typesize ty <= size_arguments_64 tyl ir fr ofs0.
-Proof.
- induction tyl; simpl; intros.
- contradiction.
- assert (T: forall ty0, typesize ty0 <= 2).
- { destruct ty0; simpl; omega. }
- assert (A: forall ty0,
- In (S Outgoing ofs ty) (regs_of_rpairs
- match list_nth_z int_param_regs ir with
- | Some ireg =>
- One (R ireg) :: loc_arguments_64 tyl (ir + 1) fr ofs0
- | None => One (S Outgoing ofs0 ty0) :: loc_arguments_64 tyl ir fr (ofs0 + 2)
- end) ->
- ofs + typesize ty <=
- match list_nth_z int_param_regs ir with
- | Some _ => size_arguments_64 tyl (ir + 1) fr ofs0
- | None => size_arguments_64 tyl ir fr (ofs0 + 2)
- end).
- { intros. destruct (list_nth_z int_param_regs ir); simpl in H0; destruct H0.
- - discriminate.
- - eapply IHtyl; eauto.
- - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.
- - eapply IHtyl; eauto. }
- assert (B: forall ty0,
- In (S Outgoing ofs ty) (regs_of_rpairs
- match list_nth_z float_param_regs fr with
- | Some ireg =>
- One (R ireg) :: loc_arguments_64 tyl ir (fr + 1) ofs0
- | None => One (S Outgoing ofs0 ty0) :: loc_arguments_64 tyl ir fr (ofs0 + 2)
- end) ->
- ofs + typesize ty <=
- match list_nth_z float_param_regs fr with
- | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0
- | None => size_arguments_64 tyl ir fr (ofs0 + 2)
- end).
- { intros. destruct (list_nth_z float_param_regs fr); simpl in H0; destruct H0.
- - discriminate.
- - eapply IHtyl; eauto.
- - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.
- - eapply IHtyl; eauto. }
- destruct a; eauto.
-Qed.
-
-Lemma loc_arguments_bounded:
- forall (s: signature) (ofs: Z) (ty: typ),
- In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) ->
- ofs + typesize ty <= size_arguments s.
-Proof.
- unfold loc_arguments, size_arguments; intros.
- destruct Archi.ptr64; eauto using loc_arguments_32_bounded, loc_arguments_64_bounded.
-Qed.
-
-Lemma loc_arguments_main:
- loc_arguments signature_main = nil.
-Proof.
- unfold loc_arguments; destruct Archi.ptr64; reflexivity.
-Qed.