From 99f867eee3f3176a5ae9dc9bac2869d98f524e1b 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 1/4] [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 9732eb51e..4e099cce4 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 141559cca..d43bef972 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 1413e9191..8cd156411 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 000000000..6f99ff0f4 --- /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 000000000..ed791412c --- /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 000000000..99bcb1175 --- /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 000000000..0233d238a --- /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 000000000..720c05e74 --- /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 000000000..ade3d104f --- /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) From 6409856a7b2dc545ffc17802615d7a503fae8903 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <129742207+bclement-ocp@users.noreply.github.com> Date: Fri, 29 Sep 2023 10:25:32 +0200 Subject: [PATCH 2/4] Better comment wording Co-authored-by: Pierrot --- src/lib/reasoners/bitv.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index 4e099cce4..a646335e3 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -1333,7 +1333,7 @@ module Shostak(X : ALIEN) = struct | { 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 + (* Fills the segment of [buf] from [pos] to [sz] with a bitvector that is different from all those in [abstracts]. Uninterpreted ("Other" and "Ext") components in [abstracts] are ignored. @@ -1353,7 +1353,7 @@ module Shostak(X : ALIEN) = struct | _, [] -> Bytes.fill buf pos sz '0' | [], _ -> Bytes.fill buf pos sz '1' | _, _ -> - (* Prefer searching where there are less candidates. *) + (* Prefer searching where there are more candidates, i.e. less constraints. *) let x, cx, y, cy = if nt < nf then t, '1', f, '0' else f, '0', t, '1' in From f1381aaf96ae31d86a8455431f30ef5b4325fd48 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Fri, 29 Sep 2023 10:29:28 +0200 Subject: [PATCH 3/4] Use is_cte_abstract for constant checks --- src/lib/reasoners/bitv.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index a646335e3..8094effdb 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -1371,9 +1371,10 @@ module Shostak(X : ALIEN) = struct 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 + (fun (_, x) -> + match X.extract x with + | Some b -> is_cte_abstract b + | None -> false) eq then None else let sz = List.fold_left (fun tot { sz; _ } -> tot + sz) 0 biv in (* Only try to be distinct from constants. *) From d5eddc0b2ea1a470f4fab8f7414596c269d12843 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Fri, 29 Sep 2023 10:31:35 +0200 Subject: [PATCH 4/4] Fix style --- src/lib/reasoners/bitv.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index 8094effdb..f3c5bd40a 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -1353,7 +1353,8 @@ module Shostak(X : ALIEN) = struct | _, [] -> Bytes.fill buf pos sz '0' | [], _ -> Bytes.fill buf pos sz '1' | _, _ -> - (* Prefer searching where there are more candidates, i.e. less constraints. *) + (* Prefer searching where there are more candidates, i.e. less + constraints. *) let x, cx, y, cy = if nt < nf then t, '1', f, '0' else f, '0', t, '1' in