Unverified Commit 16608ca8 authored by Xavier Leroy's avatar Xavier Leroy Committed by GitHub
Browse files

Improve strength reduction of unsigned comparisons x ==u 0, x !=u 0, etc (#59)

When x is known to be either 0 or 1, comparisons such as
x == 0   x != 0    x == 1    x != 1
can be optimized away.  This optimization was already performed
for signed comparisons.  This commit extends the optimization to
unsigned comparisons as well.

Additionally, for PowerPC only, some unsigned (dis)equality comparisons are
turned into signed comparisons when we know it makes no difference,
i.e. when both arguments are guaranteed not to be pointers.  The
reason is that Asmgen can produce shorter instruction sequences for
some signed equality comparisons than for the corresponding unsigned
comparisons.

It's important to optimize unsigned integer comparisons because casts
to the C99 type _Bool are compiled as x !=u 0 unsigned comparisons.
In particular, cascades of casts to _Bool are now reduced to a single
cast much more often than before.
parent d2c5701f
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment