Change how we query for version (#1023)

Fixes #1021

This also should decrease how many times we invoke z3. (The instance used to query version should stick around)

manticore/core/smtlib/solver.py

@@ -20,6 +20,7 @@
 from .constraints import *
 import logging
 import re
+import shlex
 import time
 from .visitors import *
 from ...utils.helpers import issymbolic, istainted, taint_with, get_taints, memoized
@@ -128,7 +129,13 @@ def __init__(self):
         super().__init__()
         self._proc = None
 
+        self._command = 'z3 -t:240000 -memory:16384 -smt2 -in'
+        self._init = ['(set-logic QF_AUFBV)', '(set-option :global-decls false)']
+        self._get_value_fmt = (re.compile('\(\((?P<expr>(.*))\ #x(?P<value>([0-9a-fA-F]*))\)\)'), 16)
+
         self.debug = False
+        # To cache what get-info returned; can be directly set when writing tests
+        self._received_version = None
         self.version = self._solver_version()
 
         self.support_maximize = False
@@ -147,12 +154,7 @@ def __init__(self):
         else:
             logger.debug(' Please install Z3 4.4.1 or newer to get optimization support')
 
-        self._command = 'z3 -t:240000 -memory:16384 -smt2 -in'
-        self._init = ['(set-logic QF_AUFBV)', '(set-option :global-decls false)']
-        self._get_value_fmt = (re.compile('\(\((?P<expr>(.*))\ #x(?P<value>([0-9a-fA-F]*))\)\)'), 16)
-
-    @staticmethod
-    def _solver_version():
+    def _solver_version(self):
         '''
         If we
         fail to parse the version, we assume z3's output has changed, meaning it's a newer
@@ -164,16 +166,12 @@ def _solver_version():
 
         '''
         their_version = Version(0, 0, 0)
-        try:
-            version_cmd_output = check_output('z3 -version'.split())
-        except OSError:
-            raise Z3NotFoundError
-        try:
-            version = version_cmd_output.split()[2]
-            their_version = Version(*map(int, version.split('.')))
-        except (IndexError, ValueError, TypeError):
-            pass
-        return their_version
+        self._reset()
+        if self._received_version is None:
+            self._send('(get-info :version)')
+            self._received_version = self._recv()
+        key, version = shlex.split(self._received_version[1:-1])
+        return Version(*map(int, version.split('.')))
 
     def _start_proc(self):
         ''' Auxiliary method to spawn the external solver process'''

tests/test_smtlibv2.py

@@ -794,33 +794,23 @@ def test_SDIV(self):
         self.assertTrue(solver.check(cs))
         self.assertEqual(solver.get_value(cs, a), -7&0xFF)
 
-import importlib
-class Z3Test(unittest.TestCase):
-    def setUp(self):
-        #Manual mock for check_output
-        self.module = importlib.import_module('manticore.core.smtlib.solver')
-        self.module.check_output = lambda *args, **kwargs: self.version
-        self.z3 = self.module.Z3Solver
-
     def test_check_solver_min(self):
-        self.version = 'Z3 version 4.4.1'
-        self.assertTrue(self.z3._solver_version() == Version(major=4, minor=4, patch=1))
+        self.solver._received_version = '(:version "4.4.1")'
+        self.assertTrue(self.solver._solver_version() == Version(major=4, minor=4, patch=1))
 
     def test_check_solver_newer(self):
-        self.version = 'Z3 version 4.5.0'
-        self.assertTrue(self.z3._solver_version() > Version(major=4, minor=4, patch=1))
+        self.solver._received_version = '(:version "4.5.0")'
+        self.assertTrue(self.solver._solver_version() > Version(major=4, minor=4, patch=1))
 
     def test_check_solver_optimize(self):
-        self.version = 'Z3 version 4.5.0'
-        solver = self.z3()
-        self.assertTrue(solver.support_maximize)
-        self.assertTrue(solver.support_minimize)
+        self.solver._received_version = '(:version "4.5.0")'
+        self.assertTrue(self.solver.support_maximize)
+        self.assertTrue(self.solver.support_minimize)
 
     def test_check_solver_optimize(self):
-        self.version = 'Z3 version 4.4.0'
-        solver = self.z3()
-        self.assertFalse(solver.support_maximize)
-        self.assertFalse(solver.support_minimize)
+        self.solver._received_version = '(:version "4.4.0")'
+        self.assertFalse(self.solver.support_maximize)
+        self.assertFalse(self.solver.support_minimize)
 
 if __name__ == '__main__':
     unittest.main()