diff options
| -rw-r--r-- | riscv/Makefile | 8 | ||||
| -rw-r--r-- | riscv/prelude.sail | 6 | ||||
| -rw-r--r-- | riscv/riscv_platform.c | 48 | ||||
| -rw-r--r-- | riscv/riscv_platform.h | 24 | ||||
| -rw-r--r-- | riscv/riscv_platform.sail | 22 | ||||
| -rw-r--r-- | riscv/riscv_prelude.c | 2 | ||||
| -rw-r--r-- | riscv/riscv_prelude.h | 1 | ||||
| -rw-r--r-- | riscv/riscv_sys.sail | 4 |
8 files changed, 97 insertions, 18 deletions
diff --git a/riscv/Makefile b/riscv/Makefile index a3079148..b5f518d8 100644 --- a/riscv/Makefile +++ b/riscv/Makefile @@ -2,6 +2,8 @@ SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail ris PLATFORM_OCAML_SRCS = platform.ml platform_impl.ml platform_main.ml SAIL_DIR ?= $(realpath ..) SAIL ?= $(SAIL_DIR)/sail +C_WARNINGS ?= -Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function +C_SRCS = riscv_prelude.c riscv_platform.c export SAIL_DIR @@ -33,10 +35,10 @@ coverage: _sbuild/coverage.native mkdir coverage && bisect-ppx-report -html coverage/ -I _sbuild/ bisect/bisect*.out riscv.c: $(SAIL_SRCS) main.sail Makefile - $(SAIL) -O -memo_z3 -c -c_include riscv_prelude.h $(SAIL_SRCS) main.sail 1> $@ + $(SAIL) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h $(SAIL_SRCS) main.sail 1> $@ -riscv_c: riscv.c riscv_prelude.h riscv_prelude.c Makefile - gcc -O2 riscv.c riscv_prelude.c ../lib/*.c -lgmp -lz -I ../lib -o riscv_c +riscv_c: riscv.c riscv_prelude.h $(C_SRCS) Makefile + gcc $(C_WARNINGS) -O2 riscv.c $(C_SRCS) ../lib/*.c -lgmp -lz -I ../lib -o riscv_c latex: $(SAIL_SRCS) Makefile $(SAIL) -latex -latex_prefix sail -o sail_ltx $(SAIL_SRCS) diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 7ddb9369..6b2e13ff 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -169,7 +169,7 @@ val update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec", val vcons = {lem: "cons_vec"} : forall ('n : Int) ('a : Type). ('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a) -val bitvector_concat = {ocaml: "append", lem: "concat_vec", coq: "concat_vec"} : forall ('n : Int) ('m : Int). +val bitvector_concat = {c: "append", ocaml: "append", lem: "concat_vec", coq: "concat_vec"} : forall ('n : Int) ('m : Int). (bits('n), bits('m)) -> bits('n + 'm) val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type). @@ -264,9 +264,9 @@ val print = "print_endline" : string -> unit val putchar = "putchar" : forall ('a : Type). 'a -> unit -val concat_str = {ocaml: "concat_str", lem: "stringAppend", coq: "String.append"} : (string, string) -> string +val concat_str = {c: "concat_str", ocaml: "concat_str", lem: "stringAppend", coq: "String.append"} : (string, string) -> string -val string_of_int = {ocaml: "string_of_int", lem: "stringFromInteger"} : int -> string +val string_of_int = {c: "string_of_int", ocaml: "string_of_int", lem: "stringFromInteger"} : int -> string val DecStr : int -> string diff --git a/riscv/riscv_platform.c b/riscv/riscv_platform.c new file mode 100644 index 00000000..2ad3d3c1 --- /dev/null +++ b/riscv/riscv_platform.c @@ -0,0 +1,48 @@ +#include "sail.h" +#include "rts.h" +#include "riscv_prelude.h" + +bool plat_enable_dirty_update(unit u) +{ return false; } + +bool plat_enable_misaligned_access(unit u) +{ return false; } + +mach_bits plat_ram_base(unit u) +{ return 0; } + +mach_bits plat_ram_size(unit u) +{ return 0; } + +mach_bits plat_rom_base(unit u) +{ return 0; } + +mach_bits plat_rom_size(unit u) +{ return 0; } + +mach_bits plat_clint_base(unit u) +{ return 0; } + +mach_bits plat_clint_size(unit u) +{ return 0; } + +bool within_phys_mem(mach_bits addr, sail_int len) +{ return 0; } + +unit load_reservation(mach_bits addr) +{ return UNIT; } + +bool match_reservation(mach_bits addr) +{ return false; } + +unit cancel_reservation(unit u) +{ return UNIT; } + +unit plat_term_write(mach_bits c) +{ return UNIT; } + +void plat_insns_per_tick(sail_int *rop, unit u) +{ } + +mach_bits plat_htif_tohost(unit u) +{ return 0; } diff --git a/riscv/riscv_platform.h b/riscv/riscv_platform.h new file mode 100644 index 00000000..2d63dca6 --- /dev/null +++ b/riscv/riscv_platform.h @@ -0,0 +1,24 @@ +#pragma once +#include "sail.h" + +bool plat_enable_dirty_update(unit); +bool plat_enable_misaligned_access(unit); + +mach_bits plat_ram_base(unit); +mach_bits plat_ram_size(unit); +bool within_phys_mem(mach_bits, sail_int); + +mach_bits plat_rom_base(unit); +mach_bits plat_rom_size(unit); + +mach_bits plat_clint_base(unit); +mach_bits plat_clint_size(unit); + +unit load_reservation(mach_bits); +bool match_reservation(mach_bits); +unit cancel_reservation(unit); + +void plat_insns_per_tick(sail_int *rop, unit); + +unit plat_term_write(mach_bits); +mach_bits plat_htif_tohost(unit); diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail index 08c88b38..80f546b8 100644 --- a/riscv/riscv_platform.sail +++ b/riscv/riscv_platform.sail @@ -7,29 +7,31 @@ */ /* Main memory */ -val plat_ram_base = {ocaml: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits -val 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", lem: "plat_ram_base"} : unit -> xlenbits +val plat_ram_size = {c: "plat_ram_size", ocaml: "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", + c: "plat_enable_dirty_update", lem: "plat_enable_dirty_update"} : unit -> bool /* whether the platform supports misaligned accesses without trapping to M-mode. if false, * misaligned loads/stores are trapped to Machine mode. */ val plat_enable_misaligned_access = {ocaml: "Platform.enable_misaligned_access", + c: "plat_enable_misaligned_access", lem: "plat_enable_misaligned_access"} : unit -> bool /* ROM holding reset vector and device-tree DTB */ -val plat_rom_base = {ocaml: "Platform.rom_base", lem: "plat_rom_base"} : unit -> xlenbits -val plat_rom_size = {ocaml: "Platform.rom_size", lem: "plat_rom_size"} : unit -> xlenbits +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 /* Location of clock-interface, which should match with the spec in the DTB */ -val plat_clint_base = {ocaml: "Platform.clint_base", lem: "plat_clint_base"} : unit -> xlenbits -val plat_clint_size = {ocaml: "Platform.clint_size", lem: "plat_clint_size"} : unit -> xlenbits +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 /* Location of HTIF ports */ -val plat_htif_tohost = {ocaml: "Platform.htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits +val plat_htif_tohost = {ocaml: "Platform.htif_tohost", c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits // todo: fromhost val phys_mem_segments : unit -> list((xlenbits, xlenbits)) @@ -62,7 +64,7 @@ function within_htif_readable(addr : xlenbits, width : atom('n)) -> forall 'n. b /* CLINT (Core Local Interruptor), based on Spike. */ -val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick", lem: "plat_insns_per_tick"} : unit -> int +val plat_insns_per_tick = {ocaml: "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 : xlenbits // memory-mapped internal clint register. @@ -148,8 +150,8 @@ function tick_clock() = { /* Basic terminal character I/O. */ -val plat_term_write = {ocaml: "Platform.term_write", lem: "plat_term_write"} : bits(8) -> unit -val plat_term_read = {ocaml: "Platform.term_read", lem: "plat_term_read"} : unit -> bits(8) +val plat_term_write = {ocaml: "Platform.term_write", c: "plat_term_write", lem: "plat_term_write"} : bits(8) -> unit +val plat_term_read = {ocaml: "Platform.term_read", c: "plat_term_read", lem: "plat_term_read"} : unit -> bits(8) /* Spike's HTIF device interface, which multiplexes the above MMIO devices. */ diff --git a/riscv/riscv_prelude.c b/riscv/riscv_prelude.c index a1f06b4d..c8145df4 100644 --- a/riscv/riscv_prelude.c +++ b/riscv/riscv_prelude.c @@ -3,4 +3,6 @@ unit print_string(sail_string prefix, sail_string msg) { printf("%s%s\n", prefix, msg); + return UNIT; } + diff --git a/riscv/riscv_prelude.h b/riscv/riscv_prelude.h index a0686086..514022cd 100644 --- a/riscv/riscv_prelude.h +++ b/riscv/riscv_prelude.h @@ -1,3 +1,4 @@ +#pragma once #include "sail.h" #include "rts.h" diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail index 451ff9ec..94643ec2 100644 --- a/riscv/riscv_sys.sail +++ b/riscv/riscv_sys.sail @@ -763,11 +763,11 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool = * where cancellation can be performed. */ -val load_reservation = {ocaml: "Platform.load_reservation", lem: "load_reservation"} : xlenbits -> unit +val load_reservation = {ocaml: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit val match_reservation = {ocaml: "Platform.match_reservation", lem: "speculate_conditional_success"} : xlenbits -> bool effect {exmem} -val cancel_reservation = {ocaml: "Platform.cancel_reservation", lem: "cancel_reservation"} : unit -> unit +val cancel_reservation = {ocaml: "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. |