Execute

.gitignore

@@ -1,2 +1,4 @@
 *z3_problems
 test.*
+sail_smt_cache
+*test_types*

Makefile

@@ -1,15 +1,19 @@
 SAIL_DIR=`sail --dir`
+X86_FILES=prelude.sail registers.sail interface.sail operands.sail tiny-x86.sail tests.sail
 
 type-check:
-	sail prelude.sail registers.sail tiny-x86.sail tests.sail
+	sail $(X86_FILES)
 
 test: test.o
 	./test.o;
 
 test.o: test.c
 	gcc test.c $(SAIL_DIR)/lib/*.c -lgmp -lz -I $(SAIL_DIR)/lib/ -o test.o;
 
-test.c: prelude.sail registers.sail tiny-x86.sail tests.sail
-	sail -c prelude.sail registers.sail tiny-x86.sail tests.sail -o test;
+test.c: $(X86_FILES)
+	sail -c $(X86_FILES) -o test;
 
-.PHONY: type-check test
+rocq: $(X86_FILES)
+	sail -coq $(X86_FILES) -o test;
+
+.PHONY: type-check test

interface.sail

@@ -0,0 +1,144 @@
+$include <concurrency_interface.sail>
+
+/*
+   - mem_acc : Type, An architecture specific description of the access kind.
+     This may also contain arbitrary architecture specific metadata about the
+     access.
+*/
+enum AccessType = {
+  AccessType_IFETCH, // instruction fetch
+  AccessType_RW // read or write
+}
+struct AccessDescriptor = {
+  acctype : AccessType,
+  atomicop : bool,
+  standalone: bool,
+  read : bool,
+  write : bool,
+}
+function base_AccessDescriptor (acctype : AccessType) -> AccessDescriptor = struct {
+  acctype = acctype,
+  atomicop = false,
+  standalone = true,
+  read = false,
+  write = false,
+}
+function create_iFetchAccessDescriptor() -> AccessDescriptor = {
+  var accdesc = base_AccessDescriptor(AccessType_IFETCH);
+  accdesc.read = true;
+  accdesc
+}
+function create_readAccessDescriptor() -> AccessDescriptor = {
+  var accdesc = base_AccessDescriptor(AccessType_RW);
+  accdesc.read = true;
+  accdesc
+}
+function create_writeAccessDescriptor() -> AccessDescriptor = {
+  var accdesc = base_AccessDescriptor(AccessType_RW);
+  accdesc.write = true;
+  accdesc
+}
+
+// Memory access generated by an explicit instruction
+function mem_acc_is_explicit     (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_RW
+
+// Memory access requested by an instruction fetch
+function mem_acc_is_ifetch       (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_IFETCH
+
+// Memory access is a translation table walk. False as memory model is flat.
+function mem_acc_is_ttw          (acc : AccessDescriptor) -> bool = false
+
+// Access is relaxed 
+function mem_acc_is_relaxed      (acc : AccessDescriptor) -> bool = true
+
+// Access uses release-acquire semantics
+function mem_acc_is_rel_acq_rcpc (acc : AccessDescriptor) -> bool = false
+function mem_acc_is_rel_acq_rcsc (acc : AccessDescriptor) -> bool = false
+
+// access is from a standalone instruction (not part of an atomic sequence of instructionns)
+function mem_acc_is_standalone   (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_RW & acc.standalone
+
+// access is part of an exclusive instruction 
+function mem_acc_is_exclusive    (acc : AccessDescriptor) -> bool = false
+
+// access is for part of an atomic read-modify-write instruction
+function mem_acc_is_atomic_rmw   (acc : AccessDescriptor) -> bool = acc.acctype == AccessType_RW & acc.atomicop
+
+/* instantiate */
+instantiation sail_mem_read with
+  'addr_size = 64,
+  'addr_space = unit,
+  'mem_acc = AccessDescriptor,
+  'abort = unit,
+  'CHERI = false,
+  'cap_size_log = 0,
+  mem_acc_is_explicit = mem_acc_is_explicit,
+  mem_acc_is_ifetch = mem_acc_is_ifetch,
+  mem_acc_is_ttw = mem_acc_is_ttw,
+  mem_acc_is_relaxed = mem_acc_is_relaxed,
+  mem_acc_is_rel_acq_rcpc = mem_acc_is_rel_acq_rcpc,
+  mem_acc_is_rel_acq_rcsc = mem_acc_is_rel_acq_rcsc,
+  mem_acc_is_standalone = mem_acc_is_standalone,
+  mem_acc_is_exclusive = mem_acc_is_exclusive,
+  mem_acc_is_atomic_rmw = mem_acc_is_atomic_rmw
+
+instantiation sail_mem_write with
+  'addr_size = 64,
+  'addr_space = unit,
+  'mem_acc = AccessDescriptor,
+  'abort = unit,
+  'CHERI = false,
+  'cap_size_log = 0,
+  mem_acc_is_explicit = mem_acc_is_explicit,
+  mem_acc_is_ifetch = mem_acc_is_ifetch,
+  mem_acc_is_ttw = mem_acc_is_ttw,
+  mem_acc_is_relaxed = mem_acc_is_relaxed,
+  mem_acc_is_rel_acq_rcpc = mem_acc_is_rel_acq_rcpc,
+  mem_acc_is_rel_acq_rcsc = mem_acc_is_rel_acq_rcsc,
+  mem_acc_is_standalone = mem_acc_is_standalone,
+  mem_acc_is_exclusive = mem_acc_is_exclusive,
+  mem_acc_is_atomic_rmw = mem_acc_is_atomic_rmw
+
+/* memory read and write */
+val read_memory : forall 'N, 'N > 0.
+  (int('N), bits(64), AccessDescriptor) -> bits(8 * 'N)
+
+function read_memory(N, addr, accdesc) = {
+  let req : Mem_request('N, 0, 64, unit, AccessDescriptor) = struct {
+    access_kind   = accdesc,
+    address       = truncate(addr, 64),
+    address_space = (),
+    size          = N,
+    num_tag       = 0
+  };
+
+  match sail_mem_read(req) {
+    Ok((bytes, _)) => from_bytes_le(bytes),
+    Err(_e) => { exit() }
+  }
+}
+
+val write_memory : forall 'N, 'N > 0. (int('N), bits(64), bits(8 * 'N), AccessDescriptor) -> unit
+function write_memory(N, addr, value, accdesc) = {
+  let req : Mem_request('N, 0, 64, unit, AccessDescriptor) = struct {
+    access_kind = accdesc,
+    address = truncate(addr, 64),
+    address_space = (),
+    size = N,
+    num_tag = 0,
+  };
+  match sail_mem_write(req,to_bytes_le(N, value),[]) {
+    Ok(_) => (),
+    Err(_) => exit(),
+  }
+}
+
+/* memory barrier */
+enum Barrier = {
+  Barrier_SFENCE, // store fence
+  Barrier_LFENCE, // load fence
+  Barrier_MFENCE // memory fence
+}
+
+instantiation sail_barrier with
+  'barrier = Barrier

operands.sail

@@ -0,0 +1,94 @@
+/* Memory addresses are 64 bits. Assume all possible addresses can be used. */
+type mem_addr = bits(64)
+
+/* immediate value types */
+type imm8 = bits(8)
+type imm16 = bits(16)
+type imm32 = bits(32)
+type imm64 = bits(64)
+union imm = {
+    IMM8: imm8,
+    IMM16: imm16,
+    IMM32: imm32,
+    IMM64: imm64
+}
+
+/* union types for operand */
+// register or memory operand
+union rm_operand = {
+    rm_REG: reg_index,
+    rm_MEM: mem_addr
+}
+// register, memory, or immediate operand
+union rmi_operand = {
+    rmi_IMM: imm,
+    rmi_REG: reg_index,
+    rmi_MEM: mem_addr
+}
+
+/* permitted word sizes */
+type word_size = {8,16,32,64}
+
+/* read immediate value from variable bit-extended to 64 bits */
+val read_imm: forall 'm, 'm in {8, 16, 32, 64}. (int('m), imm) -> bits('m)
+function read_imm(wsize, imm) = {
+    // If imm size is smaller than word size, then sign-extend the imm before returning it
+    match imm {
+        IMM8(value) => {
+            assert(wsize == 8, "Immediate value size is 8 bits, but word size is not.");
+            value[7 .. 0]
+        },
+        IMM16(value) => {
+            assert(wsize == 16, "Immediate value size is 16 bits, but word size is not.");
+            value[15 .. 0]
+        },
+        IMM32(value) => {
+            assert(wsize >= 32, "Immediate value size is 32 bits, but word size is not 32 or 64 bits.");
+            sail_sign_extend(value[31 .. 0], wsize)
+        },
+        IMM64(value) => {
+            assert(wsize == 64, "Immediate value size is 64 bits, but word size is not.");
+            value[63 .. 0]
+        },
+    }
+}
+
+/* read register or memory operand */
+val read_rm_operand: forall 'm, 'm in {8, 16, 32, 64}. (int('m), rm_operand) -> bits('m)
+function read_rm_operand(wsize, operand: rm_operand) = {
+    let wsize_bytes = wsize / 8;
+    assert('m == wsize_bytes * 8); // required for type-checking
+    match operand {
+        rm_REG(reg_index) => read_GPR(wsize, reg_index),
+        rm_MEM(mem_addr) => read_memory(wsize_bytes, mem_addr, create_readAccessDescriptor()),
+    }
+}
+
+/* read register / memory / immediate operand */
+val read_rmi_operand: forall 'm, 'm in {8, 16, 32, 64}. (int('m), rmi_operand) -> bits('m)
+function read_rmi_operand(wsize, operand: rmi_operand) = {
+    let wsize_bytes = wsize / 8;
+    assert('m == wsize_bytes * 8); // required for type-checking
+    match operand {
+        rmi_IMM(imm) => read_imm(wsize, imm),
+        rmi_REG(reg_index) => read_GPR(wsize, reg_index),
+        rmi_MEM(mem_addr) => read_memory(wsize_bytes, mem_addr, create_readAccessDescriptor()),
+    }
+}
+
+/* overloaded function to read any operand type present in the ast */
+overload read_operand = {read_rm_operand, read_rmi_operand, read_imm, read_GPR}
+
+/* write to reg or mem location */
+val write_rm_operand: forall 'm, 'm in {8, 16, 32, 64}. (int('m), rm_operand, bits('m)) -> unit
+function write_rm_operand(wsize, operand: rm_operand, value) = {
+    let wsize_bytes = wsize / 8;
+    assert('m == wsize_bytes * 8); // required for type-checking
+    match operand {
+        rm_REG(reg_index) => write_GPR(wsize, reg_index, value),
+        rm_MEM(mem_addr) => write_memory(wsize_bytes, mem_addr, value, create_writeAccessDescriptor()),
+    }
+}
+
+/* overloaded function to write to any register or memory type */
+overload write_operand = {write_rm_operand, write_GPR}

prelude.sail

@@ -1,2 +1,19 @@
 default Order dec // LSB is index 0
+$define CONCURRENCY_INTERFACE_V2 // use concurrency_interface/read_write_v2.sail instead of v1
 $include <prelude.sail>
+
+// use equality overload from sail-tiny-arm
+val eq_any = pure {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq", lean: "BEq.beq", c: "eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
+val eq_bits_int : forall 'n 'm, 'n >= 0 & 'm >= 0. (bits('n), int('m)) -> bool
+function eq_bits_int (x, y) = (unsigned(x) == y)
+overload operator == = {eq_any, eq_bits_int}
+
+overload operator / = {tdiv_int}
+
+val fail: string -> unit
+function fail(message) = assert(false, message)
+
+val flip_bit: bit -> bit
+function flip_bit(bit_to_flip) = {
+    if bit_to_flip == bitzero then bitone else bitzero;
+}

registers.sail

@@ -1,19 +1,5 @@
-type reg_index = range(0, 15) // range of registers that one can refer to
-type word_size = {8,16,32,64}
-type imm8 = bits(8)
-type imm16 = bits(16)
-type imm32 = bits(32)
-type imm64 = bits(64)
-union imm = {
-    IMM8: imm8,
-    IMM16: imm16,
-    IMM32: imm32,
-    IMM64: imm64
-}
-union imm_or_reg = {
-    IMM: imm,
-    REG: reg_index
-}
+/* range of registers that one can refer to */
+type reg_index = range(0, 15)
 
 /* program counter */
 
@@ -58,35 +44,46 @@ let GPRs : vector(16, register(bits(64))) = [
     ref RAX
 ]
 
-/* status flags, part of register RFLAGS (which is mostly restricted access) */
-// could use bitfield for this
-register CF: bits(1) // bit 0
-register PF: bits(1) // bit 2
-register AF: bits(1) // bit 4
-register ZF: bits(1) // bit 6
-register SF: bits(1) // bit 7
-register OF: bits(1) // bit 11
-
-/*
-read and write least-significant 8,16,32,64 (32 with 0 extend for write) bits 
- */
+/* register RFLAGS, system and status flags + mostly restricted access */
+bitfield rflags : bits(64) = {
+    // status flags
+    OF: 11, // overflow flag (for operations between signed values)
+    SF: 7, // sign flag
+    ZF: 6, // zero flag
+    AF: 4, // auxiliary carry flag
+    PF: 2, // parity flag
+    CF: 0 // carry flag (for operations between unsigned values)
+}
+register RFLAGS: rflags
 
- val read_reg: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_index) -> bits('m)
+/* read and write least-significant 8,16,32,64 (32 with 0 extend for write) bits */
+ val read_GPR: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_index) -> bits('m)
 
- function read_reg(wsize, i: reg_index) = {
+ function read_GPR(wsize, i: reg_index) = {
     let reg = *GPRs[i];
     reg[wsize - 1 .. 0]
 }
 
-val write_reg: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_index, bits('m)) -> unit
+val write_GPR: forall 'm, 'm in {8, 16, 32, 64}. (int('m), reg_index, bits('m)) -> unit
 
-function write_reg(wsize, i: reg_index, value) = {
+function write_GPR(wsize, i: reg_index, value) = {
     if wsize == 32 then {
         // if writing 32 bits to a register, the value to be written is zero-extended to 64 bits
-        (*GPRs[i])[63 .. 32]= 0x0000_0000;
-        (*GPRs[i])[31 .. 0]= value;
+        (*GPRs[i])[63 .. 32] = 0x0000_0000;
+        (*GPRs[i])[31 .. 0] = value;
     }
     else
         // the value is written to the last wsize bits of the register
         (*GPRs[i])[wsize - 1 .. 0] = value;
-}
+}
+
+/* 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];
+}