diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/prelude.sail | 59 | ||||
| -rw-r--r-- | lib/prelude_wrappers.sail | 49 |
2 files changed, 81 insertions, 27 deletions
diff --git a/lib/prelude.sail b/lib/prelude.sail index 795fe8fc..fe5d7d5b 100644 --- a/lib/prelude.sail +++ b/lib/prelude.sail @@ -3,9 +3,9 @@ val cast forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m val forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0 - (2**('m - 1)):2**('m - 1) - 1|] effect pure signed -val extern forall Num 'n, Num 'm. [|0:'n|] -> vector<'m - 1,'m,dec,bit> effect pure to_vec = "to_vec_dec" +val forall Num 'n, Num 'm. [|0:'n|] -> vector<'m - 1,'m,dec,bit> effect pure to_vec -val extern forall Num 'm. int -> vector<'m - 1,'m,dec,bit> effect pure to_svec = "to_vec_dec" +val forall Num 'm. int -> vector<'m - 1,'m,dec,bit> effect pure to_svec (* Vector access can't actually be properly polymorphic on vector direction because of the ranges being different for each type, so @@ -39,14 +39,14 @@ overload vector_subrange [bitvector_subrange_inc; bitvector_subrange_dec; vector (* Type safe vector append *) val extern forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,'a> effect pure vec_append = "vector_concat" - -val (list<bit>, list<bit>) -> list<bit> effect pure list_append + (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,'a> effect pure vector_append = "vector_concat" val extern forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,bit> effect pure bitvec_append = "bitvector_concat" + (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,bit> effect pure bitvector_append = "bitvector_concat" + +val (list<bit>, list<bit>) -> list<bit> effect pure list_append -overload vector_append [bitvec_append; vec_append; list_append] +overload append [bitvector_append; vector_append; list_append] (* Implicit register dereferencing *) val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref @@ -65,27 +65,27 @@ val forall Num 'n, Num 'o, Order 'ord. overload (deinfix ^^) [duplicate; duplicate_bits; duplicate_to_list; duplicate_bits_to_list] (* Bitvector extension *) -val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. +val extern forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz -val forall Num 'm, Num 'p, Order 'ord. +val extern forall Num 'm, Num 'p, Order 'ord. list<bit> -> vector<'p, 'm, 'ord, bit> effect pure extz_bl -val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. +val extern forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts -val forall Num 'm, Num 'p, Order 'ord. +val extern forall Num 'm, Num 'p, Order 'ord. list<bit> -> vector<'p, 'm, 'ord, bit> effect pure exts_bl (* If we want an automatic bitvector extension, then this is the function to use, but I've disabled the cast because it hides signedness bugs. *) -val (*cast*) forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'n. +val extern (*cast*) forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'n. vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extzi overload EXTZ [extz; extz_bl] overload EXTS [exts; exts_bl] -val forall Type 'a, Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'o. +val extern forall Type 'a, Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'o. vector<'n, 'm, 'ord, 'a> -> vector<'p, 'o, 'ord, 'a> effect pure mask (* Adjust the start index of a decreasing bitvector *) @@ -98,9 +98,12 @@ val cast forall Num 'n, Num 'm, Num 'o, 'n >= 'm - 1, 'o >= 'm - 1. effect pure adjust_dec (* Various casts from 0 and 1 to bitvectors *) -val cast forall Num 'n, Num 'l, Order 'ord. [:0:] -> vector<'n,'l,'ord,bit> effect pure cast_0_vec -val cast forall Num 'n, Num 'l, Order 'ord. [:1:] -> vector<'n,'l,'ord,bit> effect pure cast_1_vec -val cast forall Num 'n, Num 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec +val cast forall Num 'n, Num 'l. [:0:] -> vector<'n,'l,dec,bit> effect pure cast_0_vec_dec +val cast forall Num 'n, Num 'l. [:1:] -> vector<'n,'l,dec,bit> effect pure cast_1_vec_dec +val cast forall Num 'n, Num 'l. [|0:1|] -> vector<'n,'l,dec,bit> effect pure cast_01_vec_dec +val cast forall Num 'n, Num 'l. [:0:] -> vector<'n,'l,inc,bit> effect pure cast_0_vec_inc +val cast forall Num 'n, Num 'l. [:1:] -> vector<'n,'l,inc,bit> effect pure cast_1_vec_inc +val cast forall Num 'n, Num 'l. [|0:1|] -> vector<'n,'l,inc,bit> effect pure cast_01_vec_inc val cast forall Num 'n, Order 'ord. vector<'n,1,'ord,bit> -> bool effect pure cast_vec_bool val cast bit -> bool effect pure cast_bit_bool @@ -113,7 +116,7 @@ val forall Num 'n, Num 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> bit effect p (* Arithmetic *) val extern forall Num 'n, Num 'm, Num 'o, Num 'p. - ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add + ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add_range = "add" val extern (nat, nat) -> nat effect pure add_nat = "add" @@ -129,7 +132,7 @@ val forall Num 'n, Num 'o, Order 'ord. (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure add_overflow_vec val extern forall Num 'n, Num 'm, Num 'o, Num 'p. - ([|'n:'m|], [|'o:'p|]) -> [|'n - 'p:'m - 'o|] effect pure sub + ([|'n:'m|], [|'o:'p|]) -> [|'n - 'p:'m - 'o|] effect pure sub_range = "sub" val extern (int, int) -> int effect pure sub_int = "sub" @@ -146,7 +149,7 @@ overload (deinfix +) [ add_vec; add_overflow_vec; add_vec_int; - add; + add_range; add_nat; add_int ] @@ -155,26 +158,28 @@ overload (deinfix -) [ sub_vec_int; sub_vec; sub_underflow_vec; - sub; + sub_range; sub_int ] val extern bool -> bit effect pure bool_to_bit = "bool_to_bitU" -val (int, int) -> int effect pure mul_int +val (int, int) -> int effect pure mult_int +val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> [:'n * 'm:] effect pure mult_range = "mult_int" val forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mul_vec + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mult_vec overload (deinfix * ) [ - mul_vec; - mul_int + mult_vec; + mult; + mult_int ] val forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mul_svec + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mult_svec overload (deinfix *_s) [ - mul_svec + mult_svec ] val extern (bool, bool) -> bool effect pure bool_xor @@ -281,7 +286,7 @@ val (int, int) -> int effect pure modulo overload (deinfix mod) [modulo] -val extern forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'m:] effect pure vec_length = "length" +val extern forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'m:] effect pure vector_length = "length" val forall Type 'a. list<'a> -> nat effect pure list_length val extern forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [:'m:] effect pure bitvector_length = "bvlength" diff --git a/lib/prelude_wrappers.sail b/lib/prelude_wrappers.sail new file mode 100644 index 00000000..4568f6ab --- /dev/null +++ b/lib/prelude_wrappers.sail @@ -0,0 +1,49 @@ +val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec +val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,inc,bit> effect pure to_vec_inc +function forall Num 'n, Num 'm. (vector<'m - 1,'m,dec,bit>) to_vec (n) = to_vec_dec ((sizeof 'm) - 1, sizeof 'm, n) + +function forall Num 'm. (vector<'m - 1,'m,dec,bit>) to_svec (n) = to_vec_dec ((sizeof 'm) - 1, sizeof 'm, n) + +(* Bitvector extension *) +val extern forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. + ([:'p:], [:'m:], vector<'o, 'n, 'ord, bit>) -> vector<'p, 'm, 'ord, bit> effect pure extz' = "extz" +function forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. + (vector<'p, 'm, 'ord, bit>) extz (v) = extz' (sizeof 'p, sizeof 'm, v) + +val extern forall Num 'm, Num 'p, Order 'ord. + ([:'p:], [:'m:], list<bit>) -> vector<'p, 'm, 'ord, bit> effect pure extz_bl' = "extz_bl" +function forall Num 'm, Num 'p, Order 'ord. + (vector<'p, 'm, 'ord, bit>) extz_bl (v) = extz_bl' (sizeof 'p, sizeof 'm, v) + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. + ([:'p:], [:'m:], vector<'o, 'n, 'ord, bit>) -> vector<'p, 'm, 'ord, bit> effect pure exts' = "exts" +function forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. + (vector<'p, 'm, 'ord, bit>) exts (v) = exts' (sizeof 'p, sizeof 'm, v) + +val extern forall Num 'm, Num 'p, Order 'ord. + ([:'p:], [:'m:], list<bit>) -> vector<'p, 'm, 'ord, bit> effect pure exts_bl' = "exts_bl" +function forall Num 'm, Num 'p, Order 'ord. + vector<'p, 'm, 'ord, bit> exts_bl (v) = exts_bl' (sizeof 'p, sizeof 'm, v) + +val extern forall Type 'a, Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'o. + ([:'p:], [:'o:], vector<'n, 'm, 'ord, 'a>) -> vector<'p, 'o, 'ord, 'a> effect pure mask' = "extz" +function forall Type 'a, Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'o. + (vector<'p, 'o, 'ord, 'a>) mask (v) = mask' (sizeof 'p, sizeof 'o, v) + +(* Adjust the start index of a decreasing bitvector *) +val extern forall Num 'n, Num 'm, Num 'o, 'n >= 'm - 1, 'o >= 'm - 1. + ([:'o:], vector<'n,'m,dec,bit>) -> vector<'o,'m,dec,bit> + effect pure adjust_dec' = "adjust_start_index" +function forall Num 'n, Num 'm, Num 'o, 'n >= 'm - 1, 'o >= 'm - 1. + (vector<'o,'m,dec,bit>) adjust_dec (v) = adjust_dec' (sizeof 'o, v) + +(* Various casts from 0 and 1 to bitvectors *) +function forall Num 'n, Num 'l. (vector<'n,'l,dec,bit>) cast_0_vec_dec i = to_vec_dec (sizeof 'n, sizeof 'l, i) +function forall Num 'n, Num 'l. (vector<'n,'l,dec,bit>) cast_1_vec_dec i = to_vec_dec (sizeof 'n, sizeof 'l, i) +function forall Num 'n, Num 'l. (vector<'n,'l,dec,bit>) cast_01_vec_dec i = to_vec_dec (sizeof 'n, sizeof 'l, i) +function forall Num 'n, Num 'l. (vector<'n,'l,inc,bit>) cast_0_vec_inc i = to_vec_inc (sizeof 'n, sizeof 'l, i) +function forall Num 'n, Num 'l. (vector<'n,'l,inc,bit>) cast_1_vec_inc i = to_vec_inc (sizeof 'n, sizeof 'l, i) +function forall Num 'n, Num 'l. (vector<'n,'l,inc,bit>) cast_01_vec_inc i = to_vec_inc (sizeof 'n, sizeof 'l, i) + +val extern forall Num 'n, Num 'm, 'n >= 'm - 1, 'm >= 1. ([:'n:], [:'m:], bit) -> vector<'n,'m,dec,bit> effect pure cast_bit_vec' = "cast_bit_vec" +function forall Num 'n, Num 'm, 'n >= 'm - 1, 'm >= 1. (vector<'n,'m,dec,bit>) cast_bit_vec b = cast_bit_vec' (sizeof 'n, sizeof 'm, b) |