change in file structure

rems-project · Sep 30, 2020 · 9beec1f · 9beec1f
1 parent 8e48e2b
commit 9beec1f
Show file tree

Hide file tree

Showing 37 changed files with 26 additions and 63 deletions.
diff --git a/Makefile b/Makefile
@@ -433,42 +433,42 @@ LEMFLAGS += -wl_comp_message ign
 LEMFLAGS += -wl_rename ign
 
 ifeq ($(filter PPCGEN,$(ISA_LIST)),)
-  POWER_FILES += src_concurrency_model/isa_stubs/power/power_embed_types.lem
-  POWER_FILES += src_concurrency_model/isa_stubs/power/power_embed.lem
-  POWER_FILES += src_concurrency_model/isa_stubs/power/powerIsa.lem
+  POWER_FILES += src_isa_stubs/power/power_embed_types.lem
+  POWER_FILES += src_isa_stubs/power/power_embed.lem
+  POWER_FILES += src_isa_stubs/power/powerIsa.lem
 else
   POWER_FILES += $(saildir)/arch/power/power_extras_embed.lem
   POWER_FILES += $(saildir)/arch/power/power_embed_types.lem
   POWER_FILES += $(saildir)/arch/power/power_embed.lem
-  POWER_FILES += src_concurrency_model/powerIsa.lem
+  POWER_FILES += src_isa_defs/powerIsa.lem
 endif
 
 ifeq ($(filter AArch64,$(ISA_LIST)),)
-  AARCH64_FILES += src_concurrency_model/isa_stubs/aarch64/armV8_embed_types.lem
-  AARCH64_FILES += src_concurrency_model/isa_stubs/aarch64/armV8_embed.lem
-  AARCH64_FILES += src_concurrency_model/isa_stubs/aarch64/aarch64Isa.lem
+  AARCH64_FILES += src_isa_stubs/aarch64/armV8_embed_types.lem
+  AARCH64_FILES += src_isa_stubs/aarch64/armV8_embed.lem
+  AARCH64_FILES += src_isa_stubs/aarch64/aarch64Isa.lem
 else
   AARCH64_FILES += $(saildir)/arch/arm/armV8_extras_embed.lem
   AARCH64_FILES += $(saildir)/arch/arm/armV8_embed_types.lem
   AARCH64_FILES += $(saildir)/arch/arm/armV8_embed.lem
-  AARCH64_FILES += src_concurrency_model/aarch64Isa.lem
+  AARCH64_FILES += src_isa_defs/aarch64Isa.lem
 endif
 
 ifeq ($(filter MIPS,$(ISA_LIST)),)
-  MIPS_FILES += src_concurrency_model/isa_stubs/mips/mips_embed_types.lem
-  MIPS_FILES += src_concurrency_model/isa_stubs/mips/mips_embed.lem
-  MIPS_FILES += src_concurrency_model/isa_stubs/mips/mipsIsa.lem
+  MIPS_FILES += src_isa_stubs/mips/mips_embed_types.lem
+  MIPS_FILES += src_isa_stubs/mips/mips_embed.lem
+  MIPS_FILES += src_isa_stubs/mips/mipsIsa.lem
 else
   MIPS_FILES += $(saildir)/arch/mips/mips_extras_embed.lem
   MIPS_FILES += $(saildir)/arch/mips/mips_embed_types.lem
   MIPS_FILES += $(saildir)/arch/mips/mips_embed.lem
-  MIPS_FILES += src_concurrency_model/mipsIsa.lem
+  MIPS_FILES += src_isa_defs/mipsIsa.lem
 endif
 
 ifeq ($(filter RISCV,$(ISA_LIST)),)
