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

18 files changed, 94 insertions, 16 deletions

diff --git a/etc/regfp.sail b/etc/regfp.sail
index 71f53547..776e22af 100644
--- a/etc/regfp.sail
+++ b/etc/regfp.sail
@@ -71,6 +71,8 @@ typedef barrier_kind = enumerate {
   Barrier_RISCV_rw_rw;
   Barrier_RISCV_r_rw;
   Barrier_RISCV_rw_w;
+  Barrier_RISCV_w_w;
+  Barrier_RISCV_i;
 }
 
 typedef trans_kind = enumerate {
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;
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index fda9d5dd..6a9a77a1 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -1267,6 +1267,10 @@ let nias_of_instruction
           else [NIA_successor]
        | _ -> [ NIA_successor ]
        end
+    | ("PPCGEN_ism", s) ->
+        let () = ensure (not unknown_nia_address)
+                  ("unexpected unknown/undefined address in nia_values 4 (\"PPCGEN_ism\", \"" ^ s ^ "\")") in
+        [ NIA_successor ]
 
     (* AARch64 label branch (i.e. address must be known) although
     these instructions take the address as an offset from PC, in here
@@ -1301,7 +1305,10 @@ let nias_of_instruction
                             | (Reg name _ _ _) -> name = n_reg
                             | _ -> false
                             end]
-
+    | ("AArch64HandSail", s) ->
+        let () = ensure (not unknown_nia_address)
+                  ("unexpected unknown/undefined address in nia_values 4 (\"AArch64HandSail\", \"" ^ s ^ "\")") in
+        [ NIA_successor ]
 
     (** hacky cut-and-paste for AArch64Gen, duplicating code just to see if this suffices *)
 
@@ -1334,18 +1341,52 @@ let nias_of_instruction
                             | (Reg name _ _ _) -> name = n_reg
                             | _ -> false
                             end]
+    | ("AArch64GenSail", s) ->
+        let () = ensure (not unknown_nia_address)
+                  ("unexpected unknown/undefined address in nia_values 4 (\"AArch64GenSail\", \"" ^ s ^ "\")") in
+        [ NIA_successor ]
 
     (** end of hacky *)
 
     | ("AArch64LitmusSail", "CtrlDep") -> NIA_successor :: nias
+    | ("AArch64LitmusSail", s) ->
+        let () = ensure (not unknown_nia_address)
+                  ("unexpected unknown/undefined address in nia_values 4 (\"AArch64LitmusSail\", \"" ^ s ^ "\")") in
+        [ NIA_successor ]
 
 
     | ("MIPS_ism", "B") -> fail
+    | ("MIPS_ism", s) ->
+        let () = ensure (not unknown_nia_address)
+                  ("unexpected unknown/undefined address in nia_values 4 (\"MIPS_ism\", \"" ^ s ^ "\")") in
+        [ NIA_successor ]
 
-    | (s1,s2) ->
-       let () = ensure (not unknown_nia_address)
-                       ("unexpected unknown/undefined address in nia_values 4 (\""^s1^"\", \""^s2^"\")") in
+    | ("RISCV_ism", "JAL") -> nias
+    | ("RISCV_ism", "JALR") ->
+        let rs1_integer =
+          match instruction_fields with
+          | [_; (_, _, rs1); _] -> integer_of_bit_list rs1
+          | _ -> fail
+          end
+        in
+        let () = ensure (0 <= rs1_integer && rs1_integer <= 31)
+                  "expected register number from 0 to 31"
+        in
+        if rs1_integer = 0 then nias
+        else
+          let rs1_reg = "x" ^ (String_extra.stringFromInteger rs1_integer) in
+          [NIA_register r | forall (r MEM regs_in)
+                          | match r with
+                            | (Reg name _ _ _) -> name = rs1_reg
+                            | _ -> false
+                            end]
+    | ("RISCV_ism", "BTYPE") -> NIA_successor :: nias
+    | ("RISCV_ism", s) ->
+        let () = ensure (not unknown_nia_address)
+                  ("unexpected unknown/undefined address in nia_values 4 (\"RISCV_ism\", \"" ^ s ^ "\")") in
         [ NIA_successor ]
+
+    | (s1, s2) -> failwith ("unexpected (thread_ism, instruction_name): (" ^ s1 ^ ", " ^ s2 ^ ")")
     end
 
 let interp_instruction_analysis 
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index caec3838..ebf0db4a 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -479,6 +479,8 @@ type barrier_kind =
   | Barrier_RISCV_rw_rw
   | Barrier_RISCV_r_rw
   | Barrier_RISCV_rw_w
+  | Barrier_RISCV_w_w
+  | Barrier_RISCV_i
 
 
 instance (Show barrier_kind)
@@ -499,6 +501,8 @@ instance (Show barrier_kind)
     | Barrier_RISCV_rw_rw -> "Barrier_RISCV_rw_rw"
     | Barrier_RISCV_r_rw  -> "Barrier_RISCV_r_rw"
     | Barrier_RISCV_rw_w  -> "Barrier_RISCV_rw_w"
+    | Barrier_RISCV_w_w   -> "Barrier_RISCV_w_w"
+    | Barrier_RISCV_I     -> "Barrier_RISCV_i"
   end
 end