From 27ff2640aff7eb7dd53fee643067e7aa5e47dffd Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 21 Jul 2023 00:14:53 +0200 Subject: [PATCH 1/6] Support bnot in the solver of bitv.ml --- dune-project | 1 + src/lib/dune | 3 +-- src/lib/reasoners/bitv.ml | 57 ++++++++++++++++++++++----------------- 3 files changed, 35 insertions(+), 26 deletions(-) diff --git a/dune-project b/dune-project index 251d40b4e..48602d535 100644 --- a/dune-project +++ b/dune-project @@ -86,6 +86,7 @@ See more details on http://alt-ergo.ocamlpro.com/" fmt stdlib-shims ppx_blob + ppx_deriving (camlzip (>= 1.07)) (odoc :with-doc) ) diff --git a/src/lib/dune b/src/lib/dune index 8265aabac..e57160e99 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -25,8 +25,7 @@ alt_ergo_prelude fmt ) - - (preprocess (pps ppx_blob)) + (preprocess (pps ppx_blob ppx_deriving.show)) (preprocessor_deps (glob_files ../preludes/*.ae)) ; .mli only modules *also* need to be in this field diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index a21ff2831..71884f725 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -100,7 +100,7 @@ type 'a simple_term = ('a simple_term_aux) alpha_term let equal_simple_term eq = equal_alpha_term (equal_simple_term_aux eq) -type 'a abstract = ('a simple_term) list +type 'a abstract = 'a simple_term list let equal_abstract eq = Lists.equal (equal_simple_term eq) @@ -139,7 +139,7 @@ module Shostak(X : ALIEN) = struct let is_mine_symb sy _ = match sy with - | Sy.Bitv _ | Sy.Op (Concat | Extract _ | BV2Nat) -> true + | Sy.Bitv _ | Sy.Op (Concat | Extract _ | BV2Nat | BVnot) -> true | _ -> false let embed r = @@ -198,8 +198,10 @@ module Shostak(X : ALIEN) = struct | Vother of 'a | Vextract of 'a * int * int | Vconcat of 'a * 'a + | Vnot of 'a + [@@deriving show] - and 'a view = { descr : 'a view_descr ; size : int } + type 'a view = { descr : 'a view_descr ; size : int } let view t = match E.term_view t with @@ -209,6 +211,8 @@ module Shostak(X : ALIEN) = struct | { f = Op Extract (i, j); xs = [ t' ]; ty = Tbitv size; _ } -> assert (size = j - i + 1); { descr = Vextract (t', i, j); size } + | { f = Op BVnot; xs = [ t ]; ty = Tbitv size; _ } -> + { descr = Vnot t; size } | { ty = Tbitv size; _ } -> { descr = Vother t; size } | _ -> assert false @@ -227,7 +231,7 @@ module Shostak(X : ALIEN) = struct f x, ctx let (and+) = (and*) - let other t sz ctx = + let other neg_mode t sz ctx = let r, ctx' = X.make t in let ctx = List.rev_append ctx' ctx in match X.extract r with @@ -282,53 +286,58 @@ module Shostak(X : ALIEN) = struct | _ -> normalize_st s :: normalize tts end - let rec make t = vmake (view t) - and vextract i j tv = + let rec make neg_mode t = vmake neg_mode (view t) + and vextract neg_mode i j tv = let size = j - i + 1 in match tv.descr with | Vcte z -> - vmake { descr = Vcte (String.sub z (tv.size - j - 1) size); size } + vmake neg_mode { descr = Vcte (String.sub z (tv.size - j - 1) size); size } | Vother t -> - let+ o = other t tv.size in + let+ o = other neg_mode t tv.size in extract tv.size i j o | Vextract (t'', k, _) -> - vmake { descr = Vextract (t'', i + k, j + k); size } + vmake neg_mode { descr = Vextract (t'', i + k, j + k); size } | Vconcat (u, v) -> let vu = view u and vv = view v in if j < vv.size then - vextract i j vv + vextract neg_mode i j vv else if i >= vv.size then - vextract (i - vv.size) (j - vv.size) vu + vextract neg_mode (i - vv.size) (j - vv.size) vu else - let+ u = vextract 0 (j - vv.size) vu - and+ v = vextract i (vv.size - 1) vv + let+ u = vextract neg_mode 0 (j - vv.size) vu + and+ v = vextract neg_mode i (vv.size - 1) vv in u @ v - and vmake tv ctx = + | Vnot t -> + vextract (not neg_mode) i j (view t) + and vmake neg_mode tv ctx = match tv.descr with | Vcte z -> let acc = ref [] in for i = String.length z - 1 downto 0 do let c = z.[i] in match c, !acc with - | '0', { bv = Cte false; sz } :: rst -> - acc := { bv = Cte false; sz = sz + 1 } :: rst + | '0', { bv = Cte b; sz } :: rst when Bool.equal b neg_mode -> + acc := { bv = Cte b; sz = sz + 1 } :: rst | '0', rst -> - acc := { bv = Cte false; sz = 1 } :: rst - | _, { bv = Cte true; sz } :: rst -> - acc := { bv = Cte true; sz = sz + 1 } :: rst + acc := { bv = Cte neg_mode; sz = 1 } :: rst + | _, { bv = Cte b; sz } :: rst when Bool.equal b (not neg_mode) -> + acc := { bv = Cte b; sz = sz + 1 } :: rst | _, rst -> - acc := { bv = Cte true; sz = 1 } :: rst + acc := { bv = Cte (not neg_mode); sz = 1 } :: rst done; !acc, ctx - | Vother t -> other t tv.size ctx + | Vother t -> other neg_mode t tv.size ctx | Vextract (t', i, j) -> - run ctx @@ vextract i j (view t') + run ctx @@ vextract neg_mode i j (view t') | Vconcat (t1, t2) -> run ctx @@ - let+ t1 = make t1 and+ t2 = make t2 in t1 @ t2 + let+ t1 = make neg_mode t1 and+ t2 = make neg_mode t2 in + t1 @ t2 + | Vnot t -> + run ctx @@ make (not neg_mode) t let make t = - let r, ctx = make t [] in + let r, ctx = make false t [] in normalize r, ctx end From 4b551ed8cbcf9664003ee358124aa68c41630660 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 21 Jul 2023 16:27:35 +0200 Subject: [PATCH 2/6] Support partially the semantic of bvnot on uninterpreted semantic values of Bitv --- src/lib/reasoners/bitv.ml | 67 ++++++++++++++++++++++++++++----------- 1 file changed, 48 insertions(+), 19 deletions(-) diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index 71884f725..8ad453e12 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -199,7 +199,7 @@ module Shostak(X : ALIEN) = struct | Vextract of 'a * int * int | Vconcat of 'a * 'a | Vnot of 'a - [@@deriving show] + (* [@@deriving show] *) type 'a view = { descr : 'a view_descr ; size : int } @@ -231,11 +231,40 @@ module Shostak(X : ALIEN) = struct f x, ctx let (and+) = (and*) - let other neg_mode t sz ctx = + let negate_abstract r = + List.map (fun { bv = st; sz } -> + let st = + match st with + | Cte b -> Cte (not b) + | _ -> assert false + in + { bv = st; sz } + ) r + + let no_variable r = + List.for_all (fun { bv = st; _ } -> + match st with + | Cte _ -> true + | Other _ | Ext _ -> + (* After normalization, the semantic value in + the constructor Other and Ext cannot be a bitvector. + Thus, these values are always uninterpreted for the + Bitv theory. *) + false + ) r + + let other ~neg_mode t sz ctx = let r, ctx' = X.make t in let ctx = List.rev_append ctx' ctx in match X.extract r with - | Some bv -> bv, ctx + | Some bv -> + if neg_mode then + if no_variable bv then + negate_abstract bv, ctx + else + [ { bv = Other (X.term_embed (E.BV.bvnot t)); sz } ], ctx + else + bv, ctx | None -> [ { bv = Other r; sz } ], ctx let extract_st i j ({ bv; sz } as st) = @@ -286,30 +315,30 @@ module Shostak(X : ALIEN) = struct | _ -> normalize_st s :: normalize tts end - let rec make neg_mode t = vmake neg_mode (view t) - and vextract neg_mode i j tv = + let rec make ~neg_mode t = vmake ~neg_mode (view t) + and vextract ~neg_mode i j tv = let size = j - i + 1 in match tv.descr with | Vcte z -> - vmake neg_mode { descr = Vcte (String.sub z (tv.size - j - 1) size); size } + vmake ~neg_mode { descr = Vcte (String.sub z (tv.size - j - 1) size); size } | Vother t -> - let+ o = other neg_mode t tv.size in + let+ o = other ~neg_mode t tv.size in extract tv.size i j o | Vextract (t'', k, _) -> - vmake neg_mode { descr = Vextract (t'', i + k, j + k); size } + vmake ~neg_mode { descr = Vextract (t'', i + k, j + k); size } | Vconcat (u, v) -> let vu = view u and vv = view v in if j < vv.size then - vextract neg_mode i j vv + vextract ~neg_mode i j vv else if i >= vv.size then - vextract neg_mode (i - vv.size) (j - vv.size) vu + vextract ~neg_mode (i - vv.size) (j - vv.size) vu else - let+ u = vextract neg_mode 0 (j - vv.size) vu - and+ v = vextract neg_mode i (vv.size - 1) vv + let+ u = vextract ~neg_mode 0 (j - vv.size) vu + and+ v = vextract ~neg_mode i (vv.size - 1) vv in u @ v | Vnot t -> - vextract (not neg_mode) i j (view t) - and vmake neg_mode tv ctx = + vextract ~neg_mode:(not neg_mode) i j (view t) + and vmake ~neg_mode tv ctx = match tv.descr with | Vcte z -> let acc = ref [] in @@ -326,18 +355,18 @@ module Shostak(X : ALIEN) = struct acc := { bv = Cte (not neg_mode); sz = 1 } :: rst done; !acc, ctx - | Vother t -> other neg_mode t tv.size ctx + | Vother t -> other ~neg_mode t tv.size ctx | Vextract (t', i, j) -> - run ctx @@ vextract neg_mode i j (view t') + run ctx @@ vextract ~neg_mode i j (view t') | Vconcat (t1, t2) -> run ctx @@ - let+ t1 = make neg_mode t1 and+ t2 = make neg_mode t2 in + let+ t1 = make ~neg_mode t1 and+ t2 = make ~neg_mode t2 in t1 @ t2 | Vnot t -> - run ctx @@ make (not neg_mode) t + run ctx @@ make ~neg_mode:(not neg_mode) t let make t = - let r, ctx = make false t [] in + let r, ctx = make ~neg_mode:false t [] in normalize r, ctx end From 417108a3ffa29b29710864066ac41dfc3bdea9ff Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 24 Jul 2023 13:25:08 +0200 Subject: [PATCH 3/6] Update opam files --- alt-ergo-lib.opam | 1 + 1 file changed, 1 insertion(+) diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam index 1bffd419d..5888baadb 100644 --- a/alt-ergo-lib.opam +++ b/alt-ergo-lib.opam @@ -26,6 +26,7 @@ depends: [ "fmt" "stdlib-shims" "ppx_blob" + "ppx_deriving" "camlzip" {>= "1.07"} "odoc" {with-doc} ] From aae3767cfcce35d25cd2ed54b7c3ec2ba0e129e2 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 24 Jul 2023 18:17:54 +0200 Subject: [PATCH 4/6] Rename neg_mode and remove no_variables function --- src/lib/reasoners/bitv.ml | 70 ++++++++++++++++++--------------------- 1 file changed, 32 insertions(+), 38 deletions(-) diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index 8ad453e12..d4a87358c 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -236,32 +236,26 @@ module Shostak(X : ALIEN) = struct let st = match st with | Cte b -> Cte (not b) - | _ -> assert false + | Other _ | Ext _ -> + (* After normalization, the semantic value in + the constructor Other and Ext cannot be a bitvector. + Thus, these values are always uninterpreted for the + Bitv theory. Supporting these cases requires important + modifications of the solver function and will be supported + later. *) + raise (Failure "Not supported") in { bv = st; sz } ) r - let no_variable r = - List.for_all (fun { bv = st; _ } -> - match st with - | Cte _ -> true - | Other _ | Ext _ -> - (* After normalization, the semantic value in - the constructor Other and Ext cannot be a bitvector. - Thus, these values are always uninterpreted for the - Bitv theory. *) - false - ) r - - let other ~neg_mode t sz ctx = + let other ~neg t sz ctx = let r, ctx' = X.make t in let ctx = List.rev_append ctx' ctx in match X.extract r with | Some bv -> - if neg_mode then - if no_variable bv then - negate_abstract bv, ctx - else + if neg then + try negate_abstract bv, ctx with + | Failure _ -> [ { bv = Other (X.term_embed (E.BV.bvnot t)); sz } ], ctx else bv, ctx @@ -315,58 +309,58 @@ module Shostak(X : ALIEN) = struct | _ -> normalize_st s :: normalize tts end - let rec make ~neg_mode t = vmake ~neg_mode (view t) - and vextract ~neg_mode i j tv = + let rec make ~neg t = vmake ~neg (view t) + and vextract ~neg i j tv = let size = j - i + 1 in match tv.descr with | Vcte z -> - vmake ~neg_mode { descr = Vcte (String.sub z (tv.size - j - 1) size); size } + vmake ~neg { descr = Vcte (String.sub z (tv.size - j - 1) size); size } | Vother t -> - let+ o = other ~neg_mode t tv.size in + let+ o = other ~neg t tv.size in extract tv.size i j o | Vextract (t'', k, _) -> - vmake ~neg_mode { descr = Vextract (t'', i + k, j + k); size } + vmake ~neg { descr = Vextract (t'', i + k, j + k); size } | Vconcat (u, v) -> let vu = view u and vv = view v in if j < vv.size then - vextract ~neg_mode i j vv + vextract ~neg i j vv else if i >= vv.size then - vextract ~neg_mode (i - vv.size) (j - vv.size) vu + vextract ~neg (i - vv.size) (j - vv.size) vu else - let+ u = vextract ~neg_mode 0 (j - vv.size) vu - and+ v = vextract ~neg_mode i (vv.size - 1) vv + let+ u = vextract ~neg 0 (j - vv.size) vu + and+ v = vextract ~neg i (vv.size - 1) vv in u @ v | Vnot t -> - vextract ~neg_mode:(not neg_mode) i j (view t) - and vmake ~neg_mode tv ctx = + vextract ~neg:(not neg) i j (view t) + and vmake ~neg tv ctx = match tv.descr with | Vcte z -> let acc = ref [] in for i = String.length z - 1 downto 0 do let c = z.[i] in match c, !acc with - | '0', { bv = Cte b; sz } :: rst when Bool.equal b neg_mode -> + | '0', { bv = Cte b; sz } :: rst when Bool.equal b neg -> acc := { bv = Cte b; sz = sz + 1 } :: rst | '0', rst -> - acc := { bv = Cte neg_mode; sz = 1 } :: rst - | _, { bv = Cte b; sz } :: rst when Bool.equal b (not neg_mode) -> + acc := { bv = Cte neg; sz = 1 } :: rst + | _, { bv = Cte b; sz } :: rst when Bool.equal b (not neg) -> acc := { bv = Cte b; sz = sz + 1 } :: rst | _, rst -> - acc := { bv = Cte (not neg_mode); sz = 1 } :: rst + acc := { bv = Cte (not neg); sz = 1 } :: rst done; !acc, ctx - | Vother t -> other ~neg_mode t tv.size ctx + | Vother t -> other ~neg t tv.size ctx | Vextract (t', i, j) -> - run ctx @@ vextract ~neg_mode i j (view t') + run ctx @@ vextract ~neg i j (view t') | Vconcat (t1, t2) -> run ctx @@ - let+ t1 = make ~neg_mode t1 and+ t2 = make ~neg_mode t2 in + let+ t1 = make ~neg t1 and+ t2 = make ~neg t2 in t1 @ t2 | Vnot t -> - run ctx @@ make ~neg_mode:(not neg_mode) t + run ctx @@ make ~neg:(not neg) t let make t = - let r, ctx = make ~neg_mode:false t [] in + let r, ctx = make ~neg:false t [] in normalize r, ctx end From c87a4e974357320209e1fe87c0c57a602d0b82af Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 24 Jul 2023 18:18:17 +0200 Subject: [PATCH 5/6] Add tests --- tests/bitv/testfile-bvnot.dolmen.expected | 10 ++++++++ tests/bitv/testfile-bvnot.dolmen.smt2 | 28 +++++++++++++++++++++++ 2 files changed, 38 insertions(+) create mode 100644 tests/bitv/testfile-bvnot.dolmen.expected create mode 100644 tests/bitv/testfile-bvnot.dolmen.smt2 diff --git a/tests/bitv/testfile-bvnot.dolmen.expected b/tests/bitv/testfile-bvnot.dolmen.expected new file mode 100644 index 000000000..fd7df2ef6 --- /dev/null +++ b/tests/bitv/testfile-bvnot.dolmen.expected @@ -0,0 +1,10 @@ + +unsat + +unsat + +unsat + +unsat + +unsat diff --git a/tests/bitv/testfile-bvnot.dolmen.smt2 b/tests/bitv/testfile-bvnot.dolmen.smt2 new file mode 100644 index 000000000..65f6f111a --- /dev/null +++ b/tests/bitv/testfile-bvnot.dolmen.smt2 @@ -0,0 +1,28 @@ +(set-logic BV) +(push 1) +(assert (distinct #b0110 (bvnot #b1001))) +(check-sat) +(pop 1) + +(push 1) +(assert (distinct #b0110 (bvnot (bvnot #b0110)))) +(check-sat) +(pop 1) + +(push 1) +(assert (distinct #b1101 (bvnot ((_ extract 5 2) #b001011)))) +(check-sat) +(pop 1) + +(push 1) +(declare-const x (_ BitVec 4)) +(assert (distinct x (bvnot (bvnot x)))) +(check-sat) +(pop 1) + +(push 1) +(declare-const x (_ BitVec 4)) +(assert (= x (bvnot (bvadd #b0000 #b0000)))) +(assert (distinct x #b1111)) +(check-sat) +(pop 1) From cf8416dea8785b1857bfe378d49f44a08c1744c4 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 25 Jul 2023 15:22:09 +0200 Subject: [PATCH 6/6] Remove ppx_deriving dependency --- alt-ergo-lib.opam | 1 - dune-project | 1 - src/lib/dune | 2 +- src/lib/reasoners/bitv.ml | 1 - 4 files changed, 1 insertion(+), 4 deletions(-) diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam index 5888baadb..1bffd419d 100644 --- a/alt-ergo-lib.opam +++ b/alt-ergo-lib.opam @@ -26,7 +26,6 @@ depends: [ "fmt" "stdlib-shims" "ppx_blob" - "ppx_deriving" "camlzip" {>= "1.07"} "odoc" {with-doc} ] diff --git a/dune-project b/dune-project index 48602d535..251d40b4e 100644 --- a/dune-project +++ b/dune-project @@ -86,7 +86,6 @@ See more details on http://alt-ergo.ocamlpro.com/" fmt stdlib-shims ppx_blob - ppx_deriving (camlzip (>= 1.07)) (odoc :with-doc) ) diff --git a/src/lib/dune b/src/lib/dune index e57160e99..fe1f9080f 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -25,7 +25,7 @@ alt_ergo_prelude fmt ) - (preprocess (pps ppx_blob ppx_deriving.show)) + (preprocess (pps ppx_blob)) (preprocessor_deps (glob_files ../preludes/*.ae)) ; .mli only modules *also* need to be in this field diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index d4a87358c..4eab14800 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -199,7 +199,6 @@ module Shostak(X : ALIEN) = struct | Vextract of 'a * int * int | Vconcat of 'a * 'a | Vnot of 'a - (* [@@deriving show] *) type 'a view = { descr : 'a view_descr ; size : int }