summaryrefslogtreecommitdiff
path: root/test/c
diff options
context:
space:
mode:
Diffstat (limited to 'test/c')
-rw-r--r--test/c/cheri_capreg.expect10
-rw-r--r--test/c/cheri_capreg.sail254
-rw-r--r--test/c/eq_struct.expect1
-rw-r--r--test/c/eq_struct.sail38
-rw-r--r--test/c/foreach_none.expect1
-rw-r--r--test/c/foreach_none.sail11
-rw-r--r--test/c/gvectorlit.expect4
-rw-r--r--test/c/large_bitvector.expect12
-rw-r--r--test/c/large_bitvector.sail30
9 files changed, 359 insertions, 2 deletions
diff --git a/test/c/cheri_capreg.expect b/test/c/cheri_capreg.expect
new file mode 100644
index 00000000..6e46a0e8
--- /dev/null
+++ b/test/c/cheri_capreg.expect
@@ -0,0 +1,10 @@
+default_cap = 0b10000000000000000000000000000000011111111111111110000111111111110000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001111111111111111111111111111111111111111111111111111111111111111
+null_cap = 0b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001111111111111111111111111111111111111111111111111111111111111111
+C03 = 0b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
+C02 = 0b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
+C01 = 0b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
+DDC = 0b10000000000000000000000000000000011111111111111110000111111111110000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001111111111111111111111111111111111111111111111111111111111111111
+C03 = 0b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001111111111111111111111111111111111111111111111111111111111111111
+C02 = 0b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001111111111111111111111111111111111111111111111111111111111111111
+C01 = 0b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001111111111111111111111111111111111111111111111111111111111111111
+DDC = 0b10000000000000000000000000000000011111111111111110000111111111110000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001111111111111111111111111111111111111111111111111111111111111111
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
diff --git a/test/c/eq_struct.expect b/test/c/eq_struct.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/eq_struct.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/eq_struct.sail b/test/c/eq_struct.sail
new file mode 100644
index 00000000..b4258569
--- /dev/null
+++ b/test/c/eq_struct.sail
@@ -0,0 +1,38 @@
+default Order dec
+
+$include <flow.sail>
+$include <exception_basic.sail>
+
+val eq = "eq_anything" : forall ('a : Type). ('a, 'a) -> bool
+
+overload operator == = {eq}
+
+val neq : forall ('a : Type). ('a, 'a) -> bool
+
+overload operator != = {neq}
+
+overload ~ = {not_bool}
+
+function neq(x, y) = ~(eq(x, y))
+
+struct S = {
+ field1: int,
+ field2: vector(8, dec, bit)
+}
+
+val "print" : string -> unit
+
+val main : unit -> unit effect {escape}
+
+function main() = {
+ let s : S = struct {
+ field1 = 4,
+ field2 = 0xFF
+ };
+ assert(s == s, "1");
+ assert(~(s == { s with field2 = 0xAB }), "2");
+ assert(s != { s with field1 = 5}, "3");
+ assert(s == { s with field2 = 0xFF });
+ assert({ s with field1 = 0} == {s with field1 = 0});
+ print("ok\n")
+} \ No newline at end of file
diff --git a/test/c/foreach_none.expect b/test/c/foreach_none.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/foreach_none.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/foreach_none.sail b/test/c/foreach_none.sail
new file mode 100644
index 00000000..bc960b85
--- /dev/null
+++ b/test/c/foreach_none.sail
@@ -0,0 +1,11 @@
+
+val "print" : string -> unit
+
+val main : unit -> unit
+
+function main() = {
+ foreach (i from 0 to -1 by 1 in inc) {
+ print("unreachable\n");
+ };
+ print("ok\n")
+} \ No newline at end of file
diff --git a/test/c/gvectorlit.expect b/test/c/gvectorlit.expect
index d3a1e9ab..9328600c 100644
--- a/test/c/gvectorlit.expect
+++ b/test/c/gvectorlit.expect
@@ -1,2 +1,2 @@
-x[0] = 0xAB
-x[1] = 0xCD
+x[0] = 0xCD
+x[1] = 0xAB
diff --git a/test/c/large_bitvector.expect b/test/c/large_bitvector.expect
new file mode 100644
index 00000000..f67ec84a
--- /dev/null
+++ b/test/c/large_bitvector.expect
@@ -0,0 +1,12 @@
+x = 0x1FFFF0000FFFFFFFF
+length(x) = 68
+y = 0x1FFFF0000FFFFFFFF1FFFF0000FFFFFFFF1FFFF0000FFFFFFFF
+length(y) = 204
+z = 0x1FFFF0000FFFFFFFF1FFFF0000FFFFFFFF1CAFE0000FFFFFFFF
+length(z) = 204
+q = 0xFF0000FFFFFFFF1FFFF0000FFFFFFFF1CAFE0000FFFFFFFF
+w = -24519554509435141245919758063389544641259977658452672513
+length(q) = 192
+0x8000
+0b1 @ zeros(64 * 3 - 1) = 0x800000000000000000000000000000000000000000000000
+q = 0x800000000000000000000000000000000000000000000000
diff --git a/test/c/large_bitvector.sail b/test/c/large_bitvector.sail
new file mode 100644
index 00000000..78189d7d
--- /dev/null
+++ b/test/c/large_bitvector.sail
@@ -0,0 +1,30 @@
+default Order dec
+
+$include <arith.sail>
+$include <vector_dec.sail>
+
+val "zeros" : forall 'n. int('n) -> bits('n)
+
+val main : unit -> unit
+
+function main() = {
+ let x = [0x1FFFF0000FFFF0000 with 15 .. 0 = 0xFFFF];
+ print_bits("x = ", x);
+ print_int("length(x) = ", length(x));
+ let y = replicate_bits(x, 3);
+ print_bits("y = ", y);
+ print_int("length(y) = ", length(y));
+ let z = [y with 63 .. (63 - 15) = 0xCAFE];
+ print_bits("z = ", z);
+ print_int("length(z) = ", length(z));
+ q = slice(z, 0, 64 * 3);
+ print_bits("q = ", q);
+ w = signed(q);
+ print_int("w = ", w);
+ print_int("length(q) = ", length(q));
+ print_bits("", [0xFFFF with 14 .. 0 = zeros(15)]);
+ print_bits("0b1 @ zeros(64 * 3 - 1) = ", 0b1 @ zeros(64 * 3 - 1));
+ q[64 * 3 - 2 .. 0] = zeros(64 * 3 - 1);
+ print_bits("q = ", q);
+ ()
+}
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-16 00:11:40 +0000