diff options
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asm.v | 1 | ||||
-rw-r--r-- | mppa_k1c/Asmvliw.v | 9 | ||||
-rw-r--r-- | mppa_k1c/ExtValues.v | 57 | ||||
-rw-r--r-- | mppa_k1c/Op.v | 26 | ||||
-rw-r--r-- | mppa_k1c/SelectLongproof.v | 10 | ||||
-rw-r--r-- | mppa_k1c/SelectOpproof.v | 9 | ||||
-rw-r--r-- | mppa_k1c/ValueAOp.v | 10 |
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. |