start of extfzl/extfsl

7 files changed, 50 insertions, 6 deletions

diff --git a/common/Values.v b/common/Values.v
index 059a72d9..45774913 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -794,6 +794,33 @@ Definition extfs stop start v :=
     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 (Int64.repr (Z.sub Int64.zwordsize stop'))) (Int64.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 (Int64.repr (Z.sub Int64.zwordsize stop'))) (Int64.repr (Z.sub Int64.zwordsize (Z.sub stop' start))))
+    | _ => Vundef
+    end
+  else Vundef.
+
 
 (** Comparisons *)
 
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 1e1f6e36..ec67d703 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -133,6 +133,9 @@ Inductive instruction : Type :=
   | Pextfz  (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields unsigned *)

   | Pextfs  (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields signed *)

 

+  | Pextfzl  (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields unsigned *)

+  | Pextfsl  (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields signed *)

+

   | Pfabsd  (rd rs: ireg)                           (**r float absolute double *)

   | Pfabsw  (rd rs: ireg)                           (**r float absolute word *)

   | Pfnegd  (rd rs: ireg)                           (**r float negate double *)

@@ -286,6 +289,8 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRR Asmvliw.Pzxwd rd rs  => Pzxwd rd rs

   | PArithRR (Asmvliw.Pextfz stop start) rd rs => Pextfz rd rs stop start

   | PArithRR (Asmvliw.Pextfs stop start) rd rs => Pextfs rd rs stop start

+  | PArithRR (Asmvliw.Pextfzl stop start) rd rs => Pextfzl rd rs stop start

+  | PArithRR (Asmvliw.Pextfsl stop start) rd rs => Pextfsl 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 b3a72517..a1a11701 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1215,6 +1215,8 @@ Definition string_of_name_rr (n: arith_name_rr): pstring :=
   | Pzxwd => "Pzxwd"
   | Pextfz _ _ => "Pextfz"
   | Pextfs _ _ => "Pextfs"
+  | Pextfzl _ _ => "Pextfzl"
+  | Pextfsl _ _ => "Pextfsl"
   | Pfabsd => "Pfabsd"
   | Pfabsw => "Pfabsw"
   | Pfnegd => "Pfnegd"
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 13ff5422..3c308960 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -309,6 +309,8 @@ Inductive arith_name_rr : Type :=
 (*  | Pextfs (stop : int) (start : int)               (**r extract bit field, signed *) *)
   | Pextfz (stop : Z) (start : Z)               (**r extract bit field, unsigned *)
   | Pextfs (stop : Z) (start : Z)               (**r extract bit field, signed *)
+  | Pextfzl (stop : Z) (start : Z)              (**r extract bit field, unsigned *)
+  | Pextfsl (stop : Z) (start : Z)              (**r extract bit field, signed *)
            
   | Pfabsd                                          (**r float absolute double *)
   | Pfabsw                                          (**r float absolute word *)
@@ -883,6 +885,8 @@ Definition arith_eval_rr n 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
   | 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 87f34ee6..b9344116 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -36,6 +36,8 @@ let arith_rr_str = function
   | Pzxwd -> "Pzxwd"
   | Pextfz(_,_) -> "Pextfz"
   | Pextfs(_,_) -> "Pextfs"
+  | Pextfzl(_,_) -> "Pextfzl"
+  | Pextfsl(_,_) -> "Pextfsl"
   | Pfabsw -> "Pfabsw"
   | Pfabsd -> "Pfabsd"
   | Pfnegw -> "Pfnegw"
@@ -476,10 +478,8 @@ let ab_inst_to_real = function
   | "Pmaddl" -> Maddd
   | "Pmake" | "Pmakel" | "Pmakefs" | "Pmakef" | "Ploadsymbol" -> Make
   | "Pnop" | "Pcvtw2l" -> Nop
-  | "Psxwd" -> Extfs
-  | "Pzxwd" -> Extfz
-  | "Pextfz" -> Extfz
-  | "Pextfs" -> Extfs
+  | "Pextfz" | "Pextfzl" | "Pzxwd" -> Extfz
+  | "Pextfs" | "Pextfsl" | "Psxwd" -> Extfs
   | "Pfnarrowdw" -> Fnarrowdw
   | "Pfwidenlwd" -> Fwidenlwd
   | "Pfloatwrnsz" -> Floatwz
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 8826e6a2..f986db39 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -377,9 +377,9 @@ 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) ->
+      | Pextfz(rd, rs, stop, start) | Pextfzl(rd, rs, stop, start) ->
          fprintf oc "	extfz	%a = %a, %ld, %ld\n" ireg rd ireg rs (camlint_of_coqint stop) (camlint_of_coqint start)
-      | Pextfs(rd, rs, stop, start) ->
+      | Pextfs(rd, rs, stop, start) | Pextfsl(rd, rs, stop, start) ->
          fprintf oc "	extfs	%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
diff --git a/test/monniaux/bitfields/bitfields.c b/test/monniaux/bitfields/bitfields.c
index 868d7483..f9e84399 100644
--- a/test/monniaux/bitfields/bitfields.c
+++ b/test/monniaux/bitfields/bitfields.c
@@ -14,7 +14,13 @@ int get_f2(struct fields x) {
   return x.f2;
 }
 
+void set_f1(struct fields *x, unsigned v) {
+  x->f1 = v;
+}
+
 int main() {
   struct fields x = {1, 2, -1};
   printf("%d %d\n", get_f1(x), get_f2(x));
+  set_f1(&x, 4);
+  printf("%d %d\n", get_f1(x), get_f2(x));
 }