diff options
-rw-r--r-- | Makefile | 142 | ||||
-rw-r--r-- | README.md | 33 | ||||
-rw-r--r-- | c_emulator/reset_vec.S (renamed from reset_vec.S) | 0 | ||||
-rwxr-xr-x | c_emulator/reset_vec.bin (renamed from reset_vec.bin) | bin | 28 -> 28 bytes | |||
-rw-r--r-- | handwritten_support/Holmakefile (renamed from hol4/Holmakefile) | 0 | ||||
-rw-r--r-- | handwritten_support/ROOT (renamed from isabelle/ROOT) | 4 | ||||
-rw-r--r-- | handwritten_support/riscv_extras.lem (renamed from lem/riscv_extras.lem) | 0 | ||||
-rw-r--r-- | handwritten_support/riscv_extras.v (renamed from coq/riscv_extras.v) | 0 | ||||
-rw-r--r-- | handwritten_support/riscv_extras_sequential.lem (renamed from lem/riscv_extras_sequential.lem) | 0 |
9 files changed, 89 insertions, 90 deletions
@@ -70,18 +70,18 @@ interpret: $(SAIL_SRCS) model/main.sail cgen: $(SAIL_SRCS) model/main.sail $(SAIL) -cgen $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail -generated_models/ocaml/riscv.ml: $(SAIL_SRCS) Makefile - mkdir -p generated_models/ocaml - $(SAIL) $(SAIL_FLAGS) -ocaml -ocaml-nobuild -ocaml_build_dir generated_models/ocaml -o riscv $(SAIL_SRCS) +generated_definitions/ocaml/riscv.ml: $(SAIL_SRCS) Makefile + mkdir -p generated_definitions/ocaml + $(SAIL) $(SAIL_FLAGS) -ocaml -ocaml-nobuild -ocaml_build_dir generated_definitions/ocaml -o riscv $(SAIL_SRCS) -ocaml_emulator/_sbuild/riscv_ocaml_sim.native: generated_models/ocaml/riscv.ml ocaml_emulator/_tags $(PLATFORM_OCAML_SRCS) Makefile +ocaml_emulator/_sbuild/riscv_ocaml_sim.native: generated_definitions/ocaml/riscv.ml ocaml_emulator/_tags $(PLATFORM_OCAML_SRCS) Makefile mkdir -p ocaml_emulator/_sbuild - cp ocaml_emulator/_tags $(PLATFORM_OCAML_SRCS) generated_models/ocaml/*.ml ocaml_emulator/_sbuild + cp ocaml_emulator/_tags $(PLATFORM_OCAML_SRCS) generated_definitions/ocaml/*.ml ocaml_emulator/_sbuild cd ocaml_emulator/_sbuild && ocamlbuild -use-ocamlfind riscv_ocaml_sim.native -ocaml_emulator/_sbuild/coverage.native: generated_models/ocaml/riscv.ml ocaml_emulator/_tags.bisect $(PLATFORM_OCAML_SRCS) Makefile +ocaml_emulator/_sbuild/coverage.native: generated_definitions/ocaml/riscv.ml ocaml_emulator/_tags.bisect $(PLATFORM_OCAML_SRCS) Makefile mkdir -p ocaml_emulator/_sbuild - cp $(PLATFORM_OCAML_SRCS) generated_models/ocaml/*.ml ocaml_emulator/_sbuild + cp $(PLATFORM_OCAML_SRCS) generated_definitions/ocaml/*.ml ocaml_emulator/_sbuild cp ocaml_emulator/_tags.bisect ocaml_emulator/_sbuild/_tags cd ocaml_emulator/_sbuild && ocamlbuild -use-ocamlfind riscv_ocaml_sim.native && cp -L riscv_ocaml_sim.native coverage.native @@ -98,100 +98,100 @@ ocaml_emulator/coverage: ocaml_emulator/_sbuild/coverage.native gcovr: gcovr -r . --html --html-detail -o index.html -generated_models/ocaml/riscv_duopod_ocaml: model/prelude.sail model/riscv_duopod.sail - mkdir -p generated_models/ocaml - $(SAIL) $(SAIL_FLAGS) -ocaml -ocaml_build_dir generated_models/ocaml -o riscv_duopod_ocaml $^ +generated_definitions/ocaml/riscv_duopod_ocaml: model/prelude.sail model/riscv_duopod.sail + mkdir -p generated_definitions/ocaml + $(SAIL) $(SAIL_FLAGS) -ocaml -ocaml_build_dir generated_definitions/ocaml -o riscv_duopod_ocaml $^ ocaml_emulator/tracecmp: ocaml_emulator/tracecmp.ml ocamlfind ocamlopt -annot -linkpkg -package unix $^ -o $@ -generated_models/c/riscv.c: $(SAIL_SRCS) model/main.sail Makefile - mkdir -p generated_models/c +generated_definitions/c/riscv.c: $(SAIL_SRCS) model/main.sail Makefile + mkdir -p generated_definitions/c $(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h $(SAIL_SRCS) model/main.sail 1> $@ -c_emulator/riscv_c: generated_models/c/riscv.c $(C_INCS) $(C_SRCS) Makefile +c_emulator/riscv_c: generated_definitions/c/riscv.c $(C_INCS) $(C_SRCS) Makefile gcc $(C_WARNINGS) $(C_FLAGS) $< $(C_SRCS) $(SAIL_LIB_DIR)/*.c -lgmp -lz -I $(SAIL_LIB_DIR) -o $@ -generated_models/c/riscv_model.c: $(SAIL_SRCS) model/main.sail Makefile - mkdir -p generated_models/c +generated_definitions/c/riscv_model.c: $(SAIL_SRCS) model/main.sail Makefile + mkdir -p generated_definitions/c $(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail 1> $@ -c_emulator/riscv_sim: generated_models/c/riscv_model.c c_emulator/riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile +c_emulator/riscv_sim: generated_definitions/c/riscv_model.c c_emulator/riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile gcc -g $(C_WARNINGS) $(C_FLAGS) $< c_emulator/riscv_sim.c $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ -generated_models/c/riscv_rvfi_model.c: $(SAIL_RVFI_SRCS) model/main_rvfi.sail Makefile - mkdir -p generated_models/c +generated_definitions/c/riscv_rvfi_model.c: $(SAIL_RVFI_SRCS) model/main_rvfi.sail Makefile + mkdir -p generated_definitions/c $(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main_rvfi.sail | sed '/^[[:space:]]*$$/d' > $@ -c_emulator/riscv_rvfi: generated_models/c/riscv_rvfi_model.c c_emulator/riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile +c_emulator/riscv_rvfi: generated_definitions/c/riscv_rvfi_model.c c_emulator/riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile gcc -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII c_emulator/riscv_sim.c $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ latex: $(SAIL_SRCS) Makefile - mkdir -p generated_models/latex - $(SAIL) -latex -latex_prefix sail -o generated_models/latex $(SAIL_SRCS) - -generated_models/lem/riscv_duopod.lem: $(addprefix model/, prelude.sail riscv_duopod.sail) - mkdir -p generated_models/lem - $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_models/lem -lem_mwords -lem_lib Riscv_extras -o riscv_duopod $^ -generated_models/isabelle/Riscv_duopod.thy: generated_models/lem/riscv_duopod.lem lem/riscv_extras.lem - lem -isa -outdir generated_models/isabelle -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ - lem/riscv_extras.lem \ - generated_models/lem/riscv_duopod_types.lem \ - generated_models/lem/riscv_duopod.lem - -riscv_duopod: generated_models/ocaml/riscv_duopod_ocaml generated_models/isabelle/Riscv_duopod.thy - -riscv_isa: generated_models/isabelle/Riscv.thy - -generated_models/lem/riscv.lem: $(SAIL_SRCS) Makefile - mkdir -p generated_models/lem - $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_models/lem -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS) - -generated_models/lem/riscv_sequential.lem: $(SAIL_SRCS) Makefile - mkdir -p generated_models/lem - $(SAIL_DIR)/sail -lem -lem_output_dir generated_models/lem -lem_sequential -o riscv_sequential -lem_mwords -lem_lib Riscv_extras_sequential $(SAIL_SRCS) - -generated_models/isabelle/Riscv.thy: generated_models/lem/riscv.lem lem/riscv_extras.lem Makefile - mkdir -p generated_models/isabelle - lem -isa -outdir generated_models/isabelle -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ - lem/riscv_extras.lem \ - generated_models/lem/riscv_types.lem \ - generated_models/lem/riscv.lem - sed -i 's/datatype ast/datatype (plugins only: size) ast/' generated_models/isabelle/Riscv_types.thy - -generated_models/hol4/riscvScript.sml: generated_models/lem/riscv.lem lem/riscv_extras.lem - mkdir -p generated_models/hol4 - lem -hol -outdir generated_models/hol4 -lib $(SAIL_LIB_DIR)/hol -i $(SAIL_LIB_DIR)/hol/sail2_prompt_monad.lem -i $(SAIL_LIB_DIR)/hol/sail2_prompt.lem \ + mkdir -p generated_definitions/latex + $(SAIL) -latex -latex_prefix sail -o generated_definitions/latex $(SAIL_SRCS) + +generated_definitions/lem/riscv_duopod.lem: $(addprefix model/, prelude.sail riscv_duopod.sail) + mkdir -p generated_definitions/lem + $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem -lem_mwords -lem_lib Riscv_extras -o riscv_duopod $^ +generated_definitions/isabelle/Riscv_duopod.thy: generated_definitions/lem/riscv_duopod.lem handwritten_support/riscv_extras.lem + lem -isa -outdir generated_definitions/isabelle -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ + handwritten_support/riscv_extras.lem \ + generated_definitions/lem/riscv_duopod_types.lem \ + generated_definitions/lem/riscv_duopod.lem + +riscv_duopod: generated_definitions/ocaml/riscv_duopod_ocaml generated_definitions/isabelle/Riscv_duopod.thy + +riscv_isa: generated_definitions/isabelle/Riscv.thy + +generated_definitions/lem/riscv.lem: $(SAIL_SRCS) Makefile + mkdir -p generated_definitions/lem + $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS) + +generated_definitions/lem/riscv_sequential.lem: $(SAIL_SRCS) Makefile + mkdir -p generated_definitions/lem + $(SAIL_DIR)/sail -lem -lem_output_dir generated_definitions/lem -lem_sequential -o riscv_sequential -lem_mwords -lem_lib Riscv_extras_sequential $(SAIL_SRCS) + +generated_definitions/isabelle/Riscv.thy: generated_definitions/lem/riscv.lem handwritten_support/riscv_extras.lem Makefile + mkdir -p generated_definitions/isabelle + lem -isa -outdir generated_definitions/isabelle -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ + handwritten_support/riscv_extras.lem \ + generated_definitions/lem/riscv_types.lem \ + generated_definitions/lem/riscv.lem + sed -i 's/datatype ast/datatype (plugins only: size) ast/' generated_definitions/isabelle/Riscv_types.thy + +generated_definitions/hol4/riscvScript.sml: generated_definitions/lem/riscv.lem handwritten_support/riscv_extras.lem + mkdir -p generated_definitions/hol4 + lem -hol -outdir generated_definitions/hol4 -lib $(SAIL_LIB_DIR)/hol -i $(SAIL_LIB_DIR)/hol/sail2_prompt_monad.lem -i $(SAIL_LIB_DIR)/hol/sail2_prompt.lem \ -lib $(SAIL_DIR)/src/lem_interp -lib $(SAIL_DIR)/src/gen_lib \ - lem/riscv_extras.lem \ - generated_models/lem/riscv_types.lem \ - generated_models/lem/riscv.lem + handwritten_support/riscv_extras.lem \ + generated_definitions/lem/riscv_types.lem \ + generated_definitions/lem/riscv.lem -$(addprefix generated_models/hol4/,riscvTheory.uo riscvTheory.ui): generated_models/hol4/riscvScript.sml - (cd generated_models/hol4 && Holmake riscvTheory.uo) +$(addprefix generated_definitions/hol4/,riscvTheory.uo riscvTheory.ui): generated_definitions/hol4/riscvScript.sml + (cd generated_definitions/hol4 && Holmake riscvTheory.uo) -COQ_LIBS = -R $(BBV_DIR)/theories bbv -R $(SAIL_LIB_DIR)/coq Sail -R coq '' -R generated_models/coq '' +COQ_LIBS = -R $(BBV_DIR)/theories bbv -R $(SAIL_LIB_DIR)/coq Sail -R coq '' -R generated_definitions/coq '' -riscv_coq: $(addprefix generated_models/coq/,riscv.v riscv_types.v) +riscv_coq: $(addprefix generated_definitions/coq/,riscv.v riscv_types.v) -$(addprefix generated_models/coq/,riscv.v riscv_types.v): $(SAIL_COQ_SRCS) Makefile - mkdir -p generated_models/coq - $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_models/coq -o riscv -coq_lib riscv_extras $(SAIL_COQ_SRCS) -$(addprefix generated_models/coq/,riscv_duopod.v riscv_duopod_types.v): model/prelude.sail model/riscv_duopod.sail - mkdir -p generated_models/coq - $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_models/coq -o riscv_duopod -coq_lib riscv_extras $^ +$(addprefix generated_definitions/coq/,riscv.v riscv_types.v): $(SAIL_COQ_SRCS) Makefile + mkdir -p generated_definitions/coq + $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq -o riscv -coq_lib riscv_extras $(SAIL_COQ_SRCS) +$(addprefix generated_definitions/coq/,riscv_duopod.v riscv_duopod_types.v): model/prelude.sail model/riscv_duopod.sail + mkdir -p generated_definitions/coq + $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq -o riscv_duopod -coq_lib riscv_extras $^ %.vo: %.v coqc $(COQ_LIBS) $< -generated_models/coq/riscv.vo: generated_models/coq/riscv_types.vo coq/riscv_extras.vo -generated_models/coq/riscv_duopod.vo: generated_models/coq/riscv_duopod_types.vo coq/riscv_extras.vo +generated_definitions/coq/riscv.vo: generated_definitions/coq/riscv_types.vo handwritten_support/riscv_extras.vo +generated_definitions/coq/riscv_duopod.vo: generated_definitions/coq/riscv_duopod_types.vo handwritten_support/riscv_extras.vo # we exclude prelude.sail here, most code there should move to sail lib #LOC_FILES:=$(SAIL_SRCS) main.sail #include $(SAIL_DIR)/etc/loc.mk clean: - -rm -rf generated_models/ocaml/* generated_models/c/* - -rm -rf generated_models/lem/* generated_models/isabelle/* generated_models/hol4/* generated_models/coq/* + -rm -rf generated_definitions/ocaml/* generated_definitions/c/* + -rm -rf generated_definitions/lem/* generated_definitions/isabelle/* generated_definitions/hol4/* generated_definitions/coq/* -rm -f c_emulator/riscv_sim c_emulator/riscv_rvfi -rm -rf ocaml_emulator/_sbuild ocaml_emulator/_build ocaml_emulator/riscv_ocaml_sim ocaml_emulator/tracecmp -rm -f *.gcno *.gcda @@ -16,27 +16,26 @@ Directory Structure ``` sail-riscv | -+---- model // Sail specification modules ++---- model // Sail specification modules | -+---- generated_models // Files generated by Sail ++---- generated_definitions // Files generated by Sail | | -| +---- c // C simulator definitions -| +---- ocaml // OCaml simulator definitions -| +---- lem // Lem model -| +---- isabelle // Isabelle model -| +---- coq // Coq model -| +---- hol4 // HOL4 model +| +---- c +| +---- ocaml +| +---- lem +| +---- isabelle +| +---- coq +| +---- hol4 +| +---- latex | -| // Handwritten files +|---- handwritten_support // Prover support files | -+---- c_emulator // supporting platform files for C emulator -+---- ocaml_emulator // supporting platform files for OCaml emulator -+---- lem // Lem library -+---- coq // Coq library ++---- c_emulator // supporting platform files for C emulator ++---- ocaml_emulator // supporting platform files for OCaml emulator | -+---- test // test files ++---- test // test files | - +---- riscv-tests // snapshot of tests from the riscv/riscv-tests github repo + +---- riscv-tests // snapshot of tests from the riscv/riscv-tests github repo ``` An outline of the specification @@ -81,8 +80,8 @@ your environment pointing to its top-level directory. $ make ``` will build the OCaml simulator in `ocaml_emulator/riscv_ocaml_sim`, the C simulator in -`c_emulator/riscv_sim`, the Isabelle model in `generated_models/isabelle/Riscv.thy`, and the Coq -model in `generated_models/coq/riscv.v`. +`c_emulator/riscv_sim`, the Isabelle model in `generated_definitions/isabelle/Riscv.thy`, and the Coq +model in `generated_definitions/coq/riscv.v`. Executing test binaries ----------------------- diff --git a/reset_vec.S b/c_emulator/reset_vec.S index 526bbc7..526bbc7 100644 --- a/reset_vec.S +++ b/c_emulator/reset_vec.S diff --git a/reset_vec.bin b/c_emulator/reset_vec.bin Binary files differindex d2d3563..d2d3563 100755 --- a/reset_vec.bin +++ b/c_emulator/reset_vec.bin diff --git a/hol4/Holmakefile b/handwritten_support/Holmakefile index 8269bc3..8269bc3 100644 --- a/hol4/Holmakefile +++ b/handwritten_support/Holmakefile diff --git a/isabelle/ROOT b/handwritten_support/ROOT index 4dcebbc..5452298 100644 --- a/isabelle/ROOT +++ b/handwritten_support/ROOT @@ -1,9 +1,9 @@ session "Sail-RISC-V" = "Sail" + options [document = false] theories - "../generated_models/lem/Riscv_lemmas" + "../generated_definitions/lem/Riscv_lemmas" session "Sail-RISC-V-Duopod" = "Sail" + options [document = false] theories - "../generated_models/lem/Riscv_duopod_lemmas" + "../generated_definitions/lem/Riscv_duopod_lemmas" diff --git a/lem/riscv_extras.lem b/handwritten_support/riscv_extras.lem index c1a52c9..c1a52c9 100644 --- a/lem/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem diff --git a/coq/riscv_extras.v b/handwritten_support/riscv_extras.v index ff235a9..ff235a9 100644 --- a/coq/riscv_extras.v +++ b/handwritten_support/riscv_extras.v diff --git a/lem/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index c1a52c9..c1a52c9 100644 --- a/lem/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem |