diff options
| -rw-r--r-- | lib/reverse_endianness.sail | 32 | ||||
| -rw-r--r-- | src/jib/jib_smt.ml | 30 | ||||
| -rw-r--r-- | test/smt/revrev_endianness.sail | 25 | ||||
| -rw-r--r-- | test/smt/revrev_endianness2.sail | 20 |
4 files changed, 97 insertions, 10 deletions
diff --git a/lib/reverse_endianness.sail b/lib/reverse_endianness.sail new file mode 100644 index 00000000..ff75f6c3 --- /dev/null +++ b/lib/reverse_endianness.sail @@ -0,0 +1,32 @@ +$ifndef _REVERSE_ENDIANNESS +$define _REVERSE_ENDIANNESS + +$ifdef _DEFAULT_DEC + +$include <vector_dec.sail> + +/* reverse_endianness function set up to ensure it generates good SMT +definitions. The concat/extract pattern may be less efficient in other +backends where these are not primitive operations. */ + +val reverse_endianness : forall 'n, 'n in {8, 16, 32, 64, 128}. bits('n) -> bits('n) + +function reverse_endianness(xs) = { + let len = length(xs); + if len == 8 then { + xs + } else if len == 16 then { + xs[7 .. 0] @ xs[15 .. 8] + } else if len == 32 then { + xs[7 .. 0] @ xs[15 .. 8] @ xs[23 .. 16] @ xs[31 .. 24] + } else if len == 64 then { + xs[7 .. 0] @ xs[15 .. 8] @ xs[23 .. 16] @ xs[31 .. 24] @ xs[39 .. 32] @ xs[47 .. 40] @ xs[55 .. 48] @ xs[63 .. 56] + } else { + xs[7 .. 0] @ xs[15 .. 8] @ xs[23 .. 16] @ xs[31 .. 24] @ xs[39 .. 32] @ xs[47 .. 40] @ xs[55 .. 48] @ xs[63 .. 56] + @ xs[71 .. 64] @ xs[79 .. 72] @ xs[87 .. 80] @ xs[95 .. 88] @ xs[103 .. 96] @ xs[111 .. 104] @ xs[119 .. 112] @ xs[127 .. 120] + } +} + +$endif + +$endif diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index da0048d7..6308a73f 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -536,6 +536,11 @@ let builtin_min_int ctx v1 v2 ret_ctyp = smt1, smt2) +let bvmask ctx len = + let all_ones = bvones (lbits_size ctx) in + let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); len]) in + bvnot (bvshl all_ones shift) + let builtin_eq_bits ctx v1 v2 = match cval_ctyp v1, cval_ctyp v2 with | CT_fbits (n, _), CT_fbits (m, _) -> @@ -545,15 +550,20 @@ let builtin_eq_bits ctx v1 v2 = Fn ("=", [smt1; smt2]) | CT_lbits _, CT_lbits _ -> - Fn ("=", [smt_cval ctx v1; smt_cval ctx v2]) + let len1 = Fn ("len", [smt_cval ctx v1]) in + let contents1 = Fn ("contents", [smt_cval ctx v1]) in + let len2 = Fn ("len", [smt_cval ctx v1]) in + let contents2 = Fn ("contents", [smt_cval ctx v1]) in + Fn ("and", [Fn ("=", [len1; len2]); + Fn ("=", [Fn ("bvand", [bvmask ctx len1; contents1]); Fn ("bvand", [bvmask ctx len2; contents2])])]) | CT_lbits _, CT_fbits (n, _) -> - let smt2 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v2) in - Fn ("=", [Fn ("contents", [smt_cval ctx v1]); smt2]) + let smt1 = unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [smt_cval ctx v1])) in + Fn ("=", [smt1; smt_cval ctx v2]) | CT_fbits (n, _), CT_lbits _ -> - let smt1 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v1) in - Fn ("=", [smt1; Fn ("contents", [smt_cval ctx v2])]) + let smt2 = unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [smt_cval ctx v2])) in + Fn ("=", [smt_cval ctx v1; smt2]) | _ -> builtin_type_error ctx "eq_bits" [v1; v2] None @@ -566,11 +576,6 @@ let builtin_zeros ctx v ret_ctyp = Fn ("Bits", [extract (ctx.lbits_index - 1) 0 (smt_cval ctx v); bvzero (lbits_size ctx)]) | _ -> builtin_type_error ctx "zeros" [v] (Some ret_ctyp) -let bvmask ctx len = - let all_ones = bvones (lbits_size ctx) in - let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); len]) in - bvnot (bvshl all_ones shift) - let builtin_ones ctx cval = function | CT_fbits (n, _) -> bvones n | CT_lbits _ -> @@ -747,6 +752,9 @@ let builtin_vector_subrange ctx vec i j ret_ctyp = | CT_fbits (n, _), CT_constant i, CT_constant j -> Extract (Big_int.to_int i, Big_int.to_int j, smt_cval ctx vec) + | CT_lbits _, CT_constant i, CT_constant j -> + Extract (Big_int.to_int i, Big_int.to_int j, Fn ("contents", [smt_cval ctx vec])) + | _ -> builtin_type_error ctx "vector_subrange" [vec; i; j] (Some ret_ctyp) let builtin_vector_access ctx vec i ret_ctyp = @@ -1162,6 +1170,8 @@ let rec smt_conversion ctx from_ctyp to_ctyp x = bvint ctx.lint_size c | CT_fint sz, CT_lint -> force_size ctx ctx.lint_size sz x + | CT_lbits _, CT_fbits (n, _) -> + unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [x])) | _, _ -> failwith (Printf.sprintf "Cannot perform conversion from %s to %s" (string_of_ctyp from_ctyp) (string_of_ctyp to_ctyp)) let define_const ctx id ctyp exp = Define_const (zencode_name id, smt_ctyp ctx ctyp, exp) diff --git a/test/smt/revrev_endianness.sail b/test/smt/revrev_endianness.sail new file mode 100644 index 00000000..f792871f --- /dev/null +++ b/test/smt/revrev_endianness.sail @@ -0,0 +1,25 @@ +default Order dec + +$include <reverse_endianness.sail> + +$property +function prop forall 'n, 'n in {8, 16, 32, 64, 128}. (n: int('n), xs: bits('n)) -> bool = { + if length(xs) == 8 then { + let ys: bits(8) = xs; + reverse_endianness(reverse_endianness(ys)) == ys + } else if length(xs) == 16 then { + let ys: bits(16) = xs; + reverse_endianness(reverse_endianness(ys)) == ys + } else if length(xs) == 32 then { + let ys: bits(32) = xs; + reverse_endianness(reverse_endianness(ys)) == ys + } else if length(xs) == 64 then { + let ys: bits(64) = xs; + reverse_endianness(reverse_endianness(ys)) == ys + } else if length(xs) == 128 then { + let ys: bits(128) = xs; + reverse_endianness(reverse_endianness(ys)) == ys + } else { + true + } +} diff --git a/test/smt/revrev_endianness2.sail b/test/smt/revrev_endianness2.sail new file mode 100644 index 00000000..33ba93a2 --- /dev/null +++ b/test/smt/revrev_endianness2.sail @@ -0,0 +1,20 @@ +default Order dec + +$include <reverse_endianness.sail> + +$property +function prop forall 'n, 'n in {8, 16, 32, 64, 128}. (n: int('n), xs: bits('n)) -> bool = { + if length(xs) == 8 then { + reverse_endianness(reverse_endianness(xs)) == xs + } else if length(xs) == 16 then { + reverse_endianness(reverse_endianness(xs)) == xs + } else if length(xs) == 32 then { + reverse_endianness(reverse_endianness(xs)) == xs + } else if length(xs) == 64 then { + reverse_endianness(reverse_endianness(xs)) == xs + } else if length(xs) == 128 then { + reverse_endianness(reverse_endianness(xs)) == xs + } else { + true + } +} |