diff --git a/.gitignore b/.gitignore index 7d5969f..d70f9f7 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,4 @@ *z3_problems test.* +sail_smt_cache +*test_types* diff --git a/Makefile b/Makefile index ad0ab43..92b78eb 100644 --- a/Makefile +++ b/Makefile @@ -1,7 +1,8 @@ SAIL_DIR=`sail --dir` +X86_FILES=prelude.sail registers.sail interface.sail operands.sail tiny-x86.sail tests.sail type-check: - sail prelude.sail registers.sail tiny-x86.sail tests.sail + sail $(X86_FILES) test: test.o ./test.o; @@ -9,7 +10,10 @@ test: test.o test.o: test.c gcc test.c $(SAIL_DIR)/lib/*.c -lgmp -lz -I $(SAIL_DIR)/lib/ -o test.o; -test.c: prelude.sail registers.sail tiny-x86.sail tests.sail - sail -c prelude.sail registers.sail tiny-x86.sail tests.sail -o test; +test.c: $(X86_FILES) + sail -c $(X86_FILES) -o test; -.PHONY: type-check test \ No newline at end of file +rocq: $(X86_FILES) + sail -coq $(X86_FILES) -o test; + +.PHONY: type-check test diff --git a/interface.sail b/interface.sail new file mode 100644 index 0000000..beb34f7 --- /dev/null +++ b/interface.sail @@ -0,0 +1,144 @@ +$include + +/* + - mem_acc : Type, An architecture specific description of the access kind. + This may also contain arbitrary architecture specific metadata about the + access. +*/ +enum AccessType = { + AccessType_IFETCH, // instruction fetch + AccessType_RW // read or write +} +struct AccessDescriptor = { + acctype : AccessType, + atomicop : bool, + standalone: bool, + read : bool, + write : bool, +} +function base_AccessDescriptor (acctype : AccessType) -> AccessDescriptor = struct { + acctype = acctype, + atomicop = false, + standalone = true, + read = false, + write = false, +} +function create_iFetchAccessDescriptor() -> AccessDescriptor = { + var accdesc = base_AccessDescriptor(AccessType_IFETCH); + accdesc.read = true; + accdesc +} +function create_readAccessDescriptor() -> AccessDescriptor = { + var accdesc = base_AccessDescriptor(AccessType_RW); + accdesc.read = true; + accdesc +} +function create_writeAccessDescriptor() -> AccessDescriptor = { + var accdesc = base_AccessDescriptor(AccessType_RW); + accdesc.write = true; + accdesc +} + +// Memory access generated by an explicit instruction +function mem_acc_is_explicit (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_RW + +// Memory access requested by an instruction fetch +function mem_acc_is_ifetch (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_IFETCH + +// Memory access is a translation table walk. False as memory model is flat. +function mem_acc_is_ttw (acc : AccessDescriptor) -> bool = false + +// Access is relaxed +function mem_acc_is_relaxed (acc : AccessDescriptor) -> bool = true + +// Access uses release-acquire semantics +function mem_acc_is_rel_acq_rcpc (acc : AccessDescriptor) -> bool = false +function mem_acc_is_rel_acq_rcsc (acc : AccessDescriptor) -> bool = false + +// access is from a standalone instruction (not part of an atomic sequence of instructionns) +function mem_acc_is_standalone (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_RW & acc.standalone + +// access is part of an exclusive instruction +function mem_acc_is_exclusive (acc : AccessDescriptor) -> bool = false + +// access is for part of an atomic read-modify-write instruction +function mem_acc_is_atomic_rmw (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_RW & acc.atomicop + +/* instantiate */ +instantiation sail_mem_read with + 'addr_size = 64, + 'addr_space = unit, + 'mem_acc = AccessDescriptor, + 'abort = unit, + 'CHERI = false, + 'cap_size_log = 0, + mem_acc_is_explicit = mem_acc_is_explicit, + mem_acc_is_ifetch = mem_acc_is_ifetch, + mem_acc_is_ttw = mem_acc_is_ttw, + mem_acc_is_relaxed = mem_acc_is_relaxed, + mem_acc_is_rel_acq_rcpc = mem_acc_is_rel_acq_rcpc, + mem_acc_is_rel_acq_rcsc = mem_acc_is_rel_acq_rcsc, + mem_acc_is_standalone = mem_acc_is_standalone, + mem_acc_is_exclusive = mem_acc_is_exclusive, + mem_acc_is_atomic_rmw = mem_acc_is_atomic_rmw + +instantiation sail_mem_write with + 'addr_size = 64, + 'addr_space = unit, + 'mem_acc = AccessDescriptor, + 'abort = unit, + 'CHERI = false, + 'cap_size_log = 0, + mem_acc_is_explicit = mem_acc_is_explicit, + mem_acc_is_ifetch = mem_acc_is_ifetch, + mem_acc_is_ttw = mem_acc_is_ttw, + mem_acc_is_relaxed = mem_acc_is_relaxed, + mem_acc_is_rel_acq_rcpc = mem_acc_is_rel_acq_rcpc, + mem_acc_is_rel_acq_rcsc = mem_acc_is_rel_acq_rcsc, + mem_acc_is_standalone = mem_acc_is_standalone, + mem_acc_is_exclusive = mem_acc_is_exclusive, + mem_acc_is_atomic_rmw = mem_acc_is_atomic_rmw + +/* memory read and write */ +val read_memory : forall 'N, 'N > 0. + (int('N), bits(64), AccessDescriptor) -> bits(8 * 'N) + +function read_memory(N, addr, accdesc) = { + let req : Mem_request('N, 0, 64, unit, AccessDescriptor) = struct { + access_kind = accdesc, + address = truncate(addr, 64), + address_space = (), + size = N, + num_tag = 0 + }; + + match sail_mem_read(req) { + Ok((bytes, _)) => from_bytes_le(bytes), + Err(_e) => { exit() } + } +} + +val write_memory : forall 'N, 'N > 0. (int('N), bits(64), bits(8 * 'N), AccessDescriptor) -> unit +function write_memory(N, addr, value, accdesc) = { + let req : Mem_request('N, 0, 64, unit, AccessDescriptor) = struct { + access_kind = accdesc, + address = truncate(addr, 64), + address_space = (), + size = N, + num_tag = 0, + }; + match sail_mem_write(req,to_bytes_le(N, value),[]) { + Ok(_) => (), + Err(_) => exit(), + } +} + +/* memory barrier */ +enum Barrier = { + Barrier_SFENCE, // store fence + Barrier_LFENCE, // load fence + Barrier_MFENCE // memory fence +} + +instantiation sail_barrier with + 'barrier = Barrier diff --git a/operands.sail b/operands.sail new file mode 100644 index 0000000..18262fb --- /dev/null +++ b/operands.sail @@ -0,0 +1,94 @@ +/* Memory addresses are 64 bits. Assume all possible addresses can be used. */ +type mem_addr = bits(64) + +/* immediate value types */ +type imm8 = bits(8) +type imm16 = bits(16) +type imm32 = bits(32) +type imm64 = bits(64) +union imm = { + IMM8: imm8, + IMM16: imm16, + IMM32: imm32, + IMM64: imm64 +} + +/* union types for operand */ +// register or memory operand +union rm_operand = { + rm_REG: reg_index, + rm_MEM: mem_addr +} +// register, memory, or immediate operand +union rmi_operand = { + rmi_IMM: imm, + rmi_REG: reg_index, + rmi_MEM: mem_addr +} + +/* 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) +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."); + value[7 .. 0] + }, + IMM16(value) => { + assert(wsize == 16, "Immediate value size is 16 bits, but word size is not."); + value[15 .. 0] + }, + IMM32(value) => { + 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) + }, + IMM64(value) => { + assert(wsize == 64, "Immediate value size is 64 bits, but word size is not."); + value[63 .. 0] + }, + } +} + +/* 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 + match operand { + rm_REG(reg_index) => read_GPR(wsize, reg_index), + rm_MEM(mem_addr) => read_memory(wsize_bytes, mem_addr, create_readAccessDescriptor()), + } +} + +/* 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 + 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()), + } +} + +/* overloaded function to read any operand type present in the ast */ +overload read_operand = {read_rm_operand, read_rmi_operand, read_imm, read_GPR} + +/* 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 + 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()), + } +} + +/* overloaded function to write to any register or memory type */ +overload write_operand = {write_rm_operand, write_GPR} diff --git a/prelude.sail b/prelude.sail index fdb7921..73ee7a6 100644 --- a/prelude.sail +++ b/prelude.sail @@ -1,2 +1,19 @@ default Order dec // LSB is index 0 +$define CONCURRENCY_INTERFACE_V2 // use concurrency_interface/read_write_v2.sail instead of v1 $include + +// use equality overload from sail-tiny-arm +val eq_any = pure {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq", lean: "BEq.beq", c: "eq_anything"} : forall ('a : Type). ('a, 'a) -> bool +val eq_bits_int : forall 'n 'm, 'n >= 0 & 'm >= 0. (bits('n), int('m)) -> bool +function eq_bits_int (x, y) = (unsigned(x) == y) +overload operator == = {eq_any, eq_bits_int} + +overload operator / = {tdiv_int} + +val fail: string -> unit +function fail(message) = assert(false, message) + +val flip_bit: bit -> bit +function flip_bit(bit_to_flip) = { + if bit_to_flip == bitzero then bitone else bitzero; +} diff --git a/registers.sail b/registers.sail index 5ec4aa5..5c7f33d 100644 --- a/registers.sail +++ b/registers.sail @@ -1,19 +1,5 @@ -type reg_index = range(0, 15) // range of registers that one can refer to -type word_size = {8,16,32,64} -type imm8 = bits(8) -type imm16 = bits(16) -type imm32 = bits(32) -type imm64 = bits(64) -union imm = { - IMM8: imm8, - IMM16: imm16, - IMM32: imm32, - IMM64: imm64 -} -union imm_or_reg = { - IMM: imm, - REG: reg_index -} +/* range of registers that one can refer to */ +type reg_index = range(0, 15) /* program counter */ @@ -58,35 +44,46 @@ let GPRs : vector(16, register(bits(64))) = [ ref RAX ] -/* status flags, part of register RFLAGS (which is mostly restricted access) */ -// could use bitfield for this -register CF: bits(1) // bit 0 -register PF: bits(1) // bit 2 -register AF: bits(1) // bit 4 -register ZF: bits(1) // bit 6 -register SF: bits(1) // bit 7 -register OF: bits(1) // bit 11 - -/* -read and write least-significant 8,16,32,64 (32 with 0 extend for write) bits - */ +/* register RFLAGS, system and status flags + mostly restricted access */ +bitfield rflags : bits(64) = { + // status flags + OF: 11, // overflow flag (for operations between signed values) + SF: 7, // sign flag + ZF: 6, // zero flag + AF: 4, // auxiliary carry flag + PF: 2, // parity flag + CF: 0 // carry flag (for operations between unsigned values) +} +register RFLAGS: rflags - val read_reg: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_index) -> bits('m) +/* read and write least-significant 8,16,32,64 (32 with 0 extend for write) bits */ + val read_GPR: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_index) -> bits('m) - function read_reg(wsize, i: reg_index) = { + function read_GPR(wsize, i: reg_index) = { let reg = *GPRs[i]; reg[wsize - 1 .. 0] } -val write_reg: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_index, bits('m)) -> unit +val write_GPR: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_index, bits('m)) -> unit -function write_reg(wsize, i: reg_index, value) = { +function write_GPR(wsize, i: reg_index, value) = { if wsize == 32 then { // if writing 32 bits to a register, the value to be written is zero-extended to 64 bits - (*GPRs[i])[63 .. 32]= 0x0000_0000; - (*GPRs[i])[31 .. 0]= value; + (*GPRs[i])[63 .. 32] = 0x0000_0000; + (*GPRs[i])[31 .. 0] = value; } else // the value is written to the last wsize bits of the register (*GPRs[i])[wsize - 1 .. 0] = value; -} \ No newline at end of file +} + +/* change the value of the parity flag depending on the result of an operation */ +val modify_parity_flag: forall 'm, 'm >= 8. bits('m) -> unit +function modify_parity_flag(result) = { + // we set if least significant byte of result has an even number of 1s, else clear + var even_parity = bitone; + foreach (i from 0 to 7) { + if result[i] == bitone then even_parity = flip_bit(even_parity); + }; + RFLAGS[PF] = [even_parity]; +} diff --git a/tests.sail b/tests.sail index fd6e09a..1141296 100644 --- a/tests.sail +++ b/tests.sail @@ -1,5 +1,90 @@ +function write_then_read_mem() -> unit = { + let mem_addr = 0x0000_0000_0000_0007; + let value = 0x0000_0000_0000_0004; + write_memory(8, mem_addr, value, create_writeAccessDescriptor()); + 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"); +} + +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") +} + +function xor_2_numbers() -> unit = { + 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)))); + assert(read_GPR(wsize1, 8) == 0x0101_0101_0101_1010, "XOR(reg, imm) gave an incorrect answer") +} + +function cmp_jns() -> unit = { + 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"); + let current_RIP = RIP; + execute(JNS(0x34)); + assert(RIP == current_RIP, "JNS performs a jump when the sign is set"); + RFLAGS[SF] = 0b0; + 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 wsize1 = 16; + let RSP1 = RSP; + 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"); + 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 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)))); + assert(signed(read_GPR(wsize1, 8)) == 30 - 250, "ADD(reg, imm) gave an incorrect answer") +} + +function subtract_2_numbers() -> unit = { + 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)))); + assert(signed(read_GPR(wsize1, 8)) == 30 - (- 250), "SUB(reg, imm) gave an incorrect answer"); +} + +function multiply_2_numbers() -> unit = { + let wsize = 16; + 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))); + assert(signed(read_GPR(wsize, 8)) == 30 * (- 250), "IMUL(reg, reg) gave an incorrect answer"); +} + +function jmp() -> unit = { + let current_RIP = RIP; + execute(JMP(0xFF)); + assert(RIP == add_bits(current_RIP, sail_sign_extend(0xFF, 64)), "JMP does not perform a correct jump"); +} + function main() : unit -> unit = { - let x: imm = IMM16(0x0002); - let y: bits(64) = 0x0000_0000_0000_0007; - print_bits("",y + 0x0000_0000_0000_0004) -} \ No newline at end of file + write_then_read_mem(); + mov_reg_to_mem(); + xor_2_numbers(); + cmp_jns(); + push_pop(); + add_2_numbers(); + subtract_2_numbers(); + multiply_2_numbers(); + jmp(); +} diff --git a/tiny-x86.sail b/tiny-x86.sail index cf5c096..c7e444d 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -1,18 +1,281 @@ union ast = { - // if one of the types is a tuple with first element word_size, the tuple represents (word_size, dest, src) - MOV: (word_size, reg_index, imm_or_reg), - XOR: (word_size, reg_index, imm_or_reg), + // 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), SFENCE: unit, LFENCE: unit, MFENCE: unit, - CMP: (word_size, reg_index, imm_or_reg), - PUSH: imm_or_reg, - POP: reg_index, - SUB: (word_size, reg_index, imm_or_reg), - IMUL: (word_size, reg_index, reg_index), // 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: (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) + CALL: imm32, LEAVE: unit, - RET: unit, - JMP_short: imm8, - JNS_short: imm8, - CALL: imm32 -} \ No newline at end of file + RET: unit, // near return only + JMP: imm8, // jump short only + JNS: imm8 // jump short if not sign only +} + +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"); + match (dest, src) { + (rm_MEM(_), rmi_MEM(_)) => fail(error_message), + (_,_) => () + } +} + +val execute : ast -> unit +scattered function execute + +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 + match (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) +} + +function clause execute(XOR(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 + match src { + rmi_IMM(IMM64(_)) => fail("For operation XOR, src = imm64 is not a valid operand"), + _ => () + }; + // 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); + + /* 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]]; + // set zero flag if result = 0, else clear zero flag + 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); +} + +// Wait_On_Following_Stores_Until(preceding_stores_globally_visible); +function clause execute(SFENCE()) = { + // apply barrier + sail_barrier(Barrier_SFENCE) +} + +// Wait_On_Following_Instructions_Until(preceding_instructions_complete); +function clause execute(LFENCE()) = { + // apply barrier + sail_barrier(Barrier_LFENCE) +} + +// Wait_On_Following_Loads_And_Stores_Until(preceding_loads_and_stores_globally_visible); +function clause execute(MFENCE()) = { + // apply barrier + sail_barrier(Barrier_MFENCE) +} + +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 + match second { + rmi_IMM(IMM64(_)) => fail("For operation CMP, second = imm64 is not a valid operand"), + _ => () + }; + + // execute CMP instruction + let first_val = read_operand(wsize, first); + let second_val = read_operand(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. */ + // 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 + RFLAGS[OF] = if not_bool(first_val[wsize - 1] == second_val[wsize - 1]) & not_bool(result[wsize - 1] == first_val[wsize - 1]) then 0b1 else 0b0; + // set carry flag if result < 0 (as it represents a borrow when subtracting 2 unsigned values), else clear + RFLAGS[CF] = if unsigned(first_val) < unsigned(second_val) then 0b1 else 0b0; + // set zero flag if result = 0, else clear zero flag + RFLAGS[ZF] = if result == sail_zero_extend(0x0, wsize) then 0b1 else 0b0; + // Set aux carry flag if an arithmetic operation generates a borrow out of bit 3 (i.e. least significant 4 bits) of the result; cleared otherwise + RFLAGS[AF] = if unsigned(first_val[3 .. 0]) < unsigned(second_val[3 .. 0]) 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); +} + +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"), + _ => () + }; + + // 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); + // 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) +} + +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 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(64, rm_MEM(RSP)); + write_operand(64, dest, popped_val); + // increment stack pointer to free the popped stack space + RSP = RSP + 8; +} + +function clause execute(ADD(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 + match src { + rmi_IMM(IMM64(_)) => fail("For operation ADD, src = imm64 is not a valid operand"), + _ => () + }; + + // execute ADD instruction + let dest_val = read_operand(wsize, dest); + let src_val = read_operand(wsize, src); + let result = add_bits(dest_val, src_val); + write_operand(wsize, dest, result); + + /* change value of status flags */ + // 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 + RFLAGS[OF] = if dest_val[wsize - 1] == src_val[wsize - 1] & not_bool(result[wsize - 1] == dest_val[wsize - 1]) then 0b1 else 0b0; + // set carry flag (which is for unsigned values) if result is smaller than dest or src, else clear + RFLAGS[CF] = if unsigned(result) < unsigned(dest_val) | unsigned(result) < unsigned(src_val) then 0b1 else 0b0; + // set zero flag if result = 0, else clear zero flag + RFLAGS[ZF] = if result == sail_zero_extend(0x0, wsize) then 0b1 else 0b0; + // Set aux carry flag if an arithmetic operation generates a carry out of bit 3 (i.e. least significant 4 bits) of the result; cleared otherwise + RFLAGS[AF] = if unsigned(dest_val[3 .. 0]) + unsigned(src_val[3 .. 0]) >= 16 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); +} + +function clause execute(SUB(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 + match src { + rmi_IMM(IMM64(_)) => fail("For operation SUB, src = imm64 is not a valid operand"), + _ => () + }; + + // execute SUB instruction + let dest_val = read_operand(wsize, dest); + let src_val = read_operand(wsize, src); + let result = sub_bits(dest_val, src_val); + write_operand(wsize, dest, result); + + /* change value of status flags */ + // 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 + RFLAGS[OF] = if not_bool(dest_val[wsize - 1] == src_val[wsize - 1]) & not_bool(result[wsize - 1] == dest_val[wsize - 1]) then 0b1 else 0b0; + // set carry flag if result < 0 (as it represents a borrow when subtracting 2 unsigned values), else clear + RFLAGS[CF] = if unsigned(dest_val) < unsigned(src_val) then 0b1 else 0b0; + // set zero flag if result = 0, else clear zero flag + RFLAGS[ZF] = if result == sail_zero_extend(0x0, wsize) then 0b1 else 0b0; + // Set aux carry flag if an arithmetic operation generates a borrow out of bit 3 (i.e. least significant 4 bits) of the result; cleared otherwise + RFLAGS[AF] = if unsigned(dest_val[3 .. 0]) < unsigned(src_val[3 .. 0]) 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); +} + +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"); + + // execute IMUL + let dest_val = read_operand(wsize, dest); + let src_val = read_operand(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); + + // 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 { + RFLAGS[CF] = 0b0; + RFLAGS[OF] = 0b0; + } + else { + RFLAGS[CF] = 0b1; + RFLAGS[OF] = 0b1; + } +} + +function clause execute(CALL(rel32)) = { + /* execute near relative call */ + let displacement = read_operand(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); + // change RIP as specified by the instruction + RIP = add_bits(RIP, displacement); +} + +function clause execute(LEAVE()) = { + /* copy frame pointer (RBP) into the stack pointer register (RSP) + to release the stack space allocated to the topmost stack frame */ + RSP = RBP; + // pop value into RBP + RBP = read_operand(64, rm_MEM(RSP)); + // increment stack pointer to free the popped stack space + RSP = RSP + 8; +} + +function clause execute(RET()) = { + /* execute near return */ + // pop value into RIP + RIP = read_operand(64, rm_MEM(RSP)); + // increment stack pointer to free the popped stack space + RSP = RSP + 8; +} + +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); + RIP = RIP + displacement; +} + +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); + RIP = RIP + displacement; + } +} + +end execute