Reorganize directory structure.

41 files changed, 128 insertions, 108 deletions

diff --git a/Makefile b/Makefile
index 397ec4c..13ca925 100644
--- a/Makefile
+++ b/Makefile
@@ -8,12 +8,12 @@ SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.s
 SAIL_OTHER_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail
 SAIL_OTHER_RVFI_SRCS = prelude.sail rvfi_dii.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail
 
-SAIL_SRCS      = $(SAIL_OTHER_SRCS) $(SAIL_SEQ_INST_SRCS)  riscv_step.sail riscv_analysis.sail
-SAIL_RMEM_SRCS = $(SAIL_OTHER_SRCS) $(SAIL_RMEM_INST_SRCS) riscv_step.sail riscv_analysis.sail
-SAIL_RVFI_SRCS = $(SAIL_OTHER_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS)  riscv_step.sail riscv_analysis.sail
-SAIL_COQ_SRCS  = $(SAIL_OTHER_SRCS) $(SAIL_SEQ_INST_SRCS)  riscv_termination.sail riscv_analysis.sail
+SAIL_SRCS      = $(addprefix model/,$(SAIL_OTHER_SRCS) $(SAIL_SEQ_INST_SRCS)  riscv_step.sail riscv_analysis.sail)
+SAIL_RMEM_SRCS = $(addprefix model/,$(SAIL_OTHER_SRCS) $(SAIL_RMEM_INST_SRCS) riscv_step.sail riscv_analysis.sail)
+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 = platform.ml platform_impl.ml platform_main.ml
+PLATFORM_OCAML_SRCS = $(addprefix ocaml/,platform.ml platform_impl.ml platform_main.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 = riscv_prelude.h riscv_platform_impl.h riscv_platform.h
-C_SRCS = riscv_prelude.c riscv_platform_impl.c riscv_platform.c
+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_FLAGS = -I $(SAIL_LIB_DIR)
+C_FLAGS = -I $(SAIL_LIB_DIR) -I c
 C_LIBS  = -lgmp -lz
 
 # The C simulator can be built to be linked against Spike for tandem-verification.
@@ -57,135 +57,129 @@ else
 C_FLAGS += -O2
 endif
 
-all: platform riscv_sim riscv_isa riscv_coq
+all: ocaml/platform c/riscv_sim riscv_isa riscv_coq
 
 .PHONY: all riscv_coq riscv_isa
 
-check: $(SAIL_SRCS) main.sail Makefile
-	$(SAIL) $(SAIL_FLAGS) $(SAIL_SRCS) main.sail
+check: $(SAIL_SRCS) model/main.sail Makefile
+	$(SAIL) $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail
 
-interpret: $(SAIL_SRCS)
-	$(SAIL) -i $(SAIL_FLAGS) $(SAIL_SRCS) main.sail
+interpret: $(SAIL_SRCS) model/main.sail
+	$(SAIL) -i $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail
 
-cgen: $(SAIL_SRCS)
-	$(SAIL) -cgen $(SAIL_FLAGS) $(SAIL_SRCS) main.sail
+cgen: $(SAIL_SRCS) model/main.sail
+	$(SAIL) -cgen $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail
 
-_sbuild/riscv.ml: $(SAIL_SRCS) Makefile main.sail
-	$(SAIL) $(SAIL_FLAGS) -ocaml -ocaml-nobuild -o riscv $(SAIL_SRCS)
+generated_models/ocaml/riscv.ml: $(SAIL_SRCS) Makefile
+	$(SAIL) $(SAIL_FLAGS) -ocaml -ocaml-nobuild -ocaml_build_dir generated_models/ocaml -o riscv $(SAIL_SRCS)
 
-_sbuild/platform_main.native: _sbuild/riscv.ml _tags $(PLATFORM_OCAML_SRCS) Makefile
-	cp _tags $(PLATFORM_OCAML_SRCS) _sbuild
-	cd _sbuild && ocamlbuild -use-ocamlfind platform_main.native
+ocaml/_sbuild/platform_main.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 platform_main.native
 
-_sbuild/coverage.native: _sbuild/riscv.ml _tags.bisect $(PLATFORM_OCAML_SRCS) Makefile
-	cp $(PLATFORM_OCAML_SRCS) _sbuild
-	cp _tags.bisect _sbuild/_tags
-	cd _sbuild && ocamlbuild -use-ocamlfind platform_main.native && cp -L platform_main.native coverage.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 platform_main.native && cp -L platform_main.native coverage.native
 
-platform: _sbuild/platform_main.native
-	rm -f $@ && ln -s $^ $@
+ocaml/platform: ocaml/_sbuild/platform_main.native
+	rm -f $@ && ln -s _sbuild/platform_main.native $@
 
-coverage: _sbuild/coverage.native
-	rm -f platform && ln -s $^ platform # since the test scripts runs this file
-	rm -rf bisect*.out bisect coverage
-	../test/riscv/run_tests.sh # this will generate bisect*.out files in this directory
-	mkdir bisect && mv bisect*.out bisect/
-	mkdir coverage && bisect-ppx-report -html coverage/ -I _sbuild/ bisect/bisect*.out
+ocaml/coverage: ocaml/_sbuild/coverage.native
+	rm -f ocaml/platform && ln -s _sbuild/coverage.native ocaml/platform # since the test scripts runs this file
+	rm -rf bisect*.out bisect ocaml/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
 
 gcovr:
 	gcovr -r . --html --html-detail -o index.html
 
-riscv.c: $(SAIL_SRCS) main.sail Makefile
-	$(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h $(SAIL_SRCS) main.sail 1> $@
+generated_models/ocaml/riscv_duopod_ocaml: model/prelude.sail model/riscv_duopod.sail
+	$(SAIL) $(SAIL_FLAGS) -ocaml -ocaml_build_dir generated_models/ocaml -o riscv_duopod_ocaml $^
 
-riscv_c: riscv.c $(C_INCS) $(C_SRCS) Makefile
-	gcc $(C_WARNINGS) $(C_FLAGS) riscv.c $(C_SRCS) $(SAIL_LIB_DIR)/*.c -lgmp -lz -I $(SAIL_LIB_DIR) -o riscv_c
+ocaml/tracecmp: ocaml/tracecmp.ml
+	ocamlfind ocamlopt -annot -linkpkg -package unix $^ -o $@
 
-riscv_model.c: $(SAIL_SRCS) main.sail Makefile
-	$(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) main.sail 1> $@
+generated_models/c/riscv.c: $(SAIL_SRCS) model/main.sail Makefile
+	$(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h $(SAIL_SRCS) model/main.sail 1> $@
 
-riscv_sim: riscv_model.c riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile
-	gcc -g $(C_WARNINGS) $(C_FLAGS) riscv_model.c riscv_sim.c $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
+c/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 $@
 
-riscv_rvfi_model.c: $(SAIL_RVFI_SRCS) main_rvfi.sail Makefile
-	$(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) main_rvfi.sail | sed '/^[[:space:]]*$$/d' > $@
+generated_models/c/riscv_model.c: $(SAIL_SRCS) model/main.sail Makefile
+	$(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> $@
 
-riscv_rvfi: riscv_rvfi_model.c riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile
-	gcc -g $(C_WARNINGS) $(C_FLAGS) riscv_rvfi_model.c -DRVFI_DII riscv_sim.c $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
+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 $@
 
-latex: $(SAIL_SRCS) Makefile
-	$(SAIL) -latex -latex_prefix sail -o sail_ltx $(SAIL_SRCS)
+generated_models/c/riscv_rvfi_model.c: $(SAIL_RVFI_SRCS) model/main_rvfi.sail Makefile
+	$(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' > $@
 
-tracecmp: tracecmp.ml
-	ocamlfind ocamlopt -annot -linkpkg -package unix $^ -o $@
+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 $@
 
-riscv_duopod_ocaml: prelude.sail riscv_duopod.sail
-	$(SAIL) $(SAIL_FLAGS) -ocaml -o $@ $^
+latex: $(SAIL_SRCS) Makefile
+	$(SAIL) -latex -latex_prefix sail -o sail_ltx $(SAIL_SRCS)
 
-riscv_duopod.lem: prelude.sail riscv_duopod.sail
-	$(SAIL) $(SAIL_FLAGS) -lem -lem_mwords -lem_lib Riscv_extras -o riscv_duopod $^
-Riscv_duopod.thy: riscv_duopod.lem riscv_extras.lem
-	lem -isa -outdir . -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \
-		riscv_extras.lem \
-		riscv_duopod_types.lem \
-		riscv_duopod.lem
+generated_models/lem/riscv_duopod.lem: $(addprefix model/, prelude.sail riscv_duopod.sail)
+	$(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: riscv_duopod_ocaml Riscv_duopod.thy
+riscv_duopod: generated_models/ocaml/riscv_duopod_ocaml generated_models/isabelle/Riscv_duopod.thy
 
-riscv_isa: Riscv.thy
+riscv_isa: generated_models/isabelle/Riscv.thy
 
-Riscv.thy: riscv.lem riscv_extras.lem Makefile
-	lem -isa -outdir . -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \
-		riscv_extras.lem \
-		riscv_types.lem \
-		riscv.lem
-	sed -i 's/datatype ast/datatype (plugins only: size) ast/' Riscv_types.thy
+generated_models/lem/riscv.lem: $(SAIL_SRCS) Makefile
+	$(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_models/lem -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS)
 
-riscv.lem: $(SAIL_SRCS) Makefile
-	$(SAIL) $(SAIL_FLAGS) -lem -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS)
+generated_models/lem/riscv_sequential.lem: $(SAIL_SRCS) Makefile
+	$(SAIL_DIR)/sail -lem -lem_output_dir generated_models/lem -lem_sequential -o riscv_sequential -lem_mwords -lem_lib Riscv_extras_sequential $(SAIL_SRCS)
 
-riscv_sequential.lem: $(SAIL_SRCS) Makefile
-	$(SAIL_DIR)/sail -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
+	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
 
-riscvScript.sml : riscv.lem riscv_extras.lem
-	lem -hol -outdir . -lib $(SAIL_LIB_DIR)/hol -i $(SAIL_LIB_DIR)/hol/sail2_prompt_monad.lem -i $(SAIL_LIB_DIR)/hol/sail2_prompt.lem \
+generated_models/hol4/riscvScript.sml: generated_models/lem/riscv.lem lem/riscv_extras.lem
+	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 \
 	    -lib $(SAIL_DIR)/src/lem_interp -lib $(SAIL_DIR)/src/gen_lib \
-		riscv_extras.lem \
-		riscv_types.lem \
-		riscv.lem
+		lem/riscv_extras.lem \
+		generated_models/lem/riscv_types.lem \
+		generated_models/lem/riscv.lem
 
-riscvTheory.uo riscvTheory.ui: riscvScript.sml
-	Holmake riscvTheory.uo
+$(addprefix generated_models/hol4/,riscvTheory.uo riscvTheory.ui): generated_models/hol4/riscvScript.sml
+	(cd generated_models/hol4 && Holmake riscvTheory.uo)
 
-COQ_LIBS = -R $(BBV_DIR)/theories bbv -R $(SAIL_LIB_DIR)/coq Sail
+COQ_LIBS = -R $(BBV_DIR)/theories bbv -R $(SAIL_LIB_DIR)/coq Sail -R coq '' -R generated_models/coq ''
 
-riscv_coq: riscv.v riscv_types.v
+riscv_coq: $(addprefix generated_models/coq/,riscv.v riscv_types.v)
 
-riscv.v riscv_types.v: $(SAIL_COQ_SRCS) Makefile
-	$(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -o riscv -coq_lib riscv_extras $(SAIL_COQ_SRCS)
-riscv_duopod.v riscv_duopod_types.v:  prelude.sail riscv_duopod.sail
-	$(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -o riscv_duopod -coq_lib riscv_extras $^
+$(addprefix generated_models/coq/,riscv.v riscv_types.v): $(SAIL_COQ_SRCS) Makefile
+	$(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
+	$(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_models/coq -o riscv_duopod -coq_lib riscv_extras $^
 %.vo: %.v
 	coqc $(COQ_LIBS) $<
-riscv.vo: riscv_types.vo riscv_extras.vo
-riscv_duopod.vo: riscv_duopod_types.vo riscv_extras.vo
+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
 
 # 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 riscv _sbuild
-	-rm -f riscv.lem riscv_types.lem
-	-rm -f Riscv.thy Riscv_types.thy \
-		Riscv_extras.thy
-	-rm -f Riscv_duopod.thy Riscv_duopod_types.thy riscv_duopod.lem riscv_duopod_types.lem
-	-rm -f riscvScript.sml riscv_typesScript.sml riscv_extrasScript.sml
-	-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 riscv_model.c riscv_sim
-	-rm -f riscv_rvfi_model.c riscv_rvfi
+	-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/platform ocaml/tracecmp
 	-rm -f *.gcno *.gcda
 	-Holmake cleanAll
 	ocamlbuild -clean
diff --git a/README.md b/README.md
index 62c82b1..14c937c 100644
--- a/README.md
+++ b/README.md
@@ -10,10 +10,36 @@ with a terminal output device.  Work on a 32-bit model is ongoing.
 The model specifies assembly language formats of the instructions, and
 implements the corresponding encoders and decoders.
 
+Directory Structure
+-------------------
+
+```
+sail-riscv
+|
++---- model              // Sail specification modules
+|
++---- generated_models   // Files generated by Sail
+|     |
+|     +---- c            // C simulator definitions
+|     +---- ocaml        // OCaml simulator definitions
+|     +---- lem          // Lem model
+|     +---- isabelle     // Isabelle model
+|     +---- coq          // Coq model
+|     +---- hol4         // HOL4 model
+|
+|                        // Handwritten files
++---- c                  // C simulator
++---- ocaml              // OCaml simulator
++---- lem                // Lem library
++---- coq                // Coq library
+|
++---- test               // unit test files
+```
+
 An outline of the specification
 -------------------------------
 
-The model contains the following Sail modules:
+The model contains the following Sail modules in the `model` directory:
 
 - `prelude.sail` contains useful Sail library functions
 
@@ -51,9 +77,9 @@ your environment pointing to its top-level directory.
 ```
 $ make
 ```
-will build the OCaml simulator in `platform`, the C simulator in
-`riscv_sim`, the Isabelle model in `Riscv.thy`, and the Coq
-model in `riscv.v`.
+will build the OCaml simulator in `ocaml/platform`, the C simulator in
+`c/riscv_sim`, the Isabelle model in `generated_models/isabelle/Riscv.thy`, and the Coq
+model in `generated_models/coq/riscv.v`.
 
 Executing test binaries
 -----------------------
@@ -61,11 +87,11 @@ Executing test binaries
 The C and OCaml simulators can be used to execute small test RV64 binaries.
 
 ```
-$ ./platform  <elf-file>
-$ ./riscv_sim <elf-file>
+$ ./ocaml/platform  <elf-file>
+$ ./c/riscv_sim <elf-file>
 ```
 Some information on additional configuration options for each simulator is available
-from `./platform -h` and `./riscv_sim -h`.
+from `./ocaml/platform -h` and `./c/riscv_sim -h`.
 
 Booting Linux with the C backend
 --------------------------------
@@ -77,7 +103,7 @@ a DTB (device-tree blob) file describing the platform (say in the file
 the model should be run as:
 
 ```
-$ ./riscv_sim -t console.log -b spike.dtb bbl > execution-trace.log 2>&1 &
+$ ./c/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.
@@ -88,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.
 ```
-$ ./platform bbl > execution-trace.log 2> console.log
+$ ./ocaml/platform bbl > execution-trace.log 2> console.log
 ```
 
 Generating input files for Linux boot
diff --git a/riscv_config.h b/c/riscv_config.h
index f8f3eb3..f8f3eb3 100644
--- a/riscv_config.h
+++ b/c/riscv_config.h
diff --git a/riscv_platform.c b/c/riscv_platform.c
index 3587206..3587206 100644
--- a/riscv_platform.c
+++ b/c/riscv_platform.c
diff --git a/riscv_platform.h b/c/riscv_platform.h
index 728555e..728555e 100644
--- a/riscv_platform.h
+++ b/c/riscv_platform.h
diff --git a/riscv_platform_impl.c b/c/riscv_platform_impl.c
index 04a661c..04a661c 100644
--- a/riscv_platform_impl.c
+++ b/c/riscv_platform_impl.c
diff --git a/riscv_platform_impl.h b/c/riscv_platform_impl.h
index 85e25c9..85e25c9 100644
--- a/riscv_platform_impl.h
+++ b/c/riscv_platform_impl.h
diff --git a/riscv_prelude.c b/c/riscv_prelude.c
index 1621913..1621913 100644
--- a/riscv_prelude.c
+++ b/c/riscv_prelude.c
diff --git a/riscv_prelude.h b/c/riscv_prelude.h
index a296c7e..a296c7e 100644
--- a/riscv_prelude.h
+++ b/c/riscv_prelude.h
diff --git a/riscv_sail.h b/c/riscv_sail.h
index 424b64b..424b64b 100644
--- a/riscv_sail.h
+++ b/c/riscv_sail.h
diff --git a/riscv_sim.c b/c/riscv_sim.c
index 2a70167..2a70167 100644
--- a/riscv_sim.c
+++ b/c/riscv_sim.c
diff --git a/riscv_extras.v b/coq/riscv_extras.v
index ff235a9..ff235a9 100644
--- a/riscv_extras.v
+++ b/coq/riscv_extras.v
diff --git a/Holmakefile b/hol4/Holmakefile
index 8269bc3..8269bc3 100644
--- a/Holmakefile
+++ b/hol4/Holmakefile
diff --git a/ROOT b/isabelle/ROOT
index ea74bca..ea74bca 100644
--- a/ROOT
+++ b/isabelle/ROOT
diff --git a/riscv_extras.lem b/lem/riscv_extras.lem
index c1a52c9..c1a52c9 100644
--- a/riscv_extras.lem
+++ b/lem/riscv_extras.lem
diff --git a/riscv_extras_sequential.lem b/lem/riscv_extras_sequential.lem
index c1a52c9..c1a52c9 100644
--- a/riscv_extras_sequential.lem
+++ b/lem/riscv_extras_sequential.lem
diff --git a/main.sail b/model/main.sail
index dbf41f4..dbf41f4 100644
--- a/main.sail
+++ b/model/main.sail
diff --git a/main_rvfi.sail b/model/main_rvfi.sail
index 0ba4acf..0ba4acf 100644
--- a/main_rvfi.sail
+++ b/model/main_rvfi.sail
diff --git a/prelude.sail b/model/prelude.sail
index c0e93e9..c0e93e9 100644
--- a/prelude.sail
+++ b/model/prelude.sail
diff --git a/riscv.sail b/model/riscv.sail
index 6f1cd2e..6f1cd2e 100644
--- a/riscv.sail
+++ b/model/riscv.sail
diff --git a/riscv_analysis.sail b/model/riscv_analysis.sail
index 34572f8..34572f8 100644
--- a/riscv_analysis.sail
+++ b/model/riscv_analysis.sail
diff --git a/riscv_duopod.sail b/model/riscv_duopod.sail
index 0a5a7f8..0a5a7f8 100644
--- a/riscv_duopod.sail
+++ b/model/riscv_duopod.sail
diff --git a/riscv_insts_begin.sail b/model/riscv_insts_begin.sail
index 56fd8b4..56fd8b4 100644
--- a/riscv_insts_begin.sail
+++ b/model/riscv_insts_begin.sail
diff --git a/riscv_insts_end.sail b/model/riscv_insts_end.sail
index 144f06e..144f06e 100644
--- a/riscv_insts_end.sail
+++ b/model/riscv_insts_end.sail
diff --git a/riscv_jalr_rmem.sail b/model/riscv_jalr_rmem.sail
index daf4bb0..daf4bb0 100644
--- a/riscv_jalr_rmem.sail
+++ b/model/riscv_jalr_rmem.sail
diff --git a/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail
index fcf9526..fcf9526 100644
--- a/riscv_jalr_seq.sail
+++ b/model/riscv_jalr_seq.sail
diff --git a/riscv_mem.sail b/model/riscv_mem.sail
index 0b3e550..0b3e550 100644
--- a/riscv_mem.sail
+++ b/model/riscv_mem.sail
diff --git a/riscv_platform.sail b/model/riscv_platform.sail
index aee72e4..aee72e4 100644
--- a/riscv_platform.sail
+++ b/model/riscv_platform.sail
diff --git a/riscv_step.sail b/model/riscv_step.sail
index 755420d..755420d 100644
--- a/riscv_step.sail
+++ b/model/riscv_step.sail
diff --git a/riscv_sys.sail b/model/riscv_sys.sail
index 450eb12..450eb12 100644
--- a/riscv_sys.sail
+++ b/model/riscv_sys.sail
diff --git a/riscv_termination.sail b/model/riscv_termination.sail
index 6da4896..6da4896 100644
--- a/riscv_termination.sail
+++ b/model/riscv_termination.sail
diff --git a/riscv_types.sail b/model/riscv_types.sail
index 4d012e0..4d012e0 100644
--- a/riscv_types.sail
+++ b/model/riscv_types.sail
diff --git a/riscv_vmem.sail b/model/riscv_vmem.sail
index b617d29..b617d29 100644
--- a/riscv_vmem.sail
+++ b/model/riscv_vmem.sail
diff --git a/rvfi_dii.sail b/model/rvfi_dii.sail
index 9680ab4..9680ab4 100644
--- a/rvfi_dii.sail
+++ b/model/rvfi_dii.sail
diff --git a/_tags b/ocaml/_tags
index eab7e89..eab7e89 100644
--- a/_tags
+++ b/ocaml/_tags
diff --git a/_tags.bisect b/ocaml/_tags.bisect
index d3b996f..d3b996f 100644
--- a/_tags.bisect
+++ b/ocaml/_tags.bisect
diff --git a/platform.ml b/ocaml/platform.ml
index 6ee2d2b..6ee2d2b 100644
--- a/platform.ml
+++ b/ocaml/platform.ml
diff --git a/platform_impl.ml b/ocaml/platform_impl.ml
index 3eb8217..3eb8217 100644
--- a/platform_impl.ml
+++ b/ocaml/platform_impl.ml
diff --git a/platform_main.ml b/ocaml/platform_main.ml
index 1c9ba20..1c9ba20 100644
--- a/platform_main.ml
+++ b/ocaml/platform_main.ml
diff --git a/tracecmp.ml b/ocaml/tracecmp.ml
index 64a918d..64a918d 100644
--- a/tracecmp.ml
+++ b/ocaml/tracecmp.ml
diff --git a/test/run_tests.sh b/test/run_tests.sh
index 04d72a2..491c64c 100755
--- a/test/run_tests.sh
+++ b/test/run_tests.sh
@@ -51,7 +51,7 @@ cd $RISCVDIR
 
 printf "Building RISCV specification...\n"
 
-if make platform ;
+if make ocaml/platform ;
 then
     green "Building RISCV specification" "ok"
 else
@@ -59,7 +59,7 @@ else
 fi
 
 for test in $DIR/tests/*.elf; do
-    if $RISCVDIR/platform "$test" >"${test/.elf/.out}" 2>&1 && grep -q SUCCESS "${test/.elf/.out}"
+    if $RISCVDIR/ocaml/platform "$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 riscv_sim;
+if make c/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/riscv_sim -p $test > ${test%.elf}.cout 2>&1 && grep -q SUCCESS ${test%.elf}.cout
+    if timeout 5 $RISCVDIR/c/riscv_sim -p $test > ${test%.elf}.cout 2>&1 && grep -q SUCCESS ${test%.elf}.cout
     then
 	green "$(basename $test)" "ok"
     else