-  RISCV_FILES += src_concurrency_model/isa_stubs/riscv/riscv_types.lem
-  RISCV_FILES += src_concurrency_model/isa_stubs/riscv/riscv.lem
-  RISCV_FILES += src_concurrency_model/isa_stubs/riscv/riscvIsa.lem
+  RISCV_FILES += src_isa_stubs/riscv/riscv_types.lem
+  RISCV_FILES += src_isa_stubs/riscv/riscv.lem
+  RISCV_FILES += src_isa_stubs/riscv/riscvIsa.lem
 else
   RISCV_FILES += $(riscvdir)/handwritten_support/0.11/riscv_extras.lem
   RISCV_FILES += $(riscvdir)/handwritten_support/0.11/riscv_extras_fdext.lem
@@ -478,18 +478,18 @@ else
   # FIXME: using '-wl_pat_red ign' is very bad but because riscv.lem is
   # generated by shallow embedding there is not much we can do
   LEMFLAGS += -wl_pat_red ign
-  RISCV_FILES += src_concurrency_model/riscvIsa.lem
+  RISCV_FILES += src_isa_defs/riscvIsa.lem
 endif
 
 ifeq ($(filter X86,$(ISA_LIST)),)
-  X86_FILES += src_concurrency_model/isa_stubs/x86/x86_embed_types.lem
-  X86_FILES += src_concurrency_model/isa_stubs/x86/x86_embed.lem
-  X86_FILES += src_concurrency_model/isa_stubs/x86/x86Isa.lem
+  X86_FILES += src_isa_stubs/x86/x86_embed_types.lem
+  X86_FILES += src_isa_stubs/x86/x86_embed.lem
+  X86_FILES += src_isa_stubs/x86/x86Isa.lem
 else
   X86_FILES += $(saildir)/arch/x86/x86_extras_embed.lem
   X86_FILES += $(saildir)/arch/x86/x86_embed_types.lem
   X86_FILES += $(saildir)/arch/x86/x86_embed.lem
-  X86_FILES += src_concurrency_model/x86Isa.lem
+  X86_FILES += src_isa_defs/x86Isa.lem
 endif
 
 MACHINEFILES=\
@@ -541,6 +541,7 @@ SAIL1_LEM_INPUT_FILES=\
   -i $(saildir)/src/gen_lib/sail_values.lem\
   -i $(saildir)/src/gen_lib/prompt.lem\
   -i $(saildir)/src/lem_interp/sail_impl_base.lem\
+  -i src_concurrency_model/regUtils.lem\
   -i src_concurrency_model/isa.lem
 
 SAIL2_LEM_INPUT_FILES=\
@@ -558,7 +559,7 @@ build_concurrency_model/make_sentinel: $(FORCECONCSENTINEL) $(MACHINEFILES)
 	rm -rf $(dir $@)
 	mkdir -p $(dir $@)
 	$(LEM) $(LEMFLAGS) -outdir $(dir $@) -ocaml $(MACHINEFILES)
-	$(LEM) $(LEMFLAGS) $(SAIL2_LEM_INPUT_FILES) -outdir $(dir $@) -ocaml $(RISCV_FILES) src_concurrency_model/sail_1_2_convert.lem
+	$(LEM) $(LEMFLAGS) $(SAIL2_LEM_INPUT_FILES) -outdir $(dir $@) -ocaml $(RISCV_FILES) src_isa_defs/sail_1_2_convert.lem
 	$(LEM) $(LEMFLAGS) $(SAIL1_LEM_INPUT_FILES) -outdir $(dir $@) -ocaml $(POWER_FILES)
 	$(LEM) $(LEMFLAGS) $(SAIL1_LEM_INPUT_FILES) -outdir $(dir $@) -ocaml $(AARCH64_FILES)
 	$(LEM) $(LEMFLAGS) $(SAIL1_LEM_INPUT_FILES) -outdir $(dir $@) -ocaml $(MIPS_FILES)
@@ -629,45 +630,6 @@ headers_makefiles
 # headers_scripts \
 
 
