From 27e50559f2c05216e1e218a89819a58c718c3ad1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Tue, 27 Jun 2023 09:58:07 +0200 Subject: [PATCH] [bitv] Add support for model generation This patch adds support for model generation in the bitvector theory. To generate a value for a model, a simple brute-force backtracking search amongst all possible bitvector values is performed to find one that is different from the values that were asserted distinct. If none can be found (or if exactly one is found, in which case the value is forced) the `case_split` flag is set so that we report `unsat` instead of looping during model generation. In the future, this should be augmented with proper support for case splits / bit-blasting in the relational theory. Note that even if we add support for case splits in the relational theory, having an enumeration in model generation is useful, because we may not always want to perform case splits on large bitvector types. --- src/lib/reasoners/bitv.ml | 117 ++++++++++++++++++-- src/lib/structures/ty.ml | 4 +- tests/dune.inc | 71 ++++++++++++ tests/models/bitv/cardinal.models.expected | 2 + tests/models/bitv/cardinal.models.smt2 | 9 ++ tests/models/bitv/extract.models.expected | 8 ++ tests/models/bitv/extract.models.smt2 | 18 +++ tests/models/bitv/specified.models.expected | 5 + tests/models/bitv/specified.models.smt2 | 10 ++ 9 files changed, 234 insertions(+), 10 deletions(-) create mode 100644 tests/models/bitv/cardinal.models.expected create mode 100644 tests/models/bitv/cardinal.models.smt2 create mode 100644 tests/models/bitv/extract.models.expected create mode 100644 tests/models/bitv/extract.models.smt2 create mode 100644 tests/models/bitv/specified.models.expected create mode 100644 tests/models/bitv/specified.models.smt2 diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index 9732eb51ef..8fca5c6f8f 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -1325,14 +1325,113 @@ module Shostak(X : ALIEN) = struct let solve r1 r2 pb = Sig.{pb with sbt = List.rev_append (solve_bis r1 r2) pb.sbt} - let assign_value _ _ _ = - Printer.print_err - "[Bitv.models] assign_value currently not implemented"; - raise (Util.Not_implemented "Models for bit-vectors") - - let choose_adequate_model _ _ = - Printer.print_err - "[Bitv.models] choose_adequate_model currently not implemented"; - raise (Util.Not_implemented "Models for bit-vectors") + (* Pop the first bit, raises [Not_found] if there is no first bit *) + let pop_bit = function + | [] -> raise Not_found + | { bv = Cte b; sz } as st :: rst -> + Some b, if sz > 1 then { st with sz = sz - 1 } :: rst else rst + | { bv = Other _ | Ext _ ; sz } as st :: rst -> + None, if sz > 1 then { st with sz = sz - 1 } :: rst else rst + + (* Fills an initial segment of [buf] from [0] to [sz] with a bitvector that is + different from all those in [abstracts]. + + Uninterpreted ("Other" and "Ext") components in [abstracts] are ignored. + + Currently a fairly naive backtracking search. *) + let rec search buf pos sz abstracts = + (* [t] are the values we must be distinct from that starts with a '1' *) + (* [f] are the values we must be distinct from that starts with a '0' *) + let t, nt, f, nf = List.fold_left (fun (t, nt, f, nf) ab -> + let b, bv = pop_bit ab in + match b with + | Some true -> (bv :: t, 1 + nt, f, nf) + | Some false -> (t, nt, bv :: f, 1 + nf) + | None -> (t, nt, f, nf)) ([], 0, [], 0) abstracts + in + match t, f with + | _, [] -> Bytes.fill buf pos sz '0' + | [], _ -> Bytes.fill buf pos sz '1' + | _, _ -> + (* Prefer searching where there are less candidates. *) + let x, cx, y, cy = + if nt < nf then t, '1', f, '0' else f, '0', t, '1' + in + match search buf (pos + 1) (sz - 1) x with + | () -> Bytes.set buf pos cx + | exception Not_found -> + search buf (pos + 1) (sz - 1) y; + Bytes.set buf pos cy + + let is_cte = function | { bv = Cte _; _ } -> true | _ -> false + let is_cte_abstract = List.for_all is_cte + + let assign_value r distincts eq = + (* If we are trying to assign a value to a constant, or a term that has a + constant in its equivalence class, bail out *) + let biv = embed r in + if is_cte_abstract biv || List.exists + (fun (t, x) -> + let { E.f; ty; _ } = E.term_view t in + is_mine_symb f ty && X.leaves x == [] ) eq + then None else + let sz = List.fold_left (fun tot { sz; _ } -> tot + sz) 0 biv in + (* Only try to be distinct from constants. *) + let distincts = + List.fold_left (fun acc x -> + let biv = embed x in + if is_cte_abstract biv then biv :: acc else acc) [] distincts + in + let buf = Bytes.create sz in + match search buf 0 sz distincts with + | () -> + (* If there are exactly [2^n - 1] constant values we must be distinct + from, this is not a case split: the choice is forced. *) + let nb = + List.fold_left (fun nb a -> + if is_cte_abstract a then nb + 1 else nb) 1 distincts + in + let is_cs = not (Z.equal (Z.of_int nb) (Z.pow (Z.of_int 2) sz)) in + let bv = Bytes.unsafe_to_string buf in + Some (E.bitv bv (Ty.Tbitv sz), is_cs) + | exception Not_found -> + (* This is not solvable: we are forced to be distinct from all possible + values. We signal that by returning an arbitrary bitvector and setting + the "case-split" flag to [false], which means that the choice was + "forced". + + Since a forced choice is actually inconsistent, this will cause + backtracking (and possibly unsat-ness). *) + let bv = String.make sz '0' in + Some (E.bitv bv (Ty.Tbitv sz), false) + + let choose_adequate_model t r l = + if Options.get_debug_interpretation () then + Printer.print_dbg + ~module_name:"Bitv" ~function_name:"choose_adequate_model" + "choose_adequate_model for %a" E.print t; + let l = List.map (fun (t, r) -> (t, r, embed r)) l in + let l = List.filter (fun (_, _, a) -> is_cte_abstract a) l in + let r, a = + match l with + | [] -> + let a = embed r in + assert (is_cte_abstract a); + r, a + | (_, r, a) :: l -> + List.iter (fun (_, x, _) -> assert (X.equal x r)) l; + r, a + in + let s = + List.map (function + | { bv = Cte b; sz } -> String.make sz (if b then '1' else '0') + | _ -> + (* Cannot happen because [a] must satisfy [is_cte_abstract] at this + point. *) + assert false + ) a + |> String.concat "" + in + r, "#b" ^ s end diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index 141559cca1..d43bef9729 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -107,7 +107,9 @@ let print_generic body_of = | Treal -> fprintf fmt "real" | Tbool -> fprintf fmt "bool" | Tunit -> fprintf fmt "unit" - | Tbitv n -> fprintf fmt "bitv[%d]" n + | Tbitv n -> + if Options.get_output_smtlib () then fprintf fmt "(_ BitVec %d)" n + else fprintf fmt "bitv[%d]" n | Tvar{v=v ; value = None} -> fprintf fmt "'a_%d" v | Tvar{v=v ; value = Some (Trecord { args = l; name = n; _ } as t) } -> if Hashtbl.mem h v then diff --git a/tests/dune.inc b/tests/dune.inc index 1413e91916..8cd1564112 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -192313,6 +192313,77 @@ ; Auto-generated part end ; File auto-generated by gentests +; Auto-generated part begin +(subdir models/bitv + (rule + (target specified.models_tableaux.output) + (deps (:input specified.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) + (rule + (deps specified.models_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff specified.models.expected specified.models_tableaux.output))) + (rule + (target extract.models_tableaux.output) + (deps (:input extract.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) + (rule + (deps extract.models_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff extract.models.expected extract.models_tableaux.output))) + (rule + (target cardinal.models_tableaux.output) + (deps (:input cardinal.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) + (rule + (deps cardinal.models_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff cardinal.models.expected cardinal.models_tableaux.output)))) +; Auto-generated part end +; File auto-generated by gentests + ; Auto-generated part begin (subdir models/bool (rule diff --git a/tests/models/bitv/cardinal.models.expected b/tests/models/bitv/cardinal.models.expected new file mode 100644 index 0000000000..6f99ff0f44 --- /dev/null +++ b/tests/models/bitv/cardinal.models.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/models/bitv/cardinal.models.smt2 b/tests/models/bitv/cardinal.models.smt2 new file mode 100644 index 0000000000..ed791412cf --- /dev/null +++ b/tests/models/bitv/cardinal.models.smt2 @@ -0,0 +1,9 @@ +(set-logic BV) +(set-option :produce-models true) + +; Without :produce-models we say 'unknown', not 'unsat' +(declare-const a (_ BitVec 1)) +(declare-const b (_ BitVec 1)) +(declare-const c (_ BitVec 1)) +(assert (distinct a b c)) +(check-sat) diff --git a/tests/models/bitv/extract.models.expected b/tests/models/bitv/extract.models.expected new file mode 100644 index 0000000000..99bcb11755 --- /dev/null +++ b/tests/models/bitv/extract.models.expected @@ -0,0 +1,8 @@ + +unknown +( + (define-fun z () (_ BitVec 1) #b0) + (define-fun a () (_ BitVec 2) #b11) + (define-fun b () (_ BitVec 3) #b111) + (define-fun c () (_ BitVec 6) #b111011) +) diff --git a/tests/models/bitv/extract.models.smt2 b/tests/models/bitv/extract.models.smt2 new file mode 100644 index 0000000000..0233d238a7 --- /dev/null +++ b/tests/models/bitv/extract.models.smt2 @@ -0,0 +1,18 @@ +(set-logic BV) +(set-option :produce-models true) + +(declare-const a (_ BitVec 2)) +(declare-const b (_ BitVec 3)) +(declare-const c (_ BitVec 6)) +(declare-const z (_ BitVec 1)) + +(assert (= ((_ extract 0 0) c) #b1)) +(assert (= ((_ extract 5 5) c) #b1)) +(assert (= (concat (concat b z) a) c)) + +(assert (= ((_ extract 1 1) a) #b1)) +(assert (= ((_ extract 1 0) b) #b11)) +(assert (= z #b0)) + +(check-sat) +(get-model) diff --git a/tests/models/bitv/specified.models.expected b/tests/models/bitv/specified.models.expected new file mode 100644 index 0000000000..720c05e743 --- /dev/null +++ b/tests/models/bitv/specified.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun x () (_ BitVec 4) #b0101) +) diff --git a/tests/models/bitv/specified.models.smt2 b/tests/models/bitv/specified.models.smt2 new file mode 100644 index 0000000000..ade3d104f8 --- /dev/null +++ b/tests/models/bitv/specified.models.smt2 @@ -0,0 +1,10 @@ +(set-logic BV) +(set-option :produce-models true) + +(declare-const x (_ BitVec 4)) +(assert (= ((_ extract 0 0) x) #b1)) +(assert (= ((_ extract 1 1) x) #b0)) +(assert (= ((_ extract 2 2) x) #b1)) +(assert (= ((_ extract 3 3) x) #b0)) +(check-sat) +(get-model)