From f6686d81092ccaaf3a22b4e34aecc7c5895b08ba Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 14 Feb 2022 15:48:43 +0100 Subject: begin adding abdw abdd --- kvx/ValueAOp.v | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) (limited to 'kvx/ValueAOp.v') diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v index 87554258..f0fed567 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 => Int.repr (ExtValues.int_abs_diff (Int.signed i1) (Int.signed i2))). + +Definition absdiffl := binop_long + (fun i1 i2 => Int64.repr (ExtValues.int_abs_diff (Int64.signed i1) (Int64.signed 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. -- cgit From ed6e20995761614ee7ea6235b978a463f071c123 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 14 Feb 2022 17:49:40 +0100 Subject: abs builtins --- kvx/ValueAOp.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kvx/ValueAOp.v') diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v index f0fed567..ddfe94f3 100644 --- a/kvx/ValueAOp.v +++ b/kvx/ValueAOp.v @@ -157,10 +157,10 @@ Definition eval_static_insfl stop start prev fld := else Vtop. Definition absdiff := binop_int - (fun i1 i2 => Int.repr (ExtValues.int_abs_diff (Int.signed i1) (Int.signed i2))). + (fun i1 i2 => ExtValues.int_absdiff i1 i2). Definition absdiffl := binop_long - (fun i1 i2 => Int64.repr (ExtValues.int_abs_diff (Int64.signed i1) (Int64.signed i2))). + (fun i1 i2 => ExtValues.long_absdiff i1 i2). Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with -- cgit