diff options
32 files changed, 679 insertions, 272 deletions
@@ -21,3 +21,12 @@ language/*.aux language/*.log language/*.dvi language/*.ps +# HOL4 +.HOLMK +.hollogs +*Theory.dat +*Theory.sig +*Theory.sml +*Theory.ui +*Theory.uo +lib/hol/sail-heap diff --git a/aarch64/mono/mono_rewrites.sail b/aarch64/mono/mono_rewrites.sail index c9164b6c..10f2d07b 100644..120000 --- a/aarch64/mono/mono_rewrites.sail +++ b/aarch64/mono/mono_rewrites.sail @@ -1,157 +1 @@ -/* Definitions for use with the -mono_rewrites option */ - -/* External definitions not in the usual asl prelude */ - -infix 6 << - -val shiftleft = "shiftl" : forall 'n ('ord : Order). - (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure - -overload operator << = {shiftleft} - -infix 6 >> - -val shiftright = "shiftr" : forall 'n ('ord : Order). - (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure - -overload operator >> = {shiftright} - -val arith_shiftright = "arith_shiftr" : forall 'n ('ord : Order). - (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure - -val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure -function extzv(v) = extz_vec(sizeof('m),v) - -val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val extsv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure -function extsv(v) = exts_vec(sizeof('m),v) - -/* This is generated internally to deal with case splits which reveal the size - of a bitvector */ -val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure - -/* Definitions for the rewrites */ - -val slice_mask : forall 'n, 'n >= 0. (int, int) -> bits('n) effect pure -function slice_mask(i,l) = - let one : bits('n) = extzv(0b1) in - ((one << l) - one) << i - -val is_zero_subrange : forall 'n, 'n >= 0. - (bits('n), int, int) -> bool effect pure - -function is_zero_subrange (xs, i, j) = { - (xs & slice_mask(j, i-j)) == extzv(0b0) -} - -val is_ones_subrange : forall 'n, 'n >= 0. - (bits('n), int, int) -> bool effect pure - -function is_ones_subrange (xs, i, j) = { - let m : bits('n) = slice_mask(j,j-i) in - (xs & m) == m -} - -val slice_slice_concat : forall 'n 'm 'r, 'n >= 0 & 'm >= 0 & 'r >= 0. - (bits('n), int, int, bits('m), int, int) -> bits('r) effect pure - -function slice_slice_concat (xs, i, l, ys, i', l') = { - let xs = (xs & slice_mask(i,l)) >> i in - let ys = (ys & slice_mask(i',l')) >> i' in - extzv(xs) << l' | extzv(ys) -} - -val slice_zeros_concat : forall 'n 'p 'q 'r, 'r = 'p + 'q & 'n >= 0 & 'p >= 0 & 'q >= 0 & 'r >= 0. - (bits('n), int, atom('p), atom('q)) -> bits('r) effect pure - -function slice_zeros_concat (xs, i, l, l') = { - let xs = (xs & slice_mask(i,l)) >> i in - extzv(xs) << l' -} - -/* Assumes initial vectors are of equal size */ - -val subrange_subrange_eq : forall 'n, 'n >= 0. - (bits('n), int, int, bits('n), int, int) -> bool effect pure - -function subrange_subrange_eq (xs, i, j, ys, i', j') = { - let xs = (xs & slice_mask(j,i-j)) >> j in - let ys = (ys & slice_mask(j',i'-j')) >> j' in - xs == ys -} - -val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's = 'o - ('p - 1) + 'q - ('r - 1) & 'n >= 0 & 'm >= 0. - (bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure - -function subrange_subrange_concat (xs, i, j, ys, i', j') = { - let xs = (xs & slice_mask(j,i-j)) >> j in - let ys = (ys & slice_mask(j',i'-j')) >> j' in - extzv(xs) << i' - (j' - 1) | extzv(ys) -} - -val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0. - (bits('n), int, int, int) -> bits('m) effect pure - -function place_subrange(xs,i,j,shift) = { - let xs = (xs & slice_mask(j,i-j)) >> j in - extzv(xs) << shift -} - -val place_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. - (bits('n), int, int, int) -> bits('m) effect pure - -function place_slice(xs,i,l,shift) = { - let xs = (xs & slice_mask(i,l)) >> i in - extzv(xs) << shift -} - -val zext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. - (bits('n), int, int) -> bits('m) effect pure - -function zext_slice(xs,i,l) = { - let xs = (xs & slice_mask(i,l)) >> i in - extzv(xs) -} - -val sext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. - (bits('n), int, int) -> bits('m) effect pure - -function sext_slice(xs,i,l) = { - let xs = arith_shiftright(((xs & slice_mask(i,l)) << ('n - i - l)), 'n - l) in - extsv(xs) -} - -/* This has different names in the aarch64 prelude (UInt) and the other - preludes (unsigned). To avoid variable name clashes, we redeclare it - here with a suitably awkward name. */ -val _builtin_unsigned = { - ocaml: "uint", - lem: "uint", - interpreter: "uint", - c: "sail_uint" -} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) - -val unsigned_slice : forall 'n, 'n >= 0. - (bits('n), int, int) -> int effect pure - -function unsigned_slice(xs,i,l) = { - let xs = (xs & slice_mask(i,l)) >> i in - _builtin_unsigned(xs) -} - -val unsigned_subrange : forall 'n, 'n >= 0. - (bits('n), int, int) -> int effect pure - -function unsigned_subrange(xs,i,j) = { - let xs = (xs & slice_mask(j,i-j)) >> i in - _builtin_unsigned(xs) -} - - -val zext_ones : forall 'n, 'n >= 0. int -> bits('n) effect pure - -function zext_ones(m) = { - let v : bits('n) = extsv(0b1) in - v >> ('n - m) -} +../../lib/mono_rewrites.sail
\ No newline at end of file diff --git a/cheri/.gitignore b/cheri/.gitignore new file mode 100644 index 00000000..f7f98624 --- /dev/null +++ b/cheri/.gitignore @@ -0,0 +1,5 @@ +cheri.lem +cheri_types.lem +cheriScript.sml +cheri_typesScript.sml +mips_extrasScript.sml
\ No newline at end of file diff --git a/cheri/Holmakefile b/cheri/Holmakefile new file mode 100644 index 00000000..d64fc3fd --- /dev/null +++ b/cheri/Holmakefile @@ -0,0 +1,11 @@ +LEMDIR=../../lem/hol-lib + +INCLUDES = $(LEMDIR) ../lib/hol + +all: cheriTheory.uo +.PHONY: all + +ifdef POLY +BASE_HEAP = ../lib/hol/sail-heap + +endif diff --git a/cheri/Makefile b/cheri/Makefile index 5861dde4..42c7ef86 100644 --- a/cheri/Makefile +++ b/cheri/Makefile @@ -17,6 +17,7 @@ CHERI128_PRE:=$(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude CHERI_INSTS:=$(CHERI_SAIL_DIR)/cheri_insts.sail CHERI_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_PRE) $(MIPS_TLB) $(CHERI_PRE) $(MIPS_INSTS) $(CHERI_INSTS) $(MIPS_EPILOGUE) +CHERI_MONO_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_PRE) $(SAIL_LIB_DIR)/mono_rewrites.sail $(MIPS_TLB) $(CHERI_PRE) $(MIPS_INSTS) $(CHERI_INSTS) $(MIPS_EPILOGUE) CHERI_NO_TLB_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_PRE) $(MIPS_TLB_STUB) $(CHERI_PRE) $(MIPS_INSTS) $(CHERI_INSTS) $(MIPS_EPILOGUE) CHERI128_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_PRE) $(MIPS_TLB) $(CHERI128_PRE) $(MIPS_INSTS) $(CHERI_INSTS) $(MIPS_EPILOGUE) CHERI128_NO_TLB_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_PRE) $(MIPS_TLB_STUB) $(CHERI128_PRE) $(MIPS_INSTS) $(CHERI_INSTS) $(MIPS_EPILOGUE) @@ -59,8 +60,8 @@ cheri_no_tlb.lem: $(CHERI_NO_TLB_SAILS) $(SAIL) -lem -o cheri_no_tlb -lem_lib Mips_extras -undefined_gen -memo_z3 $^ cheri_no_tlb_types.lem: cheri_no_tlb.lem -cheri.lem: $(CHERI_SAILS) $(CHERI_MAIN) - $(SAIL) -lem -o cheri -lem_lib Mips_extras -undefined_gen -memo_z3 $^ +cheri.lem: $(CHERI_MONO_SAILS) $(CHERI_MAIN) + $(SAIL) -lem -o cheri -auto_mono -mono_rewrites -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ cheri_types.lem: cheri.lem cheri128_no_tlb.lem: $(CHERI128_NO_TLB_SAILS) @@ -75,5 +76,13 @@ C%.thy: c%.lem c%_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ sed -i 's/datatype ast/datatype (plugins only: size) ast/' C$*_types.thy +%Script.sml: %.lem %_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem + lem -hol -outdir . -lib $(SAIL_DIR)/lib/hol -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ + +%Theory.uo: %Script.sml + Holmake $@ + clean: rm -rf cheri cheri_trace cheri128 cheri128_trace _sbuild inst_*.sail cheri.c sail_latex sail_latexcc + rm -f cheriScript.sml cheri_typesScript.sml mips_extrasScript.sml + -Holmake cleanAll diff --git a/lib/hol/.gitignore b/lib/hol/.gitignore new file mode 100644 index 00000000..fe652801 --- /dev/null +++ b/lib/hol/.gitignore @@ -0,0 +1,9 @@ +prompt_monadScript.sml +promptScript.sml +sail_instr_kindsScript.sml +sail_operators_bitlistsScript.sml +sail_operators_mwordsScript.sml +sail_operatorsScript.sml +sail_valuesScript.sml +state_monadScript.sml +stateScript.sml diff --git a/lib/hol/Holmakefile b/lib/hol/Holmakefile new file mode 100644 index 00000000..6698e210 --- /dev/null +++ b/lib/hol/Holmakefile @@ -0,0 +1,32 @@ +LEM_SCRIPTS = sail_instr_kindsScript.sml sail_valuesScript.sml sail_operatorsScript.sml \ + sail_operators_mwordsScript.sml sail_operators_bitlistsScript.sml \ + state_monadScript.sml stateScript.sml promptScript.sml prompt_monadScript.sml + +LEM_CLEANS = $(LEM_SCRIPTS) + +SCRIPTS = $(LEM_SCRIPTS) \ + sail_valuesAuxiliaryScript.sml + +THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS)) + +LEMDIR=../../../lem/hol-lib + +INCLUDES = $(LEMDIR) + +all: $(THYS) +.PHONY: all + +EXTRA_CLEANS = $(LEM_CLEANS) + +ifdef POLY +HOLHEAP = sail-heap +EXTRA_CLEANS = $(LEM_CLEANS) $(HOLHEAP) $(HOLHEAP).o + +BASE_HEAP = $(LEMDIR)/lemheap + +$(HOLHEAP): + $(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) -b $(BASE_HEAP) + +all: $(HOLHEAP) + +endif diff --git a/lib/hol/Makefile b/lib/hol/Makefile new file mode 100644 index 00000000..065f887a --- /dev/null +++ b/lib/hol/Makefile @@ -0,0 +1,31 @@ +LEMSRC = \ + ../../src/lem_interp/sail_instr_kinds.lem \ + ../../src/gen_lib/sail_values.lem \ + ../../src/gen_lib/sail_operators.lem \ + ../../src/gen_lib/sail_operators_mwords.lem \ + ../../src/gen_lib/sail_operators_bitlists.lem \ + ../../src/gen_lib/state_monad.lem \ + ../../src/gen_lib/state.lem \ + prompt_monad.lem \ + prompt.lem + +SCRIPTS = sail_instr_kindsScript.sml sail_valuesScript.sml sail_operatorsScript.sml \ + sail_operators_mwordsScript.sml sail_operators_bitlistsScript.sml \ + state_monadScript.sml stateScript.sml \ + prompt_monadScript.sml promptScript.sml + +THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS)) + +all: sail-heap $(THYS) + +$(SCRIPTS): $(LEMSRC) + lem -hol -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $(LEMSRC) + +$(THYS) sail-heap: $(SCRIPTS) + Holmake + +# Holmake will also clear out the generated $(SCRIPTS) files +clean: + Holmake cleanAll + +.PHONY: all clean diff --git a/lib/hol/prompt.lem b/lib/hol/prompt.lem new file mode 100644 index 00000000..edbd3752 --- /dev/null +++ b/lib/hol/prompt.lem @@ -0,0 +1,18 @@ +open import Prompt_monad +open import State_monad +open import State + +let inline undefined_bool = undefined_boolS +let inline bool_of_bitU_oracle = bool_of_bitU_oracleS +let inline bool_of_bitU_fail = bool_of_bitU_fail +let inline bools_of_bits_oracle = bools_of_bits_oracleS +let inline of_bits_oracle = of_bits_oracleS +let inline of_bits_fail = of_bits_failS +let inline mword_oracle = mword_oracleS +let inline reg_deref = read_regS + +let inline foreachM = foreachS +let inline whileM = whileS +let inline untilM = untilS +let inline and_boolM = and_boolS +let inline or_boolM = or_boolS diff --git a/lib/hol/prompt_monad.lem b/lib/hol/prompt_monad.lem new file mode 100644 index 00000000..8fcd645a --- /dev/null +++ b/lib/hol/prompt_monad.lem @@ -0,0 +1,49 @@ +open import Pervasives_extra +open import Sail_instr_kinds +open import Sail_values +open import State_monad + +(* Fake interface of the prompt monad by redirecting to the state monad, since + the former is not currently supported by HOL4 *) + +type monad 'rv 'a 'e = monadS 'rv 'a 'e +type monadR 'rv 'a 'e 'r = monadRS 'rv 'a 'e 'r + +(* We need to use a target_rep for these because HOL doesn't handle unused + type parameters well. *) + +type base_monad 'regval 'regstate 'a 'e = monad 'regstate 'a 'e +declare hol target_rep type base_monad 'regval 'regstate 'a 'e = `monad` 'regstate 'a 'e +type base_monadR 'regval 'regstate 'a 'r 'e = monadR 'regstate 'a 'r 'e +declare hol target_rep type base_monadR 'regval 'regstate 'a 'r 'e = `monadR` 'regstate 'a 'r 'e + +let inline return = returnS +let inline bind = bindS +let inline (>>=) = (>>$=) +let inline (>>) = (>>$) + +let inline exit = exitS + +let inline throw = throwS +let inline try_catch = try_catchS + +let inline catch_early_return = catch_early_returnS +let inline early_return = early_returnS +let inline liftR = liftRS +let inline try_catchR = try_catchRS + +let inline maybe_fail = maybe_failS + +let inline read_mem_bytes = read_mem_bytesS +let inline read_reg = read_regS +let inline reg_deref = read_regS +let inline read_mem = read_memS +let inline read_tag = read_tagS +let inline excl_result = excl_resultS +let inline write_reg = write_regS +let inline write_tag = write_tagS +let inline write_mem_ea wk addr sz = write_mem_eaS wk addr (nat_of_int sz) +let inline write_mem_val = write_mem_valS +let barrier _ = return () + +let inline assert_exp = assert_expS diff --git a/lib/hol/sail_valuesAuxiliaryScript.sml b/lib/hol/sail_valuesAuxiliaryScript.sml new file mode 100644 index 00000000..af3f56c5 --- /dev/null +++ b/lib/hol/sail_valuesAuxiliaryScript.sml @@ -0,0 +1,132 @@ +(*Generated by Lem from ../../src/gen_lib/sail_values.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_pervasives_extraTheory lem_machine_wordTheory sail_valuesTheory; +open intLib; + +val _ = numLib.prefer_num(); + + + +open lemLib; +(* val _ = lemLib.run_interactive := true; *) +val _ = new_theory "sail_valuesAuxiliary" + + +(****************************************************) +(* *) +(* Termination Proofs *) +(* *) +(****************************************************) + +(* val gst = Defn.tgoal_no_defn (shr_int_def, shr_int_ind) *) +val (shr_int_rw, shr_int_ind_rw) = + Defn.tprove_no_defn ((shr_int_def, shr_int_ind), + WF_REL_TAC`measure (Num o SND)` \\ COOPER_TAC + ) +val shr_int_rw = save_thm ("shr_int_rw", shr_int_rw); +val shr_int_ind_rw = save_thm ("shr_int_ind_rw", shr_int_ind_rw); + + +(* val gst = Defn.tgoal_no_defn (shl_int_def, shl_int_ind) *) +val (shl_int_rw, shl_int_ind_rw) = + Defn.tprove_no_defn ((shl_int_def, shl_int_ind), + WF_REL_TAC`measure (Num o SND)` \\ COOPER_TAC + ) +val shl_int_rw = save_thm ("shl_int_rw", shl_int_rw); +val shl_int_ind_rw = save_thm ("shl_int_ind_rw", shl_int_ind_rw); + + +(* val gst = Defn.tgoal_no_defn (repeat_def, repeat_ind) *) +val (repeat_rw, repeat_ind_rw) = + Defn.tprove_no_defn ((repeat_def, repeat_ind), + WF_REL_TAC`measure (Num o SND)` \\ COOPER_TAC + ) +val repeat_rw = save_thm ("repeat_rw", repeat_rw); +val repeat_ind_rw = save_thm ("repeat_ind_rw", repeat_ind_rw); + + +(* val gst = Defn.tgoal_no_defn (bools_of_nat_aux_def, bools_of_nat_aux_ind) *) +val (bools_of_nat_aux_rw, bools_of_nat_aux_ind_rw) = + Defn.tprove_no_defn ((bools_of_nat_aux_def, bools_of_nat_aux_ind), + WF_REL_TAC`measure (Num o FST)` \\ COOPER_TAC + ) +val bools_of_nat_aux_rw = save_thm ("bools_of_nat_aux_rw", bools_of_nat_aux_rw); +val bools_of_nat_aux_ind_rw = save_thm ("bools_of_nat_aux_ind_rw", bools_of_nat_aux_ind_rw); + + +(* val gst = Defn.tgoal_no_defn (pad_list_def, pad_list_ind) *) +val (pad_list_rw, pad_list_ind_rw) = + Defn.tprove_no_defn ((pad_list_def, pad_list_ind), + WF_REL_TAC`measure (Num o SND o SND)` \\ COOPER_TAC + ) +val pad_list_rw = save_thm ("pad_list_rw", pad_list_rw); +val pad_list_ind_rw = save_thm ("pad_list_ind_rw", pad_list_ind_rw); + + +(* val gst = Defn.tgoal_no_defn (reverse_endianness_list_def, reverse_endianness_list_ind) *) +val (reverse_endianness_list_rw, reverse_endianness_list_ind_rw) = + Defn.tprove_no_defn ((reverse_endianness_list_def, reverse_endianness_list_ind), + WF_REL_TAC`measure LENGTH` \\ rw[drop_list_def,nat_of_int_def] + ) +val reverse_endianness_list_rw = save_thm ("reverse_endianness_list_rw", reverse_endianness_list_rw); +val reverse_endianness_list_ind_rw = save_thm ("reverse_endianness_list_ind_rw", reverse_endianness_list_ind_rw); + + +(* val gst = Defn.tgoal_no_defn (index_list_def, index_list_ind) *) +val (index_list_rw, index_list_ind_rw) = + Defn.tprove_no_defn ((index_list_def, index_list_ind), + WF_REL_TAC`measure (λ(x,y,z). Num(1+(if z > 0 then int_max (-1) (y - x) else int_max (-1) (x - y))))` + \\ rw[integerTheory.INT_MAX] + \\ intLib.COOPER_TAC + ) +val index_list_rw = save_thm ("index_list_rw", index_list_rw); +val index_list_ind_rw = save_thm ("index_list_ind_rw", index_list_ind_rw); + + +(* +(* val gst = Defn.tgoal_no_defn (while_def, while_ind) *) +val (while_rw, while_ind_rw) = + Defn.tprove_no_defn ((while_def, while_ind), + cheat (* the termination proof *) + ) +val while_rw = save_thm ("while_rw", while_rw); +val while_ind_rw = save_thm ("while_ind_rw", while_ind_rw); +*) + + +(* +(* val gst = Defn.tgoal_no_defn (until_def, until_ind) *) +val (until_rw, until_ind_rw) = + Defn.tprove_no_defn ((until_def, until_ind), + cheat (* the termination proof *) + ) +val until_rw = save_thm ("until_rw", until_rw); +val until_ind_rw = save_thm ("until_ind_rw", until_ind_rw); +*) + + +(****************************************************) +(* *) +(* Lemmata *) +(* *) +(****************************************************) + +val just_list_spec = store_thm("just_list_spec", +``((! xs. (just_list xs = NONE) <=> MEM NONE xs) /\ + (! xs es. (just_list xs = SOME es) <=> (xs = MAP SOME es)))``, + (* Theorem: just_list_spec*) + conj_tac + \\ ho_match_mp_tac just_list_ind + \\ Cases \\ rw[] + \\ rw[Once just_list_def] + >- ( CASE_TAC \\ fs[] \\ CASE_TAC ) + >- PROVE_TAC[] + \\ Cases_on`es` \\ fs[] + \\ CASE_TAC \\ fs[] + \\ CASE_TAC \\ fs[] +); + + + +val _ = export_theory() + diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index f8786321..b10dde78 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -1,6 +1,6 @@ THYS = Sail_instr_kinds.thy Sail_values.thy Sail_operators.thy \ Sail_operators_mwords.thy Sail_operators_bitlists.thy \ - State_monad.thy State.thy Prompt_monad.thy Prompt.thy + State_monad.thy State.thy State_lifting.thy Prompt_monad.thy Prompt.thy EXTRA_THYS = State_monad_lemmas.thy State_lemmas.thy Prompt_monad_lemmas.thy \ Sail_operators_mwords_lemmas.thy Hoare.thy @@ -51,5 +51,8 @@ State_monad.thy: ../../src/gen_lib/state_monad.lem Sail_values.thy State.thy: ../../src/gen_lib/state.lem Prompt.thy State_monad.thy State_monad_lemmas.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< +State_lifting.thy: ../../src/gen_lib/state_lifting.lem Prompt.thy State.thy + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< + clean: -rm $(THYS) diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/State_lemmas.thy index 84b08e6c..253c21b9 100644 --- a/lib/isabelle/State_lemmas.thy +++ b/lib/isabelle/State_lemmas.thy @@ -1,5 +1,5 @@ theory State_lemmas - imports State + imports State State_lifting begin lemma All_liftState_dom: "liftState_dom (r, m)" @@ -44,12 +44,12 @@ lemma liftState_catch_early_return[simp]: by (auto simp: catch_early_return_def catch_early_returnS_def sum.case_distrib cong: sum.case_cong) lemma liftState_liftR[simp]: - "liftState r (liftR m) = liftSR (liftState r m)" - by (auto simp: liftR_def liftSR_def) + "liftState r (liftR m) = liftRS (liftState r m)" + by (auto simp: liftR_def liftRS_def) lemma liftState_try_catchR[simp]: - "liftState r (try_catchR m h) = try_catchSR (liftState r m) (liftState r \<circ> h)" - by (auto simp: try_catchR_def try_catchSR_def sum.case_distrib cong: sum.case_cong) + "liftState r (try_catchR m h) = try_catchRS (liftState r m) (liftState r \<circ> h)" + by (auto simp: try_catchR_def try_catchRS_def sum.case_distrib cong: sum.case_cong) lemma liftState_read_mem_BC: assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a" diff --git a/lib/isabelle/manual/Manual.thy b/lib/isabelle/manual/Manual.thy index 6cdfbfa1..51591531 100644 --- a/lib/isabelle/manual/Manual.thy +++ b/lib/isabelle/manual/Manual.thy @@ -288,7 +288,7 @@ exception handler as arguments. The exception mechanism is also used to implement early returns by throwing and catching return values: A function body with one or more early returns of type @{typ 'a} (and exception type @{typ 'e}) is lifted to a monadic expression with exception type @{typ "('a + 'e)"} using -@{term liftSR}, such that an early return of the value @{term a} throws @{term "Inl a"}, and a +@{term liftRS}, such that an early return of the value @{term a} throws @{term "Inl a"}, and a regular exception @{term e} is thrown as @{term "Inr e"}. The function body is then wrapped in @{term catch_early_returnS} to lower it back to the default monad and exception type. These liftings and lowerings are automatically inserted by Sail for functions with early returns.\<^footnote>\<open>To be diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail new file mode 100644 index 00000000..c9164b6c --- /dev/null +++ b/lib/mono_rewrites.sail @@ -0,0 +1,157 @@ +/* Definitions for use with the -mono_rewrites option */ + +/* External definitions not in the usual asl prelude */ + +infix 6 << + +val shiftleft = "shiftl" : forall 'n ('ord : Order). + (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure + +overload operator << = {shiftleft} + +infix 6 >> + +val shiftright = "shiftr" : forall 'n ('ord : Order). + (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure + +overload operator >> = {shiftright} + +val arith_shiftright = "arith_shiftr" : forall 'n ('ord : Order). + (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure + +val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure +function extzv(v) = extz_vec(sizeof('m),v) + +val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +val extsv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure +function extsv(v) = exts_vec(sizeof('m),v) + +/* This is generated internally to deal with case splits which reveal the size + of a bitvector */ +val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure + +/* Definitions for the rewrites */ + +val slice_mask : forall 'n, 'n >= 0. (int, int) -> bits('n) effect pure +function slice_mask(i,l) = + let one : bits('n) = extzv(0b1) in + ((one << l) - one) << i + +val is_zero_subrange : forall 'n, 'n >= 0. + (bits('n), int, int) -> bool effect pure + +function is_zero_subrange (xs, i, j) = { + (xs & slice_mask(j, i-j)) == extzv(0b0) +} + +val is_ones_subrange : forall 'n, 'n >= 0. + (bits('n), int, int) -> bool effect pure + +function is_ones_subrange (xs, i, j) = { + let m : bits('n) = slice_mask(j,j-i) in + (xs & m) == m +} + +val slice_slice_concat : forall 'n 'm 'r, 'n >= 0 & 'm >= 0 & 'r >= 0. + (bits('n), int, int, bits('m), int, int) -> bits('r) effect pure + +function slice_slice_concat (xs, i, l, ys, i', l') = { + let xs = (xs & slice_mask(i,l)) >> i in + let ys = (ys & slice_mask(i',l')) >> i' in + extzv(xs) << l' | extzv(ys) +} + +val slice_zeros_concat : forall 'n 'p 'q 'r, 'r = 'p + 'q & 'n >= 0 & 'p >= 0 & 'q >= 0 & 'r >= 0. + (bits('n), int, atom('p), atom('q)) -> bits('r) effect pure + +function slice_zeros_concat (xs, i, l, l') = { + let xs = (xs & slice_mask(i,l)) >> i in + extzv(xs) << l' +} + +/* Assumes initial vectors are of equal size */ + +val subrange_subrange_eq : forall 'n, 'n >= 0. + (bits('n), int, int, bits('n), int, int) -> bool effect pure + +function subrange_subrange_eq (xs, i, j, ys, i', j') = { + let xs = (xs & slice_mask(j,i-j)) >> j in + let ys = (ys & slice_mask(j',i'-j')) >> j' in + xs == ys +} + +val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's = 'o - ('p - 1) + 'q - ('r - 1) & 'n >= 0 & 'm >= 0. + (bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure + +function subrange_subrange_concat (xs, i, j, ys, i', j') = { + let xs = (xs & slice_mask(j,i-j)) >> j in + let ys = (ys & slice_mask(j',i'-j')) >> j' in + extzv(xs) << i' - (j' - 1) | extzv(ys) +} + +val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0. + (bits('n), int, int, int) -> bits('m) effect pure + +function place_subrange(xs,i,j,shift) = { + let xs = (xs & slice_mask(j,i-j)) >> j in + extzv(xs) << shift +} + +val place_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. + (bits('n), int, int, int) -> bits('m) effect pure + +function place_slice(xs,i,l,shift) = { + let xs = (xs & slice_mask(i,l)) >> i in + extzv(xs) << shift +} + +val zext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. + (bits('n), int, int) -> bits('m) effect pure + +function zext_slice(xs,i,l) = { + let xs = (xs & slice_mask(i,l)) >> i in + extzv(xs) +} + +val sext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. + (bits('n), int, int) -> bits('m) effect pure + +function sext_slice(xs,i,l) = { + let xs = arith_shiftright(((xs & slice_mask(i,l)) << ('n - i - l)), 'n - l) in + extsv(xs) +} + +/* This has different names in the aarch64 prelude (UInt) and the other + preludes (unsigned). To avoid variable name clashes, we redeclare it + here with a suitably awkward name. */ +val _builtin_unsigned = { + ocaml: "uint", + lem: "uint", + interpreter: "uint", + c: "sail_uint" +} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) + +val unsigned_slice : forall 'n, 'n >= 0. + (bits('n), int, int) -> int effect pure + +function unsigned_slice(xs,i,l) = { + let xs = (xs & slice_mask(i,l)) >> i in + _builtin_unsigned(xs) +} + +val unsigned_subrange : forall 'n, 'n >= 0. + (bits('n), int, int) -> int effect pure + +function unsigned_subrange(xs,i,j) = { + let xs = (xs & slice_mask(j,i-j)) >> i in + _builtin_unsigned(xs) +} + + +val zext_ones : forall 'n, 'n >= 0. int -> bits('n) effect pure + +function zext_ones(m) = { + let v : bits('n) = extsv(0b1) in + v >> ('n - m) +} diff --git a/mips/.gitignore b/mips/.gitignore new file mode 100644 index 00000000..2ee9fde0 --- /dev/null +++ b/mips/.gitignore @@ -0,0 +1,5 @@ +mips.lem +mips_types.lem +mipsScript.sml +mips_typesScript.sml +mips_extrasScript.sml
\ No newline at end of file diff --git a/mips/Holmakefile b/mips/Holmakefile new file mode 100644 index 00000000..a31bfd4f --- /dev/null +++ b/mips/Holmakefile @@ -0,0 +1,11 @@ +LEMDIR=../../lem/hol-lib + +INCLUDES = $(LEMDIR) ../lib/hol + +all: mipsTheory.uo +.PHONY: all + +ifdef POLY +BASE_HEAP = ../lib/hol/sail-heap + +endif diff --git a/mips/Makefile b/mips/Makefile index 6d605d60..100687e8 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -19,17 +19,24 @@ mips_no_tlb.lem: $(MIPS_PRE) $(MIPS_TLB_STUB) $(MIPS_SAILS) $(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ mips_no_tlb_types.lem: mips_no_tlb.lem -# TODO: Use monomorphisation so that we can switch to machine words -mips.lem: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) - $(SAIL) -lem -o mips -lem_lib Mips_extras -undefined_gen -memo_z3 $^ +mips.lem: $(MIPS_PRE) $(SAIL_LIB_DIR)/mono_rewrites.sail $(MIPS_TLB) $(MIPS_SAILS) + $(SAIL) -lem -o mips -auto_mono -mono_rewrites -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ mips_types.lem: mips.lem M%.thy: m%.lem m%_types.lem mips_extras.lem lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ sed -i 's/datatype ast/datatype (plugins only: size) ast/' M$*_types.thy +%Script.sml: %.lem %_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem + lem -hol -outdir . -lib $(SAIL_DIR)/lib/hol -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ + +%Theory.uo: %Script.sml + Holmake $@ + LOC_FILES:=$(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) include ../etc/loc.mk clean: - rm -rf mips Mips.thy mips.lem _sbuild + rm -rf mips Mips.thy mips.lem mips_types.lem _sbuild + rm -f mipsScript.sml mips_typesScript.sml mips_extrasScript.sml + -Holmake cleanAll diff --git a/mips/main.sail b/mips/main.sail index 8ec91ba6..54fb34ee 100644 --- a/mips/main.sail +++ b/mips/main.sail @@ -1,39 +1,35 @@ register instCount : int -val fetch_and_execute : unit -> unit effect {barr, eamem, escape, rmem, rreg, wmv, wreg, undef, wmvt, rmemt} +val fetch_and_execute : unit -> bool effect {barr, eamem, escape, rmem, rreg, wmv, wreg, undef, wmvt, rmemt} function fetch_and_execute () = { - while true do { - PC = nextPC; - inBranchDelay = branchPending; - branchPending = 0b0; - nextPC = if inBranchDelay then delayedPC else PC + 4; - cp2_next_pc(); - instCount = instCount + 1; - print_bits("PC: ", PC); - try { - let pc_pa = TranslatePC(PC); - /*print_bits("pa: ", pc_pa);*/ - let instr = MEMr_wrapper(pc_pa, 4); - /*print_bits("hex: ", instr);*/ - let instr_ast = decode(instr); - match instr_ast { - Some(HCF()) => { - print("simulation stopped due to halt instruction."); - return (); - }, - Some(ast) => execute(ast), - None() => {print("Decode failed"); exit (())} /* Never expect this -- unknown instruction should actually result in reserved instruction ISA-level exception (see mips_ri.sail). */ - } - } catch { - ISAException() => print("EXCEPTION") - /* ISA-level exception occurrred either during TranslatePC or execute -- - just continue from nextPC, which should have been set to the appropriate - exception vector (along with clearing branchPending etc.) . */ - }; + PC = nextPC; + inBranchDelay = branchPending; + branchPending = 0b0; + nextPC = if inBranchDelay then delayedPC else PC + 4; + cp2_next_pc(); + instCount = instCount + 1; + print_bits("PC: ", PC); + try { + let pc_pa = TranslatePC(PC); + /*print_bits("pa: ", pc_pa);*/ + let instr = MEMr_wrapper(pc_pa, 4); + /*print_bits("hex: ", instr);*/ + let instr_ast = decode(instr); + match instr_ast { + Some(HCF()) => { + print("simulation stopped due to halt instruction."); + false + }, + Some(ast) => { execute(ast); true }, + None() => { print("Decode failed"); exit (()) } /* Never expect this -- unknown instruction should actually result in reserved instruction ISA-level exception (see mips_ri.sail). */ + } + } catch { + ISAException() => { print("EXCEPTION"); true } + /* ISA-level exception occurrred either during TranslatePC or execute -- + just continue from nextPC, which should have been set to the appropriate + exception vector (along with clearing branchPending etc.) . */ }; - skip_rmemt(); - skip_wmvt(); } val elf_entry = { @@ -42,7 +38,13 @@ val elf_entry = { c: "elf_entry" } : unit -> int -val main : unit -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg, rmemt, wmvt} +val init_registers : bits(64) -> unit effect {wreg} + +function init_registers (initialPC) = { + init_cp0_state(); + init_cp2_state(); + nextPC = initialPC; +} function dump_mips_state () : unit -> unit = { print_bits("DEBUG MIPS PC ", PC); @@ -51,12 +53,12 @@ function dump_mips_state () : unit -> unit = { } } +val main : unit -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg, rmemt, wmvt} + function main () = { - init_cp0_state(); - init_cp2_state(); - nextPC = to_bits(64, elf_entry()); + init_registers(to_bits(64, elf_entry())); startTime = get_time_ns(); - fetch_and_execute(); + while (fetch_and_execute()) do (); endTime = get_time_ns(); elapsed = endTime - startTime; inst_1e9 = instCount * 1000000000; diff --git a/mips/prelude.sail b/mips/prelude.sail index e0bcd8cf..f805876a 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -1,8 +1,11 @@ +$include <smt.sail> + default Order dec type bits ('n : Int) = vector('n, dec, bit) union option ('a : Type) = {None : unit, Some : 'a} + val eq_bit = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", interpreter: "eq_anything", c: "eq_bit"} : (bit, bit) -> bool val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool @@ -126,6 +129,9 @@ val int_power = {ocaml: "int_power", lem: "pow"} : (int, int) -> int overload operator ^ = {xor_vec, int_power} +val add_atom = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm. + (atom('n), atom('m)) -> atom('n + 'm) + val add_range = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) @@ -137,6 +143,9 @@ val add_vec_int = "add_vec_int" : forall 'n. (bits('n), int) -> bits('n) overload operator + = {add_range, add_int, add_vec, add_vec_int} +val sub_atom = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int"} : forall 'n 'm. + (atom('n), atom('m)) -> atom('n - 'm) + val sub_range = {ocaml: "sub_int", lem: "integerMinus"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) diff --git a/riscv/.gitignore b/riscv/.gitignore new file mode 100644 index 00000000..52f3767a --- /dev/null +++ b/riscv/.gitignore @@ -0,0 +1,5 @@ +riscv.lem +riscv_types.lem +riscvScript.sml +riscv_extrasScript.sml +riscv_typesScript.sml diff --git a/riscv/Holmakefile b/riscv/Holmakefile new file mode 100644 index 00000000..8269bc36 --- /dev/null +++ b/riscv/Holmakefile @@ -0,0 +1,11 @@ +LEMDIR=../../lem/hol-lib + +INCLUDES = $(LEMDIR) ../lib/hol + +all: riscvTheory.uo +.PHONY: all + +ifdef POLY +BASE_HEAP = ../lib/hol/sail-heap + +endif diff --git a/riscv/Makefile b/riscv/Makefile index 11cc7731..0532bf09 100644 --- a/riscv/Makefile +++ b/riscv/Makefile @@ -34,6 +34,18 @@ Riscv.thy: riscv.lem riscv_extras.lem riscv.lem: $(SAIL_SRCS) Makefile $(SAIL_DIR)/sail -lem -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS) +riscv_sequential.lem: $(SAIL_SRCS) Makefile + $(SAIL_DIR)/sail -lem -lem_sequential -o riscv_sequential -lem_mwords -lem_lib Riscv_extras_sequential $(SAIL_SRCS) + +riscvScript.sml : riscv.lem riscv_extras.lem + lem -hol -outdir . -lib ../lib/hol -lib ../src/lem_interp -lib ../src/gen_lib \ + riscv_extras.lem \ + riscv_types.lem \ + riscv.lem + +riscvTheory.uo riscvTheory.ui: riscvScript.sml + Holmake riscvTheory.uo + # we exclude prelude.sail here, most code there should move to sail lib LOC_FILES:=$(SAIL_SRCS) main.sail include ../etc/loc.mk @@ -44,3 +56,5 @@ clean: -rm -f Riscv.thy Riscv_types.thy \ Riscv_extras.thy -rm -f Riscv_duopod.thy Riscv_duopod_types.thy riscv_duopod.lem riscv_duopod_types.lem + -rm -f riscvScript.sml riscv_typesScript.sml riscv_extrasScript.sml + -Holmake cleanAll diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem index 9eb59319..87c9af39 100644 --- a/src/gen_lib/prompt_monad.lem +++ b/src/gen_lib/prompt_monad.lem @@ -212,3 +212,10 @@ let barrier bk = Barrier bk (Done ()) val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e let footprint _ = Footprint (Done ()) + +(* Define a type synonym that also takes the register state as a type parameter, + in order to make switching to the state monad without changing generated + definitions easier, see also lib/hol/prompt_monad.lem. *) + +type base_monad 'regval 'regstate 'a 'e = monad 'regval 'a 'e +type base_monadR 'regval 'regstate 'a 'r 'e = monadR 'regval 'a 'r 'e diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 5c6dc593..a709a8c1 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -85,7 +85,7 @@ let rec replace bs (n : integer) b' = match bs with if n = 0 then b' :: bs else b :: replace bs (n - 1) b' end -declare {isabelle} termination_argument replace = automatic +declare {isabelle; hol} termination_argument replace = automatic let upper n = n @@ -128,7 +128,7 @@ let rec just_list l = match l with | (_, _) -> Nothing end end -declare {isabelle} termination_argument just_list = automatic +declare {isabelle; hol} termination_argument just_list = automatic lemma just_list_spec: ((forall xs. (just_list xs = Nothing) <-> List.elem Nothing xs) && @@ -267,7 +267,7 @@ let rec nat_of_bools_aux acc bs = match bs with | true :: bs -> nat_of_bools_aux ((2 * acc) + 1) bs | false :: bs -> nat_of_bools_aux (2 * acc) bs end -declare {isabelle} termination_argument nat_of_bools_aux = automatic +declare {isabelle; hol} termination_argument nat_of_bools_aux = automatic let nat_of_bools bs = nat_of_bools_aux 0 bs val unsigned_of_bools : list bool -> integer @@ -306,7 +306,7 @@ let rec add_one_bool_ignore_overflow_aux bits = match bits with | false :: bits -> true :: bits | true :: bits -> false :: add_one_bool_ignore_overflow_aux bits end -declare {isabelle} termination_argument add_one_bool_ignore_overflow_aux = automatic +declare {isabelle; hol} termination_argument add_one_bool_ignore_overflow_aux = automatic let add_one_bool_ignore_overflow bits = List.reverse (add_one_bool_ignore_overflow_aux (List.reverse bits)) @@ -369,7 +369,7 @@ let rec add_one_bit_ignore_overflow_aux bits = match bits with | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits | BU :: bits -> BU :: List.map (fun _ -> BU) bits end -declare {isabelle} termination_argument add_one_bit_ignore_overflow_aux = automatic +declare {isabelle; hol} termination_argument add_one_bit_ignore_overflow_aux = automatic let add_one_bit_ignore_overflow bits = List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits)) @@ -417,7 +417,7 @@ let rec hexstring_of_bits bs = match bs with | [] -> Just [] | _ -> Nothing end -declare {isabelle} termination_argument hexstring_of_bits = automatic +declare {isabelle; hol} termination_argument hexstring_of_bits = automatic let show_bitlist bs = match hexstring_of_bits bs with @@ -630,7 +630,7 @@ let rec byte_chunks bs = match bs with Maybe.bind (byte_chunks rest) (fun rest -> Just ([a;b;c;d;e;f;g;h] :: rest)) | _ -> Nothing end -declare {isabelle} termination_argument byte_chunks = automatic +declare {isabelle; hol} termination_argument byte_chunks = automatic val bytes_of_bits : forall 'a. Bitvector 'a => 'a -> maybe (list memory_byte) let bytes_of_bits bs = byte_chunks (bits_of bs) @@ -854,7 +854,7 @@ let rec foreach l vars body = | (x :: xs) -> foreach xs (body x vars) body end -declare {isabelle} termination_argument foreach = automatic +declare {isabelle; hol} termination_argument foreach = automatic val index_list : integer -> integer -> integer -> list integer let rec index_list from to step = diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 61477258..f69f59c1 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -1,33 +1,8 @@ open import Pervasives_extra -(*open import Sail_impl_base*) open import Sail_values -open import Prompt_monad -open import Prompt open import State_monad open import {isabelle} `State_monad_lemmas` -(* State monad wrapper around prompt monad *) - -val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e -let rec liftState ra s = match s with - | (Done a) -> returnS a - | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v)) - | (Read_tag t k) -> bindS (read_tagS t) (fun v -> liftState ra (k v)) - | (Write_memv a k) -> bindS (write_mem_bytesS a) (fun v -> liftState ra (k v)) - | (Write_tag a t k) -> bindS (write_tagS a t) (fun v -> liftState ra (k v)) - | (Read_reg r k) -> bindS (read_regvalS ra r) (fun v -> liftState ra (k v)) - | (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v)) - | (Undefined k) -> bindS (undefined_boolS ()) (fun v -> liftState ra (k v)) - | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz) (liftState ra k) - | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k) - | (Footprint k) -> liftState ra k - | (Barrier _ k) -> liftState ra k - | (Print _ k) -> liftState ra k (* TODO *) - | (Fail descr) -> failS descr - | (Exception e) -> throwS e -end - - val iterS_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e let rec iterS_aux i f xs = match xs with | x :: xs -> f i x >>$ iterS_aux (i + 1) f xs @@ -53,6 +28,46 @@ end declare {isabelle} termination_argument foreachS = automatic +val and_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e +let and_boolS l r = l >>$= (fun l -> if l then r else returnS false) + +val or_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e +let or_boolS l r = l >>$= (fun l -> if l then returnS true else r) + +val bool_of_bitU_fail : forall 'rv 'e. bitU -> monadS 'rv bool 'e +let bool_of_bitU_fail = function + | B0 -> returnS false + | B1 -> returnS true + | BU -> failS "bool_of_bitU" +end + +val bool_of_bitU_oracleS : forall 'rv 'e. bitU -> monadS 'rv bool 'e +let bool_of_bitU_oracleS = function + | B0 -> returnS false + | B1 -> returnS true + | BU -> undefined_boolS () +end + +val bools_of_bits_oracleS : forall 'rv 'e. list bitU -> monadS 'rv (list bool) 'e +let bools_of_bits_oracleS bits = + foreachS bits [] + (fun b bools -> + bool_of_bitU_oracleS b >>$= (fun b -> + returnS (bools ++ [b]))) + +val of_bits_oracleS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e +let of_bits_oracleS bits = + bools_of_bits_oracleS bits >>$= (fun bs -> + returnS (of_bools bs)) + +val of_bits_failS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e +let of_bits_failS bits = maybe_failS "of_bits" (of_bits bits) + +val mword_oracleS : forall 'rv 'a 'e. Size 'a => unit -> monadS 'rv (mword 'a) 'e +let mword_oracleS () = + bools_of_bits_oracleS (repeat [BU] (integerFromNat size)) >>$= (fun bs -> + returnS (wordFromBitlist bs)) + val whileS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) -> ('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e diff --git a/src/gen_lib/state_lifting.lem b/src/gen_lib/state_lifting.lem new file mode 100644 index 00000000..7e569a7e --- /dev/null +++ b/src/gen_lib/state_lifting.lem @@ -0,0 +1,27 @@ +open import Pervasives_extra +open import Sail_values +open import Prompt_monad +open import Prompt +open import State_monad +open import {isabelle} `State_monad_lemmas` + +(* State monad wrapper around prompt monad *) + +val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e +let rec liftState ra s = match s with + | (Done a) -> returnS a + | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v)) + | (Read_tag t k) -> bindS (read_tagS t) (fun v -> liftState ra (k v)) + | (Write_memv a k) -> bindS (write_mem_bytesS a) (fun v -> liftState ra (k v)) + | (Write_tag a t k) -> bindS (write_tagS a t) (fun v -> liftState ra (k v)) + | (Read_reg r k) -> bindS (read_regvalS ra r) (fun v -> liftState ra (k v)) + | (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v)) + | (Undefined k) -> bindS (undefined_boolS ()) (fun v -> liftState ra (k v)) + | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz) (liftState ra k) + | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k) + | (Footprint k) -> liftState ra k + | (Barrier _ k) -> liftState ra k + | (Print _ k) -> liftState ra k (* TODO *) + | (Fail descr) -> failS descr + | (Exception e) -> throwS e +end diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem index a2919762..89021890 100644 --- a/src/gen_lib/state_monad.lem +++ b/src/gen_lib/state_monad.lem @@ -94,12 +94,12 @@ let assert_expS exp msg = if exp then returnS () else failS msg (* For early return, we abuse exceptions by throwing and catching the return value. The exception type is "either 'r 'e", where "Right e" represents a proper exception and "Left r" an early return of value "r". *) -type monadSR 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e) +type monadRS 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e) -val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadSR 'regs 'a 'r 'e +val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadRS 'regs 'a 'r 'e let early_returnS r = throwS (Left r) -val catch_early_returnS : forall 'regs 'a 'e. monadSR 'regs 'a 'a 'e -> monadS 'regs 'a 'e +val catch_early_returnS : forall 'regs 'a 'e. monadRS 'regs 'a 'a 'e -> monadS 'regs 'a 'e let catch_early_returnS m = try_catchS m (function @@ -108,12 +108,12 @@ let catch_early_returnS m = end) (* Lift to monad with early return by wrapping exceptions *) -val liftSR : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadSR 'regs 'a 'r 'e -let liftSR m = try_catchS m (fun e -> throwS (Right e)) +val liftRS : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadRS 'regs 'a 'r 'e +let liftRS m = try_catchS m (fun e -> throwS (Right e)) (* Catch exceptions in the presence of early returns *) -val try_catchSR : forall 'regs 'a 'r 'e1 'e2. monadSR 'regs 'a 'r 'e1 -> ('e1 -> monadSR 'regs 'a 'r 'e2) -> monadSR 'regs 'a 'r 'e2 -let try_catchSR m h = +val try_catchRS : forall 'regs 'a 'r 'e1 'e2. monadRS 'regs 'a 'r 'e1 -> ('e1 -> monadRS 'regs 'a 'r 'e2) -> monadRS 'regs 'a 'r 'e2 +let try_catchRS m h = try_catchS m (function | Left r -> throwS (Left r) diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 58bbfc4b..c872d420 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -883,8 +883,7 @@ let doc_exp_lem, doc_let_lem = let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in let middle = match fst (untyp_pat pat) with - | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> - string ">>" + | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ">>" | P_aux (P_tup _, _) when not (IdSet.mem (mk_id "varstup") (find_e_ids e2)) -> (* Work around indentation issues in Lem when translating @@ -894,7 +893,8 @@ let doc_exp_lem, doc_let_lem = doc_pat_lem ctxt true pat; string "= varstup in"] | _ -> - separate space [string ">>= fun"; doc_pat_lem ctxt true pat; arrow] + separate space [string ">>= fun"; + doc_pat_lem ctxt true pat; arrow] in infix 0 1 middle (expV b e1) (expN e2) in @@ -908,12 +908,11 @@ let doc_exp_lem, doc_let_lem = raise (Reporting_basic.err_unreachable l "pretty-printing non-constant sizeof expressions to Lem not supported")) | E_return r -> - let ret_monad = if !opt_sequential then " : MR regstate" else " : MR" in let ta = if contains_t_pp_var ctxt (typ_of full_exp) || contains_t_pp_var ctxt (typ_of r) then empty else separate space - [string ret_monad; + [string ": MR"; parens (doc_typ_lem (typ_of full_exp)); parens (doc_typ_lem (typ_of r))] in align (parens (string "early_return" ^//^ expV true r ^//^ ta)) @@ -1438,17 +1437,11 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) (Defs defs) separate empty (List.map doc_def_lem statedefs); hardline; hardline; register_refs; hardline; - (* if !opt_sequential then - concat [ - string ("type MR 'a 'r = State_monad.MR regstate 'a 'r " ^ exc_typ); hardline; - string ("type M 'a = State_monad.M regstate 'a " ^ exc_typ); hardline; - ] - else *) - concat [ - string ("type MR 'a 'r = monadR register_value 'a 'r " ^ exc_typ); hardline; - string ("type M 'a = monad register_value 'a " ^ exc_typ); hardline - ] - ]); + concat [ + string ("type MR 'a 'r = base_monadR register_value regstate 'a 'r " ^ exc_typ); hardline; + string ("type M 'a = base_monad register_value regstate 'a " ^ exc_typ); hardline + ] + ]); (print defs_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; diff --git a/src/process_file.ml b/src/process_file.ml index 4856c20a..34c1a255 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -51,9 +51,6 @@ open PPrint open Pretty_print_common -let opt_lem_sequential = ref false -let opt_lem_mwords = ref false - type out_type = | Lem_ast_out | Lem_out of string list @@ -246,10 +243,7 @@ let output_lem filename libs defs = let generated_line = generated_line filename in (* let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in *) let types_module = (filename ^ "_types") in - let monad_modules = ["Prompt_monad"; "Prompt"; "State"] in - (* if !Pretty_print_lem.opt_sequential - then ["State_monad"; "State"] - else ["Prompt_monad"; "Prompt"] in *) + let monad_modules = ["Prompt_monad"; "Prompt"] in let operators_module = if !Pretty_print_lem.opt_mwords then "Sail_operators_mwords" diff --git a/src/process_file.mli b/src/process_file.mli index b38b4259..cc94888e 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -65,8 +65,6 @@ val rewrite_ast_check : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val load_file_no_check : Ast.order -> string -> unit Ast.defs val load_file : Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t -val opt_lem_sequential : bool ref -val opt_lem_mwords : bool ref val opt_just_check : bool ref val opt_ddump_tc_ast : bool ref val opt_ddump_rewrite_ast : ((string * int) option) ref diff --git a/test/isabelle/run_cheri.ml b/test/isabelle/run_cheri.ml index e6d752b7..f51ef4dd 100644 --- a/test/isabelle/run_cheri.ml +++ b/test/isabelle/run_cheri.ml @@ -64,7 +64,7 @@ let () = Arg.parse options (fun s -> opt_file_arguments := !opt_file_arguments @ [s]) usage_msg let (>>) = State_monad.bindS -let liftS = State.liftState (Cheri_types.get_regval, Cheri_types.set_regval) +let liftS = State_lifting.liftState (Cheri_types.get_regval, Cheri_types.set_regval) let load_elf_segment seg = let open Elf_interpreted_segment in |