diff options
Diffstat (limited to 'ia32/SelectOp.vp')
-rw-r--r-- | ia32/SelectOp.vp | 84 |
1 files changed, 40 insertions, 44 deletions
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index 6d44cf50..7bb2bee6 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -74,36 +74,6 @@ Definition addrstack (ofs: int) := Definition notint (e: expr) := Eop (Oxorimm Int.mone) (e ::: Enil). -(** ** Boolean value and boolean negation *) - -Fixpoint boolval (e: expr) {struct e} : expr := - let default := Eop (Ocmp (Ccompuimm Cne Int.zero)) (e ::: Enil) in - match e with - | Eop (Ointconst n) Enil => - Eop (Ointconst (if Int.eq n Int.zero then Int.zero else Int.one)) Enil - | Eop (Ocmp cond) args => - Eop (Ocmp cond) args - | Econdition e1 e2 e3 => - Econdition e1 (boolval e2) (boolval e3) - | _ => - default - end. - -(** ** Boolean negation *) - -Fixpoint notbool (e: expr) {struct e} : expr := - let default := Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil) in - match e with - | Eop (Ointconst n) Enil => - Eop (Ointconst (if Int.eq n Int.zero then Int.one else Int.zero)) Enil - | Eop (Ocmp cond) args => - Eop (Ocmp (negate_condition cond)) args - | Econdition e1 e2 e3 => - Econdition e1 (notbool e2) (notbool e3) - | _ => - default - end. - (** ** Integer addition and pointer addition *) Definition offset_addressing (a: addressing) (ofs: int) : addressing := @@ -368,12 +338,46 @@ Definition divf (e1 e2: expr) := Eop Odivf (e1 ::: e2 ::: Enil). (** ** Comparisons *) +Nondetfunction compimm (default: comparison -> int -> condition) + (sem: comparison -> int -> int -> bool) + (c: comparison) (e1: expr) (n2: int) := + match c, e1 with + | c, Eop (Ointconst n1) Enil => + Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil + | Ceq, Eop (Ocmp c) el => + if Int.eq_dec n2 Int.zero then + Eop (Ocmp (negate_condition c)) el + else if Int.eq_dec n2 Int.one then + Eop (Ocmp c) el + else + Eop (Ointconst Int.zero) Enil + | Cne, Eop (Ocmp c) el => + if Int.eq_dec n2 Int.zero then + Eop (Ocmp c) el + else if Int.eq_dec n2 Int.one then + Eop (Ocmp (negate_condition c)) el + else + Eop (Ointconst Int.one) Enil + | Ceq, Eop (Oandimm n1) (t1 ::: Enil) => + if Int.eq_dec n2 Int.zero then + Eop (Ocmp (Cmaskzero n1)) (t1 ::: Enil) + else + Eop (Ocmp (default c n2)) (e1 ::: Enil) + | Cne, Eop (Oandimm n1) (t1 ::: Enil) => + if Int.eq_dec n2 Int.zero then + Eop (Ocmp (Cmasknotzero n1)) (t1 ::: Enil) + else + Eop (Ocmp (default c n2)) (e1 ::: Enil) + | _, _ => + Eop (Ocmp (default c n2)) (e1 ::: Enil) + end. + Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) := match e1, e2 with | Eop (Ointconst n1) Enil, t2 => - Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2 ::: Enil) + compimm Ccompimm Int.cmp (swap_comparison c) t2 n1 | t1, Eop (Ointconst n2) Enil => - Eop (Ocmp (Ccompimm c n2)) (t1 ::: Enil) + compimm Ccompimm Int.cmp c t1 n2 | _, _ => Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil) end. @@ -381,9 +385,9 @@ Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) := Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) := match e1, e2 with | Eop (Ointconst n1) Enil, t2 => - Eop (Ocmp (Ccompuimm (swap_comparison c) n1)) (t2 ::: Enil) + compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1 | t1, Eop (Ointconst n2) Enil => - Eop (Ocmp (Ccompuimm c n2)) (t1 ::: Enil) + compimm Ccompuimm Int.cmpu c t1 n2 | _, _ => Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil) end. @@ -420,17 +424,16 @@ Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil). Definition intuoffloat (e: expr) := - let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in Elet e (Elet (Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil) - (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) + (Econdition (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil) (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)) + (Econdition (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil) (floatofint (Eletvar O)) (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f)). @@ -442,10 +445,3 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) := | _ => (Aindexed Int.zero, e:::Enil) end. -(** ** Turning an expression into a condition *) - -Nondetfunction cond_of_expr (e: expr) := - match e with - | Eop (Oandimm n) (t1:::Enil) => (Cmasknotzero n, t1:::Enil) - | _ => (Ccompuimm Cne Int.zero, e:::Enil) - end. |