diff options
Diffstat (limited to 'cheri')
| -rw-r--r-- | cheri/Makefile | 7 | ||||
| -rw-r--r-- | cheri/cheri_prelude_256.sail | 2 |
2 files changed, 6 insertions, 3 deletions
diff --git a/cheri/Makefile b/cheri/Makefile index 88c5cf0d..3ccc14df 100644 --- a/cheri/Makefile +++ b/cheri/Makefile @@ -25,6 +25,9 @@ CHERI_MAIN:=$(MIPS_SAIL_DIR)/main.sail cheri: $(CHERI_SAILS) $(CHERI_MAIN) $(SAIL) -ocaml -o $@ $^ +cheri.c: $(CHERI_SAILS) $(CHERI_MAIN) + $(SAIL) -memo_z3 -c $^ 1> $@ + cheri128: $(CHERI128_SAILS) $(CHERI_MAIN) $(SAIL) -ocaml -o $@ $^ @@ -54,7 +57,7 @@ C%.thy: c%.lem c%_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem sed -i 's/datatype ast/datatype (plugins only: size) ast/' C$*_types.thy clean: - rm -rf cheri cheri128 _sbuild inst_*.sail + rm -rf cheri cheri128 _sbuild inst_*.sail cheri.c EXTRACT_INST=sed -n "/START_${1}\b/,/END_${1}\b/p" cheri_insts.sail | sed 's/^ //;1d;$$d' > inst_$1.sail extract: cheri_insts.sail @@ -67,7 +70,7 @@ extract: cheri_insts.sail $(call EXTRACT_INST,CGetSealed) $(call EXTRACT_INST,CGetPCC) $(call EXTRACT_INST,CGetPCCSetOffset) - $(call EXTRACT_INST,CGetCause) + $(call EXTRACT_INST,CGetCause $(call EXTRACT_INST,CSetCause) $(call EXTRACT_INST,CAndPerm) $(call EXTRACT_INST,CToPtr) diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail index 3af7ee28..8e4a14f8 100644 --- a/cheri/cheri_prelude_256.sail +++ b/cheri/cheri_prelude_256.sail @@ -230,7 +230,7 @@ function getCapLength(c) : CapStruct -> CapLen = unsigned(c.length) function getCapCursor(cap) : CapStruct -> uint64 = (unsigned(cap.base) + unsigned(cap.offset)) % (pow2(64)) -function setCapOffset(c, offset) : (CapStruct, bits(64)) -> (bool, CapStruct) = +function setCapOffset(c, offset) : (CapStruct, bits(64)) -> (bool, CapStruct) = (true, {c with offset=offset}) function incCapOffset(c, delta) : (CapStruct, bits(64)) -> (bool, CapStruct) = |