Skip to content

Commit

Permalink
Merge branch 'svpbmt1' of https://github.com/ved-rivos/sail-riscv-cfi
Browse files Browse the repository at this point in the history
…into svpbmt1
  • Loading branch information
ved-rivos committed Mar 16, 2024
2 parents 3f932fe + 31658df commit 22a9eac
Show file tree
Hide file tree
Showing 52 changed files with 1,095 additions and 1,722 deletions.
8 changes: 5 additions & 3 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ SAIL_VM_SRCS += $(SAIL_RV64_VM_SRCS)
endif

# Non-instruction sources
PRELUDE = prelude.sail prelude_mapping.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail
PRELUDE = prelude.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail

SAIL_REGS_SRCS = riscv_reg_type.sail riscv_freg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail
SAIL_REGS_SRCS += riscv_pmp_regs.sail riscv_pmp_control.sail
Expand Down Expand Up @@ -247,9 +247,11 @@ gcovr:
ocaml_emulator/tracecmp: ocaml_emulator/tracecmp.ml
ocamlfind ocamlopt -annot -linkpkg -package unix $^ -o $@

c_preserve_fns=-c_preserve _set_Misa_C

generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile
mkdir -p generated_definitions/c
$(SAIL) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@)
$(SAIL) $(SAIL_FLAGS) $(c_preserve_fns) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@)

generated_definitions/c2/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile
mkdir -p generated_definitions/c2
Expand Down Expand Up @@ -288,7 +290,7 @@ rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
# sed -i isn't posix compliant, unfortunately
generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main.sail Makefile
mkdir -p generated_definitions/c
$(SAIL) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@)
$(SAIL) $(c_preserve_fns) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@)
sed -e '/^[[:space:]]*$$/d' $@ > $@.new
mv $@.new $@

Expand Down
19 changes: 17 additions & 2 deletions c_emulator/riscv_platform.c
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,16 @@ bool sys_enable_vext(unit u)
return rv_enable_vext;
}

uint64_t sys_pmp_count(unit u)
{
return rv_pmp_count;
}

uint64_t sys_pmp_grain(unit u)
{
return rv_pmp_grain;
}

bool sys_enable_writable_misa(unit u)
{
return rv_enable_writable_misa;
Expand All @@ -67,9 +77,14 @@ bool plat_mtval_has_illegal_inst_bits(unit u)
return rv_mtval_has_illegal_inst_bits;
}

bool plat_enable_pmp(unit u)
bool sys_enable_svnapot(unit u)
{
return rv_enable_pmp;
return rv_enable_svnapot;
}

bool sys_enable_svpbmt(unit u)
{
return rv_enable_svpbmt;
}

bool sys_enable_svnapot(unit u)
Expand Down
4 changes: 3 additions & 1 deletion c_emulator/riscv_platform.h
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,12 @@ bool sys_enable_vext(unit);
bool sys_enable_svnapot(unit);
bool sys_enable_svpbmt(unit);

uint64_t sys_pmp_count(unit);
uint64_t sys_pmp_grain(unit);

bool plat_enable_dirty_update(unit);
bool plat_enable_misaligned_access(unit);
bool plat_mtval_has_illegal_inst_bits(unit);
bool plat_enable_pmp(unit);

mach_bits plat_ram_base(unit);
mach_bits plat_ram_size(unit);
Expand Down
4 changes: 3 additions & 1 deletion c_emulator/riscv_platform_impl.c
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,9 @@
#include <stdio.h>

/* Settings of the platform implementation, with common defaults. */
bool rv_enable_pmp = false;
uint64_t rv_pmp_count = 0;
uint64_t rv_pmp_grain = 0;

bool rv_enable_zfinx = false;
bool rv_enable_rvc = true;
bool rv_enable_next = false;
Expand Down
4 changes: 3 additions & 1 deletion c_emulator/riscv_platform_impl.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,9 @@

#define DEFAULT_RSTVEC 0x00001000

extern bool rv_enable_pmp;
extern uint64_t rv_pmp_count;
extern uint64_t rv_pmp_grain;

extern bool rv_enable_zfinx;
extern bool rv_enable_rvc;
extern bool rv_enable_next;
Expand Down
31 changes: 25 additions & 6 deletions c_emulator/riscv_sim.c
Original file line number Diff line number Diff line change
Expand Up @@ -51,8 +51,10 @@ const char *RV32ISA = "RV32IMAC";

#define OPT_TRACE_OUTPUT 1000
#define OPT_ENABLE_WRITABLE_FIOM 1001
#define OPT_ENABLE_SVNAPOT 1002
#define OPT_ENABLE_SVPBMT 1003
#define OPT_PMP_COUNT 1002
#define OPT_PMP_GRAIN 1003
#define OPT_ENABLE_SVNAPOT 1004
#define OPT_ENABLE_SVPBMT 1005

