aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asm.v8
-rw-r--r--mppa_k1c/Asmblockdeps.v4
-rw-r--r--mppa_k1c/Asmvliw.v8
-rw-r--r--mppa_k1c/ExtValues.v18
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml14
-rw-r--r--mppa_k1c/TargetPrinter.ml8
-rw-r--r--test/monniaux/bitfields/bitfields.c10
7 files changed, 65 insertions, 5 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index f1ccc126..53747851 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -189,6 +189,7 @@ Inductive instruction : Type :=
| Pandnw (rd rs1 rs2: ireg) (**r andn word *)
| Pornw (rd rs1 rs2: ireg) (**r orn word *)
| Psraw (rd rs1 rs2: ireg) (**r shift right arithmetic word *)
+ | Psrxw (rd rs1 rs2: ireg) (**r shift right arithmetic word round to 0*)
| Psrlw (rd rs1 rs2: ireg) (**r shift right logical word *)
| Psllw (rd rs1 rs2: ireg) (**r shift left logical word *)
| Pmaddw (rd rs1 rs2: ireg) (**r multiply-add words *)
@@ -207,6 +208,7 @@ Inductive instruction : Type :=
| Pslll (rd rs1 rs2: ireg) (**r shift left logical long *)
| Psrll (rd rs1 rs2: ireg) (**r shift right logical long *)
| Psral (rd rs1 rs2: ireg) (**r shift right arithmetic long *)
+ | Psrxl (rd rs1 rs2: ireg) (**r shift right arithmetic long round to 0*)
| Pmaddl (rd rs1 rs2: ireg) (**r multiply-add long *)
| Pfaddd (rd rs1 rs2: ireg) (**r Float addition double *)
@@ -230,11 +232,13 @@ Inductive instruction : Type :=
| Pandniw (rd rs: ireg) (imm: int) (**r andn imm word *)
| Porniw (rd rs: ireg) (imm: int) (**r orn imm word *)
| Psraiw (rd rs: ireg) (imm: int) (**r shift right arithmetic imm word *)
+ | Psrxiw (rd rs: ireg) (imm: int) (**r shift right arithmetic imm word round to 0*)
| Psrliw (rd rs: ireg) (imm: int) (**r shift right logical imm word *)
| Pslliw (rd rs: ireg) (imm: int) (**r shift left logical imm word *)
| Proriw (rd rs: ireg) (imm: int) (**r rotate right imm word *)
| Pmaddiw (rd rs: ireg) (imm: int) (**r multiply add imm word *)
| Psllil (rd rs: ireg) (imm: int) (**r shift left logical immediate long *)
+ | Psrxil (rd rs: ireg) (imm: int) (**r shift right arithmetic imm word round to 0*)
| Psrlil (rd rs: ireg) (imm: int) (**r shift right logical immediate long *)
| Psrail (rd rs: ireg) (imm: int) (**r shift right arithmetic immediate long *)
@@ -343,6 +347,7 @@ Definition basic_to_instruction (b: basic) :=
| PArithRRR Asmvliw.Pandnw rd rs1 rs2 => Pandnw rd rs1 rs2
| PArithRRR Asmvliw.Pornw rd rs1 rs2 => Pornw rd rs1 rs2
| PArithRRR Asmvliw.Psraw rd rs1 rs2 => Psraw rd rs1 rs2
+ | PArithRRR Asmvliw.Psrxw rd rs1 rs2 => Psrxw rd rs1 rs2
| PArithRRR Asmvliw.Psrlw rd rs1 rs2 => Psrlw rd rs1 rs2
| PArithRRR Asmvliw.Psllw rd rs1 rs2 => Psllw rd rs1 rs2
@@ -360,6 +365,7 @@ Definition basic_to_instruction (b: basic) :=
| PArithRRR Asmvliw.Pslll rd rs1 rs2 => Pslll rd rs1 rs2
| PArithRRR Asmvliw.Psrll rd rs1 rs2 => Psrll rd rs1 rs2
| PArithRRR Asmvliw.Psral rd rs1 rs2 => Psral rd rs1 rs2
+ | PArithRRR Asmvliw.Psrxl rd rs1 rs2 => Psrxl rd rs1 rs2
| PArithRRR Asmvliw.Pfaddd rd rs1 rs2 => Pfaddd rd rs1 rs2
| PArithRRR Asmvliw.Pfaddw rd rs1 rs2 => Pfaddw rd rs1 rs2
@@ -381,11 +387,13 @@ Definition basic_to_instruction (b: basic) :=
| PArithRRI32 Asmvliw.Pandniw rd rs imm => Pandniw rd rs imm
| PArithRRI32 Asmvliw.Porniw rd rs imm => Porniw rd rs imm
| PArithRRI32 Asmvliw.Psraiw rd rs imm => Psraiw rd rs imm
+ | PArithRRI32 Asmvliw.Psrxiw rd rs imm => Psrxiw rd rs imm
| PArithRRI32 Asmvliw.Psrliw rd rs imm => Psrliw rd rs imm
| PArithRRI32 Asmvliw.Pslliw rd rs imm => Pslliw rd rs imm
| PArithRRI32 Asmvliw.Proriw rd rs imm => Proriw rd rs imm
| PArithRRI32 Asmvliw.Psllil rd rs imm => Psllil rd rs imm
| PArithRRI32 Asmvliw.Psrlil rd rs imm => Psrlil rd rs imm
+ | PArithRRI32 Asmvliw.Psrxil rd rs imm => Psrxil rd rs imm
| PArithRRI32 Asmvliw.Psrail rd rs imm => Psrail rd rs imm
(* RRI64 *)
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 8fccdd99..ff625bdd 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1287,6 +1287,7 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring :=
| Pornw => "Pornw"
| Psraw => "Psraw"
| Psrlw => "Psrlw"
+ | Psrxw => "Psrxw"
| Psllw => "Psllw"
| Paddl => "Paddl"
| Psubl => "Psubl"
@@ -1301,6 +1302,7 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring :=
| Pmull => "Pmull"
| Pslll => "Pslll"
| Psrll => "Psrll"
+ | Psrxl => "Psrxl"
| Psral => "Psral"
| Pfaddd => "Pfaddd"
| Pfaddw => "Pfaddw"
@@ -1325,11 +1327,13 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring :=
| Porniw => "Porniw"
| Psraiw => "Psraiw"
| Psrliw => "Psrliw"
+ | Psrxiw => "Psrxiw"
| Pslliw => "Pslliw"
| Proriw => "Proriw"
| Psllil => "Psllil"
| Psrlil => "Psrlil"
| Psrail => "Psrail"
+ | Psrxil => "Psrxil"
end.
Definition string_of_name_rri64 (n: arith_name_rri64): pstring :=
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 0427d93c..3f2179c2 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -367,6 +367,7 @@ Inductive arith_name_rrr : Type :=
| Pandnw (**r andn word *)
| Pornw (**r orn word *)
| Psraw (**r shift right arithmetic word *)
+ | Psrxw (**r shift right arithmetic word round to 0*)
| Psrlw (**r shift right logical word *)
| Psllw (**r shift left logical word *)
@@ -383,6 +384,7 @@ Inductive arith_name_rrr : Type :=
| Pmull (**r mul long (low part) *)
| Pslll (**r shift left logical long *)
| Psrll (**r shift right logical long *)
+ | Psrxl (**r shift right logical long round to 0*)
| Psral (**r shift right arithmetic long *)
| Pfaddd (**r float add double *)
@@ -407,12 +409,14 @@ Inductive arith_name_rri32 : Type :=
| Pandniw (**r andn word *)
| Porniw (**r orn word *)
| Psraiw (**r shift right arithmetic imm word *)
+ | Psrxiw (**r shift right arithmetic imm word round to 0*)
| Psrliw (**r shift right logical imm word *)
| Pslliw (**r shift left logical imm word *)
| Proriw (**r rotate right imm word *)
| Psllil (**r shift left logical immediate long *)
| Psrlil (**r shift right logical immediate long *)
| Psrail (**r shift right arithmetic immediate long *)
+ | Psrxil (**r shift right arithmetic immediate long round to 0*)
.
Inductive arith_name_rri64 : Type :=
@@ -956,6 +960,7 @@ Definition arith_eval_rrr n v1 v2 :=
| Psrlw => Val.shru v1 v2
| Psraw => Val.shr v1 v2
| Psllw => Val.shl v1 v2
+ | Psrxw => ExtValues.val_shrx v1 v2
| Paddl => Val.addl v1 v2
| Psubl => Val.subl v1 v2
@@ -971,6 +976,7 @@ Definition arith_eval_rrr n v1 v2 :=
| Pslll => Val.shll v1 v2
| Psrll => Val.shrlu v1 v2
| Psral => Val.shrl v1 v2
+ | Psrxl => ExtValues.val_shrxl v1 v2
| Pfaddd => Val.addf v1 v2
| Pfaddw => Val.addfs v1 v2
@@ -994,10 +1000,12 @@ Definition arith_eval_rri32 n v i :=
| Pandniw => Val.and (Val.notint v) (Vint i)
| Porniw => Val.or (Val.notint v) (Vint i)
| Psraiw => Val.shr v (Vint i)
+ | Psrxiw => ExtValues.val_shrx v (Vint i)
| Psrliw => Val.shru v (Vint i)
| Pslliw => Val.shl v (Vint i)
| Proriw => Val.ror v (Vint i)
| Psllil => Val.shll v (Vint i)
+ | Psrxil => ExtValues.val_shrxl v (Vint i)
| Psrlil => Val.shrlu v (Vint i)
| Psrail => Val.shrl v (Vint i)
end.
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
index fe8ce203..5d16b79c 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -99,3 +99,21 @@ Definition int_highest_bit (x : int) : Z :=
Definition int64_highest_bit (x : int64) : Z :=
highest_bit (Int64.unsigned x) (63%nat).
+
+Definition val_shrx (v1 v2: val): val :=
+ match v1, v2 with
+ | Vint n1, Vint n2 =>
+ if Int.ltu n2 (Int.repr 31)
+ then Vint(Int.shrx n1 n2)
+ else Vundef
+ | _, _ => Vundef
+ end.
+
+Definition val_shrxl (v1 v2: val): val :=
+ match v1, v2 with
+ | Vlong n1, Vint n2 =>
+ if Int.ltu n2 (Int.repr 63)
+ then Vlong(Int64.shrx' n1 n2)
+ else Vundef
+ | _, _ => Vundef
+ end.
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 7a9e683d..5f016e53 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -75,6 +75,7 @@ let arith_rrr_str = function
| Pornw -> "Pornw"
| Psraw -> "Psraw"
| Psrlw -> "Psrlw"
+ | Psrxw -> "Psrxw"
| Psllw -> "Psllw"
| Paddl -> "Paddl"
| Psubl -> "Psubl"
@@ -89,6 +90,7 @@ let arith_rrr_str = function
| Pmull -> "Pmull"
| Pslll -> "Pslll"
| Psrll -> "Psrll"
+ | Psrxl -> "Psrxl"
| Psral -> "Psral"
| Pfaddd -> "Pfaddd"
| Pfaddw -> "Pfaddw"
@@ -110,12 +112,14 @@ let arith_rri32_str = function
| Pandniw -> "Pandniw"
| Porniw -> "Porniw"
| Psraiw -> "Psraiw"
+ | Psrxiw -> "Psrxiw"
| Psrliw -> "Psrliw"
| Pslliw -> "Pslliw"
| Proriw -> "Proriw"
| Psllil -> "Psllil"
| Psrlil -> "Psrlil"
| Psrail -> "Psrail"
+ | Psrxil -> "Psrxil"
let arith_rri64_str = function
| Pcompil it -> "Pcompil"
@@ -432,8 +436,8 @@ let lsu_data_y : int array = let resmap = fun r -> match r with
type real_instruction =
(* ALU *)
- | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Rorw | Xorw
- | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Xord
+ | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Srsw | Rorw | Xorw
+ | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Srsd | Xord
| Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd
| Maddw | Maddd | Cmoved
| Make | Nop | Extfz | Extfs | Insf
@@ -580,7 +584,7 @@ let rec_to_usage r =
| Some U27L5 | Some U27L10 -> mau_x
| Some E27U27L10 -> mau_y)
| Nop -> alu_nop
- | Sraw | Srlw | Sllw | Srad | Srld | Slld -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding)
+ | Sraw | Srlw | Srsw | Sllw | Srad | Srld | Slld | Srsd -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding)
(* TODO: check *)
| Rorw -> (match encoding with None | Some U6 -> alu_lite | _ -> raise InvalidEncoding)
| Extfz | Extfs | Insf -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding)
@@ -601,11 +605,11 @@ let rec_to_usage r =
let real_inst_to_latency = function
| Nop -> 0 (* Only goes through ID *)
- | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw
+ | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srsw | Srlw | Sllw | Xorw
(* TODO check rorw *)
| Rorw | Nandw | Norw | Nxorw | Ornw | Andnw
| Nandd | Nord | Nxord | Ornd | Andnd
- | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make
+ | Addd | Andd | Compd | Ord | Sbfd | Srad | Srsd | Srld | Slld | Xord | Make
| Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved
-> 1
| Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 99c89804..8e8efefc 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -471,6 +471,8 @@ module Target (*: TARGET*) =
fprintf oc " ornw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
| Psraw (rd, rs1, rs2) ->
fprintf oc " sraw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+ | Psrxw (rd, rs1, rs2) ->
+ fprintf oc " srsw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
| Psrlw (rd, rs1, rs2) ->
fprintf oc " srlw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
| Psllw (rd, rs1, rs2) ->
@@ -504,6 +506,8 @@ module Target (*: TARGET*) =
fprintf oc " slld %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
| Psrll (rd, rs1, rs2) ->
fprintf oc " srld %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+ | Psrxl (rd, rs1, rs2) ->
+ fprintf oc " srsd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
| Psral (rd, rs1, rs2) ->
fprintf oc " srad %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
| Pmaddl (rd, rs1, rs2) ->
@@ -547,6 +551,8 @@ module Target (*: TARGET*) =
fprintf oc " ornw %a = %a, %a\n" ireg rd ireg rs coqint imm
| Psraiw (rd, rs, imm) ->
fprintf oc " sraw %a = %a, %a\n" ireg rd ireg rs coqint imm
+ | Psrxiw (rd, rs, imm) ->
+ fprintf oc " srsw %a = %a, %a\n" ireg rd ireg rs coqint imm
| Psrliw (rd, rs, imm) ->
fprintf oc " srlw %a = %a, %a\n" ireg rd ireg rs coqint imm
| Pslliw (rd, rs, imm) ->
@@ -562,6 +568,8 @@ module Target (*: TARGET*) =
fprintf oc " srld %a = %a, %a\n" ireg rd ireg rs coqint64 imm
| Psrail (rd, rs, imm) ->
fprintf oc " srad %a = %a, %a\n" ireg rd ireg rs coqint64 imm
+ | Psrxil (rd, rs, imm) ->
+ fprintf oc " srsd %a = %a, %a\n" ireg rd ireg rs coqint64 imm
(* Arith RRI64 instructions *)
| Pcompil (it, rd, rs, imm) ->
diff --git a/test/monniaux/bitfields/bitfields.c b/test/monniaux/bitfields/bitfields.c
index f9e84399..16ad5a61 100644
--- a/test/monniaux/bitfields/bitfields.c
+++ b/test/monniaux/bitfields/bitfields.c
@@ -4,8 +4,18 @@ struct fields {
unsigned f0 : 3;
unsigned f1 : 5;
signed f2 : 3;
+ unsigned toto1: 16;
+ unsigned toto2: 16;
};
+unsigned get_toto1(struct fields x) {
+ return x.toto1;
+}
+
+unsigned get_toto2(struct fields x) {
+ return x.toto2;
+}
+
int get_f1(struct fields x) {
return x.f1;
}
generated by cgit (git 2.34.1) at 2024-07-14 01:36:45 +0000