Merge pull request diffblue#273 from diffblue/smowton/fix/end_to_end_tests

SEC-144: Add a variety of end-to-end security analyser tests, and fix several bugs exposed by them

Author: smowton

cbmc/src/util/irep_ids.def

@@ -845,6 +845,7 @@ IREP_ID_ONE(havoc_object)
 IREP_ID_TWO(overflow_shl, overflow-shl)
 IREP_ID_ONE(lvsa_evs_type)
 IREP_ID_ONE(is_initializer)
+IREP_ID_TWO(C_is_taint_wrapper_type, #is_taint_wrapper_type)
 
 #undef IREP_ID_ONE
 #undef IREP_ID_TWO

regression/end_to_end/.gitignore

@@ -0,0 +1,3 @@
+# Ensure Ant build directories are ignored below here:
+build/
+dist/

regression/end_to_end/driver.py

@@ -18,6 +18,8 @@ def working_dir(new_dir):
 @contextlib.contextmanager
 def temp_dir_deleter(dirname):
     yield
+    if "SECURITY_ANALYSER_END_TO_END_TESTS_KEEP_RESULTS" in os.environ:
+        return
     try:
         shutil.rmtree(dirname)
     except:
@@ -51,8 +53,9 @@ def trace_exists(self, function, line_no):
         return False
 
 def run_security_analyser_pipeline(
-    relative_jar_path,
+    relative_binary_path,
     relative_rules_path,
+    base_path,
     extra_args = []):
 
     regression_tests_path = os.getcwd()
@@ -61,22 +64,24 @@ def run_security_analyser_pipeline(
         raise Exception("Set SECURITY_SCANNER_HOME to a path containing the 'security-analyzer' binary")
     pipeline_driver_path = \
         os.path.realpath(os.path.join(regression_tests_path, "..", "driver", "run.py"))
-    absolute_jar_path = \
-        os.path.join(regression_tests_path, "end_to_end", relative_jar_path)
+    absolute_binary_path = \
+        os.path.join(base_path, relative_binary_path)
     absolute_rules_path = \
-        os.path.join(regression_tests_path, "end_to_end", relative_rules_path)
+        os.path.join(base_path, relative_rules_path)
 
     results_dir = tempfile.mkdtemp()
     temporary_dir = tempfile.mkdtemp()
 
     cmdline = ["python", pipeline_driver_path,
                "-C", absolute_rules_path,
-               "-I", absolute_jar_path,
+               "-I", absolute_binary_path,
                "-R", results_dir,
                "-T", temporary_dir,
-               "--name", relative_jar_path,
-               "--verbosity", "0"]
+               "--name", relative_binary_path,
+               "--verbosity", "9"]
     cmdline.extend(extra_args)
+    if "SECURITY_ANALYSER_END_TO_END_TESTS_EXTRA_ARGS" in os.environ:
+        cmdline.extend(os.environ["SECURITY_ANALYSER_END_TO_END_TESTS_EXTRA_ARGS"].split(","))
 
     with working_dir(analyzer_home), \
          temp_dir_deleter(results_dir), \
@@ -106,4 +111,7 @@ def run_security_analyser_pipeline(
                         trace_json = json.load(trace_file)
                         inline_traces.append(trace_json)
 
+        if "SECURITY_ANALYSER_END_TO_END_TESTS_KEEP_RESULTS" in os.environ:
+            print("Test %s kept results (%s) and temporary directory (%s)" % (cmdline, results_dir, temporary_dir))
+
         return ErrorTraces(traces)

regression/end_to_end/general001/test_general001.py

@@ -2,9 +2,12 @@
 from regression.end_to_end.driver \
     import run_security_analyser_pipeline
 
+import os
+
 def test_general001():
     traces = run_security_analyser_pipeline(
-        "general001/taint_traces_01.jar",
-        "general001/taint_traces_01_rules.json")
+        "taint_traces_01.jar",
+        "taint_traces_01_rules.json",
+        os.path.realpath(os.path.dirname(__file__)))
     assert traces.count_traces() > 0
     assert traces.trace_exists("java::Main.bug:(I)V", 84)

regression/end_to_end/general002/test_general002.py

@@ -2,8 +2,11 @@
 from regression.end_to_end.driver \
     import run_security_analyser_pipeline
 
+import os
+
 def test_general002():
     traces = run_security_analyser_pipeline(
-        "general002/taint_traces_02.jar",
-        "general002/taint_traces_02_rules.json")
+        "taint_traces_02.jar",
+        "taint_traces_02_rules.json",
+        os.path.realpath(os.path.dirname(__file__)))
     assert traces.count_traces() == 0

