Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions interface.sail
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,18 @@ function create_writeAccessDescriptor() -> AccessDescriptor = {
accdesc.write = true;
accdesc
}
function create_atomicReadAccessDescriptor() -> AccessDescriptor = {
var accdesc = create_readAccessDescriptor();
accdesc.atomicop = true;
accdesc.standalone = false;
accdesc
}
function create_atomicWriteAccessDescriptor() -> AccessDescriptor = {
var accdesc = create_writeAccessDescriptor();
accdesc.atomicop = true;
accdesc.standalone = false;
accdesc
}

// Memory access generated by an explicit instruction
function mem_acc_is_explicit (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_RW
Expand Down
49 changes: 29 additions & 20 deletions operands.sail
Original file line number Diff line number Diff line change
Expand Up @@ -29,10 +29,9 @@ union rmi_operand = {
/* permitted word sizes */
type word_size = {8,16,32,64}

/* read immediate value from variable bit-extended to 64 bits */
val read_imm: forall 'm, 'm in {8, 16, 32, 64}. (int('m), imm) -> bits('m)
/* read immediate value from operand */
val read_imm: forall 'wsize, 'wsize in {8, 16, 32, 64}. (int('wsize), imm) -> bits('wsize)
function read_imm(wsize, imm) = {
// If imm size is smaller than word size, then sign-extend the imm before returning it
match imm {
IMM8(value) => {
assert(wsize == 8, "Immediate value size is 8 bits, but word size is not.");
Expand All @@ -43,6 +42,7 @@ function read_imm(wsize, imm) = {
value[15 .. 0]
},
IMM32(value) => {
// If imm size is smaller than word size, then sign-extend the imm before returning it
assert(wsize >= 32, "Immediate value size is 32 bits, but word size is not 32 or 64 bits.");
sail_sign_extend(value[31 .. 0], wsize)
},
Expand All @@ -54,41 +54,50 @@ function read_imm(wsize, imm) = {
}

/* read register or memory operand */
val read_rm_operand: forall 'm, 'm in {8, 16, 32, 64}. (int('m), rm_operand) -> bits('m)
function read_rm_operand(wsize, operand: rm_operand) = {
let wsize_bytes = wsize / 8;
assert('m == wsize_bytes * 8); // required for type-checking
val read_rm_operand: forall 'wsize, 'wsize in {8, 16, 32, 64}. (bool, int('wsize), rm_operand) -> bits('wsize)
function read_rm_operand(lock, wsize, operand) = {
match operand {
rm_REG(reg_index) => read_GPR(wsize, reg_index),
rm_MEM(mem_addr) => read_memory(wsize_bytes, mem_addr, create_readAccessDescriptor()),
rm_MEM(mem_addr) => {
let acc_desc = if lock then create_atomicReadAccessDescriptor() else create_readAccessDescriptor();
let wsize_bytes = wsize / 8;
assert(wsize == wsize_bytes * 8); // required for type-checking
read_memory(wsize_bytes, mem_addr, acc_desc)
},
}
}

/* read register / memory / immediate operand */
val read_rmi_operand: forall 'm, 'm in {8, 16, 32, 64}. (int('m), rmi_operand) -> bits('m)
function read_rmi_operand(wsize, operand: rmi_operand) = {
let wsize_bytes = wsize / 8;
assert('m == wsize_bytes * 8); // required for type-checking
val read_rmi_operand: forall 'wsize, 'wsize in {8, 16, 32, 64}. (bool, int('wsize), rmi_operand) -> bits('wsize)
function read_rmi_operand(lock, wsize, operand) = {
match operand {
rmi_IMM(imm) => read_imm(wsize, imm),
rmi_REG(reg_index) => read_GPR(wsize, reg_index),
rmi_MEM(mem_addr) => read_memory(wsize_bytes, mem_addr, create_readAccessDescriptor()),
rmi_MEM(mem_addr) => {
let acc_desc = if lock then create_atomicReadAccessDescriptor() else create_readAccessDescriptor();
let wsize_bytes = wsize / 8;
assert(wsize == wsize_bytes * 8); // required for type-checking
read_memory(wsize_bytes, mem_addr, acc_desc)
},
}
}

/* overloaded function to read any operand type present in the ast */
overload read_operand = {read_rm_operand, read_rmi_operand, read_imm, read_GPR}
overload read_operand = {read_rm_operand, read_rmi_operand}

/* write to reg or mem location */
val write_rm_operand: forall 'm, 'm in {8, 16, 32, 64}. (int('m), rm_operand, bits('m)) -> unit
function write_rm_operand(wsize, operand: rm_operand, value) = {
let wsize_bytes = wsize / 8;
assert('m == wsize_bytes * 8); // required for type-checking
val write_rm_operand: forall 'wsize, 'wsize in {8, 16, 32, 64}. (bool, int('wsize), rm_operand, bits('wsize)) -> unit
function write_rm_operand(lock, wsize, operand, value) = {
match operand {
rm_REG(reg_index) => write_GPR(wsize, reg_index, value),
rm_MEM(mem_addr) => write_memory(wsize_bytes, mem_addr, value, create_writeAccessDescriptor()),
rm_MEM(mem_addr) => {
let acc_desc = if lock then create_atomicWriteAccessDescriptor() else create_writeAccessDescriptor();
let wsize_bytes = wsize / 8;
assert(wsize == wsize_bytes * 8); // required for type-checking
write_memory(wsize_bytes, mem_addr, value, acc_desc)
},
}
}

/* overloaded function to write to any register or memory type */
overload write_operand = {write_rm_operand, write_GPR}
overload write_operand = {write_rm_operand}
52 changes: 46 additions & 6 deletions tests.sail
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
function write_then_read_mem() -> unit = {
// write test
let mem_addr = 0x0000_0000_0000_0007;
let value = 0x0000_0000_0000_0004;
write_memory(8, mem_addr, value, create_writeAccessDescriptor());
// read test
let read_value: bits(64) = read_memory(8, mem_addr, create_readAccessDescriptor());
assert(read_value == value, "Writing then reading from the same memory address was inconsistent");
}
Expand All @@ -10,22 +12,25 @@ function mov_reg_to_mem() -> unit = {
let wsize = 16;
write_GPR(wsize, 8, get_slice_int(wsize, -236, 0));
execute(MOV(wsize, rm_MEM(0xFFFF_FFFF_FFFF_FFF8), rmi_REG(8)));
assert(signed(read_operand(wsize, rm_MEM(0xFFFF_FFFF_FFFF_FFF8))) == -236, "MOV(mem, reg) gave an incorrect answer")
assert(signed(read_operand(false, wsize, rm_MEM(0xFFFF_FFFF_FFFF_FFF8))) == -236, "MOV(mem, reg) gave an incorrect answer")
}

function xor_2_numbers() -> unit = {
let lock = false;
let wsize1 = 64;
let wsize2 = 32;
write_GPR(wsize1, 8, 0x0101_0101_0101_0101);
let imm_val = 0x0000_1111;
execute(XOR(wsize1, rm_REG(8), rmi_IMM(IMM32(imm_val))));
execute(XOR(lock, wsize1, rm_REG(8), rmi_IMM(IMM32(imm_val))));
assert(read_GPR(wsize1, 8) == 0x0101_0101_0101_1010, "XOR(reg, imm) gave an incorrect answer")
}

function cmp_jns() -> unit = {
// cmp test
write_GPR(32, 0, 0x4444_4444);
execute(CMP(32, rm_REG(0), rmi_IMM(IMM32(0x5555_5555))));
assert(RFLAGS[SF] == 1, "CMP does not set sign flag correctly");
// jns test
let current_RIP = RIP;
execute(JNS(0x34));
assert(RIP == current_RIP, "JNS performs a jump when the sign is set");
Expand All @@ -35,31 +40,35 @@ function cmp_jns() -> unit = {
}

function push_pop() -> unit = {
let wsize1 = 16;
let RSP1 = RSP;
// push test
let wsize1 = 16;
execute(PUSH(wsize1, rmi_IMM(IMM16(0xF0F0))));
assert(RSP + 8 == RSP1, "PUSH does not correctly change stack pointer");
assert(read_operand(64, rm_MEM(RSP)) == sail_sign_extend(0xF0F0, 64), "PUSH does not push the correct value to the top of the stack");
assert(read_operand(false, 64, rm_MEM(RSP)) == sail_sign_extend(0xF0F0, 64), "PUSH does not push the correct value to the top of the stack");
// pop test
execute(POP(64, rm_REG(15)));
assert(RSP == RSP1, "POP does not correctly change stack pointer");
assert(read_GPR(64, 15) == sail_sign_extend(0xF0F0, 64), "POP does not put the correct value in the destination")
}

function add_2_numbers() -> unit = {
let lock = false;
let wsize1 = 64;
let wsize2 = 32;
write_GPR(wsize1, 8, get_slice_int(wsize1, 30, 0));
let imm_val = get_slice_int(wsize2, -250, 0);
execute(ADD(wsize1, rm_REG(8), rmi_IMM(IMM32(imm_val))));
execute(ADD(lock, wsize1, rm_REG(8), rmi_IMM(IMM32(imm_val))));
assert(signed(read_GPR(wsize1, 8)) == 30 - 250, "ADD(reg, imm) gave an incorrect answer")
}

function subtract_2_numbers() -> unit = {
let lock = false;
let wsize1 = 64;
let wsize2 = 32;
write_GPR(wsize1, 8, get_slice_int(wsize1, 30, 0));
let imm_val = get_slice_int(wsize2, -250, 0);
execute(SUB(wsize1, rm_REG(8), rmi_IMM(IMM32(imm_val))));
execute(SUB(lock, wsize1, rm_REG(8), rmi_IMM(IMM32(imm_val))));
assert(signed(read_GPR(wsize1, 8)) == 30 - (- 250), "SUB(reg, imm) gave an incorrect answer");
}

Expand All @@ -71,6 +80,36 @@ function multiply_2_numbers() -> unit = {
assert(signed(read_GPR(wsize, 8)) == 30 * (- 250), "IMUL(reg, reg) gave an incorrect answer");
}

function call_leave_ret() -> unit = {
// call test
RSP = 0x0000_0000_0000_ABC8;
RIP = 0xFFFF_0000_0000_0000;
let original_RIP = RIP;
let original_RSP = RSP;
execute(CALL(0xFEFE_FEFE));
assert(RSP == 0x0000_0000_0000_ABC0, "CALL instruction does not decrement RSP correctly (when pushing a value to the stack)");
assert(read_operand(false, 64, rm_MEM(RSP)) == original_RIP, "CALL instruction puts incorrect value at the top of the stack");
assert(RIP == add_bits(original_RIP, sail_sign_extend(0xFEFE_FEFE, 64)), "CALL instruction does not change RIP correctly");

// "push" and "mov" instructions used to test "leave" and "ret"
let old_RBP = RBP;
let old_RSP = RSP;
// push RBP value to the stack
execute(PUSH(64, rmi_REG(5))); // 5 is the reg_index for RBP
// copy RSP value into RBP register
execute(MOV(64, rm_REG(5), rmi_REG(4))); // 4 is the reg_index for RSP, 5 for RBP

// leave test
execute(LEAVE());
assert(RSP == old_RSP, "LEAVE instruction does not increment RSP correctly (when popping from the stack)");
assert(RBP == old_RBP, "LEAVE instruction does not pop correct item from the stack into RBP");

// ret test
execute(RET());
assert(RSP == original_RSP, "RET instruction does not increment RSP correctly (when popping from the stack)");
assert(RIP == original_RIP, "RET instruction does not pop correct item from the stack into RIP");
}

function jmp() -> unit = {
let current_RIP = RIP;
execute(JMP(0xFF));
Expand All @@ -86,5 +125,6 @@ function main() : unit -> unit = {
add_2_numbers();
subtract_2_numbers();
multiply_2_numbers();
call_leave_ret();
jmp();
}
Loading