summaryrefslogtreecommitdiff
path: root/arm
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-04-09 16:59:13 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-04-09 16:59:13 +0000
commitabe2bb5c40260a31ce5ee27b841bcbd647ff8b88 (patch)
treeae109a136508da283a9e2be5f039c5f9cca4f95c /arm
parentffd6080f9e1e742c73ac38354b31c6fc4e3963ba (diff)
Merge of branch "unsigned-offsets":
- In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm')
-rw-r--r--arm/Asm.v26
-rw-r--r--arm/Asmgen.v102
-rw-r--r--arm/Asmgenproof.v161
-rw-r--r--arm/Asmgenproof1.v473
-rw-r--r--arm/Asmgenretaddr.v32
-rw-r--r--arm/ConstpropOpproof.v111
-rw-r--r--arm/Op.v322
-rw-r--r--arm/PrintAsm.ml31
-rw-r--r--arm/SelectOp.v2
-rw-r--r--arm/SelectOpproof.v85
-rw-r--r--arm/linux/Stacklayout.v88
11 files changed, 913 insertions, 520 deletions
diff --git a/arm/Asm.v b/arm/Asm.v
index 7ea1a8a..051b7e4 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -165,8 +165,8 @@ Inductive instruction : Type :=
| Psufd: freg -> freg -> freg -> instruction (**r float subtraction *)
(* Pseudo-instructions *)
- | Pallocframe: Z -> Z -> int -> instruction (**r allocate new stack frame *)
- | Pfreeframe: Z -> Z -> int -> instruction (**r deallocate stack frame and restore previous frame *)
+ | Pallocframe: Z -> int -> instruction (**r allocate new stack frame *)
+ | Pfreeframe: Z -> int -> instruction (**r deallocate stack frame and restore previous frame *)
| 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 *)
@@ -186,20 +186,20 @@ lbl: .word symbol
>>
Initialized data in the constant data section are not modeled here,
which is why we use a pseudo-instruction for this purpose.
-- [Pallocframe lo hi pos]: in the formal semantics, this pseudo-instruction
- allocates a memory block with bounds [lo] and [hi], stores the value
+- [Pallocframe sz pos]: in the formal semantics, this pseudo-instruction
+ allocates a memory block with bounds [0] and [sz], stores the value
of the stack pointer at offset [pos] in this block, and sets the
stack pointer to the address of the bottom of this block.
In the printed ASM assembly code, this allocation is:
<<
mov r12, sp
- sub sp, sp, #(hi - lo)
+ sub sp, sp, #sz
str r12, [sp, #pos]
>>
This cannot be expressed in our memory model, which does not reflect
the fact that stack frames are adjacent and allocated/freed
following a stack discipline.
-- [Pfreeframe pos]: in the formal semantics, this pseudo-instruction
+- [Pfreeframe sz pos]: in the formal semantics, this pseudo-instruction
reads the word at [pos] of the block pointed by the stack pointer,
frees this block, and sets the stack pointer to the value read.
In the printed ASM assembly code, this freeing
@@ -494,20 +494,20 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
| Psufd r1 r2 r3 =>
OK (nextinstr (rs#r1 <- (Val.subf rs#r2 rs#r3))) m
(* Pseudo-instructions *)
- | Pallocframe lo hi pos =>
- let (m1, stk) := Mem.alloc m lo hi in
- let sp := (Vptr stk (Int.repr lo)) in
+ | Pallocframe sz pos =>
+ let (m1, stk) := Mem.alloc m 0 sz in
+ let sp := (Vptr stk Int.zero) in
match Mem.storev Mint32 m1 (Val.add sp (Vint pos)) rs#IR13 with
| None => Error
- | Some m2 => OK (nextinstr (rs#IR13 <- sp)) m2
+ | Some m2 => OK (nextinstr (rs #IR12 <- (rs#IR13) #IR13 <- sp)) m2
end
- | Pfreeframe lo hi pos =>
+ | Pfreeframe sz pos =>
match Mem.loadv Mint32 m (Val.add rs#IR13 (Vint pos)) with
| None => Error
| Some v =>
match rs#IR13 with
| Vptr stk ofs =>
- match Mem.free m stk lo hi with
+ match Mem.free m stk 0 sz with
| None => Error
| Some m' => OK (nextinstr (rs#IR13 <- v)) m'
end
@@ -521,7 +521,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
| Pbtbl r tbl =>
match rs#r with
| Vint n =>
- let pos := Int.signed n in
+ let pos := Int.unsigned n in
if zeq (Zmod pos 4) 0 then
match list_nth_z tbl (pos / 4) with
| None => Error
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index b3412fb..a1f8d96 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -36,7 +36,7 @@ Require Import Asm.
Fixpoint is_immed_arith_aux (n: nat) (x msk: int) {struct n}: bool :=
match n with
- | O => false
+ | Datatypes.O => false
| Datatypes.S n' =>
Int.eq (Int.and x (Int.not msk)) Int.zero ||
is_immed_arith_aux n' x (Int.ror msk (Int.repr 2))
@@ -55,46 +55,65 @@ Definition is_immed_mem_float (x: int) : bool :=
Int.eq (Int.and x (Int.repr 3)) Int.zero
&& Int.lt x (Int.repr 1024) && Int.lt (Int.repr (-1024)) x.
+(** Decomposition of a 32-bit integer into a list of immediate arguments,
+ whose sum or "or" or "xor" equals the integer. *)
+
+Fixpoint decompose_int_rec (N: nat) (n p: int) : list int :=
+ match N with
+ | Datatypes.O =>
+ if Int.eq_dec n Int.zero then nil else n :: nil
+ | Datatypes.S M =>
+ if Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero then
+ decompose_int_rec M n (Int.add p (Int.repr 2))
+ else
+ let m := Int.shl (Int.repr 255) p in
+ Int.and n m ::
+ decompose_int_rec M (Int.and n (Int.not m)) (Int.add p (Int.repr 2))
+ end.
+
+Definition decompose_int (n: int) : list int :=
+ match decompose_int_rec 12%nat n Int.zero with
+ | nil => Int.zero :: nil
+ | l => l
+ end.
+
+Definition iterate_op (op1 op2: shift_op -> instruction) (l: list int) (k: code) :=
+ match l with
+ | nil =>
+ op1 (SOimm Int.zero) :: k (**r should never happen *)
+ | i :: l' =>
+ op1 (SOimm i) :: map (fun i => op2 (SOimm i)) l' ++ k
+ end.
+
(** Smart constructors for integer immediate arguments. *)
Definition loadimm (r: ireg) (n: int) (k: code) :=
- if is_immed_arith n then
- Pmov r (SOimm n) :: k
- else if is_immed_arith (Int.not n) then
- Pmvn r (SOimm (Int.not n)) :: k
- else (* could be much improved! *)
- Pmov r (SOimm (Int.and n (Int.repr 255))) ::
- Porr r r (SOimm (Int.and n (Int.repr 65280))) ::
- Porr r r (SOimm (Int.and n (Int.repr 16711680))) ::
- Porr r r (SOimm (Int.and n (Int.repr 4278190080))) ::
- k.
+ let d1 := decompose_int n in
+ let d2 := decompose_int (Int.not n) in
+ if le_dec (List.length d1) (List.length d2)
+ then iterate_op (Pmov r) (Porr r r) d1 k
+ else iterate_op (Pmvn r) (Pbic r r) d2 k.
Definition addimm (r1 r2: ireg) (n: int) (k: code) :=
- if is_immed_arith n then
- Padd r1 r2 (SOimm n) :: k
- else if is_immed_arith (Int.neg n) then
- Psub r1 r2 (SOimm (Int.neg n)) :: k
- else
- Padd r1 r2 (SOimm (Int.and n (Int.repr 255))) ::
- Padd r1 r1 (SOimm (Int.and n (Int.repr 65280))) ::
- Padd r1 r1 (SOimm (Int.and n (Int.repr 16711680))) ::
- Padd r1 r1 (SOimm (Int.and n (Int.repr 4278190080))) ::
- k.
+ let d1 := decompose_int n in
+ let d2 := decompose_int (Int.neg n) in
+ if le_dec (List.length d1) (List.length d2)
+ then iterate_op (Padd r1 r2) (Padd r1 r1) d1 k
+ else iterate_op (Psub r1 r2) (Psub r1 r1) d2 k.
Definition andimm (r1 r2: ireg) (n: int) (k: code) :=
- if is_immed_arith n then
- Pand r1 r2 (SOimm n) :: k
- else if is_immed_arith (Int.not n) then
- Pbic r1 r2 (SOimm (Int.not n)) :: k
- else
- loadimm IR14 n (Pand r1 r2 (SOreg IR14) :: k).
+ if is_immed_arith n
+ then Pand r1 r2 (SOimm n) :: k
+ else iterate_op (Pbic r1 r2) (Pbic r1 r1) (decompose_int (Int.not n)) k.
-Definition makeimm (instr: ireg -> ireg -> shift_op -> instruction)
- (r1 r2: ireg) (n: int) (k: code) :=
- if is_immed_arith n then
- instr r1 r2 (SOimm n) :: k
- else
- loadimm IR14 n (instr r1 r2 (SOreg IR14) :: k).
+Definition rsubimm (r1 r2: ireg) (n: int) (k: code) :=
+ iterate_op (Prsb r1 r2) (Padd r1 r1) (decompose_int n) k.
+
+Definition orimm (r1 r2: ireg) (n: int) (k: code) :=
+ iterate_op (Porr r1 r2) (Porr r1 r1) (decompose_int n) k.
+
+Definition xorimm (r1 r2: ireg) (n: int) (k: code) :=
+ iterate_op (Peor r1 r2) (Peor r1 r1) (decompose_int n) k.
(** Translation of a shift immediate operation (type [Op.shift]) *)
@@ -235,7 +254,7 @@ Definition transl_op
| Orsubshift s, a1 :: a2 :: nil =>
Prsb (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
| Orsubimm n, a1 :: nil =>
- makeimm Prsb (ireg_of r) (ireg_of a1) n k
+ rsubimm (ireg_of r) (ireg_of a1) n k
| Omul, a1 :: a2 :: nil =>
if ireg_eq (ireg_of r) (ireg_of a1)
|| ireg_eq (ireg_of r) (ireg_of a2)
@@ -256,13 +275,13 @@ Definition transl_op
| Oorshift s, a1 :: a2 :: nil =>
Porr (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
| Oorimm n, a1 :: nil =>
- makeimm Porr (ireg_of r) (ireg_of a1) n k
+ orimm (ireg_of r) (ireg_of a1) n k
| Oxor, a1 :: a2 :: nil =>
Peor (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k
| Oxorshift s, a1 :: a2 :: nil =>
Peor (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k
| Oxorimm n, a1 :: nil =>
- makeimm Peor (ireg_of r) (ireg_of a1) n k
+ xorimm (ireg_of r) (ireg_of a1) n k
| Obic, a1 :: a2 :: nil =>
Pbic (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k
| Obicshift s, a1 :: a2 :: nil =>
@@ -469,12 +488,10 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
Pblsymb symb :: k
| Mtailcall sig (inl r) =>
loadind_int IR13 f.(fn_retaddr_ofs) IR14
- (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
- :: Pbreg (ireg_of r) :: k)
+ (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg (ireg_of r) :: k)
| Mtailcall sig (inr symb) =>
loadind_int IR13 f.(fn_retaddr_ofs) IR14
- (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
- :: Pbsymb symb :: k)
+ (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbsymb symb :: k)
| Mbuiltin ef args res =>
Pbuiltin ef (map preg_of args) (preg_of res) :: k
| Mlabel lbl =>
@@ -488,8 +505,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
Pbtbl IR14 tbl :: k
| Mreturn =>
loadind_int IR13 f.(fn_retaddr_ofs) IR14
- (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
- :: Pbreg IR14 :: k)
+ (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 :: k)
end.
Definition transl_code (f: Mach.function) (il: list Mach.instruction) :=
@@ -501,7 +517,7 @@ Definition transl_code (f: Mach.function) (il: list Mach.instruction) :=
around, leading to incorrect executions. *)
Definition transl_function (f: Mach.function) :=
- Pallocframe (- f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) ::
+ Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
Pstr IR14 IR13 (SAimm f.(fn_retaddr_ofs)) ::
transl_code f f.(fn_code).
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index d3e082f..0a429cc 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -330,12 +330,26 @@ Section TRANSL_LABEL.
Variable lbl: label.
+Remark iterate_op_label:
+ forall op1 op2 l k,
+ (forall so, is_label lbl (op1 so) = false) ->
+ (forall so, is_label lbl (op2 so) = false) ->
+ find_label lbl (iterate_op op1 op2 l k) = find_label lbl k.
+Proof.
+ intros. unfold iterate_op.
+ destruct l as [ | hd tl].
+ simpl. rewrite H. auto.
+ simpl. rewrite H.
+ induction tl; simpl. auto. rewrite H0; auto.
+Qed.
+Hint Resolve iterate_op_label: labels.
+
Remark loadimm_label:
forall r n k, find_label lbl (loadimm r n k) = find_label lbl k.
Proof.
- intros. unfold loadimm.
- destruct (is_immed_arith n). reflexivity.
- destruct (is_immed_arith (Int.not n)); reflexivity.
+ intros. unfold loadimm.
+ destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.not n))));
+ auto with labels.
Qed.
Hint Rewrite loadimm_label: labels.
@@ -343,9 +357,8 @@ Remark addimm_label:
forall r1 r2 n k, find_label lbl (addimm r1 r2 n k) = find_label lbl k.
Proof.
intros; unfold addimm.
- destruct (is_immed_arith n). reflexivity.
- destruct (is_immed_arith (Int.neg n)). reflexivity.
- autorewrite with labels. reflexivity.
+ destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.neg n))));
+ auto with labels.
Qed.
Hint Rewrite addimm_label: labels.
@@ -353,31 +366,30 @@ Remark andimm_label:
forall r1 r2 n k, find_label lbl (andimm r1 r2 n k) = find_label lbl k.
Proof.
intros; unfold andimm.
- destruct (is_immed_arith n). reflexivity.
- destruct (is_immed_arith (Int.not n)). reflexivity.
- autorewrite with labels. reflexivity.
+ destruct (is_immed_arith n). reflexivity. auto with labels.
Qed.
Hint Rewrite andimm_label: labels.
-Remark makeimm_Prsb_label:
- forall r1 r2 n k, find_label lbl (makeimm Prsb r1 r2 n k) = find_label lbl k.
+Remark rsubimm_label:
+ forall r1 r2 n k, find_label lbl (rsubimm r1 r2 n k) = find_label lbl k.
Proof.
- intros; unfold makeimm.
- destruct (is_immed_arith n). reflexivity. autorewrite with labels; auto.
+ intros; unfold rsubimm. auto with labels.
Qed.
-Remark makeimm_Porr_label:
- forall r1 r2 n k, find_label lbl (makeimm Porr r1 r2 n k) = find_label lbl k.
+Hint Rewrite rsubimm_label: labels.
+
+Remark orimm_label:
+ forall r1 r2 n k, find_label lbl (orimm r1 r2 n k) = find_label lbl k.
Proof.
- intros; unfold makeimm.
- destruct (is_immed_arith n). reflexivity. autorewrite with labels; auto.
+ intros; unfold orimm. auto with labels.
Qed.
-Remark makeimm_Peor_label:
- forall r1 r2 n k, find_label lbl (makeimm Peor r1 r2 n k) = find_label lbl k.
+Hint Rewrite orimm_label: labels.
+
+Remark xorimm_label:
+ forall r1 r2 n k, find_label lbl (xorimm r1 r2 n k) = find_label lbl k.
Proof.
- intros; unfold makeimm.
- destruct (is_immed_arith n). reflexivity. autorewrite with labels; auto.
+ intros; unfold xorimm. auto with labels.
Qed.
-Hint Rewrite makeimm_Prsb_label makeimm_Porr_label makeimm_Peor_label: labels.
+Hint Rewrite xorimm_label: labels.
Remark loadind_int_label:
forall base ofs dst k, find_label lbl (loadind_int base ofs dst k) = find_label lbl k.
@@ -692,7 +704,7 @@ Proof.
rewrite (sp_val _ _ _ AG) in A.
exploit loadind_correct. eexact A. reflexivity.
intros [rs2 [EX [RES OTH]]].
- left; eapply exec_straight_steps; eauto with coqlib.
+ left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto.
exists m'; split; auto.
simpl. exists rs2; split. eauto.
apply agree_set_mreg with rs; auto. congruence. auto with ppcgen.
@@ -715,19 +727,19 @@ Proof.
rewrite (sp_val _ _ _ AG) in B.
exploit storeind_correct. eexact B. reflexivity. congruence.
intros [rs2 [EX OTH]].
- left; eapply exec_straight_steps; eauto with coqlib.
+ left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto.
exists m2; split; auto.
- exists rs2; split; eauto.
+ simpl. exists rs2; split. eauto.
apply agree_exten with rs; auto with ppcgen.
Qed.
Lemma exec_Mgetparam_prop:
- forall (s : list stackframe) (fb : block) (f: Mach.function) (sp parent : val)
+ forall (s : list stackframe) (fb : block) (f: Mach.function) (sp : val)
(ofs : int) (ty : typ) (dst : mreg) (c : list Mach.instruction)
(ms : Mach.regset) (m : mem) (v : val),
Genv.find_funct_ptr ge fb = Some (Internal f) ->
- load_stack m sp Tint f.(fn_link_ofs) = Some parent ->
- load_stack m parent ty ofs = Some v ->
+ load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) ->
+ load_stack m (parent_sp s) ty ofs = Some v ->
exec_instr_prop (Machconcr.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0
(Machconcr.State s fb sp c (Regmap.set dst v (Regmap.set IT1 Vundef ms)) m).
Proof.
@@ -738,18 +750,18 @@ Proof.
unfold load_stack in *.
exploit Mem.loadv_extends. eauto. eexact H0. eauto.
intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A.
- assert (parent' = parent). inv B. auto. simpl in H1; discriminate. subst parent'.
+ assert (parent' = parent_sp s). inv B. auto. rewrite <- H3 in H1; discriminate. subst parent'.
exploit Mem.loadv_extends. eauto. eexact H1. eauto.
intros [v' [C D]].
exploit (loadind_int_correct tge (transl_function f) IR13 f.(fn_link_ofs) IR14
- rs m' parent (loadind IR14 ofs (mreg_type dst) dst (transl_code f c))).
+ rs m' (parent_sp s) (loadind IR14 ofs (mreg_type dst) dst (transl_code f c))).
auto.
intros [rs1 [EX1 [RES1 OTH1]]].
exploit (loadind_correct tge (transl_function f) IR14 ofs (mreg_type dst) dst
(transl_code f c) rs1 m' v').
rewrite RES1. auto. auto.
intros [rs2 [EX2 [RES2 OTH2]]].
- left. eapply exec_straight_steps; eauto with coqlib.
+ left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto.
exists m'; split; auto.
exists rs2; split; simpl.
eapply exec_straight_trans; eauto.
@@ -762,20 +774,20 @@ Lemma exec_Mop_prop:
forall (s : list stackframe) (fb : block) (sp : val) (op : operation)
(args : list mreg) (res : mreg) (c : list Mach.instruction)
(ms : mreg -> val) (m : mem) (v : val),
- eval_operation ge sp op ms ## args = Some v ->
+ eval_operation ge sp op ms ## args m = Some v ->
exec_instr_prop (Machconcr.State s fb sp (Mop op args res :: c) ms m) E0
(Machconcr.State s fb sp c (Regmap.set res v (undef_op op ms)) m).
Proof.
intros; red; intros; inv MS.
generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
intro WTI.
- exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto.
+ exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto.
intros [v' [A B]].
- assert (C: eval_operation tge sp op rs ## (preg_of ## args) = Some v').
+ assert (C: eval_operation tge sp op rs ## (preg_of ## args) m' = Some v').
rewrite <- A. apply eval_operation_preserved. exact symbols_preserved.
rewrite (sp_val _ _ _ AG) in C.
exploit transl_op_correct; eauto. intros [rs' [P [Q R]]].
- left; eapply exec_straight_steps; eauto with coqlib.
+ left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto.
exists m'; split; auto.
exists rs'; split. simpl. eexact P.
assert (agree (Regmap.set res v ms) sp rs').
@@ -809,7 +821,8 @@ Proof.
eauto; intros; reflexivity.
Qed.
-Lemma storev_8_signed_unsigned: forall m a v, Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v. Proof. intros. unfold Mem.storev. destruct a; auto. apply Mem.store_signed_unsigned_8. Qed. Lemma storev_16_signed_unsigned: forall m a v, Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v. Proof. intros. unfold Mem.storev. destruct a; auto. apply Mem.store_signed_unsigned_16. Qed.
+Lemma storev_8_signed_unsigned: forall m a v, Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v. Proof. intros. unfold Mem.storev.
+ destruct a; auto. apply Mem.store_signed_unsigned_8. Qed. Lemma storev_16_signed_unsigned: forall m a v, Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v. Proof. intros. unfold Mem.storev. destruct a; auto. apply Mem.store_signed_unsigned_16. Qed.
Lemma exec_Mstore_prop:
forall (s : list stackframe) (fb : block) (sp : val)
@@ -826,7 +839,7 @@ Proof.
intro WTI; inv WTI.
assert (eval_addressing tge sp addr ms##args = Some a).
rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
- left; eapply exec_straight_steps; eauto with coqlib.
+ left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto.
destruct chunk; simpl; simpl in H6;
try (rewrite storev_8_signed_unsigned in H0);
try (rewrite storev_16_signed_unsigned in H0);
@@ -896,8 +909,19 @@ Proof.
intros. rewrite Pregmap.gso; auto with ppcgen.
Qed.
-
-Lemma exec_Mtailcall_prop: forall (s : list stackframe) (fb stk : block) (soff : int) (sig : signature) (ros : mreg + ident) (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m', find_function_ptr ge ros ms = Some f' -> Genv.find_funct_ptr ge fb = Some (Internal f) -> load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0 (Callstate s f' ms m'). Proof.
+Lemma exec_Mtailcall_prop:
+ forall (s : list stackframe) (fb stk : block) (soff : int)
+ (sig : signature) (ros : mreg + ident) (c : list Mach.instruction)
+ (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m',
+ find_function_ptr ge ros ms = Some f' ->
+ Genv.find_funct_ptr ge fb = Some (Internal f) ->
+ load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
+ load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
+ Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+ exec_instr_prop
+ (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
+ (Callstate s f' ms m').
+Proof.
intros; red; intros; inv MS.
assert (f0 = f) by congruence. subst f0.
generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -906,7 +930,7 @@ Lemma exec_Mtailcall_prop: forall (s : list stackframe) (fb stk : block) (soff
match ros with inl r => Pbreg (ireg_of r) | inr symb => Pbsymb symb end).
assert (TR: transl_code f (Mtailcall sig ros :: c) =
loadind_int IR13 (fn_retaddr_ofs f) IR14
- (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) (fn_link_ofs f) :: call_instr :: transl_code f c)).
+ (Pfreeframe f.(fn_stacksize) (fn_link_ofs f) :: call_instr :: transl_code f c)).
unfold call_instr; destruct ros; auto.
unfold load_stack in *.
exploit Mem.loadv_extends. eauto. eexact H1. auto.
@@ -918,7 +942,7 @@ Lemma exec_Mtailcall_prop: forall (s : list stackframe) (fb stk : block) (soff
exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
destruct (loadind_int_correct tge (transl_function f) IR13 f.(fn_retaddr_ofs) IR14
rs m'0 (parent_ra s)
- (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: call_instr :: transl_code f c))
+ (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: call_instr :: transl_code f c))
as [rs1 [EXEC1 [RES1 OTH1]]].
rewrite <- (sp_val ms (Vptr stk soff) rs); auto.
set (rs2 := nextinstr (rs1#IR13 <- (parent_sp s))).
@@ -1021,7 +1045,7 @@ Lemma exec_Mcond_true_prop:
(cond : condition) (args : list mreg) (lbl : Mach.label)
(c : list Mach.instruction) (ms : mreg -> val) (m : mem)
(c' : Mach.code),
- eval_condition cond ms ## args = Some true ->
+ eval_condition cond ms ## args m = Some true ->
Genv.find_funct_ptr ge fb = Some (Internal f) ->
Mach.find_label lbl (fn_code f) = Some c' ->
exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0
@@ -1030,7 +1054,8 @@ Proof.
intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0.
generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
intro WTI. inv WTI.
- exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. intros A.
+ exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto.
+ intros A.
exploit transl_cond_correct. eauto. eauto.
intros [rs2 [EX [RES OTH]]].
inv AT. simpl in H5.
@@ -1057,14 +1082,15 @@ Lemma exec_Mcond_false_prop:
forall (s : list stackframe) (fb : block) (sp : val)
(cond : condition) (args : list mreg) (lbl : Mach.label)
(c : list Mach.instruction) (ms : mreg -> val) (m : mem),
- eval_condition cond ms ## args = Some false ->
+ eval_condition cond ms ## args m = Some false ->
exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0
(Machconcr.State s fb sp c (undef_temps ms) m).
Proof.
intros; red; intros; inv MS.
generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
intro WTI. inv WTI.
- exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. intros A.
+ exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto.
+ intros A.
exploit transl_cond_correct. eauto. eauto.
intros [rs2 [EX [RES OTH]]].
left; eapply exec_straight_steps; eauto with coqlib.
@@ -1081,7 +1107,7 @@ Lemma exec_Mjumptable_prop:
(ms : mreg -> val) (m : mem) (n : int) (lbl : Mach.label)
(c' : Mach.code),
ms arg = Vint n ->
- list_nth_z tbl (Int.signed n) = Some lbl ->
+ list_nth_z tbl (Int.unsigned n) = Some lbl ->
Genv.find_funct_ptr ge fb = Some (Internal f) ->
Mach.find_label lbl (fn_code f) = Some c' ->
exec_instr_prop
@@ -1093,11 +1119,10 @@ Proof.
generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
intro WTI. inv WTI.
exploit list_nth_z_range; eauto. intro RANGE.
- assert (SHIFT: Int.signed (Int.shl n (Int.repr 2)) = Int.signed n * 4).
+ assert (SHIFT: Int.unsigned (Int.shl n (Int.repr 2)) = Int.unsigned n * 4).
rewrite Int.shl_mul.
- rewrite Int.mul_signed.
- apply Int.signed_repr.
- split. apply Zle_trans with 0. vm_compute; congruence. omega.
+ unfold Int.mul.
+ apply Int.unsigned_repr.
omega.
inv AT. simpl in H7.
set (k1 := Pbtbl IR14 tbl :: transl_code f c).
@@ -1122,9 +1147,8 @@ Proof.
eapply find_instr_tail. unfold k1 in CT1. eauto.
unfold exec_instr.
change (rs1 IR14) with (Vint (Int.shl n (Int.repr 2))).
-Opaque Zmod. Opaque Zdiv.
- simpl. rewrite SHIFT. rewrite Z_mod_mult. rewrite zeq_true.
- rewrite Z_div_mult.
+ lazy iota beta. rewrite SHIFT.
+ rewrite Z_mod_mult. rewrite zeq_true. rewrite Z_div_mult.
change label with Mach.label; rewrite H0. exact GOTO. omega. traceEq.
econstructor; eauto.
eapply Mach.find_label_incl; eauto.
@@ -1133,7 +1157,16 @@ Opaque Zmod. Opaque Zdiv.
apply agree_undef_temps; auto.
Qed.
-Lemma exec_Mreturn_prop: forall (s : list stackframe) (fb stk : block) (soff : int) (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m', Genv.find_funct_ptr ge fb = Some (Internal f) -> load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0 (Returnstate s ms m'). Proof.
+Lemma exec_Mreturn_prop:
+ forall (s : list stackframe) (fb stk : block) (soff : int)
+ (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m',
+ Genv.find_funct_ptr ge fb = Some (Internal f) ->
+ load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
+ load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
+ Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+ exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
+ (Returnstate s ms m').
+Proof.
intros; red; intros; inv MS.
assert (f0 = f) by congruence. subst f0.
unfold load_stack in *.
@@ -1147,13 +1180,13 @@ Lemma exec_Mreturn_prop: forall (s : list stackframe) (fb stk : block) (soff :
exploit (loadind_int_correct tge (transl_function f) IR13 f.(fn_retaddr_ofs) IR14
rs m'0 (parent_ra s)
- (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 :: transl_code f c)).
+ (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 :: transl_code f c)).
rewrite <- (sp_val ms (Vptr stk soff) rs); auto.
intros [rs1 [EXEC1 [RES1 OTH1]]].
set (rs2 := nextinstr (rs1#IR13 <- (parent_sp s))).
assert (EXEC2: exec_straight tge (transl_function f)
(loadind_int IR13 (fn_retaddr_ofs f) IR14
- (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) (fn_link_ofs f) :: Pbreg IR14 :: transl_code f c))
+ (Pfreeframe f.(fn_stacksize) (fn_link_ofs f) :: Pbreg IR14 :: transl_code f c))
rs m'0 (Pbreg IR14 :: transl_code f c) rs2 m2').
eapply exec_straight_trans. eexact EXEC1.
apply exec_straight_one. simpl. rewrite OTH1; try congruence.
@@ -1188,12 +1221,12 @@ Lemma exec_function_internal_prop:
forall (s : list stackframe) (fb : block) (ms : Mach.regset)
(m : mem) (f : function) (m1 m2 m3 : mem) (stk : block),
Genv.find_funct_ptr ge fb = Some (Internal f) ->
- Mem.alloc m (- fn_framesize f) (fn_stacksize f) = (m1, stk) ->
- let sp := Vptr stk (Int.repr (- fn_framesize f)) in
+ Mem.alloc m 0 (fn_stacksize f) = (m1, stk) ->
+ let sp := Vptr stk Int.zero in
store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 ->
store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 ->
exec_instr_prop (Machconcr.Callstate s fb ms m) E0
- (Machconcr.State s fb sp (fn_code f) ms m3).
+ (Machconcr.State s fb sp (fn_code f) (undef_temps ms) m3).
Proof.
intros; red; intros; inv MS.
assert (WTF: wt_function f).
@@ -1201,7 +1234,7 @@ Proof.
inversion TY; auto.
exploit functions_transl; eauto. intro TFIND.
generalize (functions_transl_no_overflow _ _ H); intro NOOV.
- set (rs2 := nextinstr (rs#IR13 <- sp)).
+ set (rs2 := nextinstr (rs#IR12 <- (rs#IR13) #IR13 <- sp)).
set (rs3 := nextinstr rs2).
exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl.
intros [m1' [A B]].
@@ -1218,7 +1251,7 @@ Proof.
unfold transl_function at 2.
apply exec_straight_two with rs2 m2'.
unfold exec_instr. rewrite A. fold sp.
- rewrite <- (sp_val ms (parent_sp s) rs); auto. rewrite C. auto.
+ rewrite (sp_val ms (parent_sp s) rs) in C; auto. rewrite C. auto.
unfold exec_instr. unfold eval_shift_addr. unfold exec_store.
change (rs2 IR13) with sp. change (rs2 IR14) with (rs IR14). rewrite ATLR.
rewrite E. auto.
@@ -1231,10 +1264,12 @@ Proof.
eapply code_tail_next_int; auto.
change (Int.unsigned Int.zero) with 0.
unfold transl_function. constructor.
- assert (AG3: agree ms sp rs3).
+ assert (AG3: agree (undef_temps ms) sp rs3).
unfold rs3. apply agree_nextinstr.
unfold rs2. apply agree_nextinstr.
- apply agree_change_sp with (parent_sp s); auto.
+ apply agree_change_sp with (parent_sp s).
+ apply agree_exten_temps with rs; auto.
+ intros. apply Pregmap.gso; auto with ppcgen.
unfold sp. congruence.
left; exists (State rs3 m3'); split.
(* execution *)
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index c10c9df..fb49cb7 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -441,6 +441,169 @@ Qed.
(** * Correctness of ARM constructor functions *)
+(** Decomposition of an integer constant *)
+
+Lemma decompose_int_rec_or:
+ forall N n p x, List.fold_left Int.or (decompose_int_rec N n p) x = Int.or x n.
+Proof.
+ induction N; intros; simpl.
+ destruct (Int.eq_dec n Int.zero); simpl.
+ subst n. rewrite Int.or_zero. auto.
+ auto.
+ destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero).
+ auto.
+ simpl. rewrite IHN. rewrite Int.or_assoc. decEq. rewrite <- Int.and_or_distrib.
+ rewrite Int.or_not_self. apply Int.and_mone.
+Qed.
+
+Lemma decompose_int_rec_xor:
+ forall N n p x, List.fold_left Int.xor (decompose_int_rec N n p) x = Int.xor x n.
+Proof.
+ induction N; intros; simpl.
+ destruct (Int.eq_dec n Int.zero); simpl.
+ subst n. rewrite Int.xor_zero. auto.
+ auto.
+ destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero).
+ auto.
+ simpl. rewrite IHN. rewrite Int.xor_assoc. decEq. rewrite <- Int.and_xor_distrib.
+ rewrite Int.xor_not_self. apply Int.and_mone.
+Qed.
+
+Lemma decompose_int_rec_add:
+ forall N n p x, List.fold_left Int.add (decompose_int_rec N n p) x = Int.add x n.
+Proof.
+ induction N; intros; simpl.
+ destruct (Int.eq_dec n Int.zero); simpl.
+ subst n. rewrite Int.add_zero. auto.
+ auto.
+ destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero).
+ auto.
+ simpl. rewrite IHN. rewrite Int.add_assoc. decEq. rewrite Int.add_and.
+ rewrite Int.or_not_self. apply Int.and_mone. apply Int.and_not_self.
+Qed.
+
+Remark decompose_int_rec_nil:
+ forall N n p, decompose_int_rec N n p = nil -> n = Int.zero.
+Proof.
+ intros. generalize (decompose_int_rec_or N n p Int.zero). rewrite H. simpl.
+ rewrite Int.or_commut; rewrite Int.or_zero; auto.
+Qed.
+
+Lemma decompose_int_general:
+ forall (f: val -> int -> val) (g: int -> int -> int),
+ (forall v1 n2 n3, f (f v1 n2) n3 = f v1 (g n2 n3)) ->
+ (forall n1 n2 n3, g (g n1 n2) n3 = g n1 (g n2 n3)) ->
+ (forall n, g Int.zero n = n) ->
+ (forall N n p x, List.fold_left g (decompose_int_rec N n p) x = g x n) ->
+ forall n v,
+ List.fold_left f (decompose_int n) v = f v n.
+Proof.
+ intros f g DISTR ASSOC ZERO DECOMP.
+ assert (A: forall l x y, g x (fold_left g l y) = fold_left g l (g x y)).
+ induction l; intros; simpl. auto. rewrite IHl. decEq. rewrite ASSOC; auto.
+ assert (B: forall l v n, fold_left f l (f v n) = f v (fold_left g l n)).
+ induction l; intros; simpl.
+ auto.
+ rewrite IHl. rewrite DISTR. decEq. decEq. auto.
+ intros. unfold decompose_int.
+ destruct (decompose_int_rec 12 n Int.zero) as []_eqn.
+ simpl. exploit decompose_int_rec_nil; eauto. congruence.
+ simpl. rewrite B. decEq.
+ generalize (DECOMP 12%nat n Int.zero Int.zero).
+ rewrite Heql. simpl. repeat rewrite ZERO. auto.
+Qed.
+
+Lemma decompose_int_or:
+ forall n v,
+ List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) v = Val.or v (Vint n).
+Proof.
+ intros. apply decompose_int_general with (f := fun v n => Val.or v (Vint n)) (g := Int.or).
+ intros. rewrite Val.or_assoc. auto.
+ apply Int.or_assoc.
+ intros. rewrite Int.or_commut. apply Int.or_zero.
+ apply decompose_int_rec_or.
+Qed.
+
+Lemma decompose_int_bic:
+ forall n v,
+ List.fold_left (fun v i => Val.and v (Vint (Int.not i))) (decompose_int n) v = Val.and v (Vint (Int.not n)).
+Proof.
+ intros. apply decompose_int_general with (f := fun v n => Val.and v (Vint (Int.not n))) (g := Int.or).
+ intros. rewrite Val.and_assoc. simpl. decEq. decEq. rewrite Int.not_or_and_not. auto.
+ apply Int.or_assoc.
+ intros. rewrite Int.or_commut. apply Int.or_zero.
+ apply decompose_int_rec_or.
+Qed.
+
+Lemma decompose_int_xor:
+ forall n v,
+ List.fold_left (fun v i => Val.xor v (Vint i)) (decompose_int n) v = Val.xor v (Vint n).
+Proof.
+ intros. apply decompose_int_general with (f := fun v n => Val.xor v (Vint n)) (g := Int.xor).
+ intros. rewrite Val.xor_assoc. auto.
+ apply Int.xor_assoc.
+ intros. rewrite Int.xor_commut. apply Int.xor_zero.
+ apply decompose_int_rec_xor.
+Qed.
+
+Lemma decompose_int_add:
+ forall n v,
+ List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) v = Val.add v (Vint n).
+Proof.
+ intros. apply decompose_int_general with (f := fun v n => Val.add v (Vint n)) (g := Int.add).
+ intros. rewrite Val.add_assoc. auto.
+ apply Int.add_assoc.
+ intros. rewrite Int.add_commut. apply Int.add_zero.
+ apply decompose_int_rec_add.
+Qed.
+
+Lemma decompose_int_sub:
+ forall n v,
+ List.fold_left (fun v i => Val.sub v (Vint i)) (decompose_int n) v = Val.sub v (Vint n).
+Proof.
+ intros. apply decompose_int_general with (f := fun v n => Val.sub v (Vint n)) (g := Int.add).
+ intros. repeat rewrite Val.sub_add_opp. rewrite Val.add_assoc. decEq. simpl. decEq.
+ rewrite Int.neg_add_distr; auto.
+ apply Int.add_assoc.
+ intros. rewrite Int.add_commut. apply Int.add_zero.
+ apply decompose_int_rec_add.
+Qed.
+
+Lemma iterate_op_correct:
+ forall op1 op2 (f: val -> int -> val) (rs: regset) (r: ireg) m v0 n k,
+ (forall (rs:regset) n,
+ exec_instr ge fn (op2 (SOimm n)) rs m =
+ OK (nextinstr (rs#r <- (f (rs#r) n))) m) ->
+ (forall n,
+ exec_instr ge fn (op1 (SOimm n)) rs m =
+ OK (nextinstr (rs#r <- (f v0 n))) m) ->
+ exists rs',
+ exec_straight (iterate_op op1 op2 (decompose_int n) k) rs m k rs' m
+ /\ rs'#r = List.fold_left f (decompose_int n) v0
+ /\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'.
+Proof.
+ intros until k; intros SEM2 SEM1.
+ unfold iterate_op.
+ destruct (decompose_int n) as [ | i tl] _eqn.
+ unfold decompose_int in Heql. destruct (decompose_int_rec 12%nat n Int.zero); congruence.
+ revert k. pattern tl. apply List.rev_ind.
+ (* base case *)
+ intros; simpl. econstructor.
+ split. apply exec_straight_one. rewrite SEM1. reflexivity. reflexivity.
+ split. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. auto.
+ intros. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso; auto with ppcgen.
+ (* inductive case *)
+ intros.
+ rewrite List.map_app. simpl. rewrite app_ass. simpl.
+ destruct (H (op2 (SOimm x) :: k)) as [rs' [A [B C]]].
+ econstructor.
+ split. eapply exec_straight_trans. eexact A. apply exec_straight_one.
+ rewrite SEM2. reflexivity. reflexivity.
+ split. rewrite fold_left_app; simpl. rewrite nextinstr_inv; auto with ppcgen.
+ rewrite Pregmap.gss. rewrite B. auto.
+ intros. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso; auto with ppcgen.
+Qed.
+
(** Loading a constant. *)
Lemma loadimm_correct:
@@ -451,46 +614,19 @@ Lemma loadimm_correct:
/\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'.
Proof.
intros. unfold loadimm.
- case (is_immed_arith n).
- (* single move *)
- exists (nextinstr (rs#r <- (Vint n))).
- split. apply exec_straight_one. reflexivity. reflexivity.
- split. rewrite nextinstr_inv; auto with ppcgen.
- apply Pregmap.gss.
- intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
- case (is_immed_arith (Int.not n)).
- (* single move-complement *)
- exists (nextinstr (rs#r <- (Vint n))).
- split. apply exec_straight_one.
- simpl. change (Int.xor (Int.not n) Int.mone) with (Int.not (Int.not n)).
- rewrite Int.not_involutive. auto.
- reflexivity.
- split. rewrite nextinstr_inv; auto with ppcgen.
- apply Pregmap.gss.
- intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
- (* mov - or - or - or *)
- set (n1 := Int.and n (Int.repr 255)).
- set (n2 := Int.and n (Int.repr 65280)).
- set (n3 := Int.and n (Int.repr 16711680)).
- set (n4 := Int.and n (Int.repr 4278190080)).
- set (rs1 := nextinstr (rs#r <- (Vint n1))).
- set (rs2 := nextinstr (rs1#r <- (Val.or rs1#r (Vint n2)))).
- set (rs3 := nextinstr (rs2#r <- (Val.or rs2#r (Vint n3)))).
- set (rs4 := nextinstr (rs3#r <- (Val.or rs3#r (Vint n4)))).
- exists rs4.
- split. apply exec_straight_four with rs1 m rs2 m rs3 m; auto.
- split. unfold rs4. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
- unfold rs3. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
- unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
- unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
- repeat rewrite Val.or_assoc. simpl. decEq.
- unfold n4, n3, n2, n1. repeat rewrite <- Int.and_or_distrib.
- change (Int.and n Int.mone = n). apply Int.and_mone.
- intros.
- unfold rs4. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
- unfold rs3. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
- unfold rs2. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
- unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+ destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.not n)))).
+ (* mov - orr* *)
+ replace (Vint n) with (List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) Vzero).
+ apply iterate_op_correct.
+ auto.
+ intros; simpl. rewrite Int.or_commut; rewrite Int.or_zero; auto.
+ rewrite decompose_int_or. simpl. rewrite Int.or_commut; rewrite Int.or_zero; auto.
+ (* mvn - bic* *)
+ replace (Vint n) with (List.fold_left (fun v i => Val.and v (Vint (Int.not i))) (decompose_int (Int.not n)) (Vint Int.mone)).
+ apply iterate_op_correct.
+ auto.
+ intros. simpl. rewrite Int.and_commut; rewrite Int.and_mone; auto.
+ rewrite decompose_int_bic. simpl. rewrite Int.not_involutive. rewrite Int.and_commut. rewrite Int.and_mone; auto.
Qed.
(** Add integer immediate. *)
@@ -503,46 +639,21 @@ Lemma addimm_correct:
/\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
Proof.
intros. unfold addimm.
- (* addi *)
- case (is_immed_arith n).
- exists (nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n)))).
- split. apply exec_straight_one; auto.
- split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
- intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
- (* subi *)
- case (is_immed_arith (Int.neg n)).
- exists (nextinstr (rs#r1 <- (Val.sub rs#r2 (Vint (Int.neg n))))).
- split. apply exec_straight_one; auto.
- split. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
- apply Val.sub_opp_add.
- intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
- (* general *)
- set (n1 := Int.and n (Int.repr 255)).
- set (n2 := Int.and n (Int.repr 65280)).
- set (n3 := Int.and n (Int.repr 16711680)).
- set (n4 := Int.and n (Int.repr 4278190080)).
- set (rs1 := nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n1)))).
- set (rs2 := nextinstr (rs1#r1 <- (Val.add rs1#r1 (Vint n2)))).
- set (rs3 := nextinstr (rs2#r1 <- (Val.add rs2#r1 (Vint n3)))).
- set (rs4 := nextinstr (rs3#r1 <- (Val.add rs3#r1 (Vint n4)))).
- exists rs4.
- split. apply exec_straight_four with rs1 m rs2 m rs3 m; auto.
- simpl.
- split. unfold rs4. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
- unfold rs3. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
- unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
- unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
- repeat rewrite Val.add_assoc. simpl. decEq. decEq.
- unfold n4, n3, n2, n1. repeat rewrite Int.add_and.
- change (Int.and n Int.mone = n). apply Int.and_mone.
- vm_compute; auto.
- vm_compute; auto.
- vm_compute; auto.
- intros.
- unfold rs4. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
- unfold rs3. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
- unfold rs2. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
- unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+ destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.neg n)))).
+ (* add - add* *)
+ replace (Val.add (rs r2) (Vint n))
+ with (List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) (rs r2)).
+ apply iterate_op_correct.
+ auto.
+ auto.
+ apply decompose_int_add.
+ (* sub - sub* *)
+ replace (Val.add (rs r2) (Vint n))
+ with (List.fold_left (fun v i => Val.sub v (Vint i)) (decompose_int (Int.neg n)) (rs r2)).
+ apply iterate_op_correct.
+ auto.
+ auto.
+ rewrite decompose_int_sub. apply Val.sub_opp_add.
Qed.
(* And integer immediate *)
@@ -553,7 +664,7 @@ Lemma andimm_correct:
exists rs',
exec_straight (andimm r1 r2 n k) rs m k rs' m
/\ rs'#r1 = Val.and rs#r2 (Vint n)
- /\ forall r': preg, r' <> r1 -> r' <> IR14 -> r' <> PC -> rs'#r' = rs#r'.
+ /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
Proof.
intros. unfold andimm.
(* andi *)
@@ -562,57 +673,72 @@ Proof.
split. apply exec_straight_one; auto.
split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
- (* bici *)
- case (is_immed_arith (Int.not n)).
- exists (nextinstr (rs#r1 <- (Val.and rs#r2 (Vint n)))).
- split. apply exec_straight_one; auto. simpl.
- change (Int.xor (Int.not n) Int.mone) with (Int.not (Int.not n)).
- rewrite Int.not_involutive. auto.
- split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
- intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
- (* general *)
- exploit loadimm_correct. intros [rs' [A [B C]]].
- exists (nextinstr (rs'#r1 <- (Val.and rs#r2 (Vint n)))).
- split. eapply exec_straight_trans. eauto. apply exec_straight_one.
- simpl. rewrite B. rewrite C; auto with ppcgen.
+ (* bic - bic* *)
+ replace (Val.and (rs r2) (Vint n))
+ with (List.fold_left (fun v i => Val.and v (Vint (Int.not i))) (decompose_int (Int.not n)) (rs r2)).
+ apply iterate_op_correct.
auto.
- split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
- intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
+ auto.
+ rewrite decompose_int_bic. rewrite Int.not_involutive. auto.
Qed.
-(** Other integer immediate *)
+(** Reverse sub immediate *)
-Lemma makeimm_correct:
- forall (instr: ireg -> ireg -> shift_op -> instruction)
- (sem: val -> val -> val)
- r1 (r2: ireg) n k (rs : regset) m,
- (forall c r1 r2 so rs m,
- exec_instr ge c (instr r1 r2 so) rs m
- = OK (nextinstr rs#r1 <- (sem rs#r2 (eval_shift_op so rs))) m) ->
- r2 <> IR14 ->
+Lemma rsubimm_correct:
+ forall r1 r2 n k rs m,
exists rs',
- exec_straight (makeimm instr r1 r2 n k) rs m k rs' m
- /\ rs'#r1 = sem rs#r2 (Vint n)
- /\ forall r': preg, r' <> r1 -> r' <> PC -> r' <> IR14 -> rs'#r' = rs#r'.
+ exec_straight (rsubimm r1 r2 n k) rs m k rs' m
+ /\ rs'#r1 = Val.sub (Vint n) rs#r2
+ /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
Proof.
- intros. unfold makeimm.
- case (is_immed_arith n).
- (* one immed instr *)
- exists (nextinstr (rs#r1 <- (sem rs#r2 (Vint n)))).
- split. apply exec_straight_one.
- change (Vint n) with (eval_shift_op (SOimm n) rs). auto.
- auto.
- split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
- intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
- (* general case *)
- exploit loadimm_correct. intros [rs' [A [B C]]].
- exists (nextinstr (rs'#r1 <- (sem rs#r2 (Vint n)))).
- split. eapply exec_straight_trans. eauto. apply exec_straight_one.
- rewrite <- B. rewrite <- (C r2).
- change (rs' IR14) with (eval_shift_op (SOreg IR14) rs'). auto.
- congruence. auto with ppcgen. auto.
- split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
- intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto with ppcgen.
+ intros. unfold rsubimm.
+ (* rsb - add* *)
+ replace (Val.sub (Vint n) (rs r2))
+ with (List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) (Val.neg (rs r2))).
+ apply iterate_op_correct.
+ auto.
+ intros. simpl. destruct (rs r2); auto. simpl. rewrite Int.sub_add_opp.
+ rewrite Int.add_commut; auto.
+ rewrite decompose_int_add.
+ destruct (rs r2); simpl; auto. rewrite Int.sub_add_opp. rewrite Int.add_commut; auto.
+Qed.
+
+(** Or immediate *)
+
+Lemma orimm_correct:
+ forall r1 r2 n k rs m,
+ exists rs',
+ exec_straight (orimm r1 r2 n k) rs m k rs' m
+ /\ rs'#r1 = Val.or rs#r2 (Vint n)
+ /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
+Proof.
+ intros. unfold orimm.
+ (* ori - ori* *)
+ replace (Val.or (rs r2) (Vint n))
+ with (List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) (rs r2)).
+ apply iterate_op_correct.
+ auto.
+ auto.
+ apply decompose_int_or.
+Qed.
+
+(** Xor immediate *)
+
+Lemma xorimm_correct:
+ forall r1 r2 n k rs m,
+ exists rs',
+ exec_straight (xorimm r1 r2 n k) rs m k rs' m
+ /\ rs'#r1 = Val.xor rs#r2 (Vint n)
+ /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
+Proof.
+ intros. unfold xorimm.
+ (* xori - xori* *)
+ replace (Val.xor (rs r2) (Vint n))
+ with (List.fold_left (fun v i => Val.xor v (Vint i)) (decompose_int n) (rs r2)).
+ apply iterate_op_correct.
+ auto.
+ auto.
+ apply decompose_int_xor.
Qed.
(** Indexed memory loads. *)
@@ -636,8 +762,7 @@ Proof.
split. eapply exec_straight_trans. eauto. apply exec_straight_one.
simpl. unfold exec_load. rewrite B.
rewrite Val.add_assoc. simpl. rewrite Int.add_zero.
- rewrite H. auto.
- auto.
+ rewrite H. auto. auto.
split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
Qed.
@@ -659,7 +784,8 @@ Proof.
exploit addimm_correct. eauto. intros [rs' [A [B C]]].
exists (nextinstr (rs'#dst <- v)).
split. eapply exec_straight_trans. eauto. apply exec_straight_one.
- simpl. unfold exec_load. rewrite B. rewrite Val.add_assoc. simpl.
+ simpl. unfold exec_load. rewrite B.
+ rewrite Val.add_assoc. simpl.
rewrite Int.add_zero. rewrite H. auto. auto.
split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss.
intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto.
@@ -700,8 +826,8 @@ Proof.
exploit addimm_correct. eauto. intros [rs' [A [B C]]].
exists (nextinstr rs').
split. eapply exec_straight_trans. eauto. apply exec_straight_one.
- simpl. unfold exec_store. rewrite B. rewrite C.
- rewrite Val.add_assoc. simpl. rewrite Int.add_zero.
+ simpl. unfold exec_store. rewrite B.
+ rewrite C. rewrite Val.add_assoc. simpl. rewrite Int.add_zero.
rewrite H. auto.
congruence. auto with ppcgen. auto.
intros. rewrite nextinstr_inv; auto.
@@ -723,10 +849,11 @@ Proof.
exploit addimm_correct. eauto. intros [rs' [A [B C]]].
exists (nextinstr rs').
split. eapply exec_straight_trans. eauto. apply exec_straight_one.
- simpl. unfold exec_store. rewrite B. rewrite C.
- rewrite Val.add_assoc. simpl. rewrite Int.add_zero.
+ simpl. unfold exec_store. rewrite B.
+ rewrite C. rewrite Val.add_assoc. simpl. rewrite Int.add_zero.
rewrite H. auto.
- congruence. congruence. auto with ppcgen. auto.
+ congruence. congruence.
+ auto with ppcgen.
intros. rewrite nextinstr_inv; auto.
Qed.
@@ -827,13 +954,14 @@ Ltac TypeInv := TypeInv1; simpl in *; unfold preg_of in *; TypeInv2.
Lemma transl_cond_correct:
forall cond args k rs m b,
map mreg_type args = type_of_condition cond ->
- eval_condition cond (map rs (map preg_of args)) = Some b ->
+ eval_condition cond (map rs (map preg_of args)) m = Some b ->
exists rs',
exec_straight (transl_cond cond args k) rs m k rs' m
/\ rs'#(CR (crbit_for_cond cond)) = Val.of_bool b
/\ forall r, important_preg r = true -> rs'#r = rs r.
Proof.
- intros until b; intros TY EV. rewrite <- (eval_condition_weaken _ _ EV). clear EV.
+ intros until b; intros TY EV.
+ rewrite <- (eval_condition_weaken _ _ _ EV). clear EV.
destruct cond; simpl in TY; TypeInv.
(* Ccomp *)
generalize (compare_int_spec rs (rs (ireg_of m0)) (rs (ireg_of m1))).
@@ -917,11 +1045,11 @@ Qed.
Ltac Simpl :=
match goal with
- | [ |- nextinstr _ _ = _ ] => rewrite nextinstr_inv; [auto | auto with ppcgen]
- | [ |- Pregmap.get ?x (Pregmap.set ?x _ _) = _ ] => rewrite Pregmap.gss; auto
- | [ |- Pregmap.set ?x _ _ ?x = _ ] => rewrite Pregmap.gss; auto
- | [ |- Pregmap.get _ (Pregmap.set _ _ _) = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
- | [ |- Pregmap.set _ _ _ _ = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
+ | [ |- context[nextinstr _ _] ] => rewrite nextinstr_inv; [auto | auto with ppcgen]
+ | [ |- context[Pregmap.get ?x (Pregmap.set ?x _ _)] ] => rewrite Pregmap.gss; auto
+ | [ |- context[Pregmap.set ?x _ _ ?x] ] => rewrite Pregmap.gss; auto
+ | [ |- context[Pregmap.get _ (Pregmap.set _ _ _)] ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
+ | [ |- context[Pregmap.set _ _ _ _] ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
end.
Ltac TranslOpSimpl :=
@@ -932,13 +1060,13 @@ Ltac TranslOpSimpl :=
Lemma transl_op_correct:
forall op args res k (rs: regset) m v,
wt_instr (Mop op args res) ->
- eval_operation ge rs#IR13 op (map rs (map preg_of args)) = Some v ->
+ eval_operation ge rs#IR13 op (map rs (map preg_of args)) m = Some v ->
exists rs',
exec_straight (transl_op op args res k) rs m k rs' m
/\ rs'#(preg_of res) = v
/\ forall r, important_preg r = true -> r <> preg_of res -> rs'#r = rs#r.
Proof.
- intros. rewrite <- (eval_operation_weaken _ _ _ _ H0). inv H.
+ intros. rewrite <- (eval_operation_weaken _ _ _ _ _ H0). inv H.
(* Omove *)
simpl.
exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of r1)))).
@@ -952,7 +1080,7 @@ Proof.
congruence.
(* Ointconst *)
generalize (loadimm_correct (ireg_of res) i k rs m). intros [rs' [A [B C]]].
- exists rs'. split. auto. split. auto. intros. auto with ppcgen.
+ exists rs'. split. auto. split. rewrite B; auto. intros. auto with ppcgen.
(* Oaddrstack *)
generalize (addimm_correct (ireg_of res) IR13 i k rs m).
intros [rs' [EX [RES OTH]]].
@@ -960,41 +1088,43 @@ Proof.
(* Ocast8signed *)
econstructor; split.
eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
- split. Simpl. Simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
- destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity.
+ split. Simpl. Simpl. Simpl. Simpl.
+ destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.sign_ext_shr_shl.
+ reflexivity.
compute; auto.
intros. repeat Simpl.
(* Ocast8unsigned *)
econstructor; split.
- eapply exec_straight_one. simpl; eauto. auto.
- split. Simpl. Simpl.
- destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.zero_ext_and. reflexivity.
+ eapply exec_straight_one. simpl; eauto. auto.
+ split. Simpl. Simpl.
+ destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.zero_ext_and. auto.
compute; auto.
- intros. repeat Simpl.
+ intros. repeat Simpl.
(* Ocast16signed *)
econstructor; split.
eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
- split. Simpl. Simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
- destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity.
+ split. Simpl. Simpl. Simpl. Simpl.
+ destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.sign_ext_shr_shl. auto.
compute; auto.
intros. repeat Simpl.
(* Ocast16unsigned *)
econstructor; split.
- eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
- split. Simpl. Simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss.
- destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.zero_ext_shru_shl. reflexivity.
+ eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
+ split. Simpl. Simpl. Simpl. Simpl.
+ destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.zero_ext_shru_shl; auto.
compute; auto.
- intros. repeat Simpl.
+ intros. repeat Simpl.
(* Oaddimm *)
generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m).
intros [rs' [A [B C]]].
exists rs'. split. auto. split. auto. auto with ppcgen.
(* Orsbimm *)
- exploit (makeimm_correct Prsb (fun v1 v2 => Val.sub v2 v1) (ireg_of res) (ireg_of m0));
- auto with ppcgen.
+ generalize (rsubimm_correct (ireg_of res) (ireg_of m0) i k rs m).
intros [rs' [A [B C]]].
exists rs'.
- split. eauto. split. rewrite B. auto. auto with ppcgen.
+ split. eauto. split. rewrite B.
+ destruct (rs (ireg_of m0)); auto.
+ auto with ppcgen.
(* Omul *)
destruct (ireg_eq (ireg_of res) (ireg_of m0) || ireg_eq (ireg_of res) (ireg_of m1)).
econstructor; split.
@@ -1006,17 +1136,15 @@ Proof.
generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m
(ireg_of_not_IR14 m0)).
intros [rs' [A [B C]]].
- exists rs'. split. auto. split. auto. auto with ppcgen.
+ exists rs'; auto with ppcgen.
(* Oorimm *)
- exploit (makeimm_correct Porr Val.or (ireg_of res) (ireg_of m0));
- auto with ppcgen.
+ generalize (orimm_correct (ireg_of res) (ireg_of m0) i k rs m).
intros [rs' [A [B C]]].
- exists rs'. split. eauto. split. auto. auto with ppcgen.
+ exists rs'; auto with ppcgen.
(* Oxorimm *)
- exploit (makeimm_correct Peor Val.xor (ireg_of res) (ireg_of m0));
- auto with ppcgen.
+ generalize (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m).
intros [rs' [A [B C]]].
- exists rs'. split. eauto. split. auto. auto with ppcgen.
+ exists rs'; auto with ppcgen.
(* Oshrximm *)
assert (exists n, rs (ireg_of m0) = Vint n /\ Int.ltu i (Int.repr 31) = true).
destruct (rs (ireg_of m0)); try discriminate.
@@ -1050,8 +1178,11 @@ Proof.
auto. unfold rs3. case islt; auto. auto.
split. unfold rs4. repeat Simpl. rewrite ARG1. simpl. rewrite LTU'. rewrite Int.shrx_shr.
fold islt. unfold rs3. rewrite nextinstr_inv; auto with ppcgen.
- destruct islt. rewrite RES2. change (rs1 (IR (ireg_of m0))) with (rs (IR (ireg_of m0))).
- rewrite ARG1. simpl. rewrite LTU'. auto.
+ destruct islt.
+ rewrite RES2.
+ change (rs1 (IR (ireg_of m0))) with (rs (IR (ireg_of m0))).
+ rewrite ARG1.
+ simpl. rewrite LTU'. auto.
rewrite Pregmap.gss. simpl. rewrite LTU'. auto.
assumption.
intros. unfold rs4; repeat Simpl. unfold rs3; repeat Simpl.
@@ -1059,10 +1190,10 @@ Proof.
rewrite OTH2; auto with ppcgen.
(* Ocmp *)
fold preg_of in *.
- assert (exists b, eval_condition c rs ## (preg_of ## args) = Some b /\ v = Val.of_bool b).
- fold preg_of in H0. destruct (eval_condition c rs ## (preg_of ## args)).
+ assert (exists b, eval_condition c rs ## (preg_of ## args) m = Some b /\ v = Val.of_bool b).
+ fold preg_of in H0. destruct (eval_condition c rs ## (preg_of ## args) m).
exists b; split; auto. destruct b; inv H0; auto. congruence.
- clear H0. destruct H as [b [EVC VBO]]. rewrite (eval_condition_weaken _ _ EVC).
+ clear H0. destruct H as [b [EVC VBO]]. rewrite (eval_condition_weaken _ _ _ EVC).
destruct (transl_cond_correct c args
(Pmov (ireg_of res) (SOimm Int.zero)
:: Pmovc (crbit_for_cond c) (ireg_of res) (SOimm Int.one) :: k)
diff --git a/arm/Asmgenretaddr.v b/arm/Asmgenretaddr.v
index 359aaf2..97250a6 100644
--- a/arm/Asmgenretaddr.v
+++ b/arm/Asmgenretaddr.v
@@ -102,6 +102,16 @@ Ltac IsTail :=
| _ => idtac
end.
+Lemma iterate_op_tail:
+ forall op1 op2 l k, is_tail k (iterate_op op1 op2 l k).
+Proof.
+ intros. unfold iterate_op.
+ destruct l.
+ auto with coqlib.
+ constructor. revert l; induction l; simpl; auto with coqlib.
+Qed.
+Hint Resolve iterate_op_tail: ppcretaddr.
+
Lemma loadimm_tail:
forall r n k, is_tail k (loadimm r n k).
Proof. unfold loadimm; intros; IsTail. Qed.
@@ -117,10 +127,20 @@ Lemma andimm_tail:
Proof. unfold andimm; intros; IsTail. Qed.
Hint Resolve andimm_tail: ppcretaddr.
-Lemma makeimm_tail:
- forall f r1 r2 n k, is_tail k (makeimm f r1 r2 n k).
-Proof. unfold makeimm; intros; IsTail. Qed.
-Hint Resolve makeimm_tail: ppcretaddr.
+Lemma rsubimm_tail:
+ forall r1 r2 n k, is_tail k (rsubimm r1 r2 n k).
+Proof. unfold rsubimm; intros; IsTail. Qed.
+Hint Resolve rsubimm_tail: ppcretaddr.
+
+Lemma orimm_tail:
+ forall r1 r2 n k, is_tail k (orimm r1 r2 n k).
+Proof. unfold orimm; intros; IsTail. Qed.
+Hint Resolve orimm_tail: ppcretaddr.
+
+Lemma xorimm_tail:
+ forall r1 r2 n k, is_tail k (xorimm r1 r2 n k).
+Proof. unfold xorimm; intros; IsTail. Qed.
+Hint Resolve xorimm_tail: ppcretaddr.
Lemma transl_cond_tail:
forall cond args k, is_tail k (transl_cond cond args k).
@@ -189,11 +209,11 @@ Proof.
Qed.
Lemma return_address_exists:
- forall f c, is_tail c f.(fn_code) ->
+ forall f sg ros c, is_tail (Mcall sg ros :: c) f.(fn_code) ->
exists ra, return_address_offset f c ra.
Proof.
intros. assert (is_tail (transl_code f c) (transl_function f)).
- unfold transl_function. IsTail. apply transl_code_tail; auto.
+ unfold transl_function. IsTail. apply transl_code_tail; eauto with coqlib.
destruct (is_tail_code_tail _ _ H0) as [ofs A].
exists (Int.repr ofs). constructor. auto.
Qed.
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 3f98b88..25758cc 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -88,10 +88,10 @@ Ltac InvVLMA :=
approximations returned by [eval_static_operation]. *)
Lemma eval_static_condition_correct:
- forall cond al vl b,
+ forall cond al vl m b,
val_list_match_approx al vl ->
eval_static_condition cond al = Some b ->
- eval_condition cond vl = Some b.
+ eval_condition cond vl m = Some b.
Proof.
intros until b.
unfold eval_static_condition.
@@ -100,9 +100,9 @@ Proof.
Qed.
Lemma eval_static_operation_correct:
- forall op sp al vl v,
+ forall op sp al vl m v,
val_list_match_approx al vl ->
- eval_operation ge sp op vl = Some v ->
+ eval_operation ge sp op vl m = Some v ->
val_match_approx (eval_static_operation op al) v.
Proof.
intros until v.
@@ -144,7 +144,7 @@ Proof.
inv H4. destruct (Float.intoffloat f); simpl in H0; inv H0. red; auto.
caseEq (eval_static_condition c vl0).
- intros. generalize (eval_static_condition_correct _ _ _ _ H H1).
+ intros. generalize (eval_static_condition_correct _ _ _ m _ H H1).
intro. rewrite H2 in H0.
destruct b; injection H0; intro; subst v; simpl; auto.
intros; simpl; auto.
@@ -168,6 +168,7 @@ Section STRENGTH_REDUCTION.
Variable app: reg -> approx.
Variable sp: val.
Variable rs: regset.
+Variable m: mem.
Hypothesis MATCH: forall r, val_match_approx (app r) rs#r.
Lemma intval_correct:
@@ -183,7 +184,7 @@ Qed.
Lemma cond_strength_reduction_correct:
forall cond args,
let (cond', args') := cond_strength_reduction app cond args in
- eval_condition cond' rs##args' = eval_condition cond rs##args.
+ eval_condition cond' rs##args' m = eval_condition cond rs##args m.
Proof.
intros. unfold cond_strength_reduction.
case (cond_strength_reduction_match cond args); intros.
@@ -191,7 +192,6 @@ Proof.
caseEq (intval app r1); intros.
simpl. rewrite (intval_correct _ _ H).
destruct (rs#r2); auto. rewrite Int.swap_cmp. auto.
- destruct c; reflexivity.
caseEq (intval app r2); intros.
simpl. rewrite (intval_correct _ _ H0). auto.
auto.
@@ -199,6 +199,7 @@ Proof.
caseEq (intval app r1); intros.
simpl. rewrite (intval_correct _ _ H).
destruct (rs#r2); auto. rewrite Int.swap_cmpu. auto.
+ destruct c; reflexivity.
caseEq (intval app r2); intros.
simpl. rewrite (intval_correct _ _ H0). auto.
auto.
@@ -217,8 +218,8 @@ Qed.
Lemma make_addimm_correct:
forall n r v,
let (op, args) := make_addimm n r in
- eval_operation ge sp Oadd (rs#r :: Vint n :: nil) = Some v ->
- eval_operation ge sp op rs##args = Some v.
+ eval_operation ge sp Oadd (rs#r :: Vint n :: nil) m = Some v ->
+ eval_operation ge sp op rs##args m = Some v.
Proof.
intros; unfold make_addimm.
generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -230,8 +231,8 @@ Qed.
Lemma make_shlimm_correct:
forall n r v,
let (op, args) := make_shlimm n r in
- eval_operation ge sp Oshl (rs#r :: Vint n :: nil) = Some v ->
- eval_operation ge sp op rs##args = Some v.
+ eval_operation ge sp Oshl (rs#r :: Vint n :: nil) m = Some v ->
+ eval_operation ge sp op rs##args m = Some v.
Proof.
intros; unfold make_shlimm.
generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -244,8 +245,8 @@ Qed.
Lemma make_shrimm_correct:
forall n r v,
let (op, args) := make_shrimm n r in
- eval_operation ge sp Oshr (rs#r :: Vint n :: nil) = Some v ->
- eval_operation ge sp op rs##args = Some v.
+ eval_operation ge sp Oshr (rs#r :: Vint n :: nil) m = Some v ->
+ eval_operation ge sp op rs##args m = Some v.
Proof.
intros; unfold make_shrimm.
generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -258,8 +259,8 @@ Qed.
Lemma make_shruimm_correct:
forall n r v,
let (op, args) := make_shruimm n r in
- eval_operation ge sp Oshru (rs#r :: Vint n :: nil) = Some v ->
- eval_operation ge sp op rs##args = Some v.
+ eval_operation ge sp Oshru (rs#r :: Vint n :: nil) m = Some v ->
+ eval_operation ge sp op rs##args m = Some v.
Proof.
intros; unfold make_shruimm.
generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -273,8 +274,8 @@ Lemma make_mulimm_correct:
forall n r r' v,
rs#r' = Vint n ->
let (op, args) := make_mulimm n r r' in
- eval_operation ge sp Omul (rs#r :: Vint n :: nil) = Some v ->
- eval_operation ge sp op rs##args = Some v.
+ eval_operation ge sp Omul (rs#r :: Vint n :: nil) m = Some v ->
+ eval_operation ge sp op rs##args m = Some v.
Proof.
intros; unfold make_mulimm.
generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -282,8 +283,8 @@ Proof.
generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intros.
subst n. simpl in H2. simpl. FuncInv. rewrite Int.mul_one in H1. congruence.
caseEq (Int.is_power2 n); intros.
- replace (eval_operation ge sp Omul (rs # r :: Vint n :: nil))
- with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil)).
+ replace (eval_operation ge sp Omul (rs # r :: Vint n :: nil) m)
+ with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil) m).
apply make_shlimm_correct.
simpl. generalize (Int.is_power2_range _ _ H2).
change (Z_of_nat Int.wordsize) with 32. intro. rewrite H3.
@@ -294,8 +295,8 @@ Qed.
Lemma make_andimm_correct:
forall n r v,
let (op, args) := make_andimm n r in
- eval_operation ge sp Oand (rs#r :: Vint n :: nil) = Some v ->
- eval_operation ge sp op rs##args = Some v.
+ eval_operation ge sp Oand (rs#r :: Vint n :: nil) m = Some v ->
+ eval_operation ge sp op rs##args m = Some v.
Proof.
intros; unfold make_andimm.
generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -308,8 +309,8 @@ Qed.
Lemma make_orimm_correct:
forall n r v,
let (op, args) := make_orimm n r in
- eval_operation ge sp Oor (rs#r :: Vint n :: nil) = Some v ->
- eval_operation ge sp op rs##args = Some v.
+ eval_operation ge sp Oor (rs#r :: Vint n :: nil) m = Some v ->
+ eval_operation ge sp op rs##args m = Some v.
Proof.
intros; unfold make_orimm.
generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -322,8 +323,8 @@ Qed.
Lemma make_xorimm_correct:
forall n r v,
let (op, args) := make_xorimm n r in
- eval_operation ge sp Oxor (rs#r :: Vint n :: nil) = Some v ->
- eval_operation ge sp op rs##args = Some v.
+ eval_operation ge sp Oxor (rs#r :: Vint n :: nil) m = Some v ->
+ eval_operation ge sp op rs##args m = Some v.
Proof.
intros; unfold make_xorimm.
generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -336,16 +337,16 @@ Qed.
Lemma op_strength_reduction_correct:
forall op args v,
let (op', args') := op_strength_reduction app op args in
- eval_operation ge sp op rs##args = Some v ->
- eval_operation ge sp op' rs##args' = Some v.
+ eval_operation ge sp op rs##args m = Some v ->
+ eval_operation ge sp op' rs##args' m = Some v.
Proof.
intros; unfold op_strength_reduction;
case (op_strength_reduction_match op args); intros; simpl List.map.
(* Oadd *)
caseEq (intval app r1); intros.
rewrite (intval_correct _ _ H).
- replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil))
- with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil)).
+ replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil) m)
+ with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil) m).
apply make_addimm_correct.
simpl. destruct rs#r2; auto. rewrite Int.add_commut; auto.
caseEq (intval app r2); intros.
@@ -354,8 +355,8 @@ Proof.
(* Oaddshift *)
caseEq (intval app r2); intros.
rewrite (intval_correct _ _ H).
- replace (eval_operation ge sp (Oaddshift s) (rs # r1 :: Vint i :: nil))
- with (eval_operation ge sp Oadd (rs # r1 :: Vint (eval_shift s i) :: nil)).
+ replace (eval_operation ge sp (Oaddshift s) (rs # r1 :: Vint i :: nil) m)
+ with (eval_operation ge sp Oadd (rs # r1 :: Vint (eval_shift s i) :: nil) m).
apply make_addimm_correct.
simpl. destruct rs#r1; auto.
assumption.
@@ -365,16 +366,16 @@ Proof.
simpl in *. destruct rs#r2; auto.
caseEq (intval app r2); intros.
rewrite (intval_correct _ _ H0).
- replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil))
- with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil)).
+ replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil) m)
+ with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil) m).
apply make_addimm_correct.
simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto.
assumption.
(* Osubshift *)
caseEq (intval app r2); intros.
rewrite (intval_correct _ _ H).
- replace (eval_operation ge sp (Osubshift s) (rs # r1 :: Vint i :: nil))
- with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg (eval_shift s i)) :: nil)).
+ replace (eval_operation ge sp (Osubshift s) (rs # r1 :: Vint i :: nil) m)
+ with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg (eval_shift s i)) :: nil) m).
apply make_addimm_correct.
simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto.
assumption.
@@ -386,8 +387,8 @@ Proof.
(* Omul *)
caseEq (intval app r1); intros.
rewrite (intval_correct _ _ H).
- replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil))
- with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil)).
+ replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil) m)
+ with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil) m).
apply make_mulimm_correct. apply intval_correct; auto.
simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto.
caseEq (intval app r2); intros.
@@ -398,8 +399,8 @@ Proof.
caseEq (intval app r2); intros.
caseEq (Int.is_power2 i); intros.
rewrite (intval_correct _ _ H).
- replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil))
- with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil)).
+ replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil) m)
+ with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil) m).
apply make_shruimm_correct.
simpl. destruct rs#r1; auto.
change 32 with (Z_of_nat Int.wordsize).
@@ -412,8 +413,8 @@ Proof.
(* Oand *)
caseEq (intval app r1); intros.
rewrite (intval_correct _ _ H).
- replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil))
- with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil)).
+ replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil) m)
+ with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil) m).
apply make_andimm_correct.
simpl. destruct rs#r2; auto. rewrite Int.and_commut; auto.
caseEq (intval app r2); intros.
@@ -422,15 +423,15 @@ Proof.
(* Oandshift *)
caseEq (intval app r2); intros.
rewrite (intval_correct _ _ H).
- replace (eval_operation ge sp (Oandshift s) (rs # r1 :: Vint i :: nil))
- with (eval_operation ge sp Oand (rs # r1 :: Vint (eval_shift s i) :: nil)).
+ replace (eval_operation ge sp (Oandshift s) (rs # r1 :: Vint i :: nil) m)
+ with (eval_operation ge sp Oand (rs # r1 :: Vint (eval_shift s i) :: nil) m).
apply make_andimm_correct. reflexivity.
assumption.
(* Oor *)
caseEq (intval app r1); intros.
rewrite (intval_correct _ _ H).
- replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil))
- with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil)).
+ replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil) m)
+ with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil) m).
apply make_orimm_correct.
simpl. destruct rs#r2; auto. rewrite Int.or_commut; auto.
caseEq (intval app r2); intros.
@@ -439,15 +440,15 @@ Proof.
(* Oorshift *)
caseEq (intval app r2); intros.
rewrite (intval_correct _ _ H).
- replace (eval_operation ge sp (Oorshift s) (rs # r1 :: Vint i :: nil))
- with (eval_operation ge sp Oor (rs # r1 :: Vint (eval_shift s i) :: nil)).
+ replace (eval_operation ge sp (Oorshift s) (rs # r1 :: Vint i :: nil) m)
+ with (eval_operation ge sp Oor (rs # r1 :: Vint (eval_shift s i) :: nil) m).
apply make_orimm_correct. reflexivity.
assumption.
(* Oxor *)
caseEq (intval app r1); intros.
rewrite (intval_correct _ _ H).
- replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil))
- with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil)).
+ replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil) m)
+ with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil) m).
apply make_xorimm_correct.
simpl. destruct rs#r2; auto. rewrite Int.xor_commut; auto.
caseEq (intval app r2); intros.
@@ -456,22 +457,22 @@ Proof.
(* Oxorshift *)
caseEq (intval app r2); intros.
rewrite (intval_correct _ _ H).
- replace (eval_operation ge sp (Oxorshift s) (rs # r1 :: Vint i :: nil))
- with (eval_operation ge sp Oxor (rs # r1 :: Vint (eval_shift s i) :: nil)).
+ replace (eval_operation ge sp (Oxorshift s) (rs # r1 :: Vint i :: nil) m)
+ with (eval_operation ge sp Oxor (rs # r1 :: Vint (eval_shift s i) :: nil) m).
apply make_xorimm_correct. reflexivity.
assumption.
(* Obic *)
caseEq (intval app r2); intros.
rewrite (intval_correct _ _ H).
- replace (eval_operation ge sp Obic (rs # r1 :: Vint i :: nil))
- with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not i) :: nil)).
+ replace (eval_operation ge sp Obic (rs # r1 :: Vint i :: nil) m)
+ with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not i) :: nil) m).
apply make_andimm_correct. reflexivity.
assumption.
(* Obicshift *)
caseEq (intval app r2); intros.
rewrite (intval_correct _ _ H).
- replace (eval_operation ge sp (Obicshift s) (rs # r1 :: Vint i :: nil))
- with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not (eval_shift s i)) :: nil)).
+ replace (eval_operation ge sp (Obicshift s) (rs # r1 :: Vint i :: nil) m)
+ with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not (eval_shift s i)) :: nil) m).
apply make_andimm_correct. reflexivity.
assumption.
(* Oshl *)
diff --git a/arm/Op.v b/arm/Op.v
index 0a3504e..bb688ce 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -32,6 +32,7 @@ Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
+Require Import Events.
Set Implicit Arguments.
@@ -175,33 +176,36 @@ Definition eval_shift (s: shift) (n: int) : int :=
| Sror x => Int.ror n (s_amount x)
end.
-Definition eval_condition (cond: condition) (vl: list val):
+Definition eval_condition (cond: condition) (vl: list val) (m: mem):
option bool :=
match cond, vl with
| Ccomp c, Vint n1 :: Vint n2 :: nil =>
Some (Int.cmp c n1 n2)
- | Ccomp c, Vptr b1 n1 :: Vptr b2 n2 :: nil =>
- if eq_block b1 b2
- then Some (Int.cmp c n1 n2)
- else eval_compare_mismatch c
- | Ccomp c, Vptr b1 n1 :: Vint n2 :: nil =>
- eval_compare_null c n2
- | Ccomp c, Vint n1 :: Vptr b2 n2 :: nil =>
- eval_compare_null c n1
| Ccompu c, Vint n1 :: Vint n2 :: nil =>
Some (Int.cmpu c n1 n2)
+ | Ccompu c, Vptr b1 n1 :: Vptr b2 n2 :: nil =>
+ if Mem.valid_pointer m b1 (Int.unsigned n1)
+ && Mem.valid_pointer m b2 (Int.unsigned n2) then
+ if eq_block b1 b2
+ then Some (Int.cmpu c n1 n2)
+ else eval_compare_mismatch c
+ else None
+ | Ccompu c, Vptr b1 n1 :: Vint n2 :: nil =>
+ eval_compare_null c n2
+ | Ccompu c, Vint n1 :: Vptr b2 n2 :: nil =>
+ eval_compare_null c n1
| Ccompshift c s, Vint n1 :: Vint n2 :: nil =>
Some (Int.cmp c n1 (eval_shift s n2))
- | Ccompshift c s, Vptr b1 n1 :: Vint n2 :: nil =>
- eval_compare_null c (eval_shift s n2)
| Ccompushift c s, Vint n1 :: Vint n2 :: nil =>
Some (Int.cmpu c n1 (eval_shift s n2))
+ | Ccompushift c s, Vptr b1 n1 :: Vint n2 :: nil =>
+ eval_compare_null c (eval_shift s n2)
| Ccompimm c n, Vint n1 :: nil =>
Some (Int.cmp c n1 n)
- | Ccompimm c n, Vptr b1 n1 :: nil =>
- eval_compare_null c n
| Ccompuimm c n, Vint n1 :: nil =>
Some (Int.cmpu c n1 n)
+ | Ccompuimm c n, Vptr b1 n1 :: nil =>
+ eval_compare_null c n
| Ccompf c, Vfloat f1 :: Vfloat f2 :: nil =>
Some (Float.cmp c f1 f2)
| Cnotcompf c, Vfloat f1 :: Vfloat f2 :: nil =>
@@ -218,7 +222,7 @@ Definition offset_sp (sp: val) (delta: int) : option val :=
Definition eval_operation
(F V: Type) (genv: Genv.t F V) (sp: val)
- (op: operation) (vl: list val): option val :=
+ (op: operation) (vl: list val) (m: mem): option val :=
match op, vl with
| Omove, v1::nil => Some v1
| Ointconst n, nil => Some (Vint n)
@@ -285,7 +289,7 @@ Definition eval_operation
| Ointoffloat, Vfloat f1 :: nil => option_map Vint (Float.intoffloat f1)
| Ofloatofint, Vint n1 :: nil => Some (Vfloat (Float.floatofint n1))
| Ocmp c, _ =>
- match eval_condition c vl with
+ match eval_condition c vl m with
| None => None
| Some false => Some Vfalse
| Some true => Some Vtrue
@@ -346,24 +350,26 @@ Proof.
Qed.
Lemma eval_negate_condition:
- forall (cond: condition) (vl: list val) (b: bool),
- eval_condition cond vl = Some b ->
- eval_condition (negate_condition cond) vl = Some (negb b).
+ forall (cond: condition) (vl: list val) (b: bool) (m: mem),
+ eval_condition cond vl m = Some b ->
+ eval_condition (negate_condition cond) vl m = Some (negb b).
Proof.
intros.
destruct cond; simpl in H; FuncInv; try subst b; simpl.
rewrite Int.negate_cmp. auto.
+ rewrite Int.negate_cmpu. auto.
apply eval_negate_compare_null; auto.
apply eval_negate_compare_null; auto.
- destruct (eq_block b0 b1). rewrite Int.negate_cmp. congruence.
+ destruct (Mem.valid_pointer m b0 (Int.unsigned i) &&
+ Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate.
+ destruct (eq_block b0 b1). rewrite Int.negate_cmpu. congruence.
destruct c; simpl in H; inv H; auto.
- rewrite Int.negate_cmpu. auto.
rewrite Int.negate_cmp. auto.
- apply eval_negate_compare_null; auto.
rewrite Int.negate_cmpu. auto.
- rewrite Int.negate_cmp. auto.
apply eval_negate_compare_null; auto.
+ rewrite Int.negate_cmp. auto.
rewrite Int.negate_cmpu. auto.
+ apply eval_negate_compare_null; auto.
auto.
rewrite negb_elim. auto.
Qed.
@@ -382,8 +388,8 @@ Hypothesis agree_on_symbols:
forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s.
Lemma eval_operation_preserved:
- forall sp op vl,
- eval_operation ge2 sp op vl = eval_operation ge1 sp op vl.
+ forall sp op vl m,
+ eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m.
Proof.
intros.
unfold eval_operation; destruct op; try rewrite agree_on_symbols;
@@ -518,9 +524,9 @@ Variable A V: Type.
Variable genv: Genv.t A V.
Lemma type_of_operation_sound:
- forall op vl sp v,
+ forall op vl sp v m,
op <> Omove ->
- eval_operation genv sp op vl = Some v ->
+ eval_operation genv sp op vl m = Some v ->
Val.has_type v (snd (type_of_operation op)).
Proof.
intros.
@@ -684,22 +690,24 @@ Proof.
Qed.
Lemma eval_condition_weaken:
- forall c vl b,
- eval_condition c vl = Some b ->
+ forall c vl b m,
+ eval_condition c vl m = Some b ->
eval_condition_total c vl = Val.of_bool b.
Proof.
intros.
unfold eval_condition in H; destruct c; FuncInv;
try subst b; try reflexivity; simpl;
try (apply eval_compare_null_weaken; auto).
+ destruct (Mem.valid_pointer m b0 (Int.unsigned i) &&
+ Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate.
unfold eq_block in H. destruct (zeq b0 b1); try congruence.
apply eval_compare_mismatch_weaken; auto.
symmetry. apply Val.notbool_negb_1.
Qed.
Lemma eval_operation_weaken:
- forall sp op vl v,
- eval_operation genv sp op vl = Some v ->
+ forall sp op vl v m,
+ eval_operation genv sp op vl m = Some v ->
eval_operation_total sp op vl = v.
Proof.
intros.
@@ -721,7 +729,7 @@ Proof.
assert (Int.unsigned (Int.repr 31) < Int.unsigned Int.iwordsize). vm_compute; auto.
omega. discriminate.
destruct (Float.intoffloat f); simpl in H; inv H. auto.
- caseEq (eval_condition c vl); intros; rewrite H0 in H.
+ caseEq (eval_condition c vl m); intros; rewrite H0 in H.
replace v with (Val.of_bool b).
eapply eval_condition_weaken; eauto.
destruct b; simpl; congruence.
@@ -783,12 +791,20 @@ Ltac InvLessdef :=
end.
Lemma eval_condition_lessdef:
- forall cond vl1 vl2 b,
+ forall cond vl1 vl2 b m1 m2,
Val.lessdef_list vl1 vl2 ->
- eval_condition cond vl1 = Some b ->
- eval_condition cond vl2 = Some b.
+ Mem.extends m1 m2 ->
+ eval_condition cond vl1 m1 = Some b ->
+ eval_condition cond vl2 m2 = Some b.
Proof.
intros. destruct cond; simpl in *; FuncInv; InvLessdef; auto.
+ destruct (Mem.valid_pointer m1 b0 (Int.unsigned i) &&
+ Mem.valid_pointer m1 b1 (Int.unsigned i0)) as [] _eqn; try discriminate.
+ destruct (andb_prop _ _ Heqb2) as [A B].
+ assert (forall b ofs, Mem.valid_pointer m1 b ofs = true -> Mem.valid_pointer m2 b ofs = true).
+ intros until ofs. repeat rewrite Mem.valid_pointer_nonempty_perm.
+ apply Mem.perm_extends; auto.
+ rewrite (H _ _ A). rewrite (H _ _ B). auto.
Qed.
Ltac TrivialExists :=
@@ -799,34 +815,36 @@ Ltac TrivialExists :=
end.
Lemma eval_operation_lessdef:
- forall sp op vl1 vl2 v1,
+ forall sp op vl1 vl2 v1 m1 m2,
Val.lessdef_list vl1 vl2 ->
- eval_operation genv sp op vl1 = Some v1 ->
- exists v2, eval_operation genv sp op vl2 = Some v2 /\ Val.lessdef v1 v2.
+ Mem.extends m1 m2 ->
+ eval_operation genv sp op vl1 m1 = Some v1 ->
+ exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2.
Proof.
intros. destruct op; simpl in *; FuncInv; InvLessdef; TrivialExists.
exists v2; auto.
- destruct (Genv.find_symbol genv i); inv H0. TrivialExists.
+ destruct (Genv.find_symbol genv i); inv H1. TrivialExists.
exists v1; auto.
exists (Val.sign_ext 8 v2); split. auto. apply Val.sign_ext_lessdef; auto.
exists (Val.zero_ext 8 v2); split. auto. apply Val.zero_ext_lessdef; auto.
exists (Val.sign_ext 16 v2); split. auto. apply Val.sign_ext_lessdef; auto.
exists (Val.zero_ext 16 v2); split. auto. apply Val.zero_ext_lessdef; auto.
- destruct (eq_block b b0); inv H0. TrivialExists.
- destruct (Int.eq i0 Int.zero); inv H0; TrivialExists.
- destruct (Int.eq i0 Int.zero); inv H0; TrivialExists.
- destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists.
- destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists.
- destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists.
+ destruct (eq_block b b0); inv H1. TrivialExists.
+ destruct (Int.eq i0 Int.zero); inv H1; TrivialExists.
+ destruct (Int.eq i0 Int.zero); inv H1; TrivialExists.
destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists.
destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists.
- destruct (Int.ltu i (Int.repr 31)); inv H0; TrivialExists.
+ destruct (Int.ltu i Int.iwordsize); inv H1; TrivialExists.
+ destruct (Int.ltu i0 Int.iwordsize); inv H2; TrivialExists.
+ destruct (Int.ltu i0 Int.iwordsize); inv H2; TrivialExists.
+ destruct (Int.ltu i (Int.repr 31)); inv H1; TrivialExists.
exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto.
- destruct (Float.intoffloat f); simpl in *; inv H0. TrivialExists.
- caseEq (eval_condition c vl1); intros. rewrite H1 in H0.
- rewrite (eval_condition_lessdef c H H1).
- destruct b; inv H0; TrivialExists.
- rewrite H1 in H0. discriminate.
+ destruct (Float.intoffloat f); simpl in *; inv H1. TrivialExists.
+ exists v1; split; auto.
+ destruct (eval_condition c vl1 m1) as [] _eqn.
+ rewrite (eval_condition_lessdef c H H0 Heqo).
+ auto.
+ discriminate.
Qed.
Lemma eval_addressing_lessdef:
@@ -841,6 +859,154 @@ Qed.
End EVAL_LESSDEF.
+(** Shifting stack-relative references. This is used in [Stacking]. *)
+
+Definition shift_stack_addressing (delta: int) (addr: addressing) :=
+ match addr with
+ | Ainstack ofs => Ainstack (Int.add delta ofs)
+ | _ => addr
+ end.
+
+Definition shift_stack_operation (delta: int) (op: operation) :=
+ match op with
+ | Oaddrstack ofs => Oaddrstack (Int.add delta ofs)
+ | _ => op
+ end.
+
+Lemma type_shift_stack_addressing:
+ forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr.
+Proof.
+ intros. destruct addr; auto.
+Qed.
+
+Lemma type_shift_stack_operation:
+ forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op.
+Proof.
+ intros. destruct op; auto.
+Qed.
+
+(** Compatibility of the evaluation functions with memory injections. *)
+
+Section EVAL_INJECT.
+
+Variable F V: Type.
+Variable genv: Genv.t F V.
+Variable f: meminj.
+Hypothesis globals: meminj_preserves_globals genv f.
+Variable sp1: block.
+Variable sp2: block.
+Variable delta: Z.
+Hypothesis sp_inj: f sp1 = Some(sp2, delta).
+
+Ltac InvInject :=
+ match goal with
+ | [ H: val_inject _ (Vint _) _ |- _ ] =>
+ inv H; InvInject
+ | [ H: val_inject _ (Vfloat _) _ |- _ ] =>
+ inv H; InvInject
+ | [ H: val_inject _ (Vptr _ _) _ |- _ ] =>
+ inv H; InvInject
+ | [ H: val_list_inject _ nil _ |- _ ] =>
+ inv H; InvInject
+ | [ H: val_list_inject _ (_ :: _) _ |- _ ] =>
+ inv H; InvInject
+ | _ => idtac
+ end.
+
+Lemma eval_condition_inject:
+ forall cond vl1 vl2 b m1 m2,
+ val_list_inject f vl1 vl2 ->
+ Mem.inject f m1 m2 ->
+ eval_condition cond vl1 m1 = Some b ->
+ eval_condition cond vl2 m2 = Some b.
+Proof.
+ intros. destruct cond; simpl in *; FuncInv; InvInject; auto.
+ destruct (Mem.valid_pointer m1 b0 (Int.unsigned i)) as [] _eqn; try discriminate.
+ destruct (Mem.valid_pointer m1 b1 (Int.unsigned i0)) as [] _eqn; try discriminate.
+ simpl in H1.
+ exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb0. econstructor; eauto.
+ intros V1. rewrite V1.
+ exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb2. econstructor; eauto.
+ intros V2. rewrite V2.
+ simpl.
+ destruct (eq_block b0 b1); inv H1.
+ rewrite H3 in H5; inv H5. rewrite dec_eq_true.
+ decEq. apply Int.translate_cmpu.
+ eapply Mem.valid_pointer_inject_no_overflow; eauto.
+ eapply Mem.valid_pointer_inject_no_overflow; eauto.
+ exploit Mem.different_pointers_inject; eauto. intros P.
+ destruct (eq_block b3 b4); auto.
+ destruct P. contradiction.
+ destruct c; unfold eval_compare_mismatch in *; inv H2.
+ unfold Int.cmpu. rewrite Int.eq_false; auto. congruence.
+ unfold Int.cmpu. rewrite Int.eq_false; auto. congruence.
+Qed.
+
+Ltac TrivialExists2 :=
+ match goal with
+ | [ |- exists v2, Some ?v1 = Some v2 /\ val_inject _ _ v2 ] =>
+ exists v1; split; [auto | econstructor; eauto]
+ | _ => idtac
+ end.
+
+Lemma eval_addressing_inject:
+ forall addr vl1 vl2 v1,
+ val_list_inject f vl1 vl2 ->
+ eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 ->
+ exists v2,
+ eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2
+ /\ val_inject f v1 v2.
+Proof.
+ assert (UNUSED: meminj_preserves_globals genv f). exact globals.
+ intros. destruct addr; simpl in *; FuncInv; InvInject; TrivialExists2.
+ repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+ repeat rewrite Int.add_assoc. auto.
+ repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+ repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+ repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+Qed.
+
+Lemma eval_operation_inject:
+ forall op vl1 vl2 v1 m1 m2,
+ val_list_inject f vl1 vl2 ->
+ Mem.inject f m1 m2 ->
+ eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 ->
+ exists v2,
+ eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2
+ /\ val_inject f v1 v2.
+Proof.
+ intros. destruct op; simpl in *; FuncInv; InvInject; TrivialExists2.
+ exists v'; auto.
+ destruct (Genv.find_symbol genv i) as [] _eqn; inv H1.
+ TrivialExists2. eapply (proj1 globals); eauto. rewrite Int.add_zero; auto.
+ repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+ exists (Val.sign_ext 8 v'); split; auto. inv H4; simpl; auto.
+ exists (Val.zero_ext 8 v'); split; auto. inv H4; simpl; auto.
+ exists (Val.sign_ext 16 v'); split; auto. inv H4; simpl; auto.
+ exists (Val.zero_ext 16 v'); split; auto. inv H4; simpl; auto.
+ repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+ repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+ repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+ repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+ rewrite Int.sub_add_l. auto.
+ destruct (eq_block b b0); inv H1. rewrite H3 in H5; inv H5. rewrite dec_eq_true.
+ rewrite Int.sub_shifted. TrivialExists2.
+ rewrite Int.sub_add_l. auto.
+ destruct (Int.eq i0 Int.zero); inv H1. TrivialExists2.
+ destruct (Int.eq i0 Int.zero); inv H1. TrivialExists2.
+ destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2.
+ destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2.
+ destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2.
+ destruct (Int.ltu i (Int.repr 31)); inv H1. TrivialExists2.
+ exists (Val.singleoffloat v'); split; auto. inv H4; simpl; auto.
+ destruct (Float.intoffloat f0); simpl in *; inv H1. TrivialExists2.
+ destruct (eval_condition c vl1 m1) as [] _eqn; try discriminate.
+ exploit eval_condition_inject; eauto. intros EQ; rewrite EQ.
+ destruct b; inv H1; TrivialExists2.
+Qed.
+
+End EVAL_INJECT.
+
(** Recognition of integers that are valid shift amounts. *)
Definition is_shift_amount_aux (n: int) :
@@ -891,10 +1057,10 @@ Definition op_for_binary_addressing (addr: addressing) : operation :=
end.
Lemma eval_op_for_binary_addressing:
- forall (F V: Type) (ge: Genv.t F V) sp addr args v,
+ forall (F V: Type) (ge: Genv.t F V) sp addr args v m,
(length args >= 2)%nat ->
eval_addressing ge sp addr args = Some v ->
- eval_operation ge sp (op_for_binary_addressing addr) args = Some v.
+ eval_operation ge sp (op_for_binary_addressing addr) args m = Some v.
Proof.
intros.
unfold eval_addressing in H0; destruct addr; FuncInv; simpl in H; try omegaContradiction; simpl.
@@ -926,54 +1092,22 @@ Definition is_trivial_op (op: operation) : bool :=
| _ => false
end.
-(** Shifting stack-relative references. This is used in [Stacking]. *)
-Definition shift_stack_addressing (delta: int) (addr: addressing) :=
- match addr with
- | Ainstack ofs => Ainstack (Int.add delta ofs)
- | _ => addr
- end.
+(** Operations that depend on the memory state. *)
-Definition shift_stack_operation (delta: int) (op: operation) :=
+Definition op_depends_on_memory (op: operation) : bool :=
match op with
- | Oaddrstack ofs => Oaddrstack (Int.add delta ofs)
- | _ => op
+ | Ocmp (Ccompu _) => true
+ | _ => false
end.
-Lemma shift_stack_eval_addressing:
- forall (F V: Type) (ge: Genv.t F V) sp addr args delta,
- eval_addressing ge (Val.sub sp (Vint delta)) (shift_stack_addressing delta addr) args =
- eval_addressing ge sp addr args.
+Lemma op_depends_on_memory_correct:
+ forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
+ op_depends_on_memory op = false ->
+ eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
Proof.
- intros. destruct addr; simpl; auto.
- destruct args; auto. unfold offset_sp. destruct sp; simpl; auto.
- decEq. decEq. rewrite <- Int.add_assoc. decEq.
- rewrite Int.sub_add_opp. rewrite Int.add_assoc.
- rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp.
- rewrite Int.sub_idem. apply Int.add_zero.
+ intros until m2. destruct op; simpl; try congruence.
+ destruct c; simpl; congruence.
Qed.
-Lemma shift_stack_eval_operation:
- forall (F V: Type) (ge: Genv.t F V) sp op args delta,
- eval_operation ge (Val.sub sp (Vint delta)) (shift_stack_operation delta op) args =
- eval_operation ge sp op args.
-Proof.
- intros. destruct op; simpl; auto.
- destruct args; auto. unfold offset_sp. destruct sp; simpl; auto.
- decEq. decEq. rewrite <- Int.add_assoc. decEq.
- rewrite Int.sub_add_opp. rewrite Int.add_assoc.
- rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp.
- rewrite Int.sub_idem. apply Int.add_zero.
-Qed.
-Lemma type_shift_stack_addressing:
- forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr.
-Proof.
- intros. destruct addr; auto.
-Qed.
-
-Lemma type_shift_stack_operation:
- forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op.
-Proof.
- intros. destruct op; auto.
-Qed.
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 4f470ce..883ee72 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -453,30 +453,21 @@ let print_instruction oc labels = function
| Psufd(r1, r2, r3) ->
fprintf oc " sufd %a, %a, %a\n" freg r1 freg r2 freg r3; 1
(* Pseudo-instructions *)
- | Pallocframe(lo, hi, ofs) ->
- let lo = camlint_of_coqint lo
- and hi = camlint_of_coqint hi
- and ofs = camlint_of_coqint ofs in
- let sz = Int32.sub hi lo in
- (* Keep stack 4-aligned *)
- let sz4 = Int32.logand (Int32.add sz 3l) 0xFFFF_FFFCl in
- (* FIXME: consider a store multiple? *)
- (* R12 = first int temporary is unused at this point,
- but this should be reflected in the proof *)
+ | Pallocframe(sz, ofs) ->
fprintf oc " mov r12, sp\n";
let ninstr = ref 0 in
List.iter
- (fun mask ->
- let b = Int32.logand sz4 mask in
- if b <> 0l then begin
- fprintf oc " sub sp, sp, #%ld\n" b;
- incr ninstr
- end)
- [0xFF000000l; 0x00FF0000l; 0x0000FF00l; 0x000000FFl];
- fprintf oc " str r12, [sp, #%ld]\n" ofs;
+ (fun n ->
+ fprintf oc " sub sp, sp, #%a\n" coqint n;
+ incr ninstr)
+ (Asmgen.decompose_int sz);
+ fprintf oc " str r12, [sp, #%a]\n" coqint ofs;
2 + !ninstr
- | Pfreeframe(lo, hi, ofs) ->
- fprintf oc " ldr sp, [sp, #%a]\n" coqint ofs; 1
+ | Pfreeframe(sz, ofs) ->
+ if Asmgen.is_immed_arith sz
+ then fprintf oc " add sp, sp, #%a\n" coqint sz
+ else fprintf oc " ldr sp, [sp, #%a]\n" coqint ofs;
+ 1
| Plabel lbl ->
if Labelset.mem lbl labels then
fprintf oc "%a:\n" print_label lbl; 0
diff --git a/arm/SelectOp.v b/arm/SelectOp.v
index df2413a..44528c6 100644
--- a/arm/SelectOp.v
+++ b/arm/SelectOp.v
@@ -146,7 +146,7 @@ Definition notint (e: expr) :=
(** ** Boolean negation *)
Definition notbool_base (e: expr) :=
- Eop (Ocmp (Ccompimm Ceq Int.zero)) (e ::: Enil).
+ Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil).
Fixpoint notbool (e: expr) {struct e} : expr :=
match e with
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index cdb21cb..7602b11 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -64,13 +64,13 @@ Ltac InvEval1 :=
Ltac InvEval2 :=
match goal with
- | [ H: (eval_operation _ _ _ nil = Some _) |- _ ] =>
+ | [ H: (eval_operation _ _ _ nil _ = Some _) |- _ ] =>
simpl in H; inv H
- | [ H: (eval_operation _ _ _ (_ :: nil) = Some _) |- _ ] =>
+ | [ H: (eval_operation _ _ _ (_ :: nil) _ = Some _) |- _ ] =>
simpl in H; FuncInv
- | [ H: (eval_operation _ _ _ (_ :: _ :: nil) = Some _) |- _ ] =>
+ | [ H: (eval_operation _ _ _ (_ :: _ :: nil) _ = Some _) |- _ ] =>
simpl in H; FuncInv
- | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) = Some _) |- _ ] =>
+ | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) _ = Some _) |- _ ] =>
simpl in H; FuncInv
| _ =>
idtac
@@ -162,12 +162,12 @@ Proof.
eapply eval_notbool_base; eauto.
inv H. eapply eval_Eop; eauto.
- simpl. assert (eval_condition c vl = Some b).
+ simpl. assert (eval_condition c vl m = Some b).
generalize H6. simpl.
case (eval_condition c vl); intros.
destruct b0; inv H1; inversion H0; auto; congruence.
congruence.
- rewrite (Op.eval_negate_condition _ _ H).
+ rewrite (Op.eval_negate_condition _ _ _ H).
destruct b; reflexivity.
inv H. eapply eval_Econdition; eauto.
@@ -524,9 +524,9 @@ Qed.
Lemma eval_mod_aux:
forall divop semdivop,
- (forall sp x y,
+ (forall sp x y m,
y <> Int.zero ->
- eval_operation ge sp divop (Vint x :: Vint y :: nil) =
+ eval_operation ge sp divop (Vint x :: Vint y :: nil) m =
Some (Vint (semdivop x y))) ->
forall le a b x y,
eval_expr ge sp e m le a (Vint x) ->
@@ -757,7 +757,7 @@ Theorem eval_singleoffloat:
eval_expr ge sp e m le (singleoffloat a) (Val.singleoffloat v).
Proof. TrivialOp singleoffloat. Qed.
-Theorem eval_comp_int:
+Theorem eval_comp:
forall le c a x b y,
eval_expr ge sp e m le a (Vint x) ->
eval_expr ge sp e m le b (Vint y) ->
@@ -767,11 +767,26 @@ Proof.
unfold comp; case (comp_match a b); intros; InvEval.
EvalOp. simpl. rewrite Int.swap_cmp. destruct (Int.cmp c x y); reflexivity.
EvalOp. simpl. destruct (Int.cmp c x y); reflexivity.
- EvalOp. simpl. rewrite Int.swap_cmp. rewrite H. destruct (Int.cmp c x y); reflexivity.
+ EvalOp. simpl. rewrite H. rewrite Int.swap_cmp. destruct (Int.cmp c x y); reflexivity.
EvalOp. simpl. rewrite H0. destruct (Int.cmp c x y); reflexivity.
EvalOp. simpl. destruct (Int.cmp c x y); reflexivity.
Qed.
+Theorem eval_compu_int:
+ forall le c a x b y,
+ eval_expr ge sp e m le a (Vint x) ->
+ eval_expr ge sp e m le b (Vint y) ->
+ eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)).
+Proof.
+ intros until y.
+ unfold compu; case (comp_match a b); intros; InvEval.
+ EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity.
+ EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity.
+ EvalOp. simpl. rewrite Int.swap_cmpu. rewrite H. destruct (Int.cmpu c x y); reflexivity.
+ EvalOp. simpl. rewrite H0. destruct (Int.cmpu c x y); reflexivity.
+ EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity.
+Qed.
+
Remark eval_compare_null_trans:
forall c x v,
(if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v ->
@@ -786,15 +801,15 @@ Proof.
destruct c; try discriminate; auto.
Qed.
-Theorem eval_comp_ptr_int:
+Theorem eval_compu_ptr_int:
forall le c a x1 x2 b y v,
eval_expr ge sp e m le a (Vptr x1 x2) ->
eval_expr ge sp e m le b (Vint y) ->
(if Int.eq y Int.zero then Cminor.eval_compare_mismatch c else None) = Some v ->
- eval_expr ge sp e m le (comp c a b) v.
+ eval_expr ge sp e m le (compu c a b) v.
Proof.
intros until v.
- unfold comp; case (comp_match a b); intros; InvEval.
+ unfold compu; case (comp_match a b); intros; InvEval.
EvalOp. simpl. apply eval_compare_null_trans; auto.
EvalOp. simpl. rewrite H0. apply eval_compare_null_trans; auto.
EvalOp. simpl. apply eval_compare_null_trans; auto.
@@ -814,61 +829,49 @@ Proof.
destruct c; simpl; try discriminate; auto.
Qed.
-Theorem eval_comp_int_ptr:
+Theorem eval_compu_int_ptr:
forall le c a x b y1 y2 v,
eval_expr ge sp e m le a (Vint x) ->
eval_expr ge sp e m le b (Vptr y1 y2) ->
(if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v ->
- eval_expr ge sp e m le (comp c a b) v.
+ eval_expr ge sp e m le (compu c a b) v.
Proof.
intros until v.
- unfold comp; case (comp_match a b); intros; InvEval.
+ unfold compu; case (comp_match a b); intros; InvEval.
EvalOp. simpl. apply eval_swap_compare_null_trans; auto.
EvalOp. simpl. rewrite H. apply eval_swap_compare_null_trans; auto.
EvalOp. simpl. apply eval_compare_null_trans; auto.
Qed.
-Theorem eval_comp_ptr_ptr:
+Theorem eval_compu_ptr_ptr:
forall le c a x1 x2 b y1 y2,
eval_expr ge sp e m le a (Vptr x1 x2) ->
eval_expr ge sp e m le b (Vptr y1 y2) ->
+ Mem.valid_pointer m x1 (Int.unsigned x2)
+ && Mem.valid_pointer m y1 (Int.unsigned y2) = true ->
x1 = y1 ->
- eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x2 y2)).
+ eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x2 y2)).
Proof.
intros until y2.
- unfold comp; case (comp_match a b); intros; InvEval.
- EvalOp. simpl. subst y1. rewrite dec_eq_true.
- destruct (Int.cmp c x2 y2); reflexivity.
+ unfold compu; case (comp_match a b); intros; InvEval.
+ EvalOp. simpl. rewrite H1. subst y1. rewrite dec_eq_true.
+ destruct (Int.cmpu c x2 y2); reflexivity.
Qed.
-Theorem eval_comp_ptr_ptr_2:
+Theorem eval_compu_ptr_ptr_2:
forall le c a x1 x2 b y1 y2 v,
eval_expr ge sp e m le a (Vptr x1 x2) ->
eval_expr ge sp e m le b (Vptr y1 y2) ->
+ Mem.valid_pointer m x1 (Int.unsigned x2)
+ && Mem.valid_pointer m y1 (Int.unsigned y2) = true ->
x1 <> y1 ->
Cminor.eval_compare_mismatch c = Some v ->
- eval_expr ge sp e m le (comp c a b) v.
+ eval_expr ge sp e m le (compu c a b) v.
Proof.
intros until y2.
- unfold comp; case (comp_match a b); intros; InvEval.
- EvalOp. simpl. rewrite dec_eq_false; auto.
- destruct c; simpl in H2; inv H2; auto.
-Qed.
-
-
-Theorem eval_compu:
- forall le c a x b y,
- eval_expr ge sp e m le a (Vint x) ->
- eval_expr ge sp e m le b (Vint y) ->
- eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)).
-Proof.
- intros until y.
unfold compu; case (comp_match a b); intros; InvEval.
- EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity.
- EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity.
- EvalOp. simpl. rewrite H. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity.
- EvalOp. simpl. rewrite H0. destruct (Int.cmpu c x y); reflexivity.
- EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity.
+ EvalOp. simpl. rewrite H1. rewrite dec_eq_false; auto.
+ destruct c; simpl in H3; inv H3; auto.
Qed.
Theorem eval_compf:
diff --git a/arm/linux/Stacklayout.v b/arm/linux/Stacklayout.v
index b374bfd..4521114 100644
--- a/arm/linux/Stacklayout.v
+++ b/arm/linux/Stacklayout.v
@@ -28,12 +28,6 @@ Require Import Bounds.
- Pointer to activation record of the caller.
- Space for the stack-allocated data declared in Cminor.
-To facilitate some of the proofs, the Cminor stack-allocated data
-starts at offset 0; the preceding areas in the activation record
-therefore have negative offsets. This part (with negative offsets)
-is called the ``frame'', by opposition with the ``Cminor stack data''
-which is the part with positive offsets.
-
The [frame_env] compilation environment records the positions of
the boundaries between areas in the frame part.
*)
@@ -49,7 +43,8 @@ Record frame_env : Type := mk_frame_env {
fe_num_int_callee_save: Z;
fe_ofs_float_local: Z;
fe_ofs_float_callee_save: Z;
- fe_num_float_callee_save: Z
+ fe_num_float_callee_save: Z;
+ fe_stack_data: Z
}.
(** Computation of the frame environment from the bounds of the current
@@ -63,17 +58,84 @@ Definition make_env (b: bounds) :=
let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *)
let ora := ofcs + 8 * b.(bound_float_callee_save) in (* retaddr *)
let olink := ora + 4 in (* back link *)
- let sz := olink + 4 in (* total frame size *)
+ 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).
+ ofl ofcs b.(bound_float_callee_save)
+ ostkdata.
+(** Separation property *)
-Remark align_float_part:
+Remark frame_env_separated:
forall b,
- 4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b <=
- align (4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b) 8.
+ 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.(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. apply align_le. omega.
+ 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 _)).
+ 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_stack_data, fe_ofs_arg.
+ intros.
+ generalize (bound_int_local_pos b); intro;
+ generalize (bound_float_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;
+ generalize (bound_stack_data_pos b); intro.
+ omega.
Qed.
+(** Alignment property *)
+
+Remark frame_env_aligned:
+ forall b,
+ let fe := make_env b in
+ (4 | fe.(fe_ofs_link))
+ /\ (4 | fe.(fe_ofs_int_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))
+ /\ (4 | fe.(fe_stack_data))
+ /\ (8 | fe.(fe_size)).
+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_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 (4 | x6).
+ apply Zdivides_trans with 8. exists 2; auto.
+ unfold x6. apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring.
+ set (x7 := x6 + 4).
+ assert (4 | x7). unfold x7; apply Zdivide_plus_r; auto. exists 1; auto.
+ set (x8 := x7 + 4).
+ assert (4 | x8). unfold x8; 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.
+ tauto.
+Qed.