aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/ConstpropOp.vp24
-rw-r--r--arm/ConstpropOpproof.v40
-rw-r--r--powerpc/ConstpropOp.vp16
-rw-r--r--powerpc/ConstpropOpproof.v45
-rw-r--r--riscV/ConstpropOp.vp24
-rw-r--r--riscV/ConstpropOpproof.v40
-rw-r--r--x86/ConstpropOp.vp24
-rw-r--r--x86/ConstpropOpproof.v40
8 files changed, 202 insertions, 51 deletions
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index bd08d597..d62240ef 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -105,16 +105,28 @@ Nondetfunction cond_strength_reduction
Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) :=
let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args').
+Definition make_cmp_imm_eq (c: condition) (args: list reg) (vl: list aval)
+ (n: int) (r1: reg) (v1: aval) :=
+ if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
+ else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
+ else make_cmp_base c args vl.
+
+Definition make_cmp_imm_ne (c: condition) (args: list reg) (vl: list aval)
+ (n: int) (r1: reg) (v1: aval) :=
+ if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
+ else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
+ else make_cmp_base c args vl.
+
Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) :=
match c, args, vl with
| Ccompimm Ceq n, r1 :: nil, v1 :: nil =>
- if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
- else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
- else make_cmp_base c args vl
+ make_cmp_imm_eq c args vl n r1 v1
| Ccompimm Cne n, r1 :: nil, v1 :: nil =>
- if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
- else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
- else make_cmp_base c args vl
+ make_cmp_imm_ne c args vl n r1 v1
+ | Ccompuimm Ceq n, r1 :: nil, v1 :: nil =>
+ make_cmp_imm_eq c args vl n r1 v1
+ | Ccompuimm Cne n, r1 :: nil, v1 :: nil =>
+ make_cmp_imm_ne c args vl n r1 v1
| _, _, _ =>
make_cmp_base c args vl
end.
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 1eec5923..079ba2be 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -191,24 +191,46 @@ Proof.
rs#r = Vundef \/ rs#r = Vint Int.zero \/ rs#r = Vint Int.one).
{ intros. apply vmatch_Uns_1 with bc Ptop. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. }
unfold make_cmp. case (make_cmp_match c args vl); intros.
-- destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
- simpl in H; inv H. InvBooleans. subst n.
+- unfold make_cmp_imm_eq.
+ destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
++ simpl in H; inv H. InvBooleans. subst n.
exists (rs#r1); split; auto. simpl.
exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
- simpl in H; inv H. InvBooleans. subst n.
++ destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
+* simpl in H; inv H. InvBooleans. subst n.
exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
- apply make_cmp_base_correct; auto.
-- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
- simpl in H; inv H. InvBooleans. subst n.
+* apply make_cmp_base_correct; auto.
+- unfold make_cmp_imm_ne.
+ destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
++ simpl in H; inv H. InvBooleans. subst n.
exists (rs#r1); split; auto. simpl.
exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
++ destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
+* simpl in H; inv H. InvBooleans. subst n.
+ exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+* apply make_cmp_base_correct; auto.
+- unfold make_cmp_imm_eq.
destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
- simpl in H; inv H. InvBooleans. subst n.
++ simpl in H; inv H. InvBooleans. subst n.
+ exists (rs#r1); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
++ destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
+* simpl in H; inv H. InvBooleans. subst n.
+ exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+* apply make_cmp_base_correct; auto.
+- unfold make_cmp_imm_ne.
+ destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
++ simpl in H; inv H. InvBooleans. subst n.
+ exists (rs#r1); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
++ destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
+* simpl in H; inv H. InvBooleans. subst n.
exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
- apply make_cmp_base_correct; auto.
+* apply make_cmp_base_correct; auto.
- apply make_cmp_base_correct; auto.
Qed.
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index f18a72e9..2d492b66 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -65,6 +65,12 @@ Nondetfunction cond_strength_reduction
Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) :=
let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args').
+Definition is_an_integer (v: aval) : bool :=
+ match v with
+ | Vbot | I _ | Uns _ _ | Sgn _ _ => true
+ | _ => false
+ end.
+
Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) :=
match c, args, vl with
| Ccompimm Ceq n, r1 :: nil, v1 :: nil =>
@@ -75,6 +81,16 @@ Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) :=
if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
else make_cmp_base c args vl
+ | Ccompuimm Ceq n, r1 :: nil, v1 :: nil =>
+ if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
+ else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
+ else if is_an_integer v1 then make_cmp_base (Ccompimm Ceq n) args vl
+ else make_cmp_base c args vl
+ | Ccompuimm Cne n, r1 :: nil, v1 :: nil =>
+ if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
+ else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
+ else if is_an_integer v1 then make_cmp_base (Ccompimm Cne n) args vl
+ else make_cmp_base c args vl
| _, _, _ =>
make_cmp_base c args vl
end.
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 7fddd053..fe061e5b 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -156,25 +156,58 @@ Proof.
assert (Y: forall r, vincl (AE.get r ae) (Uns Ptop 1) = true ->
rs#r = Vundef \/ rs#r = Vint Int.zero \/ rs#r = Vint Int.one).
{ intros. apply vmatch_Uns_1 with bc Ptop. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. }
+ assert (Z: forall r, is_an_integer (AE.get r ae) = true ->
+ match rs#r with Vptr _ _ => False | _ => True end).
+ { intros. generalize (MATCH r); intro V. revert H. inv V; auto; discriminate. }
unfold make_cmp. case (make_cmp_match c args vl); intros.
- destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
- simpl in H; inv H. InvBooleans. subst n.
++ simpl in H; inv H. InvBooleans. subst n.
exists (rs#r1); split; auto. simpl.
exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
- simpl in H; inv H. InvBooleans. subst n.
++ destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
+* simpl in H; inv H. InvBooleans. subst n.
exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+* apply make_cmp_base_correct; auto.
+- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
++ simpl in H; inv H. InvBooleans. subst n.
+ exists (rs#r1); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
++ destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
+* simpl in H; inv H. InvBooleans. subst n.
+ exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+* apply make_cmp_base_correct; auto.
+- destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
++ simpl in H; inv H. InvBooleans. subst n.
+ exists (rs#r1); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
++ destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
+* simpl in H; inv H. InvBooleans. subst n.
+ exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+* destruct (is_an_integer v1) eqn:E.
+** simpl in H; inv H.
+ replace (eval_condition (Ccompuimm Ceq n) rs##(r1::nil) m)
+ with (eval_condition (Ccompimm Ceq n) rs##(r1::nil) m).
apply make_cmp_base_correct; auto.
+ simpl. apply Z in E. destruct (rs#r1); auto; contradiction.
+** apply make_cmp_base_correct; auto.
- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
- simpl in H; inv H. InvBooleans. subst n.
++ simpl in H; inv H. InvBooleans. subst n.
exists (rs#r1); split; auto. simpl.
exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
- destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
- simpl in H; inv H. InvBooleans. subst n.
++ destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
+* simpl in H; inv H. InvBooleans. subst n.
exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+* destruct (is_an_integer v1) eqn:E.
+** simpl in H; inv H.
+ replace (eval_condition (Ccompuimm Cne n) rs##(r1::nil) m)
+ with (eval_condition (Ccompimm Cne n) rs##(r1::nil) m).
apply make_cmp_base_correct; auto.
+ simpl. apply Z in E. destruct (rs#r1); auto; contradiction.
+** apply make_cmp_base_correct; auto.
- apply make_cmp_base_correct; auto.
Qed.
diff --git a/riscV/ConstpropOp.vp b/riscV/ConstpropOp.vp
index 76a1e8f8..aab2424d 100644
--- a/riscV/ConstpropOp.vp
+++ b/riscV/ConstpropOp.vp
@@ -65,16 +65,28 @@ Nondetfunction cond_strength_reduction
Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) :=
let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args').
+Definition make_cmp_imm_eq (c: condition) (args: list reg) (vl: list aval)
+ (n: int) (r1: reg) (v1: aval) :=
+ if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
+ else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
+ else make_cmp_base c args vl.
+
+Definition make_cmp_imm_ne (c: condition) (args: list reg) (vl: list aval)
+ (n: int) (r1: reg) (v1: aval) :=
+ if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
+ else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
+ else make_cmp_base c args vl.
+
Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) :=
match c, args, vl with
| Ccompimm Ceq n, r1 :: nil, v1 :: nil =>
- if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
- else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
- else make_cmp_base c args vl
+ make_cmp_imm_eq c args vl n r1 v1
| Ccompimm Cne n, r1 :: nil, v1 :: nil =>
- if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
- else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
- else make_cmp_base c args vl
+ make_cmp_imm_ne c args vl n r1 v1
+ | Ccompuimm Ceq n, r1 :: nil, v1 :: nil =>
+ make_cmp_imm_eq c args vl n r1 v1
+ | Ccompuimm Cne n, r1 :: nil, v1 :: nil =>
+ make_cmp_imm_ne c args vl n r1 v1
| _, _, _ =>
make_cmp_base c args vl
end.
diff --git a/riscV/ConstpropOpproof.v b/riscV/ConstpropOpproof.v
index b7452fd4..765aa035 100644
--- a/riscV/ConstpropOpproof.v
+++ b/riscV/ConstpropOpproof.v
@@ -149,24 +149,46 @@ Proof.
e#r = Vundef \/ e#r = Vint Int.zero \/ e#r = Vint Int.one).
{ intros. apply vmatch_Uns_1 with bc Ptop. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. }
unfold make_cmp. case (make_cmp_match c args vl); intros.
-- destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
- simpl in H; inv H. InvBooleans. subst n.
+- unfold make_cmp_imm_eq.
+ destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
++ simpl in H; inv H. InvBooleans. subst n.
exists (e#r1); split; auto. simpl.
exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
- simpl in H; inv H. InvBooleans. subst n.
++ destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
+* simpl in H; inv H. InvBooleans. subst n.
exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl.
exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
- apply make_cmp_base_correct; auto.
-- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
- simpl in H; inv H. InvBooleans. subst n.
+* apply make_cmp_base_correct; auto.
+- unfold make_cmp_imm_ne.
+ destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
++ simpl in H; inv H. InvBooleans. subst n.
exists (e#r1); split; auto. simpl.
exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
++ destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
+* simpl in H; inv H. InvBooleans. subst n.
+ exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+* apply make_cmp_base_correct; auto.
+- unfold make_cmp_imm_eq.
destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
- simpl in H; inv H. InvBooleans. subst n.
++ simpl in H; inv H. InvBooleans. subst n.
+ exists (e#r1); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
++ destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
+* simpl in H; inv H. InvBooleans. subst n.
+ exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+* apply make_cmp_base_correct; auto.
+- unfold make_cmp_imm_ne.
+ destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
++ simpl in H; inv H. InvBooleans. subst n.
+ exists (e#r1); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
++ destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
+* simpl in H; inv H. InvBooleans. subst n.
exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl.
exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
- apply make_cmp_base_correct; auto.
+* apply make_cmp_base_correct; auto.
- apply make_cmp_base_correct; auto.
Qed.
diff --git a/x86/ConstpropOp.vp b/x86/ConstpropOp.vp
index 59719cf6..f59b9dba 100644
--- a/x86/ConstpropOp.vp
+++ b/x86/ConstpropOp.vp
@@ -72,16 +72,28 @@ Nondetfunction cond_strength_reduction
Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) :=
let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args').
+Definition make_cmp_imm_eq (c: condition) (args: list reg) (vl: list aval)
+ (n: int) (r1: reg) (v1: aval) :=
+ if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
+ else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
+ else make_cmp_base c args vl.
+
+Definition make_cmp_imm_ne (c: condition) (args: list reg) (vl: list aval)
+ (n: int) (r1: reg) (v1: aval) :=
+ if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
+ else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
+ else make_cmp_base c args vl.
+
Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) :=
match c, args, vl with
| Ccompimm Ceq n, r1 :: nil, v1 :: nil =>
- if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
- else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
- else make_cmp_base c args vl
+ make_cmp_imm_eq c args vl n r1 v1
| Ccompimm Cne n, r1 :: nil, v1 :: nil =>
- if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil)
- else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil)
- else make_cmp_base c args vl
+ make_cmp_imm_ne c args vl n r1 v1
+ | Ccompuimm Ceq n, r1 :: nil, v1 :: nil =>
+ make_cmp_imm_eq c args vl n r1 v1
+ | Ccompuimm Cne n, r1 :: nil, v1 :: nil =>
+ make_cmp_imm_ne c args vl n r1 v1
| _, _, _ =>
make_cmp_base c args vl
end.
diff --git a/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v
index 5d79de6c..3bb0f3cd 100644
--- a/x86/ConstpropOpproof.v
+++ b/x86/ConstpropOpproof.v
@@ -328,24 +328,46 @@ Proof.
e#r = Vundef \/ e#r = Vint Int.zero \/ e#r = Vint Int.one).
{ intros. apply vmatch_Uns_1 with bc Ptop. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. }
unfold make_cmp. case (make_cmp_match c args vl); intros.
-- destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
- simpl in H; inv H. InvBooleans. subst n.
+- unfold make_cmp_imm_eq.
+ destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
++ simpl in H; inv H. InvBooleans. subst n.
exists (e#r1); split; auto. simpl.
exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
- simpl in H; inv H. InvBooleans. subst n.
++ destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
+* simpl in H; inv H. InvBooleans. subst n.
exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl.
exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
- apply make_cmp_base_correct; auto.
-- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
- simpl in H; inv H. InvBooleans. subst n.
+* apply make_cmp_base_correct; auto.
+- unfold make_cmp_imm_ne.
+ destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
++ simpl in H; inv H. InvBooleans. subst n.
exists (e#r1); split; auto. simpl.
exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
++ destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
+* simpl in H; inv H. InvBooleans. subst n.
+ exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+* apply make_cmp_base_correct; auto.
+- unfold make_cmp_imm_eq.
destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
- simpl in H; inv H. InvBooleans. subst n.
++ simpl in H; inv H. InvBooleans. subst n.
+ exists (e#r1); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
++ destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
+* simpl in H; inv H. InvBooleans. subst n.
+ exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+* apply make_cmp_base_correct; auto.
+- unfold make_cmp_imm_ne.
+ destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
++ simpl in H; inv H. InvBooleans. subst n.
+ exists (e#r1); split; auto. simpl.
+ exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
++ destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
+* simpl in H; inv H. InvBooleans. subst n.
exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl.
exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
- apply make_cmp_base_correct; auto.
+* apply make_cmp_base_correct; auto.
- apply make_cmp_base_correct; auto.
Qed.
generated by cgit (git 2.34.1) at 2024-06-11 05:48:22 +0000