summaryrefslogtreecommitdiff
path: root/arm
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-04-20 07:54:52 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-04-20 07:54:52 +0000
commit255cee09b71255051c2b40eae0c88bffce1f6f32 (patch)
tree7951b1b13e8fd5e525b9223e8be0580e83550f55 /arm
parent6e5041958df01c56762e90770abd704b95a36e5d (diff)
Big merge of the newregalloc-int64 branch. Lots of changes in two directions:
1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm')
-rw-r--r--arm/Asm.v86
-rw-r--r--arm/Asmgen.v32
-rw-r--r--arm/Asmgenproof.v79
-rw-r--r--arm/Asmgenproof1.v44
-rw-r--r--arm/ConstpropOp.vp4
-rw-r--r--arm/ConstpropOpproof.v5
-rw-r--r--arm/Machregs.v105
-rw-r--r--arm/Machregsaux.ml9
-rw-r--r--arm/Op.v45
-rw-r--r--arm/PrintAsm.ml161
-rw-r--r--arm/PrintOp.ml4
-rw-r--r--arm/SelectOp.vp6
-rw-r--r--arm/SelectOpproof.v22
-rw-r--r--arm/linux/Conventions1.v337
-rw-r--r--arm/linux/Stacklayout.v83
15 files changed, 540 insertions, 482 deletions
diff --git a/arm/Asm.v b/arm/Asm.v
index cad7188..60dae47 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -141,6 +141,7 @@ Inductive instruction : Type :=
| Pldrh: ireg -> ireg -> shift_addr -> instruction (**r unsigned int16 load *)
| Pldrsb: ireg -> ireg -> shift_addr -> instruction (**r signed int8 load *)
| Pldrsh: ireg -> ireg -> shift_addr -> instruction (**r unsigned int16 load *)
+ | Pmla: ireg -> ireg -> ireg -> ireg -> instruction (**r integer multiply-add *)
| Pmov: ireg -> shift_op -> instruction (**r integer move *)
| Pmovc: crbit -> ireg -> shift_op -> instruction (**r integer conditional move *)
| Pmul: ireg -> ireg -> ireg -> instruction (**r integer multiplication *)
@@ -180,7 +181,7 @@ Inductive instruction : Type :=
| Plabel: label -> instruction (**r define a code label *)
| Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *)
| Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *)
- | Pbuiltin: external_function -> list preg -> preg -> instruction (**r built-in function *)
+ | Pbuiltin: external_function -> list preg -> list preg -> instruction (**r built-in function *)
| Pannot: external_function -> list annot_param -> instruction (**r annotation statement *)
with annot_param : Type :=
@@ -261,6 +262,14 @@ Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
| r :: l' => undef_regs l' (rs#r <- Vundef)
end.
+(** Assigning multiple registers *)
+
+Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset :=
+ match rl, vl with
+ | r1 :: rl', v1 :: vl' => set_regs rl' vl' (rs#r1 <- v1)
+ | _, _ => rs
+ end.
+
Section RELSEM.
(** Looking up instructions in a code sequence by position. *)
@@ -461,6 +470,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
exec_load Mint8signed (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m
| Pldrsh r1 r2 sa =>
exec_load Mint16signed (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m
+ | Pmla r1 r2 r3 r4 =>
+ Next (nextinstr (rs#r1 <- (Val.add (Val.mul rs#r2 rs#r3) rs#r4))) m
| Pmov r1 so =>
Next (nextinstr (rs#r1 <- (eval_shift_op so rs))) m
| Pmovc bit r1 so =>
@@ -522,9 +533,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| Pfuitod r1 r2 =>
Next (nextinstr (rs#r1 <- (Val.maketotal (Val.floatofintu rs#r2)))) m
| Pftosizd r1 r2 =>
- Next (nextinstr (rs#r1 <- (Val.maketotal (Val.intoffloat rs#r2)))) m
+ Next (nextinstr (rs #FR6 <- Vundef #r1 <- (Val.maketotal (Val.intoffloat rs#r2)))) m
| Pftouizd r1 r2 =>
- Next (nextinstr (rs#r1 <- (Val.maketotal (Val.intuoffloat rs#r2)))) m
+ Next (nextinstr (rs #FR6 <- Vundef #r1 <- (Val.maketotal (Val.intuoffloat rs#r2)))) m
| Pfcvtsd r1 r2 =>
Next (nextinstr (rs#r1 <- (Val.singleoffloat rs#r2))) m
| Pfldd r1 r2 n =>
@@ -535,7 +546,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
exec_store Mfloat64al32 (Val.add rs#r2 (Vint n)) r1 rs m
| Pfsts r1 r2 n =>
match exec_store Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m with
- | Next rs' m' => Next (rs'#FR7 <- Vundef) m'
+ | Next rs' m' => Next (rs'#FR6 <- Vundef) m'
| Stuck => Stuck
end
(* Pseudo-instructions *)
@@ -544,7 +555,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
let sp := (Vptr stk Int.zero) in
match Mem.storev Mint32 m1 (Val.add sp (Vint pos)) rs#IR13 with
| None => Stuck
- | Some m2 => Next (nextinstr (rs #IR10 <- (rs#IR13) #IR13 <- sp)) m2
+ | Some m2 => Next (nextinstr (rs #IR12 <- (rs#IR13) #IR13 <- sp)) m2
end
| Pfreeframe sz pos =>
match Mem.loadv Mint32 m (Val.add rs#IR13 (Vint pos)) with
@@ -585,37 +596,36 @@ Definition preg_of (r: mreg) : preg :=
match r with
| R0 => IR0 | R1 => IR1 | R2 => IR2 | R3 => IR3
| R4 => IR4 | R5 => IR5 | R6 => IR6 | R7 => IR7
- | R8 => IR8 | R9 => IR9 | R11 => IR11
- | IT1 => IR10 | IT2 => IR12
+ | R8 => IR8 | R9 => IR9 | R10 => IR10 | R11 => IR11
+ | R12 => IR12
| F0 => FR0 | F1 => FR1 | F2 => FR2 | F3 => FR3
- | F4 => FR4 | F5 => FR5
+ | F4 => FR4 | F5 => FR5 | F6 => FR6 | F7 => FR7
| F8 => FR8 | F9 => FR9 | F10 => FR10 | F11 => FR11
| F12 => FR12 | F13 => FR13 | F14 => FR14 | F15 => FR15
- | FT1 => FR6 | FT2 => FR7
end.
(** Extract the values of the arguments of an external call.
We exploit the calling conventions from module [Conventions], except that
we use ARM registers instead of locations. *)
+Definition chunk_of_type (ty: typ) :=
+ match ty with Tint => Mint32 | Tfloat => Mfloat64al32 | Tlong => Mint64 end.
+
Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
| extcall_arg_reg: forall r,
extcall_arg rs m (R r) (rs (preg_of r))
- | extcall_arg_int_stack: forall ofs bofs v,
- bofs = Stacklayout.fe_ofs_arg + 4 * ofs ->
- Mem.loadv Mint32 m (Val.add (rs (IR IR13)) (Vint (Int.repr bofs))) = Some v ->
- extcall_arg rs m (S (Outgoing ofs Tint)) v
- | extcall_arg_float_stack: forall ofs bofs v,
+ | extcall_arg_stack: forall ofs ty bofs v,
bofs = Stacklayout.fe_ofs_arg + 4 * ofs ->
- Mem.loadv Mfloat64al32 m (Val.add (rs (IR IR13)) (Vint (Int.repr bofs))) = Some v ->
- extcall_arg rs m (S (Outgoing ofs Tfloat)) v.
+ Mem.loadv (chunk_of_type ty) m
+ (Val.add (rs (IR IR13)) (Vint (Int.repr bofs))) = Some v ->
+ extcall_arg rs m (S Outgoing ofs ty) v.
Definition extcall_arguments
(rs: regset) (m: mem) (sg: signature) (args: list val) : Prop :=
list_forall2 (extcall_arg rs m) (loc_arguments sg) args.
-Definition loc_external_result (sg: signature) : preg :=
- preg_of (loc_result sg).
+Definition loc_external_result (sg: signature) : list preg :=
+ map preg_of (loc_result sg).
(** Extract the values of the arguments of an annotation. *)
@@ -645,28 +655,30 @@ Inductive step: state -> trace -> state -> Prop :=
exec_instr f i rs m = Next rs' m' ->
step (State rs m) E0 (State rs' m')
| exec_step_builtin:
- forall b ofs f ef args res rs m t v m',
+ forall b ofs f ef args res rs m t vl rs' m',
rs PC = Vptr b ofs ->
Genv.find_funct_ptr ge b = Some (Internal f) ->
find_instr (Int.unsigned ofs) (fn_code f) = Some (Pbuiltin ef args res) ->
- external_call ef ge (map rs args) m t v m' ->
- step (State rs m) t (State (nextinstr(rs # res <- v)) m')
+ external_call' ef ge (map rs args) m t vl m' ->
+ rs' = nextinstr
+ (set_regs res vl
+ (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
+ step (State rs m) t (State rs' m')
| exec_step_annot:
forall b ofs f ef args rs m vargs t v m',
rs PC = Vptr b ofs ->
Genv.find_funct_ptr ge b = Some (Internal f) ->
find_instr (Int.unsigned ofs) (fn_code f) = Some (Pannot ef args) ->
annot_arguments rs m args vargs ->
- external_call ef ge vargs m t v m' ->
+ external_call' ef ge vargs m t v m' ->
step (State rs m) t (State (nextinstr rs) m')
| exec_step_external:
forall b ef args res rs m t rs' m',
rs PC = Vptr b Int.zero ->
Genv.find_funct_ptr ge b = Some (External ef) ->
- external_call ef ge args m t res m' ->
+ external_call' ef ge args m t res m' ->
extcall_arguments rs m (ef_sig ef) args ->
- rs' = (rs#(loc_external_result (ef_sig ef)) <- res
- #PC <- (rs IR14)) ->
+ rs' = (set_regs (loc_external_result (ef_sig ef) ) res rs)#PC <- (rs IR14) ->
step (State rs m) t (State rs' m').
End RELSEM.
@@ -734,21 +746,21 @@ Ltac Equalities :=
discriminate.
discriminate.
inv H11.
- exploit external_call_determ. eexact H4. eexact H11. intros [A B].
+ exploit external_call_determ'. eexact H4. eexact H9. intros [A B].
split. auto. intros. destruct B; auto. subst. auto.
inv H12.
assert (vargs0 = vargs) by (eapply annot_arguments_determ; eauto). subst vargs0.
- exploit external_call_determ. eexact H5. eexact H13. intros [A B].
+ exploit external_call_determ'. eexact H5. eexact H13. intros [A B].
split. auto. intros. destruct B; auto. subst. auto.
assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
- exploit external_call_determ. eexact H3. eexact H8. intros [A B].
+ exploit external_call_determ'. eexact H3. eexact H8. intros [A B].
split. auto. intros. destruct B; auto. subst. auto.
(* trace length *)
red; intros; inv H; simpl.
omega.
- eapply external_call_trace_length; eauto.
- eapply external_call_trace_length; eauto.
- eapply external_call_trace_length; eauto.
+ inv H3; eapply external_call_trace_length; eauto.
+ inv H4; eapply external_call_trace_length; eauto.
+ inv H2; eapply external_call_trace_length; eauto.
(* initial states *)
inv H; inv H0. f_equal. congruence.
(* final no step *)
@@ -768,15 +780,3 @@ Definition data_preg (r: preg) : bool :=
| PC => false
end.
-Definition nontemp_preg (r: preg) : bool :=
- match r with
- | IR IR14 => false
- | IR IR10 => false
- | IR IR12 => false
- | IR _ => true
- | FR FR6 => false
- | FR FR7 => false
- | FR _ => true
- | CR _ => false
- | PC => false
- end.
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index d158c77..1ff28d9 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -290,9 +290,15 @@ Definition transl_op
OK (rsubimm r r1 n k)
| Omul, a1 :: a2 :: nil =>
do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
- OK (if ireg_eq r r1 || ireg_eq r r2
- then Pmul IR14 r1 r2 :: Pmov r (SOreg IR14) :: k
- else Pmul r r1 r2 :: k)
+ OK (if negb (ireg_eq r r1) then Pmul r r1 r2 :: k
+ else if negb (ireg_eq r r2) then Pmul r r2 r1 :: k
+ else Pmul IR14 r1 r2 :: Pmov r (SOreg IR14) :: k)
+ | Omla, a1 :: a2 :: a3 :: nil =>
+ do r <- ireg_of res; do r1 <- ireg_of a1;
+ do r2 <- ireg_of a2; do r3 <- ireg_of a3;
+ OK (if negb (ireg_eq r r1) then Pmla r r1 r2 r3 :: k
+ else if negb (ireg_eq r r2) then Pmla r r2 r1 r3 :: k
+ else Pmla IR14 r1 r2 r3 :: Pmov r (SOreg IR14) :: k)
| Odiv, a1 :: a2 :: nil =>
do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (Psdiv r r1 r2 :: k)
@@ -420,6 +426,7 @@ Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) :=
match ty with
| Tint => do r <- ireg_of dst; OK (loadind_int base ofs r k)
| Tfloat => do r <- freg_of dst; OK (loadind_float base ofs r k)
+ | Tlong => Error (msg "Asmgen.loadind")
end.
Definition storeind_int (src: ireg) (base: ireg) (ofs: int) (k: code) :=
@@ -432,6 +439,7 @@ Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) :=
match ty with
| Tint => do r <- ireg_of src; OK (storeind_int r base ofs k)
| Tfloat => do r <- freg_of src; OK (storeind_float r base ofs k)
+ | Tlong => Error (msg "Asmgen.storeind")
end.
(** Translation of memory accesses *)
@@ -512,6 +520,8 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing)
transl_memory_access_float Pflds mk_immed_mem_float dst addr args k
| Mfloat64 | Mfloat64al32 =>
transl_memory_access_float Pfldd mk_immed_mem_float dst addr args k
+ | Mint64 =>
+ Error (msg "Asmgen.transl_load")
end.
Definition transl_store (chunk: memory_chunk) (addr: addressing)
@@ -531,6 +541,8 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing)
transl_memory_access_float Pfsts mk_immed_mem_float src addr args k
| Mfloat64 | Mfloat64al32 =>
transl_memory_access_float Pfstd mk_immed_mem_float src addr args k
+ | Mint64 =>
+ Error (msg "Asmgen.transl_store")
end.
(** Translation of arguments to annotations *)
@@ -544,17 +556,17 @@ Definition transl_annot_param (p: Mach.annot_param) : Asm.annot_param :=
(** Translation of a Mach instruction. *)
Definition transl_instr (f: Mach.function) (i: Mach.instruction)
- (r10_is_parent: bool) (k: code) :=
+ (r12_is_parent: bool) (k: code) :=
match i with
| Mgetstack ofs ty dst =>
loadind IR13 ofs ty dst k
| Msetstack src ofs ty =>
storeind src IR13 ofs ty k
| Mgetparam ofs ty dst =>
- do c <- loadind IR10 ofs ty dst k;
- OK (if r10_is_parent
+ do c <- loadind IR12 ofs ty dst k;
+ OK (if r12_is_parent
then c
- else loadind_int IR13 f.(fn_link_ofs) IR10 c)
+ else loadind_int IR13 f.(fn_link_ofs) IR12 c)
| Mop op args res =>
transl_op op args res k
| Mload chunk addr args dst =>
@@ -573,7 +585,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
OK (loadind_int IR13 f.(fn_retaddr_ofs) IR14
(Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbsymb symb sig :: k))
| Mbuiltin ef args res =>
- OK (Pbuiltin ef (map preg_of args) (preg_of res) :: k)
+ OK (Pbuiltin ef (map preg_of args) (map preg_of res) :: k)
| Mannot ef args =>
OK (Pannot ef (map transl_annot_param args) :: k)
| Mlabel lbl =>
@@ -596,8 +608,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
Definition it1_is_parent (before: bool) (i: Mach.instruction) : bool :=
match i with
| Msetstack src ofs ty => before
- | Mgetparam ofs ty dst => negb (mreg_eq dst IT1)
- | Mop Omove args res => before && negb (mreg_eq res IT1)
+ | Mgetparam ofs ty dst => negb (mreg_eq dst R12)
+ | Mop Omove args res => before && negb (mreg_eq res R12)
| _ => false
end.
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 986d474..aede0da 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -264,7 +264,8 @@ Proof.
Opaque Int.eq.
unfold transl_op; intros; destruct op; TailNoLabel.
destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
- destruct (ireg_eq x x0 || ireg_eq x x1); TailNoLabel.
+ destruct (negb (ireg_eq x x0)). TailNoLabel. destruct (negb (ireg_eq x x1)); TailNoLabel.
+ destruct (negb (ireg_eq x x0)). TailNoLabel. destruct (negb (ireg_eq x x1)); TailNoLabel.
eapply tail_nolabel_trans; TailNoLabel.
eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel.
Qed.
@@ -420,7 +421,7 @@ Inductive match_states: Mach.state -> Asm.state -> Prop :=
(MEXT: Mem.extends m m')
(AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc)
(AG: agree ms sp rs)
- (DXP: ep = true -> rs#IR10 = parent_sp s),
+ (DXP: ep = true -> rs#IR12 = parent_sp s),
match_states (Mach.State s fb sp c ms m)
(Asm.State rs m')
| match_states_call:
@@ -451,7 +452,7 @@ Lemma exec_straight_steps:
exists rs2,
exec_straight tge tf c rs1 m1' k rs2 m2'
/\ agree ms2 sp rs2
- /\ (it1_is_parent ep i = true -> rs2#IR10 = parent_sp s)) ->
+ /\ (it1_is_parent ep i = true -> rs2#IR12 = parent_sp s)) ->
exists st',
plus step tge (State rs1 m1') E0 st' /\
match_states (Mach.State s fb sp c ms2 m2) st'.
@@ -515,9 +516,9 @@ Definition measure (s: Mach.state) : nat :=
| Mach.Returnstate _ _ _ => 1%nat
end.
-Remark preg_of_not_R10: forall r, negb (mreg_eq r IT1) = true -> IR IR10 <> preg_of r.
+Remark preg_of_not_R12: forall r, negb (mreg_eq r R12) = true -> IR IR12 <> preg_of r.
Proof.
- intros. change (IR IR10) with (preg_of IT1). red; intros.
+ intros. change (IR IR12) with (preg_of R12). red; intros.
exploit preg_of_injective; eauto. intros; subst r.
unfold proj_sumbool in H; rewrite dec_eq_true in H; discriminate.
Qed.
@@ -555,7 +556,7 @@ Proof.
rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR.
exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]].
exists rs'; split. eauto.
- split. change (undef_setstack rs) with rs. apply agree_exten with rs0; auto with asmgen.
+ split. change (Mach.undef_regs (destroyed_by_op Omove) rs) with rs. apply agree_exten with rs0; auto with asmgen.
simpl; intros. rewrite Q; auto with asmgen.
- (* Mgetparam *)
@@ -569,24 +570,24 @@ Proof.
Opaque loadind.
left; eapply exec_straight_steps; eauto; intros.
destruct ep; monadInv TR.
-(* R10 contains parent *)
+(* R12 contains parent *)
exploit loadind_correct. eexact EQ.
instantiate (2 := rs0). rewrite DXP; eauto.
intros [rs1 [P [Q R]]].
exists rs1; split. eauto.
split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen.
simpl; intros. rewrite R; auto with asmgen.
- apply preg_of_not_R10; auto.
+ apply preg_of_not_R12; auto.
(* GPR11 does not contain parent *)
- exploit loadind_int_correct. eexact A. instantiate (1 := IR10). intros [rs1 [P [Q R]]].
+ exploit loadind_int_correct. eexact A. instantiate (1 := IR12). intros [rs1 [P [Q R]]].
exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto. intros [rs2 [S [T U]]].
exists rs2; split. eapply exec_straight_trans; eauto.
split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto.
- instantiate (1 := rs1#IR10 <- (rs2#IR10)). intros.
+ instantiate (1 := rs1#IR12 <- (rs2#IR12)). intros.
rewrite Pregmap.gso; auto with asmgen.
- congruence. intros. unfold Pregmap.set. destruct (PregEq.eq r' IR10). congruence. auto with asmgen.
+ congruence. intros. unfold Pregmap.set. destruct (PregEq.eq r' IR12). congruence. auto with asmgen.
simpl; intros. rewrite U; auto with asmgen.
- apply preg_of_not_R10; auto.
+ apply preg_of_not_R12; auto.
- (* Mop *)
assert (eval_operation tge sp op rs##args m = Some v).
@@ -597,12 +598,9 @@ Opaque loadind.
exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]].
assert (S: Val.lessdef v (rs2 (preg_of res))) by (eapply Val.lessdef_trans; eauto).
exists rs2; split. eauto. split.
- assert (agree (Regmap.set res v (undef_temps rs)) sp rs2).
- eapply agree_set_undef_mreg; eauto with asmgen.
- unfold undef_op; destruct op; auto.
- change (undef_move rs) with rs. eapply agree_set_mreg; eauto.
+ eapply agree_set_undef_mreg; eauto with asmgen.
simpl. destruct op; try congruence. destruct ep; simpl; try congruence. intros.
- rewrite R; auto. apply preg_of_not_R10; auto.
+ rewrite R; auto. apply preg_of_not_R12; auto. exact I.
- (* Mload *)
assert (eval_addressing tge sp addr rs##args = Some a).
@@ -627,7 +625,7 @@ Opaque loadind.
intros. simpl in TR.
exploit transl_store_correct; eauto. intros [rs2 [P Q]].
exists rs2; split. eauto.
- split. eapply agree_exten_temps; eauto.
+ split. eapply agree_undef_regs; eauto.
simpl; congruence.
- (* Mcall *)
@@ -695,7 +693,7 @@ Opaque loadind.
exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]].
econstructor; split.
eapply exec_straight_trans. eexact P. apply exec_straight_one.
- simpl. rewrite R; auto with asmgen. rewrite A.
+ simpl. rewrite R; auto with asmgen. unfold Mach.chunk_of_type in A. rewrite A.
rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto.
split. Simpl.
split. Simpl.
@@ -741,19 +739,21 @@ Opaque loadind.
inv AT. monadInv H3.
exploit functions_transl; eauto. intro FN.
generalize (transf_function_no_overflow _ _ H2); intro NOOV.
- exploit external_call_mem_extends; eauto. eapply preg_vals; eauto.
+ exploit external_call_mem_extends'; eauto. eapply preg_vals; eauto.
intros [vres' [m2' [A [B [C D]]]]].
left. econstructor; split. apply plus_one.
eapply exec_step_builtin. eauto. eauto.
eapply find_instr_tail; eauto.
- eapply external_call_symbols_preserved; eauto.
+ eapply external_call_symbols_preserved'; eauto.
exact symbols_preserved. exact varinfo_preserved.
+ eauto.
econstructor; eauto.
- Simpl. rewrite <- H0. simpl. econstructor; eauto.
+ Simpl. rewrite set_pregs_other_2. rewrite undef_regs_other_2. rewrite <- H0. simpl. econstructor; eauto.
eapply code_tail_next_int; eauto.
- apply agree_nextinstr. eapply agree_set_undef_mreg; eauto.
- rewrite Pregmap.gss. auto.
- intros. Simpl.
+ apply preg_notin_charact. auto with asmgen.
+ apply preg_notin_charact. auto with asmgen.
+ apply agree_nextinstr. eapply agree_set_mregs; auto.
+ eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto.
congruence.
- (* Mannot *)
@@ -761,12 +761,12 @@ Opaque loadind.
exploit functions_transl; eauto. intro FN.
generalize (transf_function_no_overflow _ _ H3); intro NOOV.
exploit annot_arguments_match; eauto. intros [vargs' [P Q]].
- exploit external_call_mem_extends; eauto.
+ exploit external_call_mem_extends'; eauto.
intros [vres' [m2' [A [B [C D]]]]].
left. econstructor; split. apply plus_one.
eapply exec_step_annot. eauto. eauto.
eapply find_instr_tail; eauto. eauto.
- eapply external_call_symbols_preserved; eauto.
+ eapply external_call_symbols_preserved'; eauto.
exact symbols_preserved. exact varinfo_preserved.
eapply match_states_intro with (ep := false); eauto with coqlib.
unfold nextinstr. rewrite Pregmap.gss.
@@ -796,7 +796,7 @@ Opaque loadind.
destruct (transl_cond_correct tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]].
rewrite EC in B.
econstructor; econstructor; econstructor; split. eexact A.
- split. eapply agree_exten_temps; eauto with asmgen.
+ split. eapply agree_undef_regs; eauto with asmgen.
simpl. rewrite B. reflexivity.
- (* Mcond false *)
@@ -807,7 +807,7 @@ Opaque loadind.
econstructor; split.
eapply exec_straight_trans. eexact A.
apply exec_straight_one. simpl. rewrite B. reflexivity. auto.
- split. eapply agree_exten_temps; eauto with asmgen.
+ split. eapply agree_undef_regs; eauto with asmgen.
intros; Simpl.
simpl. congruence.
@@ -827,7 +827,7 @@ Opaque loadind.
eapply find_instr_tail; eauto.
simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A.
econstructor; eauto.
- eapply agree_exten_temps; eauto. intros. rewrite C; auto with asmgen. Simpl.
+ eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen. Simpl.
congruence.
- (* Mreturn *)
@@ -887,7 +887,7 @@ Opaque loadind.
exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto.
intros [m3' [P Q]].
(* Execution of function prologue *)
- set (rs2 := nextinstr (rs0#IR10 <- (parent_sp s) #IR13 <- (Vptr stk Int.zero))).
+ set (rs2 := nextinstr (rs0#IR12 <- (parent_sp s) #IR13 <- (Vptr stk Int.zero))).
set (rs3 := nextinstr rs2).
assert (EXEC_PROLOGUE:
exec_straight tge x
@@ -896,7 +896,7 @@ Opaque loadind.
rewrite <- H5 at 2; unfold fn_code.
apply exec_straight_two with rs2 m2'.
unfold exec_instr. rewrite C. fold sp.
- rewrite <- (sp_val _ _ _ AG). unfold chunk_of_type in F. rewrite F. auto.
+ rewrite <- (sp_val _ _ _ AG). unfold Mach.chunk_of_type in F. rewrite F. auto.
simpl. auto.
simpl. unfold exec_store. change (rs2 IR14) with (rs0 IR14).
rewrite Int.add_zero_l. simpl. unfold chunk_of_type in P. simpl in P.
@@ -911,7 +911,7 @@ Opaque loadind.
unfold rs3, rs2.
apply agree_nextinstr. apply agree_nextinstr.
eapply agree_change_sp.
- apply agree_exten_temps with rs0; eauto.
+ apply agree_undef_regs with rs0; eauto.
intros. Simpl. congruence.
- (* external function *)
@@ -919,16 +919,15 @@ Opaque loadind.
intros [tf [A B]]. simpl in B. inv B.
exploit extcall_arguments_match; eauto.
intros [args' [C D]].
- exploit external_call_mem_extends; eauto.
+ exploit external_call_mem_extends'; eauto.
intros [res' [m2' [P [Q [R S]]]]].
left; econstructor; split.
apply plus_one. eapply exec_step_external; eauto.
- eapply external_call_symbols_preserved; eauto.
+ eapply external_call_symbols_preserved'; eauto.
exact symbols_preserved. exact varinfo_preserved.
econstructor; eauto.
- eapply agree_set_mreg; eauto.
- rewrite Pregmap.gso; auto with asmgen. rewrite Pregmap.gss. auto.
- intros; Simpl.
+ apply agree_set_other; auto with asmgen.
+ eapply agree_set_mregs; eauto.
- (* return *)
inv STACKS. simpl in *.
@@ -962,8 +961,8 @@ Lemma transf_final_states:
Proof.
intros. inv H0. inv H. inv STACKS. constructor.
auto.
- compute in H1.
- generalize (preg_val _ _ _ R0 AG). rewrite H1. intros LD; inv LD. auto.
+ compute in H1. inv H1.
+ generalize (preg_val _ _ _ R0 AG). rewrite H2. intros LD; inv LD. auto.
Qed.
Theorem transf_program_correct:
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 06d6d17..e27ee80 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -541,7 +541,8 @@ Ltac ArgsInv :=
| [ H: Error _ = OK _ |- _ ] => discriminate
| [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args
| [ H: bind _ _ = OK _ |- _ ] => monadInv H
- | [ H: assertion _ = OK _ |- _ ] => monadInv H
+ | [ H: match _ with left _ => _ | right _ => assertion_failed end = OK _ |- _ ] => monadInv H
+ | [ H: match _ with true => _ | false => assertion_failed end = OK _ |- _ ] => monadInv H
end);
subst;
repeat (match goal with
@@ -685,7 +686,7 @@ Lemma transl_op_correct_same:
exists rs',
exec_straight ge fn c rs m k rs' m
/\ rs'#(preg_of res) = v
- /\ forall r, data_preg r = true -> r <> preg_of res -> rs'#r = rs#r.
+ /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs'#r = rs#r.
Proof.
intros until v; intros TR EV NOCMP.
unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; inv EV; try (TranslOpSimpl; fail).
@@ -713,11 +714,21 @@ Proof.
intros [rs' [A [B C]]].
exists rs'; auto with asmgen.
(* Omul *)
- destruct (ireg_eq x x0 || ireg_eq x x1).
+ destruct (negb (ireg_eq x x0)).
+ TranslOpSimpl.
+ destruct (negb (ireg_eq x x1)).
+ rewrite Val.mul_commut. TranslOpSimpl.
econstructor; split.
eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
intuition Simpl.
+ (* Omla *)
+ destruct (negb (ireg_eq x x0)).
TranslOpSimpl.
+ destruct (negb (ireg_eq x x1)).
+ rewrite Val.mul_commut. TranslOpSimpl.
+ econstructor; split.
+ eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
+ intuition Simpl.
(* divs *)
econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto.
intuition Simpl.
@@ -767,10 +778,11 @@ Proof.
intros. unfold rs4, rs3; Simpl. destruct islt; Simpl; rewrite OTH2; auto with asmgen.
(* intoffloat *)
econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
- intuition Simpl.
+Transparent destroyed_by_op.
+ simpl. intuition Simpl.
(* intuoffloat *)
econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
- intuition Simpl.
+ simpl. intuition Simpl.
(* floatofint *)
econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
intuition Simpl.
@@ -788,7 +800,7 @@ Lemma transl_op_correct:
exists rs',
exec_straight ge fn c rs m k rs' m
/\ Val.lessdef v rs'#(preg_of res)
- /\ forall r, data_preg r = true -> r <> preg_of res -> rs'#r = rs#r.
+ /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs'#r = rs#r.
Proof.
intros.
assert (EITHER: match op with Ocmp _ => False | _ => True end \/ exists cmp, op = Ocmp cmp).
@@ -878,7 +890,7 @@ Lemma transl_load_int_correct:
exists rs',
exec_straight ge fn c rs m k rs' m
/\ rs'#(preg_of dst) = v
- /\ forall r, nontemp_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
+ /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
Proof.
intros. monadInv H. erewrite ireg_of_eq by eauto.
eapply transl_memory_access_correct; eauto.
@@ -902,7 +914,7 @@ Lemma transl_load_float_correct:
exists rs',
exec_straight ge fn c rs m k rs' m
/\ rs'#(preg_of dst) = v
- /\ forall r, nontemp_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
+ /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
Proof.
intros. monadInv H. erewrite freg_of_eq by eauto.
eapply transl_memory_access_correct; eauto.
@@ -913,7 +925,7 @@ Proof.
Qed.
Lemma transl_store_int_correct:
- forall mk_instr is_immed src addr args k c (rs: regset) a chunk m m',
+ forall mr mk_instr is_immed src addr args k c (rs: regset) a chunk m m',
transl_memory_access_int mk_instr is_immed src addr args k = OK c ->
eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a ->
Mem.storev chunk m a rs#(preg_of src) = Some m' ->
@@ -922,7 +934,7 @@ Lemma transl_store_int_correct:
exec_store chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m) ->
exists rs',
exec_straight ge fn c rs m k rs' m'
- /\ forall r, nontemp_preg r = true -> rs'#r = rs#r.
+ /\ forall r, data_preg r = true -> preg_notin r mr -> rs'#r = rs#r.
Proof.
intros. monadInv H. erewrite ireg_of_eq in * by eauto.
eapply transl_memory_access_correct; eauto.
@@ -937,7 +949,7 @@ Proof.
Qed.
Lemma transl_store_float_correct:
- forall mk_instr is_immed src addr args k c (rs: regset) a chunk m m',
+ forall mr mk_instr is_immed src addr args k c (rs: regset) a chunk m m',
transl_memory_access_float mk_instr is_immed src addr args k = OK c ->
eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a ->
Mem.storev chunk m a rs#(preg_of src) = Some m' ->
@@ -946,7 +958,7 @@ Lemma transl_store_float_correct:
exec_store chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) ->
exists rs',
exec_straight ge fn c rs m k rs' m'
- /\ forall r, nontemp_preg r = true -> rs'#r = rs#r.
+ /\ forall r, data_preg r = true -> preg_notin r mr -> rs'#r = rs#r.
Proof.
intros. monadInv H. erewrite freg_of_eq in * by eauto.
eapply transl_memory_access_correct; eauto.
@@ -964,7 +976,7 @@ Lemma transl_load_correct:
exists rs',
exec_straight ge fn c rs m k rs' m
/\ rs'#(preg_of dst) = v
- /\ forall r, nontemp_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
+ /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
Proof.
intros. destruct chunk; simpl in H.
eapply transl_load_int_correct; eauto.
@@ -972,6 +984,7 @@ Proof.
eapply transl_load_int_correct; eauto.
eapply transl_load_int_correct; eauto.
eapply transl_load_int_correct; eauto.
+ discriminate.
eapply transl_load_float_correct; eauto.
apply Mem.loadv_float64al32 in H1. eapply transl_load_float_correct; eauto.
eapply transl_load_float_correct; eauto.
@@ -984,7 +997,7 @@ Lemma transl_store_correct:
Mem.storev chunk m a rs#(preg_of src) = Some m' ->
exists rs',
exec_straight ge fn c rs m k rs' m'
- /\ forall r, nontemp_preg r = true -> rs'#r = rs#r.
+ /\ forall r, data_preg r = true -> preg_notin r (destroyed_by_store chunk addr) -> rs'#r = rs#r.
Proof.
intros. destruct chunk; simpl in H.
- assert (Mem.storev Mint8unsigned m a (rs (preg_of src)) = Some m').
@@ -996,11 +1009,12 @@ Proof.
clear H1. eapply transl_store_int_correct; eauto.
- eapply transl_store_int_correct; eauto.
- eapply transl_store_int_correct; eauto.
+- discriminate.
- unfold transl_memory_access_float in H. monadInv H. rewrite (freg_of_eq _ _ EQ) in *.
eapply transl_memory_access_correct; eauto.
intros. econstructor; split. apply exec_straight_one.
simpl. unfold exec_store. rewrite H. rewrite H2; eauto with asmgen.
- rewrite H1. eauto. auto. intros. Simpl.
+ rewrite H1. eauto. auto. intros. Simpl.
simpl; auto.
- apply Mem.storev_float64al32 in H1. eapply transl_store_float_correct; eauto.
- eapply transl_store_float_correct; eauto.
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index 7e3217e..9bf066b 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -31,6 +31,7 @@ Inductive approx : Type :=
no compile-time information is available. *)
| I: int -> approx (** A known integer value. *)
| F: float -> approx (** A known floating-point value. *)
+ | L: int64 -> approx (** A know 64-bit integer value. *)
| G: ident -> int -> approx
(** The value is the address of the given global
symbol plus the given integer offset. *)
@@ -145,6 +146,9 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
| Ointuoffloat, F n1 :: nil => eval_static_intuoffloat n1
| Ofloatofint, I n1 :: nil => if propagate_float_constants tt then F(Float.floatofint n1) else Unknown
| Ofloatofintu, I n1 :: nil => if propagate_float_constants tt then F(Float.floatofintu n1) else Unknown
+ | Omakelong, I n1 :: I n2 :: nil => L(Int64.ofwords n1 n2)
+ | Olowlong, L n :: nil => I(Int64.loword n)
+ | Ohighlong, L n :: nil => I(Int64.hiword n)
| Ocmp c, vl => eval_static_condition_val c vl
| _, _ => Unknown
end.
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index c7de86d..687e08f 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -45,9 +45,10 @@ Definition val_match_approx (a: approx) (v: val) : Prop :=
| Unknown => True
| I p => v = Vint p
| F p => v = Vfloat p
+ | L p => v = Vlong p
| G symb ofs => v = symbol_address ge symb ofs
| S ofs => v = Val.add sp (Vint ofs)
- | _ => False
+ | Novalue => False
end.
Inductive val_list_match_approx: list approx -> list val -> Prop :=
@@ -65,6 +66,8 @@ Ltac SimplVMA :=
simpl in H; (try subst v); SimplVMA
| H: (val_match_approx (F _) ?v) |- _ =>
simpl in H; (try subst v); SimplVMA
+ | H: (val_match_approx (L _) ?v) |- _ =>
+ simpl in H; (try subst v); SimplVMA
| H: (val_match_approx (G _ _) ?v) |- _ =>
simpl in H; (try subst v); SimplVMA
| H: (val_match_approx (S _) ?v) |- _ =>
diff --git a/arm/Machregs.v b/arm/Machregs.v
index 317515c..4906eb0 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -13,6 +13,7 @@
Require Import Coqlib.
Require Import Maps.
Require Import AST.
+Require Import Op.
(** ** Machine registers *)
@@ -21,43 +22,36 @@ Require Import AST.
- Integer registers that can be allocated to RTL pseudo-registers ([Rxx]).
- Floating-point registers that can be allocated to RTL pseudo-registers
([Fxx]).
-- Two integer registers, not allocatable, reserved as temporaries for
- spilling and reloading ([ITx]).
-- Two float registers, not allocatable, reserved as temporaries for
- spilling and reloading ([FTx]).
- The type [mreg] does not include special-purpose machine registers
- such as the stack pointer and the condition codes. *)
+ The type [mreg] does not include reserved machine registers
+ such as the stack pointer, the link register, and the condition codes. *)
Inductive mreg: Type :=
(** Allocatable integer regs *)
| R0: mreg | R1: mreg | R2: mreg | R3: mreg
| R4: mreg | R5: mreg | R6: mreg | R7: mreg
- | R8: mreg | R9: mreg | R11: mreg
+ | R8: mreg | R9: mreg | R10: mreg | R11: mreg
+ | R12: mreg
(** Allocatable double-precision float regs *)
| F0: mreg | F1: mreg | F2: mreg | F3: mreg
- | F4: mreg | F5: mreg
+ | F4: mreg | F5: mreg | F6: mreg | F7: mreg
| F8: mreg | F9: mreg | F10: mreg | F11: mreg
- | F12: mreg | F13: mreg | F14: mreg | F15: mreg
- (** Integer temporaries *)
- | IT1: mreg (* R10 *) | IT2: mreg (* R12 *)
- (** Float temporaries *)
- | FT1: mreg (* F6 *) | FT2: mreg (* F7 *).
+ | F12: mreg | F13: mreg | F14: mreg | F15: mreg.
Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}.
Proof. decide equality. Defined.
+Global Opaque mreg_eq.
Definition mreg_type (r: mreg): typ :=
match r with
| R0 => Tint | R1 => Tint | R2 => Tint | R3 => Tint
| R4 => Tint | R5 => Tint | R6 => Tint | R7 => Tint
- | R8 => Tint | R9 => Tint | R11 => Tint
+ | R8 => Tint | R9 => Tint | R10 => Tint | R11 => Tint
+ | R12 => Tint
| F0 => Tfloat | F1 => Tfloat | F2 => Tfloat | F3 => Tfloat
- | F4 => Tfloat| F5 => Tfloat
+ | F4 => Tfloat| F5 => Tfloat | F6 => Tfloat | F7 => Tfloat
| F8 => Tfloat | F9 => Tfloat | F10 => Tfloat | F11 => Tfloat
| F12 => Tfloat | F13 => Tfloat | F14 => Tfloat | F15 => Tfloat
- | IT1 => Tint | IT2 => Tint
- | FT1 => Tfloat | FT2 => Tfloat
end.
Open Scope positive_scope.
@@ -69,13 +63,12 @@ Module IndexedMreg <: INDEXED_TYPE.
match r with
| R0 => 1 | R1 => 2 | R2 => 3 | R3 => 4
| R4 => 5 | R5 => 6 | R6 => 7 | R7 => 8
- | R8 => 9 | R9 => 10 | R11 => 11
- | F0 => 12 | F1 => 13 | F2 => 14 | F3 => 15
- | F4 => 16 | F5 => 17
- | F8 => 18 | F9 => 19 | F10 => 20 | F11 => 21
- | F12 => 22 | F13 => 23 | F14 => 24 | F15 => 25
- | IT1 => 26 | IT2 => 27
- | FT1 => 28 | FT2 => 29
+ | R8 => 9 | R9 => 10 | R10 => 11 | R11 => 12
+ | R12 => 13
+ | F0 => 14 | F1 => 15 | F2 => 16 | F3 => 17
+ | F4 => 18 | F5 => 19 | F6 => 20 | F7 => 21
+ | F8 => 22 | F9 => 23 | F10 => 24 | F11 => 25
+ | F12 => 26 | F13 => 27 | F14 => 28 | F15 => 29
end.
Lemma index_inj:
forall r1 r2, index r1 = index r2 -> r1 = r2.
@@ -84,3 +77,67 @@ Module IndexedMreg <: INDEXED_TYPE.
Qed.
End IndexedMreg.
+(** ** Destroyed registers, preferred registers *)
+
+Definition destroyed_by_op (op: operation): list mreg :=
+ match op with
+ | Odiv | Odivu => R0 :: R1 :: R2 :: R3 :: R12 :: nil
+ | Ointoffloat | Ointuoffloat => F6 :: nil
+ | _ => nil
+ end.
+
+Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg :=
+ nil.
+
+Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mreg :=
+ match chunk with
+ | Mfloat32 => F6 :: nil
+ | _ => nil
+ end.
+
+Definition destroyed_by_cond (cond: condition): list mreg :=
+ nil.
+
+Definition destroyed_by_jumptable: list mreg :=
+ nil.
+
+Definition destroyed_by_builtin (ef: external_function): list mreg :=
+ match ef with
+ | EF_memcpy sz al => if zle sz 32 then nil else R2 :: R3 :: R12 :: nil
+ | _ => R12 :: F6 :: nil
+ end.
+
+Definition destroyed_at_function_entry: list mreg :=
+ R12 :: nil.
+
+Definition temp_for_parent_frame: mreg :=
+ R12.
+
+Definition mregs_for_operation (op: operation): list (option mreg) * option mreg :=
+ match op with
+ | Odiv | Odivu => (Some R0 :: Some R1 :: nil, Some R0)
+ | _ => (nil, None)
+ end.
+
+Definition mregs_for_builtin (ef: external_function): list (option mreg) * list(option mreg) :=
+ match ef with
+ | EF_memcpy sz al =>
+ if zle sz 32 then (nil, nil) else (Some R3 :: Some R2 :: nil, nil)
+ | _ => (nil, nil)
+ end.
+
+Global Opaque
+ destroyed_by_op destroyed_by_load destroyed_by_store
+ destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin
+ destroyed_at_function_entry temp_for_parent_frame
+ mregs_for_operation mregs_for_builtin.
+
+(** Two-address operations. Return [true] if the first argument and
+ the result must be in the same location *and* are unconstrained
+ by [mregs_for_operation]. There are none for ARM. *)
+
+Definition two_address_op (op: operation) : bool :=
+ false.
+
+Global Opaque two_address_op.
+
diff --git a/arm/Machregsaux.ml b/arm/Machregsaux.ml
index 642437e..5486c4b 100644
--- a/arm/Machregsaux.ml
+++ b/arm/Machregsaux.ml
@@ -17,13 +17,12 @@ open Machregs
let register_names = [
("R0", R0); ("R1", R1); ("R2", R2); ("R3", R3);
("R4", R4); ("R5", R5); ("R6", R6); ("R7", R7);
- ("R8", R8); ("R9", R9); ("R11", R11);
+ ("R8", R8); ("R9", R9); ("R10", R10); ("R11", R11);
+ ("R12", R12);
("F0", F0); ("F1", F1); ("F2", F2); ("F3", F3);
- ("F4", F4); ("F5", F5);
+ ("F4", F4); ("F5", F5); ("F6", F6); ("F7", F7);
("F8", F8); ("F9", F9); ("F10", F10); ("F11", F11);
- ("F12", F12);("F13", F13);("F14", F14); ("F15", F15);
- ("R10", IT1); ("R12", IT2);
- ("F6", FT1); ("F7", FT2)
+ ("F12", F12);("F13", F13);("F14", F14); ("F15", F15)
]
let name_of_register r =
diff --git a/arm/Op.v b/arm/Op.v
index 06d0705..3dfea77 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -81,6 +81,7 @@ Inductive operation : Type :=
| Orsubshift: shift -> operation (**r [rd = shifted r2 - r1] *)
| Orsubimm: int -> operation (**r [rd = n - r1] *)
| Omul: operation (**r [rd = r1 * r2] *)
+ | Omla: operation (**r [rd = r1 * r2 + r3] *)
| Odiv: operation (**r [rd = r1 / r2] (signed) *)
| Odivu: operation (**r [rd = r1 / r2] (unsigned) *)
| Oand: operation (**r [rd = r1 & r2] *)
@@ -114,6 +115,10 @@ Inductive operation : Type :=
| Ointuoffloat: operation (**r [rd = unsigned_int_of_float(r1)] *)
| Ofloatofint: operation (**r [rd = float_of_signed_int(r1)] *)
| Ofloatofintu: operation (**r [rd = float_of_unsigned_int(r1)] *)
+(*c Manipulating 64-bit integers: *)
+ | Omakelong: operation (**r [rd = r1 << 32 | r2] *)
+ | Olowlong: operation (**r [rd = low-word(r1)] *)
+ | Ohighlong: operation (**r [rd = high-word(r1)] *)
(*c Boolean tests: *)
| Ocmp: condition -> operation. (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
@@ -213,6 +218,7 @@ Definition eval_operation
| Orsubshift s, v1 :: v2 :: nil => Some (Val.sub (eval_shift s v2) v1)
| Orsubimm n, v1 :: nil => Some (Val.sub (Vint n) v1)
| Omul, v1 :: v2 :: nil => Some (Val.mul v1 v2)
+ | Omla, v1 :: v2 :: v3 :: nil => Some (Val.add (Val.mul v1 v2) v3)
| Odiv, v1 :: v2 :: nil => Val.divs v1 v2
| Odivu, v1 :: v2 :: nil => Val.divu v1 v2
| Oand, v1 :: v2 :: nil => Some (Val.and v1 v2)
@@ -244,6 +250,9 @@ Definition eval_operation
| Ointuoffloat, v1::nil => Val.intuoffloat v1
| Ofloatofint, v1::nil => Val.floatofint v1
| Ofloatofintu, v1::nil => Val.floatofintu v1
+ | Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2)
+ | Olowlong, v1::nil => Some(Val.loword v1)
+ | Ohighlong, v1::nil => Some(Val.hiword v1)
| Ocmp c, _ => Some(Val.of_optbool (eval_condition c vl m))
| _, _ => None
end.
@@ -302,6 +311,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
| Orsubshift _ => (Tint :: Tint :: nil, Tint)
| Orsubimm _ => (Tint :: nil, Tint)
| Omul => (Tint :: Tint :: nil, Tint)
+ | Omla => (Tint :: Tint :: Tint :: nil, Tint)
| Odiv => (Tint :: Tint :: nil, Tint)
| Odivu => (Tint :: Tint :: nil, Tint)
| Oand => (Tint :: Tint :: nil, Tint)
@@ -333,6 +343,9 @@ Definition type_of_operation (op: operation) : list typ * typ :=
| Ointuoffloat => (Tfloat :: nil, Tint)
| Ofloatofint => (Tint :: nil, Tfloat)
| Ofloatofintu => (Tint :: nil, Tfloat)
+ | Omakelong => (Tint :: Tint :: nil, Tlong)
+ | Olowlong => (Tlong :: nil, Tint)
+ | Ohighlong => (Tlong :: nil, Tint)
| Ocmp c => (type_of_condition c, Tint)
end.
@@ -374,6 +387,7 @@ Proof with (try exact I).
generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; intuition. destruct (zeq b0 b)...
destruct v0...
destruct v0; destruct v1...
+ destruct v0... destruct v1... destruct v2...
destruct v0; destruct v1; simpl in H0; inv H0.
destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2...
destruct v0; destruct v1; simpl in H0; inv H0. destruct (Int.eq i0 Int.zero); inv H2...
@@ -406,6 +420,9 @@ Proof with (try exact I).
destruct v0; simpl in H0; inv H0. destruct (Float.intuoffloat f); simpl in H2; inv H2...
destruct v0; simpl in H0; inv H0...
destruct v0; simpl in H0; inv H0...
+ destruct v0; destruct v1...
+ destruct v0...
+ destruct v0...
destruct (eval_condition c vl m)... destruct b...
Qed.
@@ -544,6 +561,29 @@ Proof.
rewrite Val.add_assoc. simpl. auto.
Qed.
+(** Offset an addressing mode [addr] by a quantity [delta], so that
+ it designates the pointer [delta] bytes past the pointer designated
+ by [addr]. May be undefined, in which case [None] is returned. *)
+
+Definition offset_addressing (addr: addressing) (delta: int) : option addressing :=
+ match addr with
+ | Aindexed n => Some(Aindexed (Int.add n delta))
+ | Aindexed2 => None
+ | Aindexed2shift s => None
+ | Ainstack n => Some(Ainstack (Int.add n delta))
+ end.
+
+Lemma eval_offset_addressing:
+ forall (F V: Type) (ge: Genv.t F V) sp addr args delta addr' v,
+ offset_addressing addr delta = Some addr' ->
+ eval_addressing ge sp addr args = Some v ->
+ eval_addressing ge sp addr' args = Some(Val.add v (Vint delta)).
+Proof.
+ intros. destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst.
+ rewrite Val.add_assoc; auto.
+ rewrite Val.add_assoc. auto.
+Qed.
+
(** Transformation of addressing modes with two operands or more
into an equivalent arithmetic operation. This is used in the [Reload]
pass when a store instruction cannot be reloaded directly because
@@ -787,6 +827,7 @@ Proof.
apply (@Values.val_sub_inject f (Vint i) (Vint i) v v'); auto.
inv H4; inv H2; simpl; auto.
+ apply Values.val_add_inject; auto. inv H4; inv H2; simpl; auto.
inv H4; inv H3; simpl in H1; inv H1. simpl.
destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists.
inv H4; inv H3; simpl in H1; inv H1. simpl.
@@ -828,6 +869,10 @@ Proof.
inv H4; simpl in *; inv H1. TrivialExists.
inv H4; simpl in *; inv H1. TrivialExists.
+ inv H4; inv H2; simpl; auto.
+ inv H4; simpl; auto.
+ inv H4; simpl; auto.
+
subst v1. destruct (eval_condition c vl1 m1) eqn:?.
exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
destruct b; simpl; constructor.
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 5778286..1bac715 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -181,47 +181,11 @@ let emit_constants oc =
symbol_labels;
reset_constants ()
-(* Simulate instructions by calling helper functions *)
-
-let print_list_ireg oc l =
- match l with
- | [] -> assert false
- | r1 :: rs -> ireg oc r1; List.iter (fun r -> fprintf oc ", %a" ireg r) rs
-
-let rec remove l r =
- match l with
- | [] -> []
- | hd :: tl -> if hd = r then remove tl r else hd :: remove tl r
-
-let call_helper oc fn dst arg1 arg2 =
- (* Preserve caller-save registers r0...r3 except dst *)
- let tosave = remove [IR0; IR1; IR2; IR3] dst in
- fprintf oc " stmfd sp!, {%a}\n" print_list_ireg tosave;
- (* Copy arg1 to R0 and arg2 to R1 *)
- let moves =
- Parmov.parmove2 (=) (fun _ -> IR14) [arg1; arg2] [IR0; IR1] in
- List.iter
- (fun (s, d) ->
- fprintf oc " mov %a, %a\n" ireg d ireg s)
- moves;
- (* Call the helper function *)
- fprintf oc " bl %s\n" fn;
- (* Move result to dst *)
- begin match dst with
- | IR0 -> ()
- | _ -> fprintf oc " mov %a, r0\n" ireg dst
- end;
- (* Restore the other caller-save registers *)
- fprintf oc " ldmfd sp!, {%a}\n" print_list_ireg tosave;
- (* ... for a total of at most 7 instructions *)
- 7
-
(* Built-ins. They come in two flavors:
- annotation statements: take their arguments in registers or stack
locations; generate no code;
- inlined by the compiler: take their arguments in arbitrary
- registers; preserve all registers the temporaries
- (IR10, IR12, IR14, FP2, FP4)
+ registers; preserve all registers except IR2, IR3, IR12 and FP6.
*)
(* Handling of annotations *)
@@ -234,9 +198,9 @@ let print_annot_val oc txt args res =
fprintf oc "%s annotation: " comment;
PrintAnnot.print_annot_val preg oc txt args;
match args, res with
- | IR src :: _, IR dst ->
+ | [IR src], [IR dst] ->
if dst = src then 0 else (fprintf oc " mov %a, %a\n" ireg dst ireg src; 1)
- | FR src :: _, FR dst ->
+ | [FR src], [FR dst] ->
if dst = src then 0 else (fprintf oc " fcpy %a, %a\n" freg dst freg src; 1)
| _, _ -> assert false
@@ -265,16 +229,12 @@ let print_builtin_memcpy_small oc sz al src dst =
let print_builtin_memcpy_big oc sz al src dst =
assert (sz >= al);
assert (sz mod al = 0);
+ assert (src = IR2);
+ assert (dst = IR3);
let (load, store, chunksize) =
if al >= 4 then ("ldr", "str", 4)
else if al = 2 then ("ldrh", "strh", 2)
else ("ldrb", "strb", 1) in
- let tmp =
- if src <> IR0 && dst <> IR0 then IR0
- else if src <> IR1 && dst <> IR1 then IR1
- else IR2 in
- let tosave = List.sort compare [tmp;src;dst] in
- fprintf oc " stmfd sp!, {%a}\n" print_list_ireg tosave;
begin match Asmgen.decompose_int
(coqint_of_camlint (Int32.of_int (sz / chunksize))) with
| [] -> assert false
@@ -286,12 +246,11 @@ let print_builtin_memcpy_big oc sz al src dst =
tl
end;
let lbl = new_label() in
- fprintf oc ".L%d: %s %a, [%a], #%d\n" lbl load ireg tmp ireg src chunksize;
+ fprintf oc ".L%d: %s %a, [%a], #%d\n" lbl load ireg IR12 ireg src chunksize;
fprintf oc " subs %a, %a, #1\n" ireg IR14 ireg IR14;
- fprintf oc " %s %a, [%a], #%d\n" store ireg tmp ireg dst chunksize;
+ fprintf oc " %s %a, [%a], #%d\n" store ireg IR12 ireg dst chunksize;
fprintf oc " bne .L%d\n" lbl;
- fprintf oc " ldmfd sp!, {%a}\n" print_list_ireg tosave;
- 9
+ 8
let print_builtin_memcpy oc sz al args =
let (dst, src) =
@@ -308,20 +267,28 @@ let print_builtin_memcpy oc sz al args =
let print_builtin_vload_common oc chunk args res =
match chunk, args, res with
- | Mint8unsigned, [IR addr], IR res ->
+ | Mint8unsigned, [IR addr], [IR res] ->
fprintf oc " ldrb %a, [%a, #0]\n" ireg res ireg addr; 1
- | Mint8signed, [IR addr], IR res ->
+ | Mint8signed, [IR addr], [IR res] ->
fprintf oc " ldrsb %a, [%a, #0]\n" ireg res ireg addr; 1
- | Mint16unsigned, [IR addr], IR res ->
+ | Mint16unsigned, [IR addr], [IR res] ->
fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg addr; 1
- | Mint16signed, [IR addr], IR res ->
+ | Mint16signed, [IR addr], [IR res] ->
fprintf oc " ldrsh %a, [%a, #0]\n" ireg res ireg addr; 1
- | Mint32, [IR addr], IR res ->
+ | Mint32, [IR addr], [IR res] ->
fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg addr; 1
- | Mfloat32, [IR addr], FR res ->
+ | Mint64, [IR addr], [IR res1; IR res2] ->
+ if addr <> res2 then begin
+ fprintf oc " ldr %a, [%a, #0]\n" ireg res2 ireg addr;
+ fprintf oc " ldr %a, [%a, #4]\n" ireg res1 ireg addr
+ end else begin
+ fprintf oc " ldr %a, [%a, #4]\n" ireg res1 ireg addr;
+ fprintf oc " ldr %a, [%a, #0]\n" ireg res2 ireg addr
+ end; 2
+ | Mfloat32, [IR addr], [FR res] ->
fprintf oc " flds %a, [%a, #0]\n" freg_single res ireg addr;
fprintf oc " fcvtds %a, %a\n" freg res freg_single res; 2
- | (Mfloat64 | Mfloat64al32), [IR addr], FR res ->
+ | (Mfloat64 | Mfloat64al32), [IR addr], [FR res] ->
fprintf oc " fldd %a, [%a, #0]\n" freg res ireg addr; 1
| _ ->
assert false
@@ -346,6 +313,9 @@ let print_builtin_vstore_common oc chunk args =
fprintf oc " strh %a, [%a, #0]\n" ireg src ireg addr; 1
| Mint32, [IR addr; IR src] ->
fprintf oc " str %a, [%a, #0]\n" ireg src ireg addr; 1
+ | Mint64, [IR addr; IR src1; IR src2] ->
+ fprintf oc " str %a, [%a, #0]\n" ireg src2 ireg addr;
+ fprintf oc " str %a, [%a, #4]\n" ireg src1 ireg addr; 2
| Mfloat32, [IR addr; FR src] ->
fprintf oc " fcvtsd %a, %a\n" freg_single FR6 freg src;
fprintf oc " fsts %a, [%a, #0]\n" freg_single FR6 ireg addr; 2
@@ -386,22 +356,57 @@ let print_builtin_inline oc name args res =
fprintf oc "%s begin %s\n" comment name;
let n = match name, args, res with
(* Integer arithmetic *)
- | "__builtin_bswap", [IR a1], IR res ->
+ | "__builtin_bswap", [IR a1], [IR res] ->
print_bswap oc a1 IR14 res; 4
- | "__builtin_cntlz", [IR a1], IR res ->
+ | "__builtin_cntlz", [IR a1], [IR res] ->
fprintf oc " clz %a, %a\n" ireg res ireg a1; 1
(* Float arithmetic *)
- | "__builtin_fabs", [FR a1], FR res ->
+ | "__builtin_fabs", [FR a1], [FR res] ->
fprintf oc " fabsd %a, %a\n" freg res freg a1; 1
- | "__builtin_fsqrt", [FR a1], FR res ->
+ | "__builtin_fsqrt", [FR a1], [FR res] ->
fprintf oc " fsqrtd %a, %a\n" freg res freg a1; 1
+ (* 64-bit integer arithmetic *)
+ | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] ->
+ if rl = ah then begin
+ fprintf oc " rsbs %a, %a, #0\n" ireg IR14 ireg al;
+ fprintf oc " rsc %a, %a, #0\n" ireg rh ireg ah;
+ fprintf oc " mov %a, %a\n" ireg rl ireg IR14; 3
+ end else begin
+ fprintf oc " rsbs %a, %a, #0\n" ireg rl ireg al;
+ fprintf oc " rsc %a, %a, #0\n" ireg rh ireg ah; 2
+ end
+ | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
+ if rl = ah || rl = bh then begin
+ fprintf oc " adds %a, %a, %a\n" ireg IR14 ireg al ireg bl;
+ fprintf oc " adc %a, %a, %a\n" ireg rh ireg ah ireg bh;
+ fprintf oc " mov %a, %a\n" ireg rl ireg IR14; 3
+ end else begin
+ fprintf oc " adds %a, %a, %a\n" ireg rl ireg al ireg bl;
+ fprintf oc " adc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2
+ end
+ | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
+ if rl = ah || rl = bh then begin
+ fprintf oc " subs %a, %a, %a\n" ireg IR14 ireg al ireg bl;
+ fprintf oc " sbc %a, %a, %a\n" ireg rh ireg ah ireg bh;
+ fprintf oc " mov %a, %a\n" ireg rl ireg IR14; 3
+ end else begin
+ fprintf oc " subs %a, %a, %a\n" ireg rl ireg al ireg bl;
+ fprintf oc " sbc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2
+ end
+ | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
+ if rl = a || rh = a then begin
+ fprintf oc " mov %a, %a\n" ireg IR14 ireg a;
+ fprintf oc " umull %a, %a, %a, %a\n" ireg rl ireg rh ireg IR14 ireg b; 2
+ end else begin
+ fprintf oc " umull %a, %a, %a, %a\n" ireg rl ireg rh ireg a ireg b; 1
+ end
(* Memory accesses *)
- | "__builtin_read16_reversed", [IR a1], IR res ->
+ | "__builtin_read16_reversed", [IR a1], [IR res] ->
fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg a1;
fprintf oc " mov %a, %a, lsl #8\n" ireg IR14 ireg res;
fprintf oc " and %a, %a, #0xFF00\n" ireg IR14 ireg IR14;
fprintf oc " orr %a, %a, %a, lsr #8\n" ireg res ireg IR14 ireg res; 4
- | "__builtin_read32_reversed", [IR a1], IR res ->
+ | "__builtin_read32_reversed", [IR a1], [IR res] ->
fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg a1;
print_bswap oc res IR14 res; 5
| "__builtin_write16_reversed", [IR a1; IR a2], _ ->
@@ -410,9 +415,19 @@ let print_builtin_inline oc name args res =
fprintf oc " orr %a, %a, %a, lsl #8\n" ireg IR14 ireg IR14 ireg a2;
fprintf oc " strh %a, [%a, #0]\n" ireg IR14 ireg a1; 4
| "__builtin_write32_reversed", [IR a1; IR a2], _ ->
- let tmp = if a1 = IR10 then IR12 else IR10 in
- print_bswap oc a2 IR14 tmp;
- fprintf oc " str %a, [%a, #0]\n" ireg tmp ireg a1; 5
+ if a1 <> IR12 then begin
+ print_bswap oc a2 IR14 IR12;
+ fprintf oc " str %a, [%a, #0]\n" ireg IR12 ireg a1; 5
+ end else begin
+ fprintf oc " mov %a, %a, lsr #24\n" ireg IR14 ireg a2;
+ fprintf oc " str %a, [%a, #0]\n" ireg IR14 ireg a1;
+ fprintf oc " mov %a, %a, lsr #16\n" ireg IR14 ireg a2;
+ fprintf oc " str %a, [%a, #1]\n" ireg IR14 ireg a1;
+ fprintf oc " mov %a, %a, lsr #8\n" ireg IR14 ireg a2;
+ fprintf oc " str %a, [%a, #2]\n" ireg IR14 ireg a1;
+ fprintf oc " str %a, [%a, #3]\n" ireg IR14 ireg a1;
+ 7
+ end
(* Catch-all *)
| _ ->
invalid_arg ("unrecognized builtin " ^ name)
@@ -516,6 +531,8 @@ let print_instruction oc = function
fprintf oc " ldrsb %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1
| Pldrsh(r1, r2, sa) ->
fprintf oc " ldrsh %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1
+ | Pmla(r1, r2, r3, r4) ->
+ fprintf oc " mla %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1
| Pmov(r1, so) ->
fprintf oc " mov %a, %a\n" ireg r1 shift_op so; 1
| Pmovc(bit, r1, so) ->
@@ -535,11 +552,13 @@ let print_instruction oc = function
| Pstrh(r1, r2, sa) ->
fprintf oc " strh %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1
| Psdiv(r1, r2, r3) ->
- call_helper oc "__aeabi_idiv" r1 r2 r3
+ assert (r1 = IR0 && r2 = IR0 && r3 = IR1);
+ fprintf oc " bl __aeabi_idiv\n"; 1
| Psub(r1, r2, so) ->
fprintf oc " sub %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1
| Pudiv(r1, r2, r3) ->
- call_helper oc "__aeabi_uidiv" r1 r2 r3
+ assert (r1 = IR0 && r2 = IR0 && r3 = IR1);
+ fprintf oc " bl __aeabi_uidiv\n"; 1
(* Floating-point coprocessor instructions *)
| Pfcpyd(r1, r2) ->
fprintf oc " fcpyd %a, %a\n" freg r1 freg r2; 1
@@ -593,14 +612,14 @@ let print_instruction oc = function
fprintf oc " fsts %a, [%a, #%a]\n" freg_single FR6 ireg r2 coqint n; 2
(* Pseudo-instructions *)
| Pallocframe(sz, ofs) ->
- fprintf oc " mov r10, sp\n";
+ fprintf oc " mov r12, sp\n";
let ninstr = ref 0 in
List.iter
(fun n ->
fprintf oc " sub sp, sp, #%a\n" coqint n;
incr ninstr)
(Asmgen.decompose_int sz);
- fprintf oc " str r10, [sp, #%a]\n" coqint ofs;
+ fprintf oc " str r12, [sp, #%a]\n" coqint ofs;
2 + !ninstr
| Pfreeframe(sz, ofs) ->
if Asmgen.is_immed_arith sz
@@ -620,7 +639,7 @@ let print_instruction oc = function
List.iter
(fun l -> fprintf oc " .word %a\n" print_label l)
tbl;
- 2 + List.length tbl
+ 3 + List.length tbl
| Pbuiltin(ef, args, res) ->
begin match ef with
| EF_builtin(name, sg) ->
@@ -713,6 +732,8 @@ let print_init oc = function
fprintf oc " .short %ld\n" (camlint_of_coqint n)
| Init_int32 n ->
fprintf oc " .word %ld\n" (camlint_of_coqint n)
+ | Init_int64 n ->
+ fprintf oc " .quad %Ld\n" (camlint64_of_coqint n)
| Init_float32 n ->
fprintf oc " .word 0x%lx %s %.15g \n" (camlint_of_coqint (Floats.Float.bits_of_single n))
comment (camlfloat_of_coqfloat n)
diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml
index b5a8d75..eff3959 100644
--- a/arm/PrintOp.ml
+++ b/arm/PrintOp.ml
@@ -71,6 +71,7 @@ let print_operation reg pp = function
| Orsubshift s, [r1;r2] -> fprintf pp "%a %a - %a" reg r2 shift s reg r1
| Orsubimm n, [r1] -> fprintf pp "%ld - %a" (camlint_of_coqint n) reg r1
| Omul, [r1;r2] -> fprintf pp "%a * %a" reg r1 reg r2
+ | Omla, [r1;r2;r3] -> fprintf pp "%a * %a + %a" reg r1 reg r2 reg r3
| Odiv, [r1;r2] -> fprintf pp "%a /s %a" reg r1 reg r2
| Odivu, [r1;r2] -> fprintf pp "%a /u %a" reg r1 reg r2
| Oand, [r1;r2] -> fprintf pp "%a & %a" reg r1 reg r2
@@ -100,6 +101,9 @@ let print_operation reg pp = function
| Osingleoffloat, [r1] -> fprintf pp "singleoffloat(%a)" reg r1
| Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1
| Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1
+ | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2
+ | Olowlong, [r1] -> fprintf pp "lowlong(%a)" reg r1
+ | Ohighlong, [r1] -> fprintf pp "highlong(%a)" reg r1
| Ocmp c, args -> print_condition reg pp (c, args)
| _ -> fprintf pp "<bad operator>"
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 22ef88d..d81328b 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -85,6 +85,8 @@ Nondetfunction add (e1: expr) (e2: expr) :=
| t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil))
| Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil)
| t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (t1:::t2:::Enil)
+ | Eop Omul (t1:::t2:::Enil), t3 => Eop Omla (t1:::t2:::t3:::Enil)
+ | t1, Eop Omul (t2:::t3:::Enil) => Eop Omla (t2:::t3:::t1:::Enil)
| _, _ => Eop Oadd (e1:::e2:::Enil)
end.
@@ -185,6 +187,7 @@ Nondetfunction mul (e1: expr) (e2: expr) :=
Nondetfunction andimm (n1: int) (e2: expr) :=
if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else
+ if Int.eq n1 Int.mone then e2 else
match e2 with
| Eop (Ointconst n2) Enil =>
Eop (Ointconst (Int.and n1 n2)) Enil
@@ -215,6 +218,7 @@ Definition same_expr_pure (e1 e2: expr) :=
Nondetfunction orimm (n1: int) (e2: expr) :=
if Int.eq n1 Int.zero then e2 else
+ if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil else
match e2 with
| Eop (Ointconst n2) Enil => Eop (Ointconst (Int.or n1 n2)) Enil
| Eop (Oorimm n2) (t2:::Enil) => Eop (Oorimm (Int.or n1 n2)) (t2:::Enil)
@@ -407,6 +411,7 @@ Definition can_use_Aindexed2 (chunk: memory_chunk): bool :=
| Mint16signed => true
| Mint16unsigned => true
| Mint32 => true
+ | Mint64 => false
| Mfloat32 => false
| Mfloat64 => false
| Mfloat64al32 => false
@@ -419,6 +424,7 @@ Definition can_use_Aindexed2shift (chunk: memory_chunk): bool :=
| Mint16signed => false
| Mint16unsigned => false
| Mint32 => true
+ | Mint64 => false
| Mfloat32 => false
| Mfloat64 => false
| Mfloat64al32 => false
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index ecc758f..a71ead7 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -27,13 +27,6 @@ Require Import SelectOp.
Open Local Scope cminorsel_scope.
-Section CMCONSTR.
-
-Variable ge: genv.
-Variable sp: val.
-Variable e: env.
-Variable m: mem.
-
(** * Useful lemmas and tactics *)
(** The following are trivial lemmas and custom tactics that help
@@ -81,6 +74,13 @@ Ltac TrivialExists :=
(** * Correctness of the smart constructors *)
+Section CMCONSTR.
+
+Variable ge: genv.
+Variable sp: val.
+Variable e: env.
+Variable m: mem.
+
(** We now show that the code generated by "smart constructor" functions
such as [Selection.notint] behaves as expected. Continuing the
[notint] example, we show that if the expression [e]
@@ -172,6 +172,8 @@ Proof.
subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp.
subst. rewrite Val.add_commut. TrivialExists.
subst. TrivialExists.
+ subst. TrivialExists.
+ subst. rewrite Val.add_commut. TrivialExists.
TrivialExists.
Qed.
@@ -325,6 +327,9 @@ Proof.
predSpec Int.eq Int.eq_spec n Int.zero.
intros. exists (Vint Int.zero); split. EvalOp.
destruct x; simpl; auto. subst n. rewrite Int.and_zero. auto.
+ predSpec Int.eq Int.eq_spec n Int.mone.
+ intros. exists x; split; auto.
+ subst. destruct x; simpl; auto. rewrite Int.and_mone; auto.
case (andimm_match a); intros.
InvEval. TrivialExists. simpl. rewrite Int.and_commut; auto.
InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists.
@@ -352,6 +357,9 @@ Proof.
predSpec Int.eq Int.eq_spec n Int.zero.
intros. subst. exists x; split; auto.
destruct x; simpl; auto. rewrite Int.or_zero; auto.
+ predSpec Int.eq Int.eq_spec n Int.mone.
+ intros. exists (Vint Int.mone); split. EvalOp.
+ destruct x; simpl; auto. subst n. rewrite Int.or_mone. auto.
destruct (orimm_match a); intros; InvEval.
TrivialExists. simpl. rewrite Int.or_commut; auto.
subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists.
diff --git a/arm/linux/Conventions1.v b/arm/linux/Conventions1.v
index f1ddc23..1731eba 100644
--- a/arm/linux/Conventions1.v
+++ b/arm/linux/Conventions1.v
@@ -32,34 +32,19 @@ Require Import Locations.
*)
Definition int_caller_save_regs :=
- R0 :: R1 :: R2 :: R3 :: nil.
+ R0 :: R1 :: R2 :: R3 :: R12 :: nil.
Definition float_caller_save_regs :=
- F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: nil.
+ F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: nil.
Definition int_callee_save_regs :=
- R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R11 :: nil.
+ R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: R11 :: nil.
Definition float_callee_save_regs :=
F8 :: F9 :: F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: nil.
-Definition destroyed_at_call_regs :=
- int_caller_save_regs ++ float_caller_save_regs.
-
Definition destroyed_at_call :=
- List.map R destroyed_at_call_regs.
-
-Definition int_temporaries := IT1 :: IT2 :: nil.
-
-Definition float_temporaries := FT1 :: FT2 :: nil.
-
-Definition temporary_regs := int_temporaries ++ float_temporaries.
-
-Definition temporaries := List.map R temporary_regs.
-
-Definition destroyed_at_move_regs: list mreg := nil.
-
-Definition destroyed_at_move := List.map R destroyed_at_move_regs.
+ int_caller_save_regs ++ float_caller_save_regs.
Definition dummy_int_reg := R0. (**r Used in [Coloring]. *)
Definition dummy_float_reg := F0. (**r Used in [Coloring]. *)
@@ -72,7 +57,7 @@ Definition dummy_float_reg := F0. (**r Used in [Coloring]. *)
Definition index_int_callee_save (r: mreg) :=
match r with
| R4 => 0 | R5 => 1 | R6 => 2 | R7 => 3
- | R8 => 4 | R9 => 5 | R11 => 6
+ | R8 => 4 | R9 => 5 | R10 => 6 | R11 => 7
| _ => -1
end.
@@ -169,34 +154,27 @@ Qed.
Lemma register_classification:
forall r,
- (In (R r) temporaries \/ In (R r) destroyed_at_call) \/
- (In r int_callee_save_regs \/ In r float_callee_save_regs).
+ In r destroyed_at_call \/ In r int_callee_save_regs \/ In r float_callee_save_regs.
Proof.
destruct r;
- try (left; left; simpl; OrEq);
- try (left; right; simpl; OrEq);
+ try (left; simpl; OrEq);
try (right; left; simpl; OrEq);
try (right; right; simpl; OrEq).
Qed.
+
Lemma int_callee_save_not_destroyed:
forall r,
- In (R r) temporaries \/ In (R r) destroyed_at_call ->
- ~(In r int_callee_save_regs).
+ In r destroyed_at_call -> In r int_callee_save_regs -> False.
Proof.
- intros; red; intros. elim H.
- generalize H0. simpl; ElimOrEq; NotOrEq.
- generalize H0. simpl; ElimOrEq; NotOrEq.
+ intros. revert H0 H. simpl. ElimOrEq; NotOrEq.
Qed.
Lemma float_callee_save_not_destroyed:
forall r,
- In (R r) temporaries \/ In (R r) destroyed_at_call ->
- ~(In r float_callee_save_regs).
+ In r destroyed_at_call -> In r float_callee_save_regs -> False.
Proof.
- intros; red; intros. elim H.
- generalize H0. simpl; ElimOrEq; NotOrEq.
- generalize H0. simpl; ElimOrEq; NotOrEq.
+ intros. revert H0 H. simpl. ElimOrEq; NotOrEq.
Qed.
Lemma int_callee_save_type:
@@ -245,51 +223,33 @@ Qed.
Calling conventions are largely arbitrary: they must respect the properties
proved in this section (such as no overlapping between the locations
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 ARM EABI compiler, we
- implement *almost* the standard conventions defined in the ARM EABI application
- binary interface, with two exceptions:
-- Double-precision arguments and results are passed in VFP double registers
- instead of pairs of integer registers.
-- Single-precision arguments and results are passed as double-precision floats.
-*)
+ locations. *)
(** ** Location of function result *)
(** The result value of a function is passed back to the caller in
- registers [R0] or [F0], depending on the type of the returned value.
- We treat a function without result as a function with one integer result. *)
+ registers [R0] or [F0] or [R0,R1], depending on the type of the
+ returned value. We treat a function without result as a function
+ with one integer result. *)
-Definition loc_result (s: signature) : mreg :=
+Definition loc_result (s: signature) : list mreg :=
match s.(sig_res) with
- | None => R0
- | Some Tint => R0
- | Some Tfloat => F0
+ | None => R0 :: nil
+ | Some Tint => R0 :: nil
+ | Some Tfloat => F0 :: nil
+ | Some Tlong => R1 :: R0 :: nil
end.
-(** The result location has the type stated in the signature. *)
-
-Lemma loc_result_type:
- forall sig,
- mreg_type (loc_result sig) =
- match sig.(sig_res) with None => Tint | Some ty => ty end.
-Proof.
- intros; unfold loc_result.
- destruct (sig_res sig).
- destruct t; reflexivity.
- reflexivity.
-Qed.
-
(** The result location is a caller-save register or a temporary *)
Lemma loc_result_caller_save:
- forall (s: signature),
- In (R (loc_result s)) destroyed_at_call \/ In (R (loc_result s)) temporaries.
+ forall (s: signature) (r: mreg),
+ In r (loc_result s) -> In r destroyed_at_call.
Proof.
- intros; unfold loc_result. left;
- destruct (sig_res s).
- destruct t; simpl; OrEq.
- simpl; OrEq.
+ intros.
+ assert (r = R0 \/ r = R1 \/ r = F0).
+ unfold loc_result in H. destruct (sig_res s); [destruct t|idtac]; simpl in H; intuition.
+ destruct H0 as [A | [A | A]]; subst r; simpl; OrEq.
Qed.
(** ** Location of function arguments *)
@@ -299,34 +259,37 @@ Qed.
- The first 2 float arguments are passed in registers [F0] and [F1].
- Each float argument passed in a float register ``consumes'' an aligned pair
of two integer registers.
+- Each long integer argument is passed in an aligned pair of two integer
+ registers.
- Extra arguments are passed on the stack, in [Outgoing] slots, consecutively
- assigned (1 word for an integer argument, 2 words for a float),
+ assigned (1 word for an integer argument, 2 words for a float or a long),
starting at word offset 0.
*)
-Function ireg_param (n: Z) : mreg :=
+Definition ireg_param (n: Z) : mreg :=
if zeq n (-4) then R0
else if zeq n (-3) then R1
else if zeq n (-2) then R2
- else if zeq n (-1) then R3
- else R4. (**r should not happen *)
-
-Function freg_param (n: Z) : mreg :=
- if zeq n (-4) then F0
- else if zeq n (-3) then F1
- else if zeq n (-2) then F1
- else F2. (**r should not happen *)
+ else R3.
+Definition freg_param (n: Z) : mreg :=
+ if zeq n (-4) then F0 else F1.
Fixpoint loc_arguments_rec (tyl: list typ) (ofs: Z) {struct tyl} : list loc :=
match tyl with
| nil => nil
| Tint :: tys =>
- (if zle 0 ofs then S (Outgoing ofs Tint) else R (ireg_param ofs))
+ (if zle 0 ofs then S Outgoing ofs Tint else R (ireg_param ofs))
:: loc_arguments_rec tys (ofs + 1)
| Tfloat :: tys =>
- (if zle (-1) ofs then S (Outgoing (align ofs 2) Tfloat) else R (freg_param ofs))
- :: loc_arguments_rec tys (align ofs 2 + 2)
+ let ofs := align ofs 2 in
+ (if zle 0 ofs then S Outgoing ofs Tfloat else R (freg_param ofs))
+ :: loc_arguments_rec tys (ofs + 2)
+ | Tlong :: tys =>
+ let ofs := align ofs 2 in
+ (if zle 0 ofs then S Outgoing (ofs + 1) Tint else R (ireg_param (ofs + 1)))
+ :: (if zle 0 ofs then S Outgoing ofs Tint else R (ireg_param ofs))
+ :: loc_arguments_rec tys (ofs + 2)
end.
(** [loc_arguments s] returns the list of locations where to store arguments
@@ -342,7 +305,7 @@ Fixpoint size_arguments_rec (tyl: list typ) (ofs: Z) {struct tyl} : Z :=
match tyl with
| nil => ofs
| Tint :: tys => size_arguments_rec tys (ofs + 1)
- | Tfloat :: tys => size_arguments_rec tys (align ofs 2 + 2)
+ | (Tfloat | Tlong) :: tys => size_arguments_rec tys (align ofs 2 + 2)
end.
Definition size_arguments (s: signature) : Z :=
@@ -353,109 +316,85 @@ Definition size_arguments (s: signature) : Z :=
Definition loc_argument_acceptable (l: loc) : Prop :=
match l with
- | R r => ~(In l temporaries)
- | S (Outgoing ofs ty) => ofs >= 0
+ | R r => In r destroyed_at_call
+ | S Outgoing ofs ty => ofs >= 0 /\ ty <> Tlong
| _ => False
end.
+(*
Lemma align_monotone:
forall x1 x2 y, y > 0 -> x1 <= x2 -> align x1 y <= align x2 y.
Proof.
intros. unfold align. apply Zmult_le_compat_r. apply Z_div_le.
omega. omega. omega.
Qed.
+*)
+
+Remark ireg_param_caller_save:
+ forall n, In (ireg_param n) destroyed_at_call.
+Proof.
+ unfold ireg_param; intros.
+ destruct (zeq n (-4)). simpl; auto.
+ destruct (zeq n (-3)). simpl; auto.
+ destruct (zeq n (-2)); simpl; auto.
+Qed.
+
+Remark freg_param_caller_save:
+ forall n, In (freg_param n) destroyed_at_call.
+Proof.
+ unfold freg_param; intros. destruct (zeq n (-4)); simpl; OrEq.
+Qed.
Remark loc_arguments_rec_charact:
forall tyl ofs l,
In l (loc_arguments_rec tyl ofs) ->
match l with
- | R r =>
- (exists n, ofs <= n < 0 /\ r = ireg_param n)
- \/ (exists n, ofs <= n < -1 /\ r = freg_param n)
- | S (Outgoing ofs' ty) => ofs' >= 0 /\ ofs' >= ofs
- | S _ => False
+ | R r => In r destroyed_at_call
+ | S Outgoing ofs' ty => ofs' >= 0 /\ ofs <= ofs' /\ ty <> Tlong
+ | S _ _ _ => False
end.
Proof.
induction tyl; simpl loc_arguments_rec; intros.
elim H.
- destruct a; elim H; intro.
- subst l. destruct (zle 0 ofs). omega.
- left. exists ofs; split; auto; omega.
- generalize (IHtyl _ _ H0).
- destruct l. intros [[n A] | [n A]]; [left|right]; exists n; intuition omega.
- destruct s; auto; omega.
- subst l. destruct (zle (-1) ofs).
- split. apply Zle_ge. change 0 with (align (-1) 2). apply align_monotone; omega.
- apply Zle_ge. apply align_le. omega.
- right. exists ofs. intuition.
+ destruct a.
+- (* Tint *)
+ destruct H.
+ subst l. destruct (zle 0 ofs).
+ split. omega. split. omega. congruence.
+ apply ireg_param_caller_save.
+ exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
+- (* Tfloat *)
assert (ofs <= align ofs 2) by (apply align_le; omega).
- generalize (IHtyl _ _ H0).
- destruct l. intros [[n A] | [n A]]; [left|right]; exists n; intuition omega.
- destruct s; auto; omega.
-Qed.
-
-Lemma loc_notin_in_diff:
- forall l ll,
- Loc.notin l ll <-> (forall l', In l' ll -> Loc.diff l l').
-Proof.
- induction ll; simpl; intuition. subst l'. auto.
-Qed.
-
-Remark loc_arguments_rec_notin_local:
- forall tyl ofs ofs0 ty0,
- Loc.notin (S (Local ofs0 ty0)) (loc_arguments_rec tyl ofs).
-Proof.
- intros. rewrite loc_notin_in_diff. intros.
- exploit loc_arguments_rec_charact; eauto.
- destruct l'; intros; simpl; auto. destruct s; auto; contradiction.
+ destruct H.
+ subst l. destruct (zle 0 (align ofs 2)).
+ split. omega. split. auto. congruence.
+ apply freg_param_caller_save.
+ exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
+- (* Tlong *)
+ assert (ofs <= align ofs 2) by (apply align_le; omega).
+ destruct H.
+ subst l. destruct (zle 0 (align ofs 2)).
+ split. omega. split. omega. congruence.
+ apply ireg_param_caller_save.
+ destruct H.
+ subst l. destruct (zle 0 (align ofs 2)).
+ split. omega. split. omega. congruence.
+ apply ireg_param_caller_save.
+ exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
Qed.
Lemma loc_arguments_acceptable:
forall (s: signature) (r: loc),
In r (loc_arguments s) -> loc_argument_acceptable r.
Proof.
- unfold loc_arguments; intros.
+ unfold loc_arguments, loc_argument_acceptable; intros.
generalize (loc_arguments_rec_charact _ _ _ H).
- destruct r; simpl.
- intros [[n [A B]] | [n [A B]]]; subst m.
- functional induction (ireg_param n); intuition congruence.
- functional induction (freg_param n); intuition congruence.
- destruct s0; tauto.
+ destruct r; auto.
+ destruct sl; auto.
+ tauto.
Qed.
Hint Resolve loc_arguments_acceptable: locs.
-(** Arguments are parwise disjoint (in the sense of [Loc.norepet]). *)
-
-Lemma loc_arguments_norepet:
- forall (s: signature), Loc.norepet (loc_arguments s).
-Proof.
- unfold loc_arguments; intros.
- assert (forall tyl ofs, -4 <= ofs -> Loc.norepet (loc_arguments_rec tyl ofs)).
- induction tyl; simpl; intros.
- constructor.
- destruct a; constructor.
- rewrite loc_notin_in_diff. intros. exploit loc_arguments_rec_charact; eauto.
- destruct (zle 0 ofs); destruct l'; simpl; auto.
- destruct s0; intuition.
- intros [[n [A B]] | [n [A B]]]; subst m.
- functional induction (ireg_param ofs); functional induction (ireg_param n); congruence || omegaContradiction.
- functional induction (ireg_param ofs); functional induction (freg_param n); congruence || omegaContradiction.
- apply IHtyl. omega.
- rewrite loc_notin_in_diff. intros. exploit loc_arguments_rec_charact; eauto.
- destruct (zle (-1) ofs); destruct l'; simpl; auto.
- destruct s0; intuition.
- intros [[n [A B]] | [n [A B]]]; subst m.
- functional induction (freg_param ofs); functional induction (ireg_param n); congruence || omegaContradiction.
- functional induction (freg_param ofs); functional induction (freg_param n); try (congruence || omegaContradiction).
- compute in A. intuition.
- compute in A. intuition.
- compute in A. intuition.
- compute in A. intuition.
- compute in A. intuition.
- apply IHtyl. assert (ofs <= align ofs 2) by (apply align_le; omega). omega.
- apply H. omega.
-Qed.
-
(** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
Remark size_arguments_rec_above:
@@ -468,6 +407,8 @@ Proof.
apply Zle_trans with (ofs + 1); auto; omega.
assert (ofs <= align ofs 2) by (apply align_le; omega).
apply Zle_trans with (align ofs 2 + 2); auto; omega.
+ assert (ofs <= align ofs 2) by (apply align_le; omega).
+ apply Zle_trans with (align ofs 2 + 2); auto; omega.
Qed.
Lemma size_arguments_above:
@@ -478,79 +419,35 @@ Qed.
Lemma loc_arguments_bounded:
forall (s: signature) (ofs: Z) (ty: typ),
- In (S (Outgoing ofs ty)) (loc_arguments s) ->
+ In (S Outgoing ofs ty) (loc_arguments s) ->
ofs + typesize ty <= size_arguments s.
Proof.
intros.
assert (forall tyl ofs0,
0 <= ofs0 ->
ofs0 <= Zmax 0 (size_arguments_rec tyl ofs0)).
+ {
intros. generalize (size_arguments_rec_above tyl ofs0). intros.
- rewrite Zmax_spec. rewrite zlt_false. auto. omega.
+ rewrite Zmax_spec. rewrite zlt_false. auto. omega.
+ }
assert (forall tyl ofs0,
- In (S (Outgoing ofs ty)) (loc_arguments_rec tyl ofs0) ->
+ In (S Outgoing ofs ty) (loc_arguments_rec tyl ofs0) ->
ofs + typesize ty <= Zmax 0 (size_arguments_rec tyl ofs0)).
- induction tyl; simpl; intros.
- elim H1.
- destruct a; elim H1; intros.
- destruct (zle 0 ofs0); inv H2. apply H0. omega. auto.
- destruct (zle (-1) ofs0); inv H2. apply H0.
- assert (align (-1) 2 <= align ofs0 2). apply align_monotone. omega. auto.
- change (align (-1) 2) with 0 in H2. omega.
- auto.
-
+ {
+ induction tyl; simpl; intros.
+ elim H1.
+ destruct a.
+ - (* Tint *)
+ destruct H1; auto. destruct (zle 0 ofs0); inv H1. apply H0. omega.
+ - (* Tfloat *)
+ destruct H1; auto. destruct (zle 0 (align ofs0 2)); inv H1. apply H0. omega.
+ - (* Tlong *)
+ destruct H1.
+ destruct (zle 0 (align ofs0 2)); inv H1.
+ eapply Zle_trans. 2: apply H0. simpl typesize; omega. omega.
+ destruct H1; auto.
+ destruct (zle 0 (align ofs0 2)); inv H1.
+ eapply Zle_trans. 2: apply H0. simpl typesize; omega. omega.
+ }
unfold size_arguments. apply H1. auto.
Qed.
-
-(** Temporary registers do not overlap with argument locations. *)
-
-Lemma loc_arguments_not_temporaries:
- forall sig, Loc.disjoint (loc_arguments sig) temporaries.
-Proof.
- intros; red; intros x1 x2 A B.
- exploit loc_arguments_acceptable; eauto. unfold loc_argument_acceptable.
- destruct x1; intros. simpl. destruct x2; auto. intuition congruence.
- destruct s; try contradiction. revert B. simpl. ElimOrEq; auto.
-Qed.
-Hint Resolve loc_arguments_not_temporaries: locs.
-
-(** Argument registers are caller-save. *)
-
-Lemma arguments_caller_save:
- forall sig r,
- In (R r) (loc_arguments sig) -> In (R r) destroyed_at_call.
-Proof.
- unfold loc_arguments; intros.
- destruct (loc_arguments_rec_charact _ _ _ H) as [[n [A B]] | [n [A B]]]; subst r.
- functional induction (ireg_param n); simpl; auto. omegaContradiction.
- functional induction (freg_param n); simpl; auto 10.
-Qed.
-
-(** Argument locations agree in number with the function signature. *)
-
-Lemma loc_arguments_length:
- forall sig,
- List.length (loc_arguments sig) = List.length sig.(sig_args).
-Proof.
- assert (forall tyl ofs, List.length (loc_arguments_rec tyl ofs) = List.length tyl).
- induction tyl; simpl; intros.
- auto.
- destruct a; simpl; decEq; auto.
-
- intros. unfold loc_arguments. auto.
-Qed.
-
-(** Argument locations agree in types with the function signature. *)
-
-Lemma loc_arguments_type:
- forall sig, List.map Loc.type (loc_arguments sig) = sig.(sig_args).
-Proof.
- assert (forall tyl ofs, List.map Loc.type (loc_arguments_rec tyl ofs) = tyl).
- induction tyl; simpl; intros.
- auto.
- destruct a; simpl; decEq; auto.
- destruct (zle 0 ofs). auto. functional induction (ireg_param ofs); auto.
- destruct (zle (-1) ofs). auto. functional induction (freg_param ofs); auto.
-
- intros. unfold loc_arguments. apply H.
-Qed.
diff --git a/arm/linux/Stacklayout.v b/arm/linux/Stacklayout.v
index d84da6b..7694dcf 100644
--- a/arm/linux/Stacklayout.v
+++ b/arm/linux/Stacklayout.v
@@ -18,11 +18,8 @@ Require Import Bounds.
(** The general shape of activation records is as follows,
from bottom (lowest offsets) to top:
- Space for outgoing arguments to function calls.
-- Local stack slots of integer type.
+- Local stack slots.
- Saved values of integer callee-save registers used by the function.
-- One word of padding, if necessary to align the following data
- on a 8-byte boundary.
-- Local stack slots of float type.
- Saved values of float callee-save registers used by the function.
- Saved return address into caller.
- Pointer to activation record of the caller.
@@ -38,10 +35,9 @@ Record frame_env : Type := mk_frame_env {
fe_size: Z;
fe_ofs_link: Z;
fe_ofs_retaddr: Z;
- fe_ofs_int_local: Z;
+ fe_ofs_local: Z;
fe_ofs_int_callee_save: Z;
fe_num_int_callee_save: Z;
- fe_ofs_float_local: Z;
fe_ofs_float_callee_save: Z;
fe_num_float_callee_save: Z;
fe_stack_data: Z
@@ -51,18 +47,17 @@ Record frame_env : Type := mk_frame_env {
function. *)
Definition make_env (b: bounds) :=
- let oil := 4 * b.(bound_outgoing) in (* integer locals *)
- let oics := oil + 4 * b.(bound_int_local) in (* integer callee-saves *)
+ let ol := align (4 * b.(bound_outgoing)) 8 in (* locals *)
+ let oics := ol + 4 * b.(bound_local) in (* integer callee-saves *)
let oendi := oics + 4 * b.(bound_int_callee_save) in
- let ofl := align oendi 8 in (* float locals *)
- let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *)
+ let ofcs := align oendi 8 in (* float callee-saves *)
let ora := ofcs + 8 * b.(bound_float_callee_save) in (* retaddr *)
let olink := ora + 4 in (* back link *)
let ostkdata := olink + 4 in (* stack data *)
let sz := align (ostkdata + b.(bound_stack_data)) 8 in
- mk_frame_env sz olink ora
- oil oics b.(bound_int_callee_save)
- ofl ofcs b.(bound_float_callee_save)
+ mk_frame_env sz olink ora ol
+ oics b.(bound_int_callee_save)
+ ofcs b.(bound_float_callee_save)
ostkdata.
(** Separation property *)
@@ -71,26 +66,24 @@ Remark frame_env_separated:
forall b,
let fe := make_env b in
0 <= fe_ofs_arg
- /\ fe_ofs_arg + 4 * b.(bound_outgoing) <= fe.(fe_ofs_int_local)
- /\ fe.(fe_ofs_int_local) + 4 * b.(bound_int_local) <= fe.(fe_ofs_int_callee_save)
- /\ fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save) <= fe.(fe_ofs_float_local)
- /\ fe.(fe_ofs_float_local) + 8 * b.(bound_float_local) <= fe.(fe_ofs_float_callee_save)
+ /\ fe_ofs_arg + 4 * b.(bound_outgoing) <= fe.(fe_ofs_local)
+ /\ fe.(fe_ofs_local) + 4 * b.(bound_local) <= fe.(fe_ofs_int_callee_save)
+ /\ fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save) <= fe.(fe_ofs_float_callee_save)
/\ fe.(fe_ofs_float_callee_save) + 8 * b.(bound_float_callee_save) <= fe.(fe_ofs_retaddr)
/\ fe.(fe_ofs_retaddr) + 4 <= fe.(fe_ofs_link)
/\ fe.(fe_ofs_link) + 4 <= fe.(fe_stack_data)
/\ fe.(fe_stack_data) + b.(bound_stack_data) <= fe.(fe_size).
Proof.
intros.
- generalize (align_le (fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save)) 8 (refl_equal _)).
- generalize (align_le (fe.(fe_stack_data) + b.(bound_stack_data)) 8 (refl_equal _)).
+ generalize (align_le (4 * bound_outgoing b) 8 (refl_equal)).
+ generalize (align_le (fe_ofs_int_callee_save fe + 4 * b.(bound_int_callee_save)) 8 (refl_equal _)).
+ generalize (align_le (fe_stack_data fe + b.(bound_stack_data)) 8 (refl_equal)).
unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr,
- fe_ofs_int_local, fe_ofs_int_callee_save,
- fe_num_int_callee_save,
- fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save,
+ fe_ofs_local, fe_ofs_int_callee_save, fe_num_int_callee_save,
+ fe_ofs_float_callee_save, fe_num_float_callee_save,
fe_stack_data, fe_ofs_arg.
intros.
- generalize (bound_int_local_pos b); intro;
- generalize (bound_float_local_pos b); intro;
+ generalize (bound_local_pos b); intro;
generalize (bound_int_callee_save_pos b); intro;
generalize (bound_float_callee_save_pos b); intro;
generalize (bound_outgoing_pos b); intro;
@@ -104,9 +97,8 @@ Remark frame_env_aligned:
forall b,
let fe := make_env b in
(4 | fe.(fe_ofs_link))
- /\ (4 | fe.(fe_ofs_int_local))
+ /\ (8 | fe.(fe_ofs_local))
/\ (4 | fe.(fe_ofs_int_callee_save))
- /\ (8 | fe.(fe_ofs_float_local))
/\ (8 | fe.(fe_ofs_float_callee_save))
/\ (4 | fe.(fe_ofs_retaddr))
/\ (8 | fe.(fe_stack_data))
@@ -114,30 +106,27 @@ Remark frame_env_aligned:
Proof.
intros.
unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr,
- fe_ofs_int_local, fe_ofs_int_callee_save,
- fe_num_int_callee_save,
- fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save,
+ fe_ofs_local, fe_ofs_int_callee_save, fe_num_int_callee_save,
+ fe_ofs_float_callee_save, fe_num_float_callee_save,
fe_stack_data.
set (x1 := 4 * bound_outgoing b).
assert (4 | x1). unfold x1; exists (bound_outgoing b); ring.
- set (x2 := x1 + 4 * bound_int_local b).
- assert (4 | x2). unfold x2; apply Zdivide_plus_r; auto. exists (bound_int_local b); ring.
- set (x3 := x2 + 4 * bound_int_callee_save b).
- set (x4 := align x3 8).
- assert (8 | x4). unfold x4. apply align_divides. omega.
- set (x5 := x4 + 8 * bound_float_local b).
- assert (8 | x5). unfold x5. apply Zdivide_plus_r; auto. exists (bound_float_local b); ring.
- set (x6 := x5 + 8 * bound_float_callee_save b).
- assert (8 | x6).
- unfold x6. apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring.
- assert (4 | x6).
- apply Zdivides_trans with 8. exists 2; auto. auto.
+ set (x2 := align x1 8).
+ assert (8 | x2). apply align_divides. omega.
+ set (x3 := x2 + 4 * bound_local b).
+ assert (4 | x3). apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto.
+ exists (bound_local b); ring.
+ set (x4 := align (x3 + 4 * bound_int_callee_save b) 8).
+ assert (8 | x4). apply align_divides. omega.
+ set (x5 := x4 + 8 * bound_float_callee_save b).
+ assert (8 | x5). apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring.
+ assert (4 | x5). apply Zdivides_trans with 8; auto. exists 2; auto.
+ set (x6 := x5 + 4).
+ assert (4 | x6). apply Zdivide_plus_r; auto. exists 1; auto.
set (x7 := x6 + 4).
- assert (4 | x7). unfold x7; apply Zdivide_plus_r; auto. exists 1; auto.
- set (x8 := x7 + 4).
- assert (8 | x8). unfold x8, x7. replace (x6 + 4 + 4) with (x6 + 8) by omega.
- apply Zdivide_plus_r; auto. exists 1; auto.
- set (x9 := align (x8 + bound_stack_data b) 8).
- assert (8 | x9). unfold x9; apply align_divides. omega.
+ assert (8 | x7). unfold x7, x6. replace (x5 + 4 + 4) with (x5 + 8) by omega.
+ apply Zdivide_plus_r; auto. exists 1; auto.
+ set (x8 := align (x7 + bound_stack_data b) 8).
+ assert (8 | x8). apply align_divides. omega.
tauto.
Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-04 07:39:30 +0000