summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--arm/Asm.v170
-rw-r--r--arm/Asmgen.v84
-rw-r--r--arm/Asmgenproof1.v434
-rw-r--r--arm/PrintAsm.ml40
-rw-r--r--common/Values.v12
-rw-r--r--ia32/Asm.v47
-rw-r--r--ia32/Asmgenproof1.v62
-rw-r--r--lib/Floats.v6
-rw-r--r--lib/Integers.v127
9 files changed, 655 insertions, 327 deletions
diff --git a/arm/Asm.v b/arm/Asm.v
index 769b3f9..43a1435 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -51,18 +51,10 @@ Proof. decide equality. Defined.
(** Bits in the condition register. *)
Inductive crbit: Type :=
- | CReq: crbit (**r equal *)
- | CRne: crbit (**r not equal *)
- | CRhs: crbit (**r unsigned higher or same *)
- | CRlo: crbit (**r unsigned lower *)
- | CRmi: crbit (**r negative *)
- | CRpl: crbit (**r positive *)
- | CRhi: crbit (**r unsigned higher *)
- | CRls: crbit (**r unsigned lower or same *)
- | CRge: crbit (**r signed greater or equal *)
- | CRlt: crbit (**r signed less than *)
- | CRgt: crbit (**r signed greater *)
- | CRle: crbit. (**r signed less than or equal *)
+ | CN: crbit (**r negative *)
+ | CZ: crbit (**r zero *)
+ | CC: crbit (**r carry *)
+ | CV: crbit. (**r overflow *)
Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}.
Proof. decide equality. Defined.
@@ -123,12 +115,26 @@ Inductive shift_addr : Type :=
| SAasr: ireg -> int -> shift_addr
| SAror: ireg -> int -> shift_addr.
+Inductive testcond : Type :=
+ | TCeq: testcond (**r equal *)
+ | TCne: testcond (**r not equal *)
+ | TChs: testcond (**r unsigned higher or same *)
+ | TClo: testcond (**r unsigned lower *)
+ | TCmi: testcond (**r negative *)
+ | TCpl: testcond (**r positive *)
+ | TChi: testcond (**r unsigned higher *)
+ | TCls: testcond (**r unsigned lower or same *)
+ | TCge: testcond (**r signed greater or equal *)
+ | TClt: testcond (**r signed less than *)
+ | TCgt: testcond (**r signed greater *)
+ | TCle: testcond. (**r signed less than or equal *)
+
Inductive instruction : Type :=
(* Core instructions *)
| Padd: ireg -> ireg -> shift_op -> instruction (**r integer addition *)
| Pand: ireg -> ireg -> shift_op -> instruction (**r bitwise and *)
| Pb: label -> instruction (**r branch to label *)
- | Pbc: crbit -> label -> instruction (**r conditional branch to label *)
+ | Pbc: testcond -> label -> instruction (**r conditional branch to label *)
| Pbsymb: ident -> signature -> instruction (**r branch to symbol *)
| Pbreg: ireg -> signature -> instruction (**r computed branch *)
| Pblsymb: ident -> signature -> instruction (**r branch and link to symbol *)
@@ -143,7 +149,7 @@ Inductive instruction : Type :=
| Pldrsh: ireg -> ireg -> shift_addr -> instruction (**r unsigned int16 load *)
| Pmla: ireg -> ireg -> ireg -> ireg -> instruction (**r integer multiply-add *)
| Pmov: ireg -> shift_op -> instruction (**r integer move *)
- | Pmovc: crbit -> ireg -> shift_op -> instruction (**r integer conditional move *)
+ | Pmovc: testcond -> ireg -> shift_op -> instruction (**r integer conditional move *)
| Pmul: ireg -> ireg -> ireg -> instruction (**r integer multiplication *)
| Pmvn: ireg -> shift_op -> instruction (**r integer complement *)
| Porr: ireg -> ireg -> shift_op -> instruction (**r bitwise or *)
@@ -376,44 +382,102 @@ Definition exec_store (chunk: memory_chunk) (addr: val) (r: preg)
| Some m' => Next (nextinstr rs) m'
end.
-(** Operations over condition bits. *)
+(** Comparisons. *)
Definition compare_int (rs: regset) (v1 v2: val) (m: mem) :=
- rs#CReq <- (Val.cmpu (Mem.valid_pointer m) Ceq v1 v2)
- #CRne <- (Val.cmpu (Mem.valid_pointer m) Cne v1 v2)
- #CRhs <- (Val.cmpu (Mem.valid_pointer m) Cge v1 v2)
- #CRlo <- (Val.cmpu (Mem.valid_pointer m) Clt v1 v2)
- #CRmi <- Vundef
- #CRpl <- Vundef
- #CRhi <- (Val.cmpu (Mem.valid_pointer m) Cgt v1 v2)
- #CRls <- (Val.cmpu (Mem.valid_pointer m) Cle v1 v2)
- #CRge <- (Val.cmp Cge v1 v2)
- #CRlt <- (Val.cmp Clt v1 v2)
- #CRgt <- (Val.cmp Cgt v1 v2)
- #CRle <- (Val.cmp Cle v1 v2).
+ rs#CN <- (Val.negative (Val.sub v1 v2))
+ #CZ <- (Val.cmpu (Mem.valid_pointer m) Ceq v1 v2)
+ #CC <- (Val.cmpu (Mem.valid_pointer m) Cge v1 v2)
+ #CV <- (Val.sub_overflow v1 v2).
(** Semantics of [fcmpd] instruction:
<<
-== EQ=1 NE=0 HS=1 LO=0 MI=0 PL=1 VS=0 VC=1 HI=0 LS=1 GE=1 LT=0 GT=0 LE=1
-< EQ=0 NE=1 HS=0 LO=1 MI=1 PL=0 VS=0 VC=1 HI=0 LS=1 GE=0 LT=1 GT=0 LE=1
-> EQ=0 NE=1 HS=1 LO=0 MI=0 PL=1 VS=0 VC=1 HI=1 LS=0 GE=1 LT=0 GT=1 LE=0
-unord EQ=0 NE=1 HS=1 LO=0 MI=0 PL=1 VS=1 VC=0 HI=1 LS=0 GE=0 LT=1 GT=0 LE=1
+== N=0 Z=1 C=1 V=0
+< N=1 Z=0 C=0 V=0
+> N=0 Z=0 C=1 V=0
+unord N=0 Z=0 C=1 V=1
>>
*)
Definition compare_float (rs: regset) (v1 v2: val) :=
- rs#CReq <- (Val.cmpf Ceq v1 v2)
- #CRne <- (Val.cmpf Cne v1 v2)
- #CRhs <- (Val.notbool (Val.cmpf Clt v1 v2)) (**r not lt *)
- #CRlo <- (Val.cmpf Clt v1 v2) (**r lt *)
- #CRmi <- (Val.cmpf Clt v1 v2) (**r lt *)
- #CRpl <- (Val.notbool (Val.cmpf Clt v1 v2)) (**r not lt *)
- #CRhi <- (Val.notbool (Val.cmpf Cle v1 v2)) (**r not le *)
- #CRls <- (Val.cmpf Cle v1 v2) (**r le *)
- #CRge <- (Val.cmpf Cge v1 v2) (**r ge *)
- #CRlt <- (Val.notbool (Val.cmpf Cge v1 v2)) (**r not ge *)
- #CRgt <- (Val.cmpf Cgt v1 v2) (**r gt *)
- #CRle <- (Val.notbool (Val.cmpf Cgt v1 v2)). (**r not gt *)
+ match v1, v2 with
+ | Vfloat f1, Vfloat f2 =>
+ rs#CN <- (Val.of_bool (Float.cmp Clt f1 f2))
+ #CZ <- (Val.of_bool (Float.cmp Ceq f1 f2))
+ #CC <- (Val.of_bool (negb (Float.cmp Clt f1 f2)))
+ #CV <- (Val.of_bool (negb (Float.cmp Ceq f1 f2 || Float.cmp Clt f1 f2 || Float.cmp Cgt f1 f2)))
+ | _, _ =>
+ rs#CN <- Vundef
+ #CZ <- Vundef
+ #CC <- Vundef
+ #CV <- Vundef
+ end.
+
+(** Testing a condition *)
+
+Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
+ match c with
+ | TCeq => (**r equal *)
+ match rs CZ with
+ | Vint n => Some (Int.eq n Int.one)
+ | _ => None
+ end
+ | TCne => (**r not equal *)
+ match rs CZ with
+ | Vint n => Some (Int.eq n Int.zero)
+ | _ => None
+ end
+ | TClo => (**r unsigned less than *)
+ match rs CC with
+ | Vint n => Some (Int.eq n Int.zero)
+ | _ => None
+ end
+ | TCls => (**r unsigned less or equal *)
+ match rs CC, rs CZ with
+ | Vint c, Vint z => Some (Int.eq c Int.zero || Int.eq z Int.one)
+ | _, _ => None
+ end
+ | TChs => (**r unsigned greater or equal *)
+ match rs CC with
+ | Vint n => Some (Int.eq n Int.one)
+ | _ => None
+ end
+ | TChi => (**r unsigned greater *)
+ match rs CC, rs CZ with
+ | Vint c, Vint z => Some (Int.eq c Int.one && Int.eq z Int.zero)
+ | _, _ => None
+ end
+ | TClt => (**r signed less than *)
+ match rs CV, rs CN with
+ | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.one)
+ | _, _ => None
+ end
+ | TCle => (**r signed less or equal *)
+ match rs CV, rs CN, rs CZ with
+ | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.one || Int.eq z Int.one)
+ | _, _, _ => None
+ end
+ | TCge => (**r signed greater or equal *)
+ match rs CV, rs CN with
+ | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.zero)
+ | _, _ => None
+ end
+ | TCgt => (**r signed greater *)
+ match rs CV, rs CN, rs CZ with
+ | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.zero && Int.eq z Int.zero)
+ | _, _, _ => None
+ end
+ | TCpl => (**r positive *)
+ match rs CN with
+ | Vint n => Some (Int.eq n Int.zero)
+ | _ => None
+ end
+ | TCmi => (**r negative *)
+ match rs CN with
+ | Vint n => Some (Int.eq n Int.one)
+ | _ => None
+ end
+ end.
(** Execution of a single instruction [i] in initial state
[rs] and [m]. Return updated state. For instructions
@@ -441,10 +505,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
Next (nextinstr (rs#r1 <- (Val.and rs#r2 (eval_shift_op so rs)))) m
| Pb lbl =>
goto_label f lbl rs m
- | Pbc bit lbl =>
- match rs#bit with
- | Vint n => if Int.eq n Int.zero then Next (nextinstr rs) m else goto_label f lbl rs m
- | _ => Stuck
+ | Pbc cond lbl =>
+ match eval_testcond cond rs with
+ | Some true => goto_label f lbl rs m
+ | Some false => Next (nextinstr rs) m
+ | None => Stuck
end
| Pbsymb id sg =>
Next (rs#PC <- (symbol_offset id Int.zero)) m
@@ -474,12 +539,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
Next (nextinstr (rs#r1 <- (Val.add (Val.mul rs#r2 rs#r3) rs#r4))) m
| Pmov r1 so =>
Next (nextinstr (rs#r1 <- (eval_shift_op so rs))) m
- | Pmovc bit r1 so =>
- match rs#bit with
- | Vint n => if Int.eq n Int.zero
- then Next (nextinstr rs) m
- else Next (nextinstr (rs#r1 <- (eval_shift_op so rs))) m
- | _ => Next (nextinstr (rs#r1 <- Vundef)) m
+ | Pmovc cond r1 so =>
+ match eval_testcond cond rs with
+ | Some true => Next (nextinstr (rs#r1 <- (eval_shift_op so rs))) m
+ | Some false => Next (nextinstr rs) m
+ | None => Next (nextinstr (rs#r1 <- Vundef)) m
end
| Pmul r1 r2 r3 =>
Next (nextinstr (rs#r1 <- (Val.mul rs#r2 rs#r3))) m
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index d160b2d..6645149 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -189,58 +189,58 @@ Definition transl_cond
Error(msg "Asmgen.transl_cond")
end.
-Definition crbit_for_signed_cmp (cmp: comparison) :=
+Definition cond_for_signed_cmp (cmp: comparison) :=
match cmp with
- | Ceq => CReq
- | Cne => CRne
- | Clt => CRlt
- | Cle => CRle
- | Cgt => CRgt
- | Cge => CRge
+ | Ceq => TCeq
+ | Cne => TCne
+ | Clt => TClt
+ | Cle => TCle
+ | Cgt => TCgt
+ | Cge => TCge
end.
-Definition crbit_for_unsigned_cmp (cmp: comparison) :=
+Definition cond_for_unsigned_cmp (cmp: comparison) :=
match cmp with
- | Ceq => CReq
- | Cne => CRne
- | Clt => CRlo
- | Cle => CRls
- | Cgt => CRhi
- | Cge => CRhs
+ | Ceq => TCeq
+ | Cne => TCne
+ | Clt => TClo
+ | Cle => TCls
+ | Cgt => TChi
+ | Cge => TChs
end.
-Definition crbit_for_float_cmp (cmp: comparison) :=
+Definition cond_for_float_cmp (cmp: comparison) :=
match cmp with
- | Ceq => CReq
- | Cne => CRne
- | Clt => CRmi
- | Cle => CRls
- | Cgt => CRgt
- | Cge => CRge
+ | Ceq => TCeq
+ | Cne => TCne
+ | Clt => TCmi
+ | Cle => TCls
+ | Cgt => TCgt
+ | Cge => TCge
end.
-Definition crbit_for_float_not_cmp (cmp: comparison) :=
+Definition cond_for_float_not_cmp (cmp: comparison) :=
match cmp with
- | Ceq => CRne
- | Cne => CReq
- | Clt => CRpl
- | Cle => CRhi
- | Cgt => CRle
- | Cge => CRlt
+ | Ceq => TCne
+ | Cne => TCeq
+ | Clt => TCpl
+ | Cle => TChi
+ | Cgt => TCle
+ | Cge => TClt
end.
-Definition crbit_for_cond (cond: condition) :=
+Definition cond_for_cond (cond: condition) :=
match cond with
- | Ccomp cmp => crbit_for_signed_cmp cmp
- | Ccompu cmp => crbit_for_unsigned_cmp cmp
- | Ccompshift cmp s => crbit_for_signed_cmp cmp
- | Ccompushift cmp s => crbit_for_unsigned_cmp cmp
- | Ccompimm cmp n => crbit_for_signed_cmp cmp
- | Ccompuimm cmp n => crbit_for_unsigned_cmp cmp
- | Ccompf cmp => crbit_for_float_cmp cmp
- | Cnotcompf cmp => crbit_for_float_not_cmp cmp
- | Ccompfzero cmp => crbit_for_float_cmp cmp
- | Cnotcompfzero cmp => crbit_for_float_not_cmp cmp
+ | Ccomp cmp => cond_for_signed_cmp cmp
+ | Ccompu cmp => cond_for_unsigned_cmp cmp
+ | Ccompshift cmp s => cond_for_signed_cmp cmp
+ | Ccompushift cmp s => cond_for_unsigned_cmp cmp
+ | Ccompimm cmp n => cond_for_signed_cmp cmp
+ | Ccompuimm cmp n => cond_for_unsigned_cmp cmp
+ | Ccompf cmp => cond_for_float_cmp cmp
+ | Cnotcompf cmp => cond_for_float_not_cmp cmp
+ | Ccompfzero cmp => cond_for_float_cmp cmp
+ | Cnotcompfzero cmp => cond_for_float_not_cmp cmp
end.
(** Translation of the arithmetic operation [r <- op(args)].
@@ -360,7 +360,7 @@ Definition transl_op
do r <- ireg_of res; do r1 <- ireg_of a1;
OK (Pcmp r1 (SOimm Int.zero) ::
addimm IR14 r1 (Int.sub (Int.shl Int.one n) Int.one)
- (Pmovc CRge IR14 (SOreg r1) ::
+ (Pmovc TCge IR14 (SOreg r1) ::
Pmov r (SOasrimm IR14 n) :: k))
| Onegf, a1 :: nil =>
do r <- freg_of res; do r1 <- freg_of a1;
@@ -399,7 +399,7 @@ Definition transl_op
do r <- ireg_of res;
transl_cond cmp args
(Pmov r (SOimm Int.zero) ::
- Pmovc (crbit_for_cond cmp) r (SOimm Int.one) ::
+ Pmovc (cond_for_cond cmp) r (SOimm Int.one) ::
k)
| _, _ =>
Error(msg "Asmgen.transl_op")
@@ -599,7 +599,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
| Mgoto lbl =>
OK (Pb lbl :: k)
| Mcond cond args lbl =>
- transl_cond cond args (Pbc (crbit_for_cond cond) lbl :: k)
+ transl_cond cond args (Pbc (cond_for_cond cond) lbl :: k)
| Mjumptable arg tbl =>
do r <- ireg_of arg;
OK (Pbtbl r tbl :: k)
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 2f5f868..d77006a 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -536,39 +536,243 @@ Qed.
Lemma compare_int_spec:
forall rs v1 v2 m,
let rs1 := nextinstr (compare_int rs v1 v2 m) in
- rs1#CReq = (Val.cmpu (Mem.valid_pointer m) Ceq v1 v2)
- /\ rs1#CRne = (Val.cmpu (Mem.valid_pointer m) Cne v1 v2)
- /\ rs1#CRhs = (Val.cmpu (Mem.valid_pointer m) Cge v1 v2)
- /\ rs1#CRlo = (Val.cmpu (Mem.valid_pointer m) Clt v1 v2)
- /\ rs1#CRhi = (Val.cmpu (Mem.valid_pointer m) Cgt v1 v2)
- /\ rs1#CRls = (Val.cmpu (Mem.valid_pointer m) Cle v1 v2)
- /\ rs1#CRge = (Val.cmp Cge v1 v2)
- /\ rs1#CRlt = (Val.cmp Clt v1 v2)
- /\ rs1#CRgt = (Val.cmp Cgt v1 v2)
- /\ rs1#CRle = (Val.cmp Cle v1 v2)
- /\ forall r', data_preg r' = true -> rs1#r' = rs#r'.
+ rs1#CN = Val.negative (Val.sub v1 v2)
+ /\ rs1#CZ = Val.cmpu (Mem.valid_pointer m) Ceq v1 v2
+ /\ rs1#CC = Val.cmpu (Mem.valid_pointer m) Cge v1 v2
+ /\ rs1#CV = Val.sub_overflow v1 v2.
Proof.
- intros. unfold rs1. intuition; try reflexivity.
- unfold compare_int. Simpl.
+ intros. unfold rs1. intuition.
+Qed.
+
+Lemma compare_int_inv:
+ forall rs v1 v2 m,
+ let rs1 := nextinstr (compare_int rs v1 v2 m) in
+ forall r', data_preg r' = true -> rs1#r' = rs#r'.
+Proof.
+ intros. unfold rs1, compare_int.
+ repeat Simplif.
+Qed.
+
+Lemma int_signed_eq:
+ forall x y, Int.eq x y = zeq (Int.signed x) (Int.signed y).
+Proof.
+ intros. unfold Int.eq. unfold proj_sumbool.
+ destruct (zeq (Int.unsigned x) (Int.unsigned y));
+ destruct (zeq (Int.signed x) (Int.signed y)); auto.
+ elim n. unfold Int.signed. rewrite e; auto.
+ elim n. apply Int.eqm_small_eq; auto with ints.
+ eapply Int.eqm_trans. apply Int.eqm_sym. apply Int.eqm_signed_unsigned.
+ rewrite e. apply Int.eqm_signed_unsigned.
+Qed.
+
+Lemma int_not_lt:
+ forall x y, negb (Int.lt y x) = (Int.lt x y || Int.eq x y).
+Proof.
+ intros. unfold Int.lt. rewrite int_signed_eq. unfold proj_sumbool.
+ destruct (zlt (Int.signed y) (Int.signed x)).
+ rewrite zlt_false. rewrite zeq_false. auto. omega. omega.
+ destruct (zeq (Int.signed x) (Int.signed y)).
+ rewrite zlt_false. auto. omega.
+ rewrite zlt_true. auto. omega.
+Qed.
+
+Lemma int_lt_not:
+ forall x y, Int.lt y x = negb (Int.lt x y) && negb (Int.eq x y).
+Proof.
+ intros. rewrite <- negb_orb. rewrite <- int_not_lt. rewrite negb_involutive. auto.
+Qed.
+
+Lemma int_not_ltu:
+ forall x y, negb (Int.ltu y x) = (Int.ltu x y || Int.eq x y).
+Proof.
+ intros. unfold Int.ltu, Int.eq.
+ destruct (zlt (Int.unsigned y) (Int.unsigned x)).
+ rewrite zlt_false. rewrite zeq_false. auto. omega. omega.
+ destruct (zeq (Int.unsigned x) (Int.unsigned y)).
+ rewrite zlt_false. auto. omega.
+ rewrite zlt_true. auto. omega.
+Qed.
+
+Lemma int_ltu_not:
+ forall x y, Int.ltu y x = negb (Int.ltu x y) && negb (Int.eq x y).
+Proof.
+ intros. rewrite <- negb_orb. rewrite <- int_not_ltu. rewrite negb_involutive. auto.
+Qed.
+
+Lemma cond_for_signed_cmp_correct:
+ forall c v1 v2 rs m b,
+ Val.cmp_bool c v1 v2 = Some b ->
+ eval_testcond (cond_for_signed_cmp c)
+ (nextinstr (compare_int rs v1 v2 m)) = Some b.
+Proof.
+ intros. generalize (compare_int_spec rs v1 v2 m).
+ set (rs' := nextinstr (compare_int rs v1 v2 m)).
+ intros [A [B [C D]]].
+ destruct v1; destruct v2; simpl in H; inv H.
+ unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D.
+ simpl. unfold Val.cmp, Val.cmpu.
+ rewrite Int.lt_sub_overflow.
+ destruct c; simpl.
+ destruct (Int.eq i i0); auto.
+ destruct (Int.eq i i0); auto.
+ destruct (Int.lt i i0); auto.
+ rewrite int_not_lt. destruct (Int.lt i i0); simpl; destruct (Int.eq i i0); auto.
+ rewrite (int_lt_not i i0). destruct (Int.lt i i0); destruct (Int.eq i i0); reflexivity.
+ destruct (Int.lt i i0); reflexivity.
+Qed.
+
+Lemma cond_for_unsigned_cmp_correct:
+ forall c v1 v2 rs m b,
+ Val.cmpu_bool (Mem.valid_pointer m) c v1 v2 = Some b ->
+ eval_testcond (cond_for_unsigned_cmp c)
+ (nextinstr (compare_int rs v1 v2 m)) = Some b.
+Proof.
+ intros. generalize (compare_int_spec rs v1 v2 m).
+ set (rs' := nextinstr (compare_int rs v1 v2 m)).
+ intros [A [B [C D]]].
+ unfold eval_testcond. rewrite B; rewrite C. unfold Val.cmpu, Val.cmp.
+ destruct v1; destruct v2; simpl in H; inv H.
+(* int int *)
+ destruct c; simpl; auto.
+ destruct (Int.eq i i0); reflexivity.
+ destruct (Int.eq i i0); auto.
+ destruct (Int.ltu i i0); auto.
+ rewrite (int_not_ltu i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); auto.
+ rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity.
+ destruct (Int.ltu i i0); reflexivity.
+(* int ptr *)
+ destruct (Int.eq i Int.zero) eqn:?; try discriminate.
+ destruct c; simpl in *; inv H1.
+ rewrite Heqb1; reflexivity.
+ rewrite Heqb1; reflexivity.
+(* ptr int *)
+ destruct (Int.eq i0 Int.zero) eqn:?; try discriminate.
+ destruct c; simpl in *; inv H1.
+ rewrite Heqb1; reflexivity.
+ rewrite Heqb1; reflexivity.
+(* ptr ptr *)
+ simpl.
+ fold (Mem.weak_valid_pointer m b0 (Int.unsigned i)) in *.
+ fold (Mem.weak_valid_pointer m b1 (Int.unsigned i0)) in *.
+ destruct (eq_block b0 b1).
+ destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i) &&
+ Mem.weak_valid_pointer m b1 (Int.unsigned i0)); inversion H1.
+ destruct c; simpl; auto.
+ destruct (Int.eq i i0); reflexivity.
+ destruct (Int.eq i i0); auto.
+ destruct (Int.ltu i i0); auto.
+ rewrite (int_not_ltu i i0). destruct (Int.ltu i i0); simpl; destruct (Int.eq i i0); auto.
+ rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity.
+ destruct (Int.ltu i i0); reflexivity.
+ destruct (Mem.valid_pointer m b0 (Int.unsigned i) &&
+ Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate.
+ destruct c; simpl in *; inv H1; reflexivity.
Qed.
Lemma compare_float_spec:
+ forall rs f1 f2,
+ let rs1 := nextinstr (compare_float rs (Vfloat f1) (Vfloat f2)) in
+ rs1#CN = Val.of_bool (Float.cmp Clt f1 f2)
+ /\ rs1#CZ = Val.of_bool (Float.cmp Ceq f1 f2)
+ /\ rs1#CC = Val.of_bool (negb (Float.cmp Clt f1 f2))
+ /\ rs1#CV = Val.of_bool (negb (Float.cmp Ceq f1 f2 || Float.cmp Clt f1 f2 || Float.cmp Cgt f1 f2)).
+Proof.
+ intros. intuition.
+Qed.
+
+Lemma compare_float_inv:
forall rs v1 v2,
- let rs' := nextinstr (compare_float rs v1 v2) in
- rs'#CReq = (Val.cmpf Ceq v1 v2)
- /\ rs'#CRne = (Val.cmpf Cne v1 v2)
- /\ rs'#CRmi = (Val.cmpf Clt v1 v2)
- /\ rs'#CRpl = (Val.notbool (Val.cmpf Clt v1 v2))
- /\ rs'#CRhi = (Val.notbool (Val.cmpf Cle v1 v2))
- /\ rs'#CRls = (Val.cmpf Cle v1 v2)
- /\ rs'#CRge = (Val.cmpf Cge v1 v2)
- /\ rs'#CRlt = (Val.notbool (Val.cmpf Cge v1 v2))
- /\ rs'#CRgt = (Val.cmpf Cgt v1 v2)
- /\ rs'#CRle = (Val.notbool (Val.cmpf Cgt v1 v2))
- /\ forall r', data_preg r' = true -> rs'#r' = rs#r'.
+ let rs1 := nextinstr (compare_float rs v1 v2) in
+ forall r', data_preg r' = true -> rs1#r' = rs#r'.
Proof.
- intros. unfold rs'. intuition; try reflexivity.
- unfold compare_float. Simpl.
+ intros. unfold rs1, compare_float.
+ assert (nextinstr (rs#CN <- Vundef #CZ <- Vundef #CC <- Vundef #CV <- Vundef) r' = rs r').
+ { repeat Simplif. }
+ destruct v1; destruct v2; auto.
+ repeat Simplif.
+Qed.
+
+Lemma compare_float_nextpc:
+ forall rs v1 v2,
+ nextinstr (compare_float rs v1 v2) PC = Val.add (rs PC) Vone.
+Proof.
+ intros. unfold compare_float. destruct v1; destruct v2; reflexivity.
+Qed.
+
+Lemma cond_for_float_cmp_correct:
+ forall c n1 n2 rs,
+ eval_testcond (cond_for_float_cmp c)
+ (nextinstr (compare_float rs (Vfloat n1) (Vfloat n2))) =
+ Some(Float.cmp c n1 n2).
+Proof.
+ intros.
+ generalize (compare_float_spec rs n1 n2).
+ set (rs' := nextinstr (compare_float rs (Vfloat n1) (Vfloat n2))).
+ intros [A [B [C D]]].
+ unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D.
+ destruct c; simpl.
+(* eq *)
+ destruct (Float.cmp Ceq n1 n2); auto.
+(* ne *)
+ rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq n1 n2); auto.
+(* lt *)
+ destruct (Float.cmp Clt n1 n2); auto.
+(* le *)
+ rewrite Float.cmp_le_lt_eq.
+ destruct (Float.cmp Clt n1 n2); destruct (Float.cmp Ceq n1 n2); auto.
+(* gt *)
+ destruct (Float.cmp Ceq n1 n2) eqn:EQ;
+ destruct (Float.cmp Clt n1 n2) eqn:LT;
+ destruct (Float.cmp Cgt n1 n2) eqn:GT; auto.
+ exfalso; eapply Float.cmp_lt_gt_false; eauto.
+ exfalso; eapply Float.cmp_gt_eq_false; eauto.
+ exfalso; eapply Float.cmp_lt_gt_false; eauto.
+(* ge *)
+ rewrite Float.cmp_ge_gt_eq.
+ destruct (Float.cmp Ceq n1 n2) eqn:EQ;
+ destruct (Float.cmp Clt n1 n2) eqn:LT;
+ destruct (Float.cmp Cgt n1 n2) eqn:GT; auto.
+ exfalso; eapply Float.cmp_lt_eq_false; eauto.
+ exfalso; eapply Float.cmp_lt_eq_false; eauto.
+ exfalso; eapply Float.cmp_lt_gt_false; eauto.
+Qed.
+
+Lemma cond_for_float_not_cmp_correct:
+ forall c n1 n2 rs,
+ eval_testcond (cond_for_float_not_cmp c)
+ (nextinstr (compare_float rs (Vfloat n1) (Vfloat n2)))=
+ Some(negb(Float.cmp c n1 n2)).
+Proof.
+ intros.
+ generalize (compare_float_spec rs n1 n2).
+ set (rs' := nextinstr (compare_float rs (Vfloat n1) (Vfloat n2))).
+ intros [A [B [C D]]].
+ unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D.
+ destruct c; simpl.
+(* eq *)
+ destruct (Float.cmp Ceq n1 n2); auto.
+(* ne *)
+ rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq n1 n2); auto.
+(* lt *)
+ destruct (Float.cmp Clt n1 n2); auto.
+(* le *)
+ rewrite Float.cmp_le_lt_eq.
+ destruct (Float.cmp Clt n1 n2) eqn:LT; destruct (Float.cmp Ceq n1 n2) eqn:EQ; auto.
+(* gt *)
+ destruct (Float.cmp Ceq n1 n2) eqn:EQ;
+ destruct (Float.cmp Clt n1 n2) eqn:LT;
+ destruct (Float.cmp Cgt n1 n2) eqn:GT; auto.
+ exfalso; eapply Float.cmp_lt_gt_false; eauto.
+ exfalso; eapply Float.cmp_gt_eq_false; eauto.
+ exfalso; eapply Float.cmp_lt_gt_false; eauto.
+(* ge *)
+ rewrite Float.cmp_ge_gt_eq.
+ destruct (Float.cmp Ceq n1 n2) eqn:EQ;
+ destruct (Float.cmp Clt n1 n2) eqn:LT;
+ destruct (Float.cmp Cgt n1 n2) eqn:GT; auto.
+ exfalso; eapply Float.cmp_lt_eq_false; eauto.
+ exfalso; eapply Float.cmp_lt_eq_false; eauto.
+ exfalso; eapply Float.cmp_lt_gt_false; eauto.
Qed.
Ltac ArgsInv :=
@@ -591,119 +795,92 @@ Lemma transl_cond_correct:
exists rs',
exec_straight ge fn c rs m k rs' m
/\ match eval_condition cond (map rs (map preg_of args)) m with
- | Some b => rs'#(CR (crbit_for_cond cond)) = Val.of_bool b
+ | Some b => eval_testcond (cond_for_cond cond) rs' = Some b
| None => True
end
/\ forall r, data_preg r = true -> rs'#r = rs r.
Proof.
intros until c; intros TR.
- assert (MATCH: forall v ob,
- v = Val.of_optbool ob ->
- match ob with Some b => v = Val.of_bool b | None => True end).
- intros. subst v. destruct ob; auto.
- assert (MATCH2: forall cmp v1 v2 v,
- v = Val.cmpu (Mem.valid_pointer m) cmp v1 v2 ->
- cmp = Ceq \/ cmp = Cne ->
- match Val.cmp_bool cmp v1 v2 with
- | Some b => v = Val.of_bool b
- | None => True
- end).
- intros. destruct v1; simpl; auto; destruct v2; simpl; auto.
- unfold Val.cmpu, Val.cmpu_bool in H. subst v. destruct H0; subst cmp; auto.
-
unfold transl_cond in TR; destruct cond; ArgsInv.
- (* Ccomp *)
- generalize (compare_int_spec rs (rs x) (rs x0) m).
- intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
econstructor.
split. apply exec_straight_one. simpl. eauto. auto.
- split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
- auto.
+ split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) eqn:CMP; auto. apply cond_for_signed_cmp_correct; auto.
+ apply compare_int_inv.
- (* Ccompu *)
- generalize (compare_int_spec rs (rs x) (rs x0) m).
- intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
econstructor.
split. apply exec_straight_one. simpl. eauto. auto.
- split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
- auto.
+ split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:CMP; auto. apply cond_for_unsigned_cmp_correct; auto.
+ apply compare_int_inv.
- (* Ccompshift *)
- generalize (compare_int_spec rs (rs x) (eval_shift s (rs x0)) m).
- intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
econstructor.
split. apply exec_straight_one. simpl. eauto. auto.
- rewrite transl_shift_correct.
- split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
- auto.
+ split. rewrite transl_shift_correct.
+ destruct (Val.cmp_bool c0 (rs x) (eval_shift s (rs x0))) eqn:CMP; auto. apply cond_for_signed_cmp_correct; auto.
+ apply compare_int_inv.
- (* Ccompushift *)
- generalize (compare_int_spec rs (rs x) (eval_shift s (rs x0)) m).
- intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
econstructor.
split. apply exec_straight_one. simpl. eauto. auto.
- rewrite transl_shift_correct.
- split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
- auto.
+ split. rewrite transl_shift_correct.
+ destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (eval_shift s (rs x0))) eqn:CMP; auto. apply cond_for_unsigned_cmp_correct; auto.
+ apply compare_int_inv.
- (* Ccompimm *)
destruct (is_immed_arith i).
- generalize (compare_int_spec rs (rs x) (Vint i) m).
- intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
econstructor.
- split. apply exec_straight_one. simpl. eauto. auto.
- split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
- auto.
+ split. apply exec_straight_one. simpl. eauto. auto.
+ split. destruct (Val.cmp_bool c0 (rs x) (Vint i)) eqn:CMP; auto. apply cond_for_signed_cmp_correct; auto.
+ apply compare_int_inv.
exploit (loadimm_correct IR14). intros [rs' [P [Q R]]].
- generalize (compare_int_spec rs' (rs x) (Vint i) m).
- intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
econstructor.
split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl.
rewrite Q. rewrite R; eauto with asmgen. auto.
- split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
- intros. rewrite C; auto with asmgen.
+ split. rewrite <- R by (eauto with asmgen).
+ destruct (Val.cmp_bool c0 (rs' x) (Vint i)) eqn:CMP; auto. apply cond_for_signed_cmp_correct; auto.
+ intros. rewrite compare_int_inv by auto. auto with asmgen.
- (* Ccompuimm *)
destruct (is_immed_arith i).
- generalize (compare_int_spec rs (rs x) (Vint i) m).
- intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
econstructor.
- split. apply exec_straight_one. simpl. eauto. auto.
- split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
- auto.
+ split. apply exec_straight_one. simpl. eauto. auto.
+ split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (Vint i)) eqn:CMP; auto. apply cond_for_unsigned_cmp_correct; auto.
+ apply compare_int_inv.
exploit (loadimm_correct IR14). intros [rs' [P [Q R]]].
- generalize (compare_int_spec rs' (rs x) (Vint i) m).
- intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
econstructor.
split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl.
rewrite Q. rewrite R; eauto with asmgen. auto.
- split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
- intros. rewrite C; auto with asmgen.
+ split. rewrite <- R by (eauto with asmgen).
+ destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs' x) (Vint i)) eqn:CMP; auto. apply cond_for_unsigned_cmp_correct; auto.
+ intros. rewrite compare_int_inv by auto. auto with asmgen.
- (* Ccompf *)
- generalize (compare_float_spec rs (rs x) (rs x0)).
- intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
econstructor.
- split. apply exec_straight_one. simpl. eauto. auto.
- split. case c0; apply MATCH; assumption.
- auto.
+ split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc.
+ split. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) eqn:CMP; auto.
+ destruct (rs x); try discriminate. destruct (rs x0); try discriminate.
+ simpl in CMP. inv CMP. apply cond_for_float_cmp_correct.
+ apply compare_float_inv.
- (* Cnotcompf *)
- generalize (compare_float_spec rs (rs x) (rs x0)).
- intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
econstructor.
- split. apply exec_straight_one. simpl. eauto. auto.
- split. rewrite <- Val.negate_cmpf_ne in C2. rewrite <- Val.negate_cmpf_eq in C1.
- destruct c0; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto.
- auto.
+ split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc.
+ split. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) eqn:CMP; auto.
+ destruct (rs x); try discriminate. destruct (rs x0); try discriminate.
+ simpl in CMP. inv CMP.
+Local Opaque compare_float. simpl. apply cond_for_float_not_cmp_correct.
+ exact I.
+ apply compare_float_inv.
- (* Ccompfzero *)
- generalize (compare_float_spec rs (rs x) (Vfloat Float.zero)).
- intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
econstructor.
- split. apply exec_straight_one. simpl. eauto. auto.
- split. case c0; apply MATCH; assumption.
- auto.
-- (* Cnotcompf *)
- generalize (compare_float_spec rs (rs x) (Vfloat Float.zero)).
- intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
+ split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc.
+ split. destruct (Val.cmpf_bool c0 (rs x) (Vfloat Float.zero)) eqn:CMP; auto.
+ destruct (rs x); try discriminate.
+ simpl in CMP. inv CMP. apply cond_for_float_cmp_correct.
+ apply compare_float_inv.
+- (* Cnotcompfzero *)
econstructor.
- split. apply exec_straight_one. simpl. eauto. auto.
- split. rewrite <- Val.negate_cmpf_ne in C2. rewrite <- Val.negate_cmpf_eq in C1.
- destruct c0; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto.
- auto.
+ split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc.
+ split. destruct (Val.cmpf_bool c0 (rs x) (Vfloat Float.zero)) eqn:CMP; auto.
+ destruct (rs x); try discriminate. simpl in CMP. inv CMP.
+Local Opaque compare_float. simpl. apply cond_for_float_not_cmp_correct.
+ exact I.
+ apply compare_float_inv.
Qed.
(** Translation of arithmetic operations. *)
@@ -788,8 +965,7 @@ Proof.
set (islt := Int.lt n Int.zero) in *.
set (rs1 := nextinstr (compare_int rs (Vint n) (Vint Int.zero) m)).
assert (OTH1: forall r', data_preg r' = true -> rs1#r' = rs#r').
- generalize (compare_int_spec rs (Vint n) (Vint Int.zero) m).
- fold rs1. intros [A B]. intuition.
+ { apply compare_int_inv; auto. }
exploit (addimm_correct IR14 x0 (Int.sub (Int.shl Int.one i) Int.one)).
intros [rs2 [EXEC2 [RES2 OTH2]]].
set (rs3 := nextinstr (if islt then rs2 else rs2#IR14 <- (Vint n))).
@@ -799,18 +975,19 @@ Proof.
simpl. rewrite ARG1. auto. auto.
eapply exec_straight_trans. eexact EXEC2.
apply exec_straight_two with rs3 m.
- simpl. rewrite OTH2; eauto with asmgen.
- change (rs1 CRge) with (Val.cmp Cge (Vint n) (Vint Int.zero)).
- unfold Val.cmp, Val.cmp_bool. change (Int.cmp Cge n Int.zero) with (negb islt).
- rewrite OTH2; eauto with asmgen. rewrite OTH1. rewrite ARG1.
- unfold rs3. case islt; reflexivity.
- rewrite <- (ireg_of_eq _ _ EQ1). auto with asmgen.
- auto.
- unfold rs3. destruct islt; auto. auto.
- split. unfold rs4; Simpl. unfold rs3. destruct islt.
- Simpl. rewrite RES2. unfold rs1. Simpl.
- Simpl. congruence.
- intros. unfold rs4, rs3; Simpl. destruct islt; Simpl; rewrite OTH2; auto with asmgen.
+ unfold exec_instr.
+ assert (TC: eval_testcond TCge rs2 = Some (negb islt)).
+ { simpl. rewrite ! OTH2 by auto with asmgen. simpl.
+ rewrite Int.lt_sub_overflow. fold islt. destruct islt; auto. }
+ rewrite TC. simpl. rewrite OTH2 by eauto with asmgen. rewrite OTH1. rewrite ARG1.
+ unfold rs3; destruct islt; reflexivity.
+ rewrite <- (ireg_of_eq _ _ EQ1). auto with asmgen.
+ reflexivity.
+ unfold rs3; destruct islt; reflexivity.
+ reflexivity.
+ split. unfold rs4; Simpl. unfold rs3. destruct islt.
+ Simpl. rewrite RES2. unfold rs1. Simpl. Simpl. congruence.
+ intros. unfold rs4, rs3; Simpl. destruct islt; Simpl; rewrite OTH2; auto with asmgen.
(* intoffloat *)
econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
Transparent destroyed_by_op.
@@ -848,25 +1025,22 @@ Proof.
rewrite (ireg_of_eq _ _ EQ).
exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]].
set (rs2 := nextinstr (rs1#x <- (Vint Int.zero))).
- set (rs3 := nextinstr (match rs2#(crbit_for_cond cmp) with
- | Vint n => if Int.eq n Int.zero then rs2 else rs2#x <- Vone
- | _ => rs2#x <- Vundef
- end)).
+ set (rs3 := nextinstr (match eval_testcond (cond_for_cond cmp) rs2 with
+ | Some true => rs2 # x <- (Vint Int.one)
+ | Some false => rs2
+ | None => rs2 # x <- Vundef end)).
exists rs3; split.
eapply exec_straight_trans. eexact A. apply exec_straight_two with rs2 m.
auto.
- simpl. unfold rs3. destruct (rs2 (crbit_for_cond cmp)); auto. destruct (Int.eq i Int.zero); auto.
- auto. unfold rs3. destruct (rs2 (crbit_for_cond cmp)); auto. destruct (Int.eq i Int.zero); auto.
- split. unfold rs3. Simpl.
- replace (rs2 (crbit_for_cond cmp)) with (rs1 (crbit_for_cond cmp)).
- destruct (eval_condition cmp rs##(preg_of##args) m) as [[]|]; simpl in *.
- rewrite B. simpl. rewrite Int.eq_false. Simpl. apply Int.one_not_zero.
- rewrite B. simpl. rewrite Int.eq_true. unfold rs2. Simpl.
- auto.
- destruct cmp; reflexivity.
+ simpl. unfold rs3. destruct (eval_testcond (cond_for_cond cmp) rs2) as [[]|]; auto.
+ auto. unfold rs3. destruct (eval_testcond (cond_for_cond cmp) rs2) as [[]|]; auto.
+ split. destruct (eval_condition cmp rs ## (preg_of ## args) m) as [b|]; simpl; auto.
+ unfold rs3.
+ change (eval_testcond (cond_for_cond cmp) rs2) with (eval_testcond (cond_for_cond cmp) rs1). rewrite B.
+ Simpl. destruct b. Simpl. unfold rs2. Simpl.
intros. transitivity (rs2 r).
- unfold rs3. destruct (rs2 (crbit_for_cond cmp)); Simpl. destruct (Int.eq i Int.zero); auto; Simpl.
- unfold rs2. Simpl.
+ unfold rs3. Simpl. destruct (eval_testcond (cond_for_cond cmp) rs2) as [[]|]; Simpl; auto.
+ unfold rs2. Simpl.
Qed.
(** Translation of loads and stores. *)
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 3740c1f..d700326 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -93,18 +93,18 @@ let preg oc = function
| _ -> assert false
let condition_name = function
- | CReq -> "eq"
- | CRne -> "ne"
- | CRhs -> "hs"
- | CRlo -> "lo"
- | CRmi -> "mi"
- | CRpl -> "pl"
- | CRhi -> "hi"
- | CRls -> "ls"
- | CRge -> "ge"
- | CRlt -> "lt"
- | CRgt -> "gt"
- | CRle -> "le"
+ | TCeq -> "eq"
+ | TCne -> "ne"
+ | TChs -> "hs"
+ | TClo -> "lo"
+ | TCmi -> "mi"
+ | TCpl -> "pl"
+ | TChi -> "hi"
+ | TCls -> "ls"
+ | TCge -> "ge"
+ | TClt -> "lt"
+ | TCgt -> "gt"
+ | TCle -> "le"
(* Names of sections *)
@@ -744,12 +744,6 @@ let rec print_instructions oc instrs =
end;
print_instructions oc il
-(* Base-2 log of a Caml integer *)
-
-let rec log2 n =
- assert (n > 0);
- if n = 1 then 0 else 1 + log2 (n lsr 1)
-
let print_function oc name fn =
Hashtbl.clear current_function_labels;
reset_constants();
@@ -760,8 +754,8 @@ let print_function oc name fn =
| _ -> Section_text in
section oc text;
let alignment =
- match !Clflags.option_falignfunctions with Some n -> log2 n | None -> 2 in
- fprintf oc " .align %d\n" alignment;
+ match !Clflags.option_falignfunctions with Some n -> n | None -> 4 in
+ fprintf oc " .balign %d\n" alignment;
if not (C2C.atom_is_static name) then
fprintf oc " .global %a\n" print_symb name;
fprintf oc "%a:\n" print_symb name;
@@ -815,11 +809,11 @@ let print_var oc name v =
| _ -> Section_data true
and align =
match C2C.atom_alignof name with
- | Some a -> log2 a
- | None -> 3 (* 8-alignment is a safe default *)
+ | Some a -> a
+ | None -> 8 (* 8-alignment is a safe default *)
in
section oc sec;
- fprintf oc " .align %d\n" align;
+ fprintf oc " .balign %d\n" align;
if not (C2C.atom_is_static name) then
fprintf oc " .global %a\n" print_symb name;
fprintf oc "%a:\n" print_symb name;
diff --git a/common/Values.v b/common/Values.v
index b937071..05749b7 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -262,6 +262,18 @@ Definition add_carry (v1 v2 cin: val): val :=
| _, _, _ => Vundef
end.
+Definition sub_overflow (v1 v2: val) : val :=
+ match v1, v2 with
+ | Vint n1, Vint n2 => Vint(Int.sub_overflow n1 n2 Int.zero)
+ | _, _ => Vundef
+ end.
+
+Definition negative (v: val) : val :=
+ match v with
+ | Vint n => Vint (Int.negative n)
+ | _ => Vundef
+ end.
+
Definition and (v1 v2: val): val :=
match v1, v2 with
| Vint n1, Vint n2 => Vint(Int.and n1 n2)
diff --git a/ia32/Asm.v b/ia32/Asm.v
index 24dedc7..d86ff19 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -48,11 +48,10 @@ Proof. decide equality. Defined.
Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}.
Proof. decide equality. Defined.
-(** Bits of the flags register. [SOF] is a pseudo-bit representing
- the "xor" of the [OF] and [SF] bits. *)
+(** Bits of the flags register. *)
Inductive crbit: Type :=
- | ZF | CF | PF | SOF.
+ | ZF | CF | PF | SF | OF.
(** All registers modeled here. *)
@@ -304,22 +303,23 @@ Definition eval_addrmode (a: addrmode) (rs: regset) : val :=
(** Integer comparison between x and y:
- ZF = 1 if x = y, 0 if x != y
- CF = 1 if x <u y, 0 if x >=u y
-- SOF = 1 if x <s y, 0 if x >=s y
+- SF = 1 if x - y is negative, 0 if x - y is positive
+- OF = 1 if x - y overflows (signed), 0 if not
- PF is undefined
-
-SOF is (morally) the XOR of the SF and OF flags of the processor. *)
+*)
Definition compare_ints (x y: val) (rs: regset) (m: mem): regset :=
rs #ZF <- (Val.cmpu (Mem.valid_pointer m) Ceq x y)
#CF <- (Val.cmpu (Mem.valid_pointer m) Clt x y)
- #SOF <- (Val.cmp Clt x y)
+ #SF <- (Val.negative (Val.sub x y))
+ #OF <- (Val.sub_overflow x y)
#PF <- Vundef.
(** Floating-point comparison between x and y:
- ZF = 1 if x=y or unordered, 0 if x<>y
- CF = 1 if x<y or unordered, 0 if x>=y
- PF = 1 if unordered, 0 if ordered.
-- SOF is undefined
+- SF and 0F are undefined
*)
Definition compare_floats (vx vy: val) (rs: regset) : regset :=
@@ -328,9 +328,10 @@ Definition compare_floats (vx vy: val) (rs: regset) : regset :=
rs #ZF <- (Val.of_bool (negb (Float.cmp Cne x y)))
#CF <- (Val.of_bool (negb (Float.cmp Cge x y)))
#PF <- (Val.of_bool (negb (Float.cmp Ceq x y || Float.cmp Clt x y || Float.cmp Cgt x y)))
- #SOF <- Vundef
+ #SF <- Vundef
+ #OF <- Vundef
| _, _ =>
- undef_regs (CR ZF :: CR CF :: CR PF :: CR SOF :: nil) rs
+ undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs
end.
(** Testing a condition *)
@@ -368,24 +369,24 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
| _, _ => None
end
| Cond_l =>
- match rs SOF with
- | Vint n => Some (Int.eq n Int.one)
- | _ => None
+ match rs OF, rs SF with
+ | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.one)
+ | _, _ => None
end
| Cond_le =>
- match rs SOF, rs ZF with
- | Vint s, Vint z => Some (Int.eq s Int.one || Int.eq z Int.one)
- | _, _ => None
+ match rs OF, rs SF, rs ZF with
+ | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.one || Int.eq z Int.one)
+ | _, _, _ => None
end
| Cond_ge =>
- match rs SOF with
- | Vint n => Some (Int.eq n Int.zero)
- | _ => None
+ match rs OF, rs SF with
+ | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.zero)
+ | _, _ => None
end
| Cond_g =>
- match rs SOF, rs ZF with
- | Vint s, Vint z => Some (Int.eq s Int.zero && Int.eq z Int.zero)
- | _, _ => None
+ match rs OF, rs SF, rs ZF with
+ | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.zero && Int.eq z Int.zero)
+ | _, _, _ => None
end
| Cond_p =>
match rs PF with
@@ -418,7 +419,7 @@ Definition nextinstr (rs: regset) :=
rs#PC <- (Val.add rs#PC Vone).
Definition nextinstr_nf (rs: regset) : regset :=
- nextinstr (undef_regs (CR ZF :: CR CF :: CR PF :: CR SOF :: nil) rs).
+ nextinstr (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs).
Definition goto_label (c: code) (lbl: label) (rs: regset) (m: mem) :=
match label_pos lbl 0 c with
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 0bf030c..728617e 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -41,39 +41,6 @@ Proof.
intro. simpl. ElimOrEq; auto.
Qed.
-(*
-Lemma agree_undef_move:
- forall ms sp rs rs',
- agree ms sp rs ->
- (forall r, data_preg r = true -> r <> ST0 -> rs'#r = rs#r) ->
- agree (undef_move ms) sp rs'.
-Proof.
- intros. destruct H. split.
- rewrite H0; auto. congruence. auto.
- intros. unfold undef_move.
- destruct (In_dec mreg_eq r destroyed_at_move_regs).
- rewrite Mach.undef_regs_same; auto.
- rewrite Mach.undef_regs_other; auto.
- assert (data_preg (preg_of r) = true /\ preg_of r <> ST0).
- simpl in n. destruct r; simpl; auto; intuition congruence.
- destruct H. rewrite H0; auto.
-Qed.
-
-Lemma agree_set_undef_move_mreg:
- forall ms sp rs r v rs',
- agree ms sp rs ->
- Val.lessdef v (rs'#(preg_of r)) ->
- (forall r', data_preg r' = true /\ r' <> ST0 -> r' <> preg_of r -> rs'#r' = rs#r') ->
- agree (Regmap.set r v (undef_move ms)) sp rs'.
-Proof.
- intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))); auto.
- eapply agree_undef_move; eauto.
- intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of r)).
- congruence. auto.
- intros. rewrite Pregmap.gso; auto.
-Qed.
-*)
-
(** Useful properties of the PC register. *)
Lemma nextinstr_nf_inv:
@@ -82,10 +49,7 @@ Lemma nextinstr_nf_inv:
(nextinstr_nf rs)#r = rs#r.
Proof.
intros. unfold nextinstr_nf. rewrite nextinstr_inv.
- simpl. repeat rewrite Pregmap.gso; auto.
- red; intro; subst; contradiction.
- red; intro; subst; contradiction.
- red; intro; subst; contradiction.
+ simpl. repeat rewrite Pregmap.gso; auto;
red; intro; subst; contradiction.
red; intro; subst; contradiction.
Qed.
@@ -214,10 +178,8 @@ Proof.
apply exec_straight_step with rs3 m. simpl.
change (rs2 EAX) with (rs1 EAX). rewrite A. simpl.
rewrite (Int.add_commut Int.zero tnm1). rewrite Int.add_zero. auto. auto.
- apply exec_straight_step with rs4 m. simpl.
- change (rs3 SOF) with (rs2 SOF). unfold rs2. rewrite nextinstr_inv; auto with asmgen.
- unfold compare_ints. rewrite Pregmap.gso; auto with asmgen. rewrite Pregmap.gss.
- unfold Val.cmp. simpl. unfold rs4. destruct (Int.lt x Int.zero); simpl; auto.
+ apply exec_straight_step with rs4 m. simpl.
+ rewrite Int.lt_sub_overflow. unfold rs4. destruct (Int.lt x Int.zero); simpl; auto.
unfold rs4. destruct (Int.lt x Int.zero); simpl; auto.
apply exec_straight_one. auto. auto.
split. unfold rs5. Simplifs. unfold rs4. rewrite nextinstr_inv; auto with asmgen.
@@ -441,13 +403,15 @@ Lemma compare_ints_spec:
let rs' := nextinstr (compare_ints v1 v2 rs m) in
rs'#ZF = Val.cmpu (Mem.valid_pointer m) Ceq v1 v2
/\ rs'#CF = Val.cmpu (Mem.valid_pointer m) Clt v1 v2
- /\ rs'#SOF = Val.cmp Clt v1 v2
+ /\ rs'#SF = Val.negative (Val.sub v1 v2)
+ /\ rs'#OF = Val.sub_overflow v1 v2
/\ (forall r, data_preg r = true -> rs'#r = rs#r).
Proof.
intros. unfold rs'; unfold compare_ints.
split. auto.
split. auto.
split. auto.
+ split. auto.
intros. Simplifs.
Qed.
@@ -505,9 +469,11 @@ Lemma testcond_for_signed_comparison_correct:
Proof.
intros. generalize (compare_ints_spec rs v1 v2 m).
set (rs' := nextinstr (compare_ints v1 v2 rs m)).
- intros [A [B [C D]]].
+ intros [A [B [C [D E]]]].
destruct v1; destruct v2; simpl in H; inv H.
- unfold eval_testcond. rewrite A; rewrite B; rewrite C. unfold Val.cmp, Val.cmpu.
+ unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D.
+ simpl. unfold Val.cmp, Val.cmpu.
+ rewrite Int.lt_sub_overflow.
destruct c; simpl.
destruct (Int.eq i i0); auto.
destruct (Int.eq i i0); auto.
@@ -525,8 +491,8 @@ Lemma testcond_for_unsigned_comparison_correct:
Proof.
intros. generalize (compare_ints_spec rs v1 v2 m).
set (rs' := nextinstr (compare_ints v1 v2 rs m)).
- intros [A [B [C D]]].
- unfold eval_testcond. rewrite A; rewrite B; rewrite C. unfold Val.cmpu, Val.cmp.
+ intros [A [B [C [D E]]]].
+ unfold eval_testcond. rewrite A; rewrite B. unfold Val.cmpu, Val.cmp.
destruct v1; destruct v2; simpl in H; inv H.
(* int int *)
destruct c; simpl; auto.
@@ -706,11 +672,11 @@ Qed.
Remark compare_floats_inv:
forall vx vy rs r,
- r <> CR ZF -> r <> CR CF -> r <> CR PF -> r <> CR SOF ->
+ r <> CR ZF -> r <> CR CF -> r <> CR PF -> r <> CR SF -> r <> CR OF ->
compare_floats vx vy rs r = rs r.
Proof.
intros.
- assert (DFL: undef_regs (CR ZF :: CR CF :: CR PF :: CR SOF :: nil) rs r = rs r).
+ assert (DFL: undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs r = rs r).
simpl. Simplifs.
unfold compare_floats; destruct vx; destruct vy; auto. Simplifs.
Qed.
diff --git a/lib/Floats.v b/lib/Floats.v
index 7ae1705..94c19d2 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -453,6 +453,12 @@ Proof.
now apply cmp_le_lt_eq.
Qed.
+Theorem cmp_lt_gt_false:
+ forall f1 f2, cmp Clt f1 f2 = true -> cmp Cgt f1 f2 = true -> False.
+Proof.
+ unfold cmp; intros; destruct (order_float f1 f2) as [ [] | ]; discriminate.
+Qed.
+
(** Properties of conversions to/from in-memory representation.
The double-precision conversions are bijective (one-to-one).
The single-precision conversions lose precision exactly
diff --git a/lib/Integers.v b/lib/Integers.v
index 5eb4c82..49fa48f 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -257,11 +257,6 @@ Definition divu (x y: int) : int :=
Definition modu (x y: int) : int :=
repr ((unsigned x) mod (unsigned y)).
-Definition add_carry (x y cin: int): int :=
- if zlt (unsigned x + unsigned y + unsigned cin) modulus
- then zero
- else one.
-
(** Bitwise boolean operations. *)
Definition and (x y: int): int := repr (Z.land (unsigned x) (unsigned y)).
@@ -291,10 +286,30 @@ Definition rolm (x a m: int): int := and (rol x a) m.
Definition shrx (x y: int): int :=
divs x (shl one y).
+(** Condition flags *)
+
+Definition negative (x: int): int :=
+ if lt x zero then one else zero.
+
+Definition add_carry (x y cin: int): int :=
+ if zlt (unsigned x + unsigned y + unsigned cin) modulus then zero else one.
+
+Definition add_overflow (x y cin: int): int :=
+ let s := signed x + signed y + signed cin in
+ if zle min_signed s && zle s max_signed then zero else one.
+
+Definition sub_borrow (x y bin: int): int :=
+ if zlt (unsigned x - unsigned y - unsigned bin) 0 then one else zero.
+
+Definition sub_overflow (x y bin: int): int :=
+ let s := signed x - signed y - signed bin in
+ if zle min_signed s && zle s max_signed then zero else one.
+
(** [shr_carry x y] is 1 if [x] is negative and at least one 1 bit is shifted away. *)
-Definition shr_carry (x y: int) :=
- if lt x zero && negb (eq (and x (sub (shl one y) one)) zero) then one else zero.
+Definition shr_carry (x y: int) : int :=
+ if lt x zero && negb (eq (and x (sub (shl one y) one)) zero)
+ then one else zero.
(** Zero and sign extensions *)
@@ -882,7 +897,7 @@ Proof.
unfold add, add_carry. rewrite unsigned_zero. rewrite Zplus_0_r.
rewrite unsigned_repr_eq.
generalize (unsigned_range x) (unsigned_range y). intros.
- destruct (zlt (unsigned x + unsigned y) modulus).
+ destruct (zlt (unsigned x + unsigned y) modulus).
rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega.
rewrite unsigned_one. apply Zmod_unique with 1. omega. omega.
Qed.
@@ -983,6 +998,21 @@ Proof.
apply eqm_sub; apply eqm_sym; apply eqm_signed_unsigned.
Qed.
+Theorem unsigned_sub_borrow:
+ forall x y,
+ unsigned (sub x y) = unsigned x - unsigned y + unsigned (sub_borrow x y zero) * modulus.
+Proof.
+ intros.
+ unfold sub, sub_borrow. rewrite unsigned_zero. rewrite Zminus_0_r.
+ rewrite unsigned_repr_eq.
+ generalize (unsigned_range x) (unsigned_range y). intros.
+ destruct (zlt (unsigned x - unsigned y) 0).
+ rewrite unsigned_one. apply Zmod_unique with (-1). omega. omega.
+ rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega.
+Qed.
+
+
+
(** ** Properties of multiplication *)
Theorem mul_commut: forall x y, mul x y = mul y x.
@@ -1783,6 +1813,16 @@ Proof.
bit_solve. destruct (testbit x i); auto.
Qed.
+Lemma unsigned_not:
+ forall x, unsigned (not x) = max_unsigned - unsigned x.
+Proof.
+ intros. transitivity (unsigned (repr(-unsigned x - 1))).
+ f_equal. bit_solve. rewrite testbit_repr; auto. symmetry. apply Z_one_complement. omega.
+ rewrite unsigned_repr_eq. apply Zmod_unique with (-1).
+ unfold max_unsigned. omega.
+ generalize (unsigned_range x). unfold max_unsigned. omega.
+Qed.
+
Theorem not_neg:
forall x, not x = add (neg x) mone.
Proof.
@@ -1807,6 +1847,23 @@ Proof.
exists (-1). ring.
Qed.
+Theorem sub_borrow_add_carry:
+ forall x y b,
+ b = zero \/ b = one ->
+ sub_borrow x y b = xor (add_carry x (not y) (xor b one)) one.
+Proof.
+ intros. unfold sub_borrow, add_carry. rewrite unsigned_not.
+ replace (unsigned (xor b one)) with (1 - unsigned b).
+ destruct (zlt (unsigned x - unsigned y - unsigned b)).
+ rewrite zlt_true. rewrite xor_zero_l; auto.
+ unfold max_unsigned; omega.
+ rewrite zlt_false. rewrite xor_idem; auto.
+ unfold max_unsigned; omega.
+ destruct H; subst b.
+ rewrite xor_zero_l. rewrite unsigned_one, unsigned_zero; auto.
+ rewrite xor_idem. rewrite unsigned_one, unsigned_zero; auto.
+Qed.
+
(** Connections between [add] and bitwise logical operations. *)
Lemma Z_add_is_or:
@@ -3382,6 +3439,23 @@ Proof.
generalize wordsize_max_unsigned; omega.
Qed.
+Theorem shr_lt_zero:
+ forall x,
+ shr x (repr (zwordsize - 1)) = if lt x zero then mone else zero.
+Proof.
+ intros. apply same_bits_eq; intros.
+ rewrite bits_shr; auto.
+ rewrite unsigned_repr.
+ transitivity (testbit x (zwordsize - 1)).
+ f_equal. destruct (zlt (i + (zwordsize - 1)) zwordsize); omega.
+ rewrite sign_bit_of_unsigned.
+ unfold lt. rewrite signed_zero. unfold signed.
+ destruct (zlt (unsigned x) half_modulus).
+ rewrite zlt_false. rewrite bits_zero; auto. generalize (unsigned_range x); omega.
+ rewrite zlt_true. rewrite bits_mone; auto. generalize (unsigned_range x); omega.
+ generalize wordsize_max_unsigned; omega.
+Qed.
+
Theorem ltu_range_test:
forall x y,
ltu x y = true -> unsigned y <= max_signed ->
@@ -3393,6 +3467,43 @@ Proof.
generalize (unsigned_range x). omega. omega.
Qed.
+Theorem lt_sub_overflow:
+ forall x y,
+ xor (sub_overflow x y zero) (negative (sub x y)) = if lt x y then one else zero.
+Proof.
+ intros. unfold negative, sub_overflow, lt. rewrite sub_signed.
+ rewrite signed_zero. rewrite Zminus_0_r.
+ generalize (signed_range x) (signed_range y).
+ set (X := signed x); set (Y := signed y). intros RX RY.
+ unfold min_signed, max_signed in *.
+ generalize half_modulus_pos half_modulus_modulus; intros HM MM.
+ destruct (zle 0 (X - Y)).
+- unfold proj_sumbool at 1; rewrite zle_true at 1 by omega. simpl.
+ rewrite (zlt_false _ X) by omega.
+ destruct (zlt (X - Y) half_modulus).
+ + unfold proj_sumbool; rewrite zle_true by omega.
+ rewrite signed_repr. rewrite zlt_false by omega. apply xor_idem.
+ unfold min_signed, max_signed; omega.
+ + unfold proj_sumbool; rewrite zle_false by omega.
+ replace (signed (repr (X - Y))) with (X - Y - modulus).
+ rewrite zlt_true by omega. apply xor_idem.
+ rewrite signed_repr_eq. replace ((X - Y) mod modulus) with (X - Y).
+ rewrite zlt_false; auto.
+ symmetry. apply Zmod_unique with 0; omega.
+- unfold proj_sumbool at 2. rewrite zle_true at 1 by omega. rewrite andb_true_r.
+ rewrite (zlt_true _ X) by omega.
+ destruct (zlt (X - Y) (-half_modulus)).
+ + unfold proj_sumbool; rewrite zle_false by omega.
+ replace (signed (repr (X - Y))) with (X - Y + modulus).
+ rewrite zlt_false by omega. apply xor_zero.
+ rewrite signed_repr_eq. replace ((X - Y) mod modulus) with (X - Y + modulus).
+ rewrite zlt_true by omega; auto.
+ symmetry. apply Zmod_unique with (-1); omega.
+ + unfold proj_sumbool; rewrite zle_true by omega.
+ rewrite signed_repr. rewrite zlt_true by omega. apply xor_zero_l.
+ unfold min_signed, max_signed; omega.
+Qed.
+
(** Non-overlapping test *)
Definition no_overlap (ofs1: int) (sz1: Z) (ofs2: int) (sz2: Z) : bool :=