Support scripts for SV-COMP related tasks.

scripts/SV-COMP/evalall.py

@@ -0,0 +1,61 @@
+import os
+import shutil
+import subprocess
+import time
+
+
+def get_benchmarks():
+    return [
+        "ntdrivers/floppy2_true-unreach-call.i.cil.c",
+        ]
+
+
+def run_tool(command_to_execute, current_working_dir, timeout_in_seconds):
+    start_time = time.time()
+    process = subprocess.Popen(
+        command_to_execute,
+        cwd=current_working_dir,
+        stdout=subprocess.PIPE,
+        stderr=subprocess.PIPE,
+        shell=True,
+        preexec_fn=os.setsid
+        )
+    while time.time() - start_time < timeout_in_seconds:
+        is_allive = process.poll()
+        if is_allive is not None:
+            return True, str(process.stdout.read()) + str(process.stderr.read())
+        time.sleep(0.005)
+    try:
+        os.killpg(os.getpgid(process.pid), subprocess.signal.SIGTERM)
+    except ProcessLookupError:
+        if process.poll():
+            print("      WARNING: failed to kill the process! (PID=" + str(process.pid) + ")")
+    return False, ""
+
+
+def _main():
+    outdir = "./evalall_results"
+    os.makedirs(outdir, exist_ok=True)
+    for benchmark in get_benchmarks():
+        print("Processing " + benchmark)
+        # stime = time.time()
+        # out, err = subprocess.Popen(["python3", "./evaluate.py", benchmark], stdout=subprocess.PIPE, stderr=subprocess.PIPE).communicate()
+        # etime = time.time()
+        # sss = etime - stime
+        # print("Time = " + str(sss))
+        # output = out.decode("utf-8") + err.decode("utf-8")
+
+        state, output = run_tool("./evalall.sh \"" + benchmark + "\"", os.getcwd(), 3 * 60)
+        if state is False:
+            output = "EXECUTION OF THE TOOL FAILED!\n\n\n" + output
+        print(output)
+
+        with open(os.path.join(outdir, os.path.basename(benchmark) + ".txt"), "w") as ofile:
+            ofile.write(output)
+        shutil.copy("./witness", os.path.join(outdir, os.path.basename(benchmark) + ".xml"))
+        print("\n\n\n")
+    return 0
+
+
+if __name__ == "__main__":
+    exit(_main())

scripts/SV-COMP/evaluate.py

