summaryrefslogtreecommitdiff
path: root/riscv
diff options
context:
space:
mode:
Diffstat (limited to 'riscv')
-rw-r--r--riscv/Makefile8
-rw-r--r--riscv/prelude.sail6
-rw-r--r--riscv/riscv_platform.c48
-rw-r--r--riscv/riscv_platform.h24
-rw-r--r--riscv/riscv_platform.sail22
-rw-r--r--riscv/riscv_prelude.c2
-rw-r--r--riscv/riscv_prelude.h1
-rw-r--r--riscv/riscv_sys.sail4
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:33:22 +0000