Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sail

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;