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

Fixups to allow Coq output to build #86

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Fixups to allow Coq output to build #86

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
67ad650
Remove old Sail option --no_effects from the Makefile prover targets
bacam Aug 14, 2023
84a74d7
Update Coq build
bacam Aug 14, 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
41 changes: 32 additions & 9 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -159,6 +159,7 @@ ifneq ($(SAIL_DIR),)
# Use sail repo in SAIL_DIR
SAIL:=$(SAIL_DIR)/sail
export SAIL_DIR
EXPLICIT_COQ_SAIL=yes
else
# Use sail from opam package
SAIL_DIR=$(shell env OPAMCLI=2.0 opam config var sail:share)
Expand All @@ -174,8 +175,6 @@ endif

LEM_DIR?=$(shell env OPAMCLI=2.0 opam config var lem:share)
export LEM_DIR
#Coq BBV library hopefully checked out in directory above us
BBV_DIR?=../bbv

C_WARNINGS ?=
#-Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function
Expand Down Expand Up @@ -360,7 +359,7 @@ endif

generated_definitions/lem/$(ARCH)/riscv.lem: $(SAIL_SRCS) Makefile handwritten_support/dummy_assembly_mappings.sail
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 Cheri_extras -no_effects -mono_rewrites $(SAIL_LIB_DIR)/mono_rewrites.sail $(SAIL_SRCS) -splice handwritten_support/dummy_assembly_mappings.sail
$(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 Cheri_extras -mono_rewrites $(SAIL_LIB_DIR)/mono_rewrites.sail $(SAIL_SRCS) -splice handwritten_support/dummy_assembly_mappings.sail
echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/$(ARCH)/riscv_types.lem

generated_definitions/isabelle/$(ARCH)/Riscv.thy: generated_definitions/isabelle/$(ARCH)/ROOT generated_definitions/lem/$(ARCH)/riscv.lem $(RISCV_EXTRAS_LEM) handwritten_support/cheri_extras.lem Makefile
Expand Down Expand Up @@ -397,25 +396,49 @@ riscv_hol: generated_definitions/hol4/$(ARCH)/riscvScript.sml
riscv_hol_build: generated_definitions/hol4/$(ARCH)/riscvTheory.uo
.PHONY: riscv_hol riscv_hol_build

COQ_LIBS = -R $(BBV_DIR)/theories bbv -R $(SAIL_LIB_DIR)/coq Sail -R generated_definitions/coq/$(ARCH) '' -R $(SAIL_RISCV_DIR)/handwritten_support '' -R handwritten_support ''
ifdef BBV_DIR
EXPLICIT_COQ_BBV = yes
else
EXPLICIT_COQ_BBV = $(shell if opam config var coq-bbv:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi)
ifeq ($(EXPLICIT_COQ_BBV),yes)
#Coq BBV library hopefully checked out in directory above us
BBV_DIR = ../bbv
endif
endif

ifndef EXPLICIT_COQ_SAIL
EXPLICIT_COQ_SAIL = $(shell if opam config var coq-sail:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi)
endif

COQ_LIBS = -R generated_definitions/coq Riscv -R generated_definitions/coq/$(ARCH) $(ARCH) -R $(SAIL_RISCV_DIR)/handwritten_support Riscv_common -R handwritten_support Riscv_common
ifeq ($(EXPLICIT_COQ_BBV),yes)
COQ_LIBS += -Q $(BBV_DIR)/src/bbv bbv
endif
ifeq ($(EXPLICIT_COQ_SAIL),yes)
COQ_LIBS += -Q $(SAIL_LIB_DIR)/coq Sail
endif

riscv_coq: $(addprefix generated_definitions/coq/$(ARCH)/,riscv.v riscv_types.v)
riscv_coq_build: generated_definitions/coq/$(ARCH)/riscv.vo
.PHONY: riscv_coq riscv_coq_build

$(addprefix generated_definitions/coq/$(ARCH)/,riscv.v riscv_types.v): $(SAIL_COQ_SRCS) Makefile handwritten_support/dummy_assembly_mappings.sail
mkdir -p generated_definitions/coq/$(ARCH)
$(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv -coq_lib cheri_extras -coq_lib riscv_extras -no_effects $(SAIL_COQ_SRCS) -splice handwritten_support/dummy_assembly_mappings.sail
$(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv -coq_lib cheri_extras -coq_lib riscv_extras $(SAIL_COQ_SRCS) -splice handwritten_support/dummy_assembly_mappings.sail
$(addprefix generated_definitions/coq/$(ARCH)/,riscv_duopod.v riscv_duopod_types.v): $(PRELUDE_SRCS) $(SAIL_RISCV_MODEL_DIR)/riscv_duopod.sail
mkdir -p generated_definitions/coq/$(ARCH)
$(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv_duopod -coq_lib riscv_extras $^

%.vo: %.v
ifeq ($(wildcard $(BBV_DIR)/theories),)
ifeq ($(EXPLICIT_COQ_BBV),yes)
ifeq ($(wildcard $(BBV_DIR)/src),)
$(error BBV directory not found. Please set the BBV_DIR environment variable)
endif
endif
ifeq ($(wildcard $(SAIL_LIB_DIR)/coq),)
ifeq ($(EXPLICIT_COQ_SAIL),yes)
ifeq ($(wildcard $(SAIL_LIB_DIR)/coq),)
$(error lib directory of Sail not found. Please set the SAIL_LIB_DIR environment variable)
endif
endif
coqc $(COQ_LIBS) $<

Expand All @@ -429,7 +452,7 @@ generated_definitions/lem-for-rmem/riscv.lem: SAIL_FLAGS += -lem_lib Riscv_extra
generated_definitions/lem-for-rmem/riscv.lem: $(SAIL_RMEM_SRCS)
mkdir -p $(dir $@)
# We do not need the isabelle .thy files, but sail always generates them
$(SAIL) $(SAIL_FLAGS) -lem -lem_mwords -lem_output_dir $(dir $@) -isa_output_dir $(dir $@) -o $(notdir $(basename $@)) -no_effects $^
$(SAIL) $(SAIL_FLAGS) -lem -lem_mwords -lem_output_dir $(dir $@) -isa_output_dir $(dir $@) -o $(notdir $(basename $@)) $^

isail:
$(SAIL) $(SAIL_FLAGS) -i $(PRELUDE_SRCS)
Expand Down Expand Up @@ -462,5 +485,5 @@ clean:
-rm -rf ocaml_emulator/_sbuild ocaml_emulator/_build ocaml_emulator/cheri_riscv_ocaml_sim_RV32 ocaml_emulator/cheri_riscv_ocaml_sim_RV64 ocaml_emulator/tracecmp
-rm -f *.gcno *.gcda
-Holmake cleanAll
-rm -f $(SAIL_RISCV_DIR)/handwritten_support/riscv_extras.vo $(SAIL_RISCV_DIR)/handwritten_support/riscv_extras.glob $(SAIL_RISCV_DIR)/handwritten_support/.riscv_extras.aux
-rm -f handwritten_support/cheri_extras.vo handwritten_support/cheri_extras.glob handwritten_support/.cheri_extras.aux $(SAIL_RISCV_DIR)/handwritten_support/riscv_extras.vo $(SAIL_RISCV_DIR)/handwritten_support/riscv_extras.glob $(SAIL_RISCV_DIR)/handwritten_support/.riscv_extras.aux
ocamlbuild -clean
10 changes: 3 additions & 7 deletions handwritten_support/cheri_extras.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,15 +60,11 @@
(* SUCH DAMAGE. *)
(*=======================================================================================*)

Require Import Sail2_instr_kinds.
Require Import Sail2_values.
Require Import Sail2_operators_mwords.
Require Import Sail2_prompt_monad.
Require Import Sail2_prompt.
Require Import Sail.Base.

Definition write_ram {rv e} wk (addr : mword 64) size (v : mword (8 * size)) (tag : bool) : monad rv bool e := write_memt wk addr size v (bitU_of_bool tag).

Definition read_ram {rv e} rk (addr : mword 64) size (read_tag : bool) `{ArithFact (size >= 0)} : monad rv (mword (8 * size) * bool) e :=
Definition read_ram {rv e} rk (addr : mword 64) size (read_tag : bool) : monad rv (mword (8 * size) * bool) e :=
if read_tag then
read_memt rk addr size >>= fun '(data, tag) =>
bool_of_bitU_nondet tag >>= fun tag =>
Expand All @@ -82,5 +78,5 @@ Definition write_tag_bool {rv A E} (addr : mword A) tag : monad rv unit E :=
write_memt Write_plain addr 16 cap (bitU_of_bool tag) >>= (fun _ => returnm tt).

Definition read_tag_bool {rv E} (addr : mword 64) : monad rv bool E :=
read_memt (B := 128) Read_plain addr 16 >>= fun '(cap, tag) =>
read_memt Read_plain addr 16 >>= fun '(cap, tag) =>
bool_of_bitU_nondet tag.