From af4841d5fa173e2d9639afe737d9cdfab733c935 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 21 Apr 2016 13:47:10 +0100 Subject: Introduce wrapper function around MEMw* so that we can clear tags on non-capability writes on cheri. --- cheri/cheri_insts.sail | 16 ++++++------ cheri/cheri_prelude.sail | 20 +++++++++++++++ mips/mips_insts.sail | 64 ++++++++++++++++++++++++------------------------ mips/mips_wrappers.sail | 3 +++ src/Makefile | 2 +- 5 files changed, 64 insertions(+), 41 deletions(-) create mode 100644 mips/mips_wrappers.sail diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail index ee7ae0d4..935f47ca 100644 --- a/cheri/cheri_insts.sail +++ b/cheri/cheri_insts.sail @@ -573,10 +573,10 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) = success := if (CP0LLBit[0]) then switch(width) { - case B -> MEMw_conditional(pAddr, 1, rs_val[7..0]) - case H -> MEMw_conditional(pAddr, 2, rs_val[15..0]) - case W -> MEMw_conditional(pAddr, 4, rs_val[31..0]) - case D -> MEMw_conditional(pAddr, 8, rs_val) + case B -> MEMw_conditional_wrapper(pAddr, 1, rs_val[7..0]) + case H -> MEMw_conditional_wrapper(pAddr, 2, rs_val[15..0]) + case W -> MEMw_conditional_wrapper(pAddr, 4, rs_val[31..0]) + case D -> MEMw_conditional_wrapper(pAddr, 8, rs_val) } else false; @@ -585,10 +585,10 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) = else switch(width) { - case B -> MEMw(pAddr, 1) := rs_val[7..0] - case H -> MEMw(pAddr, 2) := rs_val[15..0] - case W -> MEMw(pAddr, 4) := rs_val[31..0] - case D -> MEMw(pAddr, 8) := rs_val + case B -> MEMw_wrapper(pAddr, 1) := rs_val[7..0] + case H -> MEMw_wrapper(pAddr, 2) := rs_val[15..0] + case W -> MEMw_wrapper(pAddr, 4) := rs_val[31..0] + case D -> MEMw_wrapper(pAddr, 8) := rs_val } } } diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail index 78bf019f..94e5e759 100644 --- a/cheri/cheri_prelude.sail +++ b/cheri/cheri_prelude.sail @@ -316,6 +316,7 @@ val extern (bit[64]) -> (bit[8]) effect { rmem } TAGr function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) = { + (* assumes addr is cap. aligned *) let tag = (TAGr (addr)) in let mem = (MEMr (addr, cap_size)) in (tag[0], mem) @@ -323,6 +324,7 @@ function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) = function (bool, bit[cap_size_t * 8]) MEMr_tagged_reserve ((bit[64]) addr) = { + (* assumes addr is cap. aligned *) let tag = (TAGr (addr)) in let mem = (MEMr_reserve (addr, cap_size)) in (tag[0], mem) @@ -330,14 +332,32 @@ function (bool, bit[cap_size_t * 8]) MEMr_tagged_reserve ((bit[64]) addr) = function unit MEMw_tagged((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) = { + (* assumes addr is cap. aligned *) MEMw(addr, cap_size, data); TAGw(addr, (0b0000000 : [tag])); } function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) = { + (* assumes addr is cap. aligned *) success := MEMw_conditional(addr, cap_size, data); if (success) then TAGw(addr, (0b0000000 : [tag])); success; } + +function unit effect {wmem} MEMw_wrapper(addr, size, data) = + { + (* On cheri non-capability writes must clear the corresponding tag*) + TAGw((addr[63..5] : 0b00000), 0x00); + MEMw(addr,size,data) + } + +function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) = + { + (* On cheri non-capability writes must clear the corresponding tag*) + success := MEMw_conditional(addr,size,data); + if (success) then + TAGw((addr[63..5] : 0b00000), 0x00); + success; + } diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail index 15aad01d..bb7f991f 100644 --- a/mips/mips_insts.sail +++ b/mips/mips_insts.sail @@ -1072,20 +1072,20 @@ function clause execute (Store(width, conditional, base, rt, offset)) = { success := if (CP0LLBit[0]) then switch(width) { - case B -> MEMw_conditional(pAddr, 1, rt_val[7..0]) - case H -> MEMw_conditional(pAddr, 2, rt_val[15..0]) - case W -> MEMw_conditional(pAddr, 4, rt_val[31..0]) - case D -> MEMw_conditional(pAddr, 8, rt_val) + case B -> MEMw_conditional_wrapper(pAddr, 1, rt_val[7..0]) + case H -> MEMw_conditional_wrapper(pAddr, 2, rt_val[15..0]) + case W -> MEMw_conditional_wrapper(pAddr, 4, rt_val[31..0]) + case D -> MEMw_conditional_wrapper(pAddr, 8, rt_val) } else false; wGPR(rt) := EXTZ([success]) } else switch(width) { - case B -> MEMw(pAddr, 1) := rt_val[7..0] - case H -> MEMw(pAddr, 2) := rt_val[15..0] - case W -> MEMw(pAddr, 4) := rt_val[31..0] - case D -> MEMw(pAddr, 8) := rt_val + case B -> MEMw_wrapper(pAddr, 1) := rt_val[7..0] + case H -> MEMw_wrapper(pAddr, 2) := rt_val[15..0] + case W -> MEMw_wrapper(pAddr, 4) := rt_val[31..0] + case D -> MEMw_wrapper(pAddr, 8) := rt_val } } } @@ -1143,10 +1143,10 @@ function clause execute(SWL(base, rt, offset)) = reg_val := rGPR(rt); switch (vAddr[1..0]) { - case 0b00 -> (MEMw(pAddr, 4) := reg_val[31..0]) - case 0b01 -> (MEMw(pAddr, 3) := reg_val[31..8]) - case 0b10 -> (MEMw(pAddr, 2) := reg_val[31..16]) - case 0b11 -> (MEMw(pAddr, 1) := reg_val[31..24]) + case 0b00 -> (MEMw_wrapper(pAddr, 4) := reg_val[31..0]) + case 0b01 -> (MEMw_wrapper(pAddr, 3) := reg_val[31..8]) + case 0b10 -> (MEMw_wrapper(pAddr, 2) := reg_val[31..16]) + case 0b11 -> (MEMw_wrapper(pAddr, 1) := reg_val[31..24]) } } } @@ -1163,10 +1163,10 @@ function clause execute(SWR(base, rt, offset)) = reg_val := rGPR(rt); switch (vAddr[1..0]) { - case 0b00 -> (MEMw(wordAddr, 1) := reg_val[7..0]) - case 0b01 -> (MEMw(wordAddr, 2) := reg_val[15..0]) - case 0b10 -> (MEMw(wordAddr, 3) := reg_val[23..0]) - case 0b11 -> (MEMw(wordAddr, 4) := reg_val[31..0]) + case 0b00 -> (MEMw_wrapper(wordAddr, 1) := reg_val[7..0]) + case 0b01 -> (MEMw_wrapper(wordAddr, 2) := reg_val[15..0]) + case 0b10 -> (MEMw_wrapper(wordAddr, 3) := reg_val[23..0]) + case 0b11 -> (MEMw_wrapper(wordAddr, 4) := reg_val[31..0]) } } } @@ -1233,14 +1233,14 @@ function clause execute(SDL(base, rt, offset)) = reg_val := rGPR(rt); switch (vAddr[2..0]) { - case 0b000 -> (MEMw(pAddr, 8) := reg_val[63..00]) - case 0b001 -> (MEMw(pAddr, 7) := reg_val[63..08]) - case 0b010 -> (MEMw(pAddr, 6) := reg_val[63..16]) - case 0b011 -> (MEMw(pAddr, 5) := reg_val[63..24]) - case 0b100 -> (MEMw(pAddr, 4) := reg_val[63..32]) - case 0b101 -> (MEMw(pAddr, 3) := reg_val[63..40]) - case 0b110 -> (MEMw(pAddr, 2) := reg_val[63..48]) - case 0b111 -> (MEMw(pAddr, 1) := reg_val[63..56]) + case 0b000 -> (MEMw_wrapper(pAddr, 8) := reg_val[63..00]) + case 0b001 -> (MEMw_wrapper(pAddr, 7) := reg_val[63..08]) + case 0b010 -> (MEMw_wrapper(pAddr, 6) := reg_val[63..16]) + case 0b011 -> (MEMw_wrapper(pAddr, 5) := reg_val[63..24]) + case 0b100 -> (MEMw_wrapper(pAddr, 4) := reg_val[63..32]) + case 0b101 -> (MEMw_wrapper(pAddr, 3) := reg_val[63..40]) + case 0b110 -> (MEMw_wrapper(pAddr, 2) := reg_val[63..48]) + case 0b111 -> (MEMw_wrapper(pAddr, 1) := reg_val[63..56]) } } } @@ -1259,14 +1259,14 @@ function clause execute(SDR(base, rt, offset)) = wordAddr := pAddr[63..3] : 0b000; switch (vAddr[2..0]) { - case 0b000 -> (MEMw(wordAddr, 1) := reg_val[07..0]) - case 0b001 -> (MEMw(wordAddr, 2) := reg_val[15..0]) - case 0b010 -> (MEMw(wordAddr, 3) := reg_val[23..0]) - case 0b011 -> (MEMw(wordAddr, 4) := reg_val[31..0]) - case 0b100 -> (MEMw(wordAddr, 5) := reg_val[39..0]) - case 0b101 -> (MEMw(wordAddr, 6) := reg_val[47..0]) - case 0b110 -> (MEMw(wordAddr, 7) := reg_val[55..0]) - case 0b111 -> (MEMw(wordAddr, 8) := reg_val[63..0]) + case 0b000 -> (MEMw_wrapper(wordAddr, 1) := reg_val[07..0]) + case 0b001 -> (MEMw_wrapper(wordAddr, 2) := reg_val[15..0]) + case 0b010 -> (MEMw_wrapper(wordAddr, 3) := reg_val[23..0]) + case 0b011 -> (MEMw_wrapper(wordAddr, 4) := reg_val[31..0]) + case 0b100 -> (MEMw_wrapper(wordAddr, 5) := reg_val[39..0]) + case 0b101 -> (MEMw_wrapper(wordAddr, 6) := reg_val[47..0]) + case 0b110 -> (MEMw_wrapper(wordAddr, 7) := reg_val[55..0]) + case 0b111 -> (MEMw_wrapper(wordAddr, 8) := reg_val[63..0]) } } } diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail new file mode 100644 index 00000000..218f985a --- /dev/null +++ b/mips/mips_wrappers.sail @@ -0,0 +1,3 @@ +function unit effect {wmem} MEMw_wrapper(addr, size, data) = MEMw(addr, size, data) +function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) = + MEMw_conditional(addr, size, data) \ No newline at end of file diff --git a/src/Makefile b/src/Makefile index 12535ace..cd21ed1a 100644 --- a/src/Makefile +++ b/src/Makefile @@ -25,7 +25,7 @@ LEMLIBOCAML = $(BITBUCKET_ROOT)/lem/ocaml-lib ELFDIR= $(BITBUCKET_ROOT)/linksem MIPS_SAIL_DIR:=$(BITBUCKET_ROOT)/l2/mips -MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/l2/cheri CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail -- cgit v1.2.3