From 59447f06576b66bcaa801334851130a4fe963879 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Mon, 13 Nov 2023 17:18:20 +0000 Subject: [PATCH] Adapt memory builtins for Sail concurrency interface Sail has for a while now had a flexible way of passing additional information to either operational or axiomatic concurrency models by instantiating outcomes (effects) with model-specific types. The set of possible outcomes is defined in the Sail library, and a subset of these can be instantiated by any model. As part of adapting the model to this newer concurrency interface, the riscv_analysis file is no-longer needed, so it has been removed. --- Makefile | 7 +- model/main.sail | 63 ++++++- model/prelude.sail | 2 - model/prelude_mem.sail | 131 +++++++++++-- model/riscv_analysis.sail | 367 ------------------------------------ model/riscv_insts_base.sail | 70 +------ model/riscv_pc_access.sail | 1 + model/riscv_step.sail | 7 +- 8 files changed, 194 insertions(+), 454 deletions(-) delete mode 100644 model/riscv_analysis.sail diff --git a/Makefile b/Makefile index 7068968f4..b3178f58f 100644 --- a/Makefile +++ b/Makefile @@ -107,16 +107,13 @@ SAIL_ARCH_SRCS += riscv_types_kext.sail # Shared/common code for the cryptogr SAIL_STEP_SRCS = riscv_step_common.sail riscv_step_ext.sail riscv_decode_ext.sail riscv_fetch.sail riscv_step.sail RVFI_STEP_SRCS = riscv_step_common.sail riscv_step_rvfi.sail riscv_decode_ext.sail riscv_fetch_rvfi.sail riscv_step.sail -# Control inclusion of 64-bit only riscv_analysis -ifeq ($(ARCH),RV32) SAIL_OTHER_SRCS = $(SAIL_STEP_SRCS) +ifeq ($(ARCH),RV32) SAIL_OTHER_COQ_SRCS = riscv_termination_common.sail riscv_termination_rv32.sail else -SAIL_OTHER_SRCS = $(SAIL_STEP_SRCS) riscv_analysis.sail -SAIL_OTHER_COQ_SRCS = riscv_termination_common.sail riscv_termination_rv64.sail riscv_analysis.sail +SAIL_OTHER_COQ_SRCS = riscv_termination_common.sail riscv_termination_rv64.sail endif - PRELUDE_SRCS = $(addprefix model/,$(PRELUDE)) SAIL_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_SRCS)) SAIL_RMEM_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_RMEM_INST_SRCS) $(SAIL_OTHER_SRCS)) diff --git a/model/main.sail b/model/main.sail index c545e27fd..1422635be 100644 --- a/model/main.sail +++ b/model/main.sail @@ -6,19 +6,74 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ -function main () : unit -> unit = { +// When the symbolic execution is running a litmus test, it sets a +// different entry point for each thread in the compiled litmus test. + +val get_entry_point : unit -> xlenbits + +$ifdef SYMBOLIC + +$include + +function get_entry_point() = to_bits(sizeof(xlen), elf_entry()) + +$else + +function get_entry_point() = zero_extend(0x1000) + +$endif + +function main() : unit -> unit = { // initialize extensions - ext_init (); + ext_init(); - // PC = __GetSlice_int(64, elf_entry(), 0); - PC = sail_zero_extend(0x1000, sizeof(xlen)); + PC = get_entry_point(); print_bits("PC = ", PC); try { init_model(); + sail_end_cycle(); loop() } catch { Error_not_implemented(s) => print_string("Error: Not implemented: ", s), Error_internal_error() => print("Error: internal error") } } + +// For symbolic execution using Isla, we need an entry point that +// allows us to execute a single instruction. +$ifdef SYMBOLIC + +$include + +val isla_footprint_no_init : forall 'n, 'n in {16, 32}. bits('n) -> bool + +function isla_footprint_no_init(opcode) = { + try { + isla_reset_registers(); + sail_end_cycle(); + + let instr = if length(opcode) == 16 then { + ext_decode_compressed(opcode) + } else { + ext_decode(opcode) + }; + let _ = execute(instr); + true + } catch { + _ => false + } +} + +val isla_footprint : forall 'n, 'n in {16, 32}. bits('n) -> bool + +function isla_footprint(opcode) = { + try { + init_model(); + isla_footprint_no_init(opcode) + } catch { + _ => false + } +} + +$endif diff --git a/model/prelude.sail b/model/prelude.sail index 028af2126..b876b4f23 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -14,11 +14,9 @@ $include $include $include "mapping.sail" $include -$include $include $include "hex_bits.sail" - val not_bit : bit -> bit function not_bit(b) = if b == bitone then bitzero else bitone diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index c4f3d0710..345e78c20 100644 --- a/model/prelude_mem.sail +++ b/model/prelude_mem.sail @@ -12,12 +12,68 @@ * They also depend on the type of metadata that is read and written * to physical memory. For models that do not require this metadata, * a unit type can be used. - * - * The underlying __read_mem and __write_mem functions are from the - * Sail library. The metadata primitives __{Read,Write}RAM_Meta are - * in prelude_mem_metadata. */ +$include + +enum write_kind = { + Write_plain, + Write_RISCV_release, + Write_RISCV_strong_release, + Write_RISCV_conditional, + Write_RISCV_conditional_release, + Write_RISCV_conditional_strong_release, +} + +enum read_kind = { + Read_plain, + Read_ifetch, + Read_RISCV_acquire, + Read_RISCV_strong_acquire, + Read_RISCV_reserved, + Read_RISCV_reserved_acquire, + Read_RISCV_reserved_strong_acquire, +} + +enum barrier_kind = { + Barrier_RISCV_rw_rw, + Barrier_RISCV_r_rw, + 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_tso, + Barrier_RISCV_i, +} + +/* Most of the above read/write_kinds are understood natively by the + Sail concurrency interface, except for the strong acquire release + variants which require an architecture specific access kind. */ +struct RISCV_strong_access = { + variety : Access_variety, +} + +/* The Sail concurrency interface lets us have a physical address type + with additional information, provided we can supply a function that + converts it into a bitvector. Since we are just using xlenbits as a + physical address, we need the identity function for xlenbits. */ +val xlenbits_identity : xlenbits -> xlenbits + +function xlenbits_identity xs = xs + +instantiation sail_mem_write with + 'pa = xlenbits, + pa_bits = xlenbits_identity, + /* We don't have a relaxed-memory translation model for RISC-V, so + we just use unit as a dummy type. */ + 'translation_summary = unit, + 'arch_ak = RISCV_strong_access, + /* Similarly to translation_summary, we don't have a defined type for external + aborts, so just use unit here too */ + 'abort = unit /* This is a slightly arbitrary limit on the maximum number of bytes in a memory access. It helps to generate slightly better C code @@ -27,8 +83,25 @@ capabilities and SIMD / vector instructions will also need more. */ type max_mem_access : Int = 16 -val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> bool +val write_ram : forall 'n, 0 < 'n <= max_mem_access. (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> bool + function write_ram(wk, addr, width, data, meta) = { + let request : Mem_write_request('n, 64, xlenbits, unit, RISCV_strong_access) = struct { + access_kind = match wk { + Write_plain => AK_explicit(struct { variety = AV_plain, strength = AS_normal }), + Write_RISCV_release => AK_explicit(struct { variety = AV_plain, strength = AS_rel_or_acq }), + Write_RISCV_strong_release => AK_arch(struct { variety = AV_plain }), + Write_RISCV_conditional => AK_explicit(struct { variety = AV_exclusive, strength = AS_normal }), + Write_RISCV_conditional_release => AK_explicit(struct { variety = AV_exclusive, strength = AS_rel_or_acq }), + Write_RISCV_conditional_strong_release => AK_arch(struct { variety = AV_exclusive }), + }, + va = None(), + pa = addr, + translation = (), + size = width, + value = Some(data), + tag = None(), + }; /* Write out metadata only if the value write succeeds. * It is assumed for now that this write always succeeds; * there is currently no return value. @@ -36,19 +109,47 @@ function write_ram(wk, addr, width, data, meta) = { * (not just for Lem) to consume the value along with the * metadata to ensure atomicity. */ - let ret : bool = __write_mem(wk, sizeof(xlen), addr, width, data); - if ret then __WriteRAM_Meta(addr, width, meta); - ret + match sail_mem_write(request) { + Ok(_) => { + __WriteRAM_Meta(addr, width, meta); + true + }, + Err() => false, + } } -val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('n)) -> unit -function write_ram_ea(wk, addr, width) = - __write_mem_ea(wk, sizeof(xlen), addr, width) +val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access. (write_kind, xlenbits, int('n)) -> unit +function write_ram_ea(wk, addr, width) = () + +instantiation sail_mem_read with + pa_bits = xlenbits_identity + +val read_ram : forall 'n, 0 < 'n <= max_mem_access. (read_kind, xlenbits, int('n), bool) -> (bits(8 * 'n), mem_meta) +function read_ram(rk, addr, width, read_meta) = { + let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta; + let request : Mem_read_request('n, 64, xlenbits, unit, RISCV_strong_access) = struct { + access_kind = match rk { + Read_plain => AK_explicit(struct { variety = AV_plain, strength = AS_normal }), + Read_ifetch => AK_ifetch(), + Read_RISCV_acquire => AK_explicit(struct { variety = AV_plain, strength = AS_rel_or_acq }), + Read_RISCV_strong_acquire => AK_arch(struct { variety = AV_plain }), + Read_RISCV_reserved => AK_explicit(struct { variety = AV_exclusive, strength = AS_normal }), + Read_RISCV_reserved_acquire => AK_explicit(struct { variety = AV_exclusive, strength = AS_rel_or_acq }), + Read_RISCV_reserved_strong_acquire => AK_arch(struct { variety = AV_exclusive }), + }, + va = None(), + pa = addr, + translation = (), + size = width, + tag = false, + }; + match sail_mem_read(request) { + Ok((value, _)) => (value, meta), + Err() => exit(), + } +} -val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access . (read_kind, xlenbits, int('n), bool) -> (bits(8 * 'n), mem_meta) -function read_ram(rk, addr, width, read_meta) = - let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta in - (__read_mem(rk, sizeof(xlen), addr, width), meta) +instantiation sail_barrier with 'barrier = barrier_kind val __TraceMemoryWrite : forall 'n 'm. (int('n), bits('m), bits(8 * 'n)) -> unit val __TraceMemoryRead : forall 'n 'm. (int('n), bits('m), bits(8 * 'n)) -> unit diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail deleted file mode 100644 index 0d72bed3c..000000000 --- a/model/riscv_analysis.sail +++ /dev/null @@ -1,367 +0,0 @@ -/*=======================================================================================*/ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except where otherwise noted is subject the BSD */ -/* two-clause license in the LICENSE file. */ -/* */ -/* SPDX-License-Identifier: BSD-2-Clause */ -/*=======================================================================================*/ - -$include - -/* in reverse order because inc vectors don't seem to work (bug) */ -let GPRstrs : vector(32, dec, string) = [ "x31", "x30", "x29", "x28", "x27", "x26", "x25", "x24", "x23", "x22", "x21", - "x20", "x19", "x18", "x17", "x16", "x15", "x14", "x13", "x12", "x11", - "x10", "x9", "x8", "x7", "x6", "x5", "x4", "x3", "x2", "x1", "x0" - ] - -function GPRstr(i: bits(5)) -> string = GPRstrs[unsigned(i)] - -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; - aR = [| |] : regfps; - ik = IK_simple() : instruction_kind; - Nias = [| NIAFP_successor() |] : niafps; - Dia = DIAFP_none() : diafp; - - match instr { - EBREAK() => (), - UTYPE(imm, rd, op) => { - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - RISCV_JAL(imm, rd) => { - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - let offset : bits(64) = sign_extend(imm) in - Nias = [| NIAFP_concrete_address (PC + offset) |]; - ik = IK_branch(); - }, - RISCV_JALR(imm, rs, rd) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - let offset : bits(64) = sign_extend(imm) in - Nias = [| NIAFP_indirect_address() |]; - ik = IK_branch(); - }, - BTYPE(imm, rs2, rs1, op) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - ik = IK_branch(); - let offset : bits(64) = sign_extend(imm) in - Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |]; - }, - ITYPE(imm, rs, rd, op) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - SHIFTIOP(imm, rs, rd, op) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - RTYPE(rs2, rs1, rd, op) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rd == 0b00000) 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 not(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 == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) 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(__FILE__, __LINE__, "LOAD type not implemented in initial_analysis") - } - }, - STORE(imm, rs2, rs1, width, aq, rl) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rs1 == 0b00000) 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(__FILE__, __LINE__, "STORE type not implemented in initial_analysis") - } - }, - ADDIW(imm, rs, rd) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - SHIFTIWOP(imm, rs, rd, op) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - RTYPEW(rs2, rs1, rd, op) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rd == 0b00000) 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(__FILE__, __LINE__, "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(__FILE__, __LINE__, "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 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rd == 0b00000) 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(__FILE__, __LINE__, "LOADRES type not implemented in initial_analysis") - }; - }, - STORECON(aq, rl, rs2, rs1, width, rd) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR; - if (rd == 0b00000) 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(__FILE__, __LINE__, "STORECON type not implemented in initial_analysis") - }; - }, - AMO(op, aq, rl, rs2, rs1, width, rd) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR; - if (rd == 0b00000) 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) -} - -$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 == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - RISCV_JAL(imm, rd) => { - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - let offset : bits(64) = sign_extend(imm) in - Nias = [| NIAFP_concrete_address (PC + offset) |]; - ik = IK_branch(); - }, - RISCV_JALR(imm, rs, rd) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - let offset : bits(64) = sign_extend(imm) in - Nias = [| NIAFP_indirect_address() |]; - ik = IK_branch(); - }, - BTYPE(imm, rs2, rs1, op) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - ik = IK_branch(); - let offset : bits(64) = sign_extend(imm) in - Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |]; - }, - ITYPE(imm, rs, rd, op) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - SHIFTIOP(imm, rs, rd, op) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - RTYPE(rs2, rs1, rd, op) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rd == 0b00000) 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 not(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 == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) 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(__FILE__, __LINE__, "LOAD type not implemented in initial_analysis") - } - }, - STORE(imm, rs2, rs1, width, aq, rl) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rs1 == 0b00000) 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(__FILE__, __LINE__, "STORE type not implemented in initial_analysis") - } - }, - ADDIW(imm, rs, rd) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - SHIFTIWOP(imm, rs, rd, op) => { - if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; - if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - }, - RTYPEW(rs2, rs1, rd, op) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rd == 0b00000) 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(__FILE__, __LINE__, "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(__FILE__, __LINE__, "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 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rd == 0b00000) 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(__FILE__, __LINE__, "LOADRES type not implemented in initial_analysis") - }; - }, - STORECON(aq, rl, rs2, rs1, width, rd) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR; - if (rd == 0b00000) 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(__FILE__, __LINE__, "STORECON type not implemented in initial_analysis") - }; - }, - AMO(op, aq, rl, rs2, rs1, width, rd) => { - if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; - if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; - if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR; - if (rd == 0b00000) 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 9c4630b33..25891c94f 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -544,9 +544,6 @@ function effective_fence_set(set : bits(4), fiom : bool) -> bits(4) = { } else set } -/* For future versions of Sail where barriers can be parameterised */ -$ifdef FEATURE_UNION_BARRIER - function clause execute (FENCE(pred, succ)) = { // If the FIOM bit in menvcfg/senvcfg is set then the I/O bits can imply R/W. let fiom = is_fiom_active(); @@ -554,15 +551,15 @@ function clause execute (FENCE(pred, succ)) = { let succ = effective_fence_set(succ, fiom); 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) @ 0b11, _ : bits(2) @ 0b11) => sail_barrier(Barrier_RISCV_rw_rw), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => sail_barrier(Barrier_RISCV_r_rw), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => sail_barrier(Barrier_RISCV_r_r), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => sail_barrier(Barrier_RISCV_rw_w), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => sail_barrier(Barrier_RISCV_w_w), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => sail_barrier(Barrier_RISCV_w_rw), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => sail_barrier(Barrier_RISCV_rw_r), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => sail_barrier(Barrier_RISCV_r_w), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => sail_barrier(Barrier_RISCV_w_r), (_ : bits(4) , _ : bits(2) @ 0b00) => (), (_ : bits(2) @ 0b00, _ : bits(4) ) => (), @@ -573,36 +570,6 @@ function clause execute (FENCE(pred, succ)) = { RETIRE_SUCCESS } -$else - -function clause execute (FENCE(pred, succ)) = { - // If the FIOM bit in menvcfg/senvcfg is set then the I/O bits can imply R/W. - let fiom = is_fiom_active(); - let pred = effective_fence_set(pred, fiom); - let succ = effective_fence_set(succ, fiom); - - 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(4) , _ : bits(2) @ 0b00) => (), - (_ : bits(2) @ 0b00, _ : bits(4) ) => (), - - _ => { print("FIXME: unsupported fence"); - () } - }; - RETIRE_SUCCESS -} - -$endif - mapping bit_maybe_r : bits(1) <-> string = { 0b1 <-> "r", 0b0 <-> "" @@ -636,24 +603,9 @@ 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), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => sail_barrier(Barrier_RISCV_tso), (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (), _ => { print("FIXME: unsupported fence"); @@ -662,8 +614,6 @@ 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) diff --git a/model/riscv_pc_access.sail b/model/riscv_pc_access.sail index d3e54e5d7..a17e86d32 100644 --- a/model/riscv_pc_access.sail +++ b/model/riscv_pc_access.sail @@ -22,6 +22,7 @@ function get_next_pc() = nextPC val set_next_pc : xlenbits -> unit function set_next_pc(pc) = { + sail_branch_announce(sizeof(xlen), pc); nextPC = pc } diff --git a/model/riscv_step.sail b/model/riscv_step.sail index 012f63b4d..69d2b8cda 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -47,6 +47,7 @@ function step(step_no : int) -> bool = { }, /* non-error cases: */ F_RVC(h) => { + sail_instr_announce(h); instbits = zero_extend(h); let ast = ext_decode_compressed(h); if get_config_print_instr() @@ -63,6 +64,7 @@ function step(step_no : int) -> bool = { } }, F_Base(w) => { + sail_instr_announce(w); instbits = zero_extend(w); let ast = ext_decode(w); if get_config_print_instr() @@ -96,7 +98,10 @@ function loop () : unit -> unit = { step_no : int = 0; while not(htif_done) do { let stepped = step(step_no); - if stepped then step_no = step_no + 1; + if stepped then { + step_no = step_no + 1; + sail_end_cycle() + }; /* check htif exit */ if htif_done then {