From b89c481b965c9f24ad1ff12b72db7cc124151fee Mon Sep 17 00:00:00 2001 From: Basile Clement Date: Tue, 11 Jul 2023 12:41:25 +0200 Subject: [PATCH 1/3] Add support for ground bv2nat and int2bv reasoning This patch adds support for "combined" reasoning about the int2bv and bv2nat symbols in the arith and bitv reasoners. More specifically: - The constructors for bv2nat and int2bv in `expr.ml` are now "smart" and know that they are related, so that we effectivly have the following rewrite rules: `(bv2nat ((_ int2bv n) x))` -> `(mod x (pow 2 n))` `((_ int2bv n) (bv2nat (as x (_ BitVec m))))` -> `(ite (> m n) (extract (- n 1) 0 x) (zero_extend (- m n) x))` These are added early in the bv2nat and int2bv constructors to ensure that we *never* actually build `((_ int2bv n) (bv2nat e))` or `(bv2nat ((_ int2bv n) e))` terms. This is actualy useful because the simplifications done for `bv2nat` (see below) are more powerful than what `int2bv` can recover, and there would be information loss otherwise e.g. for `((_ int2bv n) (bv2nat (concat e1 e2)))` which would become `((_ int2bv n) (+ (* (bv2nat e1) (pow 2 m)) (bv2nat e2)))` instead of `(concat e1 e2)` (assuming that `e2` is of type `(_ BitVec m)` and `e1` of type `(_ BitVec |n - m|)`). - The arith and bitv reasoners perform constant propagation of int2bv and bv2nat - The arith reasoner performs the `((_ int2bv n) (bv2nat x))` conversion more aggressivey, i.e. it performs the conversion for terms of the form `((_ int2bv n) e)` where the semantic value of `e` is of the form `(bv2nat e')` More complex transformations, such as transforming `(int2bv (* 2 (bv2nat e)))` into `(concat e #b0)`, are not supported. - The bitv reasoner also performs the `(bv2nat ((_ int2bv n) e))` conversion more aggressively, i.e. for terms that reduce to `((_ int2bv n) e)` after simplification. - The bitv reasoner performs additional simplifications on `bv2nat` terms after normalization. For instance, `(bv2nat (concat x y))` becomes `(+ (* (pow 2 n) (bv2nat x)) (bv2nat y))` when `y` is a bit-vector of size `n`, and `(bv2nat (extract j i x))` becomes `(mod (div (bv2nat x) (pow 2 i)) (pow 2 (+ (- j i) 1)))` - Finally, the bitv reasoner requires that the result of `bv2nat` for a bitvector of size `n` is in the range `0 ..< 2^n` Combined, this allows exploiting the arith reasoner for a variety of problems mostly involving bitvector arithmetic with constants. In particular, we are able to handle many aritmetic expressions involving `bv2nat`. On the other hand, bitvector expressions involving `int2bv` have more limited support. Indeed, not only does `int2bv` perform less simplifications, we are currently not able to exploit the relevant equivalence: `int2bv[n](x) = int2bv[n](y) iff x = y (mod 2^n)` --- src/lib/reasoners/arith.ml | 65 ++++++++++++++++++++++++++--- src/lib/reasoners/bitv.ml | 83 ++++++++++++++++++++++++++++++++++++-- src/lib/structures/expr.ml | 23 +++++++++-- src/lib/util/numbers.mli | 2 +- src/lib/util/util.ml | 6 +++ src/lib/util/util.mli | 2 + 6 files changed, 168 insertions(+), 13 deletions(-) diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index b70a5615d..0c2cd750b 100644 --- a/src/lib/reasoners/arith.ml +++ b/src/lib/reasoners/arith.ml @@ -31,6 +31,7 @@ module Sy = Symbols module E = Expr +module ZA = Z module Z = Numbers.Z module Q = Numbers.Q @@ -119,7 +120,7 @@ module Shostak | Sqrt_real_default | Sqrt_real_excess | Real_of_int | Int_floor | Int_ceil | Max_int | Max_real | Min_int | Min_real - | Pow | Integer_log2 + | Pow | Integer_log2 | Int2BV _ | Integer_round) -> true | _ -> false @@ -365,10 +366,64 @@ module Shostak | _ -> P.add p (P.create [coef, a] Q.zero ty), ctx let make t = - Options.tool_req 4 "TR-Arith-Make"; - let ty = E.type_info t in - let p, ctx = mke Q.one (empty_polynome ty) t [] in - is_mine p, ctx + let { E.f; xs; _ } = E.term_view t in + match f, xs with + | Op Int2BV n, [x] -> + (* When we have an Int2BV expression, we try our best to convert it to + something that is usable by the bitv theory. + + More precisely: + + - If we have (int2bv c) where [c] is a constant, we convert the + constant to a bitvector constant of the appropriate size and + create the corresponding [Bitv] term. The call to [X.make] will be + dispatched to the bitvector theory. + + - If we have (int2bv [1 * (bv2nat e) + 0]) -- that is, int2bv of a + single alien that is equal to a [bv2nat] expression -- we convert + [e] to the appropriate bitvector size using [extract] or + [zero_extend]. This is done by a roundtrip through E.BV.int2bv. + + - There are some other expressions where we could convert, for + instance, disjoint sums of bv2nat terms multiplied by powers of + two, but we only handle the simple cases for now. + + - In all other cases, Int2BV becomes uninterpreted. *) + let p, ctx = mke Q.one (empty_polynome Tint) x [] in + begin match P.to_list p with + | [], c -> + let c = Q.to_z c in + let c = ZA.(erem c @@ pow ~$2 n) in + let biv = + String.init n (fun i -> + let i = n - i - 1 in + if ZA.(extract c i 1 |> to_int) = 0 then '0' else '1') + in + let r, ctx' = E.mk_term (Bitv biv) [] (Tbitv n) |> X.make in + r, List.rev_append ctx' ctx + | [ coef, x ], const when Q.is_zero const && Q.is_one coef -> + begin match X.term_extract x with + | Some tx, _ -> + begin match (E.term_view tx).f with + | Op BV2Nat -> + (* int2bv will simplify BV2Nat: we must [X.make] again *) + let r, ctx' = E.BV.int2bv n tx |> X.make in + r, List.rev_append ctx' ctx + | _ -> + (* Otherwise we must become uninterpreted *) + E.BV.int2bv n tx |> X.term_embed, ctx + end + | None, _ -> + X.term_embed t, [] + end + | _ -> + X.term_embed t, [] + end + | _ -> + Options.tool_req 4 "TR-Arith-Make"; + let ty = E.type_info t in + let p, ctx = mke Q.one (empty_polynome ty) t [] in + is_mine p, ctx let rec expand p n acc = assert (n >=0); diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index 097f00781..c08193015 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -139,7 +139,7 @@ module Shostak(X : ALIEN) = struct let is_mine_symb sy _ = match sy with - | Sy.Bitv _ | Sy.Op (Sy.Concat | Sy.Extract _) -> true + | Sy.Bitv _ | Sy.Op (Concat | Extract _ | BV2Nat) -> true | _ -> false let embed r = @@ -1123,13 +1123,88 @@ module Shostak(X : ALIEN) = struct | Other t | Ext(t,_,_,_) -> (X.leaves t)@acc ) [] bitv - let is_mine = function [{ bv = Other r; _ }] -> r | bv -> X.embed bv + let is_mine_opt = function [{ bv = Other r; _ }] -> Some r | _ -> None + + let is_mine bv = + match is_mine_opt bv with + | Some r -> r + | None -> X.embed bv let print = Debug.print_C_ast + (* This is used to extract terms from non-bitv semantic values. + + We assume that non-bitv semantic values of a bitvector type are + necessarily uninterpreted terms, because that should be the case at the + time this code is written. + + If this ever ceases to be the case, we should either preserve the original + term along with the semantic value, or fail more gracefully here. *) + let term_extract r = + match X.term_extract r with + | Some t, _ -> t + | None, _ -> + Util.internal_error "Non-BV semantic value: %a" X.print r + + (* This is a helper function that converts a [simple_term] to an integer + expression. *) + let simple_term_to_nat acc st = + match st.bv with + | Cte false -> E.Ints.(acc * ~$Z.(pow ~$2 st.sz)) + | Cte true -> E.Ints.((acc + ~$$1) * ~$Z.(pow ~$2 st.sz) - ~$$1) + | Other r -> + let t = term_extract r in + E.Ints.(acc * ~$Z.(pow ~$2 st.sz) + E.BV.bv2nat t) + | Ext (o, _, i, j) -> + assert (st.sz = j - i + 1); + let t = term_extract o in + E.Ints.( + acc * ~$Z.(pow ~$2 st.sz) + + (E.BV.bv2nat t / ~$Z.(pow ~$2 i)) mod ~$Z.(pow ~$2 st.sz)) + + let abstract_to_nat r = + List.fold_left simple_term_to_nat (E.Ints.of_int 0) r + + (* Ideally, we would want to just call [abstract_to_nat r |> X.make]. But if + we do so, we may end up in a loop where we repeatedly call [X.make] on a + [BV2Nat] term -- so instead if we are a single [Other] term, we become + uninterpreted. *) + let bv2nat bv = + match is_mine_opt bv with + | Some r -> + let t = term_extract r in + begin match E.term_view t with + | { f = Op Int2BV _; _ } -> + (* bv2nat will simplify: we must call [X.make] again *) + E.BV.bv2nat t |> X.make + | { ty = Tbitv n; _ } -> + (* bv2nat will *not* simplify: become uninterpreted with interval + information *) + let t = E.BV.bv2nat t in + X.term_embed t, [ E.Ints.(~$$0 <= t) ; E.Ints.(t < ~$Z.(pow ~$2 n)) ] + | { ty; _ } -> + Util.internal_error "expected bitv, got %a" Ty.print ty + end + | None -> abstract_to_nat bv |> X.make + let make t = - let r, ctx = Canon.make t in - is_mine r, ctx + let { E.f; xs; _ } = E.term_view t in + match f, xs with + | Op BV2Nat, [x] -> + (* When we have a BV2Nat expression, we try our best to convert it to + something that is usable by the arithmetic theory. + + More precisely, after simplification of the argument, we get a + composition of constants and aliens or alien extractions, to which we + apply [bv2nat] recursively. If the alien or alien extraction are + [int2bv] terms, we convert the composition [(bv2nat ((_ int2bv n) x))] + into [(mod x (pow 2 n))]. *) + let r, ctx = Canon.make x in + let r, ctx' = bv2nat r in + r, List.rev_append ctx' ctx + | _ -> + let r, ctx = Canon.make t in + is_mine r, ctx let color _ = assert false diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 7060ec1fd..2305bbbdf 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -2912,9 +2912,6 @@ module BV = struct assert (size t = m); m - let int2bv n t = mk_term (Op (Int2BV n)) [t] (Tbitv n) - let bv2nat t = mk_term (Op BV2Nat) [t] Tint - (* Function symbols for concatenation *) let concat s t = let n = size s and m = size t in @@ -2956,6 +2953,26 @@ module BV = struct else concat (extract (i - 1) 0 t) (extract (m - 1) i t) + (* int2bv and bv2nat *) + let int2bv n t = + (* Note: arith.ml calls [int2bv] in [make]. If additional simplifications + are added here, arith.ml must be updated as well. *) + match term_view t with + | { f = Op BV2Nat; xs = [ t ]; ty = Tbitv m; _ } -> + if m > n then + extract (n - 1) 0 t + else + zero_extend (n - m) t + | _ -> mk_term (Op (Int2BV n)) [t] (Tbitv n) + + let bv2nat t = + (* Note: bitv.ml calls [bv2nat] in [make]. If additional simplifications + are added here, bitv.ml must be updated as well. *) + match term_view t with + | { f = Op Int2BV n; xs = [ t ]; _ } -> + Ints.(t mod ~$Z.(pow ~$2 n)) + | _ -> mk_term (Op BV2Nat) [t] Tint + (* Bit-wise operations *) let bvnot s = mk_term (Op BVnot) [s] (type_info s) let bvand s t = mk_term (Op BVand) [s; t] (type_info s) diff --git a/src/lib/util/numbers.mli b/src/lib/util/numbers.mli index c5379bbad..dccfa208d 100644 --- a/src/lib/util/numbers.mli +++ b/src/lib/util/numbers.mli @@ -30,7 +30,7 @@ (** Integers implementation. **) module Z : sig - type t + type t = Z.t val zero : t val one : t val m_one : t (* minus one *) diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index f4975df99..3817c5720 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -34,12 +34,15 @@ exception Unsolvable exception Cmp of int exception Not_implemented of string +exception Internal_error of string let () = Printexc.register_printer (function | Not_implemented s -> Some (Format.sprintf "Feature not implemented (%s)" s) + | Internal_error s -> + Some (Format.sprintf "Internal error: %s" s) | _ -> None ) @@ -183,3 +186,6 @@ let rec print_list_pp ~sep ~pp fmt = function print_list_pp ~sep ~pp fmt l let failwith msg = Format.kasprintf failwith msg + +let internal_error msg = + Format.kasprintf (fun s -> raise (Internal_error s)) msg diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 93c7b7e30..31636e8ee 100644 --- a/src/lib/util/util.mli +++ b/src/lib/util/util.mli @@ -119,3 +119,5 @@ val print_list_pp: Format.formatter -> 'a list -> unit val failwith: ('a, Format.formatter, unit, 'b) format4 -> 'a + +val internal_error : ('a, Format.formatter, unit, 'b) format4 -> 'a From df14d0ff908487280aa43bec1cf00cfcf01472c1 Mon Sep 17 00:00:00 2001 From: Basile Clement Date: Wed, 12 Jul 2023 22:57:34 +0200 Subject: [PATCH 2/3] Use `Z.(~$1 lsl n)` rather than `Z.(pow ~$2 n)` --- src/lib/reasoners/arith.ml | 2 +- src/lib/reasoners/bitv.ml | 12 ++++++------ src/lib/structures/expr.ml | 4 ++-- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index 0c2cd750b..92b7a4398 100644 --- a/src/lib/reasoners/arith.ml +++ b/src/lib/reasoners/arith.ml @@ -393,7 +393,7 @@ module Shostak begin match P.to_list p with | [], c -> let c = Q.to_z c in - let c = ZA.(erem c @@ pow ~$2 n) in + let c = ZA.(erem c @@ ~$1 lsl n) in let biv = String.init n (fun i -> let i = n - i - 1 in diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index c08193015..a21ff2831 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -1150,17 +1150,17 @@ module Shostak(X : ALIEN) = struct expression. *) let simple_term_to_nat acc st = match st.bv with - | Cte false -> E.Ints.(acc * ~$Z.(pow ~$2 st.sz)) - | Cte true -> E.Ints.((acc + ~$$1) * ~$Z.(pow ~$2 st.sz) - ~$$1) + | Cte false -> E.Ints.(acc * ~$Z.(~$1 lsl st.sz)) + | Cte true -> E.Ints.((acc + ~$$1) * ~$Z.(~$1 lsl st.sz) - ~$$1) | Other r -> let t = term_extract r in - E.Ints.(acc * ~$Z.(pow ~$2 st.sz) + E.BV.bv2nat t) + E.Ints.(acc * ~$Z.(~$1 lsl st.sz) + E.BV.bv2nat t) | Ext (o, _, i, j) -> assert (st.sz = j - i + 1); let t = term_extract o in E.Ints.( - acc * ~$Z.(pow ~$2 st.sz) + - (E.BV.bv2nat t / ~$Z.(pow ~$2 i)) mod ~$Z.(pow ~$2 st.sz)) + acc * ~$Z.(~$1 lsl st.sz) + + (E.BV.bv2nat t / ~$Z.(~$1 lsl i)) mod ~$Z.(~$1 lsl st.sz)) let abstract_to_nat r = List.fold_left simple_term_to_nat (E.Ints.of_int 0) r @@ -1181,7 +1181,7 @@ module Shostak(X : ALIEN) = struct (* bv2nat will *not* simplify: become uninterpreted with interval information *) let t = E.BV.bv2nat t in - X.term_embed t, [ E.Ints.(~$$0 <= t) ; E.Ints.(t < ~$Z.(pow ~$2 n)) ] + X.term_embed t, [ E.Ints.(~$$0 <= t) ; E.Ints.(t < ~$Z.(~$1 lsl n)) ] | { ty; _ } -> Util.internal_error "expected bitv, got %a" Ty.print ty end diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 2305bbbdf..e2531b6f0 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -2970,7 +2970,7 @@ module BV = struct are added here, bitv.ml must be updated as well. *) match term_view t with | { f = Op Int2BV n; xs = [ t ]; _ } -> - Ints.(t mod ~$Z.(pow ~$2 n)) + Ints.(t mod ~$Z.(~$1 lsl n)) | _ -> mk_term (Op BV2Nat) [t] Tint (* Bit-wise operations *) @@ -2996,7 +2996,7 @@ module BV = struct (* Arithmetic operations *) let bvneg s = let m = size s in - int2bv m Ints.(~$Z.(pow ~$2 m) - bv2nat s) + int2bv m Ints.(~$Z.(~$1 lsl m) - bv2nat s) let bvadd s t = int2bv (size s) Ints.(bv2nat s + bv2nat t) let bvsub s t = bvadd s (bvneg t) let bvmul s t = int2bv (size s) Ints.(bv2nat s * bv2nat t) From be3da73d205d025ebec9da9d5c9105a9eef3dd57 Mon Sep 17 00:00:00 2001 From: Basile Clement Date: Wed, 12 Jul 2023 22:57:45 +0200 Subject: [PATCH 3/3] Fix infinite loop: bv2nat has type int --- src/lib/structures/expr.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index e2531b6f0..d8d076213 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -2958,7 +2958,8 @@ module BV = struct (* Note: arith.ml calls [int2bv] in [make]. If additional simplifications are added here, arith.ml must be updated as well. *) match term_view t with - | { f = Op BV2Nat; xs = [ t ]; ty = Tbitv m; _ } -> + | { f = Op BV2Nat; xs = [ t ]; _ } -> + let m = match type_info t with Tbitv m -> m | _ -> assert false in if m > n then extract (n - 1) 0 t else