static bool do_dump_dts = false;
static bool do_show_times = false;
Expand Down Expand Up @@ -121,7 +123,8 @@ char *sailcov_file = NULL;
static struct option options[] = {
{"enable-dirty-update", no_argument, 0, 'd' },
{"enable-misaligned", no_argument, 0, 'm' },
{"enable-pmp", no_argument, 0, 'P' },
{"pmp-count", required_argument, 0, OPT_PMP_COUNT },
{"pmp-grain", required_argument, 0, OPT_PMP_GRAIN },
{"enable-next", no_argument, 0, 'N' },
{"ram-size", required_argument, 0, 'z' },
{"disable-compressed", no_argument, 0, 'C' },
Expand Down Expand Up @@ -240,6 +243,8 @@ static int process_args(int argc, char **argv)
{
int c;
uint64_t ram_size = 0;
uint64_t pmp_count = 0;
uint64_t pmp_grain = 0;
while (true) {
c = getopt_long(argc, argv,
"a"
Expand Down Expand Up @@ -285,9 +290,23 @@ static int process_args(int argc, char **argv)
fprintf(stderr, "enabling misaligned access.\n");
rv_enable_misaligned = true;
break;
case 'P':
fprintf(stderr, "enabling PMP support.\n");
rv_enable_pmp = true;
case OPT_PMP_COUNT:
pmp_count = atol(optarg);
fprintf(stderr, "PMP count: %lld\n", pmp_count);
if (pmp_count != 0 && pmp_count != 16 && pmp_count != 64) {
fprintf(stderr, "invalid PMP count: must be 0, 16 or 64");
exit(1);
}
rv_pmp_count = pmp_count;
break;
case OPT_PMP_GRAIN:
pmp_grain = atol(optarg);
fprintf(stderr, "PMP grain: %lld\n", pmp_grain);
if (pmp_grain >= 64) {
fprintf(stderr, "invalid PMP grain: must less than 64");
exit(1);
}
rv_pmp_grain = pmp_grain;
break;
case 'C':
fprintf(stderr, "disabling RVC compressed instructions.\n");
Expand Down
4 changes: 0 additions & 4 deletions handwritten_support/riscv_extras.lem
Original file line number Diff line number Diff line change
Expand Up @@ -201,10 +201,6 @@ val plat_enable_misaligned_access : unit -> bool
let plat_enable_misaligned_access () = false
declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access`

val plat_enable_pmp : unit -> bool
let plat_enable_pmp () = false
declare ocaml target_rep function plat_enable_pmp = `Platform.enable_pmp`

val plat_mtval_has_illegal_inst_bits : unit -> bool
let plat_mtval_has_illegal_inst_bits () = false
declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits`
Expand Down
4 changes: 0 additions & 4 deletions handwritten_support/riscv_extras_sequential.lem
Original file line number Diff line number Diff line change
Expand Up @@ -189,10 +189,6 @@ val plat_enable_misaligned_access : unit -> bool
let plat_enable_misaligned_access () = false
declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access`

val plat_enable_pmp : unit -> bool
let plat_enable_pmp () = false
declare ocaml target_rep function plat_enable_pmp = `Platform.enable_pmp`

val plat_mtval_has_illegal_inst_bits : unit -> bool
let plat_mtval_has_illegal_inst_bits () = false
declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits`
Expand Down
124 changes: 124 additions & 0 deletions model/hex_bits.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,124 @@
// Note: This file is temporarily copied here from the Sail compiler. It can
// be removed when Sail 0.18 is released.

/*==========================================================================*/
/* Sail */
/* */
/* Sail and the Sail architecture models here, comprising all files and */
/* directories except the ASL-derived Sail code in the aarch64 directory, */
/* are subject to the BSD two-clause licence below. */
/* */
/* The ASL derived parts of the ARMv8.3 specification in */
/* aarch64/no_vector and aarch64/full are copyright ARM Ltd. */
/* */
/* Copyright (c) 2013-2021 */
/* Kathyrn Gray */
/* Shaked Flur */
/* Stephen Kell */
/* Gabriel Kerneis */
/* Robert Norton-Wright */
/* Christopher Pulte */
/* Peter Sewell */
/* Alasdair Armstrong */
/* Brian Campbell */
/* Thomas Bauereiss */
/* Anthony Fox */
/* Jon French */
/* Dominic Mulligan */
/* Stephen Kell */
/* Mark Wassell */
/* Alastair Reid (Arm Ltd) */
/* */
/* All rights reserved. */
/* */
/* This work was partially supported by EPSRC grant EP/K008528/1 <a */
/* href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous */
/* Engineering for Mainstream Systems</a>, an ARM iCASE award, EPSRC IAA */
/* KTF funding, and donations from Arm. This project has received */
/* funding from the European Research Council (ERC) under the European */
/* Union’s Horizon 2020 research and innovation programme (grant */
/* agreement No 789108, ELVER). */
/* */
/* This software was developed by SRI International and the University of */
/* Cambridge Computer Laboratory (Department of Computer Science and */
/* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") */
/* and FA8750-10-C-0237 ("CTSRD"). */
/* */
/* 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. */
/*==========================================================================*/

$ifndef _HEX_BITS
$define _HEX_BITS

$include <vector.sail>
$include <string.sail>

val "parse_hex_bits" : forall 'n, 'n > 0. (int('n), string) -> bits('n)
val "valid_hex_bits" : forall 'n, 'n > 0. (int('n), string) -> bool

val hex_bits : forall 'n, 'n > 0. bits('n) <-> (int('n), string)

function hex_bits_forwards(bv) = (length(bv), hex_str(unsigned(bv)))
function hex_bits_forwards_matches(bv) = true

function hex_bits_backwards(n, str) = parse_hex_bits(n, str)
function hex_bits_backwards_matches(n, str) = valid_hex_bits(n, str)

mapping hex_bits_1 : bits(1) <-> string = { hex_bits(1, s) <-> s }
mapping hex_bits_2 : bits(2) <-> string = { hex_bits(2, s) <-> s }
mapping hex_bits_3 : bits(3) <-> string = { hex_bits(3, s) <-> s }
mapping hex_bits_4 : bits(4) <-> string = { hex_bits(4, s) <-> s }
mapping hex_bits_5 : bits(5) <-> string = { hex_bits(5, s) <-> s }
mapping hex_bits_6 : bits(6) <-> string = { hex_bits(6, s) <-> s }
mapping hex_bits_7 : bits(7) <-> string = { hex_bits(7, s) <-> s }
mapping hex_bits_8 : bits(8) <-> string = { hex_bits(8, s) <-> s }
mapping hex_bits_9 : bits(9) <-> string = { hex_bits(9, s) <-> s }

mapping hex_bits_10 : bits(10) <-> string = { hex_bits(10, s) <-> s }
mapping hex_bits_11 : bits(11) <-> string = { hex_bits(11, s) <-> s }
mapping hex_bits_12 : bits(12) <-> string = { hex_bits(12, s) <-> s }
mapping hex_bits_13 : bits(13) <-> string = { hex_bits(13, s) <-> s }
mapping hex_bits_14 : bits(14) <-> string = { hex_bits(14, s) <-> s }
mapping hex_bits_15 : bits(15) <-> string = { hex_bits(15, s) <-> s }
mapping hex_bits_16 : bits(16) <-> string = { hex_bits(16, s) <-> s }
mapping hex_bits_17 : bits(17) <-> string = { hex_bits(17, s) <-> s }
mapping hex_bits_18 : bits(18) <-> string = { hex_bits(18, s) <-> s }
mapping hex_bits_19 : bits(19) <-> string = { hex_bits(19, s) <-> s }

mapping hex_bits_20 : bits(20) <-> string = { hex_bits(20, s) <-> s }
mapping hex_bits_21 : bits(21) <-> string = { hex_bits(21, s) <-> s }
mapping hex_bits_22 : bits(22) <-> string = { hex_bits(22, s) <-> s }
mapping hex_bits_23 : bits(23) <-> string = { hex_bits(23, s) <-> s }
mapping hex_bits_24 : bits(24) <-> string = { hex_bits(24, s) <-> s }
mapping hex_bits_25 : bits(25) <-> string = { hex_bits(25, s) <-> s }
mapping hex_bits_26 : bits(26) <-> string = { hex_bits(26, s) <-> s }
mapping hex_bits_27 : bits(27) <-> string = { hex_bits(27, s) <-> s }
mapping hex_bits_28 : bits(28) <-> string = { hex_bits(28, s) <-> s }
mapping hex_bits_29 : bits(29) <-> string = { hex_bits(29, s) <-> s }

mapping hex_bits_30 : bits(30) <-> string = { hex_bits(30, s) <-> s }
mapping hex_bits_31 : bits(31) <-> string = { hex_bits(31, s) <-> s }
mapping hex_bits_32 : bits(32) <-> string = { hex_bits(32, s) <-> s }

$endif _HEX_BITS
Loading

0 comments on commit 22a9eac

Please sign in to comment.