fixed the RISC-V fences (3 types: "rw,rw"/"r,rw"/"rw,w")

18 files changed, 70 insertions, 25 deletions

diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen
index 2860484e..8983b5ae 100644
--- a/risc-v/hgen/ast.hgen
+++ b/risc-v/hgen/ast.hgen
@@ -10,4 +10,4 @@
 | `RISCVADDIW of bit12 * reg * reg
 | `RISCVSHIFTW of bit5 * reg * reg * riscvSop
 | `RISCVRTYPEW of reg * reg * reg * riscvRopw
-| `RISCVFENCE
+| `RISCVFENCE of bit4 * bit4
diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
index 16d827e2..50026612 100644
--- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
+++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -55,7 +55,6 @@
       translate_reg "rs1" rs1,
       translate_reg "rd" rd,
       translate_ropw op)
-| `RISCVFENCE -> FENCE (
-  translate_imm4 "pred" 0,
-  translate_imm4 "succ" 0
-)
+| `RISCVFENCE(pred, succ) -> FENCE(
+  translate_imm4 "pred" pred,
+  translate_imm4 "succ" succ)
diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
index 361c0e61..4d8bd87a 100644
--- a/risc-v/hgen/herdtools_types_to_shallow_types.hgen
+++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
@@ -75,5 +75,5 @@ let translate_imm6 name value =
 let translate_imm5 name value = 
     Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int value)
 
-let translate_imm4 name value = 
+let translate_imm4 name value =
     Sail_values.to_vec0 is_inc (Nat_big_num.of_int 4,Nat_big_num.of_int value)
diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen
index 3badc338..5f2c8326 100644
--- a/risc-v/hgen/lexer.hgen
+++ b/risc-v/hgen/lexer.hgen
@@ -59,3 +59,6 @@
 "sraw", RTYPEW{op=RISCVSRAW};
 
 "fence", FENCE ();
+"r",  FENCEOPTION Fence_R;
+"w",  FENCEOPTION Fence_W;
+"rw", FENCEOPTION Fence_RW;
diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen
index 8bb8ae2b..37fd8d8d 100644
--- a/risc-v/hgen/parser.hgen
+++ b/risc-v/hgen/parser.hgen
@@ -22,5 +22,15 @@
   { `RISCVSHIFTW ($6, $4, $2, $1.op) }
 | RTYPEW reg COMMA reg COMMA reg
   { `RISCVRTYPEW ($6, $4, $2, $1.op) }
-| FENCE
-  { `RISCVFENCE }
+| FENCE FENCEOPTION COMMA FENCEOPTION
+  { match ($2, $4) with
+    | (Fence_RW, Fence_RW) -> `RISCVFENCE (0b0011, 0b0011)
+    | (Fence_R,  Fence_RW) -> `RISCVFENCE (0b0010, 0b0011)
+    | (Fence_RW, Fence_W)  -> `RISCVFENCE (0b0011, 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"
+  }
diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen
index 0373783d..1da3ef11 100644
--- a/risc-v/hgen/pretty.hgen
+++ b/risc-v/hgen/pretty.hgen
@@ -12,4 +12,4 @@
 | `RISCVADDIW(imm, rs, rd)        -> sprintf "addiw %s, %s, %d" (pp_reg rd) (pp_reg rs) imm
 | `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                     -> "fence"
+| `RISCVFENCE(pred, succ)         -> sprintf "fence %s, %s" (pp_riscv_fence_option pred) (pp_riscv_fence_option succ)
diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen
index 6073242e..dca5bea1 100644
--- a/risc-v/hgen/sail_trans_out.hgen
+++ b/risc-v/hgen/sail_trans_out.hgen
@@ -11,4 +11,4 @@
 | ("ADDIW", [imm; rs; rd])        -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
 | ("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", [])                   -> `RISCVFENCE
+| ("FENCE", [pred; succ])         -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ)
diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
index da9047a3..6158ebd7 100644
--- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
+++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -11,4 +11,4 @@
 | ADDIW( imm, rs, rd)         -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
 | 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
+| FENCE( pred, succ)          -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ)
diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
index 8ef18f06..a891d7d0 100644
--- a/risc-v/hgen/shallow_types_to_herdtools_types.hgen
+++ b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
@@ -70,3 +70,4 @@ let translate_out_simm13 imm = translate_out_signed_int imm 13
 let translate_out_simm12 imm = translate_out_signed_int imm 12
 let translate_out_imm6 imm = translate_out_int imm
 let translate_out_imm5 imm = translate_out_int imm
+let translate_out_imm4 imm = translate_out_int imm
diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen
index e778d2a9..2980b985 100644
--- a/risc-v/hgen/token_types.hgen
+++ b/risc-v/hgen/token_types.hgen
@@ -11,3 +11,5 @@ type token_ADDIW    = unit
 type token_SHIFTW   = {op : riscvSop }
 type token_RTYPEW   = {op : riscvRopw }
 type token_FENCE    = unit
+
+type token_FENCEOPTION = Fence_R | Fence_W | Fence_RW
diff --git a/risc-v/hgen/tokens.hgen b/risc-v/hgen/tokens.hgen
index abe6a6c3..f952cf77 100644
--- a/risc-v/hgen/tokens.hgen
+++ b/risc-v/hgen/tokens.hgen
@@ -10,4 +10,5 @@
 %token <RISCVHGenBase.token_ADDIW>    ADDIW   
 %token <RISCVHGenBase.token_SHIFTW>   SHIFTW  
 %token <RISCVHGenBase.token_RTYPEW>   RTYPEW  
-%token <RISCVHGenBase.token_FENCE>    FENCE   
+%token <RISCVHGenBase.token_FENCE>    FENCE
+%token <RISCVHGenBase.token_FENCEOPTION> FENCEOPTION
diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen
index c72e84d5..df22d9dc 100644
--- a/risc-v/hgen/trans_sail.hgen
+++ b/risc-v/hgen/trans_sail.hgen
@@ -103,10 +103,10 @@
       translate_ropw "op" op;
     ],
     [])
-| `RISCVFENCE -> 
+| `RISCVFENCE(pred, succ) ->
   ("FENCE", 
   [
-     translate_imm4 "pred" 0;
-     translate_imm4 "succ" 0;
+     translate_imm4 "pred" pred;
+     translate_imm4 "succ" succ;
   ], 
   [])
diff --git a/risc-v/hgen/types.hgen b/risc-v/hgen/types.hgen
index e31b11f8..87fc9b95 100644
--- a/risc-v/hgen/types.hgen
+++ b/risc-v/hgen/types.hgen
@@ -2,6 +2,7 @@ type bit20 = int
 type bit12 = int
 type bit6  = int
 type bit5  = int
+type bit4  = int
 
 type riscvUop =  (* upper immediate ops *)
 | RISCVLUI
@@ -114,3 +115,9 @@ let pp_riscv_store_op width = match width with
 | RISCVWORD -> "sw"
 | RISCVDOUBLE -> "sd"
 | _ -> failwith "unexpected store op"
+
+let pp_riscv_fence_option = function
+  | 0b0011 -> "rw"
+  | 0b0010 -> "r"
+  | 0b0001 -> "w"
+  | _ -> failwith "unexpected fence option"
diff --git a/risc-v/hgen/types_sail_trans_out.hgen b/risc-v/hgen/types_sail_trans_out.hgen
index 297d0cf3..e22110d0 100644
--- a/risc-v/hgen/types_sail_trans_out.hgen
+++ b/risc-v/hgen/types_sail_trans_out.hgen
@@ -17,6 +17,7 @@ let translate_out_simm13 imm = translate_out_signed_int imm 13
 let translate_out_simm12 imm = translate_out_signed_int imm 12
 let translate_out_imm6 imm = translate_out_int imm
 let translate_out_imm5 imm = translate_out_int imm
+let translate_out_imm4 imm = translate_out_int imm
 
 let translate_out_bool = function
   | (name, Bit, [Bitc_one])  -> true
@@ -82,4 +83,4 @@ let translate_out_ropw op = match translate_out_enum op with
 | 2 -> RISCVSLLW
 | 3 -> RISCVSRLW
 | 4 -> RISCVSRAW
-| _ -> failwith "Unknown ropw in sail translate out"
\ No newline at end of file
+| _ -> failwith "Unknown ropw in sail translate out"
diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail
index 962d8280..4a80adb0 100644
--- a/risc-v/riscv.sail
+++ b/risc-v/riscv.sail
@@ -52,10 +52,17 @@ function unit wGPR((regno) r, (regval) v) =
     if (r != 0) then
         GPRs[r] := v
 
+function forall 'a. 'a effect { escape } not_implemented((string) message) =
+{
+  exit message;
+}
+
 val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
 val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea
 val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval
-val extern unit -> unit effect { barr } MEM_sync
+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
 
 (* Ideally these would be sail builtin *)
 function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) =
@@ -285,7 +292,12 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) =
 union ast member (bit[4], bit[4]) FENCE
 function clause decode (0b0000 : (bit[4]) pred : (bit[4]) succ : 0b00000 : 0b000 : 0b00000 : 0b0001111) = Some(FENCE (pred, succ))
 function clause execute (FENCE(pred, succ)) = {
- MEM_sync(); (* XXX use pred and succ *)
+  switch(pred, succ) {
+    case (0b0011, 0b0011) -> MEM_fence_rw_rw()
+    case (0b0010, 0b0011) -> MEM_fence_r_rw()
+    case (0b0011, 0b0001) -> MEM_fence_rw_w()
+    case _ -> not_implemented("unsupported fence")
+  }
 }
 
 union ast member unit FENCEI
diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem
index c09c85c2..aa5d8fb8 100644
--- a/risc-v/riscv_extras.lem
+++ b/risc-v/riscv_extras.lem
@@ -53,6 +53,8 @@ let memory_vals : memory_write_vals =
                              (IState (Interp.add_answer_to_stack interp bit) context)))));
   ]
 
-let barrier_functions = [
-  ("MEM_sync", Barrier_MIPS_SYNC);
+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);
   ]
diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem
index cbc8bd0d..1146d1cd 100644
--- a/risc-v/riscv_extras_embed.lem
+++ b/risc-v/riscv_extras_embed.lem
@@ -22,9 +22,13 @@ val MEMval_conditional     : (vector bitU * integer * vector bitU) -> M bitU
 let MEMval (_,_,v)                 = write_mem_val v >>= fun _ -> return ()
 let MEMval_conditional (_,_,v)     = write_mem_val v >>= fun b -> return (if b then B1 else B0)
 
-val MEM_sync  : unit -> M unit
+val MEM_fence_rw_rw : unit -> M unit
+val MEM_fence_r_rw  : unit -> M unit
+val MEM_fence_rw_w  : unit -> M unit
 
-let MEM_sync () = barrier Barrier_Isync
+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 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 7fb62161..f6709ff7 100644
--- a/risc-v/riscv_extras_embed_sequential.lem
+++ b/risc-v/riscv_extras_embed_sequential.lem
@@ -23,10 +23,13 @@ val MEMval_conditional     : (vector bitU * integer * vector bitU) -> M bitU
 let MEMval (_,_,v)                   = write_mem_val v >>= fun _ -> return ()
 let MEMval_conditional (_,_,v)       = write_mem_val v >>= fun b -> return (if b then B1 else B0)
 
-val MEM_sync  : unit -> M unit
-
-let MEM_sync () = barrier Barrier_MIPS_SYNC
+val MEM_fence_rw_rw : unit -> M unit
+val MEM_fence_r_rw  : unit -> M unit
+val MEM_fence_rw_w  : 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 duplicate (bit,len) =
   let bits = repeat [bit] len in