diff --git a/interface.sail b/interface.sail index beb34f7..fc2dc14 100644 --- a/interface.sail +++ b/interface.sail @@ -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 diff --git a/operands.sail b/operands.sail index 18262fb..41b37e4 100644 --- a/operands.sail +++ b/operands.sail @@ -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."); @@ -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) }, @@ -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} diff --git a/tests.sail b/tests.sail index 1141296..dc3a4ed 100644 --- a/tests.sail +++ b/tests.sail @@ -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"); } @@ -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"); @@ -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"); } @@ -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)); @@ -86,5 +125,6 @@ function main() : unit -> unit = { add_2_numbers(); subtract_2_numbers(); multiply_2_numbers(); + call_leave_ret(); jmp(); } diff --git a/tiny-x86.sail b/tiny-x86.sail index c7e444d..e3a2fc7 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -1,16 +1,16 @@ union ast = { - // if one of the types is a tuple with first element word_size, the tuple represents (word_size, dest, src), unless the instruction is CMP - // only implementing instructions where both dest and src have the same word size, or where src can be sign-extended to the target word size + // Structure of all possible executable instructions + // if a type contains 2 operands, the first operand is dest and the second is src, unless the instruction is CMP MOV: (word_size, rm_operand, rmi_operand), - XOR: (word_size, rm_operand, rmi_operand), + XOR: (bool, word_size, rm_operand, rmi_operand), SFENCE: unit, LFENCE: unit, MFENCE: unit, CMP: (word_size, rm_operand, rmi_operand), PUSH: (word_size, rmi_operand), // only allowing 64 bit operand POP: (word_size, rm_operand), - ADD: (word_size, rm_operand, rmi_operand), - SUB: (word_size, rm_operand, rmi_operand), + ADD: (bool, word_size, rm_operand, rmi_operand), + SUB: (bool, word_size, rm_operand, rmi_operand), IMUL: (word_size, reg_index, rm_operand), // IMUL with only 2 arguments (dest and src) CALL: imm32, LEAVE: unit, @@ -39,12 +39,13 @@ function clause execute(MOV(wsize, dest, src)) = { (rm_MEM(_), rmi_IMM(IMM64(_))) => fail("MOV operation cannot be executed on dest = mem64 and src = imm64"), (_,_) => () }; + // execute MOV instruction - let val_to_write = read_operand(wsize, src); - write_operand(wsize, dest, val_to_write) + let val_to_write = read_operand(false, wsize, src); + write_operand(false, wsize, dest, val_to_write) } -function clause execute(XOR(wsize, dest, src)) = { +function clause execute(XOR(lock, wsize, dest, src)) = { // XOR cannot occur between dest = memory location and src = memory location fail_if_two_mem_operands(dest, src, "XOR"); // For operation XOR, src = imm64 is not a valid operand @@ -52,11 +53,17 @@ function clause execute(XOR(wsize, dest, src)) = { rmi_IMM(IMM64(_)) => fail("For operation XOR, src = imm64 is not a valid operand"), _ => () }; + // XOR is not valid with lock = true if dest is a register location + match dest { + rm_REG(_) if lock => fail("undefined opcode exception (#UD): LOCK prefix cannot be applied to dest = reg"), + _ => () + }; + // execute XOR instruction - let operand1 = read_operand(wsize, dest); - let operand2 = read_operand(wsize, src); - let result = xor_vec(operand1, operand2); - write_operand(wsize, dest, result); + let dest_val = read_operand(lock, wsize, dest); + let src_val = read_operand(false, wsize, src); + let result = xor_vec(dest_val, src_val); + write_operand(lock, wsize, dest, result); /* change value of status flags */ // clear overflow and carry flag @@ -98,8 +105,8 @@ function clause execute(CMP(wsize, first, second)) = { }; // execute CMP instruction - let first_val = read_operand(wsize, first); - let second_val = read_operand(wsize, second); + let first_val = read_operand(false, wsize, first); + let second_val = read_operand(false, wsize, second); let result = sub_bits(first_val, second_val); /* change value of status flags. Equivalent to the changes made on executing the SUB instruction. */ @@ -120,20 +127,20 @@ function clause execute(CMP(wsize, first, second)) = { function clause execute(PUSH(wsize, src)) = { // PUSH instruction does not allow src = imm64, reg8 or mem8 match src { - rmi_IMM(_) if wsize == 64 => fail("Operand for PUSH operation not supported"), - rmi_REG(_) if wsize == 8 => fail("Operand for PUSH operation not supported"), - rmi_MEM(_) if wsize == 8 => fail("Operand for PUSH operation not supported"), + rmi_IMM(_) if wsize == 64 => fail("Operand for PUSH operation not allowed"), + rmi_REG(_) if wsize == 8 => fail("Operand for PUSH operation not allowed"), + rmi_MEM(_) if wsize == 8 => fail("Operand for PUSH operation not allowed"), _ => () }; // If the source operand is an immediate of size less than the operand size, then sign-extend the value // default operand size is 8 bytes = 64 bits - let src_val = sail_sign_extend(read_operand(wsize, src), 64); + let src_val = sail_sign_extend(read_operand(false, wsize, src), 64); // subtract 8 from RSP to point to the new top of the stack RSP = sub_bits(RSP, sail_zero_extend(0x8, 64)); // push the new item to the top of the stack let dest_address = rm_MEM(RSP); - write_operand(64, dest_address, src_val) + write_operand(false, 64, dest_address, src_val) } function clause execute(POP(wsize, dest)) = { @@ -143,13 +150,13 @@ function clause execute(POP(wsize, dest)) = { if wsize == 16 then fail("dest size for POP operation not implemented in this model"); // pop the value at the top of the stack to dest - let popped_val = read_operand(64, rm_MEM(RSP)); - write_operand(64, dest, popped_val); + let popped_val = read_operand(false, 64, rm_MEM(RSP)); + write_operand(false, 64, dest, popped_val); // increment stack pointer to free the popped stack space RSP = RSP + 8; } -function clause execute(ADD(wsize, dest, src)) = { +function clause execute(ADD(lock, wsize, dest, src)) = { // ADD cannot occur between dest = memory location and src = memory location fail_if_two_mem_operands(dest, src, "ADD"); // For operation ADD, src = imm64 is not a valid operand @@ -157,12 +164,17 @@ function clause execute(ADD(wsize, dest, src)) = { rmi_IMM(IMM64(_)) => fail("For operation ADD, src = imm64 is not a valid operand"), _ => () }; + // ADD is not valid with prefix lock = true if dest is a register location + match dest { + rm_REG(_) if lock => fail("undefined opcode exception (#UD): LOCK prefix cannot be applied to dest = reg"), + _ => () + }; // execute ADD instruction - let dest_val = read_operand(wsize, dest); - let src_val = read_operand(wsize, src); + let dest_val = read_operand(lock, wsize, dest); + let src_val = read_operand(false, wsize, src); let result = add_bits(dest_val, src_val); - write_operand(wsize, dest, result); + write_operand(lock, wsize, dest, result); /* change value of status flags */ // sign flag = msb of result (0 = +ve, 1 = -ve) @@ -179,7 +191,7 @@ function clause execute(ADD(wsize, dest, src)) = { modify_parity_flag(result); } -function clause execute(SUB(wsize, dest, src)) = { +function clause execute(SUB(lock, wsize, dest, src)) = { // SUB cannot occur between dest = memory location and src = memory location fail_if_two_mem_operands(dest, src, "SUB"); // For operation SUB, src = imm64 is not a valid operand @@ -187,12 +199,17 @@ function clause execute(SUB(wsize, dest, src)) = { rmi_IMM(IMM64(_)) => fail("For operation SUB, src = imm64 is not a valid operand"), _ => () }; + // SUB is not valid with prefix lock = true if dest is a register location + match dest { + rm_REG(_) if lock => fail("undefined opcode exception (#UD): LOCK prefix cannot be applied to dest = reg"), + _ => () + }; // execute SUB instruction - let dest_val = read_operand(wsize, dest); - let src_val = read_operand(wsize, src); + let dest_val = read_operand(lock, wsize, dest); + let src_val = read_operand(false, wsize, src); let result = sub_bits(dest_val, src_val); - write_operand(wsize, dest, result); + write_operand(lock, wsize, dest, result); /* change value of status flags */ // sign flag = msb of result (0 = +ve, 1 = -ve) @@ -214,12 +231,12 @@ function clause execute(IMUL(wsize, dest, src)) = { if wsize == 8 then fail("8 bit operands are not valid for operation IMUL"); // execute IMUL - let dest_val = read_operand(wsize, dest); - let src_val = read_operand(wsize, src); + let dest_val = read_GPR(wsize, dest); + let src_val = read_operand(false, wsize, src); let result_int = signed(dest_val) * signed(src_val); let result_temp = get_slice_int(wsize * 2, result_int, 0); let result = result_temp[wsize - 1 .. 0]; - write_operand(wsize, dest, result); + write_GPR(wsize, dest, result); // set carry and overflow flag if the result overflows the allocated space (wsize bits), else clear if sail_sign_extend(result, wsize * 2) == result_temp then { @@ -234,12 +251,12 @@ function clause execute(IMUL(wsize, dest, src)) = { function clause execute(CALL(rel32)) = { /* execute near relative call */ - let displacement = read_operand(64, IMM32(rel32)); + let displacement = read_imm(64, IMM32(rel32)); // update stack pointer to point to the new top of the stack RSP = sub_bits(RSP, sail_zero_extend(0x8, 64)); // push current RIP to the stack let dest_address = rm_MEM(RSP); - write_operand(64, dest_address, RIP); + write_operand(false, 64, dest_address, RIP); // change RIP as specified by the instruction RIP = add_bits(RIP, displacement); } @@ -249,7 +266,7 @@ function clause execute(LEAVE()) = { to release the stack space allocated to the topmost stack frame */ RSP = RBP; // pop value into RBP - RBP = read_operand(64, rm_MEM(RSP)); + RBP = read_operand(false, 64, rm_MEM(RSP)); // increment stack pointer to free the popped stack space RSP = RSP + 8; } @@ -257,7 +274,7 @@ function clause execute(LEAVE()) = { function clause execute(RET()) = { /* execute near return */ // pop value into RIP - RIP = read_operand(64, rm_MEM(RSP)); + RIP = read_operand(false, 64, rm_MEM(RSP)); // increment stack pointer to free the popped stack space RSP = RSP + 8; } @@ -265,7 +282,7 @@ function clause execute(RET()) = { function clause execute(JMP(rel8)) = { /* execute jump short */ // add the operand to the current instruction pointer value - let displacement = sail_sign_extend(read_operand(8, IMM8(rel8)), 64); + let displacement = sail_sign_extend(read_imm(8, IMM8(rel8)), 64); RIP = RIP + displacement; } @@ -273,7 +290,7 @@ function clause execute(JNS(rel8)) = { /* execute jump short if not sign */ if RFLAGS[SF] == 0b0 then { // add the operand to the current instruction pointer value - let displacement = sail_sign_extend(read_operand(8, IMM8(rel8)), 64); + let displacement = sail_sign_extend(read_imm(8, IMM8(rel8)), 64); RIP = RIP + displacement; } }