added RISC-V "fence w,w" and "fence.i";

fixed the interpreter nias analysis;

15 files changed, 43 insertions, 12 deletions

diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen
index a0a59e4a..6fd52b03 100644
--- a/risc-v/hgen/ast.hgen
+++ b/risc-v/hgen/ast.hgen
@@ -11,5 +11,6 @@
 | `RISCVSHIFTW of bit5 * reg * reg * riscvSop
 | `RISCVRTYPEW of reg * reg * reg * riscvRopw
 | `RISCVFENCE of bit4 * bit4
+| `RISCVFENCEI
 | `RISCVLoadRes of bool * bool * reg * wordWidth * reg
 | `RISCVStoreCon of bool * bool * reg * reg * wordWidth * reg
diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
index ffea1575..770f9263 100644
--- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
+++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -60,6 +60,7 @@
 | `RISCVFENCE(pred, succ) -> FENCE(
       translate_imm4 "pred" pred,
       translate_imm4 "succ" succ)
+| `RISCVFENCEI -> FENCEI
 | `RISCVLoadRes(aq, rl, rs1, width, rd) -> LOADRES(
       translate_bool "aq" aq,
       translate_bool "rl" rl,
diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen
index abc0ff82..d422e82f 100644
--- a/risc-v/hgen/lexer.hgen
+++ b/risc-v/hgen/lexer.hgen
@@ -75,6 +75,7 @@
 "r",  FENCEOPTION Fence_R;
 "w",  FENCEOPTION Fence_W;
 "rw", FENCEOPTION Fence_RW;
+"fence.i", FENCEI ();
 
 "lr.w",    LOADRES {width=RISCVWORD;   aq=false; rl=false};
 "lr.w.aq", LOADRES {width=RISCVWORD;   aq=true;  rl=false};
diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen
index d077c2df..5b000725 100644
--- a/risc-v/hgen/parser.hgen
+++ b/risc-v/hgen/parser.hgen
@@ -27,13 +27,15 @@
     | (Fence_RW, Fence_RW) -> `RISCVFENCE (0b0011, 0b0011)
     | (Fence_R,  Fence_RW) -> `RISCVFENCE (0b0010, 0b0011)
     | (Fence_RW, Fence_W)  -> `RISCVFENCE (0b0011, 0b0001)
+    | (Fence_W,  Fence_W)  -> `RISCVFENCE (0b0001, 0b0001)
     | (Fence_RW, Fence_R)  -> failwith "'fence rw,r' is not supported"
     | (Fence_R,  Fence_R)  -> failwith "'fence r,r' is not supported"
     | (Fence_R,  Fence_W)  -> failwith "'fence r,w' is not supported"
     | (Fence_W,  Fence_RW) -> failwith "'fence w,rw' is not supported"
     | (Fence_W,  Fence_R)  -> failwith "'fence w,r' is not supported"
-    | (Fence_W,  Fence_W)  -> failwith "'fence w,w' is not supported"
   }
+| FENCEI
+  { `RISCVFENCEI }
 | LOADRES reg COMMA LPAR reg RPAR
   { `RISCVLoadRes($1.aq, $1.rl, $5, $1.width, $2) }
 | STORECON reg COMMA reg COMMA LPAR reg RPAR
diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen
index b4516b16..0b6548ea 100644
--- a/risc-v/hgen/pretty.hgen
+++ b/risc-v/hgen/pretty.hgen
@@ -15,6 +15,7 @@
 | `RISCVSHIFTW(imm, rs, rd, op)   -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm
 | `RISCVRTYPEW(rs2, rs1, rd, op)  -> sprintf "%s %s, %s, %s" (pp_riscv_ropw op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2)
 | `RISCVFENCE(pred, succ)         -> sprintf "fence %s, %s" (pp_riscv_fence_option pred) (pp_riscv_fence_option succ)
+| `RISCVFENCEI                    -> sprintf "fence.i"
 | `RISCVLoadRes(aq, rl, rs1, width, rd)
                                   ->
                                     assert (rl = false);
diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen
index f216180a..61477f43 100644
--- a/risc-v/hgen/sail_trans_out.hgen
+++ b/risc-v/hgen/sail_trans_out.hgen
@@ -14,6 +14,7 @@
 | ("SHIFTW", [imm; rs; rd; op])   -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
 | ("RTYPEW", [rs2; rs1; rd; op])  -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op)
 | ("FENCE", [pred; succ])         -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ)
