diff options
Diffstat (limited to 'powerpc/ConstpropOp.vp')
-rw-r--r-- | powerpc/ConstpropOp.vp | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index 32986713..60b5c63c 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -70,11 +70,13 @@ Definition eval_static_condition_val (cond: condition) (vl: list approx) := Definition eval_static_intoffloat (f: float) := match Float.intoffloat f with Some x => I x | None => Unknown end. +Parameter propagate_float_constants: unit -> bool. + Nondetfunction eval_static_operation (op: operation) (vl: list approx) := match op, vl with | Omove, v1::nil => v1 | Ointconst n, nil => I n - | Ofloatconst n, nil => F n + | Ofloatconst n, nil => if propagate_float_constants tt then F n else Unknown | Oaddrsymbol s n, nil => G s n | Oaddrstack n, nil => S n | Ocast8signed, I n1 :: nil => I(Int.sign_ext 8 n1) @@ -119,11 +121,27 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) := | Odivf, F n1 :: F n2 :: nil => F(Float.div n1 n2) | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1) | Ointoffloat, F n1 :: nil => eval_static_intoffloat n1 - | Ofloatofwords, I n1 :: I n2 :: nil => F(Float.from_words n1 n2) + | Ofloatofwords, I n1 :: I n2 :: nil => if propagate_float_constants tt then F(Float.from_words n1 n2) else Unknown | Ocmp c, vl => eval_static_condition_val c vl | _, _ => Unknown end. +Nondetfunction eval_static_addressing (addr: addressing) (vl: list approx) := + match addr, vl with + | Aindexed n, I n1::nil => I (Int.add n1 n) + | Aindexed n, G id ofs::nil => G id (Int.add ofs n) + | Aindexed n, S ofs::nil => S (Int.add ofs n) + | Aindexed2, I n1::I n2::nil => I (Int.add n1 n2) + | Aindexed2, G id ofs::I n2::nil => G id (Int.add ofs n2) + | Aindexed2, I n1::G id ofs::nil => G id (Int.add ofs n1) + | Aindexed2, S ofs::I n2::nil => S (Int.add ofs n2) + | Aindexed2, I n1::S ofs::nil => S (Int.add ofs n1) + | Aglobal id ofs, nil => G id ofs + | Abased id ofs, I n1::nil => G id (Int.add ofs n1) + | Ainstack ofs, nil => S ofs + | _, _ => Unknown + end. + (** * Operator strength reduction *) (** We now define auxiliary functions for strength reduction of |