From 07cf22289b1b4bb2300d4670573a7faee7211a04 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 21 Jan 2019 18:53:20 +0000 Subject: Fix build of Isabelle documentation --- lib/isabelle/Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib') diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index 57459b82..f9c061b3 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -7,7 +7,7 @@ EXTRA_THYS = Sail2_state_monad_lemmas.thy Sail2_state_lemmas.thy \ Sail2_prompt_monad_lemmas.thy \ Sail2_operators_mwords_lemmas.thy Hoare.thy -RISCV_DIR = ../../riscv +RISCV ?= ../../../sail-riscv .PHONY: all heap-img clean @@ -24,8 +24,8 @@ heap-img: thys $(EXTRA_THYS) ROOT manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex cp output/document/session_graph.pdf manual/document/Sail_session_graph.pdf - make -C $(RISCV_DIR) Riscv_duopod.thy - isabelle build -d manual -d $(RISCV_DIR) Sail-Manual + make -C $(RISCV) riscv_duopod + isabelle build -d manual -d $(RISCV)/generated_definitions/isabelle Sail-Manual Sail2_instr_kinds.thy: ../../src/lem_interp/sail2_instr_kinds.lem lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -- cgit v1.2.3 From aeb0f82f67ff829cd7a4b57c638b44a07d39ba3b Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 21 Jan 2019 19:53:59 +0000 Subject: Don't require manual set up of Isabelle session directories Since Isabelle 2018, specifying the same directory both on the command line and persistently in the user's ROOTS file is allowed, so we don't have to choose between one or the other any more. --- lib/isabelle/Makefile | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) (limited to 'lib') diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index f9c061b3..3ce9b9d8 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -16,16 +16,12 @@ all: thys thys: $(THYS) heap-img: thys $(EXTRA_THYS) ROOT - @echo '*** To build a heap image with the Sail library, please' - @echo '*** add this directory to your ROOTS file' - @echo '*** (e.g. $$HOME/.isabelle/Isabelle/ROOTS)' - @echo '*** and add the isabelle binary to your PATH.' - isabelle build -b Sail + isabelle build -D . manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex cp output/document/session_graph.pdf manual/document/Sail_session_graph.pdf make -C $(RISCV) riscv_duopod - isabelle build -d manual -d $(RISCV)/generated_definitions/isabelle Sail-Manual + isabelle build -d . -d $(RISCV)/generated_definitions/isabelle -D manual Sail2_instr_kinds.thy: ../../src/lem_interp/sail2_instr_kinds.lem lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -- cgit v1.2.3 From 365cf2015c77551e37d31336220497f6ca84794c Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 21 Jan 2019 23:16:47 +0000 Subject: Pass Lem library path to Isabelle --- lib/isabelle/Makefile | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index 3ce9b9d8..a1500292 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -7,6 +7,11 @@ EXTRA_THYS = Sail2_state_monad_lemmas.thy Sail2_state_lemmas.thy \ Sail2_prompt_monad_lemmas.thy \ Sail2_operators_mwords_lemmas.thy Hoare.thy +LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib +ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),) +$(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable) +endif + RISCV ?= ../../../sail-riscv .PHONY: all heap-img clean @@ -16,12 +21,12 @@ all: thys thys: $(THYS) heap-img: thys $(EXTRA_THYS) ROOT - isabelle build -D . + isabelle build -d $(LEM_ISA_LIB) -D . manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex cp output/document/session_graph.pdf manual/document/Sail_session_graph.pdf make -C $(RISCV) riscv_duopod - isabelle build -d . -d $(RISCV)/generated_definitions/isabelle -D manual + isabelle build -d $(LEM_ISA_LIB) -d . -d $(RISCV)/generated_definitions/isabelle -D manual Sail2_instr_kinds.thy: ../../src/lem_interp/sail2_instr_kinds.lem lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -- cgit v1.2.3 From 8a3c75dfd07d7264a82450aaebce86b5e82c974b Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur Date: Mon, 21 Jan 2019 18:42:12 -0800 Subject: The RISCV environment variable collides with common usage by the RISC-V toolchain; use SAIL_RISCV instead to refer to sail-riscv. --- lib/isabelle/Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib') diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index a1500292..975810a1 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -12,7 +12,7 @@ ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),) $(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable) endif -RISCV ?= ../../../sail-riscv +SAIL_RISCV ?= ../../../sail-riscv .PHONY: all heap-img clean @@ -25,8 +25,8 @@ heap-img: thys $(EXTRA_THYS) ROOT manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex cp output/document/session_graph.pdf manual/document/Sail_session_graph.pdf - make -C $(RISCV) riscv_duopod - isabelle build -d $(LEM_ISA_LIB) -d . -d $(RISCV)/generated_definitions/isabelle -D manual + make -C $(SAIL_RISCV) riscv_duopod + isabelle build -d $(LEM_ISA_LIB) -d . -d $(SAIL_RISCV)/generated_definitions/isabelle -D manual Sail2_instr_kinds.thy: ../../src/lem_interp/sail2_instr_kinds.lem lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< -- cgit v1.2.3 From 63a3cdcd18972cdc2b6fa24d6a2deb5cae7549cc Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 22 Jan 2019 03:08:46 +0000 Subject: Make sure we optimize constrained union constructors --- lib/rts.c | 15 +++++++++++++++ lib/rts.h | 3 +++ 2 files changed, 18 insertions(+) (limited to 'lib') diff --git a/lib/rts.c b/lib/rts.c index bc0d4732..eacf0a70 100644 --- a/lib/rts.c +++ b/lib/rts.c @@ -238,6 +238,21 @@ bool write_ram(const mpz_t addr_size, // Either 32 or 64 return true; } +sbits fast_read_ram(const int64_t data_size, + const uint64_t addr) +{ + uint64_t r = 0; + + uint64_t byte; + for(uint64_t i = (uint64_t) data_size; i > 0; --i) { + byte = read_mem(addr + (i - 1)); + r = r << 8; + r = r + byte; + } + sbits res = {.len = data_size * 8, .bits = r }; + return res; +} + void read_ram(lbits *data, const mpz_t addr_size, const mpz_t data_size_mpz, diff --git a/lib/rts.h b/lib/rts.h index f5e5e3b1..c7c1259f 100644 --- a/lib/rts.h +++ b/lib/rts.h @@ -65,6 +65,9 @@ void read_ram(lbits *data, const lbits hex_ram, const lbits addr_bv); +sbits fast_read_ram(const int64_t data_size, + const uint64_t addr_bv); + unit write_tag_bool(const fbits, const bool); bool read_tag_bool(const fbits); -- cgit v1.2.3 From d7c68715687a4a65129cafaa10b9c0e0b89c5897 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 22 Jan 2019 13:30:24 +0000 Subject: Don't hardcode location of BBV library --- lib/coq/Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/coq/Makefile b/lib/coq/Makefile index a5f2874b..6dd962d1 100644 --- a/lib/coq/Makefile +++ b/lib/coq/Makefile @@ -1,8 +1,8 @@ -BBV_DIR=../../../bbv/theories +BBV_DIR?=../../../bbv SRC=Sail2_prompt_monad.v Sail2_prompt.v Sail2_impl_base.v Sail2_instr_kinds.v Sail2_operators_bitlists.v Sail2_operators_mwords.v Sail2_operators.v Sail2_values.v Sail2_state_monad.v Sail2_state.v Sail2_string.v Sail2_real.v -COQ_LIBS = -R . Sail -R "$(BBV_DIR)" bbv +COQ_LIBS = -R . Sail -R "$(BBV_DIR)/theories" bbv TARGETS=$(SRC:.v=.vo) -- cgit v1.2.3 From 1951607813f73688297840fc4ae4b3059b7528c5 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Wed, 23 Jan 2019 16:29:49 +0000 Subject: Don't let "make" fail unnecessarily in lib/isabelle Only check for availability of Lem library if actually trying to build an Isabelle heap image. --- lib/isabelle/Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib') diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index 975810a1..039a81f1 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -8,9 +8,6 @@ EXTRA_THYS = Sail2_state_monad_lemmas.thy Sail2_state_lemmas.thy \ Sail2_operators_mwords_lemmas.thy Hoare.thy LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib -ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),) -$(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable) -endif SAIL_RISCV ?= ../../../sail-riscv @@ -21,6 +18,9 @@ all: thys thys: $(THYS) heap-img: thys $(EXTRA_THYS) ROOT +ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),) + $(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable) +endif isabelle build -d $(LEM_ISA_LIB) -D . manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex -- cgit v1.2.3