diff --git a/Makefile b/Makefile index c9765ba..fef2c29 100644 --- 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 index 9d30f78..a8e47e8 100644 --- 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 - : include "build_concurrency_model" : include "src_sail_legacy/src/lem_interp" : include @@ -45,8 +44,6 @@ or : package(lem), package(linksem), package(base64) : package(lambda-term) : package(lem) - : package(lem) - : package(lem), package(base64) : package(lem) : package(lem), package(base64) diff --git a/src_concurrency_model/aarch64Isa.lem b/src_isa_defs/aarch64Isa.lem similarity index 100% rename from src_concurrency_model/aarch64Isa.lem rename to src_isa_defs/aarch64Isa.lem diff --git a/src_concurrency_model/mipsIsa.lem b/src_isa_defs/mipsIsa.lem similarity index 100% rename from src_concurrency_model/mipsIsa.lem rename to src_isa_defs/mipsIsa.lem diff --git a/src_concurrency_model/powerIsa.lem b/src_isa_defs/powerIsa.lem similarity index 100% rename from src_concurrency_model/powerIsa.lem rename to src_isa_defs/powerIsa.lem diff --git a/src_concurrency_model/riscvIsa.lem b/src_isa_defs/riscvIsa.lem similarity index 100% rename from src_concurrency_model/riscvIsa.lem rename to src_isa_defs/riscvIsa.lem diff --git a/src_concurrency_model/sail_1_2_convert.lem b/src_isa_defs/sail_1_2_convert.lem similarity index 100% rename from src_concurrency_model/sail_1_2_convert.lem rename to src_isa_defs/sail_1_2_convert.lem diff --git a/src_concurrency_model/x86Isa.lem b/src_isa_defs/x86Isa.lem similarity index 100% rename from src_concurrency_model/x86Isa.lem rename to src_isa_defs/x86Isa.lem diff --git a/src_concurrency_model/isa_stubs/aarch64/aarch64Isa.lem b/src_isa_stubs/aarch64/aarch64Isa.lem similarity index 100% rename from src_concurrency_model/isa_stubs/aarch64/aarch64Isa.lem rename to src_isa_stubs/aarch64/aarch64Isa.lem diff --git a/src_concurrency_model/isa_stubs/aarch64/armV8_embed.lem b/src_isa_stubs/aarch64/armV8_embed.lem similarity index 100% rename from src_concurrency_model/isa_stubs/aarch64/armV8_embed.lem rename to src_isa_stubs/aarch64/armV8_embed.lem diff --git a/src_concurrency_model/isa_stubs/aarch64/armV8_embed_types.lem b/src_isa_stubs/aarch64/armV8_embed_types.lem similarity index 100% rename from src_concurrency_model/isa_stubs/aarch64/armV8_embed_types.lem rename to src_isa_stubs/aarch64/armV8_embed_types.lem diff --git a/src_concurrency_model/isa_stubs/aarch64/armV8_extras.lem b/src_isa_stubs/aarch64/armV8_extras.lem similarity index 100% rename from src_concurrency_model/isa_stubs/aarch64/armV8_extras.lem rename to src_isa_stubs/aarch64/armV8_extras.lem diff --git a/src_concurrency_model/isa_stubs/aarch64/armV8_toFromInterp.lem b/src_isa_stubs/aarch64/armV8_toFromInterp.lem similarity index 100% rename from src_concurrency_model/isa_stubs/aarch64/armV8_toFromInterp.lem rename to src_isa_stubs/aarch64/armV8_toFromInterp.lem diff --git a/src_concurrency_model/isa_stubs/mips/mipsIsa.lem b/src_isa_stubs/mips/mipsIsa.lem similarity index 100% rename from src_concurrency_model/isa_stubs/mips/mipsIsa.lem rename to src_isa_stubs/mips/mipsIsa.lem diff --git a/src_concurrency_model/isa_stubs/mips/mips_embed.lem b/src_isa_stubs/mips/mips_embed.lem similarity index 100% rename from src_concurrency_model/isa_stubs/mips/mips_embed.lem rename to src_isa_stubs/mips/mips_embed.lem diff --git a/src_concurrency_model/isa_stubs/mips/mips_embed_types.lem b/src_isa_stubs/mips/mips_embed_types.lem similarity index 100% rename from src_concurrency_model/isa_stubs/mips/mips_embed_types.lem rename to src_isa_stubs/mips/mips_embed_types.lem diff --git a/src_concurrency_model/isa_stubs/mips/mips_extras.lem b/src_isa_stubs/mips/mips_extras.lem similarity index 100% rename from src_concurrency_model/isa_stubs/mips/mips_extras.lem rename to src_isa_stubs/mips/mips_extras.lem diff --git a/src_concurrency_model/isa_stubs/mips/mips_toFromInterp.lem b/src_isa_stubs/mips/mips_toFromInterp.lem similarity index 100% rename from src_concurrency_model/isa_stubs/mips/mips_toFromInterp.lem rename to src_isa_stubs/mips/mips_toFromInterp.lem diff --git a/src_concurrency_model/isa_stubs/power/powerIsa.lem b/src_isa_stubs/power/powerIsa.lem similarity index 100% rename from src_concurrency_model/isa_stubs/power/powerIsa.lem rename to src_isa_stubs/power/powerIsa.lem diff --git a/src_concurrency_model/isa_stubs/power/power_embed.lem b/src_isa_stubs/power/power_embed.lem similarity index 100% rename from src_concurrency_model/isa_stubs/power/power_embed.lem rename to src_isa_stubs/power/power_embed.lem diff --git a/src_concurrency_model/isa_stubs/power/power_embed_types.lem b/src_isa_stubs/power/power_embed_types.lem similarity index 100% rename from src_concurrency_model/isa_stubs/power/power_embed_types.lem rename to src_isa_stubs/power/power_embed_types.lem diff --git a/src_concurrency_model/isa_stubs/power/power_extras.lem b/src_isa_stubs/power/power_extras.lem similarity index 100% rename from src_concurrency_model/isa_stubs/power/power_extras.lem rename to src_isa_stubs/power/power_extras.lem diff --git a/src_concurrency_model/isa_stubs/power/power_toFromInterp.lem b/src_isa_stubs/power/power_toFromInterp.lem similarity index 100% rename from src_concurrency_model/isa_stubs/power/power_toFromInterp.lem rename to src_isa_stubs/power/power_toFromInterp.lem diff --git a/src_concurrency_model/isa_stubs/power/prompt.lem b/src_isa_stubs/power/prompt.lem similarity index 100% rename from src_concurrency_model/isa_stubs/power/prompt.lem rename to src_isa_stubs/power/prompt.lem diff --git a/src_concurrency_model/isa_stubs/power/sail_values.lem b/src_isa_stubs/power/sail_values.lem similarity index 100% rename from src_concurrency_model/isa_stubs/power/sail_values.lem rename to src_isa_stubs/power/sail_values.lem diff --git a/src_concurrency_model/isa_stubs/riscv/riscv.lem b/src_isa_stubs/riscv/riscv.lem similarity index 100% rename from src_concurrency_model/isa_stubs/riscv/riscv.lem rename to src_isa_stubs/riscv/riscv.lem diff --git a/src_concurrency_model/isa_stubs/riscv/riscvIsa.lem b/src_isa_stubs/riscv/riscvIsa.lem similarity index 100% rename from src_concurrency_model/isa_stubs/riscv/riscvIsa.lem rename to src_isa_stubs/riscv/riscvIsa.lem diff --git a/src_concurrency_model/isa_stubs/riscv/riscv_toFromInterp.lem b/src_isa_stubs/riscv/riscv_toFromInterp.lem similarity index 100% rename from src_concurrency_model/isa_stubs/riscv/riscv_toFromInterp.lem rename to src_isa_stubs/riscv/riscv_toFromInterp.lem diff --git a/src_concurrency_model/isa_stubs/riscv/riscv_toFromInterp2.lem b/src_isa_stubs/riscv/riscv_toFromInterp2.lem similarity index 100% rename from src_concurrency_model/isa_stubs/riscv/riscv_toFromInterp2.lem rename to src_isa_stubs/riscv/riscv_toFromInterp2.lem diff --git a/src_concurrency_model/isa_stubs/riscv/riscv_types.lem b/src_isa_stubs/riscv/riscv_types.lem similarity index 100% rename from src_concurrency_model/isa_stubs/riscv/riscv_types.lem rename to src_isa_stubs/riscv/riscv_types.lem diff --git a/src_concurrency_model/isa_stubs/x86/x86Isa.lem b/src_isa_stubs/x86/x86Isa.lem similarity index 100% rename from src_concurrency_model/isa_stubs/x86/x86Isa.lem rename to src_isa_stubs/x86/x86Isa.lem diff --git a/src_concurrency_model/isa_stubs/x86/x86_embed.lem b/src_isa_stubs/x86/x86_embed.lem similarity index 100% rename from src_concurrency_model/isa_stubs/x86/x86_embed.lem rename to src_isa_stubs/x86/x86_embed.lem diff --git a/src_concurrency_model/isa_stubs/x86/x86_embed_types.lem b/src_isa_stubs/x86/x86_embed_types.lem similarity index 100% rename from src_concurrency_model/isa_stubs/x86/x86_embed_types.lem rename to src_isa_stubs/x86/x86_embed_types.lem diff --git a/src_concurrency_model/isa_stubs/x86/x86_extras.lem b/src_isa_stubs/x86/x86_extras.lem similarity index 100% rename from src_concurrency_model/isa_stubs/x86/x86_extras.lem rename to src_isa_stubs/x86/x86_extras.lem diff --git a/src_concurrency_model/isa_stubs/x86/x86_toFromInterp.lem b/src_isa_stubs/x86/x86_toFromInterp.lem similarity index 100% rename from src_concurrency_model/isa_stubs/x86/x86_toFromInterp.lem rename to 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 index 1b9475b..9a02269 100644 --- 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 index e06e6d3..10ca31f 100644 --- 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 *)