diff options
| -rw-r--r-- | Makefile | 8 | ||||
| -rw-r--r-- | handwritten_support/0.11/riscv_extras.lem (renamed from handwritten_support/0.7.1/riscv_extras.lem) | 85 | ||||
| -rw-r--r-- | handwritten_support/0.11/riscv_extras_sequential.lem (renamed from handwritten_support/0.7.1/riscv_extras_sequential.lem) | 39 | ||||
| -rw-r--r-- | model/riscv_analysis.sail | 176 | ||||
| -rw-r--r-- | model/riscv_insts_base.sail | 44 |
5 files changed, 303 insertions, 49 deletions
@@ -127,12 +127,12 @@ endif # Feature detect if we are on the latest development version of Sail # and use an updated lem file if so. This is just until the opam -# version catches up with changes to the monad embedding. -SAIL_LATEST := $(shell $(SAIL) -emacs 1>&2 2> /dev/null; echo $$?) +# version catches up with changes to the barrier type. +SAIL_LATEST := $(shell $(SAIL) -has_feature FEATURE_UNION_BARRIERS 1>&2 2> /dev/null; echo $$?) ifeq ($(SAIL_LATEST),0) -RISCV_EXTRAS_LEM = riscv_extras.lem +RISCV_EXTRAS_LEM = 0.11/riscv_extras.lem else -RISCV_EXTRAS_LEM = 0.7.1/riscv_extras.lem +RISCV_EXTRAS_LEM = riscv_extras.lem endif all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH) riscv_isa riscv_coq riscv_hol riscv_rmem diff --git a/handwritten_support/0.7.1/riscv_extras.lem b/handwritten_support/0.11/riscv_extras.lem index c1a52c9..f4ade26 100644 --- a/handwritten_support/0.7.1/riscv_extras.lem +++ b/handwritten_support/0.11/riscv_extras.lem @@ -8,17 +8,17 @@ open import Sail2_prompt type bitvector 'a = mword 'a -let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw -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_tso () = barrier Barrier_RISCV_tso -let MEM_fence_i () = barrier Barrier_RISCV_i +let MEM_fence_rw_rw () = barrier (Barrier_RISCV_rw_rw ()) +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_tso () = barrier (Barrier_RISCV_tso ()) +let MEM_fence_i () = barrier (Barrier_RISCV_i ()) val MEMea : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e val MEMea_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e @@ -27,13 +27,13 @@ val MEMea_conditional : forall 'rv 'a 'e. Size 'a => bitvector 'a val MEMea_conditional_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e val MEMea_conditional_strong_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e -let MEMea addr size = write_mem_ea Write_plain addr size -let MEMea_release addr size = write_mem_ea Write_RISCV_release addr size -let MEMea_strong_release addr size = write_mem_ea Write_RISCV_strong_release addr size -let MEMea_conditional addr size = write_mem_ea Write_RISCV_conditional addr size -let MEMea_conditional_release addr size = write_mem_ea Write_RISCV_conditional_release addr size +let MEMea addr size = write_mem_ea Write_plain () addr size +let MEMea_release addr size = write_mem_ea Write_RISCV_release () addr size +let MEMea_strong_release addr size = write_mem_ea Write_RISCV_strong_release () addr size +let MEMea_conditional addr size = write_mem_ea Write_RISCV_conditional () addr size +let MEMea_conditional_release addr size = write_mem_ea Write_RISCV_conditional_release () addr size let MEMea_conditional_strong_release addr size - = write_mem_ea Write_RISCV_conditional_strong_release addr size + = write_mem_ea Write_RISCV_conditional_strong_release () addr size val MEMr : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e val MEMr_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e @@ -42,22 +42,26 @@ val MEMr_reserved : forall 'rv 'a 'b 'e. Size 'a, Size 'b => inte val MEMr_reserved_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e -let MEMr addrsize size hexRAM addr = read_mem Read_plain addr size -let MEMr_acquire addrsize size hexRAM addr = read_mem Read_RISCV_acquire addr size -let MEMr_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_strong_acquire addr size -let MEMr_reserved addrsize size hexRAM addr = read_mem Read_RISCV_reserved addr size -let MEMr_reserved_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_acquire addr size -let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addr size - -val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => - integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e -let write_ram addrsize size hexRAM address value = - write_mem_val value - -val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => - integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e -let read_ram addrsize size hexRAM address = - read_mem Read_plain address size +let MEMr addrsize size hexRAM addr = read_mem Read_plain addrsize addr size +let MEMr_acquire addrsize size hexRAM addr = read_mem Read_RISCV_acquire addrsize addr size +let MEMr_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_strong_acquire addrsize addr size +let MEMr_reserved addrsize size hexRAM addr = read_mem Read_RISCV_reserved addrsize addr size +let MEMr_reserved_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_acquire addrsize addr size +let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addrsize addr size + +val MEMw : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e +val MEMw_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e +val MEMw_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e +val MEMw_conditional : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e +val MEMw_conditional_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e +val MEMw_conditional_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e + +let MEMw addrsize size hexRAM addr = write_mem Write_plain addrsize addr size +let MEMw_release addrsize size hexRAM addr = write_mem Write_RISCV_release addrsize addr size +let MEMw_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_strong_release addrsize addr size +let MEMw_conditional addrsize size hexRAM addr = write_mem Write_RISCV_conditional addrsize addr size +let MEMw_conditional_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_release addrsize addr size +let MEMw_conditional_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_strong_release addrsize addr size val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit let load_reservation addr = () @@ -67,6 +71,14 @@ let speculate_conditional_success () = excl_result () let match_reservation _ = true let cancel_reservation () = () +val sys_enable_writable_misa : unit -> bool +let sys_enable_writable_misa () = true +declare ocaml target_rep function sys_enable_writable_misa = `Platform.enable_writable_misa` + +val sys_enable_rvc : unit -> bool +let sys_enable_rvc () = true +declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc` + val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_ram_base () = wordFromInteger 0 declare ocaml target_rep function plat_ram_base = `Platform.dram_base` @@ -99,6 +111,10 @@ val plat_enable_misaligned_access : unit -> bool let plat_enable_misaligned_access () = false declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access` +val plat_enable_pmp : unit -> bool +let plat_enable_pmp () = false +declare ocaml target_rep function plat_enable_pmp = `Platform.enable_pmp` + val plat_mtval_has_illegal_inst_bits : unit -> bool let plat_mtval_has_illegal_inst_bits () = false declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits` @@ -135,3 +151,6 @@ let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs))) val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *) + +val print_dbg : string -> unit +let print_dbg msg = () diff --git a/handwritten_support/0.7.1/riscv_extras_sequential.lem b/handwritten_support/0.11/riscv_extras_sequential.lem index c1a52c9..ac70ee5 100644 --- a/handwritten_support/0.7.1/riscv_extras_sequential.lem +++ b/handwritten_support/0.11/riscv_extras_sequential.lem @@ -8,17 +8,17 @@ open import Sail2_prompt type bitvector 'a = mword 'a -let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw -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_tso () = barrier Barrier_RISCV_tso -let MEM_fence_i () = barrier Barrier_RISCV_i +let MEM_fence_rw_rw () = barrier (Barrier_RISCV_rw_rw ()) +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_tso () = barrier (Barrier_RISCV_tso ()) +let MEM_fence_i () = barrier (Barrier_RISCV_i ()) val MEMea : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e val MEMea_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e @@ -52,7 +52,7 @@ let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e let write_ram addrsize size hexRAM address value = - write_mem_val value + write_mem Write_plain address size value val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e @@ -67,6 +67,14 @@ let speculate_conditional_success () = excl_result () let match_reservation _ = true let cancel_reservation () = () +val sys_enable_writable_misa : unit -> bool +let sys_enable_writable_misa () = true +declare ocaml target_rep function sys_enable_writable_misa = `Platform.enable_writable_misa` + +val sys_enable_rvc : unit -> bool +let sys_enable_rvc () = true +declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc` + val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_ram_base () = wordFromInteger 0 declare ocaml target_rep function plat_ram_base = `Platform.dram_base` @@ -99,6 +107,10 @@ val plat_enable_misaligned_access : unit -> bool let plat_enable_misaligned_access () = false declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access` +val plat_enable_pmp : unit -> bool +let plat_enable_pmp () = false +declare ocaml target_rep function plat_enable_pmp = `Platform.enable_pmp` + val plat_mtval_has_illegal_inst_bits : unit -> bool let plat_mtval_has_illegal_inst_bits () = false declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits` @@ -135,3 +147,6 @@ let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs))) val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *) + +val print_dbg : string -> unit +let print_dbg msg = () diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail index 34572f8..ec8c96f 100644 --- a/model/riscv_analysis.sail +++ b/model/riscv_analysis.sail @@ -10,6 +10,8 @@ let GPRstr : vector(32, dec, string) = [ "x31", "x30", "x29", "x28", "x27", "x26 let CIA_fp = RFull("CIA") let NIA_fp = RFull("NIA") +$ifndef FEATURE_UNION_BARRIER + function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,instruction_kind) = { iR = [| |] : regfps; oR = [| |] : regfps; @@ -180,3 +182,177 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst }; (iR,oR,aR,Nias,Dia,ik) } + +$else + +function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,instruction_kind) = { + iR = [| |] : regfps; + oR = [| |] : regfps; + aR = [| |] : regfps; + ik = IK_simple() : instruction_kind; + Nias = [| NIAFP_successor() |] : niafps; + Dia = DIAFP_none() : diafp; + + match instr { + EBREAK() => (), + UTYPE(imm, rd, op) => { + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + }, + RISCV_JAL(imm, rd) => { + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + let offset : bits(64) = EXTS(imm) in + Nias = [| NIAFP_concrete_address (PC + offset) |]; + ik = IK_branch(); + }, + RISCV_JALR(imm, rs, rd) => { + if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + let offset : bits(64) = EXTS(imm) in + Nias = [| NIAFP_indirect_address() |]; + ik = IK_branch(); + }, + BTYPE(imm, rs2, rs1, op) => { + if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; + ik = IK_branch(); + let offset : bits(64) = EXTS(imm) in + Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |]; + }, + ITYPE(imm, rs, rd, op) => { + if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + }, + SHIFTIOP(imm, rs, rd, op) => { + if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + }, + RTYPE(rs2, rs1, rd, op) => { + if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + }, + CSR(csr, rs1, rd, is_imm, op) => { + let isWrite : bool = match op { + CSRRW => true, + _ => if is_imm then unsigned(rs1) != 0 else unsigned(rs1) != 0 + }; + iR = RFull(csr_name(csr)) :: iR; + if ~(is_imm) then { + iR = RFull(GPRstr[rs1]) :: iR; + }; + if isWrite then { + oR = RFull(csr_name(csr)) :: oR; + }; + oR = RFull(GPRstr[rd]) :: oR; + }, + LOAD(imm, rs, rd, unsign, width, aq, rl) => { /* XXX "unsigned" causes name conflict in lem shallow embedding... */ + if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + aR = iR; + ik = + match (aq, rl) { + (false, false) => IK_mem_read (Read_plain), + (true, false) => IK_mem_read (Read_RISCV_acquire), + (true, true) => IK_mem_read (Read_RISCV_strong_acquire), + + _ => internal_error("LOAD type not implemented in initial_analysis") + } + }, + STORE(imm, rs2, rs1, width, aq, rl) => { + if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; + if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR; + ik = + match (aq, rl) { + (false, false) => IK_mem_write (Write_plain), + (false, true) => IK_mem_write (Write_RISCV_release), + (true, true) => IK_mem_write (Write_RISCV_strong_release), + + _ => internal_error("STORE type not implemented in initial_analysis") + } + }, + ADDIW(imm, rs, rd) => { + if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + }, + SHIFTW(imm, rs, rd, op) => { + if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + }, + RTYPEW(rs2, rs1, rd, op) => { + if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + }, + FENCE(pred, succ) => { + ik = + match (pred, succ) { + (_ : 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") + }; + }, + FENCE_TSO(pred, succ) => { + ik = + match (pred, succ) { + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_tso ()), + _ => internal_error("barrier type not implemented in initial_analysis") + }; + }, + FENCEI() => { + ik = IK_simple (); // for RMEM, should morally be Barrier_RISCV_i + }, + LOADRES(aq, rl, rs1, width, rd) => { + if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + aR = iR; + ik = match (aq, rl) { + (false, false) => IK_mem_read (Read_RISCV_reserved), + (true, false) => IK_mem_read (Read_RISCV_reserved_acquire), + (true, true) => IK_mem_read (Read_RISCV_reserved_strong_acquire), + (false, true) => internal_error("LOADRES type not implemented in initial_analysis") + }; + }, + STORECON(aq, rl, rs2, rs1, width, rd) => { + if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; + if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + ik = match (aq, rl) { + (false, false) => IK_mem_write (Write_RISCV_conditional), + (false, true) => IK_mem_write (Write_RISCV_conditional_release), + (true, true) => IK_mem_write (Write_RISCV_conditional_strong_release), + + (true, false) => internal_error("STORECON type not implemented in initial_analysis") + }; + }, + AMO(op, aq, rl, rs2, rs1, width, rd) => { + if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; + if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + ik = match (aq, rl) { + (false, false) => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional), + (false, true) => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional_release), + (true, false) => IK_mem_rmw (Read_RISCV_reserved_acquire, + Write_RISCV_conditional), + (true, true) => IK_mem_rmw (Read_RISCV_reserved_acquire, + Write_RISCV_conditional_release) + }; + }, + _ => () + }; + (iR,oR,aR,Nias,Dia,ik) +} + +$endif diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 14a626e..636170b 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -564,6 +564,31 @@ union clause ast = FENCE : (bits(4), bits(4)) mapping clause encdec = FENCE(pred, succ) <-> 0b0000 @ pred @ succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111 +/* For future versions of Sail where barriers can be parameterised */ +$ifdef FEATURE_UNION_BARRIER + +function clause execute (FENCE(pred, succ)) = { + match (pred, succ) { + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw()), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_r_rw()), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_r_r()), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_rw_w()), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_w_w()), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_w_rw()), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_rw_r()), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_r_w()), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_w_r()), + + (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (), + + _ => { print("FIXME: unsupported fence"); + () } + }; + RETIRE_SUCCESS +} + +$else + function clause execute (FENCE(pred, succ)) = { match (pred, succ) { (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw), @@ -584,6 +609,8 @@ function clause execute (FENCE(pred, succ)) = { RETIRE_SUCCESS } +$endif + mapping bit_maybe_r : bits(1) <-> string = { 0b1 <-> "r", 0b0 <-> "" @@ -617,6 +644,21 @@ union clause ast = FENCE_TSO : (bits(4), bits(4)) mapping clause encdec = FENCE_TSO(pred, succ) <-> 0b1000 @ pred @ succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111 +$ifdef FEATURE_UNION_BARRIER + +function clause execute (FENCE_TSO(pred, succ)) = { + match (pred, succ) { + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso()), + (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (), + + _ => { print("FIXME: unsupported fence"); + () } + }; + RETIRE_SUCCESS +} + +$else + function clause execute (FENCE_TSO(pred, succ)) = { match (pred, succ) { (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso), @@ -628,6 +670,8 @@ function clause execute (FENCE_TSO(pred, succ)) = { RETIRE_SUCCESS } +$endif + mapping clause assembly = FENCE_TSO(pred, succ) <-> "fence.tso" ^ spc() ^ fence_bits(pred) ^ sep() ^ fence_bits(succ) |