@@ -0,0 +1,212 @@
+import os
+import sys
+import traceback
+import shutil
+import argparse
+import json
+import re
+
+
+def _get_this_script_dir():
+    return os.path.dirname(__file__)
+
+
+def _get_cbmc_new_repo_dir():
+    return os.path.abspath(os.path.join(_get_this_script_dir(), "cbmc-fork-marek-trtik"))
+
+
+def _get_cbmc_new_binary():
+    return os.path.abspath(os.path.join(_get_cbmc_new_repo_dir(), "src", "cbmc", "cbmc"))
+
+
+def _get_installed_cbmc_new_binary():
+    return os.path.abspath(os.path.join(_get_this_script_dir(), "cbmc-sv-comp-2017-pr-rebase-binary"))
+
+
+def _get_cbmc_new_shell_script():
+    return _get_installed_cbmc_new_binary()[:_get_installed_cbmc_new_binary().rfind("-binary")]
+
+
+def _get_cbmc_old_repo_dir():
+    return os.path.abspath(os.path.join(_get_this_script_dir(), "cbmc-fork-tautschnig"))
+
+
+def _get_cbmc_old_binary():
+    return os.path.abspath(os.path.join(_get_cbmc_old_repo_dir(), "src", "cbmc", "cbmc"))
+
+
+def _get_installed_cbmc_old_binary():
+    return os.path.abspath(os.path.join(_get_this_script_dir(), "cbmc-sv-comp-2017-pr-binary"))
+
+
+def _get_cbmc_old_shell_script():
+    return _get_installed_cbmc_old_binary()[:_get_installed_cbmc_old_binary().rfind("-binary")]
+
+
+def _get_benchmarks_root_dir():
+    return os.path.abspath(os.path.join(_get_this_script_dir(), "..", "sv-benchmarks", "c"))
+
+
+def _get_results_diff_json_pathname():
+    return os.path.abspath(os.path.join(_get_this_script_dir(), "..", "RESULTS", "diff_CBMC-sv-comp-2017-pr-rebase_CBMC-sv-comp-2017-pr.json"))
+
+
+def _build_command_line_interface():
+    parser = argparse.ArgumentParser(
+        description="TODO",
+        )
+    parser.add_argument("-V", "--version", action="store_true",
+        help="Prints the version string of the module.")
+    parser.add_argument(
+        "benchmark", type=str,
+        help="TODO")
+    parser.add_argument(
+        "--old-cbmc", action="store_true",
+        help="TODO"
+        )
+    cmdline = parser.parse_args()
+
+    if cmdline.version:
+        print("v.1.0")
+        exit(0)
+
+    if not os.path.isfile(cmdline.benchmark):
+        if not os.path.isfile(os.path.join(_get_benchmarks_root_dir(), cmdline.benchmark)):
+            print("ERROR: In option 'benchmark': The passed path does not reference an existing file.")
+            exit(1)
+        else:
+            cmdline.benchmark = os.path.join(_get_benchmarks_root_dir(), cmdline.benchmark)
+    cmdline.benchmark = os.path.abspath(cmdline.benchmark)
+
+    return cmdline
+
+
+"""
+def get_cbmc_command_line_options():
+    return "--graphml-witness witness.graphml --32 --propertyfile ../sv-benchmarks/c/ReachSafety.prp ../sv-benchmarks/c/eca-rers2012/Problem01_label00_true-unreach-call.c
+           "--graphml-witness $LOG.witness --unwind $c --stop-on-fail $BIT_WIDTH $PROPERTY --function $ENTRY $BM"
+
+* executing the following command:
+    grep "^bitvector/.*unreach-call" *.set
+  in '../sv-benchmarks/c' produces:
+    ReachSafety-BitVectors.set:bitvector/*_false-unreach-call*.i
+    ReachSafety-BitVectors.set:bitvector/*_true-unreach-call*.i
+    ReachSafety-BitVectors.set:bitvector/*_false-unreach-call*.BV.c.cil.c
+    ReachSafety-BitVectors.set:bitvector/*_true-unreach-call*.c.cil.c
+  where I found the strings "bitvector" and "unreach-call" in the JSON file:
+                                   ========== This is the string
+    "better_right": {              v
+        "../../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i": {
+            "category": "unreach-call",
+            "left_status": "ERROR (42)",
+            "left_status_value": 2,
+            "options": "--32",              <======= This is the option for the shell script
+            "properties": "unreach-call",           <======= This is the string
+            "right_status": "true",
+            "right_status_value": 1
+        },
+
+  I should thus call the shell script:
+    /home/marek/root/SV-COMP-2018/BUG_FIXING/cbmc-sv-comp-2017-pr-rebase
+  with these options
+    ./cbmc-sv-comp-2017-pr-rebase --graphml-witness witness.graphml ${options} --propertyfile ${propertyfile} ${benchmark}
+  where
+    ${options}=--32                                                                         (this was taken from the JSON file, see above)
+    ${propertyfile}=../sv-benchmarks/c/ReachSafety.prp                                      (this was obtained from the result of the grep command)
+    ${benchmark}=../sv-benchmarks/c/eca-rers2012/Problem01_label00_true-unreach-call.c      (this was taken from the JSON file, see above)
+
+"""
+
+
+def _install_cbmc(use_old_cbmc):
+    repo_dir = _get_cbmc_old_repo_dir() if use_old_cbmc else _get_cbmc_new_repo_dir()
+    cbmc_binary = _get_cbmc_old_binary() if use_old_cbmc else _get_cbmc_new_binary()
+    cbmc_installed_binary = _get_installed_cbmc_old_binary() if use_old_cbmc else _get_installed_cbmc_new_binary()
+    if os.path.isfile(cbmc_installed_binary):
+        os.remove(cbmc_installed_binary)
+    old_cwd = os.getcwd()
+    os.chdir(repo_dir)
+    command = "make -C src"
+    print("EXECUTING: IN[" + repo_dir + "]: " + command)
+    retval = os.system(command)
+    os.chdir(old_cwd)
+    if retval != 0:
+        print("ERROR: execution of the last shell command has FAILED.")
+        return retval
+    shutil.copy(cbmc_binary, cbmc_installed_binary)
+    return 0
+
+
+def _load_diff_record_of_benchmark(benchmark_pathname):
+    with open(_get_results_diff_json_pathname(), "r") as ifile:
+        diff = json.loads(ifile.read())
+    assert "better_right" in diff
+    record_name = os.path.relpath(benchmark_pathname, _get_benchmarks_root_dir())
+    assert record_name in diff["better_right"]
+    record = diff["better_right"][record_name]
+    return record
+
+
+def _get_property_file(benchmark_pathname, raw_benchmark_category):
+    benchmark_dirname = os.path.dirname(os.path.relpath(benchmark_pathname, _get_benchmarks_root_dir()))
+    benchmark_category = raw_benchmark_category if raw_benchmark_category != "valid-memtrack" else "valid-memsafety"
+    for pathname in [os.path.abspath(os.path.join(_get_benchmarks_root_dir(), fname))
+                     for fname in os.listdir(_get_benchmarks_root_dir())
+                     if os.path.splitext(fname)[1] == ".set"]:
+        with open(pathname, "r") as ifile:
+            content = ifile.read()
+            if re.findall("^" + benchmark_dirname + "/.*" + benchmark_category, content, re.MULTILINE):
+                property_file_pathname = os.path.splitext(pathname)[0] + ".prp"
+                if os.path.isfile(property_file_pathname):
+                    return property_file_pathname
+                property_file_pathname_ex = os.path.join(
+                    os.path.dirname(pathname),
+                    os.path.basename(pathname)[:os.path.basename(pathname).find("-")] + ".prp"
+                    )
+                if os.path.isfile(property_file_pathname_ex):
+                    return property_file_pathname_ex
+                print("ERROR: the property file " + property_file_pathname + " of the found corresponding file " +
+                      pathname + " does not exist. Skipping the file.")
+                print("ERROR: the property file " + property_file_pathname_ex + " of the found corresponding file " +
+                      pathname + " does not exist. Skipping the file.")
+    print("ERROR: cannot find any property file (*.set) for the benchmark " + benchmark_pathname +
+          " and the category " + benchmark_category)
+    assert False
+
+
+def _evaluate_benchmark(benchmark_pathname, use_old_cbmc):
+    assert isinstance(benchmark_pathname, str)
+    assert isinstance(use_old_cbmc, bool)
+
+    retval = _install_cbmc(use_old_cbmc)
+    if retval != 0:
+        return retval
+    record = _load_diff_record_of_benchmark(benchmark_pathname)
+    cbmc_script = _get_cbmc_old_shell_script() if use_old_cbmc else _get_cbmc_new_shell_script()
+    property_file = _get_property_file(benchmark_pathname, record["category"])
+
+    command = (
+        cbmc_script + " " +
+        "--graphml-witness witness witness.graphml " +
+        "--propertyfile " + property_file + " " +
+        record["options"] + " " +
+        benchmark_pathname
+    )
+    print("EXECUTING: IN[" + os.getcwd() + "]: " + command)
+    return os.system(command)
+
+
+def _main(cmdline):
+    retval = 0
+    try:
+        retval = _evaluate_benchmark(cmdline.benchmark, cmdline.old_cbmc)
+    except:
+        print("ERROR: An exception was raised:")
+        traceback.print_exc(file=sys.stdout)
+        retval = 2
+    finally:
+        return retval
+
+
+if __name__ == "__main__":
+    exit(_main(_build_command_line_interface()))

