factor expressions into single file

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))