diff options
| -rw-r--r-- | cheri/Makefile | 15 | ||||
| -rw-r--r-- | cheri/cheri_insts.sail | 14 |
2 files changed, 19 insertions, 10 deletions
diff --git a/cheri/Makefile b/cheri/Makefile index e056a9a9..e6c57780 100644 --- a/cheri/Makefile +++ b/cheri/Makefile @@ -18,7 +18,7 @@ cheri128: $(CHERI128_SAILS) $(SAIL) -ocaml -o $@ $^ clean: - rm -rf cheri cheri128 _sbuild + rm -rf cheri cheri128 _sbuild inst_*.sail 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 @@ -38,21 +38,30 @@ extract: cheri_insts.sail $(call EXTRACT_INST,CSub) $(call EXTRACT_INST,CPtrCmp) $(call EXTRACT_INST,CIncOffset) + $(call EXTRACT_INST,CIncOffsetImmediate) $(call EXTRACT_INST,CSetOffset) $(call EXTRACT_INST,CSetBounds) + $(call EXTRACT_INST,CSetBoundsImmediate) $(call EXTRACT_INST,CSetBoundsExact) $(call EXTRACT_INST,CClearTag) + $(call EXTRACT_INST,CMOVX) $(call EXTRACT_INST,ClearRegs) $(call EXTRACT_INST,CFromPtr) + $(call EXTRACT_INST,CBuildCap) + $(call EXTRACT_INST,CCopyType) $(call EXTRACT_INST,CCheckPerm) $(call EXTRACT_INST,CCheckType) + $(call EXTRACT_INST,CTestSubset) $(call EXTRACT_INST,CSeal) $(call EXTRACT_INST,CUnseal) $(call EXTRACT_INST,CCall) + $(call EXTRACT_INST,CCall2) $(call EXTRACT_INST,CReturn) - $(call EXTRACT_INST,CBx) + $(call EXTRACT_INST,CBtag) + $(call EXTRACT_INST,CBz) $(call EXTRACT_INST,CJALR) $(call EXTRACT_INST,CLoad) $(call EXTRACT_INST,CStore) $(call EXTRACT_INST,CSC) - $(call EXTRACT_INST,CLC) + $(call EXTRACT_INST,CLC) + diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail index ff2c7264..ebdc474e 100644 --- a/cheri/cheri_insts.sail +++ b/cheri/cheri_insts.sail @@ -565,7 +565,7 @@ function clause execute (CSetBounds(cd, cb, rt)) = union clause ast = CSetBoundsImmediate : (regno, regno, bits(11)) function clause execute (CSetBoundsImmediate(cd, cb, imm)) = { - /* START_CSetBoundsImmedate */ + /* START_CSetBoundsImmediate */ checkCP2usable(); cb_val = readCapReg(cb); immU = unsigned(imm); @@ -1079,29 +1079,29 @@ function clause execute (CReturn()) = } union clause ast = CBX : (regno, bits(16), bool) -function clause execute (CBX(cb, imm, invert)) = +function clause execute (CBX(cb, imm, notset)) = { - /* START_CBx */ + /* START_CBtag */ checkCP2usable(); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if (((readCapReg(cb)).tag) ^ invert) then + else if (((readCapReg(cb)).tag) ^ notset) then { let offset : bits(64) = (EXTS(imm @ 0b00) + 4) in delayedPC = PC + offset; branchPending = 0b1; } - /* END_CBx */ + /* END_CBtag */ } union clause ast = CBZ : (regno, bits(16), bool) -function clause execute (CBZ(cb, imm, invert)) = +function clause execute (CBZ(cb, imm, notzero)) = { /* START_CBz */ checkCP2usable(); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if (((readCapReg(cb)) == null_cap) ^ invert) then + else if (((readCapReg(cb)) == null_cap) ^ notzero) then { let offset : bits(64) = (EXTS(imm @ 0b00) + 4) in delayedPC = PC + offset; |