From 295058286407ec6c4182f2b12b27608fc7d28f95 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 May 2019 23:53:02 +0200 Subject: use shift 1-4 in backend --- mppa_k1c/ExtValues.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'mppa_k1c/ExtValues.v') diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 5d16b79c..1aa17458 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -2,6 +2,20 @@ Require Import Coqlib. Require Import Integers. Require Import Values. +Inductive shift1_4 : Type := +| SHIFT1 | SHIFT2 | SHIFT3 | SHIFT4. + +Definition z_of_shift1_4 (x : shift1_4) := + match x with + | SHIFT1 => 1 + | SHIFT2 => 2 + | SHIFT3 => 3 + | SHIFT4 => 4 + end. + +Definition int_of_shift1_4 (x : shift1_4) := + Int.repr (z_of_shift1_4 x). + Definition is_bitfield stop start := (Z.leb start stop) && (Z.geb start Z.zero) -- cgit From ae22df3c5ef0a60527ea85b83bb71e8c95a6ab9c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 May 2019 07:59:11 +0200 Subject: Pmsub compiled --- mppa_k1c/ExtValues.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'mppa_k1c/ExtValues.v') diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 1aa17458..0d56fd1c 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -131,3 +131,19 @@ Definition val_shrxl (v1 v2: val): val := else Vundef | _, _ => Vundef end. + +Lemma sub_add_neg : + forall x y, Val.sub x y = Val.add x (Val.neg y). +Proof. + destruct x; destruct y; simpl; trivial. + f_equal. + apply Int.sub_add_opp. +Qed. + +Lemma neg_mul_distr_r : + forall x y, Val.neg (Val.mul x y) = Val.mul x (Val.neg y). +Proof. + destruct x; destruct y; simpl; trivial. + f_equal. + apply Int.neg_mul_distr_r. +Qed. \ No newline at end of file -- cgit From 3ef3e6c78026cc1d5793ccb4e905a0232ec7bb4e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 May 2019 10:21:59 +0200 Subject: generate multiply-sub long --- mppa_k1c/ExtValues.v | 33 ++++++++++++++++++++++++++++++++- 1 file changed, 32 insertions(+), 1 deletion(-) (limited to 'mppa_k1c/ExtValues.v') diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 0d56fd1c..735d5c3c 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -146,4 +146,35 @@ Proof. destruct x; destruct y; simpl; trivial. f_equal. apply Int.neg_mul_distr_r. -Qed. \ No newline at end of file +Qed. + +(* pointer diff +Lemma sub_addl_negl : + forall x y, Val.subl x y = Val.addl x (Val.negl y). +Proof. + destruct x; destruct y; simpl; trivial. + + f_equal. apply Int64.sub_add_opp. + + destruct (Archi.ptr64) eqn:ARCHI64; trivial. + f_equal. rewrite Ptrofs.sub_add_opp. + pose (Ptrofs.agree64_neg ARCHI64 (Ptrofs.of_int64 i0) i0) as Hagree. + unfold Ptrofs.agree64 in Hagree. + unfold Ptrofs.add. + f_equal. f_equal. + rewrite Hagree. + pose (Ptrofs.agree64_of_int ARCHI64 (Int64.neg i0)) as Hagree2. + rewrite Hagree2. + reflexivity. + exact (Ptrofs.agree64_of_int ARCHI64 i0). + + destruct (Archi.ptr64) eqn:ARCHI64; simpl; trivial. + destruct (eq_block _ _); simpl; trivial. +Qed. + *) + +Lemma negl_mull_distr_r : + forall x y, Val.negl (Val.mull x y) = Val.mull x (Val.negl y). +Proof. + destruct x; destruct y; simpl; trivial. + f_equal. + apply Int64.neg_mul_distr_r. +Qed. + -- cgit From 2c428ad4e0177756db2f6dfe56831b5a44f6de5c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 May 2019 15:20:02 +0200 Subject: add with shift, beginning --- mppa_k1c/ExtValues.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) (limited to 'mppa_k1c/ExtValues.v') diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 735d5c3c..32d84b60 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -13,6 +13,28 @@ Definition z_of_shift1_4 (x : shift1_4) := | SHIFT4 => 4 end. +Definition shift1_4_of_z (x : Z) := + if Z.eq_dec x 1 then Some SHIFT1 + else if Z.eq_dec x 2 then Some SHIFT2 + else if Z.eq_dec x 3 then Some SHIFT3 + else if Z.eq_dec x 4 then Some SHIFT4 + else None. + +Lemma shift1_4_of_z_correct : + forall z, + match shift1_4_of_z z with + | Some x => z_of_shift1_4 x = z + | None => True + end. +Proof. + intro. unfold shift1_4_of_z. + destruct (Z.eq_dec _ _); simpl; try congruence. + destruct (Z.eq_dec _ _); simpl; try congruence. + destruct (Z.eq_dec _ _); simpl; try congruence. + destruct (Z.eq_dec _ _); simpl; try congruence. + trivial. +Qed. + Definition int_of_shift1_4 (x : shift1_4) := Int.repr (z_of_shift1_4 x). @@ -178,3 +200,5 @@ Proof. apply Int64.neg_mul_distr_r. Qed. +Definition addx sh v1 v2 := + Val.add v2 (Val.shl v1 (Vint sh)). \ No newline at end of file -- cgit From 17a8d91a82f67d7f62f8cbad41ba76a4b0b82a30 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 May 2019 20:17:09 +0200 Subject: apply .xs onto addx4 etc --- mppa_k1c/ExtValues.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'mppa_k1c/ExtValues.v') diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 32d84b60..284d55f3 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -201,4 +201,7 @@ Proof. Qed. Definition addx sh v1 v2 := - Val.add v2 (Val.shl v1 (Vint sh)). \ No newline at end of file + Val.add v2 (Val.shl v1 (Vint sh)). + +Definition addxl sh v1 v2 := + Val.addl v2 (Val.shll v1 (Vint sh)). \ No newline at end of file -- cgit From 644814b1b266f5492e6ffd24776fc87c30acd57b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 12 May 2019 12:41:49 +0200 Subject: standardize semantics, 1 --- mppa_k1c/ExtValues.v | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'mppa_k1c/ExtValues.v') diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 284d55f3..9169cf13 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -204,4 +204,10 @@ Definition addx sh v1 v2 := Val.add v2 (Val.shl v1 (Vint sh)). Definition addxl sh v1 v2 := - Val.addl v2 (Val.shll v1 (Vint sh)). \ No newline at end of file + Val.addl v2 (Val.shll v1 (Vint sh)). + +Definition revsubx sh v1 v2 := + Val.sub v2 (Val.shl v1 (Vint sh)). + +Definition revsubxl sh v1 v2 := + Val.subl v2 (Val.shll v1 (Vint sh)). \ No newline at end of file -- cgit