summaryrefslogtreecommitdiff
path: root/riscv
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-08-29 18:01:50 +0100
committerAlasdair Armstrong2018-08-29 18:35:50 +0100
commita5ad2059821b86ef26a86d78c40cc680c57aa94e (patch)
tree468eb6bb76f995fb24872e028b0f7a9c7af8f06a /riscv
parent07e3591e2427db2d9407d554ac57984ca566c6ed (diff)
C: Fix some issues with tuples as arguments to polymorphic constructors
Now all we need to do is make sure the RISC-V builtins are mapped to the correct C functions, and RISC-V in C should work (hopefully). We're still missing some of the functions in sail.c for the mappings so those have to be implemented.
Diffstat (limited to 'riscv')
-rw-r--r--riscv/Makefile8
-rw-r--r--riscv/main.sail5
2 files changed, 9 insertions, 4 deletions
diff --git a/riscv/Makefile b/riscv/Makefile
index 4d2baaf1..e5e21709 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -32,8 +32,11 @@ coverage: _sbuild/coverage.native
mkdir bisect && mv bisect*.out bisect/
mkdir coverage && bisect-ppx-report -html coverage/ -I _sbuild/ bisect/bisect*.out
-riscv.c: $(SAIL_SRCS) Makefile
- $(SAIL) -O -memo_z3 -c $(SAIL_SRCS) 1> $@
+riscv.c: $(SAIL_SRCS) main.sail Makefile
+ $(SAIL) -O -memo_z3 -c $(SAIL_SRCS) main.sail 1> $@
+
+riscv_c: riscv.c
+ gcc -O2 riscv.c ../lib/*.c -lgmp -lz -I ../lib -o riscv_c
latex: $(SAIL_SRCS) Makefile
$(SAIL) -latex -latex_prefix sail -o sail_ltx $(SAIL_SRCS)
@@ -102,5 +105,6 @@ clean:
-rm -f platform_main.native platform coverage.native
-rm -f riscv.vo riscv_types.vo riscv_extras.vo riscv.v riscv_types.v
-rm -f riscv_duopod.vo riscv_duopod_types.vo riscv_duopod.v riscv_duopod_types.v
+ -rm -f riscv.c
-Holmake cleanAll
ocamlbuild -clean
diff --git a/riscv/main.sail b/riscv/main.sail
index b2a53b11..32f14177 100644
--- a/riscv/main.sail
+++ b/riscv/main.sail
@@ -14,8 +14,9 @@ function main () = {
PC = __GetSlice_int(64, elf_entry(), 0);
try {
- init_sys ();
- loop (elf_tohost())
+ init_platform();
+ init_sys();
+ loop()
} catch {
Error_not_implemented(s) => print_string("Error: Not implemented: ", s),
Error_internal_error() => print("Error: internal error")