summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/coq/Makefile4
-rw-r--r--lib/coq/Sail2_instr_kinds.v15
-rw-r--r--lib/coq/Sail2_operators_mwords.v9
-rw-r--r--lib/coq/Sail2_prompt.v21
-rw-r--r--lib/coq/Sail2_values.v5
-rw-r--r--lib/hol/Holmakefile8
-rw-r--r--lib/hol/Makefile4
-rw-r--r--lib/isabelle/Makefile17
-rw-r--r--lib/rts.c15
-rw-r--r--lib/rts.h3
-rw-r--r--lib/smt.sail4
11 files changed, 84 insertions, 21 deletions
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)
diff --git a/lib/coq/Sail2_instr_kinds.v b/lib/coq/Sail2_instr_kinds.v
index eadc567a..c6fb866b 100644
--- a/lib/coq/Sail2_instr_kinds.v
+++ b/lib/coq/Sail2_instr_kinds.v
@@ -157,6 +157,7 @@ Inductive barrier_kind :=
| Barrier_RISCV_rw_r
| Barrier_RISCV_r_w
| Barrier_RISCV_w_r
+ | Barrier_RISCV_tso
| Barrier_RISCV_i
(* X86 *)
| Barrier_x86_MFENCE.
@@ -182,6 +183,11 @@ instance (Show barrier_kind)
| Barrier_RISCV_r_r -> "Barrier_RISCV_r_r"
| Barrier_RISCV_rw_w -> "Barrier_RISCV_rw_w"
| Barrier_RISCV_w_w -> "Barrier_RISCV_w_w"
+ | Barrier_RISCV_w_rw -> "Barrier_RISCV_w_rw"
+ | Barrier_RISCV_rw_r -> "Barrier_RISCV_rw_r"
+ | Barrier_RISCV_r_w -> "Barrier_RISCV_r_w"
+ | Barrier_RISCV_w_r -> "Barrier_RISCV_w_r"
+ | Barrier_RISCV_tso -> "Barrier_RISCV_tso"
| Barrier_RISCV_i -> "Barrier_RISCV_i"
| Barrier_x86_MFENCE -> "Barrier_x86_MFENCE"
end
@@ -295,8 +301,13 @@ instance (EnumerationType barrier_kind)
| Barrier_RISCV_r_r -> 15
| Barrier_RISCV_rw_w -> 16
| Barrier_RISCV_w_w -> 17
- | Barrier_RISCV_i -> 18
- | Barrier_x86_MFENCE -> 19
+ | Barrier_RISCV_w_rw -> 18
+ | Barrier_RISCV_rw_r -> 19
+ | Barrier_RISCV_r_w -> 20
+ | Barrier_RISCV_w_r -> 21
+ | Barrier_RISCV_tso -> 22
+ | Barrier_RISCV_i -> 23
+ | Barrier_x86_MFENCE -> 24
end
end
*)
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index 809f9d89..7e4abe29 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -185,10 +185,19 @@ assert ((Z.to_nat m <= Z.to_nat n)%nat).
{ apply Z2Nat.inj_le; omega. }
omega.
Qed.
+Lemma truncateLSB_eq {m n} : m >= 0 -> m <= n -> (Z.to_nat n = (Z.to_nat n - Z.to_nat m) + Z.to_nat m)%nat.
+intros.
+assert ((Z.to_nat m <= Z.to_nat n)%nat).
+{ apply Z2Nat.inj_le; omega. }
+omega.
+Qed.
Definition vector_truncate {n} (v : mword n) (m : Z) `{ArithFact (m >= 0)} `{ArithFact (m <= n)} : mword m :=
cast_to_mword (Word.split1 _ _ (cast_word (get_word v) (ltac:(unwrap_ArithFacts; apply truncate_eq; auto) : Z.to_nat n = Z.to_nat m + (Z.to_nat n - Z.to_nat m))%nat)) (ltac:(unwrap_ArithFacts; apply Z2Nat.id; omega) : Z.of_nat (Z.to_nat m) = m).
+Definition vector_truncateLSB {n} (v : mword n) (m : Z) `{ArithFact (m >= 0)} `{ArithFact (m <= n)} : mword m :=
+ cast_to_mword (Word.split2 _ _ (cast_word (get_word v) (ltac:(unwrap_ArithFacts; apply truncateLSB_eq; auto) : Z.to_nat n = (Z.to_nat n - Z.to_nat m) + Z.to_nat m)%nat)) (ltac:(unwrap_ArithFacts; apply Z2Nat.id; omega) : Z.of_nat (Z.to_nat m) = m).
+
Lemma concat_eq {a b} : a >= 0 -> b >= 0 -> Z.of_nat (Z.to_nat b + Z.to_nat a)%nat = a + b.
intros.
rewrite Nat2Z.inj_add.
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 85ca95f6..bd0d7750 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -86,6 +86,27 @@ red.
omega.
Defined.
+(* A version of well-foundedness of measures with a guard to ensure that
+ definitions can be reduced without inspecting proofs, based on a coq-club
+ thread featuring Barras, Gonthier and Gregoire, see
+ https://sympa.inria.fr/sympa/arc/coq-club/2007-07/msg00014.html *)
+
+Fixpoint pos_guard_wf {A:Type} {R:A -> A -> Prop} (p:positive) : well_founded R -> well_founded R :=
+ match p with
+ | xH => fun wfR x => Acc_intro x (fun y _ => wfR y)
+ | xO p' => fun wfR x => let F := pos_guard_wf p' in Acc_intro x (fun y _ => F (F
+wfR) y)
+ | xI p' => fun wfR x => let F := pos_guard_wf p' in Acc_intro x (fun y _ => F (F
+wfR) y)
+ end.
+
+Definition Zwf_guarded (z:Z) : Acc (Zwf 0) z :=
+ match z with
+ | Zpos p => pos_guard_wf p (Zwf_well_founded _) _
+ | _ => Zwf_well_founded _ _
+ end.
+
+
(*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
let rec whileM vars cond body =
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index e3e039c2..219a6f84 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -9,6 +9,7 @@ Require Export List.
Require Export Sumbool.
Require Export DecidableClass.
Require Import Eqdep_dec.
+Require Export Zeuclid.
Import ListNotations.
Open Scope Z.
@@ -1654,8 +1655,8 @@ end
(* Arithmetic functions which return proofs that match the expected Sail
types in smt.sail. *)
-Definition div_with_eq n m : {o : Z & ArithFact (o = Z.quot n m)} := build_ex (Z.quot n m).
-Definition mod_with_eq n m : {o : Z & ArithFact (o = Z.rem n m)} := build_ex (Z.rem n m).
+Definition ediv_with_eq n m : {o : Z & ArithFact (o = ZEuclid.div n m)} := build_ex (ZEuclid.div n m).
+Definition emod_with_eq n m : {o : Z & ArithFact (o = ZEuclid.modulo n m)} := build_ex (ZEuclid.modulo n m).
Definition abs_with_eq n : {o : Z & ArithFact (o = Z.abs n)} := build_ex (Z.abs n).
(* Similarly, for ranges (currently in MIPS) *)
diff --git a/lib/hol/Holmakefile b/lib/hol/Holmakefile
index 8e8403f3..0da5813f 100644
--- a/lib/hol/Holmakefile
+++ b/lib/hol/Holmakefile
@@ -1,3 +1,5 @@
+# Ensure LEM_DIR is set before running Holmake, e.g., by using the accompanying Makefile
+
LEM_SCRIPTS = sail2_instr_kindsScript.sml sail2_valuesScript.sml sail2_operatorsScript.sml \
sail2_operators_mwordsScript.sml sail2_operators_bitlistsScript.sml \
sail2_state_monadScript.sml sail2_stateScript.sml sail2_promptScript.sml sail2_prompt_monadScript.sml \
@@ -10,9 +12,7 @@ SCRIPTS = $(LEM_SCRIPTS) \
THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS))
-LEMDIR=../../../lem/hol-lib
-
-INCLUDES = $(LEMDIR)
+INCLUDES = $(LEM_DIR)/hol-lib
all: $(THYS)
.PHONY: all
@@ -23,7 +23,7 @@ ifdef POLY
HOLHEAP = sail-heap
EXTRA_CLEANS = $(LEM_CLEANS) $(HOLHEAP) $(HOLHEAP).o
-BASE_HEAP = $(LEMDIR)/lemheap
+BASE_HEAP = $(LEM_DIR)/hol-lib/lemheap
$(HOLHEAP): $(BASE_HEAP)
$(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) -b $(BASE_HEAP)
diff --git a/lib/hol/Makefile b/lib/hol/Makefile
index 783ef23d..c863a05b 100644
--- a/lib/hol/Makefile
+++ b/lib/hol/Makefile
@@ -1,3 +1,5 @@
+LEM_DIR?=$(shell opam config var lem:share)
+
LEMSRC = \
../../src/lem_interp/sail2_instr_kinds.lem \
../../src/gen_lib/sail2_values.lem \
@@ -25,7 +27,7 @@ $(SCRIPTS): $(LEMSRC)
lem -hol -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $(LEMSRC)
$(THYS) sail-heap: $(SCRIPTS)
- Holmake
+ LEM_DIR=$(LEM_DIR) Holmake
# Holmake will also clear out the generated $(SCRIPTS) files
clean:
diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index 57459b82..039a81f1 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -7,7 +7,9 @@ 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
+LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib
+
+SAIL_RISCV ?= ../../../sail-riscv
.PHONY: all heap-img clean
@@ -16,16 +18,15 @@ 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<version>/ROOTS)'
- @echo '*** and add the isabelle binary to your PATH.'
- isabelle build -b Sail
+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
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 $(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 $<
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);
diff --git a/lib/smt.sail b/lib/smt.sail
index c57f7bd1..7006b190 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -8,7 +8,7 @@ val div = {
ocaml: "quotient",
lem: "integerDiv",
c: "tdiv_int",
- coq: "div_with_eq"
+ coq: "ediv_with_eq"
} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == div('n, 'm). atom('o)}
overload operator / = {div}
@@ -18,7 +18,7 @@ val mod = {
ocaml: "modulus",
lem: "integerMod",
c: "tmod_int",
- coq: "mod_with_eq"
+ coq: "emod_with_eq"
} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == mod('n, 'm). atom('o)}
overload operator % = {mod}
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 18:36:58 +0000