summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mips/hgen/ast.hgen6
-rw-r--r--mips/hgen/fold.hgen5
-rw-r--r--mips/hgen/lexer.hgen4
-rw-r--r--mips/hgen/map.hgen4
-rw-r--r--mips/hgen/parser.hgen8
-rw-r--r--mips/hgen/pretty.hgen9
-rw-r--r--mips/hgen/sail_trans_out.hgen4
-rw-r--r--mips/hgen/token_types.hgen11
-rw-r--r--mips/hgen/tokens.hgen4
-rw-r--r--mips/hgen/trans_sail.hgen8
-rw-r--r--mips/hgen/types.hgen1
-rw-r--r--mips/hgen/types_sail_trans_out.hgen2
-rw-r--r--mips/hgen/types_trans_sail.hgen2
-rw-r--r--mips/mips_regfp.sail6
14 files changed, 65 insertions, 9 deletions
diff --git a/mips/hgen/ast.hgen b/mips/hgen/ast.hgen
index c9a39bbf..1e70d949 100644
--- a/mips/hgen/ast.hgen
+++ b/mips/hgen/ast.hgen
@@ -10,4 +10,8 @@
| `MIPSLSLR of bool * bool * bool * reg * reg * bit16 (* store, double, left, base, rt, offset *)
| `MIPSSYNC
| `MIPSBEQ of reg * reg * bit16 * bool * bool (* rs, rt, offset, not equal, likely *)
-| `MIPSBCMPZ of reg * bit16 * mipsCmp * bool * bool (* rs, offset, cmp, link, likely *)
+| `MIPSBCMPZ of reg * bit16 * mipsCmp * bool * bool (* rs, offset, cmp, link, likely *)
+| `MIPSJ of bit26
+| `MIPSJAL of bit26
+| `MIPSJR of reg
+| `MIPSJALR of reg * reg (* rs, rd *)
diff --git a/mips/hgen/fold.hgen b/mips/hgen/fold.hgen
index 08b6cc16..fb2f6de2 100644
--- a/mips/hgen/fold.hgen
+++ b/mips/hgen/fold.hgen
@@ -11,3 +11,8 @@
| `MIPSSYNC -> (y_reg, y_sreg)
| `MIPSBEQ (rs, rt, offset, ne, likely) -> fold_reg rs (fold_reg rt (y_reg, y_sreg))
| `MIPSBCMPZ (rs, offset, cmp, link, likely) -> fold_reg rs (y_reg, y_sreg)
+| `MIPSJ (offset) -> (y_reg, y_sreg)
+| `MIPSJAL (offset) -> fold_reg (IReg(R31)) (y_reg, y_sreg)
+| `MIPSJR (rd) -> fold_reg rd (y_reg, y_sreg)
+| `MIPSJALR (rd, rs) -> fold_reg rd (fold_reg rs (y_reg, y_sreg))
+
diff --git a/mips/hgen/lexer.hgen b/mips/hgen/lexer.hgen
index 17e72450..c01b14cc 100644
--- a/mips/hgen/lexer.hgen
+++ b/mips/hgen/lexer.hgen
@@ -110,3 +110,7 @@
"blez", BCMPZ {txt="BCMPZ"; cmp=MIPS_LE; likely=false; link=false };
"blezl", BCMPZ {txt="BCMPZ"; cmp=MIPS_LE; likely=true; link=false };
+"j", J {txt="J"};
+"jal", JAL {txt="JAL"};
+"jr", JR {txt="JR"};
+"jalr", JALR {txt="JALR"};
diff --git a/mips/hgen/map.hgen b/mips/hgen/map.hgen
index 68c9e46a..5c6cde6a 100644
--- a/mips/hgen/map.hgen
+++ b/mips/hgen/map.hgen
@@ -11,4 +11,8 @@
| `MIPSSYNC -> `MIPSSYNC
| `MIPSBEQ (rs, rt, offset, ne, likely) -> `MIPSBEQ (map_reg rs, map_reg rt, offset, ne, likely)
| `MIPSBCMPZ (rs, offset, cmp, link, likely) -> `MIPSBCMPZ (map_reg rs, offset, cmp, link, likely)
+| `MIPSJ (offset) -> `MIPSJ (offset)
+| `MIPSJAL (offset) -> `MIPSJAL (offset) (* implicit R31? *)
+| `MIPSJR (rd) -> `MIPSJR (map_reg rd)
+| `MIPSJALR (rd, rs) -> `MIPSJALR(map_reg rd, map_reg rs)
diff --git a/mips/hgen/parser.hgen b/mips/hgen/parser.hgen
index bf15ab1e..1e18c01c 100644
--- a/mips/hgen/parser.hgen
+++ b/mips/hgen/parser.hgen
@@ -24,3 +24,11 @@
{ `MIPSBEQ ( $2, $4, $6, $1.ne, $1.likely) }
| BCMPZ ARCH_REG COMMA NUM
{ `MIPSBCMPZ ( $2, $4, $1.cmp, $1.link, $1.likely) }
+| J NUM
+ { `MIPSJ ($2) }
+| JAL NUM
+ { `MIPSJAL ($2) }
+| JR ARCH_REG
+ { `MIPSJR ($2) }
+| JALR ARCH_REG COMMA ARCH_REG
+ { `MIPSJALR ($2, $4) }
diff --git a/mips/hgen/pretty.hgen b/mips/hgen/pretty.hgen
index 43c41bb8..d9b94def 100644
--- a/mips/hgen/pretty.hgen
+++ b/mips/hgen/pretty.hgen
@@ -25,3 +25,12 @@
sprintf "%s, %s, %s, .%+d" (pp_beq_op ne likely) (pp_reg rs) (pp_reg rt) offset
| `MIPSBCMPZ (rs, offset, cmp, link, likely) ->
sprintf "%s, %s, .%+d" (pp_bcmpz_op cmp link likely) (pp_reg rs) offset
+| `MIPSJ (offset) ->
+ sprintf "j %d" offset
+| `MIPSJAL (offset) ->
+ sprintf "jal %d" offset
+| `MIPSJR(rd) ->
+ sprintf "jr %s" (pp_reg rd)
+| `MIPSJALR(rd, rs) ->
+ sprintf "jalr %s, %s" (pp_reg rd) (pp_reg rs)
+
diff --git a/mips/hgen/sail_trans_out.hgen b/mips/hgen/sail_trans_out.hgen
index 5ecad705..2911137e 100644
--- a/mips/hgen/sail_trans_out.hgen
+++ b/mips/hgen/sail_trans_out.hgen
@@ -90,4 +90,8 @@
| "SYNC", [] -> `MIPSSYNC
| "BEQ", [rs; rt; offset; ne; likely] -> `MIPSBEQ ((translate_out_ireg rs), (translate_out_ireg rt), (translate_out_imm16 offset), (translate_out_bool ne), (translate_out_bool likely))
| "BCMPZ", [rs; offset; cmp; link; likely] -> `MIPSBCMPZ ((translate_out_ireg rs), (translate_out_imm16 offset), (translate_out_cmp cmp), (translate_out_bool link), (translate_out_bool likely))
+| "J", [offset] -> `MIPSJ (translate_out_imm26 offset)
+| "JAL", [offset] -> `MIPSJAL (translate_out_imm26 offset)
+| "JR", [rd] -> `MIPSJR (translate_out_ireg rd)
+| "JALR", [rd; rs] -> `MIPSJALR (translate_out_ireg rd, translate_out_ireg rs)
diff --git a/mips/hgen/token_types.hgen b/mips/hgen/token_types.hgen
index 2c2df1a6..170b42d3 100644
--- a/mips/hgen/token_types.hgen
+++ b/mips/hgen/token_types.hgen
@@ -11,14 +11,12 @@ type token_LSLR = {txt : string; store : bool; double : bool; left: bool } (*
type token_SYNC = {txt : string}
type token_BEQ = {txt : string; ne : bool; likely : bool }
type token_BCMPZ = {txt : string; cmp : mipsCmp; likely : bool; link : bool }
-
+type token_J = {txt : string}
+type token_JAL = {txt : string}
+type token_JR = {txt : string}
+type token_JALR = {txt : string}
(*
-(bit[26]) J
-(bit[26]) JAL
(regno, imm16, Comparison) TRAPIMM
-(regno, imm16, Comparison, bool, bool) BCMPZ
-
-(regno, regno) JALR
(regno, regno) RDHWR
(regno, regno, Comparison) TRAPREG
@@ -29,7 +27,6 @@ TLBP
TLBR
TLBWI
TLBWR
-regno JR
regregimm16 CACHE
regregimm16 PREF
diff --git a/mips/hgen/tokens.hgen b/mips/hgen/tokens.hgen
index 00b99e8e..937c6354 100644
--- a/mips/hgen/tokens.hgen
+++ b/mips/hgen/tokens.hgen
@@ -11,3 +11,7 @@
%token <MIPSHGenBase.token_SYNC> SYNC
%token <MIPSHGenBase.token_BEQ> BEQ
%token <MIPSHGenBase.token_BCMPZ> BCMPZ
+%token <MIPSHGenBase.token_J> J
+%token <MIPSHGenBase.token_JAL> JAL
+%token <MIPSHGenBase.token_JR> JR
+%token <MIPSHGenBase.token_JALR> JALR
diff --git a/mips/hgen/trans_sail.hgen b/mips/hgen/trans_sail.hgen
index 5dcecfd2..4b7c7882 100644
--- a/mips/hgen/trans_sail.hgen
+++ b/mips/hgen/trans_sail.hgen
@@ -110,3 +110,11 @@
translate_bool "link" link;
translate_bool "likely" likely;
], [])
+| `MIPSJ (offset) ->
+ ("J", [translate_imm26 "offset" offset;], [])
+| `MIPSJAL (offset) ->
+ ("JAL", [translate_imm26 "offset" offset;], [])
+| `MIPSJR(rd) ->
+ ("JR", [translate_reg "rd" rd;], [])
+| `MIPSJALR(rd, rs) ->
+ ("JALR", [translate_reg "rd" rd; translate_reg "rs" rs;], [])
diff --git a/mips/hgen/types.hgen b/mips/hgen/types.hgen
index ba576e06..e544902e 100644
--- a/mips/hgen/types.hgen
+++ b/mips/hgen/types.hgen
@@ -36,6 +36,7 @@ let pp_rtype_op = function
| MIPSROpSUBU -> "SUBU"
| MIPSROpXOR -> "XOR"
+type bit26 = int
type bit16 = int
type bit5 = int
diff --git a/mips/hgen/types_sail_trans_out.hgen b/mips/hgen/types_sail_trans_out.hgen
index c48c4b6f..392c33f3 100644
--- a/mips/hgen/types_sail_trans_out.hgen
+++ b/mips/hgen/types_sail_trans_out.hgen
@@ -6,6 +6,8 @@ let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst))
let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg))
+let translate_out_imm26 imm = translate_out_int imm
+
let translate_out_imm16 imm = translate_out_int imm
let translate_out_imm5 imm = translate_out_int imm
diff --git a/mips/hgen/types_trans_sail.hgen b/mips/hgen/types_trans_sail.hgen
index 111cc3fd..303ef43c 100644
--- a/mips/hgen/types_trans_sail.hgen
+++ b/mips/hgen/types_trans_sail.hgen
@@ -1,5 +1,7 @@
let translate_reg name value =
(name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int (reg_to_int value)))
+let translate_imm26 name value =
+ (name, Bvector (Some 26), bit_list_of_integer 26 (Nat_big_num.of_int value))
let translate_imm16 name value =
(name, Bvector (Some 16), bit_list_of_integer 16 (Nat_big_num.of_int value))
let translate_imm5 name value =
diff --git a/mips/mips_regfp.sail b/mips/mips_regfp.sail
index ca781d23..6cfa3230 100644
--- a/mips/mips_regfp.sail
+++ b/mips/mips_regfp.sail
@@ -355,22 +355,26 @@ function (regfps,regfps,regfps,nias,dia,instruction_kind) initial_analysis (inst
case (J(offset)) -> {
(* XXX actually unconditional jump *)
ik := IK_cond_branch;
- (* Nias := XXX *)
+ Dia := DIA_concrete((PC + 4)[63..28] : offset : 0b00);
}
case (JAL(offset)) -> {
(* XXX actually unconditional jump *)
ik := IK_cond_branch;
oR := RFull("GPR31") :: oR;
+ Dia := DIA_concrete((PC + 4)[63..28] : offset : 0b00);
}
case (JR(rs)) -> {
(* XXX actually unconditional jump *)
ik := IK_cond_branch;
iR := RFull(GPRs[rs]) :: iR;
+ Dia := DIA_reg(RFull(GPRs[rs]));
}
case (JALR(rs, rd)) -> {
+ (* XXX actually unconditional jump *)
ik := IK_cond_branch;
iR := RFull(GPRs[rs]) :: iR;
oR := RFull("GPR31") :: oR;
+ Dia := DIA_reg(RFull(GPRs[rs]));
}
case (BEQ(rs, rd, imm, ne, likely)) -> {
ik := IK_cond_branch;
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 15:30:32 +0000