regression/end_to_end/general003/test_general003.py

@@ -2,8 +2,11 @@
 from regression.end_to_end.driver \
     import run_security_analyser_pipeline
 
+import os
+
 def test_general003():
     traces = run_security_analyser_pipeline(
-        "general003/taint_traces_03.jar",
-        "general003/taint_traces_03_rules.json")
+        "taint_traces_03.jar",
+        "taint_traces_03_rules.json",
+        os.path.realpath(os.path.dirname(__file__)))
     assert traces.count_traces() == 0

regression/end_to_end/general004/test_general004.py

@@ -2,10 +2,13 @@
 from regression.end_to_end.driver \
     import run_security_analyser_pipeline
 
+import os
+
 def test_general004():
     traces = run_security_analyser_pipeline(
-        "general004/taint_traces_04.jar",
-        "general004/taint_traces_04_rules.json")
+        "taint_traces_04.jar",
+        "taint_traces_04_rules.json",
+        os.path.realpath(os.path.dirname(__file__)))
     assert traces.count_traces() > 0
     assert traces.trace_exists("java::Main.baz0:()V", 19)
     assert traces.trace_exists("java::Main.baz1:()V", 26)

regression/end_to_end/general005/test_general005.py

@@ -2,10 +2,13 @@
 from regression.end_to_end.driver \
     import run_security_analyser_pipeline
 
+import os
+
 def test_general005():
     traces = run_security_analyser_pipeline(
-        "general005/taint_traces_05.jar",
-        "general005/taint_traces_05_rules.json",
+        "taint_traces_05.jar",
+        "taint_traces_05_rules.json",
+        os.path.realpath(os.path.dirname(__file__)),
         ["--data-flow-insensitive-instrumentation"])
     assert traces.count_traces() > 0
     assert traces.trace_exists("java::DummyAssignmentSubmissionEdit.setSubmittedText:(Ljava/lang/String;)V", 3)

regression/end_to_end/general006/test_general006.py

@@ -2,10 +2,13 @@
 from regression.end_to_end.driver \
     import run_security_analyser_pipeline
 
+import os
+
 def test_general006():
     traces = run_security_analyser_pipeline(
-        "general006/taint_traces_06.jar",
-        "general006/taint_traces_06_rules.json",
+        "taint_traces_06.jar",
+        "taint_traces_06_rules.json",
+        os.path.realpath(os.path.dirname(__file__)),
         ["--data-flow-insensitive-instrumentation"])
     assert traces.count_traces() > 0
     assert traces.trace_exists("java::taint_test.test.doGet:(Ljavax/servlet/http/HttpServletRequest;Ljavax/servlet/http/HttpServletResponse;)V", 165)

regression/end_to_end/general007/test_general007.py

@@ -2,9 +2,12 @@
 from regression.end_to_end.driver \
     import run_security_analyser_pipeline
 
+import os
+
 def test_general007():
     traces = run_security_analyser_pipeline(
-        "general007/taint_traces_07.jar",
-        "general007/taint_traces_07_rules.json")
+        "taint_traces_07.jar",
+        "taint_traces_07_rules.json",
+        os.path.realpath(os.path.dirname(__file__)))
     assert traces.count_traces() > 0
     assert traces.trace_exists("java::training07.test.doGet:(Ltraining07/HttpServletRequest;Ltraining07/HttpServletResponse;)V", 109)