diff options
Diffstat (limited to 'ia32/SelectOp.vp')
-rw-r--r-- | ia32/SelectOp.vp | 35 |
1 files changed, 31 insertions, 4 deletions
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index 214608e4..b6aef725 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -346,6 +346,12 @@ Definition addf (e1 e2: expr) := Eop Oaddf (e1 ::: e2 ::: Enil). Definition subf (e1 e2: expr) := Eop Osubf (e1 ::: e2 ::: Enil). Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil). +Definition negfs (e: expr) := Eop Onegfs (e ::: Enil). +Definition absfs (e: expr) := Eop Oabsfs (e ::: Enil). +Definition addfs (e1 e2: expr) := Eop Oaddfs (e1 ::: e2 ::: Enil). +Definition subfs (e1 e2: expr) := Eop Osubfs (e1 ::: e2 ::: Enil). +Definition mulfs (e1 e2: expr) := Eop Omulfs (e1 ::: e2 ::: Enil). + (** ** Comparisons *) Nondetfunction compimm (default: comparison -> int -> condition) @@ -405,6 +411,9 @@ Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) := Definition compf (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). +Definition compfs (c: comparison) (e1: expr) (e2: expr) := + Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil). + (** ** Integer conversions *) Nondetfunction cast8unsigned (e: expr) := @@ -446,32 +455,50 @@ Nondetfunction cast16signed (e: expr) := (** Floating-point conversions *) Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). +Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil). + Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). Nondetfunction floatofint (e: expr) := match e with - | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.floatofint n)) Enil + | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_int n)) Enil | _ => Eop Ofloatofint (e ::: Enil) end. Definition intuoffloat (e: expr) := Elet e - (Elet (Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil) + (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) (intoffloat (Eletvar 1)) (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat. Nondetfunction floatofintu (e: expr) := match e with - | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.floatofintu n)) Enil + | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil | _ => - let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in + let f := Eop (Ofloatconst (Float.of_intu 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. +Definition intofsingle (e: expr) := Eop Ointofsingle (e ::: Enil). + +Nondetfunction singleofint (e: expr) := + match e with + | Eop (Ointconst n) Enil => Eop (Osingleconst (Float32.of_int n)) Enil + | _ => Eop Osingleofint (e ::: Enil) + end. + +Definition intuofsingle (e: expr) := intuoffloat (floatofsingle e). + +Nondetfunction singleofintu (e: expr) := + match e with + | Eop (Ointconst n) Enil => Eop (Osingleconst (Float32.of_intu n)) Enil + | _ => singleoffloat (floatofintu e) + end. + (** ** Addressing modes *) Nondetfunction addressing (chunk: memory_chunk) (e: expr) := |