Support to use boolector as the SMT solver

.github/workflows/ci.yml

@@ -57,18 +57,34 @@ jobs:
       env:
         TEST_TYPE: ${{ matrix.type }}
       run: |
+        #install utils
+        pip install coveralls
+        pip install -e ".[dev-noks]"
         #install cvc4
         sudo wget -O /usr/bin/cvc4 https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt
         sudo chmod +x /usr/bin/cvc4
         #install yices
         sudo add-apt-repository ppa:sri-csl/formal-methods
         sudo apt-get update
         sudo apt-get install yices2
+        #install boolector
+        mkdir -p /tmp/build
+        cd /tmp/build
+        git clone https://github.com/boolector/boolector.git
+        cd boolector
+        # Version 3.2.1
+        git checkout "f61c0dcf4a76e2f7766a6358bfb9c16ca8217224"
+        git log -1 --oneline > ../boolector.commit
+        ./contrib/setup-lingeling.sh
+        ./contrib/setup-btor2tools.sh
+        ./configure.sh
+        cd build
+        make -j4
+        mkdir -p /tmp/boolector
+        sudo make DESTDIR=/usr install
         # Install solc unconditionally because it only takes a second or two
         sudo wget -O /usr/bin/solc https://github.com/ethereum/solidity/releases/download/v0.4.24/solc-static-linux
         sudo chmod +x /usr/bin/solc
-        pip install coveralls
-        pip install -e ".[dev-noks]"
     - name: Run Tests
       env:
         TEST_TYPE: ${{ matrix.type }}

manticore/core/smtlib/constraints.py

@@ -393,7 +393,7 @@ def new_bitvec(self, size, name=None, taint=frozenset(), avoid_collisions=False)
         if size <= 0:
             raise ValueError(f"Bitvec size ({size}) can't be equal to or less than 0")
         if name is None:
-            name = "BV"
+            name = "BIVEC"
             avoid_collisions = True
         if avoid_collisions:
             name = self._make_unique_name(name)

manticore/core/smtlib/solver.py

@@ -40,6 +40,7 @@ class SolverType(config.ConfigEnum):
     cvc4 = "cvc4"
     yices = "yices"
     auto = "auto"
+    boolector = "boolector"
 
 
 logger = logging.getLogger(__name__)
@@ -54,6 +55,7 @@ class SolverType(config.ConfigEnum):
 consts.add("z3_bin", default="z3", description="Z3 solver binary to use")
 consts.add("cvc4_bin", default="cvc4", description="CVC4 solver binary to use")
 consts.add("yices_bin", default="yices-smt2", description="Yices solver binary to use")
+consts.add("boolector_bin", default="boolector", description="Boolector solver binary to use")
 
 
 consts.add("defaultunsat", default=True, description="Consider solver timeouts as unsat core")
@@ -64,7 +66,7 @@ class SolverType(config.ConfigEnum):
 consts.add(
     "solver",
     default=SolverType.auto,
-    description="Choose default smtlib2 solver (z3, yices, cvc4, auto)",
+    description="Choose default smtlib2 solver (z3, yices, cvc4, boolector, auto)",
 )
 
 # Regular expressions used by the solver
@@ -263,7 +265,6 @@ def __init__(
         self,
         command: str,
         init: Sequence[str] = None,
-        value_fmt: int = 16,
         support_reset: bool = False,
         support_minmax: bool = False,
         support_pushpop: bool = False,
@@ -282,15 +283,6 @@ def __init__(
         if init is None:
             init = tuple()
         self._init = init
-        self._get_value_fmt = (
-            {
-                2: RE_GET_EXPR_VALUE_FMT_BIN,
-                10: RE_GET_EXPR_VALUE_FMT_DEC,
-                16: RE_GET_EXPR_VALUE_FMT_HEX,
-            }[value_fmt],
-            value_fmt,
-        )
-
         self._support_minmax = support_minmax
         self._support_reset = support_reset
         self._support_pushpop = support_pushpop
@@ -351,15 +343,25 @@ def _assert(self, expression: Bool):
 
     def __getvalue_bv(self, expression_str: str) -> int:
         self._smtlib.send(f"(get-value ({expression_str}))")
-        pattern, base = self._get_value_fmt
-        m = pattern.match(self._smtlib.recv())
+        t = self._smtlib.recv()
+        base = 2
+        m = RE_GET_EXPR_VALUE_FMT_BIN.match(t)
+        if m is None:
+            m = RE_GET_EXPR_VALUE_FMT_DEC.match(t)
+            base = 10
+        if m is None:
+            m = RE_GET_EXPR_VALUE_FMT_HEX.match(t)
+            base = 16
+        if m is None:
+            raise SolverError(f"I don't know how to parse the value {str(t)} from {expression_str}")
+
         expr, value = m.group("expr"), m.group("value")  # type: ignore
         return int(value, base)
 
     def __getvalue_bool(self, expression_str):
         self._smtlib.send(f"(get-value ({expression_str}))")
         ret = self._smtlib.recv()
-        return {"true": True, "false": False}[ret[2:-2].split(" ")[1]]
+        return {"true": True, "false": False, "#b0": False, "#b1": True}[ret[2:-2].split(" ")[1]]
 
     def _getvalue(self, expression) -> Union[int, bool, bytes]:
         """
@@ -657,7 +659,6 @@ def __init__(self):
         super().__init__(
             command=command,
             init=init,
-            value_fmt=16,
             support_minmax=support_minmax,
             support_reset=support_reset,
             multiple_check=multiple_check,
@@ -726,7 +727,6 @@ def __init__(self):
         super().__init__(
             command=command,
             init=init,
-            value_fmt=2,
             debug=False,
             support_minmax=False,
             support_reset=False,
@@ -737,7 +737,14 @@ class CVC4Solver(SMTLIBSolver):
     def __init__(self):
         init = ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"]
         command = f"{consts.cvc4_bin} --lang=smt2 --incremental"
-        super().__init__(command=command, value_fmt=10, init=init)
+        super().__init__(command=command, init=init)
+
+
+class BoolectorSolver(SMTLIBSolver):
+    def __init__(self):
+        init = ["(set-logic QF_AUFBV)", "(set-option :produce-models true)"]
+        command = f"{consts.boolector_bin} -i"
+        super().__init__(command=command, init=init)
 
 
 class SelectedSolver:
@@ -753,12 +760,19 @@ def instance(cls):
                     cls.choice = consts.solver.z3
                 elif shutil.which(consts.cvc4_bin):
                     cls.choice = consts.solver.cvc4
+                elif shutil.which(consts.boolector_bin):
+                    cls.choice = consts.solver.boolector
                 else:
                     raise SolverException(
-                        f"No Solver not found. Install one ({consts.yices_bin}, {consts.z3_bin}, {consts.cvc4_bin})."
+                        f"No Solver not found. Install one ({consts.yices_bin}, {consts.z3_bin}, {consts.cvc4_bin}, {consts.boolector_bin})."
                     )
         else:
             cls.choice = consts.solver
 
-        SelectedSolver = {"cvc4": CVC4Solver, "yices": YicesSolver, "z3": Z3Solver}[cls.choice.name]
+        SelectedSolver = {
+            "cvc4": CVC4Solver,
+            "boolector": BoolectorSolver,
+            "yices": YicesSolver,
+            "z3": Z3Solver,
+        }[cls.choice.name]
         return SelectedSolver.instance()