diff options
| -rw-r--r-- | cheri/Makefile | 5 | ||||
| -rw-r--r-- | lib/hol/Holmakefile | 27 | ||||
| -rw-r--r-- | lib/hol/Makefile | 31 | ||||
| -rw-r--r-- | lib/hol/prompt.lem | 12 | ||||
| -rw-r--r-- | lib/hol/prompt_monad.lem | 32 |
5 files changed, 106 insertions, 1 deletions
diff --git a/cheri/Makefile b/cheri/Makefile index d053fc67..e084d68b 100644 --- a/cheri/Makefile +++ b/cheri/Makefile @@ -57,7 +57,7 @@ cheri_types.lem: cheri.lem cheri_sequential.lem: $(CHERI_SAILS) $(SAIL) -lem -o cheri_sequential -auto_mono -mono_rewrites -lem_mwords -lem_sequential -lem_lib Mips_extras_sequential -undefined_gen -memo_z3 $^ cheri_sequential_types.lem: cheri_sequential.lem -Cheri_sequential.thy: $(MIPS_SAIL_DIR)/mips_extras_sequential.lem +Cheri_sequential.thy cheri_sequentialScript.sml: $(MIPS_SAIL_DIR)/mips_extras_sequential.lem cheri128_no_tlb.lem: $(CHERI128_NO_TLB_SAILS) $(SAIL) -lem -o cheri128_no_tlb -lem_lib Mips_extras -undefined_gen -memo_z3 $^ @@ -71,6 +71,9 @@ 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)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ + clean: rm -rf cheri cheri128 _sbuild inst_*.sail cheri.c diff --git a/lib/hol/Holmakefile b/lib/hol/Holmakefile new file mode 100644 index 00000000..442b1816 --- /dev/null +++ b/lib/hol/Holmakefile @@ -0,0 +1,27 @@ +SCRIPTS = sail_instr_kindsScript.sml sail_valuesScript.sml sail_operatorsScript.sml \ + sail_operators_mwordsScript.sml sail_operators_bitlistsScript.sml \ + state_monadScript.sml stateScript.sml + +EXTRA_CLEANS = $(SCRIPTS) + +THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS)) + +LEMDIR=../../../lem/hol-lib + +INCLUDES = $(LEMDIR) + +all: $(THYS) +.PHONY: all + +ifdef POLY +HOLHEAP = sail-heap +EXTRA_CLEANS = $(SCRIPTS) $(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..b6be46b4 --- /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 + +all: sail-heap + +$(SCRIPTS): $(LEMSRC) + lem -hol -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $(LEMSRC) + +THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS)) + +$(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..a04e0a0a --- /dev/null +++ b/lib/hol/prompt.lem @@ -0,0 +1,12 @@ +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 diff --git a/lib/hol/prompt_monad.lem b/lib/hol/prompt_monad.lem new file mode 100644 index 00000000..b1ef4bcc --- /dev/null +++ b/lib/hol/prompt_monad.lem @@ -0,0 +1,32 @@ +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 + +let inline return = returnS +let inline bind = bindS +let inline (>>=) = (>>$=) +let inline (>>) = (>>$) + +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 maybe_fail = maybe_failS + +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 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 () |