summaryrefslogtreecommitdiff
path: root/ia32/Op.v
diff options
context:
space:
mode:
Diffstat (limited to 'ia32/Op.v')
-rw-r--r--ia32/Op.v134
1 files changed, 71 insertions, 63 deletions
diff --git a/ia32/Op.v b/ia32/Op.v
index e46c740..14e4cbb 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -42,8 +42,10 @@ Inductive condition : Type :=
| Ccompu: comparison -> condition (**r unsigned integer comparison *)
| Ccompimm: comparison -> int -> condition (**r signed integer comparison with a constant *)
| Ccompuimm: comparison -> int -> condition (**r unsigned integer comparison with a constant *)
- | Ccompf: comparison -> condition (**r floating-point comparison *)
+ | Ccompf: comparison -> condition (**r 64-bit floating-point comparison *)
| Cnotcompf: comparison -> condition (**r negation of a floating-point comparison *)
+ | Ccompfs: comparison -> condition (**r 32-bit floating-point comparison *)
+ | Cnotcompfs: comparison -> condition (**r negation of a floating-point comparison *)
| Cmaskzero: int -> condition (**r test [(arg & constant) == 0] *)
| Cmasknotzero: int -> condition. (**r test [(arg & constant) != 0] *)
@@ -68,6 +70,7 @@ Inductive operation : Type :=
| Omove: operation (**r [rd = r1] *)
| Ointconst: int -> operation (**r [rd] is set to the given integer constant *)
| Ofloatconst: float -> operation (**r [rd] is set to the given float constant *)
+ | Osingleconst: float32 -> operation (**r [rd] is set to the given float constant *)
| Oindirectsymbol: ident -> operation (**r [rd] is set to the address of the symbol *)
(*c Integer arithmetic: *)
| Ocast8signed: operation (**r [rd] is 8-bit sign extension of [r1] *)
@@ -108,10 +111,19 @@ Inductive operation : Type :=
| Osubf: operation (**r [rd = r1 - r2] *)
| Omulf: operation (**r [rd = r1 * r2] *)
| Odivf: operation (**r [rd = r1 / r2] *)
+ | Onegfs: operation (**r [rd = - r1] *)
+ | Oabsfs: operation (**r [rd = abs(r1)] *)
+ | Oaddfs: operation (**r [rd = r1 + r2] *)
+ | Osubfs: operation (**r [rd = r1 - r2] *)
+ | Omulfs: operation (**r [rd = r1 * r2] *)
+ | Odivfs: operation (**r [rd = r1 / r2] *)
| Osingleoffloat: operation (**r [rd] is [r1] truncated to single-precision float *)
+ | Ofloatofsingle: operation (**r [rd] is [r1] extended to double-precision float *)
(*c Conversions between int and float: *)
- | Ointoffloat: operation (**r [rd = signed_int_of_float(r1)] *)
- | Ofloatofint: operation (**r [rd = float_of_signed_int(r1)] *)
+ | Ointoffloat: operation (**r [rd = signed_int_of_float64(r1)] *)
+ | Ofloatofint: operation (**r [rd = float64_of_signed_int(r1)] *)
+ | Ointofsingle: operation (**r [rd = signed_int_of_float32(r1)] *)
+ | Osingleofint: operation (**r [rd = float32_of_signed_int(r1)] *)
(*c Manipulating 64-bit integers: *)
| Omakelong: operation (**r [rd = r1 << 32 | r2] *)
| Olowlong: operation (**r [rd = low-word(r1)] *)
@@ -145,6 +157,7 @@ Definition eq_operation (x y: operation): {x=y} + {x<>y}.
Proof.
generalize Int.eq_dec; intro.
generalize Float.eq_dec; intro.
+ generalize Float32.eq_dec; intro.
generalize Int64.eq_dec; intro.
decide equality.
apply peq.
@@ -169,6 +182,8 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool
| Ccompuimm c n, v1 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint n)
| Ccompf c, v1 :: v2 :: nil => Val.cmpf_bool c v1 v2
| Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2)
+ | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2
+ | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2)
| Cmaskzero n, v1 :: nil => Val.maskzero_bool v1 n
| Cmasknotzero n, v1 :: nil => option_map negb (Val.maskzero_bool v1 n)
| _, _ => None
@@ -204,6 +219,7 @@ Definition eval_operation
| Omove, v1::nil => Some v1
| Ointconst n, nil => Some (Vint n)
| Ofloatconst n, nil => Some (Vfloat n)
+ | Osingleconst n, nil => Some (Vsingle n)
| Oindirectsymbol id, nil => Some (Genv.symbol_address genv id Int.zero)
| Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1)
| Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1)
@@ -243,9 +259,18 @@ Definition eval_operation
| Osubf, v1::v2::nil => Some(Val.subf v1 v2)
| Omulf, v1::v2::nil => Some(Val.mulf v1 v2)
| Odivf, v1::v2::nil => Some(Val.divf v1 v2)
+ | Onegfs, v1::nil => Some(Val.negfs v1)
+ | Oabsfs, v1::nil => Some(Val.absfs v1)
+ | Oaddfs, v1::v2::nil => Some(Val.addfs v1 v2)
+ | Osubfs, v1::v2::nil => Some(Val.subfs v1 v2)
+ | Omulfs, v1::v2::nil => Some(Val.mulfs v1 v2)
+ | Odivfs, v1::v2::nil => Some(Val.divfs v1 v2)
| Osingleoffloat, v1::nil => Some(Val.singleoffloat v1)
+ | Ofloatofsingle, v1::nil => Some(Val.floatofsingle v1)
| Ointoffloat, v1::nil => Val.intoffloat v1
| Ofloatofint, v1::nil => Val.floatofint v1
+ | Ointofsingle, v1::nil => Val.intofsingle v1
+ | Osingleofint, v1::nil => Val.singleofint v1
| Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2)
| Olowlong, v1::nil => Some(Val.loword v1)
| Ohighlong, v1::nil => Some(Val.hiword v1)
@@ -275,6 +300,8 @@ Definition type_of_condition (c: condition) : list typ :=
| Ccompuimm _ _ => Tint :: nil
| Ccompf _ => Tfloat :: Tfloat :: nil
| Cnotcompf _ => Tfloat :: Tfloat :: nil
+ | Ccompfs _ => Tsingle :: Tsingle :: nil
+ | Cnotcompfs _ => Tsingle :: Tsingle :: nil
| Cmaskzero _ => Tint :: nil
| Cmasknotzero _ => Tint :: nil
end.
@@ -295,7 +322,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
match op with
| Omove => (nil, Tint) (* treated specially *)
| Ointconst _ => (nil, Tint)
- | Ofloatconst f => (nil, if Float.is_single_dec f then Tsingle else Tfloat)
+ | Ofloatconst f => (nil, Tfloat)
+ | Osingleconst f => (nil, Tsingle)
| Oindirectsymbol _ => (nil, Tint)
| Ocast8signed => (Tint :: nil, Tint)
| Ocast8unsigned => (Tint :: nil, Tint)
@@ -334,9 +362,18 @@ Definition type_of_operation (op: operation) : list typ * typ :=
| Osubf => (Tfloat :: Tfloat :: nil, Tfloat)
| Omulf => (Tfloat :: Tfloat :: nil, Tfloat)
| Odivf => (Tfloat :: Tfloat :: nil, Tfloat)
+ | Onegfs => (Tsingle :: nil, Tsingle)
+ | Oabsfs => (Tsingle :: nil, Tsingle)
+ | Oaddfs => (Tsingle :: Tsingle :: nil, Tsingle)
+ | Osubfs => (Tsingle :: Tsingle :: nil, Tsingle)
+ | Omulfs => (Tsingle :: Tsingle :: nil, Tsingle)
+ | Odivfs => (Tsingle :: Tsingle :: nil, Tsingle)
| Osingleoffloat => (Tfloat :: nil, Tsingle)
+ | Ofloatofsingle => (Tsingle :: nil, Tfloat)
| Ointoffloat => (Tfloat :: nil, Tint)
| Ofloatofint => (Tint :: nil, Tfloat)
+ | Ointofsingle => (Tsingle :: nil, Tint)
+ | Osingleofint => (Tint :: nil, Tsingle)
| Omakelong => (Tint :: Tint :: nil, Tlong)
| Olowlong => (Tlong :: nil, Tint)
| Ohighlong => (Tlong :: nil, Tint)
@@ -380,7 +417,8 @@ Proof with (try exact I).
destruct op; simpl in H0; FuncInv; subst; simpl.
congruence.
exact I.
- destruct (Float.is_single_dec f); auto.
+ exact I.
+ exact I.
unfold Genv.symbol_address; destruct (Genv.find_symbol genv i)...
destruct v0...
destruct v0...
@@ -422,8 +460,17 @@ Proof with (try exact I).
destruct v0; destruct v1...
destruct v0; destruct v1...
destruct v0; destruct v1...
- destruct v0... apply Float.singleoffloat_is_single.
- destruct v0; simpl in H0; inv H0. destruct (Float.intoffloat f); inv H2...
+ destruct v0...
+ destruct v0...
+ destruct v0; destruct v1...
+ destruct v0; destruct v1...
+ destruct v0; destruct v1...
+ destruct v0; destruct v1...
+ destruct v0...
+ destruct v0...
+ destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); inv H2...
+ destruct v0; simpl in H0; inv H0...
+ destruct v0; simpl in H0; inv H0. destruct (Float32.to_int f); inv H2...
destruct v0; simpl in H0; inv H0...
destruct v0; destruct v1...
destruct v0...
@@ -467,6 +514,8 @@ Definition negate_condition (cond: condition): condition :=
| Ccompuimm c n => Ccompuimm (negate_comparison c) n
| Ccompf c => Cnotcompf c
| Cnotcompf c => Ccompf c
+ | Ccompfs c => Cnotcompfs c
+ | Cnotcompfs c => Ccompfs c
| Cmaskzero n => Cmasknotzero n
| Cmasknotzero n => Cmaskzero n
end.
@@ -482,6 +531,8 @@ Proof.
repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
repeat (destruct vl; auto).
repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0) as [[]|]; auto.
+ repeat (destruct vl; auto).
+ repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto.
destruct vl; auto. destruct vl; auto.
destruct vl; auto. destruct vl; auto. destruct (Val.maskzero_bool v i) as [[]|]; auto.
Qed.
@@ -608,61 +659,6 @@ Proof.
destruct c; simpl; try congruence. reflexivity.
Qed.
-(** Checking whether two addressings, applied to the same arguments, produce
- separated memory addresses. Used in [CSE]. *)
-
-Definition addressing_separated (chunk1: memory_chunk) (addr1: addressing)
- (chunk2: memory_chunk) (addr2: addressing) : bool :=
- match addr1, addr2 with
- | Aindexed ofs1, Aindexed ofs2 =>
- Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2)
- | Aglobal s1 ofs1, Aglobal s2 ofs2 =>
- if ident_eq s1 s2 then Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2) else true
- | Abased s1 ofs1, Abased s2 ofs2 =>
- if ident_eq s1 s2 then Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2) else true
- | Ainstack ofs1, Ainstack ofs2 =>
- Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2)
- | _, _ => false
- end.
-
-Lemma addressing_separated_sound:
- forall (F V: Type) (ge: Genv.t F V) sp chunk1 addr1 chunk2 addr2 vl b1 n1 b2 n2,
- addressing_separated chunk1 addr1 chunk2 addr2 = true ->
- eval_addressing ge sp addr1 vl = Some(Vptr b1 n1) ->
- eval_addressing ge sp addr2 vl = Some(Vptr b2 n2) ->
- b1 <> b2 \/ Int.unsigned n1 + size_chunk chunk1 <= Int.unsigned n2 \/ Int.unsigned n2 + size_chunk chunk2 <= Int.unsigned n1.
-Proof.
- unfold addressing_separated; intros.
- generalize (size_chunk_pos chunk1) (size_chunk_pos chunk2); intros SZ1 SZ2.
- destruct addr1; destruct addr2; try discriminate; simpl in *; FuncInv.
-(* Aindexed *)
- destruct v; simpl in *; inv H1; inv H2.
- right. apply Int.no_overlap_sound; auto.
-(* Aglobal *)
- unfold Genv.symbol_address in *.
- destruct (Genv.find_symbol ge i1) eqn:?; inv H2.
- destruct (Genv.find_symbol ge i) eqn:?; inv H1.
- destruct (ident_eq i i1). subst.
- replace (Int.unsigned n1) with (Int.unsigned (Int.add Int.zero n1)).
- replace (Int.unsigned n2) with (Int.unsigned (Int.add Int.zero n2)).
- right. apply Int.no_overlap_sound; auto.
- rewrite Int.add_commut; rewrite Int.add_zero; auto.
- rewrite Int.add_commut; rewrite Int.add_zero; auto.
- left. red; intros; elim n. subst. eapply Genv.genv_vars_inj; eauto.
-(* Abased *)
- unfold Genv.symbol_address in *.
- destruct (Genv.find_symbol ge i1) eqn:?; simpl in *; try discriminate.
- destruct v; inv H2.
- destruct (Genv.find_symbol ge i) eqn:?; inv H1.
- destruct (ident_eq i i1). subst.
- rewrite (Int.add_commut i0 i3). rewrite (Int.add_commut i2 i3).
- right. apply Int.no_overlap_sound; auto.
- left. red; intros; elim n. subst. eapply Genv.genv_vars_inj; eauto.
-(* Ainstack *)
- destruct sp; simpl in *; inv H1; inv H2.
- right. apply Int.no_overlap_sound; auto.
-Qed.
-
(** * Invariance and compatibility properties. *)
(** [eval_operation] and [eval_addressing] depend on a global environment
@@ -770,6 +766,8 @@ Proof.
eauto 3 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
inv H3; inv H2; simpl in H0; inv H0; auto.
inv H3; inv H2; simpl in H0; inv H0; auto.
+ inv H3; inv H2; simpl in H0; inv H0; auto.
+ inv H3; inv H2; simpl in H0; inv H0; auto.
inv H3; try discriminate; auto.
inv H3; try discriminate; auto.
Qed.
@@ -853,7 +851,17 @@ Proof.
inv H4; inv H2; simpl; auto.
inv H4; inv H2; simpl; auto.
inv H4; simpl; auto.
- inv H4; simpl in H1; inv H1. simpl. destruct (Float.intoffloat f0); simpl in H2; inv H2.
+ inv H4; simpl; auto.
+ inv H4; inv H2; simpl; auto.
+ inv H4; inv H2; simpl; auto.
+ inv H4; inv H2; simpl; auto.
+ inv H4; inv H2; simpl; auto.
+ inv H4; simpl; auto.
+ inv H4; simpl; auto.
+ inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_int f0); simpl in H2; inv H2.
+ exists (Vint i); auto.
+ inv H4; simpl in H1; inv H1. simpl. TrivialExists.
+ inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_int f0); simpl in H2; inv H2.
exists (Vint i); auto.
inv H4; simpl in H1; inv H1. simpl. TrivialExists.
inv H4; inv H2; simpl; auto.