aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile17
-rw-r--r--descr1
-rw-r--r--opam33
3 files changed, 51 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 8fa204f..f1acbf2 100644
--- a/Makefile
+++ b/Makefile
@@ -234,10 +234,12 @@ endif
generated_definitions/lem/$(ARCH)/riscv.lem: $(SAIL_SRCS) Makefile
mkdir -p generated_definitions/lem/$(ARCH) generated_definitions/isabelle/$(ARCH)
$(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS)
+ echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/$(ARCH)/riscv_types.lem
generated_definitions/lem/$(ARCH)/riscv_sequential.lem: $(SAIL_SRCS) Makefile
mkdir -p generated_definitions/lem/$(ARCH) generated_definitions/isabelle/$(ARCH)
$(SAIL_DIR)/sail -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -lem_sequential -o riscv_sequential -lem_mwords -lem_lib Riscv_extras_sequential $(SAIL_SRCS)
+ echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/$(ARCH)/riscv_types.lem
generated_definitions/isabelle/$(ARCH)/Riscv.thy: generated_definitions/isabelle/$(ARCH)/ROOT generated_definitions/lem/$(ARCH)/riscv.lem handwritten_support/$(RISCV_EXTRAS_LEM) Makefile
lem -isa -outdir generated_definitions/isabelle/$(ARCH) -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \
@@ -322,6 +324,21 @@ generated_definitions/for-rmem/riscv.defs: $(SAIL_RMEM_SRCS)
#LOC_FILES:=$(SAIL_SRCS) main.sail
#include $(SAIL_DIR)/etc/loc.mk
+opam-build:
+ make ARCH=64 c_emulator/riscv_sim_RV64
+ make ARCH=32 c_emulator/riscv_sim_RV32
+
+opam-install:
+ if [ -z "$(INSTALL_DIR)" ]; then echo INSTALL_DIR is unset; false; fi
+ mkdir -p $(INSTALL_DIR)/bin
+ cp c_emulator/riscv_sim_RV64 $(INSTALL_DIR)/bin
+ cp c_emulator/riscv_sim_RV32 $(INSTALL_DIR)/bin
+
+opam-uninstall:
+ if [ -z "$(INSTALL_DIR)" ]; then echo INSTALL_DIR is unset; false; fi
+ rm $(INSTALL_DIR)/bin/riscv_sim_RV64
+ rm $(INSTALL_DIR)/bin/riscv_sim_RV32
+
clean:
-rm -rf generated_definitions/ocaml/* generated_definitions/c/* generated_definitions/latex/*
-rm -rf generated_definitions/lem/* generated_definitions/isabelle/* generated_definitions/hol4/* generated_definitions/coq/*
diff --git a/descr b/descr
new file mode 100644
index 0000000..8f657db
--- /dev/null
+++ b/descr
@@ -0,0 +1 @@
+This package installs a RISC-V emulator (32 and 64 bits) built form the Sail model at https://github.com/rems-project/sail-riscv . \ No newline at end of file
diff --git a/opam b/opam
new file mode 100644
index 0000000..dc44622
--- /dev/null
+++ b/opam
@@ -0,0 +1,33 @@
+opam-version: "1.2"
+name: "sail-riscv"
+version: "0.1"
+maintainer: "Sail Devs <cl-sail-dev@lists.cam.ac.uk>"
+authors: [
+ "Alasdair Armstrong"
+ "Thomas Bauereiss"
+ "Brian Campbell"
+ "Shaked Flur"
+ "Jonathan French"
+ "Prashanth Mundkur"
+ "Robert Norton"
+ "Christopher Pulte"
+ "Peter Sewell"
+]
+homepage: "https://github.com/rems-project/sail-riscv/"
+bug-reports: "https://github.com/rems-project/sail-riscv/issues"
+license: "BSD3"
+dev-repo: "https://github.com/rems-project/sail-riscv.git"
+build: [make "INSTALL_DIR=%{prefix}%" "opam-build"]
+install: [make "INSTALL_DIR=%{prefix}%" "opam-install"]
+remove: [
+ make "INSTALL_DIR=%{prefix}%" "opam-uninstall"
+]
+depends: [
+ "ocamlfind"
+ "ocamlbuild"
+ "sail" {>= "0.9"}
+ "linksem" {>= "0.3"}
+ "conf-gmp"
+ "conf-zlib"
+]
+available: [ocaml-version >= "4.06.1"]