From f03c56e435dd21d2b420251f1eedb32666db0c02 Mon Sep 17 00:00:00 2001 From: s-prism <166765868+s-prism@users.noreply.github.com> Date: Sun, 7 Dec 2025 19:13:42 +0000 Subject: [PATCH 1/3] Add test case to cover all instructions + comments for clarity --- tests.sail | 39 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) diff --git a/tests.sail b/tests.sail index 1141296..2986408 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"); } @@ -23,9 +25,11 @@ function xor_2_numbers() -> unit = { } 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,11 +39,13 @@ 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"); + // 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") @@ -71,6 +77,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(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 +122,6 @@ function main() : unit -> unit = { add_2_numbers(); subtract_2_numbers(); multiply_2_numbers(); + call_leave_ret(); jmp(); } From 9c0400c81d9acd263c9e721f4c260ae9f6caa648 Mon Sep 17 00:00:00 2001 From: s-prism <166765868+s-prism@users.noreply.github.com> Date: Mon, 8 Dec 2025 17:11:53 +0000 Subject: [PATCH 2/3] added lock prefix and moved prefixes lock and wsize to one struct --- interface.sail | 12 ++++ operands.sail | 63 +++++++++++-------- tests.sail | 57 +++++++++-------- tiny-x86.sail | 163 +++++++++++++++++++++++++++++++++---------------- 4 files changed, 192 insertions(+), 103 deletions(-) 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..54c8a52 100644 --- a/operands.sail +++ b/operands.sail @@ -29,10 +29,15 @@ 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) +/* instruction prefixes */ +struct prefix('wsize) = { + lock: bool, + wsize: int('wsize) +} + +/* 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 +48,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 +60,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}. (prefix('wsize), rm_operand) -> bits('wsize) +function read_rm_operand(prefix, 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_REG(reg_index) => read_GPR(prefix.wsize, reg_index), + rm_MEM(mem_addr) => { + let acc_desc = if prefix.lock then create_atomicReadAccessDescriptor() else create_readAccessDescriptor(); + let wsize_bytes = prefix.wsize / 8; + assert(prefix.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}. (prefix('wsize), rmi_operand) -> bits('wsize) +function read_rmi_operand(prefix, 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_IMM(imm) => read_imm(prefix.wsize, imm), + rmi_REG(reg_index) => read_GPR(prefix.wsize, reg_index), + rmi_MEM(mem_addr) => { + let acc_desc = if prefix.lock then create_atomicReadAccessDescriptor() else create_readAccessDescriptor(); + let wsize_bytes = prefix.wsize / 8; + assert(prefix.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}. (prefix('wsize), rm_operand, bits('wsize)) -> unit +function write_rm_operand(prefix, 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_REG(reg_index) => write_GPR(prefix.wsize, reg_index, value), + rm_MEM(mem_addr) => { + let acc_desc = if prefix.lock then create_atomicWriteAccessDescriptor() else create_writeAccessDescriptor(); + let wsize_bytes = prefix.wsize / 8; + assert(prefix.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 2986408..9a02e8d 100644 --- a/tests.sail +++ b/tests.sail @@ -10,70 +10,77 @@ function write_then_read_mem() -> unit = { function mov_reg_to_mem() -> unit = { let wsize = 16; + let prefix: prefix(16) = struct {lock = false, wsize = wsize}; 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") + execute(MOV(prefix, rm_MEM(0xFFFF_FFFF_FFFF_FFF8), rmi_REG(8))); + assert(signed(read_operand(prefix, rm_MEM(0xFFFF_FFFF_FFFF_FFF8))) == -236, "MOV(mem, reg) gave an incorrect answer") } function xor_2_numbers() -> unit = { - let wsize1 = 64; - let wsize2 = 32; - write_GPR(wsize1, 8, 0x0101_0101_0101_0101); + let wsize = 64; + let prefix: prefix(64) = struct {lock = false, wsize = wsize}; + write_GPR(wsize, 8, 0x0101_0101_0101_0101); let imm_val = 0x0000_1111; - execute(XOR(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") + execute(XOR(prefix, rm_REG(8), rmi_IMM(IMM32(imm_val)))); + assert(read_GPR(wsize, 8) == 0x0101_0101_0101_1010, "XOR(reg, imm) gave an incorrect answer") } function cmp_jns() -> unit = { + let wsize = 32; + let prefix: prefix(32) = struct {lock = false, wsize = wsize}; // cmp test - write_GPR(32, 0, 0x4444_4444); - execute(CMP(32, rm_REG(0), rmi_IMM(IMM32(0x5555_5555)))); + write_GPR(wsize, 0, 0x4444_4444); + execute(CMP(prefix, 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)); + execute(JNS(0x34): default_ast); assert(RIP == current_RIP, "JNS performs a jump when the sign is set"); RFLAGS[SF] = 0b0; - execute(JNS(0x34)); + execute(JNS(0x34): default_ast); assert(RIP == add_bits(current_RIP, sail_sign_extend(0x34, 64)), "JNS does not perform a correct jump when the sign is cleared"); } function push_pop() -> unit = { let RSP1 = RSP; // push test - let wsize1 = 16; - execute(PUSH(wsize1, rmi_IMM(IMM16(0xF0F0)))); + let wsize = 16; + let prefix: prefix(16) = struct {lock = false, wsize = wsize}; + execute(PUSH(prefix, 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(DEFAULT_PREFIX, 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))); + execute(POP(DEFAULT_PREFIX, 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 wsize1 = 64; + let prefix: prefix(64) = struct {lock = false, wsize = wsize1}; 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(prefix, 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 wsize1 = 64; + let prefix: prefix(64) = struct {lock = false, wsize = wsize1}; 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(prefix, rm_REG(8), rmi_IMM(IMM32(imm_val)))); assert(signed(read_GPR(wsize1, 8)) == 30 - (- 250), "SUB(reg, imm) gave an incorrect answer"); } function multiply_2_numbers() -> unit = { let wsize = 16; + let prefix: prefix(16) = struct {lock = false, wsize = wsize}; write_GPR(wsize, 8, get_slice_int(wsize, 30, 0)); write_GPR(wsize, 9, get_slice_int(wsize, -250, 0)); - execute(IMUL(wsize, 8, rm_REG(9))); + execute(IMUL(prefix, 8, rm_REG(9))); assert(signed(read_GPR(wsize, 8)) == 30 * (- 250), "IMUL(reg, reg) gave an incorrect answer"); } @@ -83,33 +90,33 @@ function call_leave_ret() -> unit = { RIP = 0xFFFF_0000_0000_0000; let original_RIP = RIP; let original_RSP = RSP; - execute(CALL(0xFEFE_FEFE)); + execute(CALL(0xFEFE_FEFE): default_ast); assert(RSP == 0x0000_0000_0000_ABC0, "CALL instruction does not decrement RSP correctly (when pushing a value to the stack)"); - assert(read_operand(64, rm_MEM(RSP)) == original_RIP, "CALL instruction puts incorrect value at the top of the stack"); + assert(read_operand(DEFAULT_PREFIX, 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 + execute(PUSH(DEFAULT_PREFIX, 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 + execute(MOV(DEFAULT_PREFIX, rm_REG(5), rmi_REG(4))); // 4 is the reg_index for RSP, 5 for RBP // leave test - execute(LEAVE()); + execute(LEAVE(): default_ast); 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()); + execute(RET(): default_ast); 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)); + execute(JMP(0xFF): default_ast); assert(RIP == add_bits(current_RIP, sail_sign_extend(0xFF, 64)), "JMP does not perform a correct jump"); } diff --git a/tiny-x86.sail b/tiny-x86.sail index c7e444d..fed53ce 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -1,17 +1,19 @@ -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 - MOV: (word_size, rm_operand, rmi_operand), - XOR: (word_size, rm_operand, rmi_operand), +let DEFAULT_PREFIX: prefix(64) = struct {lock = false, wsize = 64} + +union ast('wsize) = { + // Structure of all possible executable instructions + // if one of the types is a tuple with first element prefix, the tuple represents (prefix, dest, src), unless the instruction is CMP + MOV: (prefix('wsize), rm_operand, rmi_operand), + XOR: (prefix('wsize), 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), - IMUL: (word_size, reg_index, rm_operand), // IMUL with only 2 arguments (dest and src) + CMP: (prefix('wsize), rm_operand, rmi_operand), + PUSH: (prefix('wsize), rmi_operand), // only allowing 64 bit operand + POP: (prefix('wsize), rm_operand), + ADD: (prefix('wsize), rm_operand, rmi_operand), + SUB: (prefix('wsize), rm_operand, rmi_operand), + IMUL: (prefix('wsize), reg_index, rm_operand), // IMUL with only 2 arguments (dest and src) CALL: imm32, LEAVE: unit, RET: unit, // near return only @@ -19,6 +21,8 @@ union ast = { JNS: imm8 // jump short if not sign only } +type default_ast = ast(64) + val fail_if_two_mem_operands : (rm_operand, rmi_operand, string) -> unit function fail_if_two_mem_operands(dest, src, operation) = { let error_message = concat_str(operation, " operation cannot occur between 2 memory locations"); @@ -28,10 +32,24 @@ function fail_if_two_mem_operands(dest, src, operation) = { } } -val execute : ast -> unit +val fail_if_invalid_lock : forall 'wsize, 'wsize in {8, 16, 32, 64}. (prefix('wsize), ast('wsize)) -> unit +function fail_if_invalid_lock(prefix, op) = { + if prefix.lock then { + match op { + XOR(prefix, rm_REG(_), src) => fail("undefined opcode exception (#UD): LOCK prefix cannot be applied to dest = reg"), + ADD(prefix, rm_REG(_), src) => fail("undefined opcode exception (#UD): LOCK prefix cannot be applied to dest = reg"), + SUB(prefix, rm_REG(_), src) => fail("undefined opcode exception (#UD): LOCK prefix cannot be applied to dest = reg"), + _ => fail("undefined opcode exception (#UD): LOCK prefix cannot be prepended to instruction") + } + } +} + +val execute : forall 'wsize, 'wsize in {8, 16, 32, 64}. ast('wsize) -> unit scattered function execute -function clause execute(MOV(wsize, dest, src)) = { +function clause execute(MOV(prefix, dest, src)) = { + // required assertion for type-checking + assert(prefix.wsize == 8 | prefix.wsize == 16 | prefix.wsize == 32 | prefix.wsize == 64); // MOV cannot occur between dest = memory location and src = memory location fail_if_two_mem_operands(dest, src, "MOV"); // MOV operation cannot be executed on dest = mem64 and src = imm64 @@ -39,12 +57,17 @@ function clause execute(MOV(wsize, dest, src)) = { (rm_MEM(_), rmi_IMM(IMM64(_))) => fail("MOV operation cannot be executed on dest = mem64 and src = imm64"), (_,_) => () }; + // MOV is not valid with prefix lock = true + fail_if_invalid_lock(prefix, MOV(prefix, dest, src)); + // execute MOV instruction - let val_to_write = read_operand(wsize, src); - write_operand(wsize, dest, val_to_write) + let val_to_write = read_operand(prefix, src); + write_operand(prefix, dest, val_to_write) } -function clause execute(XOR(wsize, dest, src)) = { +function clause execute(XOR(prefix, dest, src)) = { + // required assertion for type-checking + assert(prefix.wsize == 8 | prefix.wsize == 16 | prefix.wsize == 32 | prefix.wsize == 64); // 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,20 +75,23 @@ 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 prefix lock = true if dest is a register location + fail_if_invalid_lock(prefix, XOR(prefix, dest, src)); + // 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(prefix, dest); + let src_val = read_operand({prefix with lock = false}, src); + let result = xor_vec(dest_val, src_val); + write_operand(prefix, dest, result); /* change value of status flags */ // clear overflow and carry flag RFLAGS[OF] = 0b0; RFLAGS[CF] = 0b0; // sign flag = msb of result (0 = +ve, 1 = -ve) - RFLAGS[SF] = [result[wsize - 1]]; + RFLAGS[SF] = [result[prefix.wsize - 1]]; // set zero flag if result = 0, else clear zero flag - RFLAGS[ZF] = if result == sail_zero_extend(0x0, wsize) then 0b1 else 0b0; + RFLAGS[ZF] = if result == sail_zero_extend(0x0, prefix.wsize) then 0b1 else 0b0; // set parity flag if least significant byte of result contains an even number of 1 bits, else clear modify_parity_flag(result); } @@ -88,7 +114,9 @@ function clause execute(MFENCE()) = { sail_barrier(Barrier_MFENCE) } -function clause execute(CMP(wsize, first, second)) = { +function clause execute(CMP(prefix, first, second)) = { + // required assertion for type-checking + assert(prefix.wsize == 8 | prefix.wsize == 16 | prefix.wsize == 32 | prefix.wsize == 64); // CMP cannot occur between first = memory location and second = memory location fail_if_two_mem_operands(first, second, "CMP"); // For operation CMP, second = imm64 is not a valid operand @@ -96,13 +124,16 @@ function clause execute(CMP(wsize, first, second)) = { rmi_IMM(IMM64(_)) => fail("For operation CMP, second = imm64 is not a valid operand"), _ => () }; + // CMP is not valid with prefix lock = true + fail_if_invalid_lock(prefix, CMP(prefix, first, second)); // execute CMP instruction - let first_val = read_operand(wsize, first); - let second_val = read_operand(wsize, second); + let first_val = read_operand(prefix, first); + let second_val = read_operand(prefix, second); let result = sub_bits(first_val, second_val); /* change value of status flags. Equivalent to the changes made on executing the SUB instruction. */ + let wsize = prefix.wsize; // sign flag = msb of result (0 = +ve, 1 = -ve) RFLAGS[SF] = [result[wsize - 1]]; // set overflow flag (which is for signed values) if first and second operand have opposite signs, but the sign of the result doesn't match the first operand, else clear @@ -117,39 +148,49 @@ function clause execute(CMP(wsize, first, second)) = { modify_parity_flag(result); } -function clause execute(PUSH(wsize, src)) = { +function clause execute(PUSH(prefix, src)) = { + // required assertion for type-checking + assert(prefix.wsize == 8 | prefix.wsize == 16 | prefix.wsize == 32 | prefix.wsize == 64); // 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 prefix.wsize == 64 => fail("Operand for PUSH operation not allowed"), + rmi_REG(_) if prefix.wsize == 8 => fail("Operand for PUSH operation not allowed"), + rmi_MEM(_) if prefix.wsize == 8 => fail("Operand for PUSH operation not allowed"), _ => () }; + // PUSH is not valid with prefix lock = true + fail_if_invalid_lock(prefix, PUSH(prefix, src)); // 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(prefix, 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(DEFAULT_PREFIX, dest_address, src_val) } -function clause execute(POP(wsize, dest)) = { +function clause execute(POP(prefix, dest)) = { + // required assertion for type-checking + assert(prefix.wsize == 8 | prefix.wsize == 16 | prefix.wsize == 32 | prefix.wsize == 64); // POP instruction does not allow dest to be 8 bits long. Due to 64 bit addressing, dest also cannot be 32 bits long. // Also not allowing a 16-bit dest in this model for simplicity (to keep the stack aligned) - if wsize == 8 | wsize == 32 then fail("dest size for POP operation not supported"); - if wsize == 16 then fail("dest size for POP operation not implemented in this model"); + if prefix.wsize == 8 | prefix.wsize == 32 then fail("dest size for POP operation not supported"); + if prefix.wsize == 16 then fail("dest size for POP operation not implemented in this model"); + // POP is not valid with prefix lock = true + fail_if_invalid_lock(prefix, POP(prefix, dest)); // 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(DEFAULT_PREFIX, rm_MEM(RSP)); + write_operand(DEFAULT_PREFIX, 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(prefix, dest, src)) = { + // required assertion for type-checking + assert(prefix.wsize == 8 | prefix.wsize == 16 | prefix.wsize == 32 | prefix.wsize == 64); // 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,14 +198,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 + fail_if_invalid_lock(prefix, ADD(prefix, dest, src)); // execute ADD instruction - let dest_val = read_operand(wsize, dest); - let src_val = read_operand(wsize, src); + let dest_val = read_operand(prefix, dest); + let src_val = read_operand({prefix with lock = false}, src); let result = add_bits(dest_val, src_val); - write_operand(wsize, dest, result); + write_operand(prefix, dest, result); /* change value of status flags */ + let wsize = prefix.wsize; // sign flag = msb of result (0 = +ve, 1 = -ve) RFLAGS[SF] = [result[wsize - 1]]; // set overflow flag (which is for signed values) if dest and src operand have the same sign, but the sign of the result is different @@ -179,7 +223,9 @@ function clause execute(ADD(wsize, dest, src)) = { modify_parity_flag(result); } -function clause execute(SUB(wsize, dest, src)) = { +function clause execute(SUB(prefix, dest, src)) = { + // required assertion for type-checking + assert(prefix.wsize == 8 | prefix.wsize == 16 | prefix.wsize == 32 | prefix.wsize == 64); // 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,14 +233,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 + fail_if_invalid_lock(prefix, SUB(prefix, dest, src)); // execute SUB instruction - let dest_val = read_operand(wsize, dest); - let src_val = read_operand(wsize, src); + let dest_val = read_operand(prefix, dest); + let src_val = read_operand({prefix with lock = false}, src); let result = sub_bits(dest_val, src_val); - write_operand(wsize, dest, result); + write_operand(prefix, dest, result); /* change value of status flags */ + let wsize = prefix.wsize; // sign flag = msb of result (0 = +ve, 1 = -ve) RFLAGS[SF] = [result[wsize - 1]]; // set overflow flag (which is for signed values) if dest and src operand have opposite signs, but the sign of the result doesn't match the dest operand, else clear @@ -209,17 +258,23 @@ function clause execute(SUB(wsize, dest, src)) = { modify_parity_flag(result); } -function clause execute(IMUL(wsize, dest, src)) = { +function clause execute(IMUL(prefix, dest, src)) = { + // required assertion for type-checking + assert(prefix.wsize == 8 | prefix.wsize == 16 | prefix.wsize == 32 | prefix.wsize == 64); + + let wsize = prefix.wsize; // IMUL cannot occur between 8 bit register or memory locations if wsize == 8 then fail("8 bit operands are not valid for operation IMUL"); + // IMUL is not valid with prefix lock = true + fail_if_invalid_lock(prefix, IMUL(prefix, dest, src)); // 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(prefix, 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 +289,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(DEFAULT_PREFIX, dest_address, RIP); // change RIP as specified by the instruction RIP = add_bits(RIP, displacement); } @@ -249,7 +304,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(DEFAULT_PREFIX, rm_MEM(RSP)); // increment stack pointer to free the popped stack space RSP = RSP + 8; } @@ -257,7 +312,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(DEFAULT_PREFIX, rm_MEM(RSP)); // increment stack pointer to free the popped stack space RSP = RSP + 8; } @@ -265,7 +320,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 +328,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; } } From 34b29f1a5c634980fc5250584dd4fbadcf4acca7 Mon Sep 17 00:00:00 2001 From: s-prism <166765868+s-prism@users.noreply.github.com> Date: Wed, 10 Dec 2025 15:19:43 +0000 Subject: [PATCH 3/3] Simplified structure of lock and wsize prefixes within the ast --- operands.sail | 44 ++++++-------- tests.sail | 60 +++++++++---------- tiny-x86.sail | 158 +++++++++++++++++++------------------------------- 3 files changed, 107 insertions(+), 155 deletions(-) diff --git a/operands.sail b/operands.sail index 54c8a52..41b37e4 100644 --- a/operands.sail +++ b/operands.sail @@ -29,12 +29,6 @@ union rmi_operand = { /* permitted word sizes */ type word_size = {8,16,32,64} -/* instruction prefixes */ -struct prefix('wsize) = { - lock: bool, - wsize: int('wsize) -} - /* 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) = { @@ -60,29 +54,29 @@ function read_imm(wsize, imm) = { } /* read register or memory operand */ -val read_rm_operand: forall 'wsize, 'wsize in {8, 16, 32, 64}. (prefix('wsize), rm_operand) -> bits('wsize) -function read_rm_operand(prefix, operand) = { +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(prefix.wsize, reg_index), + rm_REG(reg_index) => read_GPR(wsize, reg_index), rm_MEM(mem_addr) => { - let acc_desc = if prefix.lock then create_atomicReadAccessDescriptor() else create_readAccessDescriptor(); - let wsize_bytes = prefix.wsize / 8; - assert(prefix.wsize == wsize_bytes * 8); // required for type-checking + 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 'wsize, 'wsize in {8, 16, 32, 64}. (prefix('wsize), rmi_operand) -> bits('wsize) -function read_rmi_operand(prefix, operand) = { +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(prefix.wsize, imm), - rmi_REG(reg_index) => read_GPR(prefix.wsize, reg_index), + rmi_IMM(imm) => read_imm(wsize, imm), + rmi_REG(reg_index) => read_GPR(wsize, reg_index), rmi_MEM(mem_addr) => { - let acc_desc = if prefix.lock then create_atomicReadAccessDescriptor() else create_readAccessDescriptor(); - let wsize_bytes = prefix.wsize / 8; - assert(prefix.wsize == wsize_bytes * 8); // required for type-checking + 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) }, } @@ -92,14 +86,14 @@ function read_rmi_operand(prefix, operand) = { overload read_operand = {read_rm_operand, read_rmi_operand} /* write to reg or mem location */ -val write_rm_operand: forall 'wsize, 'wsize in {8, 16, 32, 64}. (prefix('wsize), rm_operand, bits('wsize)) -> unit -function write_rm_operand(prefix, operand, value) = { +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(prefix.wsize, reg_index, value), + rm_REG(reg_index) => write_GPR(wsize, reg_index, value), rm_MEM(mem_addr) => { - let acc_desc = if prefix.lock then create_atomicWriteAccessDescriptor() else create_writeAccessDescriptor(); - let wsize_bytes = prefix.wsize / 8; - assert(prefix.wsize == wsize_bytes * 8); // required for type-checking + 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) }, } diff --git a/tests.sail b/tests.sail index 9a02e8d..dc3a4ed 100644 --- a/tests.sail +++ b/tests.sail @@ -10,77 +10,73 @@ function write_then_read_mem() -> unit = { function mov_reg_to_mem() -> unit = { let wsize = 16; - let prefix: prefix(16) = struct {lock = false, wsize = wsize}; write_GPR(wsize, 8, get_slice_int(wsize, -236, 0)); - execute(MOV(prefix, rm_MEM(0xFFFF_FFFF_FFFF_FFF8), rmi_REG(8))); - assert(signed(read_operand(prefix, rm_MEM(0xFFFF_FFFF_FFFF_FFF8))) == -236, "MOV(mem, reg) gave an incorrect answer") + execute(MOV(wsize, rm_MEM(0xFFFF_FFFF_FFFF_FFF8), rmi_REG(8))); + 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 wsize = 64; - let prefix: prefix(64) = struct {lock = false, wsize = wsize}; - write_GPR(wsize, 8, 0x0101_0101_0101_0101); + let lock = false; + let wsize1 = 64; + let wsize2 = 32; + write_GPR(wsize1, 8, 0x0101_0101_0101_0101); let imm_val = 0x0000_1111; - execute(XOR(prefix, rm_REG(8), rmi_IMM(IMM32(imm_val)))); - assert(read_GPR(wsize, 8) == 0x0101_0101_0101_1010, "XOR(reg, imm) gave an incorrect answer") + 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 = { - let wsize = 32; - let prefix: prefix(32) = struct {lock = false, wsize = wsize}; // cmp test - write_GPR(wsize, 0, 0x4444_4444); - execute(CMP(prefix, rm_REG(0), rmi_IMM(IMM32(0x5555_5555)))); + 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): default_ast); + execute(JNS(0x34)); assert(RIP == current_RIP, "JNS performs a jump when the sign is set"); RFLAGS[SF] = 0b0; - execute(JNS(0x34): default_ast); + execute(JNS(0x34)); assert(RIP == add_bits(current_RIP, sail_sign_extend(0x34, 64)), "JNS does not perform a correct jump when the sign is cleared"); } function push_pop() -> unit = { let RSP1 = RSP; // push test - let wsize = 16; - let prefix: prefix(16) = struct {lock = false, wsize = wsize}; - execute(PUSH(prefix, rmi_IMM(IMM16(0xF0F0)))); + let wsize1 = 16; + execute(PUSH(wsize1, rmi_IMM(IMM16(0xF0F0)))); assert(RSP + 8 == RSP1, "PUSH does not correctly change stack pointer"); - assert(read_operand(DEFAULT_PREFIX, 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(DEFAULT_PREFIX, rm_REG(15))); + 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 prefix: prefix(64) = struct {lock = false, wsize = wsize1}; let wsize2 = 32; write_GPR(wsize1, 8, get_slice_int(wsize1, 30, 0)); let imm_val = get_slice_int(wsize2, -250, 0); - execute(ADD(prefix, 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 prefix: prefix(64) = struct {lock = false, wsize = wsize1}; let wsize2 = 32; write_GPR(wsize1, 8, get_slice_int(wsize1, 30, 0)); let imm_val = get_slice_int(wsize2, -250, 0); - execute(SUB(prefix, 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"); } function multiply_2_numbers() -> unit = { let wsize = 16; - let prefix: prefix(16) = struct {lock = false, wsize = wsize}; write_GPR(wsize, 8, get_slice_int(wsize, 30, 0)); write_GPR(wsize, 9, get_slice_int(wsize, -250, 0)); - execute(IMUL(prefix, 8, rm_REG(9))); + execute(IMUL(wsize, 8, rm_REG(9))); assert(signed(read_GPR(wsize, 8)) == 30 * (- 250), "IMUL(reg, reg) gave an incorrect answer"); } @@ -90,33 +86,33 @@ function call_leave_ret() -> unit = { RIP = 0xFFFF_0000_0000_0000; let original_RIP = RIP; let original_RSP = RSP; - execute(CALL(0xFEFE_FEFE): default_ast); + 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(DEFAULT_PREFIX, rm_MEM(RSP)) == original_RIP, "CALL instruction puts incorrect value at the top of 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(DEFAULT_PREFIX, rmi_REG(5))); // 5 is the reg_index for RBP + execute(PUSH(64, rmi_REG(5))); // 5 is the reg_index for RBP // copy RSP value into RBP register - execute(MOV(DEFAULT_PREFIX, rm_REG(5), rmi_REG(4))); // 4 is the reg_index for RSP, 5 for RBP + execute(MOV(64, rm_REG(5), rmi_REG(4))); // 4 is the reg_index for RSP, 5 for RBP // leave test - execute(LEAVE(): default_ast); + 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(): default_ast); + 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): default_ast); + execute(JMP(0xFF)); assert(RIP == add_bits(current_RIP, sail_sign_extend(0xFF, 64)), "JMP does not perform a correct jump"); } diff --git a/tiny-x86.sail b/tiny-x86.sail index fed53ce..e3a2fc7 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -1,19 +1,17 @@ -let DEFAULT_PREFIX: prefix(64) = struct {lock = false, wsize = 64} - -union ast('wsize) = { +union ast = { // Structure of all possible executable instructions - // if one of the types is a tuple with first element prefix, the tuple represents (prefix, dest, src), unless the instruction is CMP - MOV: (prefix('wsize), rm_operand, rmi_operand), - XOR: (prefix('wsize), rm_operand, rmi_operand), + // 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: (bool, word_size, rm_operand, rmi_operand), SFENCE: unit, LFENCE: unit, MFENCE: unit, - CMP: (prefix('wsize), rm_operand, rmi_operand), - PUSH: (prefix('wsize), rmi_operand), // only allowing 64 bit operand - POP: (prefix('wsize), rm_operand), - ADD: (prefix('wsize), rm_operand, rmi_operand), - SUB: (prefix('wsize), rm_operand, rmi_operand), - IMUL: (prefix('wsize), reg_index, rm_operand), // IMUL with only 2 arguments (dest and src) + CMP: (word_size, rm_operand, rmi_operand), + PUSH: (word_size, rmi_operand), // only allowing 64 bit operand + POP: (word_size, rm_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, RET: unit, // near return only @@ -21,8 +19,6 @@ union ast('wsize) = { JNS: imm8 // jump short if not sign only } -type default_ast = ast(64) - val fail_if_two_mem_operands : (rm_operand, rmi_operand, string) -> unit function fail_if_two_mem_operands(dest, src, operation) = { let error_message = concat_str(operation, " operation cannot occur between 2 memory locations"); @@ -32,24 +28,10 @@ function fail_if_two_mem_operands(dest, src, operation) = { } } -val fail_if_invalid_lock : forall 'wsize, 'wsize in {8, 16, 32, 64}. (prefix('wsize), ast('wsize)) -> unit -function fail_if_invalid_lock(prefix, op) = { - if prefix.lock then { - match op { - XOR(prefix, rm_REG(_), src) => fail("undefined opcode exception (#UD): LOCK prefix cannot be applied to dest = reg"), - ADD(prefix, rm_REG(_), src) => fail("undefined opcode exception (#UD): LOCK prefix cannot be applied to dest = reg"), - SUB(prefix, rm_REG(_), src) => fail("undefined opcode exception (#UD): LOCK prefix cannot be applied to dest = reg"), - _ => fail("undefined opcode exception (#UD): LOCK prefix cannot be prepended to instruction") - } - } -} - -val execute : forall 'wsize, 'wsize in {8, 16, 32, 64}. ast('wsize) -> unit +val execute : ast -> unit scattered function execute -function clause execute(MOV(prefix, dest, src)) = { - // required assertion for type-checking - assert(prefix.wsize == 8 | prefix.wsize == 16 | prefix.wsize == 32 | prefix.wsize == 64); +function clause execute(MOV(wsize, dest, src)) = { // MOV cannot occur between dest = memory location and src = memory location fail_if_two_mem_operands(dest, src, "MOV"); // MOV operation cannot be executed on dest = mem64 and src = imm64 @@ -57,17 +39,13 @@ function clause execute(MOV(prefix, dest, src)) = { (rm_MEM(_), rmi_IMM(IMM64(_))) => fail("MOV operation cannot be executed on dest = mem64 and src = imm64"), (_,_) => () }; - // MOV is not valid with prefix lock = true - fail_if_invalid_lock(prefix, MOV(prefix, dest, src)); // execute MOV instruction - let val_to_write = read_operand(prefix, src); - write_operand(prefix, 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(prefix, dest, src)) = { - // required assertion for type-checking - assert(prefix.wsize == 8 | prefix.wsize == 16 | prefix.wsize == 32 | prefix.wsize == 64); +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 @@ -75,23 +53,26 @@ function clause execute(XOR(prefix, dest, src)) = { rmi_IMM(IMM64(_)) => fail("For operation XOR, src = imm64 is not a valid operand"), _ => () }; - // XOR is not valid with prefix lock = true if dest is a register location - fail_if_invalid_lock(prefix, XOR(prefix, dest, src)); + // 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 dest_val = read_operand(prefix, dest); - let src_val = read_operand({prefix with lock = false}, src); + 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(prefix, dest, result); + write_operand(lock, wsize, dest, result); /* change value of status flags */ // clear overflow and carry flag RFLAGS[OF] = 0b0; RFLAGS[CF] = 0b0; // sign flag = msb of result (0 = +ve, 1 = -ve) - RFLAGS[SF] = [result[prefix.wsize - 1]]; + RFLAGS[SF] = [result[wsize - 1]]; // set zero flag if result = 0, else clear zero flag - RFLAGS[ZF] = if result == sail_zero_extend(0x0, prefix.wsize) then 0b1 else 0b0; + RFLAGS[ZF] = if result == sail_zero_extend(0x0, wsize) then 0b1 else 0b0; // set parity flag if least significant byte of result contains an even number of 1 bits, else clear modify_parity_flag(result); } @@ -114,9 +95,7 @@ function clause execute(MFENCE()) = { sail_barrier(Barrier_MFENCE) } -function clause execute(CMP(prefix, first, second)) = { - // required assertion for type-checking - assert(prefix.wsize == 8 | prefix.wsize == 16 | prefix.wsize == 32 | prefix.wsize == 64); +function clause execute(CMP(wsize, first, second)) = { // CMP cannot occur between first = memory location and second = memory location fail_if_two_mem_operands(first, second, "CMP"); // For operation CMP, second = imm64 is not a valid operand @@ -124,16 +103,13 @@ function clause execute(CMP(prefix, first, second)) = { rmi_IMM(IMM64(_)) => fail("For operation CMP, second = imm64 is not a valid operand"), _ => () }; - // CMP is not valid with prefix lock = true - fail_if_invalid_lock(prefix, CMP(prefix, first, second)); // execute CMP instruction - let first_val = read_operand(prefix, first); - let second_val = read_operand(prefix, 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. */ - let wsize = prefix.wsize; // sign flag = msb of result (0 = +ve, 1 = -ve) RFLAGS[SF] = [result[wsize - 1]]; // set overflow flag (which is for signed values) if first and second operand have opposite signs, but the sign of the result doesn't match the first operand, else clear @@ -148,49 +124,39 @@ function clause execute(CMP(prefix, first, second)) = { modify_parity_flag(result); } -function clause execute(PUSH(prefix, src)) = { - // required assertion for type-checking - assert(prefix.wsize == 8 | prefix.wsize == 16 | prefix.wsize == 32 | prefix.wsize == 64); +function clause execute(PUSH(wsize, src)) = { // PUSH instruction does not allow src = imm64, reg8 or mem8 match src { - rmi_IMM(_) if prefix.wsize == 64 => fail("Operand for PUSH operation not allowed"), - rmi_REG(_) if prefix.wsize == 8 => fail("Operand for PUSH operation not allowed"), - rmi_MEM(_) if prefix.wsize == 8 => fail("Operand for PUSH operation not allowed"), + 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"), _ => () }; - // PUSH is not valid with prefix lock = true - fail_if_invalid_lock(prefix, PUSH(prefix, src)); // 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(prefix, 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(DEFAULT_PREFIX, dest_address, src_val) + write_operand(false, 64, dest_address, src_val) } -function clause execute(POP(prefix, dest)) = { - // required assertion for type-checking - assert(prefix.wsize == 8 | prefix.wsize == 16 | prefix.wsize == 32 | prefix.wsize == 64); +function clause execute(POP(wsize, dest)) = { // POP instruction does not allow dest to be 8 bits long. Due to 64 bit addressing, dest also cannot be 32 bits long. // Also not allowing a 16-bit dest in this model for simplicity (to keep the stack aligned) - if prefix.wsize == 8 | prefix.wsize == 32 then fail("dest size for POP operation not supported"); - if prefix.wsize == 16 then fail("dest size for POP operation not implemented in this model"); - // POP is not valid with prefix lock = true - fail_if_invalid_lock(prefix, POP(prefix, dest)); + if wsize == 8 | wsize == 32 then fail("dest size for POP operation not supported"); + 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(DEFAULT_PREFIX, rm_MEM(RSP)); - write_operand(DEFAULT_PREFIX, 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(prefix, dest, src)) = { - // required assertion for type-checking - assert(prefix.wsize == 8 | prefix.wsize == 16 | prefix.wsize == 32 | prefix.wsize == 64); +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 @@ -199,16 +165,18 @@ function clause execute(ADD(prefix, dest, src)) = { _ => () }; // ADD is not valid with prefix lock = true if dest is a register location - fail_if_invalid_lock(prefix, ADD(prefix, dest, src)); + 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(prefix, dest); - let src_val = read_operand({prefix with lock = false}, 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(prefix, dest, result); + write_operand(lock, wsize, dest, result); /* change value of status flags */ - let wsize = prefix.wsize; // sign flag = msb of result (0 = +ve, 1 = -ve) RFLAGS[SF] = [result[wsize - 1]]; // set overflow flag (which is for signed values) if dest and src operand have the same sign, but the sign of the result is different @@ -223,9 +191,7 @@ function clause execute(ADD(prefix, dest, src)) = { modify_parity_flag(result); } -function clause execute(SUB(prefix, dest, src)) = { - // required assertion for type-checking - assert(prefix.wsize == 8 | prefix.wsize == 16 | prefix.wsize == 32 | prefix.wsize == 64); +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 @@ -234,16 +200,18 @@ function clause execute(SUB(prefix, dest, src)) = { _ => () }; // SUB is not valid with prefix lock = true if dest is a register location - fail_if_invalid_lock(prefix, SUB(prefix, dest, src)); + 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(prefix, dest); - let src_val = read_operand({prefix with lock = false}, 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(prefix, dest, result); + write_operand(lock, wsize, dest, result); /* change value of status flags */ - let wsize = prefix.wsize; // sign flag = msb of result (0 = +ve, 1 = -ve) RFLAGS[SF] = [result[wsize - 1]]; // set overflow flag (which is for signed values) if dest and src operand have opposite signs, but the sign of the result doesn't match the dest operand, else clear @@ -258,19 +226,13 @@ function clause execute(SUB(prefix, dest, src)) = { modify_parity_flag(result); } -function clause execute(IMUL(prefix, dest, src)) = { - // required assertion for type-checking - assert(prefix.wsize == 8 | prefix.wsize == 16 | prefix.wsize == 32 | prefix.wsize == 64); - - let wsize = prefix.wsize; +function clause execute(IMUL(wsize, dest, src)) = { // IMUL cannot occur between 8 bit register or memory locations if wsize == 8 then fail("8 bit operands are not valid for operation IMUL"); - // IMUL is not valid with prefix lock = true - fail_if_invalid_lock(prefix, IMUL(prefix, dest, src)); // execute IMUL let dest_val = read_GPR(wsize, dest); - let src_val = read_operand(prefix, src); + 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]; @@ -294,7 +256,7 @@ function clause execute(CALL(rel32)) = { RSP = sub_bits(RSP, sail_zero_extend(0x8, 64)); // push current RIP to the stack let dest_address = rm_MEM(RSP); - write_operand(DEFAULT_PREFIX, dest_address, RIP); + write_operand(false, 64, dest_address, RIP); // change RIP as specified by the instruction RIP = add_bits(RIP, displacement); } @@ -304,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(DEFAULT_PREFIX, rm_MEM(RSP)); + RBP = read_operand(false, 64, rm_MEM(RSP)); // increment stack pointer to free the popped stack space RSP = RSP + 8; } @@ -312,7 +274,7 @@ function clause execute(LEAVE()) = { function clause execute(RET()) = { /* execute near return */ // pop value into RIP - RIP = read_operand(DEFAULT_PREFIX, rm_MEM(RSP)); + RIP = read_operand(false, 64, rm_MEM(RSP)); // increment stack pointer to free the popped stack space RSP = RSP + 8; }