From c080665a6fbd8c88b66440a7bddc31a9634741cf Mon Sep 17 00:00:00 2001 From: Jon French Date: Thu, 5 Jul 2018 13:09:41 +0100 Subject: restore missing RISC-V fence types in sail2; ignore io bits in fences more cleanly --- lib/regfp.sail | 4 +++ riscv/riscv.sail | 55 +++++++++++++++--------------------- riscv/riscv_extras.lem | 4 +++ riscv/riscv_extras_sequential.lem | 4 +++ riscv/riscv_mem.sail | 4 +++ riscv/riscv_types.sail | 2 +- src/lem_interp/sail2_instr_kinds.lem | 16 +++++++++-- 7 files changed, 54 insertions(+), 35 deletions(-) diff --git a/lib/regfp.sail b/lib/regfp.sail index b8cffb98..fcf10850 100644 --- a/lib/regfp.sail +++ b/lib/regfp.sail @@ -75,6 +75,10 @@ enum barrier_kind = { Barrier_RISCV_r_r, Barrier_RISCV_rw_w, Barrier_RISCV_w_w, + Barrier_RISCV_w_rw, + Barrier_RISCV_rw_r, + Barrier_RISCV_r_w, + Barrier_RISCV_w_r, Barrier_RISCV_i, Barrier_x86_MFENCE } diff --git a/riscv/riscv.sail b/riscv/riscv.sail index 87f1b7ca..b50c9225 100644 --- a/riscv/riscv.sail +++ b/riscv/riscv.sail @@ -707,19 +707,17 @@ mapping clause encdec = FENCE(pred, succ) <-> 0b0000 @ pred @ succ @ 0b00000 @ 0 function clause execute (FENCE(pred, succ)) = { match (pred, succ) { - (0b0011, 0b0011) => MEM_fence_rw_rw(), - (0b0010, 0b0011) => MEM_fence_r_rw(), - (0b0010, 0b0010) => MEM_fence_r_r(), - (0b0011, 0b0001) => MEM_fence_rw_w(), - (0b0001, 0b0001) => MEM_fence_w_w(), - - (0b1111, 0b1111) => MEM_fence_rw_rw(), - (0b1110, 0b1111) => MEM_fence_r_rw(), - (0b1110, 0b1110) => MEM_fence_r_r(), - (0b1111, 0b1101) => MEM_fence_rw_w(), - (0b1101, 0b1101) => MEM_fence_w_w(), - - (0b0000, 0b0000) => (), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => MEM_fence_rw_rw(), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => MEM_fence_r_rw(), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => MEM_fence_r_r(), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => MEM_fence_rw_w(), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => MEM_fence_w_w(), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => MEM_fence_w_rw(), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => MEM_fence_rw_r(), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => MEM_fence_r_w(), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => MEM_fence_w_r(), + + (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (), _ => { print("FIXME: unsupported fence"); () } @@ -1936,25 +1934,18 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst FENCE(pred, succ) => { ik = match (pred, succ) { - (0b0011, 0b0011) => IK_barrier (Barrier_RISCV_rw_rw), - (0b0010, 0b0011) => IK_barrier (Barrier_RISCV_r_rw), - (0b0010, 0b0010) => IK_barrier (Barrier_RISCV_r_r), - (0b0011, 0b0001) => IK_barrier (Barrier_RISCV_rw_w), - (0b0001, 0b0001) => IK_barrier (Barrier_RISCV_w_w), - - (0b1111, 0b1111) => IK_barrier (Barrier_RISCV_rw_rw), - (0b1110, 0b1111) => IK_barrier (Barrier_RISCV_r_rw), - (0b1110, 0b1110) => IK_barrier (Barrier_RISCV_r_r), - (0b1111, 0b1101) => IK_barrier (Barrier_RISCV_rw_w), - (0b1101, 0b1101) => IK_barrier (Barrier_RISCV_w_w), - - // (0b0001, 0b0011) => IK_barrier (Barrier_RISCV_w_rw), - // (0b0011, 0b0010) => IK_barrier (Barrier_RISCV_rw_r), - // (0b0010, 0b0001) => IK_barrier (Barrier_RISCV_r_w), - // (0b0001, 0b0010) => IK_barrier (Barrier_RISCV_w_r), - - - (0b0000, 0b0000) => IK_simple (), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_rw_rw), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_r_rw), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_r_r), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_rw_w), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_w_w), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_w_rw), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_rw_r), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_r_w), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_w_r), + + + (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => IK_simple (), _ => internal_error("barrier type not implemented in initial_analysis") // case (FM_NORMAL, _, _) -> exit "not implemented" diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem index 601f5008..b29fe545 100644 --- a/riscv/riscv_extras.lem +++ b/riscv/riscv_extras.lem @@ -13,6 +13,10 @@ let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw let MEM_fence_r_r () = barrier Barrier_RISCV_r_r let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w let MEM_fence_w_w () = barrier Barrier_RISCV_w_w +let MEM_fence_w_rw () = barrier Barrier_RISCV_w_rw +let MEM_fence_rw_r () = barrier Barrier_RISCV_rw_r +let MEM_fence_r_w () = barrier Barrier_RISCV_r_w +let MEM_fence_w_r () = barrier Barrier_RISCV_w_r let MEM_fence_i () = barrier Barrier_RISCV_i val MEMea : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e diff --git a/riscv/riscv_extras_sequential.lem b/riscv/riscv_extras_sequential.lem index 601f5008..b29fe545 100644 --- a/riscv/riscv_extras_sequential.lem +++ b/riscv/riscv_extras_sequential.lem @@ -13,6 +13,10 @@ let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw let MEM_fence_r_r () = barrier Barrier_RISCV_r_r let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w let MEM_fence_w_w () = barrier Barrier_RISCV_w_w +let MEM_fence_w_rw () = barrier Barrier_RISCV_w_rw +let MEM_fence_rw_r () = barrier Barrier_RISCV_rw_r +let MEM_fence_r_w () = barrier Barrier_RISCV_r_w +let MEM_fence_w_r () = barrier Barrier_RISCV_w_r let MEM_fence_i () = barrier Barrier_RISCV_i val MEMea : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail index bdbb72bf..9ead3aeb 100644 --- a/riscv/riscv_mem.sail +++ b/riscv/riscv_mem.sail @@ -140,4 +140,8 @@ val MEM_fence_r_rw = {ocaml: "skip", lem: "MEM_fence_r_rw"} : unit -> unit eff val MEM_fence_r_r = {ocaml: "skip", lem: "MEM_fence_r_r"} : unit -> unit effect {barr} val MEM_fence_rw_w = {ocaml: "skip", lem: "MEM_fence_rw_w"} : unit -> unit effect {barr} val MEM_fence_w_w = {ocaml: "skip", lem: "MEM_fence_w_w"} : unit -> unit effect {barr} +val MEM_fence_w_rw = {ocaml: "skip", lem: "MEM_fence_w_rw"} : unit -> unit effect {barr} +val MEM_fence_rw_r = {ocaml: "skip", lem: "MEM_fence_rw_r"} : unit -> unit effect {barr} +val MEM_fence_r_w = {ocaml: "skip", lem: "MEM_fence_r_w"} : unit -> unit effect {barr} +val MEM_fence_w_r = {ocaml: "skip", lem: "MEM_fence_w_r"} : unit -> unit effect {barr} val MEM_fence_i = {ocaml: "skip", lem: "MEM_fence_i"} : unit -> unit effect {barr} diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail index 2991377d..e2341a8a 100644 --- a/riscv/riscv_types.sail +++ b/riscv/riscv_types.sail @@ -468,7 +468,7 @@ mapping reg_name = { } val sep : unit <-> string -mapping sep = { +mapping sep : unit <-> string = { () <-> opt_spc() ^ "," ^ def_spc() } diff --git a/src/lem_interp/sail2_instr_kinds.lem b/src/lem_interp/sail2_instr_kinds.lem index 13e5304e..938b693d 100644 --- a/src/lem_interp/sail2_instr_kinds.lem +++ b/src/lem_interp/sail2_instr_kinds.lem @@ -151,6 +151,10 @@ type barrier_kind = | Barrier_RISCV_r_r | Barrier_RISCV_rw_w | Barrier_RISCV_w_w + | Barrier_RISCV_w_rw + | Barrier_RISCV_rw_r + | Barrier_RISCV_r_w + | Barrier_RISCV_w_r | Barrier_RISCV_i (* X86 *) | Barrier_x86_MFENCE @@ -176,6 +180,10 @@ instance (Show barrier_kind) | Barrier_RISCV_r_r -> "Barrier_RISCV_r_r" | Barrier_RISCV_rw_w -> "Barrier_RISCV_rw_w" | Barrier_RISCV_w_w -> "Barrier_RISCV_w_w" + | Barrier_RISCV_w_rw -> "Barrier_RISCV_w_rw" + | Barrier_RISCV_rw_r -> "Barrier_RISCV_rw_r" + | Barrier_RISCV_r_w -> "Barrier_RISCV_r_w" + | Barrier_RISCV_w_r -> "Barrier_RISCV_w_r" | Barrier_RISCV_i -> "Barrier_RISCV_i" | Barrier_x86_MFENCE -> "Barrier_x86_MFENCE" end @@ -288,7 +296,11 @@ instance (EnumerationType barrier_kind) | Barrier_RISCV_r_r -> 15 | Barrier_RISCV_rw_w -> 16 | Barrier_RISCV_w_w -> 17 - | Barrier_RISCV_i -> 18 - | Barrier_x86_MFENCE -> 19 + | Barrier_RISCV_w_rw -> 18 + | Barrier_RISCV_rw_r -> 19 + | Barrier_RISCV_r_w -> 20 + | Barrier_RISCV_w_r -> 21 + | Barrier_RISCV_i -> 22 + | Barrier_x86_MFENCE -> 23 end end -- cgit v1.2.3