-######################################################################
-
-sloc_concurrency_model: TEMPDIR=temp_sloc_concurrency_model
-sloc_concurrency_model:
-	$(if $(wildcard $(CONCSENTINEL)),,$(error "do 'make rmem' first"))
-	@rm -rf $(TEMPDIR)
-	@mkdir -p $(TEMPDIR)
-	@cp $(MACHINEFILES) $(TEMPDIR)
-	@for f in $(TEMPDIR)/*.lem; do mv "$$f" "$${f%.lem}.ml"; done
-	@sloccount --details $(TEMPDIR) | grep -F '.ml'
-	@sloccount $(TEMPDIR) | grep -F 'ml:'
-	@echo "*"
-	@echo "* NOTE: the .ml files above are actually .lem files that were renamed to fool sloccount"
-	@echo "*"
-	@rm -rf $(TEMPDIR)
-.PHONY: sloc_concurrency_model
-
-sloc_isa_models: ISAs := $(foreach d,$(wildcard build_isa_models/*),$(if $(wildcard $(d)/*.sail),$(notdir $(d))))
-sloc_isa_models:
-	@$(if $(ISAs),\
-	  $(MAKE) --no-print-directory $(addprefix sloc_isa_model_,$(ISAs)),\
-	  $(error do 'make rmem' first))
-.PHONY: sloc_isa_models
-
-sloc_isa_model_%: TEMPDIR=temp_sloc_isa_model
-sloc_isa_model_%: FORCE
-	$(if $(wildcard build_isa_models/$*/*.sail),,$(error "do 'make rmem' first"))
-	@echo
-	@echo '**** ISA model $*: ****'
-	@rm -rf $(TEMPDIR)
-	@mkdir -p $(TEMPDIR)
-	@cp build_isa_models/$*/*.sail $(TEMPDIR)
-	@for f in $(TEMPDIR)/*.sail; do mv "$$f" "$${f%.sail}.ml"; done
-	@sloccount --details $(TEMPDIR) | grep ml
-	@sloccount $(TEMPDIR) | grep -F 'ml:'
-	@echo "*"
-	@echo "* NOTE: the .ml files above are actually .sail files that were renamed to fool sloccount"
-	@echo "*"
-	@rm -rf $(TEMPDIR)
 
 ######################################################################
 

diff --git a/_tags b/_tags
@@ -29,7 +29,6 @@
 "src_top/herd_based"              : include
 "src_top/herd_based/lib"          : include
 "src_top/herd_based/litmus"       : include
-<build_isa_models/*>              : include
 "build_concurrency_model"         : include
 "src_sail_legacy/src/lem_interp"  : include
 
@@ -45,8 +44,6 @@
 <src_top/*.{ml,mli}> or <src_top/**/*.{ml,mli}> : package(lem), package(linksem), package(base64)
 <src_top/text/*.{ml,mli}>                    : package(lambda-term)
 <build_concurrency_model/*.{ml,mli}>         : package(lem)
-<build_isa_models/**/*.{ml,mli}>             : package(lem)
-<src_marshal_defs/*.{ml,mli}>                : package(lem), package(base64)
 <src_sail_legacy/src/lem_interp/*.{ml,mli}>  : package(lem)
 
 <src_marshal_defs/marshal_defs.{d.byte,byte,native,p.native}> : package(lem), package(base64)

diff --git a/src_concurrency_model/aarch64Isa.lem → src_isa_defs/aarch64Isa.lem b/src_concurrency_model/aarch64Isa.lem → src_isa_defs/aarch64Isa.lem
diff --git a/src_concurrency_model/mipsIsa.lem → src_isa_defs/mipsIsa.lem b/src_concurrency_model/mipsIsa.lem → src_isa_defs/mipsIsa.lem
diff --git a/src_concurrency_model/powerIsa.lem → src_isa_defs/powerIsa.lem b/src_concurrency_model/powerIsa.lem → src_isa_defs/powerIsa.lem
diff --git a/src_concurrency_model/riscvIsa.lem → src_isa_defs/riscvIsa.lem b/src_concurrency_model/riscvIsa.lem → src_isa_defs/riscvIsa.lem
diff --git a/src_concurrency_model/sail_1_2_convert.lem → src_isa_defs/sail_1_2_convert.lem b/src_concurrency_model/sail_1_2_convert.lem → src_isa_defs/sail_1_2_convert.lem
diff --git a/src_concurrency_model/x86Isa.lem → src_isa_defs/x86Isa.lem b/src_concurrency_model/x86Isa.lem → src_isa_defs/x86Isa.lem
diff --git a/...cy_model/isa_stubs/aarch64/aarch64Isa.lem → src_isa_stubs/aarch64/aarch64Isa.lem b/...cy_model/isa_stubs/aarch64/aarch64Isa.lem → src_isa_stubs/aarch64/aarch64Isa.lem
diff --git a/...y_model/isa_stubs/aarch64/armV8_embed.lem → src_isa_stubs/aarch64/armV8_embed.lem b/...y_model/isa_stubs/aarch64/armV8_embed.lem → src_isa_stubs/aarch64/armV8_embed.lem
diff --git a/...l/isa_stubs/aarch64/armV8_embed_types.lem → src_isa_stubs/aarch64/armV8_embed_types.lem b/...l/isa_stubs/aarch64/armV8_embed_types.lem → src_isa_stubs/aarch64/armV8_embed_types.lem
diff --git a/..._model/isa_stubs/aarch64/armV8_extras.lem → src_isa_stubs/aarch64/armV8_extras.lem b/..._model/isa_stubs/aarch64/armV8_extras.lem → src_isa_stubs/aarch64/armV8_extras.lem
diff --git a/.../isa_stubs/aarch64/armV8_toFromInterp.lem → src_isa_stubs/aarch64/armV8_toFromInterp.lem b/.../isa_stubs/aarch64/armV8_toFromInterp.lem → src_isa_stubs/aarch64/armV8_toFromInterp.lem
diff --git a/...currency_model/isa_stubs/mips/mipsIsa.lem → src_isa_stubs/mips/mipsIsa.lem b/...currency_model/isa_stubs/mips/mipsIsa.lem → src_isa_stubs/mips/mipsIsa.lem
diff --git a/...rency_model/isa_stubs/mips/mips_embed.lem → src_isa_stubs/mips/mips_embed.lem b/...rency_model/isa_stubs/mips/mips_embed.lem → src_isa_stubs/mips/mips_embed.lem
diff --git a/...model/isa_stubs/mips/mips_embed_types.lem → src_isa_stubs/mips/mips_embed_types.lem b/...model/isa_stubs/mips/mips_embed_types.lem → src_isa_stubs/mips/mips_embed_types.lem
diff --git a/...ency_model/isa_stubs/mips/mips_extras.lem → src_isa_stubs/mips/mips_extras.lem b/...ency_model/isa_stubs/mips/mips_extras.lem → src_isa_stubs/mips/mips_extras.lem
diff --git a/...odel/isa_stubs/mips/mips_toFromInterp.lem → src_isa_stubs/mips/mips_toFromInterp.lem b/...odel/isa_stubs/mips/mips_toFromInterp.lem → src_isa_stubs/mips/mips_toFromInterp.lem
diff --git a/...rrency_model/isa_stubs/power/powerIsa.lem → src_isa_stubs/power/powerIsa.lem b/...rrency_model/isa_stubs/power/powerIsa.lem → src_isa_stubs/power/powerIsa.lem
diff --git a/...ncy_model/isa_stubs/power/power_embed.lem → src_isa_stubs/power/power_embed.lem b/...ncy_model/isa_stubs/power/power_embed.lem → src_isa_stubs/power/power_embed.lem
diff --git a/...del/isa_stubs/power/power_embed_types.lem → src_isa_stubs/power/power_embed_types.lem b/...del/isa_stubs/power/power_embed_types.lem → src_isa_stubs/power/power_embed_types.lem
diff --git a/...cy_model/isa_stubs/power/power_extras.lem → src_isa_stubs/power/power_extras.lem b/...cy_model/isa_stubs/power/power_extras.lem → src_isa_stubs/power/power_extras.lem
diff --git a/...el/isa_stubs/power/power_toFromInterp.lem → src_isa_stubs/power/power_toFromInterp.lem b/...el/isa_stubs/power/power_toFromInterp.lem → src_isa_stubs/power/power_toFromInterp.lem
diff --git a/...currency_model/isa_stubs/power/prompt.lem → src_isa_stubs/power/prompt.lem b/...currency_model/isa_stubs/power/prompt.lem → src_isa_stubs/power/prompt.lem
diff --git a/...ncy_model/isa_stubs/power/sail_values.lem → src_isa_stubs/power/sail_values.lem b/...ncy_model/isa_stubs/power/sail_values.lem → src_isa_stubs/power/sail_values.lem
diff --git a/...ncurrency_model/isa_stubs/riscv/riscv.lem → src_isa_stubs/riscv/riscv.lem b/...ncurrency_model/isa_stubs/riscv/riscv.lem → src_isa_stubs/riscv/riscv.lem
diff --git a/...rrency_model/isa_stubs/riscv/riscvIsa.lem → src_isa_stubs/riscv/riscvIsa.lem b/...rrency_model/isa_stubs/riscv/riscvIsa.lem → src_isa_stubs/riscv/riscvIsa.lem
diff --git a/...el/isa_stubs/riscv/riscv_toFromInterp.lem → src_isa_stubs/riscv/riscv_toFromInterp.lem b/...el/isa_stubs/riscv/riscv_toFromInterp.lem → src_isa_stubs/riscv/riscv_toFromInterp.lem
diff --git a/...l/isa_stubs/riscv/riscv_toFromInterp2.lem → src_isa_stubs/riscv/riscv_toFromInterp2.lem b/...l/isa_stubs/riscv/riscv_toFromInterp2.lem → src_isa_stubs/riscv/riscv_toFromInterp2.lem
diff --git a/...ncy_model/isa_stubs/riscv/riscv_types.lem → src_isa_stubs/riscv/riscv_types.lem b/...ncy_model/isa_stubs/riscv/riscv_types.lem → src_isa_stubs/riscv/riscv_types.lem
diff --git a/...oncurrency_model/isa_stubs/x86/x86Isa.lem → src_isa_stubs/x86/x86Isa.lem b/...oncurrency_model/isa_stubs/x86/x86Isa.lem → src_isa_stubs/x86/x86Isa.lem
diff --git a/...urrency_model/isa_stubs/x86/x86_embed.lem → src_isa_stubs/x86/x86_embed.lem b/...urrency_model/isa_stubs/x86/x86_embed.lem → src_isa_stubs/x86/x86_embed.lem
diff --git a/...y_model/isa_stubs/x86/x86_embed_types.lem → src_isa_stubs/x86/x86_embed_types.lem b/...y_model/isa_stubs/x86/x86_embed_types.lem → src_isa_stubs/x86/x86_embed_types.lem
diff --git a/...rrency_model/isa_stubs/x86/x86_extras.lem → src_isa_stubs/x86/x86_extras.lem b/...rrency_model/isa_stubs/x86/x86_extras.lem → src_isa_stubs/x86/x86_extras.lem
diff --git a/..._model/isa_stubs/x86/x86_toFromInterp.lem → src_isa_stubs/x86/x86_toFromInterp.lem b/..._model/isa_stubs/x86/x86_toFromInterp.lem → src_isa_stubs/x86/x86_toFromInterp.lem
diff --git a/src_sail_legacy/src/lem_interp/printing_functions.ml b/src_sail_legacy/src/lem_interp/printing_functions.ml
@@ -1,3 +1,5 @@
+(* originally from the sail(1) development, cut down for what we need *)
+
 (**************************************************************************)
 (*     Sail                                                               *)
 (*                                                                        *)

diff --git a/src_sail_legacy/src/lem_interp/printing_functions.mli b/src_sail_legacy/src/lem_interp/printing_functions.mli
@@ -1,3 +1,5 @@
+(* originally from the sail(1) development, cut down for what we need *)
+
 (* CP: commenting out things to make this not refer to the interpreter any
    longer *)