diff options
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/c_backend.ml | 21 | ||||
| -rw-r--r-- | src/jib/jib_smt.ml | 47 |
2 files changed, 65 insertions, 3 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 2b144d35..2b2234b5 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -1481,6 +1481,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = | "undefined_bitvector", CT_lbits _ -> "UNDEFINED(lbits)" | "undefined_bit", _ -> "UNDEFINED(fbits)" | "undefined_vector", _ -> Printf.sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp) + | "undefined_list", _ -> Printf.sprintf "UNDEFINED(%s)" (sgen_ctyp_name ctyp) | fname, _ -> fname in if fname = "reg_deref" then @@ -1844,6 +1845,9 @@ let codegen_list_clear id ctyp = ^^ string " sail_free(*rop);" ^^ string "}" +let codegen_list_recreate id = + string (Printf.sprintf "static void RECREATE(%s)(%s *rop) { KILL(%s)(rop); *rop = NULL; }" (sgen_id id) (sgen_id id) (sgen_id id)) + let codegen_list_set id ctyp = string (Printf.sprintf "static void internal_set_%s(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id)) ^^ string " if (op == NULL) { *rop = NULL; return; };\n" @@ -1879,6 +1883,20 @@ let codegen_pick id ctyp = else string (Printf.sprintf "static void pick_%s(%s *x, const %s xs) { COPY(%s)(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp)) +let codegen_list_equal id ctyp = + let open Printf in + ksprintf string "static bool EQUAL(%s)(const %s op1, const %s op2) {\n" (sgen_id id) (sgen_id id) (sgen_id id) + ^^ ksprintf string " if (op1 == NULL && op2 == NULL) { return true; };\n" + ^^ ksprintf string " if (op1 == NULL || op2 == NULL) { return false; };\n" + ^^ ksprintf string " return EQUAL(%s)(op1->hd, op2->hd) && EQUAL(%s)(op1->tl, op2->tl);\n" (sgen_ctyp_name ctyp) (sgen_id id) + ^^ string "}" + +let codegen_list_undefined id ctyp = + let open Printf in + ksprintf string "static void UNDEFINED(%s)(%s *rop, %s u) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp) + ^^ ksprintf string " *rop = NULL;\n" + ^^ string "}" + let codegen_list ctx ctyp = let id = mk_id (string_of_ctyp (CT_list ctyp)) in if IdSet.mem id !generated then @@ -1889,9 +1907,12 @@ let codegen_list ctx ctyp = codegen_node id ctyp ^^ twice hardline ^^ codegen_list_init id ^^ twice hardline ^^ codegen_list_clear id ctyp ^^ twice hardline + ^^ codegen_list_recreate id ^^ twice hardline ^^ codegen_list_set id ctyp ^^ twice hardline ^^ codegen_cons id ctyp ^^ twice hardline ^^ codegen_pick id ctyp ^^ twice hardline + ^^ codegen_list_equal id ctyp ^^ twice hardline + ^^ codegen_list_undefined id ctyp ^^ twice hardline end (* Generate functions for working with non-bit vectors of some specific type. *) diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 81b876a4..c4e8576c 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -283,8 +283,14 @@ let smt_conversion ctx from_ctyp to_ctyp x = force_size ctx ctx.lint_size sz x | CT_lint, CT_fint sz -> force_size ctx sz ctx.lint_size x + | CT_lint, CT_fbits (n, _) -> + force_size ctx n ctx.lint_size x + | CT_lint, CT_lbits _ -> + Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int ctx.lint_size); force_size ctx (lbits_size ctx) ctx.lint_size x]) | CT_lbits _, CT_fbits (n, _) -> unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [x])) + | CT_fbits (n, _), CT_fbits (m, _) -> + unsigned_size ctx m n x | CT_fbits (n, _), CT_lbits _ -> Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int n); unsigned_size ctx (lbits_size ctx) n x]) @@ -580,6 +586,8 @@ let bvmask ctx len = let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); len]) in bvnot (bvshl all_ones shift) +let fbits_mask ctx n len = bvnot (bvshl (bvones n) len) + let builtin_eq_bits ctx v1 v2 = match cval_ctyp v1, cval_ctyp v2 with | CT_fbits (n, _), CT_fbits (m, _) -> @@ -796,9 +804,17 @@ let builtin_vector_subrange ctx vec i j ret_ctyp = Extract (Big_int.to_int i, Big_int.to_int j, Fn ("contents", [smt_cval ctx vec])) | CT_fbits (n, _), i_ctyp, CT_constant j, CT_lbits _ when Big_int.equal j Big_int.zero -> - let len = force_size ~checked:false ctx ctx.lbits_index (int_size ctx i_ctyp) (smt_cval ctx i) in + let i' = force_size ~checked:false ctx ctx.lbits_index (int_size ctx i_ctyp) (smt_cval ctx i) in + let len = bvadd i' (bvint ctx.lbits_index (Big_int.of_int 1)) in Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; unsigned_size ctx (lbits_size ctx) n (smt_cval ctx vec)])]) + | CT_fbits (n, b), i_ctyp, j_ctyp, ret_ctyp -> + let i' = force_size ctx n (int_size ctx i_ctyp) (smt_cval ctx i) in + let j' = force_size ctx n (int_size ctx j_ctyp) (smt_cval ctx j) in + let len = bvadd (bvadd i' (bvneg j')) (bvint n (Big_int.of_int 1)) in + let vec' = bvand (bvlshr (smt_cval ctx vec) j') (fbits_mask ctx n len) in + smt_conversion ctx (CT_fbits (n, b)) ret_ctyp vec' + | _ -> builtin_type_error ctx "vector_subrange" [vec; i; j] (Some ret_ctyp) let builtin_vector_access ctx vec i ret_ctyp = @@ -844,17 +860,31 @@ let builtin_vector_update ctx vec i x ret_ctyp = let builtin_vector_update_subrange ctx vec i j x ret_ctyp = match cval_ctyp vec, cval_ctyp i, cval_ctyp j, cval_ctyp x, ret_ctyp with - | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 > Big_int.to_int i && Big_int.to_int j >= 0 -> + | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 > Big_int.to_int i && Big_int.to_int j > 0 -> assert (n = m); let top = Extract (n - 1, Big_int.to_int i + 1, smt_cval ctx vec) in let bot = Extract (Big_int.to_int j - 1, 0, smt_cval ctx vec) in Fn ("concat", [top; Fn ("concat", [smt_cval ctx x; bot])]) - | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 = Big_int.to_int i && Big_int.to_int j >= 0 -> + | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 = Big_int.to_int i && Big_int.to_int j > 0 -> assert (n = m); let bot = Extract (Big_int.to_int j - 1, 0, smt_cval ctx vec) in Fn ("concat", [smt_cval ctx x; bot]) + | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 > Big_int.to_int i && Big_int.to_int j = 0 -> + assert (n = m); + let top = Extract (n - 1, Big_int.to_int i + 1, smt_cval ctx vec) in + Fn ("concat", [top; smt_cval ctx x]) + + | CT_fbits (n, b), ctyp_i, ctyp_j, ctyp_x, CT_fbits (m, _) -> + assert (n = m); + let i' = force_size ctx n (int_size ctx ctyp_i) (smt_cval ctx i) in + let j' = force_size ctx n (int_size ctx ctyp_j) (smt_cval ctx j) in + let x' = smt_conversion ctx ctyp_x (CT_fbits (n, b)) (smt_cval ctx x) in + let len = bvadd (bvadd i' (bvneg j')) (bvint n (Big_int.of_int 1)) in + let mask = bvshl (fbits_mask ctx n len) j' in + bvor (bvand (smt_cval ctx vec) (bvnot mask)) (bvand (bvshl x' j') mask) + | _ -> builtin_type_error ctx "vector_update_subrange" [vec; i; j; x] (Some ret_ctyp) let builtin_unsigned ctx v ret_ctyp = @@ -873,6 +903,10 @@ let builtin_unsigned ctx v ret_ctyp = | CT_lbits _, CT_lint -> Extract (ctx.lint_size - 1, 0, Fn ("contents", [smt_cval ctx v])) + | CT_lbits _, CT_fint m -> + let smt = Fn ("contents", [smt_cval ctx v]) in + force_size ctx m (lbits_size ctx) smt + | ctyp, _ -> builtin_type_error ctx "unsigned" [v] (Some ret_ctyp) let builtin_signed ctx v ret_ctyp = @@ -1021,6 +1055,13 @@ let builtin_get_slice_int ctx v1 v2 v3 ret_ctyp = let contents = unsigned_size ~checked:false ctx (lbits_size ctx) ctx.lint_size (smt_cval ctx v2) in Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; contents])]) + | CT_lint, ctyp2, ctyp3, ret_ctyp -> + let len = Extract (ctx.lbits_index - 1, 0, smt_cval ctx v1) in + let smt2 = force_size ctx (lbits_size ctx) (int_size ctx ctyp2) (smt_cval ctx v2) in + let smt3 = force_size ctx (lbits_size ctx) (int_size ctx ctyp3) (smt_cval ctx v3) in + let result = bvand (bvmask ctx len) (bvlshr smt2 smt3) in + smt_conversion ctx CT_lint ret_ctyp result + | _ -> builtin_type_error ctx "get_slice_int" [v1; v2; v3] (Some ret_ctyp) let builtin_count_leading_zeros ctx v ret_ctyp = |