diff options
Diffstat (limited to 'cheri')
| -rw-r--r-- | cheri/Makefile | 43 | ||||
| -rw-r--r-- | cheri/cheri_prelude_common.sail | 11 |
2 files changed, 47 insertions, 7 deletions
diff --git a/cheri/Makefile b/cheri/Makefile index c7f72557..6fa738a7 100644 --- a/cheri/Makefile +++ b/cheri/Makefile @@ -7,16 +7,51 @@ CHERI_SAIL_DIR:=$(SAIL_DIR)/cheri SAIL:=$(SAIL_DIR)/sail SAIL_LIB_HEADERS:=$(SAIL_LIB_DIR)/flow.sail -CHERI_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/main.sail +MIPS_PRE:=$(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail +MIPS_TLB:=$(MIPS_SAIL_DIR)/mips_tlb.sail +MIPS_TLB_STUB:=$(MIPS_SAIL_DIR)/mips_tlb_stub.sail +MIPS_INSTS:=$(MIPS_SAIL_DIR)/mips_insts.sail +MIPS_EPILOGUE:=$(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +CHERI_PRE:=$(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail +CHERI128_PRE:=$(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail +CHERI_INSTS:=$(CHERI_SAIL_DIR)/cheri_insts.sail -CHERI128_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/main.sail +CHERI_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_PRE) $(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) +CHERI_MAIN:=$(CHERI_SAIL_DIR)/main.sail -cheri: $(CHERI_SAILS) +cheri: $(CHERI_SAILS) $(CHERI_MAIN) $(SAIL) -ocaml -o $@ $^ -cheri128: $(CHERI128_SAILS) +cheri128: $(CHERI128_SAILS) $(CHERI_MAIN) $(SAIL) -ocaml -o $@ $^ +# TODO Using bit lists for now in Lem generation; for machine words, +# monomorphisation is needed due to some variable length bitvectors, e.g. in +# CLoad as of commit b34c3fb, in the TLB translation, and in compressed +# capability functions + +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) + $(SAIL) -lem -o cheri -lem_lib Mips_extras -undefined_gen -memo_z3 $^ +cheri_types.lem: cheri.lem + +cheri128_no_tlb.lem: $(CHERI128_NO_TLB_SAILS) + $(SAIL) -lem -o cheri128_no_tlb -lem_lib Mips_extras -undefined_gen -memo_z3 $^ +cheri128_no_tlb_types.lem: cheri128_no_tlb.lem + +cheri128.lem: $(CHERI128_SAILS) + $(SAIL) -lem -o cheri128 -lem_lib Mips_extras -undefined_gen -memo_z3 $^ +cheri128_types.lem: cheri128.lem + +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 $^ + clean: rm -rf cheri cheri128 _sbuild inst_*.sail diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail index 5dd14974..0072ded7 100644 --- a/cheri/cheri_prelude_common.sail +++ b/cheri/cheri_prelude_common.sail @@ -255,8 +255,8 @@ function register_inaccessible(r) = else false -val MEMr_tag = "read_tag" : bits(64) -> bool effect { rmemt } -val MEMw_tag = "write_tag" : (bits(64) , bool) -> unit effect { wmvt } +val MEMr_tag = "read_tag_bool" : bits(64) -> bool effect { rmemt } +val MEMw_tag = "write_tag_bool" : (bits(64) , bool) -> unit effect { wmvt } val MEMr_tagged : bits(64) -> (bool, bits('cap_size * 8)) effect { escape, rmem, rmemt } function MEMr_tagged (addr) = @@ -360,7 +360,12 @@ function addrWrapper(addr, accessType, width) = to_bits(64, vAddr); /* XXX vAddr not truncated because top <= 2^64 and size > 0 */ } -val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, undef, escape} +$ifdef _MIPS_TLB_STUB +val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, escape} +$else +val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, escape, undef} +$endif + function TranslatePC (vAddr) = { incrementCP0Count(); let pcc = capRegToCapStruct(PCC); |