aboutsummaryrefslogtreecommitdiffstats
path: root/arm
diff options
context:
space:
mode:
Diffstat (limited to 'arm')
-rw-r--r--arm/Asm.v2
-rw-r--r--arm/Asmgenproof1.v24
-rw-r--r--arm/ConstpropOp.vp8
-rw-r--r--arm/ConstpropOpproof.v2
-rw-r--r--arm/Conventions1.v7
-rw-r--r--arm/Op.v4
-rw-r--r--arm/SelectOp.vp6
-rw-r--r--arm/Stacklayout.v6
8 files changed, 32 insertions, 27 deletions
diff --git a/arm/Asm.v b/arm/Asm.v
index bc5ca1a5..08234975 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -900,7 +900,7 @@ Proof.
{ intros. inv H; inv H0; congruence. }
assert (B: forall p v1 v2,
extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).
- { intros. inv H; inv H0.
+ { intros. inv H; inv H0.
eapply A; eauto.
f_equal; eapply A; eauto. }
assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 252a294a..eec531dc 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -30,7 +30,7 @@ Require Import Asmgen.
Require Import Conventions.
Require Import Asmgenproof0.
-Local Transparent Archi.ptr64.
+Local Transparent Archi.ptr64.
(** Useful properties of the R14 registers. *)
@@ -530,7 +530,7 @@ Lemma loadind_int_correct:
Proof.
intros; unfold loadind_int.
assert (Val.offset_ptr (rs base) ofs = Val.add (rs base) (Vint (Ptrofs.to_int ofs))).
- { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. }
+ { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. }
apply indexed_memory_access_correct; intros.
econstructor; split.
apply exec_straight_one. simpl. unfold exec_load. rewrite H1, <- H0, H. eauto. auto.
@@ -546,9 +546,9 @@ Lemma loadind_correct:
/\ rs'#(preg_of dst) = v
/\ forall r, if_preg r = true -> r <> IR14 -> r <> preg_of dst -> rs'#r = rs#r.
Proof.
- unfold loadind; intros.
+ unfold loadind; intros.
assert (Val.offset_ptr (rs base) ofs = Val.add (rs base) (Vint (Ptrofs.to_int ofs))).
- { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. }
+ { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. }
destruct ty; destruct (preg_of dst); inv H; simpl in H0.
- (* int *)
apply loadind_int_correct; auto.
@@ -587,32 +587,32 @@ Proof.
unfold storeind; intros.
assert (DATA: data_preg (preg_of src) = true) by eauto with asmgen.
assert (Val.offset_ptr (rs base) ofs = Val.add (rs base) (Vint (Ptrofs.to_int ofs))).
- { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. }
+ { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. }
destruct ty; destruct (preg_of src); inv H; simpl in H0.
- (* int *)
apply indexed_memory_access_correct; intros.
econstructor; split.
- apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto.
+ apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto.
intros; Simpl.
- (* float *)
apply indexed_memory_access_correct; intros.
econstructor; split.
- apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto.
+ apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto.
intros; Simpl.
- (* single *)
apply indexed_memory_access_correct; intros.
econstructor; split.
- apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto.
+ apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto.
intros; Simpl.
- (* any32 *)
apply indexed_memory_access_correct; intros.
econstructor; split.
- apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto.
+ apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto.
intros; Simpl.
- (* any64 *)
apply indexed_memory_access_correct; intros.
econstructor; split.
- apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto.
+ apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto.
intros; Simpl.
Qed.
@@ -1306,7 +1306,7 @@ Proof.
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 -> preg_notin r (destroyed_by_op op) -> rs'#r = rs#r).
- { intros (rs' & A & B & C). subst v; exists rs'; auto. }
+ { intros (rs' & A & B & C). subst v; exists rs'; auto. }
destruct op; try (apply SAME; eapply transl_op_correct_same; eauto; fail).
- (* Oaddrstack *)
clear SAME; simpl in *; ArgsInv.
@@ -1372,7 +1372,7 @@ Proof.
erewrite ! ireg_of_eq; eauto. rewrite transl_shift_correct. auto.
(* Ainstack *)
inv TR. apply indexed_memory_access_correct. intros. eapply MK1; eauto.
- rewrite H. destruct (rs IR13); try contradiction. simpl. f_equal; f_equal. auto with ptrofs.
+ rewrite H. destruct (rs IR13); try contradiction. simpl. f_equal; f_equal. auto with ptrofs.
Qed.
Lemma transl_load_int_correct:
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index e0f0889f..cb7a73eb 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -10,7 +10,7 @@
(* *)
(* *********************************************************************)
-(** Static analysis and strength reduction for operators
+(** Static analysis and strength reduction for operators
and conditions. This is the machine-dependent part of [Constprop]. *)
Require Import Coqlib.
@@ -51,7 +51,7 @@ Definition eval_static_shift (s: shift) (n: int) : int :=
| Sror x => Int.ror n x
end.
-Nondetfunction cond_strength_reduction
+Nondetfunction cond_strength_reduction
(cond: condition) (args: list reg) (vl: list aval) :=
match cond, args, vl with
| Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil =>
@@ -98,7 +98,7 @@ Nondetfunction cond_strength_reduction
if Float32.eq_dec n2 Float32.zero
then (Cnotcompfszero c, r1 :: nil)
else (cond, args)
- | _, _, _ =>
+ | _, _, _ =>
(cond, args)
end.
@@ -206,7 +206,7 @@ Definition make_cast8signed (r: reg) (a: aval) :=
Definition make_cast16signed (r: reg) (a: aval) :=
if vincl a (Sgn Ptop 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil).
-Nondetfunction op_strength_reduction
+Nondetfunction op_strength_reduction
(op: operation) (args: list reg) (vl: list aval) :=
match op, args, vl with
| Ocast8signed, r1 :: nil, v1 :: nil => make_cast8signed r1 v1
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index e1ae80a2..c9f97aa8 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -116,7 +116,7 @@ Proof.
+ (* global *)
inv H2. exists (Genv.symbol_address ge id ofs); auto.
+ (* stack *)
- inv H2. exists (Vptr sp ofs); split; auto. simpl. rewrite Ptrofs.add_zero_l; auto.
+ inv H2. exists (Vptr sp ofs); split; auto. simpl. rewrite Ptrofs.add_zero_l; auto.
Qed.
Lemma eval_static_shift_correct:
diff --git a/arm/Conventions1.v b/arm/Conventions1.v
index ecf03e1d..86be8c95 100644
--- a/arm/Conventions1.v
+++ b/arm/Conventions1.v
@@ -60,6 +60,8 @@ Definition destroyed_at_call :=
Definition dummy_int_reg := R0. (**r Used in [Coloring]. *)
Definition dummy_float_reg := F0. (**r Used in [Coloring]. *)
+Definition callee_save_type := mreg_type.
+
Definition is_float_reg (r: mreg): bool :=
match r with
| R0 | R1 | R2 | R3
@@ -136,7 +138,10 @@ Lemma loc_result_pair:
forall sg,
match loc_result sg with
| One _ => True
- | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.splitlong = true
+ | Twolong r1 r2 =>
+ r1 <> r2 /\ sg.(sig_res) = Some 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.
diff --git a/arm/Op.v b/arm/Op.v
index 0d31c2ac..2e919758 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -1102,7 +1102,7 @@ Proof.
rewrite eval_shift_stack_addressing.
eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto.
intros. apply symbol_address_inject.
- econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
+ econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
Qed.
Lemma eval_operation_inject:
@@ -1122,7 +1122,7 @@ Proof.
intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
intros; eapply Mem.different_pointers_inject; eauto.
intros; apply symbol_address_inject.
- econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
+ econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
Qed.
End EVAL_INJECT.
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 4ea1e1a1..fc2fbe6b 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -199,7 +199,7 @@ Definition mulhu (e1: expr) (e2: expr) := Eop Omulhu (e1 ::: e2 ::: Enil).
(** ** Bitwise and, or, xor *)
-Nondetfunction andimm (n1: int) (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
@@ -343,14 +343,14 @@ Nondetfunction compimm (default: comparison -> int -> condition)
Eop (Ocmp (negate_condition c)) el
else if Int.eq_dec n2 Int.one then
Eop (Ocmp c) el
- else
+ else
Eop (Ointconst Int.zero) Enil
| Cne, Eop (Ocmp c) el =>
if Int.eq_dec n2 Int.zero then
Eop (Ocmp c) el
else if Int.eq_dec n2 Int.one then
Eop (Ocmp (negate_condition c)) el
- else
+ else
Eop (Ointconst Int.one) Enil
| _, _ =>
Eop (Ocmp (default c n2)) (e1 ::: Enil)
diff --git a/arm/Stacklayout.v b/arm/Stacklayout.v
index f5c07fff..c867ba59 100644
--- a/arm/Stacklayout.v
+++ b/arm/Stacklayout.v
@@ -86,16 +86,16 @@ Local Opaque Z.add Z.mul sepconj range.
retaddr
back link *)
rewrite sep_swap12.
- rewrite sep_swap45.
+ rewrite sep_swap45.
rewrite sep_swap34.
rewrite sep_swap45.
(* Apply range_split and range_split2 repeatedly *)
unfold fe_ofs_arg.
apply range_split_2. fold ol; omega. omega.
- apply range_split. omega.
+ apply range_split. omega.
apply range_split_2. fold ora; omega. omega.
apply range_split. omega.
- apply range_drop_right with ostkdata. omega.
+ apply range_drop_right with ostkdata. omega.
eapply sep_drop2. eexact H.
Qed.
generated by cgit (git 2.34.1) at 2024-06-28 23:34:19 +0000