Skip to content

Commit 73d3589

Browse files
PeterRuggPeterRugg
committed
Automate extraction of concentrate listings
1 parent ff1ff92 commit 73d3589

File tree

9 files changed

+363
-335
lines changed

9 files changed

+363
-335
lines changed

‎.gitignore‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,3 +21,5 @@
2121

2222
/sail-cheri-riscv
2323
/sail-cheri-mips
24+
25+
/cheri_concentrate_listings/cheri-cap-lib

‎Makefile‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ PREVEOUS=../branches/20150624-cheri-architecture-1-13
44

55
SAIL_LATEX_RISCV_DIR=sail_latex_riscv
66

7-
SOURCES=$(wildcard *.tex insn-riscv/*.tex $(SAIL_LATEX_RISCV_DIR)/*.tex) cheri.bib LICENSE LICENSE-sail-cheri-riscv LICENSE-sail-riscv
7+
SOURCES=$(wildcard *.tex insn-riscv/*.tex $(SAIL_LATEX_RISCV_DIR)/*.tex cheri_concentrate_listings/*.bsv) cheri.bib LICENSE LICENSE-sail-cheri-riscv LICENSE-sail-riscv
88
DIFFDIR=diff
99
DIFFTEX=$(SOURCES:%=${DIFFDIR}/%)
1010
DIFFPARAM=--type=UNDERLINE --packages=amsmath,hyperref --math-markup=1
@@ -127,7 +127,10 @@ update-sail-defs-riscv: $(SAIL_CHERI_RISCV_DIR)
127127

128128
update-sail-defs: update-sail-defs-riscv
129129

130-
.PHONY: clean update-sail-defs sail-cheri-riscv-latex update-sail-defs-riscv
130+
update-concentrate-defs:
131+
$(MAKE) -C cheri_concentrate_listings
132+
133+
.PHONY: clean update-sail-defs sail-cheri-riscv-latex update-sail-defs-riscv update-concentrate-defs
131134
clean:
132135
latexmk -C $(LATEXMK_COMMON_FLAGS) cheri-architecture.tex
133136
latexmk -C $(LATEXMK_COMMON_FLAGS) fig-*.tex

‎app-cheri-concentrate-listings.tex‎

Lines changed: 5 additions & 333 deletions
Large diffs are not rendered by default.

‎cheri_concentrate_listings/Makefile‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
.PHONY: all
2+
all: conc_getTopFat.bsv \
3+
conc_capInBounds.bsv \
4+
conc_incOffsetFat.bsv \
5+
conc_setAddress.bsv \
6+
conc_setBoundsFat.bsv
7+
8+
cheri-cap-lib:
9+
git clone https://github.com/CTSRD-CHERI/cheri-cap-lib
10+
11+
cheri-cap-lib/CHERICC_Fat.bsv: cheri-cap-lib
12+
13+
conc_%.bsv: cheri-cap-lib/CHERICC_Fat.bsv
14+
sed -n "/^function.*$*/,/^endfunction/p" $^ > $@
15+
16+
.PHONY: clean
17+
clean:
18+
rm -rf *.bsv

‎cheri_concentrate_listings/conc_capInBounds.bsv‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
function Bool capInBounds(CapFat cap, TempFields tf, Bool inclusive);
2+
// Check that the pointer of a capability is currently within the bounds
3+
// of the capability
4+
Bool ptrVStop = inclusive ? cap.addrBits <= cap.bounds.topBits
5+
: cap.addrBits < cap.bounds.topBits;
6+
// Top is ok if the pointer and top are in the same alignment region
7+
// and the pointer is less than the top. If they are not in the same
8+
// alignment region, it's ok if the top is in Hi and the bottom in Low.
9+
Bool topOk = (tf.topHi == tf.addrHi) ? ptrVStop : tf.topHi;
10+
Bool baseOk = (tf.baseHi == tf.addrHi) ? cap.addrBits >= cap.bounds.baseBits
11+
: tf.addrHi;
12+
return topOk && baseOk;
13+
endfunction

‎cheri_concentrate_listings/conc_getTopFat.bsv‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
function CapAddrPlus1 getTopFat(CapFat cap, TempFields tf);
2+
// First, construct a full length value with the top bits and the
3+
// correction bits above, and shift that value to the appropriate spot.
4+
CapAddrPlus1 addTop = signExtend({pack(tf.topCorrection), cap.bounds.topBits}) << cap.bounds.exp;
5+
// Build a mask on the high bits of a full length value to extract the high
6+
// bits of the address.
7+
Bit#(TSub#(TAdd#(CapAddrW,1),MW)) mask = ~0 << cap.bounds.exp;
8+
// Extract the high bits of the address (and append the implied zeros at the
9+
// bottom), and add with the previously prepared value.
10+
CapAddrPlus1 ret = {truncateLSB({1'b0,cap.address})&mask,0} + addTop;
11+
// If the bottom and top are more than an address space away from eachother,
12+
// invert the 64th/32nd bit of Top. This corrects for errors that happen
13+
// when the representable space wraps the address space.
14+
Bit#(2) topTip = truncateLSB(ret);
15+
// Calculate the msb of the base.
16+
// First assume that only the address and correction are involved...
17+
Bit#(TSub#(CapAddrW,MW)) bot = truncateLSB(cap.address) + (signExtend(pack(tf.baseCorrection)) << cap.bounds.exp);
18+
Bit#(2) botTip = {1'b0, msb(bot)};
19+
// If the bit we're interested in are actually coming from baseBits, select
20+
// the correct one from there.
21+
// exp == (resetExp - 1) doesn't matter since we will not flip unless
22+
// exp < resetExp-1.
23+
if (cap.bounds.exp == (resetExp - 2)) botTip = {1'b0, cap.bounds.baseBits[valueOf(MW)-1]};
24+
// Do the final check.
25+
// If exp >= resetExp - 1, the bits we're looking at are coming directly from
26+
// topBits and baseBits, are not being inferred, and therefore do not need
27+
// correction. If we are below this range, check that the difference between
28+
// the resulting top and bottom is less than one address space. If not, flip
29+
// the msb of the top.
30+
if (cap.bounds.exp<(resetExp-1) && (topTip - botTip) > 1)
31+
ret[valueOf(CapAddrW)] = ~ret[valueOf(CapAddrW)];
32+
return ret;
33+
endfunction

‎cheri_concentrate_listings/conc_incOffsetFat.bsv‎

Lines changed: 138 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,138 @@
1+
function VnD#(CapFat) incOffsetFat( CapFat cap
2+
, CapAddr pointer
3+
, CapAddr offset // this is the increment in inc offset, and the offset in set offset
4+
, TempFields tf
5+
, Bool setOffset);
6+
// NOTE:
7+
// The 'offset' argument is the "increment" value when setOffset is false, and
8+
// the actual "offset" value when setOffset is true.
9+
//
10+
// For this function to work correctly, we must have
11+
// 'offset' = 'pointer'-'cap.address'.
12+
// In the most critical case we have both available and picking one or the
13+
// other is less efficient than passing both. If the 'setOffset' flag is set,
14+
// this function will ignore the 'pointer' argument and use 'offset' to set the
15+
// offset of 'cap' by adding it to the capability base. If the 'setOffset' flag
16+
// is not set, this function will increment the offset of 'cap' by replacing
17+
// the 'cap.address' field with the 'pointer' argument (with the assumption
18+
// that the 'pointer' argument is indeed equal to 'cap.address'+'offset'. The
19+
// 'cap.addrBits' field is also updated accordingly.
20+
CapFat ret = cap;
21+
Exp e = cap.bounds.exp;
22+
// Updating the address of a capability requires checking that the new
23+
// address is still within representable bounds. For capabilities with big
24+
// representable regions (with exponents >= resetExp-2), there is no
25+
// representability issue.
26+
// For the other capabilities, the check consists of two steps:
27+
// - A "inRange" test
28+
// - A "inLimits" test
29+
30+
// The inRange test
31+
// ----------------
32+
// Conceptually, the inRange test checks the magnitude of 'offset' is less
33+
// then the representable region's size S. This ensures that the inLimits
34+
// test result is meaningful. The test succeeds if the absolute value of
35+
// 'offset' is less than S, that is -S < 'offset' < S. This test reduces to a
36+
// check that there are no significant bits in the high bits of 'offset',
37+
// that is they are all ones or all zeros.
38+
CapAddr offsetAddr = offset;
39+
Bit#(TSub#(CapAddrW,MW)) signBits = signExtend(offset[valueOf(TSub#(CapAddrW,1))]);
40+
Bit#(TSub#(CapAddrW,MW)) highOffsetBits = truncateLSB(offsetAddr);
41+
Bit#(TSub#(CapAddrW,MW)) highBitsfilter = -1 << e;
42+
highOffsetBits = (highOffsetBits ^ signBits) & highBitsfilter;
43+
Bool inRange = (highOffsetBits == 0);
44+
45+
// The inLimits test
46+
// -----------------
47+
// Conceptually, the inLimits test ensures that neither the of the edges of
48+
// the representable region have been crossed with the new address. In
49+
// essence, it compares the distance 'offsetBits' added (on MW bits) with the
50+
// distance 'toBounds' to the edge of the representable space (on MW bits).
51+
// - For a positive or null increment
52+
// inLimits = offsetBits < toBounds - 1
53+
// - For a negative increment:
54+
// inLimits = (offsetBits >= toBounds) and ('we were not already on the
55+
// bottom edge') (when already on the bottom edge of the representable
56+
// space, the relevant bits of the address and those of the representable
57+
// edge are the same, leading to a false positive on the i >= toBounds
58+
// comparison)
59+
60+
// The sign of the increment
61+
Bool posInc = msb(offsetAddr) == 1'b0;
62+
63+
// The offsetBits value corresponds to the appropriate slice of the
64+
// 'offsetAddr' argument
65+
Bit#(MW) offsetBits = truncate(offsetAddr >> e);
66+
67+
// The toBounds value is given by substracting the address of the capability
68+
// from the address of the edge of the representable region (on MW bits) when
69+
// the 'setOffset' flag is not set. When it is set, it is given by
70+
// substracting the base address of the capability from the edge of the
71+
// representable region (on MW bits). This value is both the distance to the
72+
// representable top and the distance to the representable bottom (when
73+
// appended to a one for negative sign), a convenience of the two's
74+
// complement representation.
75+
76+
// NOTE: When the setOffset flag is set, toBounds should be the distance from
77+
// the base to the representable edge. This can be computed efficiently, and
78+
// without relying on the temporary fields, as follows: equivalent to
79+
// (repBoundBits - cap.bounds.baseBits):
80+
Bit#(MW) toBounds_A = {3'b111,0} - {3'b000,truncate(cap.bounds.baseBits)};
81+
// equivalent to (repBoundBits - cap.bounds.baseBits - 1):
82+
Bit#(MW) toBoundsM1_A = {3'b110,~truncate(cap.bounds.baseBits)};
83+
/*
84+
XXX not sure if we still care about that
85+
if (toBoundsM1_A != (toBounds_A-1)) $display("error %x", toBounds_A[15:13]);
86+
*/
87+
// When the setOffset flag is not set, we need to use the temporary fields
88+
// with the upper bits of the representable bounds
89+
Bit#(MW) repBoundBits = {tf.repBoundTopBits,0};
90+
Bit#(MW) toBounds_B = repBoundBits - cap.addrBits;
91+
Bit#(MW) toBoundsM1_B = repBoundBits + ~cap.addrBits;
92+
// Select the appropriate toBounds value
93+
Bit#(MW) toBounds = setOffset ? toBounds_A : toBounds_B;
94+
Bit#(MW) toBoundsM1 = setOffset ? toBoundsM1_A : toBoundsM1_B;
95+
Bool addrAtRepBound = !setOffset && (repBoundBits == cap.addrBits);
96+
97+
// Implement the inLimit test
98+
Bool inLimits = False;
99+
if (posInc) begin
100+
// For a positive or null increment
101+
// SetOffset is offsetting against base, which has 0 in the lower bits, so
102+
// we don't need to be conservative.
103+
inLimits = setOffset ? offsetBits <= toBoundsM1
104+
: offsetBits < toBoundsM1;
105+
end else begin
106+
// For a negative increment
107+
inLimits = (offsetBits >= toBounds) && !addrAtRepBound;
108+
end
109+
110+
// Complete representable bounds check
111+
// -----------------------------------
112+
Bool inBounds = (inRange && inLimits) || (e >= (resetExp - 2));
113+
114+
// Updating the return capability
115+
// ------------------------------
116+
if (setOffset) begin
117+
// Get the base and add the offsetAddr. This could be slow, but seems to
118+
// pass timing.
119+
ret.address = getBotFat(cap,tf) + offsetAddr;
120+
// Work out the slice of the address we are interested in using MW-bit
121+
// arithmetics.
122+
Bit#(MW) newAddrBits = cap.bounds.baseBits + offsetBits;
123+
// Ensure the bits of the address slice past the top of the address space
124+
// are zero
125+
Bit#(2) mask = (e == resetExp) ? 2'b00 : (e == resetExp-1) ? 2'b01 : 2'b11;
126+
ret.addrBits = {mask, ~0} & newAddrBits;
127+
end else begin
128+
// In the incOffset case, the 'pointer' argument already contains the new
129+
// address
130+
ret.address = pointer;
131+
ret.addrBits = truncate(ret.address >> e);
132+
end
133+
// Nullify the capability if the representable bounds check has failed
134+
if (!inBounds) ret.isCapability = False;
135+
136+
// return updated / invalid capability
137+
return VnD {v: inBounds, d: ret};
138+
endfunction

‎cheri_concentrate_listings/conc_setAddress.bsv‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
function VnD#(CapFat) setAddress(CapFat cap, CapAddr address, TempFields tf);
2+
CapFat ret = setCapPointer(cap, address);
3+
Exp e = cap.bounds.exp;
4+
// Calculate what the difference in the upper bits of the new and original addresses must be if
5+
// the new address is within representable bounds.
6+
Bool newAddrHi = truncateLSB(ret.addrBits) < tf.repBoundTopBits;
7+
Bit#(TSub#(CapAddrW,MW)) deltaAddrHi = signExtend({1'b0,pack(newAddrHi)} - {1'b0,pack(tf.addrHi)}) << e;
8+
// Calculate the actual difference between the upper bits of the new address and the original address.
9+
Bit#(TSub#(CapAddrW,MW)) mask = -1 << e;
10+
Bit#(TSub#(CapAddrW,MW)) deltaAddrUpper = (truncateLSB(address)&mask) - (truncateLSB(cap.address)&mask);
11+
Bool inRepBounds = deltaAddrHi == deltaAddrUpper;
12+
if (!inRepBounds) ret.isCapability = False;
13+
return VnD {v: inRepBounds, d: ret};
14+
endfunction

‎cheri_concentrate_listings/conc_setBoundsFat.bsv‎

Lines changed: 135 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,135 @@
1+
function SetBoundsReturn#(CapFat, CapAddrW) setBoundsFat(CapFat cap, Address lengthFull);
2+
CapFat ret = cap;
3+
// Find new exponent by finding the index of the most significant bit of the
4+
// length, or counting leading zeros in the high bits of the length, and
5+
// substracting them to the CapAddr width (taking away the bottom MW-1 bits:
6+
// trim (MW-1) bits from the bottom of length since any length with a
7+
// significance that small will yield an exponent of zero).
8+
CapAddr length = truncate(lengthFull);
9+
Bit#(TSub#(CapAddrW,TSub#(MW,1))) lengthMSBs = truncateLSB(length);
10+
Exp zeros = zeroExtend(countZerosMSB(lengthMSBs));
11+
// Adjust resetExp by one since it's scale reaches 1-bit greater than a
12+
// 64-bit length can express.
13+
Bool maxZero = (zeros==(resetExp-1));
14+
Bool intExp = !(maxZero && length[fromInteger(valueOf(TSub#(MW,2)))]==1'b0);
15+
// Do this without subtraction
16+
//fromInteger(valueof(TSub#(SizeOf#(Address),TSub#(MW,1)))) - zeros;
17+
Exp e = (resetExp-1) - zeros;
18+
// Derive new base bits by extracting MW bits from the capability address
19+
// starting at the new exponent's position.
20+
CapAddrPlus2 base = {2'b0, cap.address};
21+
Bit#(TAdd#(MW,1)) newBaseBits = truncate(base>>e);
22+
23+
// Derive new top bits by extracting MW bits from the capability address +
24+
// requested length, starting at the new exponent's position, and rounding up
25+
// if significant bits are lost in the process.
26+
CapAddrPlus2 len = {2'b0, length};
27+
CapAddrPlus2 top = base + len;
28+
29+
// Create a mask with all bits set below the MSB of length and then masking
30+
// all bits below the mantissa bits.
31+
CapAddrPlus2 lmask = smearMSBRight(len);
32+
// The shift amount required to put the most significant set bit of the len
33+
// just above the bottom HalfExpW bits that are taken by the exp.
34+
Integer shiftAmount = valueOf(TSub#(TSub#(MW,2),HalfExpW));
35+
36+
// Calculate all values associated with E=e (e not rounding up)
37+
// Round up considering the stolen HalfExpW exponent bits if required
38+
Bit#(TAdd#(MW,1)) newTopBits = truncate(top>>e);
39+
// Check if non-zero bits were lost in the low bits of top, either in the 'e'
40+
// shifted out bits or in the HalfExpW bits stolen for the exponent
41+
// Shift by MW-1 to move MSB of mask just below the mantissa, then up
42+
// HalfExpW more to take in the bits that will be lost for the exponent when
43+
// it is non-zero.
44+
CapAddrPlus2 lmaskLor = lmask>>fromInteger(shiftAmount+1);
45+
CapAddrPlus2 lmaskLo = lmask>>fromInteger(shiftAmount);
46+
// For the len, we're not actually losing significance since we're not
47+
// storing it, we just want to know if any low bits are non-zero so that we
48+
// will know if it will cause the total length to round up.
49+
Bool lostSignificantLen = (len&lmaskLor)!=0 && intExp;
50+
Bool lostSignificantTop = (top&lmaskLor)!=0 && intExp;
51+
// Check if non-zero bits were lost in the low bits of base, either in the
52+
// 'e' shifted out bits or in the HalfExpW bits stolen for the exponent
53+
Bool lostSignificantBase = (base&lmaskLor)!=0 && intExp;
54+
55+
// Calculate all values associated with E=e+1 (e rounding up due to msb of L
56+
// increasing by 1) This value is just to avoid adding later.
57+
Bit#(MW) newTopBitsHigher = truncateLSB(newTopBits);
58+
// Check if non-zero bits were lost in the low bits of top, either in the 'e'
59+
// shifted out bits or in the HalfExpW bits stolen for the exponent Shift by
60+
// MW-1 to move MSB of mask just below the mantissa, then up HalfExpW more to
61+
// take in the bits that will be lost for the exponent when it is non-zero.
62+
Bool lostSignificantTopHigher = (top&lmaskLo)!=0 && intExp;
63+
// Check if non-zero bits were lost in the low bits of base, either in the
64+
// 'e' shifted out bits or in the HalfExpW bits stolen for the exponent
65+
Bool lostSignificantBaseHigher = (base&lmaskLo)!=0 && intExp;
66+
// If either base or top lost significant bits and we wanted an exact
67+
// setBounds, void the return capability
68+
69+
// We need to round up Exp if the msb of length will increase.
70+
// We can check how much the length will increase without looking at the
71+
// result of adding the length to the base. We do this by adding the lower
72+
// bits of the length to the base and then comparing both halves (above and
73+
// below the mask) to zero. Either side that is non-zero indicates an extra
74+
// "1" that will be added to the "mantissa" bits of the length, potentially
75+
// causing overflow. Finally check how close the requested length is to
76+
// overflow, and test in relation to how much the length will increase.
77+
CapAddrPlus2 topLo = (lmaskLor & len) + (lmaskLor & base);
78+
CapAddrPlus2 mwLsbMask = lmaskLor ^ lmaskLo;
79+
// If the first bit of the mantissa of the top is not the sum of the
80+
// corrosponding bits of base and length, there was a carry in.
81+
Bool lengthCarryIn = (mwLsbMask & top) != ((mwLsbMask & base)^(mwLsbMask & len));
82+
Bool lengthRoundUp = lostSignificantTop;
83+
Bool lengthIsMax = (len & (~lmaskLor)) == (lmask ^ lmaskLor);
84+
Bool lengthIsMaxLessOne = (len & (~lmaskLor)) == (lmask ^ lmaskLo);
85+
86+
Bool lengthOverflow = False;
87+
if (lengthIsMax && (lengthCarryIn || lengthRoundUp)) lengthOverflow = True;
88+
if (lengthIsMaxLessOne && lengthCarryIn && lengthRoundUp) lengthOverflow = True;
89+
90+
if(lengthOverflow && intExp) begin
91+
e = e+1;
92+
ret.bounds.topBits = lostSignificantTopHigher ? newTopBitsHigher + 'b1000
93+
: newTopBitsHigher;
94+
ret.bounds.baseBits = truncateLSB(newBaseBits);
95+
end else begin
96+
ret.bounds.topBits = lostSignificantTop ? truncate(newTopBits + 'b1000)
97+
: truncate(newTopBits);
98+
ret.bounds.baseBits = truncate(newBaseBits);
99+
end
100+
Bool exact = !(lostSignificantBase || lostSignificantTop);
101+
102+
ret.bounds.exp = e;
103+
// Update the addrBits fields
104+
ret.addrBits = ret.bounds.baseBits;
105+
// Derive new format from newly computed exponent value, and round top up if
106+
// necessary
107+
if (!intExp) begin // If we have an Exp of 0 and no implied MSB of L.
108+
ret.format = Exp0;
109+
end else begin
110+
ret.format = EmbeddedExp;
111+
Bit#(HalfExpW) botZeroes = 0;
112+
ret.bounds.baseBits = {truncateLSB(ret.bounds.baseBits), botZeroes};
113+
ret.bounds.topBits = {truncateLSB(ret.bounds.topBits), botZeroes};
114+
end
115+
116+
// Begin calculate newLength in case this is a request just for a
117+
// representable length:
118+
CapAddrPlus2 newLength = {2'b0, length};
119+
CapAddrPlus2 baseMask = -1; // Override the result from the previous line if
120+
// we represent everything.
121+
if (intExp) begin
122+
CapAddrPlus2 oneInLsb = (lmask ^ (lmask>>1)) >> shiftAmount;
123+
CapAddrPlus2 newLengthRounded = newLength + oneInLsb;
124+
newLength = (newLength & (~lmaskLor));
125+
newLengthRounded = (newLengthRounded & (~lmaskLor));
126+
if (lostSignificantLen) newLength = newLengthRounded;
127+
baseMask = (lengthIsMax && lostSignificantTop) ? ~lmaskLo : ~lmaskLor;
128+
end
129+
130+
// Return derived capability
131+
return SetBoundsReturn { cap: ret
132+
, exact: exact
133+
, length: truncate(newLength)
134+
, mask: truncate(baseMask) };
135+
endfunction

0 commit comments

Comments
 (0)