+| ("FENCEI", [])                  -> `RISCVFENCEI
 | ("LOADRES", [aq; rl; rs1; width; rd])
                                   -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
 | ("STORECON", [aq; rl; rs2; rs1; width; rd])
diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
index 01d8dded..f84ed1fa 100644
--- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
+++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -14,6 +14,7 @@
 | SHIFTW( imm, rs, rd, op)    -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
 | RTYPEW( rs2, rs1, rd, op)   -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op)
 | FENCE( pred, succ)          -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ)
+| FENCEI                      -> `RISCVFENCEI
 | LOADRES( aq, rl, rs1, width, rd)
                               -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
 | STORECON( aq, rl, rs2, rs1, width, rd)
diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen
index c0ef8445..242a7173 100644
--- a/risc-v/hgen/token_types.hgen
+++ b/risc-v/hgen/token_types.hgen
@@ -11,6 +11,7 @@ type token_ADDIW    = unit
 type token_SHIFTW   = {op : riscvSop }
 type token_RTYPEW   = {op : riscvRopw }
 type token_FENCE    = unit
+type token_FENCEI   = unit
 type token_LoadRes  = {width : wordWidth; aq: bool; rl: bool }
 type token_StoreCon = {width : wordWidth; aq: bool; rl: bool }
 
diff --git a/risc-v/hgen/tokens.hgen b/risc-v/hgen/tokens.hgen
index 1276fd68..449be0f0 100644
--- a/risc-v/hgen/tokens.hgen
+++ b/risc-v/hgen/tokens.hgen
@@ -12,5 +12,6 @@
 %token <RISCVHGenBase.token_RTYPEW>   RTYPEW  
 %token <RISCVHGenBase.token_FENCE>    FENCE
 %token <RISCVHGenBase.token_FENCEOPTION> FENCEOPTION
+%token <RISCVHGenBase.token_FENCEI>   FENCEI
 %token <RISCVHGenBase.token_LoadRes>  LOADRES
 %token <RISCVHGenBase.token_StoreCon> STORECON
diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen
index 4d568fe8..6d10471c 100644
--- a/risc-v/hgen/trans_sail.hgen
+++ b/risc-v/hgen/trans_sail.hgen
@@ -112,6 +112,10 @@
      translate_imm4 "succ" succ;
   ], 
   [])
+| `RISCVFENCEI ->
+  ("FENCEI",
+  [],
+  [])
 | `RISCVLoadRes(aq, rl, rs1, width, rd) ->
    ("LOADRES",
     [
diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail
index b5a25578..1d1867c4 100644
--- a/risc-v/riscv.sail
+++ b/risc-v/riscv.sail
@@ -104,6 +104,8 @@ function forall Nat 'n. bool effect { wmv } mem_write_conditional_value( (bit[64
 val extern unit -> unit effect { barr } MEM_fence_rw_rw
 val extern unit -> unit effect { barr } MEM_fence_r_rw
 val extern unit -> unit effect { barr } MEM_fence_rw_w
+val extern unit -> unit effect { barr } MEM_fence_w_w
+val extern unit -> unit effect { barr } MEM_fence_i
 
 (* Ideally these would be sail builtin *)
 function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) =
@@ -337,17 +339,18 @@ function clause execute (FENCE(pred, succ)) = {
     case (0b0011, 0b0011) -> MEM_fence_rw_rw()
     case (0b0010, 0b0011) -> MEM_fence_r_rw()
     case (0b0011, 0b0001) -> MEM_fence_rw_w()
+    case (0b0001, 0b0001) -> MEM_fence_w_w()
     case _ -> not_implemented("unsupported fence")
   }
 }
 
 union ast member unit FENCEI
-function clause decode (0b0000 : 0b0000 : 0b0000 : 0b00000 : 0b001 : 0b00000 : 0b0001111) = Some(FENCEI)
-function clause execute FENCEI = () (* XXX TODO *)
+function clause decode (0b000000000000 : 0b00000 : 0b001 : 0b00000 : 0b0001111) = Some(FENCEI)
+function clause execute FENCEI = MEM_fence_i()
 
 union ast member unit ECALL
 function clause decode (0b000000000000 : 0b00000 : 0b000 : 0b00000 : 0b1110011) = Some(ECALL ())
-function clause execute ECALL = ()
+function clause execute ECALL = not_implemented("ECALL is not implemented")
 
 union ast member unit EBREAK
 function clause decode (0b000000000001 : 0b00000 : 0b000 : 0b00000 : 0b1110011) = Some(EBREAK ())
diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem
index 3803839d..59e3cd4a 100644
--- a/risc-v/riscv_extras.lem
+++ b/risc-v/riscv_extras.lem
@@ -69,4 +69,6 @@ let barrier_functions =
   [ ("MEM_fence_rw_rw", Barrier_RISCV_rw_rw);
     ("MEM_fence_r_rw",  Barrier_RISCV_r_rw);
     ("MEM_fence_rw_w",  Barrier_RISCV_rw_w);
+    ("MEM_fence_w_w",   Barrier_RISCV_w_w);
+    ("MEM_fence_i",     Barrier_RISCV_i);
   ]
diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem
index 35d217ff..6bfc2490 100644
--- a/risc-v/riscv_extras_embed.lem
+++ b/risc-v/riscv_extras_embed.lem
@@ -37,10 +37,14 @@ let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun b -> return (if
 val MEM_fence_rw_rw : unit -> M unit
 val MEM_fence_r_rw  : unit -> M unit
 val MEM_fence_rw_w  : unit -> M unit
+val MEM_fence_w_w   : unit -> M unit
+val MEM_fence_i     : unit -> M unit
 
 let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw
 let MEM_fence_r_rw  () = barrier Barrier_RISCV_r_rw
 let MEM_fence_rw_w  () = barrier Barrier_RISCV_rw_w
+let MEM_fence_w_w   () = barrier Barrier_RISCV_w_w
+let MEM_fence_i     () = barrier Barrier_RISCV_i
 
 let duplicate (bit,len) =
   let bits = repeat [bit] len in
diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem
index 93b5dfec..0fca7709 100644
--- a/risc-v/riscv_extras_embed_sequential.lem
+++ b/risc-v/riscv_extras_embed_sequential.lem
@@ -37,10 +37,14 @@ let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun b -> return (if
 val MEM_fence_rw_rw : unit -> M unit
 val MEM_fence_r_rw  : unit -> M unit
 val MEM_fence_rw_w  : unit -> M unit
+val MEM_fence_w_w   : unit -> M unit
+val MEM_fence_i     : unit -> M unit
 
 let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw
 let MEM_fence_r_rw  () = barrier Barrier_RISCV_r_rw
 let MEM_fence_rw_w  () = barrier Barrier_RISCV_rw_w
+let MEM_fence_w_w   () = barrier Barrier_RISCV_w_w
+let MEM_fence_i     () = barrier Barrier_RISCV_i
 
 let duplicate (bit,len) =
   let bits = repeat [bit] len in
diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail
index 1cfc68d7..20da3da3 100644
--- a/risc-v/riscv_regfp.sail
+++ b/risc-v/riscv_regfp.sail
@@ -29,7 +29,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
             if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR;
             if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
             let (bit[64]) offset = EXTS(imm) in
-            Nias := [|| NIAFP_register (RFull(GPRstr[rs])) ||]; (* XXX this should br rs + offset... *)
+            Nias := [|| NIAFP_register (RFull(GPRstr[rs])) ||];
      }
      case (BTYPE ( imm, rs2, rs1, op)) -> {
             if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR;
@@ -77,13 +77,17 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
             if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
      }
      case (FENCE(pred, succ)) -> {
-          ik :=
-            switch(pred, succ) {
-              case (0b0011, 0b0011) -> IK_barrier (Barrier_RISCV_rw_rw)
-              case (0b0010, 0b0011) -> IK_barrier (Barrier_RISCV_r_rw)
-              case (0b0011, 0b0001) -> IK_barrier (Barrier_RISCV_rw_w)
-              case _ -> exit "not implemented"
-            };
+            ik :=
+              switch(pred, succ) {
+                case (0b0011, 0b0011) -> IK_barrier (Barrier_RISCV_rw_rw)
+                case (0b0010, 0b0011) -> IK_barrier (Barrier_RISCV_r_rw)
+                case (0b0011, 0b0001) -> IK_barrier (Barrier_RISCV_rw_w)
+                case (0b0001, 0b0001) -> IK_barrier (Barrier_RISCV_w_w)
+                case _ -> exit "not implemented"
+              };
+     }
+     case (FENCEI) -> {
+            ik := IK_barrier (Barrier_RISCV_i);
      }
      case (LOADRES ( aq, rl, rs1, width, rd)) -> {
             if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR;