diff options
Diffstat (limited to 'powerpc/ValueAOp.v')
-rw-r--r-- | powerpc/ValueAOp.v | 33 |
1 files changed, 32 insertions, 1 deletions
diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v index 8081f557..f7f65e9e 100644 --- a/powerpc/ValueAOp.v +++ b/powerpc/ValueAOp.v @@ -34,6 +34,10 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Cmaskzero n, v1 :: nil => maskzero v1 n | Cmasknotzero n, v1 :: nil => cnot (maskzero v1 n) + | Ccompl c, v1 :: v2 :: nil => cmpl_bool c v1 v2 + | Ccomplu c, v1 :: v2 :: nil => cmplu_bool c v1 v2 + | Ccomplimm c n, v1 :: nil => cmpl_bool c v1 (L n) + | Ccompluimm c n, v1 :: nil => cmplu_bool c v1 (L n) | _, _ => Bnone end. @@ -87,6 +91,33 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Oshru, v1::v2::nil => shru v1 v2 | Orolm amount mask, v1::nil => rolm v1 amount mask | Oroli amount mask, v1::v2::nil => or (and v1 (I (Int.not mask))) (rolm v2 amount mask) + | Olongconst n, nil => L n + | Ocast32signed, v1::nil => longofint v1 + | Ocast32unsigned, v1::nil => longofintu v1 + | Oaddl, v1::v2::nil => addl v1 v2 + | Oaddlimm n, v1::nil => addl v1 (L n) + | Osubl, v1::v2::nil => subl v1 v2 + | Onegl, v1::nil => negl v1 + | Omull, v1::v2::nil => mull v1 v2 + | Omullhs, v1::v2::nil => mullhs v1 v2 + | Omullhu, v1::v2::nil => mullhu v1 v2 + | Odivl, v1::v2::nil => divls v1 v2 + | Odivlu, v1::v2::nil => divlu v1 v2 + | Oandl, v1::v2::nil => andl v1 v2 + | Oandlimm n, v1::nil => andl v1 (L n) + | Oorl, v1::v2::nil => orl v1 v2 + | Oorlimm n, v1::nil => orl v1 (L n) + | Oxorl, v1::v2::nil => xorl v1 v2 + | Oxorlimm n, v1::nil => xorl v1 (L n) + | Onotl, v1::nil => notl v1 + | Oshll, v1::v2::nil => shll v1 v2 + | Oshrl, v1::v2::nil => shrl v1 v2 + | Oshrlimm n, v1::nil => shrl v1 (I n) + | Oshrxlimm n, v1::nil => shrxl v1 (I n) + | Oshrlu, v1::v2::nil => shrlu v1 v2 + | Orolml amount mask, v1::nil => rolml v1 amount mask + | Olongoffloat, v1::nil => longoffloat v1 + | Ofloatoflong, v1::nil => floatoflong v1 | Onegf, v1::nil => negf v1 | Oabsf, v1::nil => absf v1 | Oaddf, v1::v2::nil => addf v1 v2 @@ -177,9 +208,9 @@ Proof. destruct (propagate_float_constants tt); constructor. rewrite Ptrofs.add_zero_l; eauto with va. fold (Val.sub (Vint i) a1). auto with va. + apply rolml_sound; auto. apply floatofwords_sound; auto. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. Qed. End SOUNDNESS. - |