add risc-v fence instruction as re-using MIPS sync for now. Also place holders for FENCE.I and ECALL.

13 files changed, 37 insertions, 3 deletions

diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen
index 62e7cf4b..2860484e 100644
--- a/risc-v/hgen/ast.hgen
+++ b/risc-v/hgen/ast.hgen
@@ -10,3 +10,4 @@
 | `RISCVADDIW of bit12 * reg * reg
 | `RISCVSHIFTW of bit5 * reg * reg * riscvSop
 | `RISCVRTYPEW of reg * reg * reg * riscvRopw
+| `RISCVFENCE
diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
index ac6f22bd..46b11310 100644
--- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
+++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -55,3 +55,7 @@
       translate_reg "rs1" rs1,
       translate_reg "rd" rd,
       translate_ropw op)
+| `RISCVFENCE -> FENCE (
+  translate_imm4 "pred" 0,
+  translate_imm4 "succ" 0
+)
diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
index c4a1fd37..c15b3f94 100644
--- a/risc-v/hgen/herdtools_types_to_shallow_types.hgen
+++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
@@ -69,3 +69,6 @@ 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 = 
+    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 75d890e4..1888d42b 100644
--- a/risc-v/hgen/lexer.hgen
+++ b/risc-v/hgen/lexer.hgen
@@ -58,3 +58,4 @@
 "srlw", RTYPEW{op=RISCVSRLW};
 "sraw", RTYPEW{op=RISCVSRAW};
 
+"fence", FENCE ();
diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen
index abd87c7f..ba780857 100644
--- a/risc-v/hgen/parser.hgen
+++ b/risc-v/hgen/parser.hgen
@@ -22,3 +22,5 @@
   { `RISCVSHIFTW ($6, $4, $2, $1.op) }
 | RTYPEW reg COMMA reg COMMA reg
   { `RISCVRTYPEW ($6, $4, $2, $1.op) }
+| FENCE
+  { `RISCVFENCE }
diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen
index 0587c321..d8572ae2 100644
--- a/risc-v/hgen/pretty.hgen
+++ b/risc-v/hgen/pretty.hgen
@@ -12,3 +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"
diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen
index 7f1ae8ea..a9d3159c 100644
--- a/risc-v/hgen/sail_trans_out.hgen
+++ b/risc-v/hgen/sail_trans_out.hgen
@@ -11,3 +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
diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
index 9dc80a98..9278b92e 100644
--- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
+++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -11,3 +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
diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen
index cc993ae3..e778d2a9 100644
--- a/risc-v/hgen/token_types.hgen
+++ b/risc-v/hgen/token_types.hgen
@@ -10,3 +10,4 @@ type token_Store    = {width : wordWidth }
 type token_ADDIW    = unit
 type token_SHIFTW   = {op : riscvSop }
 type token_RTYPEW   = {op : riscvRopw }
+type token_FENCE    = unit
diff --git a/risc-v/hgen/tokens.hgen b/risc-v/hgen/tokens.hgen
index 0a874b81..abe6a6c3 100644
--- a/risc-v/hgen/tokens.hgen
+++ b/risc-v/hgen/tokens.hgen
@@ -10,4 +10,4 @@
 %token <RISCVHGenBase.token_ADDIW>    ADDIW   
 %token <RISCVHGenBase.token_SHIFTW>   SHIFTW  
 %token <RISCVHGenBase.token_RTYPEW>   RTYPEW  
-
+%token <RISCVHGenBase.token_FENCE>    FENCE   
diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen
index fd51c81f..c2e3138b 100644
--- a/risc-v/hgen/trans_sail.hgen
+++ b/risc-v/hgen/trans_sail.hgen
@@ -103,4 +103,4 @@
       translate_ropw "op" op;
     ],
     [])
-
+| `RISCVFENCE -> ("FENCE", [], [])
diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail
index 5234d128..e464c5f7 100644
--- a/risc-v/riscv.sail
+++ b/risc-v/riscv.sail
@@ -55,6 +55,7 @@ function unit wGPR((regno) r, (regval) v) =
 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
 
 (* Ideally these would be sail builtin *)
 function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) =
@@ -281,10 +282,25 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) =
   } in
   wGPR(rd, EXTS(result))
 
+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 *)
+}
+
+union ast member unit FENCEI
+function clause decode (0b0000 : 0b0000 : 0b0000 : 0b00000 : 0b001 : 0b00000 : 0b0001111) = Some(FENCEI)
+function clause execute FENCEI = () (* XXX TODO *)
+
+union ast member unit ECALL
+function clause decode (0b000000000000 : 0b00000 : 0b000 : 0b00000 : 0b1110011) = Some(ECALL ())
+function clause execute ECALL = ()
+
 union ast member unit EBREAK
 function clause decode (0b000000000001 : 0b00000 : 0b000 : 0b00000 : 0b1110011) = Some(EBREAK ())
 function clause execute EBREAK = { exit () }
 
+
 function clause decode _ = None
 
 end ast
diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail
index 1dff5064..0c7a67d8 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])) ||];
+            Nias := [|| NIAFP_register (RFull(GPRstr[rs])) ||]; (* XXX this should br rs + offset... *)
      }
      case (BTYPE ( imm, rs2, rs1, op)) -> {
             if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR;
@@ -76,6 +76,9 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
             if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR;
             if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
      }
+     case (FENCE(pred, succ)) -> {
+          ik := IK_barrier (Barrier_MIPS_SYNC);
+     }
   };
   (iR,oR,aR,Nias,Dia,ik)
 }