diff options
| -rw-r--r-- | Makefile | 55 | ||||
| -rw-r--r-- | README.md | 14 | ||||
| -rw-r--r-- | c_emulator/riscv_config.h (renamed from c/riscv_config.h) | 0 | ||||
| -rw-r--r-- | c_emulator/riscv_platform.c (renamed from c/riscv_platform.c) | 0 | ||||
| -rw-r--r-- | c_emulator/riscv_platform.h (renamed from c/riscv_platform.h) | 0 | ||||
| -rw-r--r-- | c_emulator/riscv_platform_impl.c (renamed from c/riscv_platform_impl.c) | 0 | ||||
| -rw-r--r-- | c_emulator/riscv_platform_impl.h (renamed from c/riscv_platform_impl.h) | 0 | ||||
| -rw-r--r-- | c_emulator/riscv_prelude.c (renamed from c/riscv_prelude.c) | 0 | ||||
| -rw-r--r-- | c_emulator/riscv_prelude.h (renamed from c/riscv_prelude.h) | 0 | ||||
| -rw-r--r-- | c_emulator/riscv_sail.h (renamed from c/riscv_sail.h) | 0 | ||||
| -rw-r--r-- | c_emulator/riscv_sim.c (renamed from c/riscv_sim.c) | 0 | ||||
| -rw-r--r-- | ocaml_emulator/_tags (renamed from ocaml/_tags) | 0 | ||||
| -rw-r--r-- | ocaml_emulator/_tags.bisect (renamed from ocaml/_tags.bisect) | 0 | ||||
| -rw-r--r-- | ocaml_emulator/platform.ml (renamed from ocaml/platform.ml) | 0 | ||||
| -rw-r--r-- | ocaml_emulator/platform_impl.ml (renamed from ocaml/platform_impl.ml) | 0 | ||||
| -rw-r--r-- | ocaml_emulator/riscv_ocaml_sim.ml (renamed from ocaml/riscv_ocaml_sim.ml) | 0 | ||||
| -rw-r--r-- | ocaml_emulator/tracecmp.ml (renamed from ocaml/tracecmp.ml) | 0 | ||||
| -rwxr-xr-x | test/run_tests.sh | 8 |
18 files changed, 39 insertions, 38 deletions
@@ -13,7 +13,7 @@ SAIL_RMEM_SRCS = $(addprefix model/,$(SAIL_OTHER_SRCS) $(SAIL_RMEM_INST_SRCS) ri SAIL_RVFI_SRCS = $(addprefix model/,$(SAIL_OTHER_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS) riscv_step.sail riscv_analysis.sail) SAIL_COQ_SRCS = $(addprefix model/,$(SAIL_OTHER_SRCS) $(SAIL_SEQ_INST_SRCS) riscv_termination.sail riscv_analysis.sail) -PLATFORM_OCAML_SRCS = $(addprefix ocaml/,platform.ml platform_impl.ml riscv_ocaml_sim.ml) +PLATFORM_OCAML_SRCS = $(addprefix ocaml_emulator/,platform.ml platform_impl.ml riscv_ocaml_sim.ml) #Attempt to work with either sail from opam or built from repo in SAIL_DIR ifneq ($(SAIL_DIR),) @@ -33,10 +33,10 @@ BBV_DIR?=../bbv C_WARNINGS ?= #-Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function -C_INCS = $(addprefix c/,riscv_prelude.h riscv_platform_impl.h riscv_platform.h) -C_SRCS = $(addprefix c/,riscv_prelude.c riscv_platform_impl.c riscv_platform.c) +C_INCS = $(addprefix c_emulator/,riscv_prelude.h riscv_platform_impl.h riscv_platform.h) +C_SRCS = $(addprefix c_emulator/,riscv_prelude.c riscv_platform_impl.c riscv_platform.c) -C_FLAGS = -I $(SAIL_LIB_DIR) -I c +C_FLAGS = -I $(SAIL_LIB_DIR) -I c_emulator C_LIBS = -lgmp -lz # The C simulator can be built to be linked against Spike for tandem-verification. @@ -57,7 +57,7 @@ else C_FLAGS += -O2 endif -all: ocaml/riscv_ocaml_sim c/riscv_sim riscv_isa riscv_coq +all: ocaml_emulator/riscv_ocaml_sim c_emulator/riscv_sim riscv_isa riscv_coq .PHONY: all riscv_coq riscv_isa @@ -74,25 +74,26 @@ 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) -ocaml/_sbuild/riscv_ocaml_sim.native: generated_models/ocaml/riscv.ml ocaml/_tags $(PLATFORM_OCAML_SRCS) Makefile - mkdir -p ocaml/_sbuild - cp ocaml/_tags $(PLATFORM_OCAML_SRCS) generated_models/ocaml/*.ml ocaml/_sbuild - cd ocaml/_sbuild && ocamlbuild -use-ocamlfind riscv_ocaml_sim.native +ocaml_emulator/_sbuild/riscv_ocaml_sim.native: generated_models/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 + cd ocaml_emulator/_sbuild && ocamlbuild -use-ocamlfind riscv_ocaml_sim.native -ocaml/_sbuild/coverage.native: ocaml/_sbuild/riscv.ml ocaml/_tags.bisect $(PLATFORM_OCAML_SRCS) Makefile - cp $(PLATFORM_OCAML_SRCS) generated_models/ocaml/*.ml ocaml/_sbuild - cp ocaml/_tags.bisect ocaml/_sbuild/_tags - cd ocaml/_sbuild && ocamlbuild -use-ocamlfind riscv_ocaml_sim.native && cp -L riscv_ocaml_sim.native coverage.native +ocaml_emulator/_sbuild/coverage.native: generated_models/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 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 -ocaml/riscv_ocaml_sim: ocaml/_sbuild/riscv_ocaml_sim.native +ocaml_emulator/riscv_ocaml_sim: ocaml_emulator/_sbuild/riscv_ocaml_sim.native rm -f $@ && ln -s _sbuild/riscv_ocaml_sim.native $@ -ocaml/coverage: ocaml/_sbuild/coverage.native - rm -f ocaml/riscv_ocaml_sim && ln -s _sbuild/coverage.native ocaml/riscv_ocaml_sim # since the test scripts runs this file - rm -rf bisect*.out bisect ocaml/coverage +ocaml_emulator/coverage: ocaml_emulator/_sbuild/coverage.native + rm -f ocaml_emulator/riscv_ocaml_sim && ln -s ocaml_emulator/_sbuild/coverage.native ocaml_emulator/riscv_ocaml_sim # since the test scripts runs this file + rm -rf bisect*.out bisect ocaml_emulator/coverage ./test/run_tests.sh # this will generate bisect*.out files in this directory - mkdir ocaml/bisect && mv bisect*.out bisect/ - mkdir ocaml/coverage && bisect-ppx-report -html ocaml/coverage/ -I ocaml/_sbuild/ bisect/bisect*.out + mkdir ocaml_emulator/bisect && mv bisect*.out bisect/ + mkdir ocaml_emulator/coverage && bisect-ppx-report -html ocaml_emulator/coverage/ -I ocaml_emulator/_sbuild/ bisect/bisect*.out gcovr: gcovr -r . --html --html-detail -o index.html @@ -101,29 +102,29 @@ generated_models/ocaml/riscv_duopod_ocaml: model/prelude.sail model/riscv_duopod mkdir -p generated_models/ocaml $(SAIL) $(SAIL_FLAGS) -ocaml -ocaml_build_dir generated_models/ocaml -o riscv_duopod_ocaml $^ -ocaml/tracecmp: ocaml/tracecmp.ml +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 $(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h $(SAIL_SRCS) model/main.sail 1> $@ -c/riscv_c: generated_models/c/riscv.c $(C_INCS) $(C_SRCS) Makefile +c_emulator/riscv_c: generated_models/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 $(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/riscv_sim: generated_models/c/riscv_model.c c/riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile - gcc -g $(C_WARNINGS) $(C_FLAGS) $< c/riscv_sim.c $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ +c_emulator/riscv_sim: generated_models/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 $(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/riscv_rvfi: generated_models/c/riscv_rvfi_model.c c/riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile - gcc -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII c/riscv_sim.c $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ +c_emulator/riscv_rvfi: generated_models/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 $(SAIL) -latex -latex_prefix sail -o sail_ltx $(SAIL_SRCS) @@ -190,8 +191,8 @@ generated_models/coq/riscv_duopod.vo: generated_models/coq/riscv_duopod_types.vo clean: -rm -rf generated_models/ocaml/* generated_models/c/* -rm -rf generated_models/lem/* generated_models/isabelle/* generated_models/hol4/* generated_models/coq/* - -rm -f c/riscv_sim c/riscv_rvfi - -rm -rf ocaml/_sbuild ocaml/_build ocaml/riscv_ocaml_sim ocaml/tracecmp + -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 -Holmake cleanAll ocamlbuild -clean @@ -77,8 +77,8 @@ your environment pointing to its top-level directory. ``` $ make ``` -will build the OCaml simulator in `ocaml/riscv_ocaml_sim`, the C simulator in -`c/riscv_sim`, the Isabelle model in `generated_models/isabelle/Riscv.thy`, and the Coq +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`. Executing test binaries @@ -87,11 +87,11 @@ Executing test binaries The C and OCaml simulators can be used to execute small test RV64 binaries. ``` -$ ./ocaml/riscv_ocaml_sim <elf-file> -$ ./c/riscv_sim <elf-file> +$ ./ocaml_emulator/riscv_ocaml_sim <elf-file> +$ ./c_emulator/riscv_sim <elf-file> ``` Some information on additional configuration options for each simulator is available -from `./ocaml/riscv_ocaml_sim -h` and `./c/riscv_sim -h`. +from `./ocaml_emulator/riscv_ocaml_sim -h` and `./c_emulator/riscv_sim -h`. Booting Linux with the C backend -------------------------------- @@ -103,7 +103,7 @@ a DTB (device-tree blob) file describing the platform (say in the file the model should be run as: ``` -$ ./c/riscv_sim -t console.log -b spike.dtb bbl > execution-trace.log 2>&1 & +$ ./c_emulator/riscv_sim -t console.log -b spike.dtb bbl > execution-trace.log 2>&1 & $ tail -f console.log ``` The `console.log` file contains the console boot messages. @@ -114,7 +114,7 @@ Booting Linux with the OCaml backend The OCaml model only needs the ELF-version of the BBL, since it can generate its own DTB. ``` -$ ./ocaml/riscv_ocaml_sim bbl > execution-trace.log 2> console.log +$ ./ocaml_emulator/riscv_ocaml_sim bbl > execution-trace.log 2> console.log ``` Generating input files for Linux boot diff --git a/c/riscv_config.h b/c_emulator/riscv_config.h index f8f3eb3..f8f3eb3 100644 --- a/c/riscv_config.h +++ b/c_emulator/riscv_config.h diff --git a/c/riscv_platform.c b/c_emulator/riscv_platform.c index 3587206..3587206 100644 --- a/c/riscv_platform.c +++ b/c_emulator/riscv_platform.c diff --git a/c/riscv_platform.h b/c_emulator/riscv_platform.h index 728555e..728555e 100644 --- a/c/riscv_platform.h +++ b/c_emulator/riscv_platform.h diff --git a/c/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index 04a661c..04a661c 100644 --- a/c/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c diff --git a/c/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index 85e25c9..85e25c9 100644 --- a/c/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h diff --git a/c/riscv_prelude.c b/c_emulator/riscv_prelude.c index 1621913..1621913 100644 --- a/c/riscv_prelude.c +++ b/c_emulator/riscv_prelude.c diff --git a/c/riscv_prelude.h b/c_emulator/riscv_prelude.h index a296c7e..a296c7e 100644 --- a/c/riscv_prelude.h +++ b/c_emulator/riscv_prelude.h diff --git a/c/riscv_sail.h b/c_emulator/riscv_sail.h index 424b64b..424b64b 100644 --- a/c/riscv_sail.h +++ b/c_emulator/riscv_sail.h diff --git a/c/riscv_sim.c b/c_emulator/riscv_sim.c index 2a70167..2a70167 100644 --- a/c/riscv_sim.c +++ b/c_emulator/riscv_sim.c diff --git a/ocaml/_tags b/ocaml_emulator/_tags index 168de09..168de09 100644 --- a/ocaml/_tags +++ b/ocaml_emulator/_tags diff --git a/ocaml/_tags.bisect b/ocaml_emulator/_tags.bisect index ca6f27a..ca6f27a 100644 --- a/ocaml/_tags.bisect +++ b/ocaml_emulator/_tags.bisect diff --git a/ocaml/platform.ml b/ocaml_emulator/platform.ml index 6ee2d2b..6ee2d2b 100644 --- a/ocaml/platform.ml +++ b/ocaml_emulator/platform.ml diff --git a/ocaml/platform_impl.ml b/ocaml_emulator/platform_impl.ml index 3eb8217..3eb8217 100644 --- a/ocaml/platform_impl.ml +++ b/ocaml_emulator/platform_impl.ml diff --git a/ocaml/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml index 1c9ba20..1c9ba20 100644 --- a/ocaml/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml diff --git a/ocaml/tracecmp.ml b/ocaml_emulator/tracecmp.ml index 64a918d..64a918d 100644 --- a/ocaml/tracecmp.ml +++ b/ocaml_emulator/tracecmp.ml diff --git a/test/run_tests.sh b/test/run_tests.sh index 491c64c..d45e682 100755 --- a/test/run_tests.sh +++ b/test/run_tests.sh @@ -51,7 +51,7 @@ cd $RISCVDIR printf "Building RISCV specification...\n" -if make ocaml/platform ; +if make ocaml_emulator/riscv_ocaml_sim ; then green "Building RISCV specification" "ok" else @@ -59,7 +59,7 @@ else fi for test in $DIR/tests/*.elf; do - if $RISCVDIR/ocaml/platform "$test" >"${test/.elf/.out}" 2>&1 && grep -q SUCCESS "${test/.elf/.out}" + if $RISCVDIR/ocaml_emulator/riscv_ocaml_sim "$test" >"${test/.elf/.out}" 2>&1 && grep -q SUCCESS "${test/.elf/.out}" then green "$(basename $test)" "ok" else @@ -69,7 +69,7 @@ done finish_suite "RISCV OCaml tests" -if make c/riscv_sim; +if make c_emulator/riscv_sim; then green "Building RISCV specification to C" "ok" else @@ -77,7 +77,7 @@ else fi for test in $DIR/tests/*.elf; do - if timeout 5 $RISCVDIR/c/riscv_sim -p $test > ${test%.elf}.cout 2>&1 && grep -q SUCCESS ${test%.elf}.cout + if timeout 5 $RISCVDIR/c_emulator/riscv_sim -p $test > ${test%.elf}.cout 2>&1 && grep -q SUCCESS ${test%.elf}.cout then green "$(basename $test)" "ok" else |