From 70dee35f42945a845c79982d219c897e1025bdc6 Mon Sep 17 00:00:00 2001 From: s-prism Date: Mon, 24 Nov 2025 20:03:39 +0000 Subject: [PATCH 01/24] Added add instruction and added memory operand --- registers.sail | 19 ++++++++++++++++--- tiny-x86.sail | 15 ++++++++------- 2 files changed, 24 insertions(+), 10 deletions(-) diff --git a/registers.sail b/registers.sail index 5ec4aa5..8eea3e8 100644 --- a/registers.sail +++ b/registers.sail @@ -1,4 +1,12 @@ type reg_index = range(0, 15) // range of registers that one can refer to + +/* +* Memory addresses are 64 bits, but not all of these are allowed to be used. +* (Must verify that a memory address is valid before use. +* Implementing a flat memory model, so no segmentation.) +*/ +type mem_addr = bits(64) + type word_size = {8,16,32,64} type imm8 = bits(8) type imm16 = bits(16) @@ -10,9 +18,14 @@ union imm = { IMM32: imm32, IMM64: imm64 } -union imm_or_reg = { - IMM: imm, - REG: reg_index +union reg_or_mem = { + rm_REG: reg_index, + rm_MEM: mem_addr +} +union any = { + rmi_IMM: imm, + rmi_REG: reg_index, + rmi_MEM: mem_addr } /* program counter */ diff --git a/tiny-x86.sail b/tiny-x86.sail index cf5c096..2f63c9a 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -1,15 +1,16 @@ 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), + MOV: (word_size, reg_or_mem, any), + XOR: (word_size, reg_or_mem, any), 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, reg_or_mem, any), + PUSH: (word_size, any), + POP: (word_size, reg_or_mem), + ADD: (word_size, reg_or_mem, any), + SUB: (word_size, reg_or_mem, any), + IMUL: (word_size, reg_index, reg_or_mem), // IMUL with only 2 arguments (dest and src) LEAVE: unit, RET: unit, JMP_short: imm8, From 39ac66c080401988a75d986056771e881d2d87d4 Mon Sep 17 00:00:00 2001 From: s-prism Date: Mon, 24 Nov 2025 20:10:47 +0000 Subject: [PATCH 02/24] Moved operand types away from register-specific file --- Makefile | 6 +++--- operands.sail | 35 +++++++++++++++++++++++++++++++++++ registers.sail | 30 ------------------------------ 3 files changed, 38 insertions(+), 33 deletions(-) create mode 100644 operands.sail diff --git a/Makefile b/Makefile index ad0ab43..1ae5d4c 100644 --- a/Makefile +++ b/Makefile @@ -1,7 +1,7 @@ SAIL_DIR=`sail --dir` type-check: - sail prelude.sail registers.sail tiny-x86.sail tests.sail + sail prelude.sail operands.sail registers.sail tiny-x86.sail tests.sail test: test.o ./test.o; @@ -9,7 +9,7 @@ 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: prelude.sail operands.sail registers.sail tiny-x86.sail tests.sail + sail -c prelude.sail operands.sail registers.sail tiny-x86.sail tests.sail -o test; .PHONY: type-check test \ No newline at end of file diff --git a/operands.sail b/operands.sail new file mode 100644 index 0000000..efd189a --- /dev/null +++ b/operands.sail @@ -0,0 +1,35 @@ +/* range of registers that one can refer to */ +type reg_index = range(0, 15) + +/* +* Memory addresses are 64 bits, but not all of these are allowed to be used. +* (Must verify that a memory address is valid before use. +* Implementing a flat memory model, so no segmentation.) +*/ +type mem_addr = bits(64) + +/* permitted word sizes */ +type word_size = {8,16,32,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 */ +union reg_or_mem = { + rm_REG: reg_index, + rm_MEM: mem_addr +} +union any = { + rmi_IMM: imm, + rmi_REG: reg_index, + rmi_MEM: mem_addr +} \ No newline at end of file diff --git a/registers.sail b/registers.sail index 8eea3e8..e7e45ee 100644 --- a/registers.sail +++ b/registers.sail @@ -1,33 +1,3 @@ -type reg_index = range(0, 15) // range of registers that one can refer to - -/* -* Memory addresses are 64 bits, but not all of these are allowed to be used. -* (Must verify that a memory address is valid before use. -* Implementing a flat memory model, so no segmentation.) -*/ -type mem_addr = bits(64) - -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 reg_or_mem = { - rm_REG: reg_index, - rm_MEM: mem_addr -} -union any = { - rmi_IMM: imm, - rmi_REG: reg_index, - rmi_MEM: mem_addr -} - /* program counter */ register RIP: bits(64) From 0aed5fb42a8ddc4e0f3c98ed979e70273bd9a53d Mon Sep 17 00:00:00 2001 From: s-prism Date: Tue, 25 Nov 2025 00:05:04 +0000 Subject: [PATCH 03/24] In progress: Defining read and write operand functions --- Makefile | 7 ++++--- operand_types.sail | 36 ++++++++++++++++++++++++++++++++ operands.sail | 52 ++++++++++++++++++++-------------------------- tests.sail | 2 +- 4 files changed, 63 insertions(+), 34 deletions(-) create mode 100644 operand_types.sail diff --git a/Makefile b/Makefile index 1ae5d4c..d3adaab 100644 --- a/Makefile +++ b/Makefile @@ -1,7 +1,8 @@ SAIL_DIR=`sail --dir` +X86_FILES=prelude.sail operand_types.sail registers.sail operands.sail tiny-x86.sail tests.sail type-check: - sail prelude.sail operands.sail registers.sail tiny-x86.sail tests.sail + sail $(X86_FILES) test: test.o ./test.o; @@ -9,7 +10,7 @@ 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 operands.sail registers.sail tiny-x86.sail tests.sail - sail -c prelude.sail operands.sail registers.sail tiny-x86.sail tests.sail -o test; +test.c: prelude.sail operand_types.sail registers.sail operands.sail tiny-x86.sail tests.sail + sail -c $(X86_FILES) -o test; .PHONY: type-check test \ No newline at end of file diff --git a/operand_types.sail b/operand_types.sail new file mode 100644 index 0000000..96981da --- /dev/null +++ b/operand_types.sail @@ -0,0 +1,36 @@ +/* range of registers that one can refer to */ +type reg_index = range(0, 15) + +/* +* Memory addresses are 64 bits, but not all of these are allowed to be used. +* (Must verify that a memory address is valid before use. +* Implementing a flat memory model, so no segmentation.) +*/ +type mem_addr = bits(64) + +/* permitted word sizes */ +type word_size = {8,16,32,64} + +/* immediate value types */ +type imm8 = bits(8) +type imm16 = bits(16) +type imm32 = bits(32) +type imm64 = bits(64) +type generic_imm = bits(64) + +/* union types for operand */ +union reg_or_mem = { + rm_REG: reg_index, + rm_MEM: mem_addr +} +union any = { + rmi_IMM: generic_imm, + rmi_REG: reg_index, + rmi_MEM: mem_addr +} + +/* read operand */ +union exception = { + EUnsupported: string, + EUnreachable: string +} \ No newline at end of file diff --git a/operands.sail b/operands.sail index efd189a..614b2f1 100644 --- a/operands.sail +++ b/operands.sail @@ -1,35 +1,27 @@ -/* range of registers that one can refer to */ -type reg_index = range(0, 15) +// TODO: Implement read and write operand for memory -/* -* Memory addresses are 64 bits, but not all of these are allowed to be used. -* (Must verify that a memory address is valid before use. -* Implementing a flat memory model, so no segmentation.) -*/ -type mem_addr = bits(64) +/* read immediate value from variable bit-extended to 64 bits */ +val read_imm: forall 'm, 'm in {8, 16, 32, 64}. (int('m), generic_imm) -> bits('m) +function read_imm(wsize, imm) = imm[wsize - 1 .. 0] -/* permitted word sizes */ -type word_size = {8,16,32,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 +/* read reg_or_mem operand */ +val read_rm_operand: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_or_mem) -> bits('m) +function read_rm_operand(wsize, operand: reg_or_mem) = { + match operand { + rm_REG(reg_index) => read_reg(wsize, reg_index), + _ => throw(EUnsupported("This operand is not supported")) + } } -/* union types for operand */ -union reg_or_mem = { - rm_REG: reg_index, - rm_MEM: mem_addr +/* read any (reg / mem / imm) operand */ +val read_rmi_operand: forall 'm, 'm in {8, 16, 32, 64}. (int('m), any) -> bits('m) +function read_rmi_operand(wsize, operand: any) = { + match operand { + rmi_IMM(imm) => read_imm(wsize, imm), + rmi_REG(reg_index) => read_reg(wsize, reg_index), + _ => throw(EUnsupported("This operand is not supported")) + } } -union any = { - rmi_IMM: imm, - rmi_REG: reg_index, - rmi_MEM: mem_addr -} \ No newline at end of file + +/* overloaded function to read any operand type present in the ast */ +overload read_operand = {read_rm_operand, read_rmi_operand, read_imm, read_reg} \ No newline at end of file diff --git a/tests.sail b/tests.sail index fd6e09a..7bacbac 100644 --- a/tests.sail +++ b/tests.sail @@ -1,5 +1,5 @@ function main() : unit -> unit = { - let x: imm = IMM16(0x0002); + let x: imm16 = 0x0002; let y: bits(64) = 0x0000_0000_0000_0007; print_bits("",y + 0x0000_0000_0000_0004) } \ No newline at end of file From 7059f4cb3a639b49bd9fcb8419d58f9ad69831ed Mon Sep 17 00:00:00 2001 From: s-prism Date: Tue, 25 Nov 2025 22:57:01 +0000 Subject: [PATCH 04/24] Read and write to operand implemented, minus memory --- operands.sail | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/operands.sail b/operands.sail index 614b2f1..f77a527 100644 --- a/operands.sail +++ b/operands.sail @@ -24,4 +24,16 @@ function read_rmi_operand(wsize, operand: any) = { } /* overloaded function to read any operand type present in the ast */ -overload read_operand = {read_rm_operand, read_rmi_operand, read_imm, read_reg} \ No newline at end of file +overload read_operand = {read_rm_operand, read_rmi_operand, read_imm, read_reg} + +/* write to reg or mem location */ +val write_rm_operand: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_or_mem, bits('m)) -> unit +function write_rm_operand(wsize: operand: reg_or_mem, value) = { + match operand { + rm_REG(reg_index) => write_reg(wsize, operand, value), + _ => throw(EUnsupported("This operand is not supported")) + } +} + +/* overloaded function to write to any register or memory type */ +overload write_operand = {write_rm_operand, write_reg} \ No newline at end of file From 616355099db028218005bf6009285919cb222fdd Mon Sep 17 00:00:00 2001 From: s-prism Date: Wed, 26 Nov 2025 01:07:06 +0000 Subject: [PATCH 05/24] Begin defining memory interface using Sail's concurrency interface --- Makefile | 4 ++-- interface.sail | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++ operands.sail | 4 ++-- 3 files changed, 54 insertions(+), 4 deletions(-) create mode 100644 interface.sail diff --git a/Makefile b/Makefile index d3adaab..728f980 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,5 @@ SAIL_DIR=`sail --dir` -X86_FILES=prelude.sail operand_types.sail registers.sail operands.sail tiny-x86.sail tests.sail +X86_FILES=prelude.sail interface.sail operand_types.sail registers.sail operands.sail tiny-x86.sail tests.sail type-check: sail $(X86_FILES) @@ -10,7 +10,7 @@ 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 operand_types.sail registers.sail operands.sail tiny-x86.sail tests.sail +test.c: prelude.sail interface.sail operand_types.sail registers.sail operands.sail tiny-x86.sail tests.sail sail -c $(X86_FILES) -o test; .PHONY: type-check test \ No newline at end of file diff --git a/interface.sail b/interface.sail new file mode 100644 index 0000000..01bc5bd --- /dev/null +++ b/interface.sail @@ -0,0 +1,50 @@ +$include +$include +$include +$include +$include + +/* + This interface depends on a few parameters: + - mem_acc : Type, An architecture specific description of the access kind. + This may also contain arbitrary architecture specific metadata about the + access. + - CHERI : Bool, Whether CHERI is active on this architecture, which means the + memory has capability tags + - cap_size_log : Int, If CHERI is on, the log2 of the size of capabilities in + bytes. For example for 16 bytes capabilities, this should be 4. +*/ + +// addr_size : Int, The size of addresses to be used, in bits +type addr_size : Int = 64 +let addr_size' : int(64) = 64 + +/* +addr_space : Type, An extra tag on the address to identify its address + space. For Arm this is Secure/Non-Secure, for all other architecture this + should probably be unit. +*/ +type addr_space : Type = unit +let addr_space_def = () + +/* +abort : Type, The type of memory aborts/access failure: To be + returned when the access has failed. In system-level instantiations, this is + expected to be for physical memory abort (e.g. SError in Arm) + +Using a generic name 'Fault' as implementing a simplified memory model +*/ +enum Fault = { + // see 6.5.1 Call and Return Operation for Interrupt or Exception Handling Procedures (Intel manual) + Fault_DB, // Debug + Fault_NMI, // Non-maskable interrupt + Fault_DF, // Double Fault + Fault_NP, // Segment Not Present + Fault_SS, // Stack Segment Fault + Fault_GP, // General Protection + Fault_PF, // Page Fault + Fault_AC, // Alignment Check + Fault_MC, // Machine Check + Fault_CP, // Control Protection Exceptiobn +} +type abort: Type = Fault \ No newline at end of file diff --git a/operands.sail b/operands.sail index f77a527..d912c56 100644 --- a/operands.sail +++ b/operands.sail @@ -28,9 +28,9 @@ overload read_operand = {read_rm_operand, read_rmi_operand, read_imm, read_reg} /* write to reg or mem location */ val write_rm_operand: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_or_mem, bits('m)) -> unit -function write_rm_operand(wsize: operand: reg_or_mem, value) = { +function write_rm_operand(wsize, operand: reg_or_mem, value) = { match operand { - rm_REG(reg_index) => write_reg(wsize, operand, value), + rm_REG(reg_index) => write_reg(wsize, reg_index, value), _ => throw(EUnsupported("This operand is not supported")) } } From 2fddb23e89455e08793dd700fd389f61ab47d4fc Mon Sep 17 00:00:00 2001 From: s-prism Date: Wed, 26 Nov 2025 15:39:13 +0000 Subject: [PATCH 06/24] Adding to sequential memory model --- Makefile | 4 +-- interface.sail | 87 ++++++++++++++++++++++++++++++++++++++++++++++---- prelude.sail | 6 ++++ registers.sail | 37 ++++++++++++++++----- 4 files changed, 118 insertions(+), 16 deletions(-) diff --git a/Makefile b/Makefile index 728f980..3b23262 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,5 @@ SAIL_DIR=`sail --dir` -X86_FILES=prelude.sail interface.sail operand_types.sail registers.sail operands.sail tiny-x86.sail tests.sail +X86_FILES=prelude.sail operand_types.sail registers.sail interface.sail operands.sail tiny-x86.sail tests.sail type-check: sail $(X86_FILES) @@ -10,7 +10,7 @@ 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 interface.sail operand_types.sail registers.sail operands.sail tiny-x86.sail tests.sail +test.c: prelude.sail operand_types.sail registers.sail interface.sail operands.sail tiny-x86.sail tests.sail sail -c $(X86_FILES) -o test; .PHONY: type-check test \ No newline at end of file diff --git a/interface.sail b/interface.sail index 01bc5bd..b50cecb 100644 --- a/interface.sail +++ b/interface.sail @@ -6,9 +6,6 @@ $include /* This interface depends on a few parameters: - - mem_acc : Type, An architecture specific description of the access kind. - This may also contain arbitrary architecture specific metadata about the - access. - CHERI : Bool, Whether CHERI is active on this architecture, which means the memory has capability tags - cap_size_log : Int, If CHERI is on, the log2 of the size of capabilities in @@ -31,8 +28,6 @@ let addr_space_def = () abort : Type, The type of memory aborts/access failure: To be returned when the access has failed. In system-level instantiations, this is expected to be for physical memory abort (e.g. SError in Arm) - -Using a generic name 'Fault' as implementing a simplified memory model */ enum Fault = { // see 6.5.1 Call and Return Operation for Interrupt or Exception Handling Procedures (Intel manual) @@ -47,4 +42,84 @@ enum Fault = { Fault_MC, // Machine Check Fault_CP, // Control Protection Exceptiobn } -type abort: Type = Fault \ No newline at end of file +type abort: Type = Fault + +/* + - 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, + cpl: bits(2), // current privilege level + acqsc : bool, + acqpc : bool, + relsc : bool, + exclusive : bool, + atomicop : bool, + read : bool, + write : bool, +} +function base_AccessDescriptor (acctype : AccessType) -> AccessDescriptor = struct { + acctype = acctype, + cpl = 0b11, // lowest privilege level + acqsc = true, // acquire (load / read) sequential consistency applied + acqpc = false, // acquire with processor consistency (weaker than sequential consistency) + relsc = true, // release (store / write) sequential consistency applied + exclusive = false, + atomicop = false, + read = false, + write = false, +} +function create_iFetchAccessDescriptor() -> AccessDescriptor = { + var accdesc = base_AccessDescriptor(AccessType_IFETCH); + accdesc.read = true; + accdesc.write = false; + accdesc.cpl = CS[CPL]; + accdesc +} +function create_readAccessDescriptor() -> AccessDescriptor = { + var accdesc = base_AccessDescriptor(AccessType_RW); + accdesc.read = true; + accdesc.write = false; + accdesc.cpl = CS[CPL]; + accdesc +} +function create_writeAccessDescriptor() -> AccessDescriptor = { + var accdesc = base_AccessDescriptor(AccessType_RW); + accdesc.write = true; + accdesc.read = false; + accdesc.cpl = CS[CPL]; + 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 (can be reordered by hardware). False as we are implementing a model with sequential consistency. +function mem_acc_is_relaxed (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_RW & not_bool(acc.acqpc) & not_bool(acc.acqsc) & not_bool(acc.relsc) + +// Access is release acquire rcpc = release consistent processor consistent +function mem_acc_is_rel_acq_rcpc (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_RW & acc.acqpc + +// Access is release acquire rcsc = release consistent sequentially consistent +function mem_acc_is_rel_acq_rcsc (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_RW & (acc.acqsc | acc.relsc) + +// 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 & not_bool(acc.exclusive) & not_bool(acc.atomicop) + +// access is part of an exclusive instruction +function mem_acc_is_exclusive (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_RW & acc.exclusive + +// 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 \ No newline at end of file diff --git a/prelude.sail b/prelude.sail index fdb7921..65dd247 100644 --- a/prelude.sail +++ b/prelude.sail @@ -1,2 +1,8 @@ default Order dec // LSB is index 0 $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} \ No newline at end of file diff --git a/registers.sail b/registers.sail index e7e45ee..909ba4a 100644 --- a/registers.sail +++ b/registers.sail @@ -41,14 +41,35 @@ 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 +/* register RFLAGS, system and status flags + mostly restricted access */ +bitfield rflags : bits(64) = { + // system flags and IOPL field + ID: 21, + VIP: 20, + VIF: 19, + AC: 18, + VM: 17, + RF: 16, + NT: 14, + IOPL: 13 .. 12, + IF: 9, + TF: 8, + + // status flags + OF: 11, + SF: 7, + ZF: 6, + AF: 4, + PF: 2, + CF: 0 +} +register RFLAGS: rflags + +/* Code Segment register - bits 0-1 contain CPL (Current Provilege Level) of the currently executing program*/ +bitfield cs: bits(16) = { + CPL: 1 .. 0 +} +register CS: cs /* read and write least-significant 8,16,32,64 (32 with 0 extend for write) bits From c2304571651d02109207a154be585148d265db3c Mon Sep 17 00:00:00 2001 From: s-prism Date: Wed, 26 Nov 2025 17:47:58 +0000 Subject: [PATCH 07/24] More progress made on memory --- interface.sail | 67 +++++++++++++++++++++++++++++++++++++++++--------- prelude.sail | 2 ++ 2 files changed, 57 insertions(+), 12 deletions(-) diff --git a/interface.sail b/interface.sail index b50cecb..ef72f73 100644 --- a/interface.sail +++ b/interface.sail @@ -30,17 +30,17 @@ abort : Type, The type of memory aborts/access failure: To be expected to be for physical memory abort (e.g. SError in Arm) */ enum Fault = { - // see 6.5.1 Call and Return Operation for Interrupt or Exception Handling Procedures (Intel manual) - Fault_DB, // Debug - Fault_NMI, // Non-maskable interrupt - Fault_DF, // Double Fault - Fault_NP, // Segment Not Present - Fault_SS, // Stack Segment Fault - Fault_GP, // General Protection - Fault_PF, // Page Fault - Fault_AC, // Alignment Check - Fault_MC, // Machine Check - Fault_CP, // Control Protection Exceptiobn + // see 6.5.1 Call and Return Operation for Interrupt or Exception Handling Procedures (Intel manual) + Fault_DB, // Debug + Fault_NMI, // Non-maskable interrupt + Fault_DF, // Double Fault + Fault_NP, // Segment Not Present + Fault_SS, // Stack Segment Fault + Fault_GP, // General Protection + Fault_PF, // Page Fault + Fault_AC, // Alignment Check + Fault_MC, // Machine Check + Fault_CP, // Control Protection Exception } type abort: Type = Fault @@ -122,4 +122,47 @@ function mem_acc_is_standalone (acc : AccessDescriptor) -> bool = acc.acctype function mem_acc_is_exclusive (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_RW & acc.exclusive // 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 \ No newline at end of file +function mem_acc_is_atomic_rmw (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_RW & acc.atomicop + +/* instantiate */ +instantiation sail_mem_read with + 'addr_size = addr_size, + 'addr_space = addr_space, + 'mem_acc = AccessDescriptor, + 'abort = abort, + '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 = addr_size, + 'addr_space = addr_space, + 'mem_acc = AccessDescriptor, + 'abort = abort, + '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_address_announce with + 'addr_size = addr_size, + 'addr_space = addr_space, + 'mem_acc = AccessDescriptor, + 'abort = abort, + 'CHERI = false, + 'cap_size_log = 0 \ No newline at end of file diff --git a/prelude.sail b/prelude.sail index 65dd247..a359b3a 100644 --- a/prelude.sail +++ b/prelude.sail @@ -1,6 +1,8 @@ default Order dec // LSB is index 0 $include +$define CONCURRENCY_INTERFACE_V2 // use concurrency_interface/read_write_v2.sail instead of v1 + // 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 From 427f15062f87d746c38076f32e3131065ad2ceb1 Mon Sep 17 00:00:00 2001 From: s-prism Date: Thu, 27 Nov 2025 01:54:40 +0000 Subject: [PATCH 08/24] Progress made on memory read and write --- interface.sail | 52 ++++++++++++++++++++++++++++++++++++++++++++++++-- operands.sail | 11 +++++++++++ prelude.sail | 3 +-- tests.sail | 3 ++- 4 files changed, 64 insertions(+), 5 deletions(-) diff --git a/interface.sail b/interface.sail index ef72f73..6d7ed16 100644 --- a/interface.sail +++ b/interface.sail @@ -1,8 +1,9 @@ $include $include -$include +$include $include $include +$include /* This interface depends on a few parameters: @@ -165,4 +166,51 @@ instantiation sail_mem_address_announce with 'mem_acc = AccessDescriptor, 'abort = abort, 'CHERI = false, - 'cap_size_log = 0 \ No newline at end of file + 'cap_size_log = 0 + +/* memory read and write */ +val iFetch : forall 'm, 'm >=1 & 'm <= 8. (bits(addr_size), int('m), AccessDescriptor) -> bits(8 * 'm) +val rMem : forall 'm, 'm in {1, 2, 4, 8}. (bits(addr_size), int('m), AccessDescriptor) -> bits(8 * 'm) +val wMem_Addr : (bits(addr_size)) -> unit +val wMem : forall 'm, 'm in {1, 2, 4, 8}. (bits(addr_size), int('m), bits(8 * 'm), AccessDescriptor) -> unit +val translate_address : (bits(64), AccessDescriptor) -> option(bits(addr_size)) + +val read_memory : forall 'N, 'N > 0. + (int('N), bits(addr_size), AccessDescriptor) -> bits('N * 8) + +function read_memory(N, addr, accdesc) = { + let req : Mem_read_request('N, 0, addr_size, addr_space, AccessDescriptor) = struct { + access_kind = accdesc, + address = truncate(addr, addr_size'), + address_space = addr_space_def, + size = N, + num_tag = 0 + }; + + match sail_mem_read(req) { + Ok((bytes, _)) => from_bytes_le(bytes), + Err(_e) => { exit() } + } +} + +function iFetch(addr, bytes, accdesc) = read_memory(bytes, addr, accdesc) + +function rMem(addr, bytes, accdesc) = read_memory(bytes, addr, accdesc) + +function wMem_Addr(addr) = sail_address_announce(64, sail_zero_extend(addr, 64)) + +function wMem(addr, bytes, value, accdesc) = { + let req : Mem_write_request('m, 0, addr_size, addr_space, AccessDescriptor) = struct { + access_kind = accdesc, + address = truncate(addr, addr_size'), + address_space = addr_space_def, + size = bytes, + num_tag = 0, + value = to_bytes_le(bytes, value), + tags = [] + }; + match sail_mem_write(req) { + Ok(_) => (), + Err(_) => exit(), + } +} \ No newline at end of file diff --git a/operands.sail b/operands.sail index d912c56..fe81bff 100644 --- a/operands.sail +++ b/operands.sail @@ -4,11 +4,22 @@ val read_imm: forall 'm, 'm in {8, 16, 32, 64}. (int('m), generic_imm) -> bits('m) function read_imm(wsize, imm) = imm[wsize - 1 .. 0] +function bits_to_bytes(value: {8, 16, 32, 64}) -> int = { + match value { + 8 => 1, + 16 => 2, + 32 => 4, + 64 => 8 + } +} + /* read reg_or_mem operand */ val read_rm_operand: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_or_mem) -> bits('m) function read_rm_operand(wsize, operand: reg_or_mem) = { + let wsize_bytes = fdiv_int(wsize,8); match operand { rm_REG(reg_index) => read_reg(wsize, reg_index), + // rm_MEM(mem_addr) => rMem(mem_addr, wsize, create_readAccessDescriptor()), _ => throw(EUnsupported("This operand is not supported")) } } diff --git a/prelude.sail b/prelude.sail index a359b3a..adcb621 100644 --- a/prelude.sail +++ b/prelude.sail @@ -1,7 +1,6 @@ default Order dec // LSB is index 0 -$include - $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 diff --git a/tests.sail b/tests.sail index 7bacbac..ecfa40b 100644 --- a/tests.sail +++ b/tests.sail @@ -1,5 +1,6 @@ function main() : unit -> unit = { let x: imm16 = 0x0002; let y: bits(64) = 0x0000_0000_0000_0007; - print_bits("",y + 0x0000_0000_0000_0004) + print_bits("",y + 0x0000_0000_0000_0004); + print_int("", fdiv_int(17,8)) } \ No newline at end of file From b80368886587f0d5513dedabe4a450dc7450ac05 Mon Sep 17 00:00:00 2001 From: s-prism Date: Thu, 27 Nov 2025 16:15:29 +0000 Subject: [PATCH 09/24] Removed unnecessary code + code cleanup. Interface for read and write mem functions exist --- .gitignore | 1 + Makefile | 4 +- interface.sail | 134 +++++++++------------------------------------ operand_types.sail | 36 ------------ operands.sail | 69 +++++++++++++++-------- prelude.sail | 5 +- registers.sail | 9 +-- tiny-x86.sail | 16 +++--- 8 files changed, 90 insertions(+), 184 deletions(-) delete mode 100644 operand_types.sail diff --git a/.gitignore b/.gitignore index 7d5969f..5ca479f 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ *z3_problems test.* +sail_smt_cache diff --git a/Makefile b/Makefile index 3b23262..e58353f 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,5 @@ SAIL_DIR=`sail --dir` -X86_FILES=prelude.sail operand_types.sail registers.sail interface.sail operands.sail tiny-x86.sail tests.sail +X86_FILES=prelude.sail registers.sail interface.sail operands.sail tiny-x86.sail tests.sail type-check: sail $(X86_FILES) @@ -10,7 +10,7 @@ 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 operand_types.sail registers.sail interface.sail operands.sail tiny-x86.sail tests.sail +test.c: prelude.sail registers.sail interface.sail operands.sail tiny-x86.sail tests.sail sail -c $(X86_FILES) -o test; .PHONY: type-check test \ No newline at end of file diff --git a/interface.sail b/interface.sail index 6d7ed16..92af93d 100644 --- a/interface.sail +++ b/interface.sail @@ -1,49 +1,4 @@ $include -$include -$include -$include -$include -$include - -/* - This interface depends on a few parameters: - - CHERI : Bool, Whether CHERI is active on this architecture, which means the - memory has capability tags - - cap_size_log : Int, If CHERI is on, the log2 of the size of capabilities in - bytes. For example for 16 bytes capabilities, this should be 4. -*/ - -// addr_size : Int, The size of addresses to be used, in bits -type addr_size : Int = 64 -let addr_size' : int(64) = 64 - -/* -addr_space : Type, An extra tag on the address to identify its address - space. For Arm this is Secure/Non-Secure, for all other architecture this - should probably be unit. -*/ -type addr_space : Type = unit -let addr_space_def = () - -/* -abort : Type, The type of memory aborts/access failure: To be - returned when the access has failed. In system-level instantiations, this is - expected to be for physical memory abort (e.g. SError in Arm) -*/ -enum Fault = { - // see 6.5.1 Call and Return Operation for Interrupt or Exception Handling Procedures (Intel manual) - Fault_DB, // Debug - Fault_NMI, // Non-maskable interrupt - Fault_DF, // Double Fault - Fault_NP, // Segment Not Present - Fault_SS, // Stack Segment Fault - Fault_GP, // General Protection - Fault_PF, // Page Fault - Fault_AC, // Alignment Check - Fault_MC, // Machine Check - Fault_CP, // Control Protection Exception -} -type abort: Type = Fault /* - mem_acc : Type, An architecture specific description of the access kind. @@ -56,45 +11,31 @@ enum AccessType = { } struct AccessDescriptor = { acctype : AccessType, - cpl: bits(2), // current privilege level - acqsc : bool, - acqpc : bool, - relsc : bool, - exclusive : bool, atomicop : bool, + standalone: bool, read : bool, write : bool, } function base_AccessDescriptor (acctype : AccessType) -> AccessDescriptor = struct { acctype = acctype, - cpl = 0b11, // lowest privilege level - acqsc = true, // acquire (load / read) sequential consistency applied - acqpc = false, // acquire with processor consistency (weaker than sequential consistency) - relsc = true, // release (store / write) sequential consistency applied - exclusive = false, atomicop = false, + standalone = true, read = false, write = false, } function create_iFetchAccessDescriptor() -> AccessDescriptor = { var accdesc = base_AccessDescriptor(AccessType_IFETCH); accdesc.read = true; - accdesc.write = false; - accdesc.cpl = CS[CPL]; accdesc } function create_readAccessDescriptor() -> AccessDescriptor = { var accdesc = base_AccessDescriptor(AccessType_RW); accdesc.read = true; - accdesc.write = false; - accdesc.cpl = CS[CPL]; accdesc } function create_writeAccessDescriptor() -> AccessDescriptor = { var accdesc = base_AccessDescriptor(AccessType_RW); accdesc.write = true; - accdesc.read = false; - accdesc.cpl = CS[CPL]; accdesc } @@ -107,30 +48,28 @@ function mem_acc_is_ifetch (acc : AccessDescriptor) -> bool = acc.acctype // 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 (can be reordered by hardware). False as we are implementing a model with sequential consistency. -function mem_acc_is_relaxed (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_RW & not_bool(acc.acqpc) & not_bool(acc.acqsc) & not_bool(acc.relsc) - -// Access is release acquire rcpc = release consistent processor consistent -function mem_acc_is_rel_acq_rcpc (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_RW & acc.acqpc +// Access is relaxed +function mem_acc_is_relaxed (acc : AccessDescriptor) -> bool = true -// Access is release acquire rcsc = release consistent sequentially consistent -function mem_acc_is_rel_acq_rcsc (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_RW & (acc.acqsc | acc.relsc) +// 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 & not_bool(acc.exclusive) & not_bool(acc.atomicop) +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 = acc.acctype == AccessType_RW & acc.exclusive +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 = addr_size, - 'addr_space = addr_space, + 'addr_size = 64, + 'addr_space = unit, 'mem_acc = AccessDescriptor, - 'abort = abort, + 'abort = unit, 'CHERI = false, 'cap_size_log = 0, mem_acc_is_explicit = mem_acc_is_explicit, @@ -144,10 +83,10 @@ instantiation sail_mem_read with mem_acc_is_atomic_rmw = mem_acc_is_atomic_rmw instantiation sail_mem_write with - 'addr_size = addr_size, - 'addr_space = addr_space, + 'addr_size = 64, + 'addr_space = unit, 'mem_acc = AccessDescriptor, - 'abort = abort, + 'abort = unit, 'CHERI = false, 'cap_size_log = 0, mem_acc_is_explicit = mem_acc_is_explicit, @@ -160,29 +99,15 @@ instantiation sail_mem_write with mem_acc_is_exclusive = mem_acc_is_exclusive, mem_acc_is_atomic_rmw = mem_acc_is_atomic_rmw -instantiation sail_mem_address_announce with - 'addr_size = addr_size, - 'addr_space = addr_space, - 'mem_acc = AccessDescriptor, - 'abort = abort, - 'CHERI = false, - 'cap_size_log = 0 - /* memory read and write */ -val iFetch : forall 'm, 'm >=1 & 'm <= 8. (bits(addr_size), int('m), AccessDescriptor) -> bits(8 * 'm) -val rMem : forall 'm, 'm in {1, 2, 4, 8}. (bits(addr_size), int('m), AccessDescriptor) -> bits(8 * 'm) -val wMem_Addr : (bits(addr_size)) -> unit -val wMem : forall 'm, 'm in {1, 2, 4, 8}. (bits(addr_size), int('m), bits(8 * 'm), AccessDescriptor) -> unit -val translate_address : (bits(64), AccessDescriptor) -> option(bits(addr_size)) - val read_memory : forall 'N, 'N > 0. - (int('N), bits(addr_size), AccessDescriptor) -> bits('N * 8) + (int('N), bits(64), AccessDescriptor) -> bits(8 * 'N) function read_memory(N, addr, accdesc) = { - let req : Mem_read_request('N, 0, addr_size, addr_space, AccessDescriptor) = struct { + let req : Mem_request('N, 0, 64, unit, AccessDescriptor) = struct { access_kind = accdesc, - address = truncate(addr, addr_size'), - address_space = addr_space_def, + address = truncate(addr, 64), + address_space = (), size = N, num_tag = 0 }; @@ -193,23 +118,16 @@ function read_memory(N, addr, accdesc) = { } } -function iFetch(addr, bytes, accdesc) = read_memory(bytes, addr, accdesc) - -function rMem(addr, bytes, accdesc) = read_memory(bytes, addr, accdesc) - -function wMem_Addr(addr) = sail_address_announce(64, sail_zero_extend(addr, 64)) - -function wMem(addr, bytes, value, accdesc) = { - let req : Mem_write_request('m, 0, addr_size, addr_space, AccessDescriptor) = struct { +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, addr_size'), - address_space = addr_space_def, - size = bytes, + address = truncate(addr, 64), + address_space = (), + size = N, num_tag = 0, - value = to_bytes_le(bytes, value), - tags = [] }; - match sail_mem_write(req) { + match sail_mem_write(req,to_bytes_le(N, value),[]) { Ok(_) => (), Err(_) => exit(), } diff --git a/operand_types.sail b/operand_types.sail deleted file mode 100644 index 96981da..0000000 --- a/operand_types.sail +++ /dev/null @@ -1,36 +0,0 @@ -/* range of registers that one can refer to */ -type reg_index = range(0, 15) - -/* -* Memory addresses are 64 bits, but not all of these are allowed to be used. -* (Must verify that a memory address is valid before use. -* Implementing a flat memory model, so no segmentation.) -*/ -type mem_addr = bits(64) - -/* permitted word sizes */ -type word_size = {8,16,32,64} - -/* immediate value types */ -type imm8 = bits(8) -type imm16 = bits(16) -type imm32 = bits(32) -type imm64 = bits(64) -type generic_imm = bits(64) - -/* union types for operand */ -union reg_or_mem = { - rm_REG: reg_index, - rm_MEM: mem_addr -} -union any = { - rmi_IMM: generic_imm, - rmi_REG: reg_index, - rmi_MEM: mem_addr -} - -/* read operand */ -union exception = { - EUnsupported: string, - EUnreachable: string -} \ No newline at end of file diff --git a/operands.sail b/operands.sail index fe81bff..7f0eb88 100644 --- a/operands.sail +++ b/operands.sail @@ -1,36 +1,57 @@ -// TODO: Implement read and write operand for memory +/* +* Memory addresses are 64 bits, but not all of these are allowed to be used. +* (Must verify that a memory address is valid before use. +* Implementing a flat memory model, so no segmentation.) +*/ +type mem_addr = bits(64) + +/* immediate value types */ +type imm8 = bits(8) +type imm16 = bits(16) +type imm32 = bits(32) +type imm64 = bits(64) +type generic_imm = bits(64) + +/* 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: generic_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), generic_imm) -> bits('m) function read_imm(wsize, imm) = imm[wsize - 1 .. 0] -function bits_to_bytes(value: {8, 16, 32, 64}) -> int = { - match value { - 8 => 1, - 16 => 2, - 32 => 4, - 64 => 8 - } -} - -/* read reg_or_mem operand */ -val read_rm_operand: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_or_mem) -> bits('m) -function read_rm_operand(wsize, operand: reg_or_mem) = { - let wsize_bytes = fdiv_int(wsize,8); +/* 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 = tdiv_int(wsize,8); + assert('m == wsize_bytes * 8); // required for type-checking match operand { rm_REG(reg_index) => read_reg(wsize, reg_index), - // rm_MEM(mem_addr) => rMem(mem_addr, wsize, create_readAccessDescriptor()), - _ => throw(EUnsupported("This operand is not supported")) + rm_MEM(mem_addr) => read_memory(wsize_bytes, mem_addr, create_readAccessDescriptor()), } } -/* read any (reg / mem / imm) operand */ -val read_rmi_operand: forall 'm, 'm in {8, 16, 32, 64}. (int('m), any) -> bits('m) -function read_rmi_operand(wsize, operand: any) = { +/* 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 = tdiv_int(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_reg(wsize, reg_index), - _ => throw(EUnsupported("This operand is not supported")) + rmi_MEM(mem_addr) => read_memory(wsize_bytes, mem_addr, create_readAccessDescriptor()), } } @@ -38,11 +59,13 @@ function read_rmi_operand(wsize, operand: any) = { overload read_operand = {read_rm_operand, read_rmi_operand, read_imm, read_reg} /* write to reg or mem location */ -val write_rm_operand: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_or_mem, bits('m)) -> unit -function write_rm_operand(wsize, operand: reg_or_mem, value) = { +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 = tdiv_int(wsize,8); + assert('m == wsize_bytes * 8); // required for type-checking match operand { rm_REG(reg_index) => write_reg(wsize, reg_index, value), - _ => throw(EUnsupported("This operand is not supported")) + rm_MEM(mem_addr) => write_memory(wsize_bytes, mem_addr, value, create_writeAccessDescriptor()), } } diff --git a/prelude.sail b/prelude.sail index adcb621..46fdf6e 100644 --- a/prelude.sail +++ b/prelude.sail @@ -6,4 +6,7 @@ $include 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} \ No newline at end of file +overload operator == = {eq_any, eq_bits_int} + +val fail: string -> unit +function fail(message) = assert(false, message) \ No newline at end of file diff --git a/registers.sail b/registers.sail index 909ba4a..c123ce4 100644 --- a/registers.sail +++ b/registers.sail @@ -1,3 +1,6 @@ +/* range of registers that one can refer to */ +type reg_index = range(0, 15) + /* program counter */ register RIP: bits(64) @@ -65,12 +68,6 @@ bitfield rflags : bits(64) = { } register RFLAGS: rflags -/* Code Segment register - bits 0-1 contain CPL (Current Provilege Level) of the currently executing program*/ -bitfield cs: bits(16) = { - CPL: 1 .. 0 -} -register CS: cs - /* read and write least-significant 8,16,32,64 (32 with 0 extend for write) bits */ diff --git a/tiny-x86.sail b/tiny-x86.sail index 2f63c9a..f87988b 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) - MOV: (word_size, reg_or_mem, any), - XOR: (word_size, reg_or_mem, any), + MOV: (word_size, rm_operand, rmi_operand), + XOR: (word_size, rm_operand, rmi_operand), SFENCE: unit, LFENCE: unit, MFENCE: unit, - CMP: (word_size, reg_or_mem, any), - PUSH: (word_size, any), - POP: (word_size, reg_or_mem), - ADD: (word_size, reg_or_mem, any), - SUB: (word_size, reg_or_mem, any), - IMUL: (word_size, reg_index, reg_or_mem), // IMUL with only 2 arguments (dest and src) + CMP: (word_size, rm_operand, rmi_operand), + PUSH: (word_size, rmi_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) LEAVE: unit, RET: unit, JMP_short: imm8, From 3e829b3ddb0a6fa0a7602b266cd863c97af61ccb Mon Sep 17 00:00:00 2001 From: s-prism Date: Fri, 28 Nov 2025 16:56:30 +0000 Subject: [PATCH 10/24] Added test for memory read and write --- operands.sail | 6 +----- tests.sail | 13 +++++++++---- 2 files changed, 10 insertions(+), 9 deletions(-) diff --git a/operands.sail b/operands.sail index 7f0eb88..8b6a0f3 100644 --- a/operands.sail +++ b/operands.sail @@ -1,8 +1,4 @@ -/* -* Memory addresses are 64 bits, but not all of these are allowed to be used. -* (Must verify that a memory address is valid before use. -* Implementing a flat memory model, so no segmentation.) -*/ +/* Memory addresses are 64 bits. Assume all possible addresses can be used. */ type mem_addr = bits(64) /* immediate value types */ diff --git a/tests.sail b/tests.sail index ecfa40b..2ae50ba 100644 --- a/tests.sail +++ b/tests.sail @@ -1,6 +1,11 @@ +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 main() : unit -> unit = { - let x: imm16 = 0x0002; - let y: bits(64) = 0x0000_0000_0000_0007; - print_bits("",y + 0x0000_0000_0000_0004); - print_int("", fdiv_int(17,8)) + write_then_read_mem() } \ No newline at end of file From 0d19506e266777050ef87adb6b318d5ed881fd50 Mon Sep 17 00:00:00 2001 From: s-prism Date: Sat, 29 Nov 2025 14:31:35 +0000 Subject: [PATCH 11/24] Added sail barrier and started defining execute function --- interface.sail | 12 +++++++- prelude.sail | 7 ++++- registers.sail | 32 +++++++++++++-------- tiny-x86.sail | 75 ++++++++++++++++++++++++++++++++++++++++++++++++-- 4 files changed, 110 insertions(+), 16 deletions(-) diff --git a/interface.sail b/interface.sail index 92af93d..25e9b55 100644 --- a/interface.sail +++ b/interface.sail @@ -131,4 +131,14 @@ function write_memory(N, addr, value, accdesc) = { Ok(_) => (), Err(_) => exit(), } -} \ No newline at end of file +} + +/* memory barrier */ +enum Barrier = { + Barrier_SFENCE, // store fence + Barrier_LFENCE, // load fence + Barrier_MFENCE // memory fence +} + +instantiation sail_barrier with + 'barrier = Barrier \ No newline at end of file diff --git a/prelude.sail b/prelude.sail index 46fdf6e..198523e 100644 --- a/prelude.sail +++ b/prelude.sail @@ -9,4 +9,9 @@ function eq_bits_int (x, y) = (unsigned(x) == y) overload operator == = {eq_any, eq_bits_int} val fail: string -> unit -function fail(message) = assert(false, message) \ No newline at end of file +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; +} \ No newline at end of file diff --git a/registers.sail b/registers.sail index c123ce4..e0bec2b 100644 --- a/registers.sail +++ b/registers.sail @@ -59,19 +59,16 @@ bitfield rflags : bits(64) = { TF: 8, // status flags - OF: 11, - SF: 7, - ZF: 6, - AF: 4, - PF: 2, - CF: 0 + OF: 11, // overflow flag + SF: 7, // sign flag + ZF: 6, // zero flag + AF: 4, // auxiliary carry flag + PF: 2, // parity flag + CF: 0 // carry flag } register RFLAGS: rflags -/* -read and write least-significant 8,16,32,64 (32 with 0 extend for write) bits - */ - +/* read and write least-significant 8,16,32,64 (32 with 0 extend for write) bits */ val read_reg: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_index) -> bits('m) function read_reg(wsize, i: reg_index) = { @@ -84,10 +81,21 @@ val write_reg: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_index, bits('m)) function write_reg(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; +} + +/* 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]; } \ No newline at end of file diff --git a/tiny-x86.sail b/tiny-x86.sail index f87988b..f0070db 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -1,5 +1,6 @@ union ast = { - // if one of the types is a tuple with first element word_size, the tuple represents (word_size, dest, src) + // 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 MOV: (word_size, rm_operand, rmi_operand), XOR: (word_size, rm_operand, rmi_operand), SFENCE: unit, @@ -16,4 +17,74 @@ union ast = { JMP_short: imm8, JNS_short: imm8, CALL: imm32 -} \ No newline at end of file +} + +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"); + + assert(match (dest, src) { + (rm_MEM(x), rmi_MEM(y)) => false, + _ => true + }, 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"); + // 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"); + // 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 + if result == sail_zero_extend(0x0, wsize) then + RFLAGS[ZF] = 0b1 + else + RFLAGS[ZF] = 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(SFENCE()) = { + // apply barrier + sail_barrier(Barrier_SFENCE) +} + +function clause execute(LFENCE()) = { + // apply barrier + sail_barrier(Barrier_LFENCE) +} + +function clause execute(MFENCE()) = { + // apply barrier + sail_barrier(Barrier_MFENCE) +} + +function clause execute(CMP(wsize, first, second)) = { + fail_if_two_mem_operands(first, second, "CMP"); + let first_val = read_operand(wsize, first); + let second_val = read_operand(wsize, second); + + // TODO: complete this function +} + +end execute \ No newline at end of file From 34d14682d25ba1ce581c011264242359cda0d913 Mon Sep 17 00:00:00 2001 From: s-prism <166765868+s-prism@users.noreply.github.com> Date: Sat, 29 Nov 2025 16:36:10 +0000 Subject: [PATCH 12/24] Finished defining execute for CMP instruction --- registers.sail | 4 ++-- tiny-x86.sail | 25 ++++++++++++++++++++----- 2 files changed, 22 insertions(+), 7 deletions(-) diff --git a/registers.sail b/registers.sail index e0bec2b..3bb2f79 100644 --- a/registers.sail +++ b/registers.sail @@ -59,12 +59,12 @@ bitfield rflags : bits(64) = { TF: 8, // status flags - OF: 11, // overflow flag + 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 + CF: 0 // carry flag (for operations between unsigned values) } register RFLAGS: rflags diff --git a/tiny-x86.sail b/tiny-x86.sail index f0070db..969e1c2 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -56,35 +56,50 @@ function clause execute(XOR(wsize, dest, src)) = { // sign flag = msb of result (0 = +ve, 1 = -ve) RFLAGS[SF] = [result[wsize - 1]]; // set zero flag if result = 0, else clear zero flag - if result == sail_zero_extend(0x0, wsize) then - RFLAGS[ZF] = 0b1 - else - RFLAGS[ZF] = 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); } +// 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"); let first_val = read_operand(wsize, first); let second_val = read_operand(wsize, second); + // execute CMP instruction + let result = sub_bits(first_val, second_val); - // TODO: complete this function + /* 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); } end execute \ No newline at end of file From 97e23990d45f782c01bc0bb7e6168d2f258bf9bf Mon Sep 17 00:00:00 2001 From: s-prism <166765868+s-prism@users.noreply.github.com> Date: Sun, 30 Nov 2025 18:25:31 +0000 Subject: [PATCH 13/24] More progress on execute function --- operands.sail | 6 +++--- prelude.sail | 2 ++ tiny-x86.sail | 39 +++++++++++++++++++++++++++++++++++++++ 3 files changed, 44 insertions(+), 3 deletions(-) diff --git a/operands.sail b/operands.sail index 8b6a0f3..98b9274 100644 --- a/operands.sail +++ b/operands.sail @@ -31,7 +31,7 @@ function read_imm(wsize, imm) = imm[wsize - 1 .. 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 = tdiv_int(wsize,8); + let wsize_bytes = wsize / 8; assert('m == wsize_bytes * 8); // required for type-checking match operand { rm_REG(reg_index) => read_reg(wsize, reg_index), @@ -42,7 +42,7 @@ function read_rm_operand(wsize, operand: rm_operand) = { /* 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 = tdiv_int(wsize,8); + let wsize_bytes = wsize / 8; assert('m == wsize_bytes * 8); // required for type-checking match operand { rmi_IMM(imm) => read_imm(wsize, imm), @@ -57,7 +57,7 @@ overload read_operand = {read_rm_operand, read_rmi_operand, read_imm, read_reg} /* 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 = tdiv_int(wsize,8); + let wsize_bytes = wsize / 8; assert('m == wsize_bytes * 8); // required for type-checking match operand { rm_REG(reg_index) => write_reg(wsize, reg_index, value), diff --git a/prelude.sail b/prelude.sail index 198523e..01ad807 100644 --- a/prelude.sail +++ b/prelude.sail @@ -8,6 +8,8 @@ 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) diff --git a/tiny-x86.sail b/tiny-x86.sail index 969e1c2..547216e 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -102,4 +102,43 @@ function clause execute(CMP(wsize, first, second)) = { modify_parity_flag(result); } +function clause execute(PUSH(wsize, src)) = { + // PUSH instruction does not allow src = imm64, reg8 or mem8 + match src { + rmi_IMM(operand) if wsize == 64 => fail("Operand for PUSH operation not supported"), + rmi_REG(operand) if wsize == 8 => fail("Operand for PUSH operation not supported"), + rmi_MEM(operand) if wsize == 8 => fail("Operand for PUSH operation not supported") + }; + + let src_val = read_operand(wsize, src); + let wsize_bytes = wsize / 8; + RSP = sub_bits(RSP, get_slice_int(64, wsize_bytes, 0)); + let dest_address = rm_MEM(RSP); + write_operand(wsize, dest_address, src_val) +} + +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"); + let dest_val = read_operand(wsize, dest); + let src_val = read_operand(wsize, src); + // execute SUB instruction + 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); +} + end execute \ No newline at end of file From b2221123b7c64a326c6f007f2e86729d60be7737 Mon Sep 17 00:00:00 2001 From: s-prism <166765868+s-prism@users.noreply.github.com> Date: Mon, 1 Dec 2025 19:30:09 +0000 Subject: [PATCH 14/24] Enforced stricter requirements on imm operands --- operands.sail | 33 +++++++++++++++++++++++++++++---- tiny-x86.sail | 37 +++++++++++++++++++++++++++---------- 2 files changed, 56 insertions(+), 14 deletions(-) diff --git a/operands.sail b/operands.sail index 98b9274..46306d1 100644 --- a/operands.sail +++ b/operands.sail @@ -6,7 +6,12 @@ type imm8 = bits(8) type imm16 = bits(16) type imm32 = bits(32) type imm64 = bits(64) -type generic_imm = bits(64) +union imm = { + IMM8: imm8, + IMM16: imm16, + IMM32: imm32, + IMM64: imm64 +} /* union types for operand */ // register or memory operand @@ -16,7 +21,7 @@ union rm_operand = { } // register, memory, or immediate operand union rmi_operand = { - rmi_IMM: generic_imm, + rmi_IMM: imm, rmi_REG: reg_index, rmi_MEM: mem_addr } @@ -25,8 +30,28 @@ union rmi_operand = { 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), generic_imm) -> bits('m) -function read_imm(wsize, imm) = imm[wsize - 1 .. 0] +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) diff --git a/tiny-x86.sail b/tiny-x86.sail index 547216e..ab73101 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -22,11 +22,9 @@ union ast = { 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"); - - assert(match (dest, src) { - (rm_MEM(x), rmi_MEM(y)) => false, - _ => true - }, error_message) + match (dest, src) { + (rm_MEM(_), rmi_MEM(_)) => fail(error_message) + } } val execute : ast -> unit @@ -35,6 +33,10 @@ 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) @@ -43,6 +45,10 @@ function clause execute(MOV(wsize, dest, src)) = { 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); @@ -82,9 +88,15 @@ function clause execute(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 + assert(match second { + rmi_IMM(IMM64(_)) => false, + _ => true + }, "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); - // execute CMP instruction let result = sub_bits(first_val, second_val); /* change value of status flags. Equivalent to the changes made on executing the SUB instruction. */ @@ -105,9 +117,9 @@ 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(operand) if wsize == 64 => fail("Operand for PUSH operation not supported"), - rmi_REG(operand) if wsize == 8 => fail("Operand for PUSH operation not supported"), - rmi_MEM(operand) if wsize == 8 => fail("Operand for PUSH operation not supported") + 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") }; let src_val = read_operand(wsize, src); @@ -120,9 +132,14 @@ function clause execute(PUSH(wsize, src)) = { 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); - // execute SUB instruction let result = sub_bits(dest_val, src_val); write_operand(wsize, dest, result); From 019c14b0a286ad579e345c35b8b9ef13d62d5196 Mon Sep 17 00:00:00 2001 From: s-prism <166765868+s-prism@users.noreply.github.com> Date: Tue, 2 Dec 2025 17:36:59 +0000 Subject: [PATCH 15/24] Execute function defined up to instruction IMUL --- tiny-x86.sail | 92 ++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 83 insertions(+), 9 deletions(-) diff --git a/tiny-x86.sail b/tiny-x86.sail index ab73101..c23e945 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -23,7 +23,8 @@ 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) + (rm_MEM(_), rmi_MEM(_)) => fail(error_message), + (_,_) => () } } @@ -35,7 +36,8 @@ function clause execute(MOV(wsize, dest, src)) = { 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") + (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); @@ -47,7 +49,8 @@ function clause execute(XOR(wsize, dest, src)) = { 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") + rmi_IMM(IMM64(_)) => fail("For operation XOR, src = imm64 is not a valid operand"), + _ => () }; // execute XOR instruction let operand1 = read_operand(wsize, dest); @@ -89,10 +92,10 @@ 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 - assert(match second { - rmi_IMM(IMM64(_)) => false, - _ => true - }, "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); @@ -119,9 +122,11 @@ function clause execute(PUSH(wsize, src)) = { 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_MEM(_) if wsize == 8 => fail("Operand for PUSH operation not supported"), + _ => () }; + // execute PUSH let src_val = read_operand(wsize, src); let wsize_bytes = wsize / 8; RSP = sub_bits(RSP, get_slice_int(64, wsize_bytes, 0)); @@ -129,12 +134,58 @@ function clause execute(PUSH(wsize, src)) = { write_operand(wsize, dest_address, src_val) } +function clause execute(POP(wsize, dest)) = { + // POP instruction does not allow dest = reg8 or mem8. Due to 64 bit addressing, dest also cannot be 32 bits long. + match dest { + _ if wsize == 8 => fail("8 bit operand for POP operation not supported"), + _ if wsize == 32 => fail("32 bit operand for POP operation not supported"), + _ => () + }; + + // execute POP + let popped_val = read_operand(wsize, rm_MEM(RSP)); + let wsize_bytes = wsize / 8; + RSP = add_bits(RSP, get_slice_int(64, wsize_bytes, 0)); + write_operand(wsize, dest, popped_val); +} + +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") + rmi_IMM(IMM64(_)) => fail("For operation SUB, src = imm64 is not a valid operand"), + _ => () }; // execute SUB instruction @@ -158,4 +209,27 @@ function clause execute(SUB(wsize, dest, src)) = { 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; + } +} + end execute \ No newline at end of file From 03ef10aa3b609d929efc28e973c6567b6acbafb9 Mon Sep 17 00:00:00 2001 From: s-prism <166765868+s-prism@users.noreply.github.com> Date: Tue, 2 Dec 2025 20:52:50 +0000 Subject: [PATCH 16/24] define execute function for the whole AST --- tiny-x86.sail | 52 +++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 48 insertions(+), 4 deletions(-) diff --git a/tiny-x86.sail b/tiny-x86.sail index c23e945..db616e0 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -12,11 +12,11 @@ union ast = { 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 + 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 @@ -232,4 +232,48 @@ function clause execute(IMUL(wsize, dest, src)) = { } } +function clause execute(CALL(rel32)) = { + /* execute near relative call */ + let displacement = read_operand(64, IMM32(rel32)); + // 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 from the top of the stack (RSP) into RBP + RBP now contains the old / now current base / frame pointer + */ + RBP = read_operand(64, rm_MEM(RSP)); + RSP = RSP + 8; +} + +function clause execute(RET()) = { + /* execute near return */ + // pop from the top of the stack (RSP) into RIP + RIP = read_operand(64, rm_MEM(RSP)); + 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 \ No newline at end of file From 72fb0a0daf3d66442b857e02fe36ddaf7f1c15da Mon Sep 17 00:00:00 2001 From: s-prism <166765868+s-prism@users.noreply.github.com> Date: Wed, 3 Dec 2025 01:34:38 +0000 Subject: [PATCH 17/24] Added some fail clauses for stack faults --- tiny-x86.sail | 32 ++++++++++++++++++++++++++------ 1 file changed, 26 insertions(+), 6 deletions(-) diff --git a/tiny-x86.sail b/tiny-x86.sail index db616e0..2ec1b77 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -126,9 +126,14 @@ function clause execute(PUSH(wsize, src)) = { _ => () }; - // execute PUSH + /* execute PUSH */ let src_val = read_operand(wsize, src); let wsize_bytes = wsize / 8; + // fail with a stack fault if stack is not large enough for the item about to be pushed + if unsigned(RSP) < wsize_bytes then { + fail("Stack Fault #SS(0): Stack has insufficient space left") + }; + // continue push RSP = sub_bits(RSP, get_slice_int(64, wsize_bytes, 0)); let dest_address = rm_MEM(RSP); write_operand(wsize, dest_address, src_val) @@ -142,9 +147,13 @@ function clause execute(POP(wsize, dest)) = { _ => () }; + let wsize_bytes = wsize / 8; + // fail with a stack fault if stack is too empty to pop an item + if unsigned(RSP) > 2^64 - wsize_bytes then { + fail("Stack Fault #SS(0): Stack is too empty to read value") + }; // execute POP let popped_val = read_operand(wsize, rm_MEM(RSP)); - let wsize_bytes = wsize / 8; RSP = add_bits(RSP, get_slice_int(64, wsize_bytes, 0)); write_operand(wsize, dest, popped_val); } @@ -235,7 +244,12 @@ function clause execute(IMUL(wsize, dest, src)) = { function clause execute(CALL(rel32)) = { /* execute near relative call */ let displacement = read_operand(64, IMM32(rel32)); - // push current RIP to the stack + // fail with a stack fault if stack is not large enough for an 8-byte return address + if unsigned(RSP) < 8 then { + fail("Stack Fault #SS(0): Stack has fewer than 8 bytes of space left") + }; + // push current RIP to the stack (and change stack pointer (RSP) accordingly) + RSP = sub_bits(RSP, sail_zero_extend(0x8, 64)); let dest_address = rm_MEM(RSP); write_operand(64, dest_address, RIP); // change RIP as specified by the instruction @@ -246,15 +260,21 @@ 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 from the top of the stack (RSP) into RBP - RBP now contains the old / now current base / frame pointer - */ + // fail with a stack fault if the stack is too empty to contain a base / frame pointer + if unsigned(RSP) > 2^64 - 8 then { + fail("Stack Fault #SS(0): Stack has fewer than 8 bytes of filled space") + }; + // pop from the top of the stack (RSP) into RBP RBP = read_operand(64, rm_MEM(RSP)); RSP = RSP + 8; } function clause execute(RET()) = { /* execute near return */ + // fail with a stack fault if the stack is too empty to contain an instruction pointer + if unsigned(RSP) > 2^64 - 8 then { + fail("Stack Fault #SS(0): Stack has fewer than 8 bytes of filled space") + }; // pop from the top of the stack (RSP) into RIP RIP = read_operand(64, rm_MEM(RSP)); RSP = RSP + 8; From f78e4617cb4dcba9da7e0b29a592f2fe3cb49b15 Mon Sep 17 00:00:00 2001 From: s-prism <166765868+s-prism@users.noreply.github.com> Date: Wed, 3 Dec 2025 14:43:49 +0000 Subject: [PATCH 18/24] Fix operand size for push instruction --- tiny-x86.sail | 40 +++++++++++++++++++++------------------- 1 file changed, 21 insertions(+), 19 deletions(-) diff --git a/tiny-x86.sail b/tiny-x86.sail index 2ec1b77..394cd72 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -126,36 +126,35 @@ function clause execute(PUSH(wsize, src)) = { _ => () }; - /* execute PUSH */ - let src_val = read_operand(wsize, src); - let wsize_bytes = wsize / 8; - // fail with a stack fault if stack is not large enough for the item about to be pushed - if unsigned(RSP) < wsize_bytes then { + // If the source operand is an immediate of size less than the operand size, a sign-extended value is pushed on the stack + // default operand size is 8 bytes = 64 bits + let src_val = sail_sign_extend(read_operand(wsize, src), 64); + // fail with a stack fault if stack is not large enough to fit an 8 byte item + if unsigned(RSP) < 8 then { fail("Stack Fault #SS(0): Stack has insufficient space left") }; - // continue push - RSP = sub_bits(RSP, get_slice_int(64, wsize_bytes, 0)); + // subtract 8 from RSP to point to the new top of the stack + RSP = sub_bits(RSP, sail_zero_extend(0x8, 64)); let dest_address = rm_MEM(RSP); - write_operand(wsize, dest_address, src_val) + // push the new item to the top of the stack + write_operand(64, dest_address, src_val) } function clause execute(POP(wsize, dest)) = { - // POP instruction does not allow dest = reg8 or mem8. Due to 64 bit addressing, dest also cannot be 32 bits long. - match dest { - _ if wsize == 8 => fail("8 bit operand for POP operation not supported"), - _ if wsize == 32 => fail("32 bit operand for POP operation not supported"), - _ => () - }; + // POP instruction does not allow dest to be 8 bits long. Due to 64 bit addressing, dest also cannot be 32 bits long. + if wsize == 8 then fail("8 bit operand for POP operation not supported"); + if wsize == 32 then fail("32 bit operand for POP operation not supported"); let wsize_bytes = wsize / 8; // fail with a stack fault if stack is too empty to pop an item if unsigned(RSP) > 2^64 - wsize_bytes then { fail("Stack Fault #SS(0): Stack is too empty to read value") }; - // execute POP + // pop the value at the top of the stack to dest let popped_val = read_operand(wsize, rm_MEM(RSP)); - RSP = add_bits(RSP, get_slice_int(64, wsize_bytes, 0)); write_operand(wsize, dest, popped_val); + // increment stack pointer to free the popped stack space + RSP = RSP + wsize_bytes; } function clause execute(ADD(wsize, dest, src)) = { @@ -248,8 +247,9 @@ function clause execute(CALL(rel32)) = { if unsigned(RSP) < 8 then { fail("Stack Fault #SS(0): Stack has fewer than 8 bytes of space left") }; - // push current RIP to the stack (and change stack pointer (RSP) accordingly) + // 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 @@ -264,8 +264,9 @@ function clause execute(LEAVE()) = { if unsigned(RSP) > 2^64 - 8 then { fail("Stack Fault #SS(0): Stack has fewer than 8 bytes of filled space") }; - // pop from the top of the stack (RSP) into RBP + // pop value into RBP RBP = read_operand(64, rm_MEM(RSP)); + // increment stack pointer to free the popped stack space RSP = RSP + 8; } @@ -275,8 +276,9 @@ function clause execute(RET()) = { if unsigned(RSP) > 2^64 - 8 then { fail("Stack Fault #SS(0): Stack has fewer than 8 bytes of filled space") }; - // pop from the top of the stack (RSP) into RIP + // pop value into RIP RIP = read_operand(64, rm_MEM(RSP)); + // increment stack pointer to free the popped stack space RSP = RSP + 8; } From e21d9409ab7622283c593a0e84c8dd2ff411c19c Mon Sep 17 00:00:00 2001 From: s-prism <166765868+s-prism@users.noreply.github.com> Date: Wed, 3 Dec 2025 15:42:51 +0000 Subject: [PATCH 19/24] Removed fail clauses that are not needed + simplified pop instruction to only allow a 64 bit destination --- tiny-x86.sail | 36 ++++++++---------------------------- 1 file changed, 8 insertions(+), 28 deletions(-) diff --git a/tiny-x86.sail b/tiny-x86.sail index 394cd72..59a4fd4 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -126,35 +126,27 @@ function clause execute(PUSH(wsize, src)) = { _ => () }; - // If the source operand is an immediate of size less than the operand size, a sign-extended value is pushed on the stack + // 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); - // fail with a stack fault if stack is not large enough to fit an 8 byte item - if unsigned(RSP) < 8 then { - fail("Stack Fault #SS(0): Stack has insufficient space left") - }; // subtract 8 from RSP to point to the new top of the stack RSP = sub_bits(RSP, sail_zero_extend(0x8, 64)); - let dest_address = rm_MEM(RSP); // 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. - if wsize == 8 then fail("8 bit operand for POP operation not supported"); - if wsize == 32 then fail("32 bit operand for POP operation not supported"); + // 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"); - let wsize_bytes = wsize / 8; - // fail with a stack fault if stack is too empty to pop an item - if unsigned(RSP) > 2^64 - wsize_bytes then { - fail("Stack Fault #SS(0): Stack is too empty to read value") - }; // pop the value at the top of the stack to dest - let popped_val = read_operand(wsize, rm_MEM(RSP)); - write_operand(wsize, dest, popped_val); + 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 + wsize_bytes; + RSP = RSP + 8; } function clause execute(ADD(wsize, dest, src)) = { @@ -243,10 +235,6 @@ function clause execute(IMUL(wsize, dest, src)) = { function clause execute(CALL(rel32)) = { /* execute near relative call */ let displacement = read_operand(64, IMM32(rel32)); - // fail with a stack fault if stack is not large enough for an 8-byte return address - if unsigned(RSP) < 8 then { - fail("Stack Fault #SS(0): Stack has fewer than 8 bytes of space left") - }; // 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 @@ -260,10 +248,6 @@ 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; - // fail with a stack fault if the stack is too empty to contain a base / frame pointer - if unsigned(RSP) > 2^64 - 8 then { - fail("Stack Fault #SS(0): Stack has fewer than 8 bytes of filled space") - }; // pop value into RBP RBP = read_operand(64, rm_MEM(RSP)); // increment stack pointer to free the popped stack space @@ -272,10 +256,6 @@ function clause execute(LEAVE()) = { function clause execute(RET()) = { /* execute near return */ - // fail with a stack fault if the stack is too empty to contain an instruction pointer - if unsigned(RSP) > 2^64 - 8 then { - fail("Stack Fault #SS(0): Stack has fewer than 8 bytes of filled space") - }; // pop value into RIP RIP = read_operand(64, rm_MEM(RSP)); // increment stack pointer to free the popped stack space From 45b15c9947ce302c1720a32530ffa6c60fdc5a81 Mon Sep 17 00:00:00 2001 From: s-prism <166765868+s-prism@users.noreply.github.com> Date: Wed, 3 Dec 2025 18:37:27 +0000 Subject: [PATCH 20/24] Removed unnecessary register fields --- operands.sail | 10 +++++----- registers.sail | 52 ++++++++++---------------------------------------- tiny-x86.sail | 6 +++--- 3 files changed, 18 insertions(+), 50 deletions(-) diff --git a/operands.sail b/operands.sail index 46306d1..0147c2e 100644 --- a/operands.sail +++ b/operands.sail @@ -16,13 +16,13 @@ union imm = { /* union types for operand */ // register or memory operand union rm_operand = { - rm_REG: reg_index, + rm_REG: reg_ref, rm_MEM: mem_addr } // register, memory, or immediate operand union rmi_operand = { rmi_IMM: imm, - rmi_REG: reg_index, + rmi_REG: reg_ref, rmi_MEM: mem_addr } @@ -59,7 +59,7 @@ 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_reg(wsize, reg_index), + rm_REG(reg_ref) => read_reg(wsize, reg_ref), rm_MEM(mem_addr) => read_memory(wsize_bytes, mem_addr, create_readAccessDescriptor()), } } @@ -71,7 +71,7 @@ function read_rmi_operand(wsize, operand: rmi_operand) = { assert('m == wsize_bytes * 8); // required for type-checking match operand { rmi_IMM(imm) => read_imm(wsize, imm), - rmi_REG(reg_index) => read_reg(wsize, reg_index), + rmi_REG(reg_ref) => read_reg(wsize, reg_ref), rmi_MEM(mem_addr) => read_memory(wsize_bytes, mem_addr, create_readAccessDescriptor()), } } @@ -85,7 +85,7 @@ 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_reg(wsize, reg_index, value), + rm_REG(reg_ref) => write_reg(wsize, reg_ref, value), rm_MEM(mem_addr) => write_memory(wsize_bytes, mem_addr, value, create_writeAccessDescriptor()), } } diff --git a/registers.sail b/registers.sail index 3bb2f79..2b65faa 100644 --- a/registers.sail +++ b/registers.sail @@ -1,5 +1,5 @@ -/* range of registers that one can refer to */ -type reg_index = range(0, 15) +/* register pointer type */ +type reg_ref = register(bits(64)) /* program counter */ @@ -25,39 +25,8 @@ register R13: bits(64) register R14: bits(64) register R15: bits(64) -let GPRs : vector(16, register(bits(64))) = [ - ref R15, - ref R14, - ref R13, - ref R12, - ref R11, - ref R10, - ref R9, - ref R8, - ref RDI, - ref RSI, - ref RBP, - ref RSP, - ref RBX, - ref RDX, - ref RCX, - ref RAX -] - /* register RFLAGS, system and status flags + mostly restricted access */ bitfield rflags : bits(64) = { - // system flags and IOPL field - ID: 21, - VIP: 20, - VIF: 19, - AC: 18, - VM: 17, - RF: 16, - NT: 14, - IOPL: 13 .. 12, - IF: 9, - TF: 8, - // status flags OF: 11, // overflow flag (for operations between signed values) SF: 7, // sign flag @@ -69,24 +38,23 @@ bitfield rflags : bits(64) = { register RFLAGS: rflags /* read and write least-significant 8,16,32,64 (32 with 0 extend for write) bits */ - val read_reg: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_index) -> bits('m) + val read_reg: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_ref) -> bits('m) - function read_reg(wsize, i: reg_index) = { - let reg = *GPRs[i]; - reg[wsize - 1 .. 0] + function read_reg(wsize, reg_ref) = { + (*reg_ref)[wsize - 1 .. 0] } -val write_reg: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_index, bits('m)) -> unit +val write_reg: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_ref, bits('m)) -> unit -function write_reg(wsize, i: reg_index, value) = { +function write_reg(wsize, reg_ref, 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; + (*reg_ref)[63 .. 32] = 0x0000_0000; + (*reg_ref)[31 .. 0] = value; } else // the value is written to the last wsize bits of the register - (*GPRs[i])[wsize - 1 .. 0] = value; + (*reg_ref)[wsize - 1 .. 0] = value; } /* change the value of the parity flag depending on the result of an operation */ diff --git a/tiny-x86.sail b/tiny-x86.sail index 59a4fd4..c20f1fd 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -1,17 +1,17 @@ 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 + // 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, rm_operand, rmi_operand), - PUSH: (word_size, 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) + IMUL: (word_size, reg_ref, rm_operand), // IMUL with only 2 arguments (dest and src) CALL: imm32, LEAVE: unit, RET: unit, // near return only From 45c0dc6fcbf9b919b97c3bfe41e719f48b0591fd Mon Sep 17 00:00:00 2001 From: s-prism <166765868+s-prism@users.noreply.github.com> Date: Thu, 4 Dec 2025 13:08:10 +0000 Subject: [PATCH 21/24] Added some very rough not unit tests --- registers.sail | 3 +- tests.sail | 81 +++++++++++++++++++++++++++++++++++++++++++++++++- tiny-x86.sail | 6 ---- 3 files changed, 81 insertions(+), 9 deletions(-) diff --git a/registers.sail b/registers.sail index 2b65faa..da4ffac 100644 --- a/registers.sail +++ b/registers.sail @@ -27,11 +27,10 @@ register R15: bits(64) /* register RFLAGS, system and status flags + mostly restricted access */ bitfield rflags : bits(64) = { - // status flags + // status flags (exclusing AF as it is only used for legacy instructions) 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) } diff --git a/tests.sail b/tests.sail index 2ae50ba..6657ce0 100644 --- a/tests.sail +++ b/tests.sail @@ -6,6 +6,85 @@ function write_then_read_mem() -> unit = { assert(read_value == value, "Writing then reading from the same memory address was inconsistent"); } +function mov_reg_to_mem() -> unit = { + let wsize = 16; + write_reg(wsize, ref R8, get_slice_int(wsize, -236, 0)); + execute(MOV(wsize, rm_MEM(0xFFFF_FFFF_FFFF_FFF8), rmi_REG(ref R8))); + 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_reg(wsize1, ref R8, 0x0101_0101_0101_0101); + let imm_val = 0x0000_1111; + execute(XOR(wsize1, rm_REG(ref R8), rmi_IMM(IMM32(imm_val)))); + assert(read_reg(wsize1, ref R8) == 0x0101_0101_0101_1010, "XOR(reg, imm) gave an incorrect answer") +} + +function cmp_jns() -> unit = { + write_reg(32, ref RAX, 0x4444_4444); + execute(CMP(32, rm_REG(ref RAX), 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(ref R15))); + assert(RSP == RSP1, "POP does not correctly change stack pointer"); + assert(read_reg(64, ref R15) == 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_reg(wsize1, ref R8, get_slice_int(wsize1, 30, 0)); + let imm_val = get_slice_int(wsize2, -250, 0); + execute(ADD(wsize1, rm_REG(ref R8), rmi_IMM(IMM32(imm_val)))); + assert(signed(read_reg(wsize1, ref R8)) == 30 - 250, "ADD(reg, imm) gave an incorrect answer") +} + +function subtract_2_numbers() -> unit = { + let wsize1 = 64; + let wsize2 = 32; + write_reg(wsize1, ref R8, get_slice_int(wsize1, 30, 0)); + let imm_val = get_slice_int(wsize2, -250, 0); + execute(SUB(wsize1, rm_REG(ref R8), rmi_IMM(IMM32(imm_val)))); + assert(signed(read_reg(wsize1, ref R8)) == 30 - (- 250), "SUB(reg, imm) gave an incorrect answer"); +} + +function multiply_2_numbers() -> unit = { + let wsize = 16; + write_reg(wsize, ref R8, get_slice_int(wsize, 30, 0)); + write_reg(wsize, ref R9, get_slice_int(wsize, -250, 0)); + execute(IMUL(wsize, ref R8, rm_REG(ref R9))); + assert(signed(read_reg(wsize, ref R8)) == 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 = { - write_then_read_mem() + 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(); } \ No newline at end of file diff --git a/tiny-x86.sail b/tiny-x86.sail index c20f1fd..ff20104 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -111,8 +111,6 @@ function clause execute(CMP(wsize, first, second)) = { 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); } @@ -173,8 +171,6 @@ function clause execute(ADD(wsize, dest, src)) = { 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); } @@ -203,8 +199,6 @@ function clause execute(SUB(wsize, dest, src)) = { 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); } From c218912a8a02a55e6d5dca7bbeec9b0a8e1edf23 Mon Sep 17 00:00:00 2001 From: s-prism <166765868+s-prism@users.noreply.github.com> Date: Thu, 4 Dec 2025 16:25:22 +0000 Subject: [PATCH 22/24] Removed unnecessary register fields, modify tests accordingly, and add rocq clause to makefile --- .gitignore | 1 + Makefile | 5 ++++- operands.sail | 10 +++++----- registers.sail | 40 ++++++++++++++++++++++++++++++---------- tests.sail | 38 +++++++++++++++++++------------------- tiny-x86.sail | 6 +++--- 6 files changed, 62 insertions(+), 38 deletions(-) diff --git a/.gitignore b/.gitignore index 5ca479f..d70f9f7 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ *z3_problems test.* sail_smt_cache +*test_types* diff --git a/Makefile b/Makefile index e58353f..fa29a91 100644 --- a/Makefile +++ b/Makefile @@ -10,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 interface.sail operands.sail tiny-x86.sail tests.sail +test.c: $(X86_FILES) sail -c $(X86_FILES) -o test; +rocq: $(X86_FILES) + sail -coq $(X86_FILES) -o test; + .PHONY: type-check test \ No newline at end of file diff --git a/operands.sail b/operands.sail index 0147c2e..46306d1 100644 --- a/operands.sail +++ b/operands.sail @@ -16,13 +16,13 @@ union imm = { /* union types for operand */ // register or memory operand union rm_operand = { - rm_REG: reg_ref, + rm_REG: reg_index, rm_MEM: mem_addr } // register, memory, or immediate operand union rmi_operand = { rmi_IMM: imm, - rmi_REG: reg_ref, + rmi_REG: reg_index, rmi_MEM: mem_addr } @@ -59,7 +59,7 @@ 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_ref) => read_reg(wsize, reg_ref), + rm_REG(reg_index) => read_reg(wsize, reg_index), rm_MEM(mem_addr) => read_memory(wsize_bytes, mem_addr, create_readAccessDescriptor()), } } @@ -71,7 +71,7 @@ function read_rmi_operand(wsize, operand: rmi_operand) = { assert('m == wsize_bytes * 8); // required for type-checking match operand { rmi_IMM(imm) => read_imm(wsize, imm), - rmi_REG(reg_ref) => read_reg(wsize, reg_ref), + rmi_REG(reg_index) => read_reg(wsize, reg_index), rmi_MEM(mem_addr) => read_memory(wsize_bytes, mem_addr, create_readAccessDescriptor()), } } @@ -85,7 +85,7 @@ 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_ref) => write_reg(wsize, reg_ref, value), + rm_REG(reg_index) => write_reg(wsize, reg_index, value), rm_MEM(mem_addr) => write_memory(wsize_bytes, mem_addr, value, create_writeAccessDescriptor()), } } diff --git a/registers.sail b/registers.sail index da4ffac..70fdbb8 100644 --- a/registers.sail +++ b/registers.sail @@ -1,5 +1,5 @@ -/* register pointer type */ -type reg_ref = register(bits(64)) +/* range of registers that one can refer to */ +type reg_index = range(0, 15) /* program counter */ @@ -25,6 +25,25 @@ register R13: bits(64) register R14: bits(64) register R15: bits(64) +let GPRs : vector(16, register(bits(64))) = [ + ref R15, + ref R14, + ref R13, + ref R12, + ref R11, + ref R10, + ref R9, + ref R8, + ref RDI, + ref RSI, + ref RBP, + ref RSP, + ref RBX, + ref RDX, + ref RCX, + ref RAX +] + /* register RFLAGS, system and status flags + mostly restricted access */ bitfield rflags : bits(64) = { // status flags (exclusing AF as it is only used for legacy instructions) @@ -37,23 +56,24 @@ bitfield rflags : bits(64) = { register RFLAGS: rflags /* read and write least-significant 8,16,32,64 (32 with 0 extend for write) bits */ - val read_reg: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_ref) -> bits('m) + val read_reg: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_index) -> bits('m) - function read_reg(wsize, reg_ref) = { - (*reg_ref)[wsize - 1 .. 0] + function read_reg(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_ref, bits('m)) -> unit +val write_reg: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_index, bits('m)) -> unit -function write_reg(wsize, reg_ref, value) = { +function write_reg(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 - (*reg_ref)[63 .. 32] = 0x0000_0000; - (*reg_ref)[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 - (*reg_ref)[wsize - 1 .. 0] = value; + (*GPRs[i])[wsize - 1 .. 0] = value; } /* change the value of the parity flag depending on the result of an operation */ diff --git a/tests.sail b/tests.sail index 6657ce0..466f5e5 100644 --- a/tests.sail +++ b/tests.sail @@ -8,23 +8,23 @@ function write_then_read_mem() -> unit = { function mov_reg_to_mem() -> unit = { let wsize = 16; - write_reg(wsize, ref R8, get_slice_int(wsize, -236, 0)); - execute(MOV(wsize, rm_MEM(0xFFFF_FFFF_FFFF_FFF8), rmi_REG(ref R8))); + write_reg(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_reg(wsize1, ref R8, 0x0101_0101_0101_0101); + write_reg(wsize1, 8, 0x0101_0101_0101_0101); let imm_val = 0x0000_1111; - execute(XOR(wsize1, rm_REG(ref R8), rmi_IMM(IMM32(imm_val)))); - assert(read_reg(wsize1, ref R8) == 0x0101_0101_0101_1010, "XOR(reg, imm) gave an incorrect answer") + execute(XOR(wsize1, rm_REG(8), rmi_IMM(IMM32(imm_val)))); + assert(read_reg(wsize1, 8) == 0x0101_0101_0101_1010, "XOR(reg, imm) gave an incorrect answer") } function cmp_jns() -> unit = { - write_reg(32, ref RAX, 0x4444_4444); - execute(CMP(32, rm_REG(ref RAX), rmi_IMM(IMM32(0x5555_5555)))); + write_reg(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)); @@ -40,35 +40,35 @@ function push_pop() -> unit = { 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(ref R15))); + execute(POP(64, rm_REG(15))); assert(RSP == RSP1, "POP does not correctly change stack pointer"); - assert(read_reg(64, ref R15) == sail_sign_extend(0xF0F0, 64), "POP does not put the correct value in the destination") + assert(read_reg(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_reg(wsize1, ref R8, get_slice_int(wsize1, 30, 0)); + write_reg(wsize1, 8, get_slice_int(wsize1, 30, 0)); let imm_val = get_slice_int(wsize2, -250, 0); - execute(ADD(wsize1, rm_REG(ref R8), rmi_IMM(IMM32(imm_val)))); - assert(signed(read_reg(wsize1, ref R8)) == 30 - 250, "ADD(reg, imm) gave an incorrect answer") + execute(ADD(wsize1, rm_REG(8), rmi_IMM(IMM32(imm_val)))); + assert(signed(read_reg(wsize1, 8)) == 30 - 250, "ADD(reg, imm) gave an incorrect answer") } function subtract_2_numbers() -> unit = { let wsize1 = 64; let wsize2 = 32; - write_reg(wsize1, ref R8, get_slice_int(wsize1, 30, 0)); + write_reg(wsize1, 8, get_slice_int(wsize1, 30, 0)); let imm_val = get_slice_int(wsize2, -250, 0); - execute(SUB(wsize1, rm_REG(ref R8), rmi_IMM(IMM32(imm_val)))); - assert(signed(read_reg(wsize1, ref R8)) == 30 - (- 250), "SUB(reg, imm) gave an incorrect answer"); + execute(SUB(wsize1, rm_REG(8), rmi_IMM(IMM32(imm_val)))); + assert(signed(read_reg(wsize1, 8)) == 30 - (- 250), "SUB(reg, imm) gave an incorrect answer"); } function multiply_2_numbers() -> unit = { let wsize = 16; - write_reg(wsize, ref R8, get_slice_int(wsize, 30, 0)); - write_reg(wsize, ref R9, get_slice_int(wsize, -250, 0)); - execute(IMUL(wsize, ref R8, rm_REG(ref R9))); - assert(signed(read_reg(wsize, ref R8)) == 30 * (- 250), "IMUL(reg, reg) gave an incorrect answer"); + write_reg(wsize, 8, get_slice_int(wsize, 30, 0)); + write_reg(wsize, 9, get_slice_int(wsize, -250, 0)); + execute(IMUL(wsize, 8, rm_REG(9))); + assert(signed(read_reg(wsize, 8)) == 30 * (- 250), "IMUL(reg, reg) gave an incorrect answer"); } function jmp() -> unit = { diff --git a/tiny-x86.sail b/tiny-x86.sail index ff20104..d5aab8d 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -1,17 +1,17 @@ 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 + // only implementing instructions where both dest and src have the same 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, rm_operand, rmi_operand), - PUSH: (word_size, rmi_operand), // only allowing 64 bit operand + PUSH: (word_size, rmi_operand), POP: (word_size, rm_operand), ADD: (word_size, rm_operand, rmi_operand), SUB: (word_size, rm_operand, rmi_operand), - IMUL: (word_size, reg_ref, rm_operand), // IMUL with only 2 arguments (dest and src) + IMUL: (word_size, reg_index, rm_operand), // IMUL with only 2 arguments (dest and src) CALL: imm32, LEAVE: unit, RET: unit, // near return only From f72a78d55c5280f5b79354da61e621e63055d805 Mon Sep 17 00:00:00 2001 From: s-prism <166765868+s-prism@users.noreply.github.com> Date: Thu, 4 Dec 2025 16:43:34 +0000 Subject: [PATCH 23/24] Flag AF is back + changes to make rocq translation work --- operands.sail | 10 +++++----- registers.sail | 11 ++++++----- tests.sail | 24 ++++++++++++------------ tiny-x86.sail | 10 ++++++++-- 4 files changed, 31 insertions(+), 24 deletions(-) diff --git a/operands.sail b/operands.sail index 46306d1..da91bf7 100644 --- a/operands.sail +++ b/operands.sail @@ -59,7 +59,7 @@ 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_reg(wsize, reg_index), + rm_REG(reg_index) => read_GPR(wsize, reg_index), rm_MEM(mem_addr) => read_memory(wsize_bytes, mem_addr, create_readAccessDescriptor()), } } @@ -71,13 +71,13 @@ function read_rmi_operand(wsize, operand: rmi_operand) = { assert('m == wsize_bytes * 8); // required for type-checking match operand { rmi_IMM(imm) => read_imm(wsize, imm), - rmi_REG(reg_index) => read_reg(wsize, reg_index), + 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_reg} +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 @@ -85,10 +85,10 @@ 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_reg(wsize, reg_index, value), + 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_reg} \ No newline at end of file +overload write_operand = {write_rm_operand, write_GPR} \ No newline at end of file diff --git a/registers.sail b/registers.sail index 70fdbb8..c0a20ed 100644 --- a/registers.sail +++ b/registers.sail @@ -46,26 +46,27 @@ let GPRs : vector(16, register(bits(64))) = [ /* register RFLAGS, system and status flags + mostly restricted access */ bitfield rflags : bits(64) = { - // status flags (exclusing AF as it is only used for legacy instructions) + // 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 /* read and write least-significant 8,16,32,64 (32 with 0 extend for write) bits */ - val read_reg: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_index) -> bits('m) + 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; diff --git a/tests.sail b/tests.sail index 466f5e5..efb169f 100644 --- a/tests.sail +++ b/tests.sail @@ -8,7 +8,7 @@ function write_then_read_mem() -> unit = { function mov_reg_to_mem() -> unit = { let wsize = 16; - write_reg(wsize, 8, get_slice_int(wsize, -236, 0)); + 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") } @@ -16,14 +16,14 @@ function mov_reg_to_mem() -> unit = { function xor_2_numbers() -> unit = { let wsize1 = 64; let wsize2 = 32; - write_reg(wsize1, 8, 0x0101_0101_0101_0101); + 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_reg(wsize1, 8) == 0x0101_0101_0101_1010, "XOR(reg, imm) gave an incorrect answer") + assert(read_GPR(wsize1, 8) == 0x0101_0101_0101_1010, "XOR(reg, imm) gave an incorrect answer") } function cmp_jns() -> unit = { - write_reg(32, 0, 0x4444_4444); + 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; @@ -42,33 +42,33 @@ function push_pop() -> unit = { 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_reg(64, 15) == sail_sign_extend(0xF0F0, 64), "POP does not put the correct value in the destination") + 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_reg(wsize1, 8, get_slice_int(wsize1, 30, 0)); + 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_reg(wsize1, 8)) == 30 - 250, "ADD(reg, imm) gave an incorrect answer") + 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_reg(wsize1, 8, get_slice_int(wsize1, 30, 0)); + 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_reg(wsize1, 8)) == 30 - (- 250), "SUB(reg, imm) gave an incorrect answer"); + assert(signed(read_GPR(wsize1, 8)) == 30 - (- 250), "SUB(reg, imm) gave an incorrect answer"); } function multiply_2_numbers() -> unit = { let wsize = 16; - write_reg(wsize, 8, get_slice_int(wsize, 30, 0)); - write_reg(wsize, 9, get_slice_int(wsize, -250, 0)); + 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_reg(wsize, 8)) == 30 * (- 250), "IMUL(reg, reg) gave an incorrect answer"); + assert(signed(read_GPR(wsize, 8)) == 30 * (- 250), "IMUL(reg, reg) gave an incorrect answer"); } function jmp() -> unit = { diff --git a/tiny-x86.sail b/tiny-x86.sail index d5aab8d..3e74ae0 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -1,13 +1,13 @@ 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 + // 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, rm_operand, rmi_operand), - PUSH: (word_size, 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), @@ -111,6 +111,8 @@ function clause execute(CMP(wsize, first, second)) = { 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); } @@ -171,6 +173,8 @@ function clause execute(ADD(wsize, dest, src)) = { 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); } @@ -199,6 +203,8 @@ function clause execute(SUB(wsize, dest, src)) = { 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); } From cc816555eb22a09ae4e27f98389c4c94efdac1e1 Mon Sep 17 00:00:00 2001 From: s-prism <166765868+s-prism@users.noreply.github.com> Date: Thu, 4 Dec 2025 16:47:56 +0000 Subject: [PATCH 24/24] Added newlines to end of files --- Makefile | 2 +- interface.sail | 2 +- operands.sail | 2 +- prelude.sail | 2 +- registers.sail | 2 +- tests.sail | 2 +- tiny-x86.sail | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Makefile b/Makefile index fa29a91..92b78eb 100644 --- a/Makefile +++ b/Makefile @@ -16,4 +16,4 @@ test.c: $(X86_FILES) rocq: $(X86_FILES) sail -coq $(X86_FILES) -o test; -.PHONY: type-check test \ No newline at end of file +.PHONY: type-check test diff --git a/interface.sail b/interface.sail index 25e9b55..beb34f7 100644 --- a/interface.sail +++ b/interface.sail @@ -141,4 +141,4 @@ enum Barrier = { } instantiation sail_barrier with - 'barrier = Barrier \ No newline at end of file + 'barrier = Barrier diff --git a/operands.sail b/operands.sail index da91bf7..18262fb 100644 --- a/operands.sail +++ b/operands.sail @@ -91,4 +91,4 @@ function write_rm_operand(wsize, operand: rm_operand, value) = { } /* overloaded function to write to any register or memory type */ -overload write_operand = {write_rm_operand, write_GPR} \ No newline at end of file +overload write_operand = {write_rm_operand, write_GPR} diff --git a/prelude.sail b/prelude.sail index 01ad807..73ee7a6 100644 --- a/prelude.sail +++ b/prelude.sail @@ -16,4 +16,4 @@ 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; -} \ No newline at end of file +} diff --git a/registers.sail b/registers.sail index c0a20ed..5c7f33d 100644 --- a/registers.sail +++ b/registers.sail @@ -86,4 +86,4 @@ function modify_parity_flag(result) = { if result[i] == bitone then even_parity = flip_bit(even_parity); }; RFLAGS[PF] = [even_parity]; -} \ No newline at end of file +} diff --git a/tests.sail b/tests.sail index efb169f..1141296 100644 --- a/tests.sail +++ b/tests.sail @@ -87,4 +87,4 @@ function main() : unit -> unit = { subtract_2_numbers(); multiply_2_numbers(); jmp(); -} \ No newline at end of file +} diff --git a/tiny-x86.sail b/tiny-x86.sail index 3e74ae0..c7e444d 100644 --- a/tiny-x86.sail +++ b/tiny-x86.sail @@ -278,4 +278,4 @@ function clause execute(JNS(rel8)) = { } } -end execute \ No newline at end of file +end execute