scripts/SV-COMP/mkxmlparts.py

@@ -0,0 +1,50 @@
+import os
+import shutil
+
+
+def get_num_parts():
+    return 23
+
+
+def get_source_file():
+    return os.path.abspath("cbmc.xml")
+
+
+def get_destination_file(idx):
+    src_file = get_source_file()
+    dir_name = os.path.dirname(src_file)
+    file_name = os.path.basename(src_file)
+    plain_file_name, extension = os.path.splitext(file_name)
+    return os.path.join(dir_name, plain_file_name + str(idx) + extension)
+
+
+def update_part_file(idx):
+    assert idx > 0
+    with open(get_destination_file(idx), "r") as ifile:
+        content = ifile.read()
+    first_task_idx = content.find("<tasks name=\"")
+    assert first_task_idx > 0
+
+    my_task_idx = 0
+    for i in range(idx):
+        my_task_idx = content.find("<tasks name=\"", my_task_idx + len("<tasks name=\""))
+        assert my_task_idx > 0
+    my_task_end_idx = content.find("</tasks>", my_task_idx)
+    assert my_task_end_idx > my_task_idx
+    my_task_end_idx += len("</tasks>")
+
+    tasks_end_idx = content.rfind("</benchmark>")
+    assert tasks_end_idx > my_task_end_idx
+
+    with open(get_destination_file(idx), "w") as ofile:
+        ofile.write(content[:first_task_idx] + content[my_task_idx:my_task_end_idx] + "\n\n" + content[tasks_end_idx:])
+
+
+def _main():
+    for i in range(1, get_num_parts() + 1):
+        shutil.copy(get_source_file(), get_destination_file(i))
+        update_part_file(i)
+
+
+if __name__ == "__main__":
+    exit(_main())

