diff options
Diffstat (limited to 'kvx/ValueAOp.v')
| -rw-r--r-- | kvx/ValueAOp.v | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v index 87554258..ddfe94f3 100644 --- a/kvx/ValueAOp.v +++ b/kvx/ValueAOp.v @@ -156,6 +156,12 @@ Definition eval_static_insfl stop start prev fld := end else Vtop. +Definition absdiff := binop_int + (fun i1 i2 => ExtValues.int_absdiff i1 i2). + +Definition absdiffl := binop_long + (fun i1 i2 => ExtValues.long_absdiff i1 i2). + Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with | Omove, v1::nil => v1 @@ -308,6 +314,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osel c ty, v1::v2::vc::nil => select (eval_static_condition0 c vc) v1 v2 | Oselimm c imm, v1::vc::nil => select (eval_static_condition0 c vc) v1 (I imm) | Osellimm c imm, v1::vc::nil => select (eval_static_condition0 c vc) v1 (L imm) + | Oabsdiff, v1::v2::nil => absdiff v1 v2 + | (Oabsdiffimm n2), v1::nil => absdiff v1 (I n2) + | Oabsdiffl, v1::v2::nil => absdiffl v1 v2 + | (Oabsdifflimm n2), v1::nil => absdiffl v1 (L n2) | _, _ => Vbot end. @@ -319,6 +329,26 @@ Hypothesis GENV: genv_match bc ge. Variable sp: block. Hypothesis STACK: bc sp = BCstack. +Lemma absdiff_sound: + forall v x w y + (vMATCH : vmatch bc v x) + (wMATCH : vmatch bc w y), + vmatch bc (ExtValues.absdiff v w) (absdiff x y). +Proof. + intros. + apply binop_int_sound; trivial. +Qed. + +Lemma absdiffl_sound: + forall v x w y + (vMATCH : vmatch bc v x) + (wMATCH : vmatch bc w y), + vmatch bc (ExtValues.absdiffl v w) (absdiffl x y). +Proof. + intros. + apply binop_long_sound; trivial. +Qed. + Lemma minf_sound: forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minf v w) (minf x y). Proof. @@ -593,6 +623,11 @@ Proof. - apply select_sound; auto with va. eapply eval_static_condition0_sound; eauto. (* select long imm *) - apply select_sound; auto with va. eapply eval_static_condition0_sound; eauto. + (* Oabsdiff *) + - apply absdiff_sound; auto with va. + - apply absdiff_sound; auto with va. + - apply absdiffl_sound; auto with va. + - apply absdiffl_sound; auto with va. Qed. End SOUNDNESS. |