diff options
-rw-r--r-- | mppa_k1c/ExtValues.v | 26 | ||||
-rw-r--r-- | mppa_k1c/Op.v | 16 | ||||
-rw-r--r-- | mppa_k1c/SelectLong.vp | 9 | ||||
-rw-r--r-- | mppa_k1c/SelectLongproof.v | 4 | ||||
-rw-r--r-- | mppa_k1c/SelectOp.vp | 9 | ||||
-rw-r--r-- | mppa_k1c/SelectOpproof.v | 4 | ||||
-rw-r--r-- | mppa_k1c/ValueAOp.v | 24 | ||||
-rwxr-xr-x | mppa_k1c/bitmasks.py | 12 |
8 files changed, 52 insertions, 52 deletions
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index d1329583..97e48eb7 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -2,10 +2,13 @@ Require Import Coqlib. Require Import Integers. Require Import Values. +Definition is_bitfield stop start := + (Z.leb start stop) + && (Z.geb start Z.zero) + && (Z.ltb stop Int.zwordsize). + Definition extfz stop start v := - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int.zwordsize) + if is_bitfield stop start then let stop' := Z.add stop Z.one in match v with @@ -17,9 +20,7 @@ Definition extfz stop start v := Definition extfs stop start v := - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int.zwordsize) + if is_bitfield stop start then let stop' := Z.add stop Z.one in match v with @@ -29,10 +30,13 @@ Definition extfs stop start v := end else Vundef. +Definition is_bitfieldl stop start := + (Z.leb start stop) + && (Z.geb start Z.zero) + && (Z.ltb stop Int64.zwordsize). + Definition extfzl stop start v := - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int64.zwordsize) + if is_bitfieldl stop start then let stop' := Z.add stop Z.one in match v with @@ -44,9 +48,7 @@ Definition extfzl stop start v := Definition extfsl stop start v := - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int64.zwordsize) + if is_bitfieldl stop start then let stop' := Z.add stop Z.one in match v with diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index d3e4270e..2836f7cf 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -975,22 +975,22 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). destruct (Val.cmp_different_blocks _); simpl; trivial. (* extfz *) - unfold extfz. - destruct (_ && _ && _). + destruct (is_bitfield _ _). + destruct v0; simpl; trivial. + constructor. (* extfs *) - unfold extfs. - destruct (_ && _ && _). + destruct (is_bitfield _ _). + destruct v0; simpl; trivial. + constructor. (* extfzl *) - unfold extfzl. - destruct (_ && _ && _). + destruct (is_bitfieldl _ _). + destruct v0; simpl; trivial. + constructor. (* extfsl *) - unfold extfsl. - destruct (_ && _ && _). + destruct (is_bitfieldl _ _). + destruct v0; simpl; trivial. + constructor. Qed. @@ -1605,25 +1605,25 @@ Proof. (* extfz *) - unfold extfz. - destruct (_ && _ && _). + destruct (is_bitfield _ _). + inv H4; trivial. + trivial. (* extfs *) - unfold extfs. - destruct (_ && _ && _). + destruct (is_bitfield _ _). + inv H4; trivial. + trivial. (* extfzl *) - unfold extfzl. - destruct (_ && _ && _). + destruct (is_bitfieldl _ _). + inv H4; trivial. + trivial. (* extfsl *) - unfold extfsl. - destruct (_ && _ && _). + destruct (is_bitfieldl _ _). + inv H4; trivial. + trivial. Qed. diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 90901e04..a2bc0587 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -23,6 +23,7 @@ Require Import AST Integers Floats. Require Import Op CminorSel. Require Import OpHelpers. Require Import SelectOp SplitLong. +Require Import ExtValues. Local Open Scope cminorsel_scope. Local Open Scope string_scope. @@ -158,9 +159,7 @@ Nondetfunction shrluimm (e1: expr) (n: int) := | Eop (Oshllimm n1) (t1:::Enil) => let stop := Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one) in let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int64.zwordsize in - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int64.zwordsize) + if is_bitfieldl stop start then Eop (Oextfzl stop start) (t1:::Enil) else Eop (Oshrluimm n) (e1:::Enil) | _ => @@ -183,9 +182,7 @@ Nondetfunction shrlimm (e1: expr) (n: int) := | Eop (Oshllimm n1) (t1:::Enil) => let stop := Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one) in let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int64.zwordsize in - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int64.zwordsize) + if is_bitfieldl stop start then Eop (Oextfsl stop start) (t1:::Enil) else Eop (Oshrlimm n) (e1:::Enil) | _ => diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 17d9d2ec..b3cb1ce0 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -251,7 +251,7 @@ Proof. - subst x. simpl negb. cbn iota. - destruct (_ && _ && _) eqn:BOUNDS. + destruct (is_bitfieldl _ _) eqn:BOUNDS. + exists (extfzl (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) (Z.sub (Z.add @@ -303,7 +303,7 @@ Proof. - subst x. simpl negb. cbn iota. - destruct (_ && _ && _) eqn:BOUNDS. + destruct (is_bitfieldl _ _) eqn:BOUNDS. + exists (extfsl (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) (Z.sub (Z.add diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 6bb5ee56..aad6249a 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -51,6 +51,7 @@ Require Import Floats. Require Import Op. Require Import CminorSel. Require Import OpHelpers. +Require Import ExtValues. Local Open Scope cminorsel_scope. @@ -189,9 +190,7 @@ Nondetfunction shruimm (e1: expr) (n: int) := | Eop (Oshlimm n1) (t1:::Enil) => let stop := Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one) in let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int.zwordsize in - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int.zwordsize) + if is_bitfield stop start then Eop (Oextfz stop start) (t1:::Enil) else Eop (Oshruimm n) (e1:::Enil) | _ => @@ -213,9 +212,7 @@ Nondetfunction shrimm (e1: expr) (n: int) := | Eop (Oshlimm n1) (t1:::Enil) => let stop := Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one) in let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int.zwordsize in - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int.zwordsize) + if is_bitfield stop start then Eop (Oextfs stop start) (t1:::Enil) else Eop (Oshrimm n) (e1:::Enil) | _ => diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index b23e2aa8..cc362eb7 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -311,7 +311,7 @@ Proof. - subst x. simpl negb. cbn iota. - destruct (_ && _ && _) eqn:BOUNDS. + destruct (is_bitfield _ _) eqn:BOUNDS. + exists (extfz (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) (Z.sub (Z.add @@ -368,7 +368,7 @@ Proof. - subst x. simpl negb. cbn iota. - destruct (_ && _ && _) eqn:BOUNDS. + destruct (is_bitfield _ _) eqn:BOUNDS. + exists (extfs (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) (Z.sub (Z.add diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index dfd2b78c..b7bd6ec9 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -76,9 +76,7 @@ Definition eval_static_selectfs (cond : condition0) (v0 v1 vselect : aval) : ava Definition eval_static_extfs (stop : Z) (start : Z) (v : aval) := - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int.zwordsize) + if is_bitfield stop start then let stop' := Z.add stop Z.one in match v with @@ -89,9 +87,7 @@ Definition eval_static_extfs (stop : Z) (start : Z) (v : aval) := else Vtop. Definition eval_static_extfz (stop : Z) (start : Z) (v : aval) := - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int.zwordsize) + if is_bitfield stop start then let stop' := Z.add stop Z.one in match v with @@ -102,9 +98,7 @@ Definition eval_static_extfz (stop : Z) (start : Z) (v : aval) := else Vtop. Definition eval_static_extfsl (stop : Z) (start : Z) (v : aval) := - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int64.zwordsize) + if is_bitfieldl stop start then let stop' := Z.add stop Z.one in match v with @@ -115,9 +109,7 @@ Definition eval_static_extfsl (stop : Z) (start : Z) (v : aval) := else Vtop. Definition eval_static_extfzl (stop : Z) (start : Z) (v : aval) := - if (Z.leb start stop) - && (Z.geb start Z.zero) - && (Z.ltb stop Int64.zwordsize) + if is_bitfieldl stop start then let stop' := Z.add stop Z.one in match v with @@ -387,25 +379,25 @@ Proof. (* extfz *) - unfold extfz, eval_static_extfz. - destruct (_ && _ && _). + destruct (is_bitfield _ _). + inv H1; constructor. + constructor. (* extfs *) - unfold extfs, eval_static_extfs. - destruct (_ && _ && _). + destruct (is_bitfield _ _). + inv H1; constructor. + constructor. (* extfzl *) - unfold extfzl, eval_static_extfzl. - destruct (_ && _ && _). + destruct (is_bitfieldl _ _). + inv H1; constructor. + constructor. (* extfsl *) - unfold extfsl, eval_static_extfsl. - destruct (_ && _ && _). + destruct (is_bitfieldl _ _). + inv H1; constructor. + constructor. Qed. diff --git a/mppa_k1c/bitmasks.py b/mppa_k1c/bitmasks.py new file mode 100755 index 00000000..9f6987d6 --- /dev/null +++ b/mppa_k1c/bitmasks.py @@ -0,0 +1,12 @@ +#!/usr/bin/env python3 +def bitmask(to, fr): + bit_to = 1<<to + return (bit_to | (bit_to - 1)) & ~((1<<fr)-1) + +def bitmask2(to, fr): + bit_to = 1<<to + return bit_to + (bit_to - (1 << fr)) + +for stop in range(32): + for start in range(stop+1): + assert(bitmask(stop, start) == bitmask2(stop, start)) |