Merge pull request #21 from testsmt/debug

Addressing #18 (Potentially missed bugs due to errors with get-models etc.)

src/parsing/parse.py

@@ -16,16 +16,42 @@ class ErrorListener(ErrorListener):
     def syntaxError(self, recognizer, offendingSymbol, line, column, msg, e):
         print("Parser error on line %d column %d." % (line, column), flush=True)
 
-def remove_set_logic_status(formula):
+def prepare_seed(formula):
+    """
+    Prepare seed script for fuzzing. Remove set-logic, set-info and output-producing 
+    commands. Set-logic and set-info may raise warning messages from SMT solvers. 
+    Output-producing commands may cause errors, e.g., get-model, get-proof etc.   
+    Errors such as 
+
+                (error "line X column Y: msg") 
+
+    are ignored to avoid false positives in the bug detection logic. As the bug  
+    detection logic is based on string matching such errors may lead to soundness   
+    issues being ignored, e.g. if the error occurred after a faulty check-sat result. 
+    Hence, we remove all output-producing SMT-LIB commands from the script.  
+    """ 
     new_cmds = []
     for cmd in formula.commands:
-        if isinstance(cmd,SMTLIBCommand) and "(set-info" in cmd.cmd_str:continue
-        if isinstance(cmd,SMTLIBCommand) and "(set-logic"  in cmd.cmd_str: continue
+        if "set-info" in cmd.__str__():continue
+        if "set-logic" in cmd.__str__(): continue
+
+        # Ignore output-producing commands to make sure the detection logic won't be mislead  
+        # by the other SMT-LIB commands which produce output.   
+        #
+        if "get-model" in cmd.__str__(): continue
+        if "get-assertions" in cmd.__str__(): continue
+        if "get-proof" in cmd.__str__(): continue
+        if "get-unsat-assumptions" in cmd.__str__(): continue
+        if "get-unsat-core" in cmd.__str__():continue
+        if "get-value" in cmd.__str__(): continue
+        if "echo" in cmd.__str__(): continue
+        if "simplify" in cmd.__str__(): continue
         new_cmds.append(cmd)
+
     formula.commands = new_cmds
     return formula
 
-def generate_ast(stream):
+def generate_ast(stream, prep_seed=True):
     error_listener = ErrorListener()
     lexer = SMTLIBv2Lexer(stream)
     lexer.removeErrorListeners()
@@ -40,8 +66,8 @@ def generate_ast(stream):
     # empty file or parser preceding parser errror
     if len(formula.commands) == 0:
         return None
-
-    return remove_set_logic_status(formula)
+    
+    return prepare_seed(formula) if prep_seed else formula 
 
 
 def parse_filestream(fn,timeout_limit):

tests/unittests/issue18.smt2

@@ -0,0 +1,9 @@
+(declare-fun a () String)
+(declare-fun b () String)
+(assert (= a b))                                                                 
+(check-sat)
+(simplify (= a b))                                                                 
+(simplify (str.++ a b))
+(assert (= a b))                                                                 
+(check-sat)
+(get-model)

tests/unittests/test_parsing.py

@@ -8,8 +8,21 @@
 class ParsingTestCase(unittest.TestCase):
     def test_issue9(self): 
         formula = parse_file("tests/unittests/issue7.smt2")
-        return '\x0a' in formula.__str__() and '\n' in formula.__str__()
+        self.assertTrue('\x0a' in formula.__str__() and '\n' in formula.__str__())
 
+    def test_issue18(self): 
+        formula = parse_file("tests/unittests/issue18.smt2",silent=False)
+        oracle="""\
+(declare-fun a () String)
+(declare-fun b () String)
+(assert (= a b))
+(check-sat)
+(assert (= a b))
+(check-sat)"""
+        self.assertEqual(oracle, formula.__str__())
+
+
+
 
 if __name__ == '__main__':
     unittest.main()