Solver Improvements (#2502)

In the course of my investigation, I found that the SMT2 definitions were being converted to text properly, but not making it all the way to the solver. This seems to be an issue with Python's unbuffered pipe implementation. I'm not sure what the exact issue is, but switching to buffered I/O and adding explicit calls to flush has fixed the tests.

* Fix invalid escape characters

* Add debug logs for solver errors

* Optimize imports

* Split buffer on newlines

We're going to have to take this out before merging but hopefully it'll help figure out what's going wrong

* Clear the debug buffer upon reset

* Make sure we flush data sent to the solver

* Fix typo

* Try buffering I/O with the solver

* Move _clear_buffers out of loop

* Remove debugging code

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 = "BIVEC"
+            name = "BITVEC"
             avoid_collisions = True
         if avoid_collisions:
             name = self._make_unique_name(name)

manticore/core/smtlib/solver.py

@@ -14,26 +14,22 @@
 # You can create new symbols operate on them. The declarations will be sent to the smtlib process when needed.
 # You can add new constraints. A new constraint may change the state from {None, sat} to {sat, unsat, unknown}
 
-import os
-import fcntl
-import shutil
-import threading
-from queue import Queue
 import collections
+import fcntl
+import os
 import shlex
+import shutil
 import time
 from abc import abstractmethod
-from functools import lru_cache
-from typing import Any, Dict, Tuple, Sequence, Optional, List
-from subprocess import PIPE, Popen, check_output
 from random import shuffle
-import re
+from subprocess import PIPE, Popen, check_output
+from typing import Any, Sequence, List
+
 from . import operators as Operators
 from .constraints import *
 from .visitors import *
-from ...exceptions import Z3NotFoundError, SolverError, SolverUnknown, TooManySolutions, SmtlibError
+from ...exceptions import SolverError, SolverUnknown, TooManySolutions, SmtlibError
 from ...utils import config
-from . import issymbolic
 
 logger = logging.getLogger(__name__)
 consts = config.get_group("smt")
@@ -57,7 +53,7 @@
 
 # Regular expressions used by the solver
 RE_GET_EXPR_VALUE_ALL = re.compile(
-    "\(([a-zA-Z0-9_]*)[ \\n\\s]*(#b[0-1]*|#x[0-9a-fA-F]*|[\(]?_ bv[0-9]* [0-9]*|true|false)\\)"
+    r"\(([a-zA-Z0-9_]*)[ \n\s]*(#b[0-1]*|#x[0-9a-fA-F]*|[(]?_ bv[0-9]* [0-9]*|true|false)\)"
 )
 RE_GET_EXPR_VALUE_FMT_BIN = re.compile(r"\(\((?P<expr>(.*))[ \n\s]*#b(?P<value>([0-1]*))\)\)")
 RE_GET_EXPR_VALUE_FMT_DEC = re.compile(r"\(\((?P<expr>(.*))\ \(_\ bv(?P<value>(\d*))\ \d*\)\)\)")
@@ -217,7 +213,7 @@ def start(self):
             shlex.split(self._command),
             stdin=PIPE,
             stdout=PIPE,
-            bufsize=0,
+            # bufsize=0,  # if we set input to unbuffered, we get syntax errors in large formulas
             universal_newlines=True,
             close_fds=True,
         )
@@ -258,6 +254,7 @@ def send(self, cmd: str) -> None:
         try:
             self._proc.stdout.flush()  # type: ignore
             self._proc.stdin.write(f"{cmd}\n")  # type: ignore
+            self._proc.stdin.flush()  # type: ignore
         except (BrokenPipeError, IOError) as e:
             logger.critical(
                 f"Solver encountered an error trying to send commands: {e}.\n"
@@ -309,7 +306,7 @@ def recv(self, wait=True) -> Optional[str]:
         self._last_buf = ""
 
         if "(error" in buf:
-            raise SolverException(f"Error in smtlib: {buf}")
+            raise SolverException(f"Solver error: {buf}")
 
         if self._debug:
             logger.debug("<%s", buf)
@@ -324,6 +321,10 @@ def _restart(self) -> None:
     def is_started(self):
         return self._proc is not None
 
+    def clear_buffers(self):
+        self._proc.stdout.flush()
+        self._proc.stdin.flush()
+
 
 class SMTLIBSolver(Solver):
     ncores: Optional[int] = None
@@ -387,6 +388,8 @@ def _reset(self, constraints: Optional[str] = None) -> None:
             self._smtlib.stop()  # does not do anything if already stopped
             self._smtlib.start()
 
+        self._smtlib.clear_buffers()
+
         for cfg in self._init:
             self._smtlib.send(cfg)
 

tests/other/test_smtlibv2.py

@@ -790,11 +790,12 @@ def test_arithmetic_simplify(self):
         exp |= 0
         self.assertEqual(get_depth(exp), 4)
         self.assertEqual(
-            translate_to_smtlib(exp), "(bvor (bvand (bvor BIVEC #x00000000) #x00000001) #x00000000)"
+            translate_to_smtlib(exp),
+            "(bvor (bvand (bvor BITVEC #x00000000) #x00000001) #x00000000)",
         )
         exp = arithmetic_simplify(exp)
         self.assertTrue(get_depth(exp) < 4)
-        self.assertEqual(translate_to_smtlib(exp), "(bvand BIVEC #x00000001)")
+        self.assertEqual(translate_to_smtlib(exp), "(bvand BITVEC #x00000001)")
 
     def test_arithmetic_simplify_extract(self):
         cs = ConstraintSet()