Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix lem build in Makefile #353

Merged
merged 2 commits into from
Dec 19, 2023
Merged

Fix lem build in Makefile #353

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e4fac6c
lem: Fix use of 'class' in riscv_insts_vext_utils
Alasdair Nov 17, 2023
2f3dc1c
lem: Fix issues created by vector extension
Alasdair Nov 18, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 3 additions & 11 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -187,15 +187,7 @@ C_LIBS += $(SAIL_LIB_DIR)/coverage/libsail_coverage.a -lm -lpthread -ldl
endif

RISCV_EXTRAS_LEM_FILES = riscv_extras.lem mem_metadata.lem riscv_extras_fdext.lem
# Feature detect if we are on the latest development version of Sail
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why was the check of the Sail version removed?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's a check for a version of Sail that is many years old, and no longer works with the model.

# and use an updated lem file if so. This is just until the opam
# version catches up with changes to the barrier type.
SAIL_LATEST := $(shell $(SAIL) -have_feature FEATURE_UNION_BARRIER 1>&2 2> /dev/null; echo $$?)
ifeq ($(SAIL_LATEST),0)
RISCV_EXTRAS_LEM = $(addprefix handwritten_support/0.11/,$(RISCV_EXTRAS_LEM_FILES))
else
RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES))
endif

.PHONY:

Expand Down Expand Up @@ -325,12 +317,12 @@ endif

generated_definitions/lem/$(ARCH)/riscv.lem: $(SAIL_SRCS) Makefile
mkdir -p generated_definitions/lem/$(ARCH) generated_definitions/isabelle/$(ARCH)
$(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -o riscv -lem_mwords -lem_lib Riscv_extras -lem_lib Riscv_extras_fdext -lem_lib Mem_metadata $(SAIL_SRCS)
$(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -o riscv -lem_lib Riscv_extras -lem_lib Riscv_extras_fdext -lem_lib Mem_metadata $(SAIL_SRCS)
echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/$(ARCH)/riscv_types.lem

# sed -i isn't posix compliant, unfortunately
generated_definitions/isabelle/$(ARCH)/Riscv.thy: generated_definitions/isabelle/$(ARCH)/ROOT generated_definitions/lem/$(ARCH)/riscv.lem $(RISCV_EXTRAS_LEM) Makefile
lem -isa -outdir generated_definitions/isabelle/$(ARCH) -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \
lem -wl ign -isa -outdir generated_definitions/isabelle/$(ARCH) -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \
$(RISCV_EXTRAS_LEM) \
generated_definitions/lem/$(ARCH)/riscv_types.lem \
generated_definitions/lem/$(ARCH)/riscv.lem
Expand Down Expand Up @@ -451,7 +443,7 @@ generated_definitions/for-rmem/riscv.defs: $(SAIL_RMEM_SRCS)

FORCE:

SHARE_FILES:=$(sort $(wildcard model/*.sail)) $(sort $(wildcard c_emulator/*.c)) $(sort $(wildcard c_emulator/*.h)) $(sort $(wildcard handwritten_support/*.lem)) $(sort $(wildcard handwritten_support/hgen/*.hgen)) $(sort $(wildcard handwritten_support/0.11/*.lem)) $(RMEM_FILES)
SHARE_FILES:=$(sort $(wildcard model/*.sail)) $(sort $(wildcard c_emulator/*.c)) $(sort $(wildcard c_emulator/*.h)) $(sort $(wildcard handwritten_support/*.lem)) $(sort $(wildcard handwritten_support/hgen/*.hgen)) $(RMEM_FILES)
sail-riscv.install: FORCE
echo 'bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"]' > sail-riscv.install
echo 'share: [ $(foreach f,$(SHARE_FILES),"$f" {"$f"}) ]' >> sail-riscv.install
Expand Down
16 changes: 0 additions & 16 deletions handwritten_support/0.11/mem_metadata.lem
View file
Open in desktop

This file was deleted.

172 changes: 0 additions & 172 deletions handwritten_support/0.11/riscv_extras.lem
View file
Open in desktop

This file was deleted.

Loading
Loading