merge

Author: feliam

manticore/core/smtlib/expression.py

@@ -1259,7 +1259,7 @@ def select(self, index):
             return ArraySelect(self, index)
 
         # if a default is defined we need to check if the index was previously written
-        return BitVecITE(self.is_known(index), ArraySelect(self, index), self.cast_value(default))
+        return local_simplify(BitVecITE(self.is_known(index), ArraySelect(self, index), self.cast_value(default)))
 
     def store(self, index, value):
         casted = self.cast_index(index)

manticore/core/smtlib/solver.py

@@ -214,7 +214,7 @@ def __readline_and_count(self):
         assert self._proc.stdout
         buf = self._proc.stdout.readline()  # No timeout enforced here
         # If debug is enabled check if the solver reports a syntax error
-        # print (">",buf)
+        #print (">",buf)
         if self._debug:
             if "(error" in buf:
                 raise SolverException(f"Error in smtlib: {buf}")
@@ -227,7 +227,7 @@ def send(self, cmd: str) -> None:
 
         :param cmd: a SMTLIBv2 command (ex. (check-sat))
         """
-        # print ("<",cmd)
+        #print ("<",cmd)
         if self._debug:
             logger.debug(">%s", cmd)
         self._proc.stdout.flush()  # type: ignore

manticore/core/smtlib/visitors.py

@@ -961,10 +961,11 @@ def visit_Operation(self, expression, *operands):
 
     @property
     def result(self):
-        return self.apply_bindings(self._stack[-1])
+        return f"{self.apply_bindings(self._stack[-1])}"
 
     def apply_bindings(self, main_smtlib_str):
         # Python program to print topological sorting of a DAG
+        # Well-sortedness requirements
         from toposort import toposort_flatten as toposort
 
         G = {}
@@ -977,25 +978,22 @@ def apply_bindings(self, main_smtlib_str):
             if not variables:
                 G[name] = set()
 
-        output = ""
         # Build let statement
+        output = main_smtlib_str
         for name in reversed(toposort(G)):
             if name not in self._bindings:
                 continue
             expr, smtlib = self._bindings[name]
 
+
             # FIXME: too much string manipulation. Search occurrences in the Expression realm
-            if main_smtlib_str.count(name) + output.count(name) == 1:
-                main_smtlib_str = main_smtlib_str.replace(name, smtlib)
+            if output.count(name) <= 1:
+                #output = f"let (({name} {smtlib})) ({output})"
                 output = output.replace(name, smtlib)
             else:
-                output = f"({name} {smtlib}) {output}"
+                output = f"(let (({name} {smtlib})) {output})"
 
-        if output:
-            output = f"(let ({output}) {main_smtlib_str})"
-        else:
-            output = main_smtlib_str
-        return output
+        return f"{output}"
 
     def declarations(self):
         result = ""

manticore/platforms/platform.py

@@ -51,7 +51,6 @@ class Platform(Eventful):
 
     _published_events = {"solve"}
 
-
     def __init__(self, *, state: Optional["StateBase"] = None, **kwargs):
         self._state = state
         super().__init__(**kwargs)

tests/other/test_smtlibv2.py

@@ -951,15 +951,14 @@ def test_visitors(self):
 
         self.assertEqual(get_depth(aux), 9)
         self.maxDiff = 5500
-        print(translate_to_smtlib(aux))
         self.assertEqual(
             translate_to_smtlib(aux, use_bindings=False),
             "(select (store (store (store MEM #x00000000 #x61) #x00000001 #x62) #x00000003 (select (store (store MEM #x00000000 #x61) #x00000001 #x62) (bvadd VAR #x00000001))) (bvadd VAR ((_ zero_extend 24) (select (store (store (store MEM #x00000000 #x61) #x00000001 #x62) #x00000003 (select (store (store MEM #x00000000 #x61) #x00000001 #x62) (bvadd VAR #x00000001))) VAR))))",
         )
 
         self.assertEqual(
             translate_to_smtlib(aux, use_bindings=True),
-            "(let ((!a_2! (store (store MEM #x00000000 #x61) #x00000001 #x62)) (!a_4! (store !a_2! #x00000003 (select !a_2! (bvadd VAR #x00000001)))) ) (select !a_4! (bvadd VAR ((_ zero_extend 24) (select !a_4! VAR)))))",
+            "(let ((!a_2! (store (store MEM #x00000000 #x61) #x00000001 #x62))) (let ((!a_4! (store !a_2! #x00000003 (select !a_2! (bvadd VAR #x00000001))))) (select !a_4! (bvadd VAR ((_ zero_extend 24) (select !a_4! VAR))))))"
         )
 
         values = arr[0:2]