Simulating memory with Datalog (big/little endian reads/writes of bytes)

memory.dl

// Here's one way to use Souffle datalog to simulate
// reading bytes from memory and assembling a value
// out of them (big/little endian-wise).

// Working with string representations of binary numbers
// in Souffle is somewhat tedious, so I'm going to do
// this by storing bytes as numbers. Then, when I pull
// out the bytes and assemble them into a value, I just
// need to calculate the number from that sequence of
// integer byte values.

// Here's the formula for doing that calculation.

// Let b0, b1, b2, b3 each be a bitvector of width w, 
// taken as integers (not binary numbers). In other words,
// each of b0, b1, b2, and b3 are "bytes," but represented
// as a number.

// Next, suppose that b0 is the LSB, and b3 is the MSB.
// In little endian, that means: b3|b2|b1|b0.
// In big endian, that means: b0|b1|b2|b3.

// Let i be 0, 1, 2, or 3 (the index of the byte).

// Then we calculate the value of each byte like this:

// ((((2^w)^i) - 1) * bi) + bi.

// After calculating that for each byte, just add 'em up.

// Conceptually, that calculation works like this.
// 
// - 2^w tells us how high we can count in binary with words
//   that are w-bits wide. E.g., if we have a 3-bit wide word,
//   we can count up to 8, because 2^3 is 8. With 8-bit words,
//   we can count up to 256, because 2^8 is 256.
//
// - At each index i, we start counting from (2^w)^i. This is
//   because in the first word slot (index 0), we are starting
//   at 0, which is what (2^w)^0 comes to. At the second word slot
//   (index 1), we are starting at (2^w), which is what (2^w)^1
//   comes to. In the third slot (index 2), we start counting at
//   (2^w) * (2^w), which is (2^w)^2). In the fourth slot (index
//   3), we start counting at (2^w) * (2^w) * (2^w), which is
//   (2^w)^3).
//
// - But since we start counting at 0, we need to subtract 1,
//   hence we have ((2^w)^i) - 1. This gives us the last number
//   that we counted up to, using all the bits in the previous
//   slots.
//
// - Next, we need to compute how high above that starting number
//   the number in our current slot is. For that, we multiply
//   our starting number by the number in our current slot.
//   For instance, if our starting number is 3, and we have
//   a 2 in our current slot, then we need to do 3 * 2, because
//   each number in our current slot cycles through 3 other
//   numbers in the slot below, like how every hour adds 60
//   minutes because each hour has to cycle through another
//   60 minutes. This effectively gets us up to the 12 o'clock
//   spot, the right number of rotations around.
//
// - Finally, we add in the number in our current slot. This is like
//   turning the minute hand from the 12 o'clock spot up to the
//   current minutes.

.type addr <: number
.type val <: number
.type sz <: number
.type endn <: symbol

// The user can say what the endianness is.
.decl endianness(endian:endn)
.decl littleEndianTag(endian:endn)
.decl bigEndianTag(endian:endn)

// Just to check that the user put in the right thing.
littleEndianTag("little").
bigEndianTag("big").

// The user can tell us the size of the bytes.
.decl byteSize(bits:sz)

// The user can tell us the size of addresses.
.decl addressSize(bits:sz)

// The user can then tell us which values are stored
// at each address.
.decl data(addr:addr,val:val)

// As a safety precaution, we'll wrap-around any numbers
// the user tries to put at an address that's too big
// to fit in the byte-sized slot.
.decl _data(addr:addr,val:val)
_data(A,V % W) :- data(A,V),byteSize(W), V >= (2^W).
_data(A,V) :- data(A,V),byteSize(W),V < (2^W).

// This builds up the value, one byte at a time,
// with the little endian ordering.
// Note that this is lazy. If there is no `doRead(_,_)`,
// then it won't compute anything.
.decl buildValLittleEnd(start:addr,offset:number,val:val)
buildValLittleEnd(A,0,V) :- _data(A,V),doRead(A,_).
buildValLittleEnd(A,N+1,(((((2^W)^(N+1))-1)*V)+V)+Z) :-
  byteSize(W),buildValLittleEnd(A,N,Z),
  _data(A+(N+1),V),doRead(A,B),N < (B-1).

// Ditto, but with the big endian ordering.
.decl buildValBigEnd(start:addr,offset:number,val:val)
buildValBigEnd(A,0,V) :- _data(A+B,V),doRead(A,B).
buildValBigEnd(A,N+1,(((((2^W)^(N+1))-1)*V)+V)+Z) :-
  byteSize(W),buildValBigEnd(A,N,Z),
  _data((A+B)-(N+1),V),doRead(A,B),N < (B-1).

// If the user wants to compute an actual read, they
// need to use this predicate to say which address
// they want to start reading from and how many bytes
// they want to read. Think of this as a command
// to actually read the specifed number of bytes and
// get the value from them.
.decl doRead(start:addr,bytes:number)

// This reports the value computed by any `doRead` commands.
.decl read(start:addr,bytes:number,val:val)
read(A,B,Z) :-
  endianness(E),littleEndianTag(E),
  buildValLittleEnd(A,B-1,Z),doRead(A,B).
read(A,B,Z) :-
  endianness("big"),bigEndianTag(E),
  buildValBigEnd(A,B-1,Z),doRead(A,B).


// USER-PROVIDED INFORMATION

// Let's say the machine is little endianed,
// with 32-bit addresses, and bytes that are only
// 2-bits wide!
endianness("little").
addressSize(32).
byteSize(2).

// Let's say that at addresses 1, 2, and 3, respectively
// are the following bytes.
data(1,2). // store 2 at address 1
data(2,5). // store 5 at address 2
data(3,1). // store 1 at address 3
// Note that the user attempts to put 5 into address 2),
// but the number 5 won't fit in a 2-bit slot. This is
// okay, because the underlying `_data` predicate will
// chop it so that 1 is actually the number that gets
// stored at address 2.sy

