From 59089e5d11428dd224b3239bc7f5db602df9b177 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 24 Apr 2019 22:20:13 +0200
Subject: begin bitfields

---
 common/Values.v                      | 15 +++++++++++++++
 mppa_k1c/Asm.v                       |  3 +++
 mppa_k1c/Asmblockdeps.v              |  1 +
 mppa_k1c/Asmvliw.v                   |  5 ++++-
 mppa_k1c/PostpassSchedulingOracle.ml |  1 +
 mppa_k1c/TargetPrinter.ml            |  2 ++
 6 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/common/Values.v b/common/Values.v
index a20dd567..ae8d31f3 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -766,6 +766,21 @@ Definition rolml (v: val) (amount: int) (mask: int64): val :=
   | _ => Vundef
   end.
 
+
+Definition extfz stop start v :=
+  if (Int.cmp Cle start stop)
+       && (Int.cmp Cge start Int.zero)
+       && (Int.cmp Clt stop Int.iwordsize)
+  then
+    let stop' := Int.add stop Int.one in
+    match v with
+    | Vint w =>
+      Vint (Int.shr (Int.shl w (Int.sub Int.iwordsize stop')) (Int.sub Int.iwordsize (Int.sub stop' start)))
+    | _ => Vundef
+    end
+  else Vundef.
+
+
 (** Comparisons *)
 
 Section COMPARISONS.
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index f679335c..2c3eef1f 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -129,6 +129,8 @@ Inductive instruction : Type :=
   | Pcvtl2w (rd rs: ireg)                           (**r Convert Long to Word *)
   | Psxwd   (rd rs: ireg)                           (**r Sign Extend Word to Double Word *)
   | Pzxwd   (rd rs: ireg)                           (**r Zero Extend Word to Double Word *)
+
+  | Pextfz  (rd : ireg) (rs : ireg) (stop : int) (start : int) (**r extract bitfields unsigned *)
   | Pfabsd  (rd rs: ireg)                           (**r float absolute double *)
   | Pfabsw  (rd rs: ireg)                           (**r float absolute word *)
   | Pfnegd  (rd rs: ireg)                           (**r float negate double *)
@@ -280,6 +282,7 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRR Asmvliw.Pcvtl2w rd rs => Pcvtl2w rd rs
   | PArithRR Asmvliw.Psxwd rd rs  => Psxwd rd rs
   | PArithRR Asmvliw.Pzxwd rd rs  => Pzxwd rd rs
+  | PArithRR (Asmvliw.Pextfz stop start) rd rs => Pextfz rd rs stop start
   | PArithRR Asmvliw.Pfabsd rd rs => Pfabsd rd rs
   | PArithRR Asmvliw.Pfabsw rd rs => Pfabsw rd rs
   | PArithRR Asmvliw.Pfnegd rd rs  => Pfnegd rd rs
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 4559dd62..b9db7760 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1213,6 +1213,7 @@ Definition string_of_name_rr (n: arith_name_rr): pstring :=
   | Pcvtl2w => "Pcvtl2w"
   | Psxwd => "Psxwd"
   | Pzxwd => "Pzxwd"
+  | Pextfz _ _ => "Pextfz"
   | Pfabsd => "Pfabsd"
   | Pfabsw => "Pfabsw"
   | Pfnegd => "Pfnegd"
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 7177d5fe..a347b6fc 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -306,7 +306,9 @@ Inductive arith_name_rr : Type :=
   | Pcvtl2w                                         (**r Convert Long to Word *)
   | Psxwd                                           (**r Sign Extend Word to Double Word *)
   | Pzxwd                                           (**r Zero Extend Word to Double Word *)
-
+(*  | Pextfs (stop : int) (start : int)               (**r extract bit field, signed *) *)
+  | Pextfz (stop : int) (start : int)               (**r extract bit field, unsigned *)
+           
   | Pfabsd                                          (**r float absolute double *)
   | Pfabsw                                          (**r float absolute word *)
   | Pfnegd                                          (**r float negate double *)
@@ -878,6 +880,7 @@ 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
   | Pfnegd => Val.negf v
   | Pfnegw => Val.negfs v
   | Pfabsd => Val.absf v
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 9a26425a..8f6484d6 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -34,6 +34,7 @@ let arith_rr_str = function
   | Pnegl -> "Pnegl"
   | Psxwd -> "Psxwd"
   | Pzxwd -> "Pzxwd"
+  | Pextfz(_,_) -> "Pextfz"
   | Pfabsw -> "Pfabsw"
   | Pfabsd -> "Pfabsd"
   | Pfnegw -> "Pfnegw"
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 5aedd557..dc207dc8 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -377,6 +377,8 @@ module Target (*: TARGET*) =
          fprintf oc "	sxwd	%a = %a\n" ireg rd ireg rs
       | Pzxwd(rd, rs) ->
          fprintf oc "	zxwd	%a = %a\n" ireg rd ireg rs
+      | Pextfz(rd, rs, stop, start) ->
+         fprintf oc "	extfz	%a = %a, %ld, %ld\n" ireg rd ireg rs (camlint_of_coqint stop) (camlint_of_coqint start)
       | Pfabsd(rd, rs) ->
          fprintf oc "	fabsd	%a = %a\n" ireg rd ireg rs
       | Pfabsw(rd, rs) ->
-- 
cgit