aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
diff options
context:
space:
mode:
Diffstat (limited to 'mppa_k1c')
-rw-r--r--mppa_k1c/Asm.v1
-rw-r--r--mppa_k1c/Asmvliw.v9
-rw-r--r--mppa_k1c/ExtValues.v57
-rw-r--r--mppa_k1c/Op.v26
-rw-r--r--mppa_k1c/SelectLongproof.v10
-rw-r--r--mppa_k1c/SelectOpproof.v9
-rw-r--r--mppa_k1c/ValueAOp.v10
7 files changed, 91 insertions, 31 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index ec67d703..609bf93e 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -23,6 +23,7 @@ Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
+Require Import ExtValues.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 3c308960..6442cecc 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -25,6 +25,7 @@ Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
+Require Import ExtValues.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
@@ -883,10 +884,10 @@ Definition arith_eval_rr n v :=
| Pcvtl2w => Val.loword v
| Psxwd => Val.longofint v
| Pzxwd => Val.longofintu v
- | Pextfz stop start => Val.extfz stop start v
- | Pextfs stop start => Val.extfs stop start v
- | Pextfzl stop start => Val.extfzl stop start v
- | Pextfsl stop start => Val.extfsl stop start v
+ | Pextfz stop start => extfz stop start v
+ | Pextfs stop start => extfs stop start v
+ | Pextfzl stop start => extfzl stop start v
+ | Pextfsl stop start => extfsl stop start v
| Pfnegd => Val.negf v
| Pfnegw => Val.negfs v
| Pfabsd => Val.absf v
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
new file mode 100644
index 00000000..d1329583
--- /dev/null
+++ b/mppa_k1c/ExtValues.v
@@ -0,0 +1,57 @@
+Require Import Coqlib.
+Require Import Integers.
+Require Import Values.
+
+Definition extfz stop start v :=
+ if (Z.leb start stop)
+ && (Z.geb start Z.zero)
+ && (Z.ltb stop Int.zwordsize)
+ then
+ let stop' := Z.add stop Z.one in
+ match v with
+ | Vint w =>
+ Vint (Int.shru (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start))))
+ | _ => Vundef
+ end
+ else Vundef.
+
+
+Definition extfs stop start v :=
+ if (Z.leb start stop)
+ && (Z.geb start Z.zero)
+ && (Z.ltb stop Int.zwordsize)
+ then
+ let stop' := Z.add stop Z.one in
+ match v with
+ | Vint w =>
+ Vint (Int.shr (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start))))
+ | _ => Vundef
+ end
+ else Vundef.
+
+Definition extfzl stop start v :=
+ if (Z.leb start stop)
+ && (Z.geb start Z.zero)
+ && (Z.ltb stop Int64.zwordsize)
+ then
+ let stop' := Z.add stop Z.one in
+ match v with
+ | Vlong w =>
+ Vlong (Int64.shru' (Int64.shl' w (Int.repr (Z.sub Int64.zwordsize stop'))) (Int.repr (Z.sub Int64.zwordsize (Z.sub stop' start))))
+ | _ => Vundef
+ end
+ else Vundef.
+
+
+Definition extfsl stop start v :=
+ if (Z.leb start stop)
+ && (Z.geb start Z.zero)
+ && (Z.ltb stop Int64.zwordsize)
+ then
+ let stop' := Z.add stop Z.one in
+ match v with
+ | Vlong w =>
+ Vlong (Int64.shr' (Int64.shl' w (Int.repr (Z.sub Int64.zwordsize stop'))) (Int.repr (Z.sub Int64.zwordsize (Z.sub stop' start))))
+ | _ => Vundef
+ end
+ else Vundef.
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 99625f5c..d3e4270e 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -31,7 +31,7 @@
Require Import BoolEqual Coqlib.
Require Import AST Integers Floats.
-Require Import Values Memory Globalenvs Events.
+Require Import Values ExtValues Memory Globalenvs Events.
Set Implicit Arguments.
@@ -502,10 +502,10 @@ Definition eval_operation
| (Oselectl cond), v0::v1::vselect::nil => Some (eval_selectl cond v0 v1 vselect m)
| (Oselectf cond), v0::v1::vselect::nil => Some (eval_selectf cond v0 v1 vselect m)
| (Oselectfs cond), v0::v1::vselect::nil => Some (eval_selectfs cond v0 v1 vselect m)
- | (Oextfz stop start), v0::nil => Some (Val.extfz stop start v0)
- | (Oextfs stop start), v0::nil => Some (Val.extfs stop start v0)
- | (Oextfzl stop start), v0::nil => Some (Val.extfzl stop start v0)
- | (Oextfsl stop start), v0::nil => Some (Val.extfsl stop start v0)
+ | (Oextfz stop start), v0::nil => Some (extfz stop start v0)
+ | (Oextfs stop start), v0::nil => Some (extfs stop start v0)
+ | (Oextfzl stop start), v0::nil => Some (extfzl stop start v0)
+ | (Oextfsl stop start), v0::nil => Some (extfsl stop start v0)
| _, _ => None
end.
@@ -974,22 +974,22 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
destruct (_ && _); simpl; trivial.
destruct (Val.cmp_different_blocks _); simpl; trivial.
(* extfz *)
- - unfold Val.extfz.
+ - unfold extfz.
destruct (_ && _ && _).
+ destruct v0; simpl; trivial.
+ constructor.
(* extfs *)
- - unfold Val.extfs.
+ - unfold extfs.
destruct (_ && _ && _).
+ destruct v0; simpl; trivial.
+ constructor.
(* extfzl *)
- - unfold Val.extfzl.
+ - unfold extfzl.
destruct (_ && _ && _).
+ destruct v0; simpl; trivial.
+ constructor.
(* extfsl *)
- - unfold Val.extfsl.
+ - unfold extfsl.
destruct (_ && _ && _).
+ destruct v0; simpl; trivial.
+ constructor.
@@ -1604,25 +1604,25 @@ Proof.
* rewrite Hcond'. constructor.
(* extfz *)
- - unfold Val.extfz.
+ - unfold extfz.
destruct (_ && _ && _).
+ inv H4; trivial.
+ trivial.
(* extfs *)
- - unfold Val.extfs.
+ - unfold extfs.
destruct (_ && _ && _).
+ inv H4; trivial.
+ trivial.
(* extfzl *)
- - unfold Val.extfzl.
+ - unfold extfzl.
destruct (_ && _ && _).
+ inv H4; trivial.
+ trivial.
(* extfsl *)
- - unfold Val.extfsl.
+ - unfold extfsl.
destruct (_ && _ && _).
+ inv H4; trivial.
+ trivial.
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 451bded7..17d9d2ec 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -19,7 +19,7 @@
Require Import String Coqlib Maps Integers Floats Errors.
Require Archi.
-Require Import AST Values Memory Globalenvs Events.
+Require Import AST Values ExtValues Memory Globalenvs Events.
Require Import Cminor Op CminorSel.
Require Import OpHelpers OpHelpersproof.
Require Import SelectOp SelectOpproof SplitLong SplitLongproof.
@@ -252,14 +252,14 @@ Proof.
simpl negb.
cbn iota.
destruct (_ && _ && _) eqn:BOUNDS.
- + exists (Val.extfzl (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one))
+ + exists (extfzl (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one))
(Z.sub
(Z.add
(Z.add (Int.unsigned n) (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)))
Z.one) Int64.zwordsize) v1).
split.
++ EvalOp.
- ++ unfold Val.extfzl.
+ ++ unfold extfzl.
rewrite BOUNDS.
destruct v1; try (simpl; apply Val.lessdef_undef).
replace (Z.sub Int64.zwordsize
@@ -304,14 +304,14 @@ Proof.
simpl negb.
cbn iota.
destruct (_ && _ && _) eqn:BOUNDS.
- + exists (Val.extfsl (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one))
+ + exists (extfsl (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one))
(Z.sub
(Z.add
(Z.add (Int.unsigned n) (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)))
Z.one) Int64.zwordsize) v1).
split.
++ EvalOp.
- ++ unfold Val.extfsl.
+ ++ unfold extfsl.
rewrite BOUNDS.
destruct v1; try (simpl; apply Val.lessdef_undef).
replace (Z.sub Int64.zwordsize
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 4df87bea..b23e2aa8 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -23,6 +23,7 @@ Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
+Require Import ExtValues.
Require Import Memory.
Require Import Globalenvs.
Require Import Cminor.
@@ -311,14 +312,14 @@ Proof.
simpl negb.
cbn iota.
destruct (_ && _ && _) eqn:BOUNDS.
- + exists (Val.extfz (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))
+ + exists (extfz (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))
(Z.sub
(Z.add
(Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)))
Z.one) Int.zwordsize) v1).
split.
++ EvalOp.
- ++ unfold Val.extfz.
+ ++ unfold extfz.
rewrite BOUNDS.
destruct v1; try (simpl; apply Val.lessdef_undef).
replace (Z.sub Int.zwordsize
@@ -368,14 +369,14 @@ Proof.
simpl negb.
cbn iota.
destruct (_ && _ && _) eqn:BOUNDS.
- + exists (Val.extfs (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))
+ + exists (extfs (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))
(Z.sub
(Z.add
(Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)))
Z.one) Int.zwordsize) v1).
split.
++ EvalOp.
- ++ unfold Val.extfs.
+ ++ unfold extfs.
rewrite BOUNDS.
destruct v1; try (simpl; apply Val.lessdef_undef).
replace (Z.sub Int.zwordsize
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index e9269213..dfd2b78c 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -12,7 +12,7 @@
Require Import Coqlib Compopts.
Require Import AST Integers Floats Values Memory Globalenvs.
-Require Import Op RTL ValueDomain.
+Require Import Op ExtValues RTL ValueDomain.
(** Value analysis for RISC V operators *)
@@ -386,25 +386,25 @@ Proof.
constructor.
(* extfz *)
- - unfold Val.extfz, eval_static_extfz.
+ - unfold extfz, eval_static_extfz.
destruct (_ && _ && _).
+ inv H1; constructor.
+ constructor.
(* extfs *)
- - unfold Val.extfs, eval_static_extfs.
+ - unfold extfs, eval_static_extfs.
destruct (_ && _ && _).
+ inv H1; constructor.
+ constructor.
(* extfzl *)
- - unfold Val.extfzl, eval_static_extfzl.
+ - unfold extfzl, eval_static_extfzl.
destruct (_ && _ && _).
+ inv H1; constructor.
+ constructor.
(* extfsl *)
- - unfold Val.extfsl, eval_static_extfsl.
+ - unfold extfsl, eval_static_extfsl.
destruct (_ && _ && _).
+ inv H1; constructor.
+ constructor.
generated by cgit (git 2.34.1) at 2024-07-14 05:17:17 +0000