From 7c9bbc93579ada9a64dfe80838dae32b6168e85b Mon Sep 17 00:00:00 2001 From: Martin Berger Date: Fri, 5 Nov 2021 12:45:03 +0000 Subject: Delete riscv_iris.sail File is no longer needed, as per this discussion: https://github.com/riscv/sail-riscv/issues/119 --- model/riscv_iris.sail | 1244 ------------------------------------------------- 1 file changed, 1244 deletions(-) delete mode 100644 model/riscv_iris.sail diff --git a/model/riscv_iris.sail b/model/riscv_iris.sail deleted file mode 100644 index 191215e..0000000 --- a/model/riscv_iris.sail +++ /dev/null @@ -1,1244 +0,0 @@ -/*=======================================================================================*/ -/* RISCV Sail Model */ -/* */ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except for the snapshots of the Lem and Sail libraries */ -/* in the prover_snapshots directory (which include copies of their */ -/* licences), is subject to the BSD two-clause licence below. */ -/* */ -/* Copyright (c) 2017-2021 */ -/* Prashanth Mundkur */ -/* Rishiyur S. Nikhil and Bluespec, Inc. */ -/* Jon French */ -/* Brian Campbell */ -/* Robert Norton-Wright */ -/* Alasdair Armstrong */ -/* Thomas Bauereiss */ -/* Shaked Flur */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alexander Richardson */ -/* Hesham Almatary */ -/* Jessica Clarke */ -/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ -/* Peter Rugg */ -/* Aril Computer Corp., for contributions by Scott Johnson */ -/* */ -/* All rights reserved. */ -/* */ -/* This software was developed by the above within the Rigorous */ -/* Engineering of Mainstream Systems (REMS) project, partly funded by */ -/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ -/* Edinburgh. */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ -/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ -/* SSITH research programme. */ -/* */ -/* This project has received funding from the European Research Council */ -/* (ERC) under the European Union’s Horizon 2020 research and innovation */ -/* programme (grant agreement 789108, ELVER). */ -/* */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in */ -/* the documentation and/or other materials provided with the */ -/* distribution. */ -/* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ -/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ -/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ -/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ -/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ -/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ -/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ -/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ -/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ -/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ -/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ -/* SUCH DAMAGE. */ -/*=======================================================================================*/ - -default Order dec - -$include -$include -$include -$include -$include -$include - -val string_startswith = "string_startswith" : (string, string) -> bool -val string_drop = "string_drop" : (string, nat) -> string -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)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq", c: "eq_anything"} : forall ('a : Type). ('a, 'a) -> bool - -overload operator == = {eq_string, eq_anything} - -val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} -/* sneaky deref with no effect necessary for bitfield writes */ -val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a - -val any_vector_update = {ocaml: "update", lem: "update_list_dec", coq: "vector_update"} : forall 'n ('a : Type). - (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) - -overload vector_update = {any_vector_update} - -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", coq: "vec_concat"} : forall ('n : Int) ('m : Int) ('a : Type). - (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a) - -overload append = {vector_concat} - -overload ~ = {not_bool, not_vec} - -val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool - -function neq_vec (x, y) = not_bool(eq_bits(x, y)) - -val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool - -function neq_anything (x, y) = not_bool(x == y) - -overload operator != = {neq_vec, neq_anything} - -overload operator & = {and_vec} - -overload operator | = {or_vec} - -val string_of_int = {c: "string_of_int", ocaml: "string_of_int", interpreter: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string - -val "string_of_bits" : forall 'n. bits('n) -> string - -function string_of_bit(b: bit) -> string = - match b { - bitzero => "0b0", - bitone => "0b1" - } - -overload BitStr = {string_of_bits, string_of_bit} - -val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) - -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} - -val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) - -val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), int) -> bits('n) - -overload operator - = {sub_vec, sub_vec_int} - -val quot_round_zero = {ocaml: "quot_round_zero", interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int -val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (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", interpreter: "min_int", lem: "min", coq: "min_nat", c: "min_int"} : (nat, nat) -> nat - -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", interpreter: "max_int", lem: "max", coq: "max_nat", c: "max_int"} : (nat, nat) -> nat - -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} - -overload max = {max_nat, max_int} - -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", 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 - -val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool -val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool -val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool - -val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool -// defaults for other backends -function get_config_print_instr () = false -function get_config_print_reg () = false -function get_config_print_mem () = false -function get_config_print_platform () = false - -val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) -val EXTZ : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) - -function EXTS(m, v) = sail_sign_extend(v, m) -function EXTZ(m, v) = sail_zero_extend(v, m) - -val zeros_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n) -function zeros_implicit (n) = sail_zeros(n) -overload zeros = {zeros_implicit} - -val ones : forall 'n, 'n >= 0 . implicit('n) -> bits('n) -function ones (n) = sail_ones (n) - -val bool_to_bits : bool -> bits(1) -function bool_to_bits x = if x then 0b1 else 0b0 - -val bit_to_bool : bit -> bool -function bit_to_bool b = match b { - bitone => true, - bitzero => false -} - -val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l) -function to_bits (l, n) = get_slice_int(l, n, 0) - -infix 4 <_s -infix 4 >=_s -infix 4 <_u -infix 4 >=_u -infix 4 <=_u - -val operator <_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool -val operator >=_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool -val operator <_u : forall 'n. (bits('n), bits('n)) -> bool -val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool -val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool - -function operator <_s (x, y) = signed(x) < signed(y) -function operator >=_s (x, y) = signed(x) >= signed(y) -function operator <_u (x, y) = unsigned(x) < unsigned(y) -function operator >=_u (x, y) = unsigned(x) >= unsigned(y) -function operator <=_u (x, y) = unsigned(x) <= unsigned(y) - -infix 7 >> -infix 7 << - -val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) -val "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) - -val "shiftl" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m) -val "shiftr" : forall 'm 'n, 'n >= 0. (bits('m), atom('n)) -> bits('m) - -overload operator >> = {shift_bits_right, shiftr} -overload operator << = {shift_bits_left, shiftl} - -/* Ideally these would be sail builtin */ - -function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) = - let v128 : bits(128) = EXTS(v) in - (v128 >> shift)[63..0] - -function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) = - let v64 : bits(64) = EXTS(v) in - (v64 >> shift)[31..0] - -val "decimal_string_of_bits" : forall 'n. bits('n) -> string -val hex_bits : forall 'n . (atom('n), bits('n)) <-> string - -/* Define the XLEN value for the architecture. */ - -type xlen : Int = 64 -type xlen_bytes : Int = 8 -type xlenbits = bits(xlen) -/* The default metadata carries no information, and is implemented - * using a unit type. - */ - -type mem_meta = unit - -let default_meta : mem_meta = () - -val __WriteRAM_Meta : forall 'n. (xlenbits, atom('n), mem_meta) -> unit effect {wmvt} -function __WriteRAM_Meta(addr, width, meta) = () - -val __ReadRAM_Meta : forall 'n. (xlenbits, atom('n)) -> mem_meta effect {rmem} -function __ReadRAM_Meta(addr, width) = () -/* These functions define the primitives for physical memory access. - * They depend on the XLEN of the architecture. - * - * 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. - */ - - -/* This is a slightly arbitrary limit on the maximum number of bytes - in a memory access. It helps to generate slightly better C code - because it means width argument can be fast native integer. It - would be even better if it could be <= 8 bytes so that data can - also be a 64-bit int but CHERI needs 128-bit accesses for - 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, atom('n), bits(8 * 'n), mem_meta) -> bool effect {wmv, wmvt} - -val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n)) -> unit effect {eamem} -function write_ram_ea(wk, addr, width) = - __write_mem_ea(wk, sizeof(xlen), addr, width) - -val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access . (read_kind, xlenbits, atom('n), bool) -> (bits(8 * 'n), mem_meta) effect {rmem, rmemt} -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) - - -/* Basic type and function definitions used pervasively in the model. */ - -/* this value is only defined for the runtime platform for ELF loading - * checks, and not used in the model. - */ -let xlen_val = sizeof(xlen) - -let xlen_max_unsigned = 2 ^ sizeof(xlen) - 1 -let xlen_max_signed = 2 ^ (sizeof(xlen) - 1) - 1 -let xlen_min_signed = 0 - 2 ^ (sizeof(xlen) - 1) - -type half = bits(16) -type word = bits(32) - -/* register identifiers */ - -type regidx = bits(5) -type cregidx = bits(3) /* identifiers in RVC instructions */ -type csreg = bits(12) /* CSR addressing */ - -/* register file indexing */ - -type regno ('n : Int), 0 <= 'n < 32 = atom('n) - -val regidx_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)} -function regidx_to_regno b = let 'r = unsigned(b) in r - -/* mapping RVC register indices into normal indices */ -val creg2reg_idx : cregidx -> regidx -function creg2reg_idx(creg) = 0b01 @ creg - -/* some architecture and ABI relevant register identifiers */ -let zreg : regidx = 0b00000 /* x0, zero register */ -let ra : regidx = 0b00001 /* x1, return address */ -let sp : regidx = 0b00010 /* x2, stack pointer */ - -/* instruction fields */ - -type opcode = bits(7) -type imm12 = bits(12) -type imm20 = bits(20) -type amo = bits(1) /* amo opcode flags */ - -/* base architecture definitions */ - -enum Architecture = {RV32, RV64, RV128} -type arch_xlen = bits(2) -function architecture(a : arch_xlen) -> option(Architecture) = - match (a) { - 0b01 => Some(RV32), - 0b10 => Some(RV64), - 0b11 => Some(RV128), - _ => None() - } - -function arch_to_bits(a : Architecture) -> arch_xlen = - match (a) { - RV32 => 0b01, - RV64 => 0b10, - RV128 => 0b11 - } - -/* enum denoting whether an executed instruction retires */ - -enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL} - -/* memory access types */ - -union AccessType ('a : Type) = { - Read : 'a, - Write : 'a, - ReadWrite : ('a, 'a), - Execute : unit -} - -enum word_width = {BYTE, HALF, WORD, DOUBLE} -/* model-internal exceptions */ - -union exception = { - Error_not_implemented : string, - Error_internal_error : unit -} - -val not_implemented : forall ('a : Type). string -> 'a effect {escape} -function not_implemented message = throw(Error_not_implemented(message)) - -val internal_error : forall ('a : Type). string -> 'a effect {escape} -function internal_error(s) = { - assert (false, s); - throw Error_internal_error() -} - -/* instruction opcode grouping */ -enum bop = {RISCV_BEQ, RISCV_BNE, RISCV_BLT, - RISCV_BGE, RISCV_BLTU, RISCV_BGEU} /* branch ops */ -enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, - RISCV_XORI, RISCV_ORI, RISCV_ANDI} /* immediate ops */ - -mapping bool_bits : bool <-> bits(1) = { - true <-> 0b1, - false <-> 0b0 -} - -mapping bool_not_bits : bool <-> bits(1) = { - true <-> 0b0, - false <-> 0b1 -} - -mapping size_bits : word_width <-> bits(2) = { - BYTE <-> 0b00, - HALF <-> 0b01, - WORD <-> 0b10, - DOUBLE <-> 0b11 -} - -val word_width_bytes : word_width -> {'s, 's == 1 | 's == 2 | 's == 4 | 's == 8 . atom('s)} -function word_width_bytes width = match width { - BYTE => 1, - HALF => 2, - WORD => 4, - DOUBLE => 8 -} -// Extensions for memory Accesstype. - -type ext_access_type = unit - -let Data : ext_access_type = () - -let default_write_acc : ext_access_type = Data - -val accessType_to_str : AccessType(ext_access_type) -> string -function accessType_to_str (a) = - match (a) { - Read(Data) => "R", - Write(Data) => "W", - ReadWrite(Data, Data) => "RW", - Execute() => "X" - } - -overload to_str = {accessType_to_str} -/* default register type */ -type regtype = xlenbits - -/* default zero register */ -let zero_reg : regtype = EXTZ(0x0) - -/* default register printer */ -val RegStr : regtype -> string -function RegStr(r) = BitStr(r) - -/* conversions */ - -val regval_from_reg : regtype -> xlenbits -function regval_from_reg(r) = r - -val regval_into_reg : xlenbits -> regtype -function regval_into_reg(v) = v -/* program counter */ - -register PC : xlenbits -register nextPC : xlenbits - -/* internal state to hold instruction bits for faulting instructions */ -register instbits : xlenbits - -/* register file and accessors */ - -register Xs : vector(32, dec, regtype) - -register x1 : regtype -register x2 : regtype -register x3 : regtype -register x4 : regtype -register x5 : regtype -register x6 : regtype -register x7 : regtype -register x8 : regtype -register x9 : regtype -register x10 : regtype -register x11 : regtype -register x12 : regtype -register x13 : regtype -register x14 : regtype -register x15 : regtype -register x16 : regtype -register x17 : regtype -register x18 : regtype -register x19 : regtype -register x20 : regtype -register x21 : regtype -register x22 : regtype -register x23 : regtype -register x24 : regtype -register x25 : regtype -register x26 : regtype -register x27 : regtype -register x28 : regtype -register x29 : regtype -register x30 : regtype -register x31 : regtype - -val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg, escape} -function rX r = { - let v : regtype = - match r { - 0 => zero_reg, - 1 => x1, - 2 => x2, - 3 => x3, - 4 => x4, - 5 => x5, - 6 => x6, - 7 => x7, - 8 => x8, - 9 => x9, - 10 => x10, - 11 => x11, - 12 => x12, - 13 => x13, - 14 => x14, - 15 => x15, - 16 => x16, - 17 => x17, - 18 => x18, - 19 => x19, - 20 => x20, - 21 => x21, - 22 => x22, - 23 => x23, - 24 => x24, - 25 => x25, - 26 => x26, - 27 => x27, - 28 => x28, - 29 => x29, - 30 => x30, - 31 => x31, - _ => {assert(false, "invalid register number"); zero_reg} - }; - regval_from_reg(v) -} - -val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg, escape} -function wX (r, in_v) = { - let v = regval_into_reg(in_v); - match r { - 0 => (), - 1 => x1 = v, - 2 => x2 = v, - 3 => x3 = v, - 4 => x4 = v, - 5 => x5 = v, - 6 => x6 = v, - 7 => x7 = v, - 8 => x8 = v, - 9 => x9 = v, - 10 => x10 = v, - 11 => x11 = v, - 12 => x12 = v, - 13 => x13 = v, - 14 => x14 = v, - 15 => x15 = v, - 16 => x16 = v, - 17 => x17 = v, - 18 => x18 = v, - 19 => x19 = v, - 20 => x20 = v, - 21 => x21 = v, - 22 => x22 = v, - 23 => x23 = v, - 24 => x24 = v, - 25 => x25 = v, - 26 => x26 = v, - 27 => x27 = v, - 28 => x28 = v, - 29 => x29 = v, - 30 => x30 = v, - 31 => x31 = v, - _ => assert(false, "invalid register number") - }; - if (r != 0) then { - if get_config_print_reg() - then print_reg("x" ^ string_of_int(r) ^ " <- " ^ RegStr(v)); - } -} - -function rX_bits(i: bits(5)) -> xlenbits = rX(unsigned(i)) - -function wX_bits(i: bits(5), data: xlenbits) -> unit = { - wX(unsigned(i)) = data -} - -overload X = {rX_bits, wX_bits, rX, wX} - -val init_base_regs : unit -> unit effect {wreg} -function init_base_regs () = { - x1 = zero_reg; - x2 = zero_reg; - x3 = zero_reg; - x4 = zero_reg; - x5 = zero_reg; - x6 = zero_reg; - x7 = zero_reg; - x8 = zero_reg; - x9 = zero_reg; - x10 = zero_reg; - x11 = zero_reg; - x12 = zero_reg; - x13 = zero_reg; - x14 = zero_reg; - x15 = zero_reg; - x16 = zero_reg; - x17 = zero_reg; - x18 = zero_reg; - x19 = zero_reg; - x20 = zero_reg; - x21 = zero_reg; - x22 = zero_reg; - x23 = zero_reg; - x24 = zero_reg; - x25 = zero_reg; - x26 = zero_reg; - x27 = zero_reg; - x28 = zero_reg; - x29 = zero_reg; - x30 = zero_reg; - x31 = zero_reg -} -/* accessors for default architectural addresses, for use from within instructions */ - -/*! - Retrieves the architectural PC value. This is not necessarily the value - found in the PC register as extensions may choose to override this function. - The value in the PC register is the absolute virtual address of the instruction - to fetch. - */ -val get_arch_pc : unit -> xlenbits effect {rreg} -function get_arch_pc() = PC - -val get_next_pc : unit -> xlenbits effect {rreg} -function get_next_pc() = nextPC - -val set_next_pc : xlenbits -> unit effect {wreg} -function set_next_pc(pc) = { - nextPC = pc -} - -val tick_pc : unit -> unit effect {rreg, wreg} -function tick_pc() = { - PC = nextPC -} - -/* Extensions may wish to interpose on fetch, control transfer, and data - * addresses used to access memory and perhaps modify them. This file - * defines the return values used by functions that perform this interposition. - * - * The model defines defaults for these functions in riscv_addr_checks.sail; - * extensions would need to define their own functions to override them. - */ - -union Ext_FetchAddr_Check ('a : Type) = { - Ext_FetchAddr_OK : xlenbits, /* PC value to use for the actual fetch */ - Ext_FetchAddr_Error : 'a -} - -union Ext_ControlAddr_Check ('a : Type) = { - Ext_ControlAddr_OK : xlenbits, /* PC value to use for the target of the control operation */ - Ext_ControlAddr_Error : 'a -} - -union Ext_DataAddr_Check ('a : Type) = { - Ext_DataAddr_OK : xlenbits, /* Address to use for the data access */ - Ext_DataAddr_Error : 'a -} -/* default fetch address checks */ - -type ext_fetch_addr_error = unit - -/* Since fetch is done in granules, the check function gets two arguments: - * start_pc: the PC at the start of the current fetch sequence - * pc: the PC for the current granule - * - * returns: the *virtual* memory address to use for the fetch. - * any address translation errors are reported for pc, not the returned value. - */ -function ext_fetch_check_pc(start_pc : xlenbits, pc : xlenbits) -> Ext_FetchAddr_Check(ext_fetch_addr_error) = - Ext_FetchAddr_OK(pc) - -function ext_handle_fetch_check_error(err : ext_fetch_addr_error) -> unit = - () - -/* default control address checks */ - -type ext_control_addr_error = unit - -/* these functions return the address to use as the target for - * the control transfer. any address translation or other errors - * are reported for the original value, not the returned value. - * - * NOTE: the input value does *not* have bit[0] set to 0, to enable - * more accurate bounds checking. There is no constraint on the output - * value, which will have bit[0] cleared by the caller if needed. - */ - -/* the control address is derived from a non-PC register, e.g. in JALR */ -function ext_control_check_addr(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) = - Ext_ControlAddr_OK(pc) - -/* the control address is derived from the PC register, e.g. in JAL */ -function ext_control_check_pc(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) = - Ext_ControlAddr_OK(pc) - -function ext_handle_control_check_error(err : ext_control_addr_error) -> unit = - () - - -/* The default data address function does not perform any checks so - just uses unit for error type. */ -type ext_data_addr_error = unit - -/* Default data addr is just base register + immediate offset (may be zero). - Extensions might override and add additional checks. */ -function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : word_width) - -> Ext_DataAddr_Check(ext_data_addr_error) = - let addr = X(base) + offset in - Ext_DataAddr_OK(addr) - -/* Machine-mode and supervisor-mode functionality. */ - -union ExceptionType = { - E_Fetch_Addr_Align : unit, - E_Fetch_Access_Fault : unit, - E_Illegal_Instr : unit, - E_Breakpoint : unit, - E_Load_Addr_Align : unit, - E_Load_Access_Fault : unit, - E_SAMO_Addr_Align : unit, - E_SAMO_Access_Fault : unit, - E_U_EnvCall : unit, - E_S_EnvCall : unit, - E_Reserved_10 : unit, - E_M_EnvCall : unit, - E_Fetch_Page_Fault : unit, - E_Load_Page_Fault : unit, - E_Reserved_14 : unit, - E_SAMO_Page_Fault : unit, -} - -function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = { - assert(false); -} - - -/* memory access exceptions, defined here for use by the platform model. */ - -union MemoryOpResult ('a : Type) = { - MemValue : 'a, - MemException : ExceptionType -} - -val MemoryOpResult_add_meta : forall ('t : Type). (MemoryOpResult('t), mem_meta) -> MemoryOpResult(('t, mem_meta)) -function MemoryOpResult_add_meta(r, m) = match r { - MemValue(v) => MemValue(v, m), - MemException(e) => MemException(e) -} - -val MemoryOpResult_drop_meta : forall ('t : Type). MemoryOpResult(('t, mem_meta)) -> MemoryOpResult('t) -function MemoryOpResult_drop_meta(r) = match r { - MemValue(v, m) => MemValue(v), - MemException(e) => MemException(e) -} - -/* whether the platform supports misaligned accesses without trapping to M-mode. if false, - * misaligned loads/stores are trapped to Machine mode. - */ -function plat_enable_misaligned_access () : unit -> bool = true - -/* Platform-specific handling of instruction faults */ - -function handle_illegal() -> unit = { - assert(false); -} - -/* Physical memory model. - * - * This assumes that the platform memory map has been defined, so that accesses - * to MMIO regions can be dispatched. - * - * The implementation below supports the reading and writing of memory - * metadata in addition to raw memory data. - * - * The external API for this module is - * {mem_read, mem_read_meta, mem_write_ea, mem_write_value_meta, mem_write_value} - * where mem_write_value is a special case of mem_write_value_meta that uses - * a default value of the metadata. - * - * The internal implementation first performs a PMP check (if PMP is - * enabled), and then dispatches to MMIO regions or physical memory as - * per the platform memory map. - */ - -function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool = - unsigned(addr) % width == 0 - -function read_kind_of_flags (aq : bool, rl : bool, res : bool) -> option(read_kind) = - match (aq, rl, res) { - (false, false, false) => Some(Read_plain), - (true, false, false) => Some(Read_RISCV_acquire), - (true, true, false) => Some(Read_RISCV_strong_acquire), - (false, false, true) => Some(Read_RISCV_reserved), - (true, false, true) => Some(Read_RISCV_reserved_acquire), - (true, true, true) => Some(Read_RISCV_reserved_strong_acquire), - (false, true, false) => None(), /* should these be instead throwing error_not_implemented as below? */ - (false, true, true) => None() - } - -// only used for actual memory regions, to avoid MMIO effects -function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = { - let result = (match read_kind_of_flags(aq, rl, res) { - Some(rk) => Some(read_ram(rk, paddr, width, meta)), - None() => None() - }) : option((bits(8 * 'n), mem_meta)); - match (t, result) { - (Execute(), None()) => MemException(E_Fetch_Access_Fault()), - (Read(Data), None()) => MemException(E_Load_Access_Fault()), - (_, None()) => MemException(E_SAMO_Access_Fault()), - (_, Some(v, m)) => { MemValue(v, m) } - } -} - -val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rmemt, rreg, escape} - -function mem_read (typ, paddr, width, aq, rl, res) = { - let result : MemoryOpResult(bits(8 * 'n)) = - if (aq | res) & (~ (is_aligned_addr(paddr, width))) - then MemException(E_Load_Addr_Align()) - else match (aq, rl, res) { - (false, true, false) => throw(Error_not_implemented("load.rl")), - (false, true, true) => throw(Error_not_implemented("lr.rl")), - (_, _, _) => MemoryOpResult_drop_meta(phys_mem_read(typ, paddr, width, aq, rl, res, false)) - }; - result -} - -val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (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(write_ram_ea(Write_plain, addr, width)), - (false, true, false) => MemValue(write_ram_ea(Write_RISCV_release, addr, width)), - (false, false, true) => MemValue(write_ram_ea(Write_RISCV_conditional, addr, width)), - (false, true , true) => MemValue(write_ram_ea(Write_RISCV_conditional_release, addr, width)), - (true, false, false) => throw(Error_not_implemented("store.aq")), - (true, true, false) => MemValue(write_ram_ea(Write_RISCV_strong_release, addr, width)), - (true, false, true) => throw(Error_not_implemented("sc.aq")), - (true, true , true) => MemValue(write_ram_ea(Write_RISCV_conditional_strong_release, addr, width)) - } -} - -// only used for actual memory regions, to avoid MMIO effects -function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : atom('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = { - let result = MemValue(write_ram(wk, paddr, width, data, meta)); - result -} - -/* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */ - -/* Memory write with an explicit metadata value. Metadata writes are - * currently assumed to have the same alignment constraints as their - * data. - * NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime. - */ -val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), ext_access_type, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape} -function mem_write_value_meta (paddr, width, value, ext_acc, meta, aq, rl, con) = { - if (rl | con) & (~ (is_aligned_addr(paddr, width))) - then MemException(E_SAMO_Addr_Align()) - else match (aq, rl, con) { - (false, false, false) => phys_mem_write(Write_plain, paddr, width, value, meta), - (false, true, false) => phys_mem_write(Write_RISCV_release, paddr, width, value, meta), - (false, false, true) => phys_mem_write(Write_RISCV_conditional, paddr, width, value, meta), - (false, true , true) => phys_mem_write(Write_RISCV_conditional_release, paddr, width, value, meta), - (true, true, false) => phys_mem_write(Write_RISCV_strong_release, paddr, width, value, meta), - (true, true , true) => phys_mem_write(Write_RISCV_conditional_strong_release, paddr, width, value, meta), - // throw an illegal instruction here? - (true, false, false) => throw(Error_not_implemented("store.aq")), - (true, false, true) => throw(Error_not_implemented("sc.aq")) - } -} - -/* Memory write with a default metadata value. */ -val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape} -function mem_write_value (paddr, width, value, aq, rl, con) = - mem_write_value_meta(paddr, width, value, default_write_acc, default_meta, aq, rl, con) - -/* Result of address translation */ - -type ext_ptw = unit - -union TR_Result('paddr : Type, 'failure : Type) = { - TR_Address : ('paddr, ext_ptw), - TR_Failure : ('failure, ext_ptw) -} - -val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} -function translateAddr(vAddr, ac) = { - TR_Address(vAddr, ()); -} - -/* Instruction definitions. - * - * This includes decoding, execution, and assembly parsing and printing. - */ - -scattered union ast - -/* returns whether an instruction was retired, used for computing minstret */ -val execute : ast -> Retired effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, rmemt, barr, exmem, undef} -scattered function execute - -val encdec : ast <-> bits(32) -scattered mapping encdec - -///* see riscv_jalr_seq.sail or riscv_jalr_rmem.sail for the execute clause. */ -// -///* ***************************************************************** -//union clause ast = BTYPE : (bits(13), regidx, regidx, bop) -// -//mapping encdec_bop : bop <-> bits(3) = { -// RISCV_BEQ <-> 0b000, -// RISCV_BNE <-> 0b001, -// RISCV_BLT <-> 0b100, -// RISCV_BGE <-> 0b101, -// RISCV_BLTU <-> 0b110, -// RISCV_BGEU <-> 0b111 -//} -// -//mapping clause encdec = BTYPE(imm7_6 @ imm5_0 @ imm7_5_0 @ imm5_4_1 @ 0b0, rs2, rs1, op) -// <-> imm7_6 : bits(1) @ imm7_5_0 : bits(6) @ rs2 @ rs1 @ encdec_bop(op) @ imm5_4_1 : bits(4) @ imm5_0 : bits(1) @ 0b1100011 -// -//function clause execute (BTYPE(imm, rs2, rs1, op)) = { -// let rs1_val = X(rs1); -// let rs2_val = X(rs2); -// let taken : bool = match op { -// RISCV_BEQ => rs1_val == rs2_val, -// RISCV_BNE => rs1_val != rs2_val, -// RISCV_BLT => rs1_val <_s rs2_val, -// RISCV_BGE => rs1_val >=_s rs2_val, -// RISCV_BLTU => rs1_val <_u rs2_val, -// RISCV_BGEU => rs1_val >=_u rs2_val -// }; -// let t : xlenbits = PC + EXTS(imm); -// if taken then { -// /* Extensions get the first checks on the prospective target address. */ -// match ext_control_check_pc(t) { -// Ext_ControlAddr_Error(e) => { -// assert(false); -// RETIRE_FAIL -// }, -// Ext_ControlAddr_OK(target) => { -// if bit_to_bool(target[1]) & (~ (haveRVC())) then { -// handle_mem_exception(target, E_Fetch_Addr_Align()); -// RETIRE_FAIL; -// } else { -// set_next_pc(target); -// RETIRE_SUCCESS -// } -// } -// } -// } else RETIRE_SUCCESS -//} - -/* ****************************************************************** */ -union clause ast = ITYPE : (bits(12), regidx, regidx, iop) - -mapping encdec_iop : iop <-> bits(3) = { - RISCV_ADDI <-> 0b000, - RISCV_SLTI <-> 0b010, - RISCV_SLTIU <-> 0b011, - RISCV_ANDI <-> 0b111, - RISCV_ORI <-> 0b110, - RISCV_XORI <-> 0b100 -} - -mapping clause encdec = ITYPE(imm, rs1, rd, op) - <-> imm @ rs1 @ encdec_iop(op) @ rd @ 0b0010011 - -function clause execute (ITYPE (imm, rs1, rd, op)) = { - let rs1_val = X(rs1); - let immext : xlenbits = EXTS(imm); - let result : xlenbits = match op { - RISCV_ADDI => rs1_val + immext, - RISCV_SLTI => EXTZ(bool_to_bits(rs1_val <_s immext)), - RISCV_SLTIU => EXTZ(bool_to_bits(rs1_val <_u immext)), - RISCV_ANDI => rs1_val & immext, - RISCV_ORI => rs1_val | immext, - RISCV_XORI => rs1_val ^ immext - }; - X(rd) = result; - RETIRE_SUCCESS -} - -mapping itype_mnemonic : iop <-> string = { - RISCV_ADDI <-> "addi", - RISCV_SLTI <-> "slti", - RISCV_SLTIU <-> "sltiu", - RISCV_XORI <-> "xori", - RISCV_ORI <-> "ori", - RISCV_ANDI <-> "andi" -} - -/* ****************************************************************** */ -union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, bool) - -/* unsigned loads are only present for widths strictly less than xlen, - signed loads also present for widths equal to xlen */ -mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not_bool(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes)) - <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not_bool(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes)) - -val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits) -function extend_value(is_unsigned, value) = match (value) { - MemValue(v) => MemValue(if is_unsigned then EXTZ(v) else EXTS(v) : xlenbits), - MemException(e) => MemException(e) -} - -val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired effect {escape, rreg, wreg} -function process_load(rd, addr, value, is_unsigned) = - match extend_value(is_unsigned, value) { - MemValue(result) => { X(rd) = result; RETIRE_SUCCESS }, - MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } - } - -function check_misaligned(vaddr : xlenbits, width : word_width) -> bool = - if plat_enable_misaligned_access() then false - else match width { - BYTE => false, - HALF => vaddr[0] == bitone, - WORD => vaddr[0] == bitone | vaddr[1] == bitone, - DOUBLE => vaddr[0] == bitone | vaddr[1] == bitone | vaddr[2] == bitone - } - -function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { - let offset : xlenbits = EXTS(imm); - /* Get the address, X(rs1) + offset. - Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, offset, Read(Data), width) { - Ext_DataAddr_Error(e) => { assert(false); RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width) - then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL } - else match translateAddr(vaddr, Read(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - TR_Address(addr, _) => - match (width, sizeof(xlen)) { - (BYTE, _) => - process_load(rd, vaddr, mem_read(Read(Data), addr, 1, aq, rl, false), is_unsigned), - (HALF, _) => - process_load(rd, vaddr, mem_read(Read(Data), addr, 2, aq, rl, false), is_unsigned), - (WORD, _) => - process_load(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, false), is_unsigned), - (DOUBLE, 64) => - process_load(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, false), is_unsigned) - } - } - } -} - -/* ****************************************************************** */ -union clause ast = STORE : (bits(12), regidx, regidx, word_width, bool, bool) - -mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) if word_width_bytes(size) <= sizeof(xlen_bytes) - <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ imm5 : bits(5) @ 0b0100011 if word_width_bytes(size) <= sizeof(xlen_bytes) - -/* NOTE: Currently, we only EA if address translation is successful. - This may need revisiting. */ -function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = { - let offset : xlenbits = EXTS(imm); - /* Get the address, X(rs1) + offset. - Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, offset, Write(Data), width) { - Ext_DataAddr_Error(e) => { assert (false); RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } - else match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - TR_Address(addr, _) => { - let eares : MemoryOpResult(unit) = match width { - BYTE => mem_write_ea(addr, 1, aq, rl, false), - HALF => mem_write_ea(addr, 2, aq, rl, false), - WORD => mem_write_ea(addr, 4, aq, rl, false), - DOUBLE => mem_write_ea(addr, 8, aq, rl, false) - }; - match (eares) { - MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }, - MemValue(_) => { - let rs2_val = X(rs2); - let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) { - (BYTE, _) => mem_write_value(addr, 1, rs2_val[7..0], aq, rl, false), - (HALF, _) => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false), - (WORD, _) => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false), - (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val, aq, rl, false) - }; - match (res) { - MemValue(true) => RETIRE_SUCCESS, - MemValue(false) => internal_error("store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } - } - } - } - } - } - } -} - -/* Put the illegal instructions last to use their wildcard match. */ - -/* ****************************************************************** */ - -union clause ast = ILLEGAL : word - -mapping clause encdec = ILLEGAL(s) <-> s - -function clause execute (ILLEGAL(s)) = { handle_illegal(); RETIRE_FAIL } - -/* ****************************************************************** */ - -/* End definitions */ -end ast -end execute -end encdec -end encdec_compressed - -val decode : bits(32) -> ast effect pure -function decode bv = encdec(bv) - -/* The result of a fetch, which includes any possible error - * from an extension that interposes on the fetch operation. - */ - -union FetchResult = { - F_Ext_Error : ext_fetch_addr_error, /* For extensions */ - F_Base : word, /* Base ISA */ - F_RVC : half, /* Compressed ISA */ - F_Error : (ExceptionType, xlenbits) /* standard exception and PC */ -} -/* The default implementation of hooks for the step() and main() functions. */ - -function ext_init() -> unit = () - -function ext_fetch_hook(f : FetchResult) -> FetchResult = f - -function ext_pre_step_hook() -> unit = () -function ext_post_step_hook() -> unit = () -/* Extensions may wish to interpose and transform decoded instructions, - * based on other machine state. This is supported via a post-decode - * instruction hook, the default implementation of which is provided below. - */ - -val ext_post_decode_hook : ast -> ast effect {rreg} -function ext_post_decode_hook(x) = x - -val fetch : unit -> FetchResult effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} -function fetch() -> FetchResult = - /* fetch PC check for extensions: extensions return a transformed PC to fetch, - * but any exceptions use the untransformed PC. - */ - match ext_fetch_check_pc(PC, PC) { - Ext_FetchAddr_Error(e) => F_Ext_Error(e), - Ext_FetchAddr_OK(use_pc) => { - if (use_pc[0] != bitzero | (use_pc[1] != bitzero)) - then F_Error(E_Fetch_Addr_Align(), PC) - else match translateAddr(use_pc, Execute()) { - TR_Failure(e, _) => F_Error(e, PC), - TR_Address(ppc, _) => { - match mem_read(Execute(), ppc, 4, false, false, false) { - MemException(e) => F_Error(e, PC), - MemValue(ibits) => F_Base(ibits) - } - } - } - } - } - -/* The emulator fetch-execute-interrupt dispatch loop. */ - -/* returns whether to increment the step count in the trace */ -function step(step_no : int) -> bool = { - /* for step extensions */ - ext_pre_step_hook(); - - let (retired, stepped) : (Retired, bool) = - /* the extension hook interposes on the fetch result */ - let f : FetchResult = ext_fetch_hook(fetch()) in - match f { - /* extension error */ - F_Ext_Error(e) => { - ext_handle_fetch_check_error(e); - (RETIRE_FAIL, false) - }, - /* standard error */ - F_Error(e, addr) => { - handle_mem_exception(addr, e); - (RETIRE_FAIL, false) - }, - F_Base(w) => { - let ast = decode(w); - nextPC = PC + 4; - (execute(ext_post_decode_hook(ast)), true) - } - }; - - tick_pc(); - - /* for step extensions */ - ext_post_step_hook(); - - stepped -} - -function loop () : unit -> unit = { - step_no : int = 0; - while (true) do { - let stepped = step(step_no); - if stepped then step_no = step_no + 1; - } -} - - -function main () : unit -> unit = { - // PC = __GetSlice_int(64, elf_entry(), 0); - PC = sail_zero_extend(0x1000, sizeof(xlen)); - print_bits("PC = ", PC); - - try { - loop() - } catch { - Error_not_implemented(s) => print_string("Error: Not implemented: ", s), - Error_internal_error() => print("Error: internal error") - } -} -- cgit v1.1