// Issue the command to read 3 bytes, starting at address 1.
doRead(1,3).

.output buildValLittleEnd
.output buildValBigEnd

.output _data
.output read

read-and-write.dl

// =========================================================
// Byte-addressed memory - reads
// =========================================================

.decl endianness(endian:endn)
.decl littleEndianTag(endian:endn)
.decl bigEndianTag(endian:endn)

littleEndianTag("little").
bigEndianTag("big").

.decl byteSize(bits:sz)

.decl addressSize(bits:sz)

.decl data(addr:addr,val:val)

.decl _data(addr:addr,val:val)
_data(A,V % W) :- data(A,V),byteSize(W), V >= (2^W).
_data(A,V) :- data(A,V),byteSize(W),V < (2^W).

.decl buildReadValLittleEnd(start:addr,offset:number,val:val)
buildReadValLittleEnd(A,0,V) :-
  _data(A,V),doRead(A,_),
  endianness(E),littleEndianTag(E).
buildReadValLittleEnd(A,N+1,(((((2^W)^(N+1))-1)*V)+V)+Z) :-
  byteSize(W),buildReadValLittleEnd(A,N,Z),
  _data(A+(N+1),V),doRead(A,B),N < (B-1).

.decl buildReadValBigEnd(start:addr,offset:number,val:val)
buildReadValBigEnd(A,0,V) :-
  _data(A+(B-1),V),doRead(A,B),
  endianness(E),bigEndianTag(E).
buildReadValBigEnd(A,N+1,(((((2^W)^(N+1))-1)*V)+V)+Z) :-
  byteSize(W),buildReadValBigEnd(A,N,Z),
  _data((A+(B-1))-(N+1),V),doRead(A,B),N < (B-1).

.decl doRead(start:addr,bytes:number)

.decl read(addr:addr,bytes:number,val:val)
read(A,B,Z) :-
  endianness(E),littleEndianTag(E),
  buildReadValLittleEnd(A,B-1,Z),doRead(A,B).
read(A,B,Z) :-
  endianness(E),bigEndianTag(E),
  buildReadValBigEnd(A,B-1,Z),doRead(A,B).


// =========================================================
// Writes
// =========================================================

.decl doWrite(addr:addr,val:val)

.decl buildBitsToWrite(base:number,step:number,next:number,val:val)
buildBitsToWrite(B,0,B / 2,B % 2) :- doWrite(_,B).
buildBitsToWrite(B,N+1,Z / 2,Z % 2) :-
  buildBitsToWrite(B,N,Z,_),doWrite(_,B),Z >= 1.


.decl buildBytesToWrite(base:number,place:number,val:val)
.decl bytesToWrite(base:number,place:number,val:val)

buildBytesToWrite(B,0,V) :-
  buildBitsToWrite(B,0,_,Z),V=Z*(2^0).

buildBytesToWrite(B,N+1,V) :-
  buildBytesToWrite(B,N,_),
  byteSize(L),
  P=(N+1) % L,
  P = 0,
  buildBitsToWrite(B,N+1,_,Z),
  V = (Z*(2^P)).

buildBytesToWrite(B,N+1,V) :-
  buildBytesToWrite(B,N,V1),
  byteSize(L),
  P=(N+1) % L,
  P != 0, P != (L-1),
  buildBitsToWrite(B,N+1,_,Z),
  V = V1 + (Z*(2^P)).

bytesToWrite(B,(N+1) / L,V),
buildBytesToWrite(B,N+1,V) :-
  buildBytesToWrite(B,N,V1),
  byteSize(L),
  P=(N+1) % L,
  P != 0, P = (L-1),
  buildBitsToWrite(B,N+1,_,Z),
  V = V1 + (Z*(2^P)).


.decl writeByteLittleEnd(orig:val,addr:addr,offset:number,val:val)

data(A,V),
writeByteLittleEnd(Z,A,0,V) :-
  doWrite(A,Z),bytesToWrite(Z,0,V),
  endianness(E),littleEndianTag(E).

data(A+N+1,V),
writeByteLittleEnd(Z,A,N+1,V) :-
  writeByteLittleEnd(Z,A,N,_),
  bytesToWrite(Z,N+1,V).


.decl writeByteBigEnd(orig:val,addr:addr,offset:number,val:val)

data(A,V),
writeByteBigEnd(Z,A,0,V) :-
  doWrite(A,Z),
  _ = max J : bytesToWrite(Z,J,V),
  endianness(E),bigEndianTag(E).

data(A+N+1,V),
writeByteBigEnd(Z,A,N+1,V) :-
  writeByteBigEnd(Z,A,N,_),
  I = max J : bytesToWrite(Z,J,_),
  bytesToWrite(Z,I-(N+1),V).

.decl write(addr:addr,bytes:number,val:val)
write(A,N+1,V) :-
  doWrite(A,V),endianness(E),bigEndianTag(E),
  N = max I : { writeByteBigEnd(V,A,I,_) }.
write(A,N+1,V) :-
  doWrite(A,V),endianness(E),littleEndianTag(E),
  N = max I : { writeByteLittleEnd(V,A,I,_) }.


/* Example of use

endianness("big").
byteSize(3).
doWrite(3,256).
doRead(3,3).

.output endianness
.output doWrite
.output buildBitsToWrite
.output buildBytesToWrite
.output bytesToWrite

.output writeByteLittleEnd
.output writeByteBigEnd
.output data
.output _data
.output write

.output buildReadValLittleEnd
.output buildReadValBigEnd
.output read
*/