diff options
| -rw-r--r-- | Makefile | 20 | ||||
| -rw-r--r-- | model/main.sail | 10 | ||||
| -rw-r--r-- | model/prelude.sail | 29 | ||||
| -rw-r--r-- | model/riscv_insts_base.sail | 26 | ||||
| -rw-r--r-- | model/riscv_mem.sail | 70 | ||||
| -rw-r--r-- | model/riscv_platform.sail | 32 | ||||
| -rw-r--r-- | model/riscv_sys_control.sail | 10 | ||||
| -rw-r--r-- | ocaml_emulator/platform.ml | 12 |
8 files changed, 116 insertions, 93 deletions
@@ -280,15 +280,27 @@ endif generated_definitions/coq/$(ARCH)/riscv.vo: generated_definitions/coq/$(ARCH)/riscv_types.vo handwritten_support/riscv_extras.vo generated_definitions/coq/$(ARCH)/riscv_duopod.vo: generated_definitions/coq/$(ARCH)/riscv_duopod_types.vo handwritten_support/riscv_extras.vo -riscv_rmem: generated_definitions/lem-for-rmem/riscv.lem +echo_rmem_srcs: + echo $(SAIL_RMEM_SRCS) + +riscv_rmem: generated_definitions/for-rmem/riscv.lem +riscv_rmem: generated_definitions/for-rmem/riscv_toFromInterp2.ml +riscv_rmem: generated_definitions/for-rmem/riscv.defs .PHONY: riscv_rmem -generated_definitions/lem-for-rmem/riscv.lem: SAIL_FLAGS += -lem_lib Riscv_extras -generated_definitions/lem-for-rmem/riscv.lem: $(SAIL_RMEM_SRCS) +generated_definitions/for-rmem/riscv.lem: SAIL_FLAGS += -lem_lib Riscv_extras +generated_definitions/for-rmem/riscv.lem: $(SAIL_RMEM_SRCS) mkdir -p $(dir $@) # We do not need the isabelle .thy files, but sail always generates them $(SAIL) $(SAIL_FLAGS) -lem -lem_mwords -lem_output_dir $(dir $@) -isa_output_dir $(dir $@) -o $(notdir $(basename $@)) $^ +generated_definitions/for-rmem/riscv_toFromInterp2.ml: $(SAIL_RMEM_SRCS) + mkdir -p $(dir $@) + $(SAIL) $(SAIL_FLAGS) -tofrominterp -tofrominterp_lem -tofrominterp_output_dir $(dir $@) -o riscv $^ + +generated_definitions/for-rmem/riscv.defs: $(SAIL_RMEM_SRCS) + mkdir -p $(dir $@) + $(SAIL) $(SAIL_FLAGS) -marshal -o $(basename $@) $^ # we exclude prelude.sail here, most code there should move to sail lib #LOC_FILES:=$(SAIL_SRCS) main.sail @@ -297,7 +309,7 @@ generated_definitions/lem-for-rmem/riscv.lem: $(SAIL_RMEM_SRCS) clean: -rm -rf generated_definitions/ocaml/* generated_definitions/c/* generated_definitions/latex/* -rm -rf generated_definitions/lem/* generated_definitions/isabelle/* generated_definitions/hol4/* generated_definitions/coq/* - -rm -rf generated_definitions/lem-for-rmem/* + -rm -rf generated_definitions/for-rmem/* -rm -f c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64 c_emulator/riscv_rvfi -rm -rf ocaml_emulator/_sbuild ocaml_emulator/_build ocaml_emulator/riscv_ocaml_sim_RV32 ocaml_emulator/riscv_ocaml_sim_RV64 ocaml_emulator/tracecmp -rm -f *.gcno *.gcda diff --git a/model/main.sail b/model/main.sail index a0965f6..c349b3f 100644 --- a/model/main.sail +++ b/model/main.sail @@ -1,13 +1,3 @@ -val elf_tohost = { - ocaml: "Elf_loader.elf_tohost", - c: "elf_tohost" -} : unit -> int - -val elf_entry = { - ocaml: "Elf_loader.elf_entry", - c: "elf_entry" -} : unit -> int - val main : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg} function main () = { diff --git a/model/prelude.sail b/model/prelude.sail index 59289ed..457c4d4 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -5,6 +5,7 @@ $include <option.sail> $include <arith.sail> $include <string.sail> $include <vector_dec.sail> +$include <regfp.sail> val string_startswith = "string_startswith" : (string, string) -> bool val string_drop = "string_drop" : (string, nat) -> string @@ -12,7 +13,7 @@ val string_take = "string_take" : (string, nat) -> string val string_length = "string_length" : string -> nat val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string -val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", coq: "generic_eq"} : forall ('a : Type). ('a, 'a) -> bool +val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq"} : forall ('a : Type). ('a, 'a) -> bool overload operator == = {eq_string, eq_anything} @@ -25,7 +26,7 @@ val any_vector_update = {ocaml: "update", lem: "update_list_dec", coq: "vector_u overload vector_update = {any_vector_update} -val update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. +val update_subrange = {ocaml: "update_subrange", interpreter: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type). @@ -47,11 +48,11 @@ function neq_anything (x, y) = not_bool(x == y) overload operator != = {neq_vec, neq_anything} -val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec", ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) +val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec", ocaml: "and_vec", interpreter: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) overload operator & = {and_vec} -val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec", ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) +val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec", ocaml: "or_vec", interpreter: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) overload operator | = {or_vec} @@ -71,7 +72,7 @@ val BitStr = "string_of_bits" : forall 'n. bits('n) -> string val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) -val int_power = {ocaml: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int +val int_power = {ocaml: "int_power", interpreter: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int overload operator ^ = {xor_vec, int_power, concat_str} @@ -81,19 +82,19 @@ val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), overload operator - = {sub_vec, sub_vec_int} -val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int"} : (int, int) -> int -val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int +val quot_round_zero = {ocaml: "quot_round_zero", interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int"} : (int, int) -> int +val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int /* The following should get us euclidean modulus, and is compatible with pre and post 0.9 versions of sail */ overload operator % = {emod_int, mod} val min_nat = {ocaml: "min_int", lem: "min", coq: "min_nat", c: "min_int"} : (nat, nat) -> nat -val min_int = {ocaml: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int +val min_int = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int -val max_nat = {ocaml: "max_int", lem: "max", coq: "max_nat", c: "max_int"} : (nat, nat) -> nat +val max_nat = {ocaml: "max_int", interpreter: "max_int", lem: "max", coq: "max_nat", c: "max_int"} : (nat, nat) -> nat -val max_int = {ocaml: "max_int", lem: "max", coq: "Z.max", c: "max_int"} : (int, int) -> int +val max_int = {ocaml: "max_int", interpreter: "max_int", lem: "max", coq: "Z.max", c: "max_int"} : (int, int) -> int overload min = {min_nat, min_int} @@ -104,10 +105,10 @@ val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) val print = "print_endline" : string -> unit val print_string = "print_string" : (string, string) -> unit -val print_instr = {ocaml: "Platform.print_instr", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_reg = {ocaml: "Platform.print_reg", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_mem = {ocaml: "Platform.print_mem_access", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_platform = {ocaml: "Platform.print_platform", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_instr = {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_reg = {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_mem = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit $ifndef FEATURE_IMPLICITS val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index bbf8aff..8ae4923 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -208,7 +208,7 @@ mapping shiftiop_mnemonic : sop <-> string = { } mapping clause assembly = SHIFTIOP(shamt, rs1, rd, op) - <-> shiftiop_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ hex_bits_6(shamt) + <-> shiftiop_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_6(shamt) /* ****************************************************************** */ union clause ast = RTYPE : (regbits, regbits, regbits, rop) @@ -525,7 +525,7 @@ mapping shiftiwop_mnemonic : sopw <-> string = { mapping clause assembly = SHIFTIWOP(shamt, rs1, rd, op) if sizeof(xlen) == 64 - <-> shiftiwop_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ hex_bits_5(shamt) + <-> shiftiwop_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt) if sizeof(xlen) == 64 /* ****************************************************************** */ @@ -536,15 +536,15 @@ mapping clause encdec = FENCE(pred, succ) function clause execute (FENCE(pred, succ)) = { match (pred, succ) { - (_ : 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) @ 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) => (), @@ -589,7 +589,7 @@ mapping clause encdec = FENCE_TSO(pred, succ) function clause execute (FENCE_TSO(pred, succ)) = { match (pred, succ) { - (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => MEM_fence_tso(), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso), (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (), _ => { print("FIXME: unsupported fence"); @@ -608,7 +608,7 @@ mapping clause encdec = FENCEI() <-> 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111 /* fence.i is a nop for the memory model */ -function clause execute FENCEI() = { /* MEM_fence_i(); */ true } +function clause execute FENCEI() = { /* __barrier(Barrier_RISCV_i); */ true } mapping clause assembly = FENCEI() <-> "fence.i" diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 1ccb5c7..7e31659 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -8,13 +8,24 @@ function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool unsigned(addr) % width == 0 // only used for actual memory regions, to avoid MMIO effects -function phys_mem_read forall 'n, 'n >= 0. (t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) = - match (t, __RISCV_read(addr, width, aq, rl, res)) { +function phys_mem_read forall 'n, 'n > 0. (t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) = { + let result = (match (aq, rl, res) { + (false, false, false) => Some(__read_mem(Read_plain, addr, width)), + (true, false, false) => Some(__read_mem(Read_RISCV_acquire, addr, width)), + (true, true, false) => Some(__read_mem(Read_RISCV_strong_acquire, addr, width)), + (false, false, true) => Some(__read_mem(Read_RISCV_reserved, addr, width)), + (true, false, true) => Some(__read_mem(Read_RISCV_reserved_acquire, addr, width)), + (true, true, true) => Some(__read_mem(Read_RISCV_reserved_strong_acquire, addr, width)), + (false, true, false) => None(), /* should these be instead throwing error_not_implemented as below? */ + (false, true, true) => None() + }) : option(bits(8 * 'n)); + match (t, result) { (Instruction, None()) => MemException(E_Fetch_Access_Fault), (Data, None()) => MemException(E_Load_Access_Fault), (_, Some(v)) => { print_mem("mem[" ^ t ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v)); MemValue(v) } } +} function checked_mem_read forall 'n, 'n > 0. (t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) = /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */ @@ -65,40 +76,37 @@ function mem_read (addr, width, aq, rl, res) = { result } -val MEMea = {lem: "MEMea", coq: "MEMea", _: "memea"} : forall 'n. - (xlenbits, atom('n)) -> unit effect {eamem} -val MEMea_release = {lem: "MEMea_release", coq: "MEMea_release", _: "memea"} : forall 'n. - (xlenbits, atom('n)) -> unit effect {eamem} -val MEMea_strong_release = {lem: "MEMea_strong_release", coq: "MEMea_strong_release", _: "memea"} : forall 'n. - (xlenbits, atom('n)) -> unit effect {eamem} -val MEMea_conditional = {lem: "MEMea_conditional", coq: "MEMea_conditional", _: "memea"} : forall 'n. - (xlenbits, atom('n)) -> unit effect {eamem} -val MEMea_conditional_release = {lem: "MEMea_conditional_release", coq: "MEMea_conditional_release", _: "memea"} : forall 'n. - (xlenbits, atom('n)) -> unit effect {eamem} -val MEMea_conditional_strong_release = {lem: "MEMea_conditional_strong_release", coq: "MEMea_conditional_strong_release", _: "memea"} : forall 'n. - (xlenbits, atom('n)) -> unit effect {eamem} - -val mem_write_ea : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape} +val mem_write_ea : forall 'n, 'n > 0. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape} function mem_write_ea (addr, width, aq, rl, con) = { if (rl | con) & (~ (is_aligned_addr(addr, width))) then MemException(E_SAMO_Addr_Align) else match (aq, rl, con) { - (false, false, false) => MemValue(MEMea(addr, width)), - (false, true, false) => MemValue(MEMea_release(addr, width)), - (false, false, true) => MemValue(MEMea_conditional(addr, width)), - (false, true , true) => MemValue(MEMea_conditional_release(addr, width)), + (false, false, false) => MemValue(__write_mem_ea(Write_plain, addr, width)), + (false, true, false) => MemValue(__write_mem_ea(Write_RISCV_release, addr, width)), + (false, false, true) => MemValue(__write_mem_ea(Write_RISCV_conditional, addr, width)), + (false, true , true) => MemValue(__write_mem_ea(Write_RISCV_conditional_release, addr, width)), (true, false, false) => throw(Error_not_implemented("store.aq")), - (true, true, false) => MemValue(MEMea_strong_release(addr, width)), + (true, true, false) => MemValue(__write_mem_ea(Write_RISCV_strong_release, addr, width)), (true, false, true) => throw(Error_not_implemented("sc.aq")), - (true, true , true) => MemValue(MEMea_conditional_strong_release(addr, width)) + (true, true , true) => MemValue(__write_mem_ea(Write_RISCV_conditional_strong_release, addr, width)) } } // only used for actual memory regions, to avoid MMIO effects -function phys_mem_write forall 'n. (addr : xlenbits, width : atom('n), data: bits(8 * 'n), aq : bool, rl : bool, con : bool) -> MemoryOpResult(bool) = { +function phys_mem_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data : bits(8 * 'n), aq : bool, rl : bool, con : bool) -> MemoryOpResult(bool) = { + let result = (match (aq, rl, con) { + (false, false, false) => MemValue(__write_mem(Write_plain, addr, width, data)), + (false, true, false) => MemValue(__write_mem(Write_RISCV_release, addr, width, data)), + (false, false, true) => MemValue(__write_mem(Write_RISCV_conditional, addr, width, data)), + (false, true , true) => MemValue(__write_mem(Write_RISCV_conditional_release, addr, width, data)), + (true, false, false) => throw(Error_not_implemented("store.aq")), + (true, true, false) => MemValue(__write_mem(Write_RISCV_strong_release, addr, width, data)), + (true, false, true) => throw(Error_not_implemented("sc.aq")), + (true, true , true) => MemValue(__write_mem(Write_RISCV_conditional_strong_release, addr, width, data)) + }) : MemoryOpResult(bool); print_mem("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data)); - MemValue(__RISCV_write(addr, width, data, aq, rl, con)) + result } // dispatches to MMIO regions or physical memory regions depending on physical memory map @@ -138,17 +146,3 @@ function mem_write_value (addr, width, value, aq, rl, con) = { (_, _, _) => checked_mem_write(addr, width, value, aq, rl, con) } } - -val MEM_fence_rw_rw = {lem: "MEM_fence_rw_rw", coq: "MEM_fence_rw_rw", _: "skip"} : unit -> unit effect {barr} -val MEM_fence_r_rw = {lem: "MEM_fence_r_rw", coq: "MEM_fence_r_rw", _: "skip"} : unit -> unit effect {barr} -val MEM_fence_r_r = {lem: "MEM_fence_r_r", coq: "MEM_fence_r_r", _: "skip"} : unit -> unit effect {barr} -val MEM_fence_rw_w = {lem: "MEM_fence_rw_w", coq: "MEM_fence_rw_w", _: "skip"} : unit -> unit effect {barr} -val MEM_fence_w_w = {lem: "MEM_fence_w_w", coq: "MEM_fence_w_w", _: "skip"} : unit -> unit effect {barr} -val MEM_fence_w_rw = {lem: "MEM_fence_w_rw", coq: "MEM_fence_w_rw", _: "skip"} : unit -> unit effect {barr} -val MEM_fence_rw_r = {lem: "MEM_fence_rw_r", coq: "MEM_fence_rw_r", _: "skip"} : unit -> unit effect {barr} -val MEM_fence_r_w = {lem: "MEM_fence_r_w", coq: "MEM_fence_r_w", _: "skip"} : unit -> unit effect {barr} -val MEM_fence_w_r = {lem: "MEM_fence_w_r", coq: "MEM_fence_w_r", _: "skip"} : unit -> unit effect {barr} - -val MEM_fence_tso = {lem: "MEM_fence_tso", coq: "MEM_fence_tso", _: "skip"} : unit -> unit effect {barr} - -val MEM_fence_i = {lem: "MEM_fence_i", coq: "MEM_fence_i", _: "skip"} : unit -> unit effect {barr} diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 015131c..437c41d 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -3,15 +3,28 @@ /* Current constraints on this implementation are: - it cannot access memory directly, but instead provides definitions for the physical memory model - it can access system register state, needed to manipulate interrupt bits - - it relies on externs to get platform address information and doesn't hardcode them. + - it relies on externs to get platform address information and doesn't hardcode them */ +val elf_tohost = { + ocaml: "Elf_loader.elf_tohost", + interpreter: "Elf_loader.elf_tohost", + c: "elf_tohost" +} : unit -> int + +val elf_entry = { + ocaml: "Elf_loader.elf_entry", + interpreter: "Elf_loader.elf_entry", + c: "elf_entry" +} : unit -> int + /* Main memory */ -val plat_ram_base = {c: "plat_ram_base", ocaml: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits -val plat_ram_size = {c: "plat_ram_size", ocaml: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits +val plat_ram_base = {c: "plat_ram_base", ocaml: "Platform.dram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits +val plat_ram_size = {c: "plat_ram_size", ocaml: "Platform.dram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits /* whether the MMU should update dirty bits in PTEs */ val plat_enable_dirty_update = {ocaml: "Platform.enable_dirty_update", + interpreter: "Platform.enable_dirty_update", c: "plat_enable_dirty_update", lem: "plat_enable_dirty_update"} : unit -> bool @@ -19,24 +32,27 @@ val plat_enable_dirty_update = {ocaml: "Platform.enable_dirty_update", * misaligned loads/stores are trapped to Machine mode. */ val plat_enable_misaligned_access = {ocaml: "Platform.enable_misaligned_access", + interpreter: "Platform.enable_misaligned_access", c: "plat_enable_misaligned_access", lem: "plat_enable_misaligned_access"} : unit -> bool /* whether mtval stores the bits of a faulting instruction on illegal instruction exceptions */ val plat_mtval_has_illegal_inst_bits = {ocaml: "Platform.mtval_has_illegal_inst_bits", + interpreter: "Platform.mtval_has_illegal_inst_bits", c: "plat_mtval_has_illegal_inst_bits", lem: "plat_mtval_has_illegal_inst_bits"} : unit -> bool /* ROM holding reset vector and device-tree DTB */ -val plat_rom_base = {ocaml: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> xlenbits -val plat_rom_size = {ocaml: "Platform.rom_size", c: "plat_rom_size", lem: "plat_rom_size"} : unit -> xlenbits +val plat_rom_base = {ocaml: "Platform.rom_base", interpreter: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> xlenbits +val plat_rom_size = {ocaml: "Platform.rom_size", interpreter: "Platform.rom_size", c: "plat_rom_size", lem: "plat_rom_size"} : unit -> xlenbits /* Location of clock-interface, which should match with the spec in the DTB */ -val plat_clint_base = {ocaml: "Platform.clint_base", c: "plat_clint_base", lem: "plat_clint_base"} : unit -> xlenbits -val plat_clint_size = {ocaml: "Platform.clint_size", c: "plat_clint_size", lem: "plat_clint_size"} : unit -> xlenbits +val plat_clint_base = {ocaml: "Platform.clint_base", interpreter: "Platform.clint_base", c: "plat_clint_base", lem: "plat_clint_base"} : unit -> xlenbits +val plat_clint_size = {ocaml: "Platform.clint_size", interpreter: "Platform.clint_size", c: "plat_clint_size", lem: "plat_clint_size"} : unit -> xlenbits /* Location of HTIF ports */ val plat_htif_tohost = {ocaml: "Platform.htif_tohost", c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits +function plat_htif_tohost () = to_bits(64, elf_tohost ()) // todo: fromhost val phys_mem_segments : unit -> list((xlenbits, xlenbits)) @@ -91,7 +107,7 @@ function within_htif_readable forall 'n. (addr : xlenbits, width : atom('n)) -> /* CLINT (Core Local Interruptor), based on Spike. */ -val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick", c: "plat_insns_per_tick", lem: "plat_insns_per_tick"} : unit -> int +val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick", interpreter: "Platform.insns_per_tick", c: "plat_insns_per_tick", lem: "plat_insns_per_tick"} : unit -> int // assumes a single hart, since this typically is a vector of per-hart registers. register mtimecmp : bits(64) // memory-mapped internal clint register. diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 48a3d90..4155d66 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -114,13 +114,11 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool = * where cancellation can be performed. */ -val speculate_conditional = {ocaml: "Platform.speculate_conditional", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool effect {exmem} +val speculate_conditional = {ocaml: "Platform.speculate_conditional", interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool effect {exmem} -val load_reservation = {ocaml: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit - -val match_reservation = {ocaml: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool - -val cancel_reservation = {ocaml: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit +val load_reservation = {ocaml: "Platform.load_reservation", interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit +val match_reservation = {ocaml: "Platform.match_reservation", interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool +val cancel_reservation = {ocaml: "Platform.cancel_reservation", interpreter: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit /* Exception delegation: given an exception and the privilege at which * it occured, returns the privilege at which it should be handled. diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index 2c0125b..95e7c57 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -106,6 +106,18 @@ let cancel_reservation () = print_platform (Printf.sprintf "reservation <- none\n"); reservation := "none" +let read_mem (rk, addr, len) = + Sail_lib.fast_read_ram (len, addr) + +let write_mem_ea _ = () + +let write_mem (wk, addr, len, value) = + Sail_lib.write_ram' (len, Sail_lib.uint addr, value); true + +let excl_res _ = true + +let barrier _ = () + (* terminal I/O *) let term_write char_bits = |