diff options
author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-14 15:48:43 +0100 |
---|---|---|
committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-14 15:48:43 +0100 |
commit | f6686d81092ccaaf3a22b4e34aecc7c5895b08ba (patch) | |
tree | 9d61868c2ad5e0ed20329512d9508280da1e4c70 /kvx/ExtValues.v | |
parent | b7aea86a0c6ace274e585fddfd0d88d13528cc90 (diff) | |
download | compcert-kvx-f6686d81092ccaaf3a22b4e34aecc7c5895b08ba.tar.gz compcert-kvx-f6686d81092ccaaf3a22b4e34aecc7c5895b08ba.zip |
begin adding abdw abdd
Diffstat (limited to 'kvx/ExtValues.v')
-rw-r--r-- | kvx/ExtValues.v | 79 |
1 files changed, 74 insertions, 5 deletions
diff --git a/kvx/ExtValues.v b/kvx/ExtValues.v index b4e14898..434d283e 100644 --- a/kvx/ExtValues.v +++ b/kvx/ExtValues.v @@ -21,14 +21,14 @@ Require Import Lia. Open Scope Z_scope. -Definition abs_diff (x y : Z) := Z.abs (x - y). -Definition abs_diff2 (x y : Z) := +Definition int_abs_diff (x y : Z) := Z.abs (x - y). +Definition int_abs_diff2 (x y : Z) := if x <=? y then y - x else x - y. -Lemma abs_diff2_correct : - forall x y : Z, (abs_diff x y) = (abs_diff2 x y). +Lemma int_abs_diff2_correct : + forall x y : Z, (int_abs_diff x y) = (int_abs_diff2 x y). Proof. intros. - unfold abs_diff, abs_diff2. + unfold int_abs_diff, int_abs_diff2. unfold Z.leb. pose proof (Z.compare_spec x y) as Hspec. inv Hspec. @@ -754,3 +754,72 @@ Definition fmaddfs := triple_op_single (fun f1 f2 f3 => Float32.fma f2 f3 f1). Definition fmsubf := triple_op_float (fun f1 f2 f3 => Float.fma (Float.neg f2) f3 f1). Definition fmsubfs := triple_op_single (fun f1 f2 f3 => Float32.fma (Float32.neg f2) f3 f1). + +Definition double_op_intZ f v1 v2 := + match v1, v2 with + | (Vint i1), (Vint i2) => Vint (Int.repr (f (Int.signed i1) (Int.signed i2))) + | _, _ => Vundef + end. + +Definition double_op_longZ f v1 v2 := + match v1, v2 with + | (Vlong i1), (Vlong i2) => Vlong (Int64.repr (f (Int64.signed i1) (Int64.signed i2))) + | _, _ => Vundef + end. + +Definition absdiff := double_op_intZ int_abs_diff. +Definition absdiffl := double_op_longZ int_abs_diff. + +Definition abs v1 := + match v1 with + | Vint x => Vint (Int.repr (Z.abs (Int.signed x))) + | _ => Vundef + end. + +Definition absl v1 := + match v1 with + | Vlong x => Vlong (Int64.repr (Z.abs (Int64.signed x))) + | _ => Vundef + end. + +Lemma absdiff_zero_correct: + forall v, abs v = absdiff v (Vint Int.zero). +Proof. + intro. destruct v; cbn; try reflexivity. + f_equal. unfold int_abs_diff. + change (Int.unsigned Int.zero) with 0%Z. + rewrite Z.sub_0_r. + reflexivity. +Qed. + +Lemma absdiffl_zero_correct: + forall v, absl v = absdiffl v (Vlong Int64.zero). +Proof. + intro. destruct v; cbn; try reflexivity. + f_equal. unfold int_abs_diff. + change (Int64.unsigned Int64.zero) with 0%Z. + rewrite Z.sub_0_r. + reflexivity. +Qed. + +Remark absdiff_inject: + forall f v1 v1' v2 v2' + (INJ1 : Val.inject f v1 v1') + (INJ2 : Val.inject f v2 v2'), + Val.inject f (absdiff v1 v2) (absdiff v1' v2'). +Proof. + intros. + inv INJ1; cbn; try constructor. + inv INJ2; cbn; constructor. +Qed. + +Remark absdiffl_inject: + forall f v1 v1' v2 v2' + (INJ1 : Val.inject f v1 v1') + (INJ2 : Val.inject f v2 v2'), + Val.inject f (absdiffl v1 v2) (absdiffl v1' v2'). +Proof. + intros. + inv INJ1; cbn; try constructor. + inv INJ2; cbn; constructor. +Qed. |