scripts/SV-COMP/results_download.py

@@ -0,0 +1,40 @@
+import os
+
+
+for name, ip in [
+        ("sv-comp-cbmc-incremental-ele-part1",          "35.195.26.50"),
+        ("sv-comp-cbmc-incremental-ele-part2",          "35.195.8.91"),
+        ("sv-comp-cbmc-incremental-part1",              "35.195.116.95"),
+        ("sv-comp-cbmc-incremental-part2",              "104.199.93.208"),
+        ("sv-comp-cbmc-incremental-rebase-ele-part1",   "35.189.240.44"),
+        ("sv-comp-cbmc-incremental-rebase-ele-part2",   "104.155.32.99"),
+        ("sv-comp-cbmc-incremental-rebase-part1",       "35.187.83.211"),
+        ("sv-comp-cbmc-incremental-rebase-part2",       "104.199.79.254"),
+        ("sv-comp-cbmc-part1",                          "35.195.222.120"),
+        ("sv-comp-cbmc-part2",                          "192.158.29.5"),
+        ("sv-comp-cbmc-sv-comp-2017-pr-part1",          "35.195.150.6"),
+        ("sv-comp-cbmc-sv-comp-2017-pr-part2",          "35.195.99.239"),
+        ("sv-comp-cbmc-sv-comp-2017-pr-rebase-part1",   "104.199.17.173"),
+        ("sv-comp-cbmc-sv-comp-2017-pr-rebase-part2",   "35.195.208.163"),
+        ("sv-comp-cbmc-symex-part1",                    "35.195.185.16"),
+        ("sv-comp-cbmc-symex-part2",                    "35.195.42.83")
+        ]:
+    user_name = "marek_trtik"
+    dst_dir = os.path.join(
+        "RESULTS",
+        "NOW",
+        name[len("sv-comp-"):min(name.rfind("-ele") if "-ele" in name else len(name),
+                                 name.rfind("-part") if "-part" in name else len(name))],
+        "results"
+        )
+    os.makedirs(dst_dir, exist_ok=True)
+    command_prefix = "scp " + user_name + "@" + ip + ":" + "~/evaluation-root/results/*."
+    command_suffix = " " + dst_dir
+    print("Retrieving results for " + name + " from " + ip)
+    # print("Executing: " + command)
+    retval = os.system(command_prefix + "bz2" + command_suffix)
+    if retval != 0:
+        retval = os.system(command_prefix + "xml" + command_suffix)
+        if retval != 0:
+            print("    ERROR: The download has failed!")
+