summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ia32/Asm.v3
-rw-r--r--ia32/Asmgen.v3
-rw-r--r--ia32/ConstpropOp.vp4
-rw-r--r--ia32/ConstpropOpproof.v2
-rw-r--r--ia32/Machregs.v1
-rw-r--r--ia32/NeedOp.v2
-rw-r--r--ia32/Op.v5
-rw-r--r--ia32/PrintAsm.ml2
-rw-r--r--ia32/SelectOp.vp66
-rw-r--r--ia32/SelectOpproof.v37
-rw-r--r--ia32/ValueAOp.v1
11 files changed, 100 insertions, 26 deletions
diff --git a/ia32/Asm.v b/ia32/Asm.v
index 08a1ef4..f03ea75 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -156,6 +156,7 @@ Inductive instruction: Type :=
| Pxor_r (rd: ireg) (**r [xor] with self = set to zero *)
| Pxor_rr (rd: ireg) (r1: ireg)
| Pxor_ri (rd: ireg) (n: int)
+ | Pnot (rd: ireg)
| Psal_rcl (rd: ireg)
| Psal_ri (rd: ireg) (n: int)
| Pshr_rcl (rd: ireg)
@@ -573,6 +574,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
Next (nextinstr_nf (rs#rd <- (Val.xor rs#rd rs#r1))) m
| Pxor_ri rd n =>
Next (nextinstr_nf (rs#rd <- (Val.xor rs#rd (Vint n)))) m
+ | Pnot rd =>
+ Next (nextinstr_nf (rs#rd <- (Val.notint rs#rd))) m
| Psal_rcl rd =>
Next (nextinstr_nf (rs#rd <- (Val.shl rs#rd rs#ECX))) m
| Psal_ri rd n =>
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index fa4112d..f92d72c 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -357,6 +357,9 @@ Definition transl_op
| Oxorimm n, a1 :: nil =>
assertion (mreg_eq a1 res);
do r <- ireg_of res; OK (Pxor_ri r n :: k)
+ | Onot, a1 :: nil =>
+ assertion (mreg_eq a1 res);
+ do r <- ireg_of res; OK (Pnot r :: k)
| Oshl, a1 :: a2 :: nil =>
assertion (mreg_eq a1 res);
assertion (mreg_eq a2 CX);
diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index aaf08a1..172f7a4 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/ConstpropOp.vp
@@ -132,8 +132,8 @@ Definition make_orimm (n: int) (r: reg) :=
else (Oorimm n, r :: nil).
Definition make_xorimm (n: int) (r: reg) :=
- if Int.eq n Int.zero
- then (Omove, r :: nil)
+ if Int.eq n Int.zero then (Omove, r :: nil)
+ else if Int.eq n Int.mone then (Onot, r :: nil)
else (Oxorimm n, r :: nil).
Definition make_divimm n (r1 r2: reg) :=
diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index 148a08d..6a83c1a 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.v
@@ -309,6 +309,8 @@ Proof.
intros; unfold make_xorimm.
predSpec Int.eq Int.eq_spec n Int.zero; intros.
subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.xor_zero; auto.
+ predSpec Int.eq Int.eq_spec n Int.mone; intros.
+ subst n. exists (Val.notint e#r); split; auto.
econstructor; split; eauto. auto.
Qed.
diff --git a/ia32/Machregs.v b/ia32/Machregs.v
index 85b561e..da80a6e 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -211,6 +211,7 @@ Definition two_address_op (op: operation) : bool :=
| Oorimm _ => true
| Oxor => true
| Oxorimm _ => true
+ | Onot => true
| Oshl => true
| Oshlimm _ => true
| Oshr => true
diff --git a/ia32/NeedOp.v b/ia32/NeedOp.v
index 1237473..2c8698f 100644
--- a/ia32/NeedOp.v
+++ b/ia32/NeedOp.v
@@ -53,6 +53,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| Oorimm n => op1 (orimm nv n)
| Oxor => op2 (bitwise nv)
| Oxorimm n => op1 (bitwise nv)
+ | Onot => op1 (bitwise nv)
| Oshl => op2 (default nv)
| Oshlimm n => op1 (shlimm nv n)
| Oshr => op2 (default nv)
@@ -158,6 +159,7 @@ Proof.
- apply orimm_sound; auto.
- apply xor_sound; auto.
- apply xor_sound; auto with na.
+- apply notint_sound; auto.
- apply shlimm_sound; auto.
- apply shrimm_sound; auto.
- apply shruimm_sound; auto.
diff --git a/ia32/Op.v b/ia32/Op.v
index 26e6688..5420607 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -90,6 +90,7 @@ Inductive operation : Type :=
| Oorimm: int -> operation (**r [rd = r1 | n] *)
| Oxor: operation (**r [rd = r1 ^ r2] *)
| Oxorimm: int -> operation (**r [rd = r1 ^ n] *)
+ | Onot: operation (**r [rd = ~r1] *)
| Oshl: operation (**r [rd = r1 << r2] *)
| Oshlimm: int -> operation (**r [rd = r1 << n] *)
| Oshr: operation (**r [rd = r1 >> r2] (signed) *)
@@ -230,6 +231,7 @@ Definition eval_operation
| Oorimm n, v1::nil => Some (Val.or v1 (Vint n))
| Oxor, v1::v2::nil => Some(Val.xor v1 v2)
| Oxorimm n, v1::nil => Some (Val.xor v1 (Vint n))
+ | Onot, v1::nil => Some(Val.notint v1)
| Oshl, v1::v2::nil => Some (Val.shl v1 v2)
| Oshlimm n, v1::nil => Some (Val.shl v1 (Vint n))
| Oshr, v1::v2::nil => Some (Val.shr v1 v2)
@@ -321,6 +323,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
| Oorimm _ => (Tint :: nil, Tint)
| Oxor => (Tint :: Tint :: nil, Tint)
| Oxorimm _ => (Tint :: nil, Tint)
+ | Onot => (Tint :: nil, Tint)
| Oshl => (Tint :: Tint :: nil, Tint)
| Oshlimm _ => (Tint :: nil, Tint)
| Oshr => (Tint :: Tint :: nil, Tint)
@@ -407,6 +410,7 @@ Proof with (try exact I).
destruct v0...
destruct v0; destruct v1...
destruct v0...
+ destruct v0...
destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)...
destruct v0; simpl... destruct (Int.ltu i Int.iwordsize)...
destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)...
@@ -835,6 +839,7 @@ Proof.
inv H4; simpl; auto.
inv H4; inv H2; simpl; auto.
inv H4; simpl; auto.
+ inv H4; simpl; auto.
inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto.
inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index d67fb9e..9a2648a 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -644,6 +644,8 @@ let print_instruction oc = function
fprintf oc " xorl %a, %a\n" ireg r1 ireg rd
| Pxor_ri(rd, n) ->
fprintf oc " xorl $%a, %a\n" coqint n ireg rd
+ | Pnot(rd) ->
+ fprintf oc " notl %a\n" ireg rd
| Psal_rcl(rd) ->
fprintf oc " sall %%cl, %a\n" ireg rd
| Psal_ri(rd, n) ->
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index e80c3f3..5f47df2 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -68,7 +68,12 @@ Definition addrstack (ofs: int) :=
(** ** Integer logical negation *)
-Definition notint (e: expr) := Eop (Oxorimm Int.mone) (e ::: Enil).
+Nondetfunction notint (e: expr) :=
+ match e with
+ | Eop (Ointconst n) Enil => Eop (Ointconst (Int.not n)) Enil
+ | Eop (Oxorimm n) (e1 ::: Enil) => Eop (Oxorimm (Int.not n)) (e1 ::: Enil)
+ | _ => Eop Onot (e ::: Enil)
+ end.
(** ** Integer addition and pointer addition *)
@@ -110,6 +115,14 @@ Nondetfunction add (e1: expr) (e2: expr) :=
Eop (Olea (Aindexed2 Int.zero)) (e1:::e2:::Enil)
end.
+(** ** Opposite *)
+
+Nondetfunction negint (e: expr) :=
+ match e with
+ | Eop (Ointconst n) Enil => Eop (Ointconst (Int.neg n)) Enil
+ | _ => Eop Oneg (e ::: Enil)
+ end.
+
(** ** Integer and pointer subtraction *)
Nondetfunction sub (e1: expr) (e2: expr) :=
@@ -125,8 +138,6 @@ Nondetfunction sub (e1: expr) (e2: expr) :=
Eop Osub (e1:::e2:::Enil)
end.
-Definition negint (e: expr) := Eop Oneg (e ::: Enil).
-
(** ** Immediate shifts *)
Definition shift_is_scale (n: int) : bool :=
@@ -275,6 +286,8 @@ Nondetfunction xorimm (n1: int) (e2: expr) :=
Eop (Ointconst (Int.xor n1 n2)) Enil
| Eop (Oxorimm n2) (t2:::Enil) =>
Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil)
+ | Eop Onot (t2:::Enil) =>
+ Eop (Oxorimm (Int.not n1)) (t2:::Enil)
| _ =>
Eop (Oxorimm n1) (e2:::Enil)
end.
@@ -399,29 +412,50 @@ Definition compf (c: comparison) (e1: expr) (e2: expr) :=
Nondetfunction cast8unsigned (e: expr) :=
match e with
+ | Eop (Ointconst n) Enil =>
+ Eop (Ointconst (Int.zero_ext 8 n)) Enil
| Eop (Oandimm n) (t:::Enil) =>
- Eop (Oandimm (Int.and (Int.repr 255) n)) (t:::Enil)
+ andimm (Int.and (Int.repr 255) n) t
| _ =>
Eop Ocast8unsigned (e:::Enil)
end.
-Definition cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil).
+Nondetfunction cast8signed (e: expr) :=
+ match e with
+ | Eop (Ointconst n) Enil =>
+ Eop (Ointconst (Int.sign_ext 8 n)) Enil
+ | _ =>
+ Eop Ocast8signed (e ::: Enil)
+ end.
Nondetfunction cast16unsigned (e: expr) :=
match e with
+ | Eop (Ointconst n) Enil =>
+ Eop (Ointconst (Int.zero_ext 16 n)) Enil
| Eop (Oandimm n) (t:::Enil) =>
- Eop (Oandimm (Int.and (Int.repr 65535) n)) (t:::Enil)
+ andimm (Int.and (Int.repr 65535) n) t
| _ =>
Eop Ocast16unsigned (e:::Enil)
end.
-Definition cast16signed (e: expr) := Eop Ocast16signed (e ::: Enil).
+Nondetfunction cast16signed (e: expr) :=
+ match e with
+ | Eop (Ointconst n) Enil =>
+ Eop (Ointconst (Int.sign_ext 16 n)) Enil
+ | _ =>
+ Eop Ocast16signed (e ::: Enil)
+ end.
(** Floating-point conversions *)
Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
-Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil).
+
+Nondetfunction floatofint (e: expr) :=
+ match e with
+ | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.floatofint n)) Enil
+ | _ => Eop Ofloatofint (e ::: Enil)
+ end.
Definition intuoffloat (e: expr) :=
Elet e
@@ -430,12 +464,16 @@ Definition intuoffloat (e: expr) :=
(intoffloat (Eletvar 1))
(addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat.
-Definition floatofintu (e: expr) :=
- let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in
- Elet e
- (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil))
- (floatofint (Eletvar O))
- (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f)).
+Nondetfunction floatofintu (e: expr) :=
+ match e with
+ | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.floatofintu n)) Enil
+ | _ =>
+ let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in
+ Elet e
+ (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil))
+ (floatofint (Eletvar O))
+ (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f))
+ end.
(** ** Addressing modes *)
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 02d3bee..30e8c5b 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -136,7 +136,10 @@ Qed.
Theorem eval_notint: unary_constructor_sound notint Val.notint.
Proof.
- unfold notint; red; intros. TrivialExists.
+ unfold notint; red; intros until x. case (notint_match a); intros.
+ InvEval. TrivialExists.
+ InvEval. subst x. rewrite Val.not_xor. rewrite Val.xor_assoc. TrivialExists.
+ TrivialExists.
Qed.
Lemma shift_symbol_address:
@@ -198,7 +201,9 @@ Qed.
Theorem eval_negint: unary_constructor_sound negint (fun v => Val.sub Vzero v).
Proof.
- red; intros. unfold negint. TrivialExists.
+ red; intros until x. unfold negint. case (negint_match a); intros; InvEval.
+ TrivialExists.
+ TrivialExists.
Qed.
Theorem eval_shlimm:
@@ -443,7 +448,9 @@ Proof.
destruct x; simpl; auto. subst n. rewrite Int.xor_zero. auto.
destruct (xorimm_match a); intros; InvEval.
TrivialExists. simpl. rewrite Int.xor_commut; auto.
- subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists.
+ subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists.
+ subst. rewrite Val.not_xor. rewrite Val.xor_assoc.
+ rewrite (Val.xor_commut (Vint Int.mone)). TrivialExists.
TrivialExists.
Qed.
@@ -679,27 +686,33 @@ Qed.
Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
Proof.
- red; intros. unfold cast8signed. TrivialExists.
+ red; intros until x. unfold cast8signed. case (cast8signed_match a); intros; InvEval.
+ TrivialExists.
+ TrivialExists.
Qed.
Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
Proof.
red; intros until x. unfold cast8unsigned. destruct (cast8unsigned_match a); intros; InvEval.
- subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc.
- rewrite Int.and_commut. TrivialExists. compute; auto.
+ TrivialExists.
+ subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc.
+ rewrite Int.and_commut. apply eval_andimm; auto. compute; auto.
TrivialExists.
Qed.
Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
Proof.
- red; intros. unfold cast16signed. TrivialExists.
+ red; intros until x. unfold cast16signed. case (cast16signed_match a); intros; InvEval.
+ TrivialExists.
+ TrivialExists.
Qed.
Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
Proof.
red; intros until x. unfold cast16unsigned. destruct (cast16unsigned_match a); intros; InvEval.
+ TrivialExists.
subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc.
- rewrite Int.and_commut. TrivialExists. compute; auto.
+ rewrite Int.and_commut. apply eval_andimm; auto. compute; auto.
TrivialExists.
Qed.
@@ -723,7 +736,9 @@ Theorem eval_floatofint:
Val.floatofint x = Some y ->
exists v, eval_expr ge sp e m le (floatofint a) v /\ Val.lessdef y v.
Proof.
- intros; unfold floatofint. TrivialExists.
+ intros until y; unfold floatofint. case (floatofint_match a); intros; InvEval.
+ TrivialExists.
+ TrivialExists.
Qed.
Theorem eval_intuoffloat:
@@ -770,7 +785,9 @@ Theorem eval_floatofintu:
Val.floatofintu x = Some y ->
exists v, eval_expr ge sp e m le (floatofintu a) v /\ Val.lessdef y v.
Proof.
- intros. destruct x; simpl in H0; try discriminate. inv H0.
+ intros until y; unfold floatofintu. case (floatofintu_match a); intros.
+ InvEval. TrivialExists.
+ destruct x; simpl in H0; try discriminate. inv H0.
exists (Vfloat (Float.floatofintu i)); split; auto.
econstructor. eauto.
set (fm := Float.floatofintu Float.ox8000_0000).
diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v
index 1802e11..f3e2194 100644
--- a/ia32/ValueAOp.v
+++ b/ia32/ValueAOp.v
@@ -76,6 +76,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
| Oorimm n, v1::nil => or v1 (I n)
| Oxor, v1::v2::nil => xor v1 v2
| Oxorimm n, v1::nil => xor v1 (I n)
+ | Onot, v1::nil => notint v1
| Oshl, v1::v2::nil => shl v1 v2
| Oshlimm n, v1::nil => shl v1 (I n)
| Oshr, v1::v2::nil => shr v1 v2
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 06:34:13 +0000