Merge remote-tracking branch 'origin/sail2' into c_fixes

1 files changed, 254 insertions, 0 deletions

diff --git a/test/c/cheri_capreg.sail b/test/c/cheri_capreg.sail
new file mode 100644
index 00000000..e8890a4a
--- /dev/null
+++ b/test/c/cheri_capreg.sail
@@ -0,0 +1,254 @@
+default Order dec
+
+/* this is here because if we don't have it before including vector_dec
+   we get infinite loops caused by interaction with bool/bit casts */
+val eq_bit2 = "eq_bit" : (bit, bit) -> bool
+overload operator == = {eq_bit2}
+
+$include <vector_dec.sail>
+
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+/* sneaky deref with no effect necessary for bitfield writes */
+val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
+
+val zeros_0 = "zeros" : forall 'n. int('n) -> bits('n)
+
+val zeros : forall 'n. unit -> bits('n)
+function zeros() = zeros_0('n)
+
+val ones : forall 'n, 'n >= 0 . unit -> bits('n)
+function ones() = replicate_bits (0b1,'n)
+
+val xor_vec = {c: "xor_bits" , _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val int_power = {ocaml: "int_power", lem: "pow", coq: "Z.pow"} : (int, int) -> int
+
+overload operator ^ = {xor_vec, int_power}
+
+val cast bool_to_bits : bool -> bits(1)
+function bool_to_bits x = if x then 0b1 else 0b0
+
+val cast bit_to_bool : bit -> bool
+function bit_to_bool b = match b {
+  bitone => true,
+  bitzero => false
+}
+
+val to_bits : forall 'l, 'l >= 0 .(atom('l), int) -> bits('l)
+function to_bits (l, n) = get_slice_int(l, n, 0)
+
+/* 256 bit cap + tag */
+type CapReg = bits(257)
+
+struct CapStruct = {
+  tag                     : bool    ,
+  padding                 : bits(8) ,
+  otype                   : bits(24),
+  uperms                  : bits(16),
+  perm_reserved11_14      : bits(4) ,
+  access_system_regs      : bool    ,
+  permit_unseal           : bool    ,
+  permit_ccall            : bool    ,
+  permit_seal             : bool    ,
+  permit_store_local_cap  : bool    ,
+  permit_store_cap        : bool    ,
+  permit_load_cap         : bool    ,
+  permit_store            : bool    ,
+  permit_load             : bool    ,
+  permit_execute          : bool    ,
+  global                  : bool    ,
+  sealed                  : bool    ,
+  address                 : bits(64),
+  base                    : bits(64),
+  length                  : bits(64),
+}
+
+let null_cap : CapStruct = struct {
+  tag = false,
+  padding = zeros(),
+  otype = zeros(),
+  uperms = zeros(),
+  perm_reserved11_14 = zeros(),
+  access_system_regs = false,
+  permit_unseal = false,
+  permit_ccall = false,
+  permit_seal = false,
+  permit_store_local_cap = false,
+  permit_store_cap = false,
+  permit_load_cap = false,
+  permit_store = false,
+  permit_load = false,
+  permit_execute = false,
+  global = false,
+  sealed = false,
+  address = zeros(),
+  base = zeros(),
+  length = 0xffffffffffffffff
+}
+
+let default_cap : CapStruct = struct {
+  tag = true,
+  padding = zeros(),
+  otype = zeros(),
+  uperms = ones(),
+  perm_reserved11_14 = zeros(),
+  access_system_regs = true,
+  permit_unseal = true,
+  permit_ccall = true,
+  permit_seal = true,
+  permit_store_local_cap = true,
+  permit_store_cap = true,
+  permit_load_cap = true,
+  permit_store = true,
+  permit_load = true,
+  permit_execute = true,
+  global = true,
+  sealed = false,
+  address = zeros(),
+  base = zeros(),
+  length = 0xffffffffffffffff
+}
+
+let null_cap : CapStruct = struct {
+  tag = false,
+  padding = zeros(),
+  otype = zeros(),
+  uperms = zeros(),
+  perm_reserved11_14 = zeros(),
+  access_system_regs = false,
+  permit_unseal = false,
+  permit_ccall = false,
+  permit_seal = false,
+  permit_store_local_cap = false,
+  permit_store_cap = false,
+  permit_load_cap = false,
+  permit_store = false,
+  permit_load = false,
+  permit_execute = false,
+  global = false,
+  sealed = false,
+  address = zeros(),
+  base = zeros(),
+  length = 0xffffffffffffffff
+}
+
+let 'cap_size = 32
+
+function capRegToCapStruct(capReg) : CapReg -> CapStruct =
+  struct {
+    tag                        = capReg[256],
+    padding                    = capReg[255..248],
+    otype                      = capReg[247..224],
+    uperms                     = capReg[223..208],
+    perm_reserved11_14         = capReg[207..204],
+    access_system_regs         = capReg[203],
+    permit_unseal              = capReg[202],
+    permit_ccall               = capReg[201],
+    permit_seal                = capReg[200],
+    permit_store_local_cap     = capReg[199],
+    permit_store_cap           = capReg[198],
+    permit_load_cap            = capReg[197],
+    permit_store               = capReg[196],
+    permit_load                = capReg[195],
+    permit_execute             = capReg[194],
+    global                     = capReg[193],
+    sealed                     = capReg[192],
+    address                    = capReg[191..128],
+    base                       = capReg[127..64],
+    length                     = capReg[63..0]
+  }
+
+function getCapPerms(cap) : CapStruct -> bits(31) = 
+  (
+    cap.uperms
+      @ cap.perm_reserved11_14
+      @ cap.access_system_regs
+      @ cap.permit_unseal
+      @ cap.permit_ccall
+      @ cap.permit_seal
+      @ cap.permit_store_local_cap
+      @ cap.permit_store_cap
+      @ cap.permit_load_cap
+      @ cap.permit_store
+      @ cap.permit_load
+      @ cap.permit_execute
+      @ cap.global
+  )
+
+
+/* Function to convert capabilities to in-memory format. */
+function capStructToMemBits256(cap) : CapStruct -> bits(256) =
+  (
+        cap.padding
+      @ cap.otype
+      @ getCapPerms(cap)
+      @ cap.sealed
+      @ cap.address
+      @ cap.base
+      @ cap.length
+  )
+
+
+/* When saving/restoring capabilities xor them with bits of null_cap --
+   this ensures that canonical null_cap is always all-zeros in memory
+   even though it may have bits set logically (e.g. length or exponent) */
+
+let null_cap_bits : bits(256) = capStructToMemBits256(null_cap)
+
+function capStructToMemBits(cap) : CapStruct -> bits(256)=
+  capStructToMemBits256(cap) ^ null_cap_bits
+
+function memBitsToCapBits(tag, b) : (bool, bits(256)) -> bits(257)  =
+  tag @ (b ^ null_cap_bits)
+
+function capStructToCapReg(cap) : CapStruct -> CapReg = cap.tag @ capStructToMemBits256(cap)
+
+register DDC : CapReg
+register C01 : CapReg
+register C02 : CapReg
+register C03 : CapReg
+
+let CapRegs : vector(4, dec, register(CapReg)) =
+  [
+    ref C03,
+    ref C02,
+    ref C01,
+    ref DDC
+  ]
+
+val readCapReg : bits(2) -> CapStruct effect {rreg}
+function readCapReg(n) =
+  if (n == 0b00) then
+    default_cap
+  else
+    let i = unsigned(n) in
+    capRegToCapStruct(reg_deref(CapRegs[i]))
+
+function writeCapReg(n, cap) : (bits(2), CapStruct) -> unit =
+  if (n == 0b00) then
+    ()
+  else
+    let i = unsigned(n) in
+    (*CapRegs[i]) = capStructToCapReg(cap) 
+
+val "print_bits" : forall 'n. (string, bits('n)) -> unit
+
+val main : unit -> unit effect {rreg, wreg}
+
+function main() = {
+  print_bits("default_cap = ", capStructToCapReg(default_cap));
+  print_bits("null_cap = ", capStructToCapReg(null_cap));
+  DDC = capStructToCapReg(default_cap);
+  print_bits("C03 = ", C03);
+  print_bits("C02 = ", C02);
+  print_bits("C01 = ", C01);
+  print_bits("DDC = ", DDC);
+  foreach(i from 1 to 3) {
+    let idx = to_bits(2, i);
+    writeCapReg(idx, null_cap)
+  };
+  print_bits("C03 = ", C03);
+  print_bits("C02 = ", C02);
+  print_bits("C01 = ", C01);
+  print_bits("DDC = ", DDC);
+}
\ No newline at end of file