feat(jobs): add more crab settings

Author: Yusen Su

CMakeLists.txt

@@ -14,7 +14,8 @@ option(SEA_LLVM_MEM_BUILTINS "Use LLVM builtins memcpy/memmove without memory sa
 
 
 option(SEA_ENABLE_FUZZ "Enable fuzzing" OFF)
-option(SEA_ENABLE_CRAB "Enable Seahorn using Clam/Crab" OFF)
+option(SEA_ENABLE_CRAB "Enable Seahorn using Crab" OFF)
+option(SEA_ENABLE_CLAM "Enable Seahorn using Clam" OFF)
 option(SEA_WITH_BLEEDING_EDGE "Enable bleeding edge proofs" OFF)
 
 option(SEA_ENABLE_KLEE "Enable klee" OFF)
@@ -58,6 +59,10 @@ set(SEA_PP "${SEAHORN_ROOT}/bin/seapp" CACHE STRING "Path to seapp binary")
 set(LLVMIR_OPT ${SEA_OPT})
 
 set(AWS_C_COMMON_ROOT ${CMAKE_CURRENT_SOURCE_DIR}/aws-c-common)
+set(AWS_C_COMPRESSION_ROOT ${CMAKE_CURRENT_SOURCE_DIR}/aws-c-compression)
+set(AWS_C_SDKUTILS_ROOT ${CMAKE_CURRENT_SOURCE_DIR}/aws-c-sdkutils)
+set(AWS_C_IO_ROOT ${CMAKE_CURRENT_SOURCE_DIR}/aws-c-io)
+set(AWS_C_CAL_ROOT ${CMAKE_CURRENT_SOURCE_DIR}/aws-c-cal)
 
 if(SEA_ENABLE_FUZZ)
   find_package(aws-c-common REQUIRED)
@@ -75,5 +80,9 @@ include_directories(BEFORE ${CMAKE_CURRENT_BINARY_DIR}/include)
 
 include_directories(seahorn/include)
 include_directories(aws-c-common/include)
+include_directories(aws-c-compression/include)
+include_directories(aws-c-sdkutils/include)
+include_directories(aws-c-io/include)
+include_directories(aws-c-cal/include)
 include_directories(${SEAHORN_ROOT}/include)
 add_subdirectory(seahorn)

scripts/get_exper_brunch_stat.py

@@ -17,7 +17,7 @@ def read_brunchstat_from_log(log_file_name):
     cur_test = None
     while line:
         # look for next test
-        new_test = re.search(BRUNCH_DICT["job_name"], line)
+        new_test = re.search("Testing: ", line)
         if new_test:
             new_test_data = defaultdict(lambda: 'n/a')
             span = new_test.span()
@@ -33,8 +33,7 @@ def read_brunchstat_from_log(log_file_name):
                 stat_num = stat[-1]
                 data[-1][stat_name] = stat_num
         line = log_file.readline()
-    if cur_test:
-        data[cur_test] = move_dict_items_to_lst(row_dict)
+
     log_file.close()
     return data
 
@@ -117,6 +116,30 @@ def write_brunchstat_into_csv(data, out_file):
             row = (job_data[k] for k, _ in metric_serlz)
             writer.writerow(row)
 
+
+# def read_timimg_results(result_dir):
+#     log_file = open(log_file_name, 'r')
+#     line = log_file.readline()
+#     data = defaultdict(list)
+#     row_dict = {}
+#     while line:
+#         if "************** ANALYSIS RESULTS ****************" in line:
+#             result_status = Status.SUCCESS
+#         if "** OS Error:" in line:
+#             result_status = Status.TIMEOUT
+#         if "BRUNCH_STAT" in line:
+#             parts = line.strip().split()
+#             name = parts[1]
+#             if name == "Clam":
+#                 number = float(parts[2])
+#                 if result_status == Status.CLAM_ERROR:
+#                     pairs.append([dirpath.strip().split('/')[1], "error"])
+#                 elif result_status == Status.TIMEOUT:
+#                     pairs.append([dirpath.strip().split('/')[1], "timeout"])
+#                 else:
+#                     pairs.append([dirpath.strip().split('/')[1], number])
+#     draw_results_table(pairs, result_dir)
+
 if __name__ == "__main__":
     parser = argparse.ArgumentParser(
         description='in and out files')
@@ -129,4 +152,4 @@ def write_brunchstat_into_csv(data, out_file):
         help="ouput csv filename")
     args = parser.parse_args()
     data = read_brunchstat_from_log(args.logfile)
-    write_brunchstat_into_csv(data, args.outfile)
+    write_brunchstat_into_csv(data, args.outfile)

scripts/get_exper_res.py

@@ -5,18 +5,18 @@
 import glob
 import subprocess
 import argparse
-from get_exper_brunch_stat import *
+from get_exper_brunch_stat import read_brunchstat_from_log, write_brunchstat_into_csv
 
-BUILDABSPATH = os.path.abspath('../exper/')
+BUILDABSPATH = os.path.abspath('../build/')
 DATAABSPATH = os.path.abspath('../') + "/data"
-SEAHORN_ROOT = '../../build-seahorn'  # Put your seahorn root dir here
+SEAHORN_ROOT = '/home/yusen/seawork/seahorn/build/run'  # Put your seahorn root dir here
 FILE_DICT = {
     "": "seahorn.csv",
     "--vac": "seahorn(vac).csv",
     "--horn-bmc-solver=smt-y2": "seahorn(smt-y2).csv",
     "--cex": "seahorn(cex).csv",
     "--cex --horn-bmc-solver=smt-y2": "seahorn(cex, smt-y2).csv",
-    "klee": "klee.csv", "symbiotic": "symbiotic.csv"}
+    "klee": "klee.csv", "symbiotic": "symbiotic.csv", "clam": "clam.csv"}
 LLVM_VERSION=14
 
 def extra_to_filename(extra, suffix='.csv', prefix=''):
@@ -52,7 +52,7 @@ def make_new_cmake_conf():
     use_klee = "ON" if args.klee else "OFF"
     use_symbiotic = "ON" if args.symbiotic else "OFF"
     use_bleeding_edge = "ON" if args.bleed_edge else "OFF"
-    use_crab = "ON" if "--crab" in extra else "OFF"
+    # use_crab = "ON" if "--crab" in extra else "OFF"
     if args.smack_parser:
         use_smack = "ON" if args.smack else "OFF"
         smack_enable_no_mem_split = "ON" if args.mem_no_split else "OFF"
@@ -62,7 +62,7 @@ def make_new_cmake_conf():
         smack_args = ""
     return f'cmake -DSEA_LINK=llvm-link-{LLVM_VERSION} -DCMAKE_C_COMPILER=clang-{LLVM_VERSION}\
     -DCMAKE_CXX_COMPILER=clang++-{LLVM_VERSION} -DSEA_ENABLE_KLEE={use_klee} {smack_args}\
-    -DSEA_WITH_BLEEDING_EDGE={use_bleeding_edge} -DSEA_ENABLE_CRAB={use_crab}\
+    -DSEA_WITH_BLEEDING_EDGE={use_bleeding_edge} -DSEA_ENABLE_CRAB=OFF\
     -DSEA_ENABLE_SYMBIOTIC={use_symbiotic} -DSEAHORN_ROOT={SEAHORN_ROOT} ../ -GNinja'
 
 
@@ -99,18 +99,6 @@ def collect_res_from_ctest(file_name):
     print("Done, find result csv file at: %s" % file_name)
 
 
-def extra_to_filename(extra, suffix='csv'):
-    '''extra: --a=b --c=d to filename: a.b.c.d.csv'''
-    if (len(extra) == 0):
-        return f'base.{suffix}'
-    parts = []
-    for flag in extra:
-        if flag.startswith('--'):
-            flag = flag[2:]
-        parts.extend(flag.split('='))
-    return f'{"_".join(parts)}.{suffix}'
-
-
 def run_ctest_for_seahorn():
     print("[SeaHorn] Start making SeaHorn results...")
     set_env = ''
@@ -120,7 +108,7 @@ def run_ctest_for_seahorn():
         set_env = f'env VERIFY_FLAGS=\"{verify_flags}\"'
     cmake_conf = make_new_cmake_conf()
     command_lst = ["rm -rf *", cmake_conf, "ninja",
-                   f'{set_env} ctest -j{os.cpu_count()} -D ExperimentalTest -R . --timeout {args.timeout}']
+                   f'{set_env} ctest -j 12 -D ExperimentalTest -R . --timeout {args.timeout}']
     make_build_path(extra)
     cddir = "cd " + BUILDABSPATH
     for strcmd in command_lst:
@@ -137,6 +125,22 @@ def run_ctest_for_seahorn():
     collect_stat_from_ctest_log(extra_to_filename(extra, suffix='.brunch.csv'),
                                 True if "--crab" in extra else False)
 
+def run_ctest_for_clam():
+    print("[Clam] Start making Clam results...")
+    cmake_conf = make_new_cmake_conf()
+    command_lst = ["rm -rf *", cmake_conf, "ninja",
+                   f'ctest -j{os.cpu_count()} -D ExperimentalTest -R smack_ --timeout 200']
+    make_build_path(["--clam"])
+    for strcmd in command_lst:
+        cddir += " ; " + strcmd
+    if args.debug:
+        print(f'[Command] {cddir}')
+    process = subprocess.Popen(
+        '/bin/bash',
+        stdin=subprocess.PIPE,
+        stdout=get_output_level())
+    _ = process.communicate(cddir.encode())
+    collect_res_from_ctest(FILE_DICT["klee"])
 
 def collect_stat_from_ctest_log(outfile, use_crab):
     test_tmpdir = os.path.join(BUILDABSPATH, 'Testing', 'Temporary')
@@ -176,8 +180,8 @@ def run_ctest_for_klee():
 def run_ctest_for_smack():
     cmake_conf = make_new_cmake_conf()
     command_lst = ["rm -rf *", cmake_conf, "ninja",
-                   f'ctest -j{os.cpu_count()} -D ExperimentalTest -R smack_ --timeout {args.timeout}']
-    print("Start making SMACK results...")
+                   f'ctest -j{os.cpu_count()} -D ExperimentalTest -R smack_ --timeout 200']
+    print("[SMACK] Start making SMACK results...")
     make_build_path(["--smack"])
     cddir = "cd " + BUILDABSPATH
     for strcmd in command_lst:
@@ -193,7 +197,6 @@ def run_ctest_for_smack():
     collect_res_from_ctest(extra_to_filename(
         [str(args.precise), str(args.checks), mem_split]))
 
-
 def run_ctest_for_symbiotic():
     cmake_conf = make_new_cmake_conf()
     command_lst = ["rm -rf *", cmake_conf, "ninja",
@@ -211,7 +214,6 @@ def run_ctest_for_symbiotic():
     _ = process.communicate(cddir.encode())
     collect_stat_from_ctest_log(FILE_DICT["symbiotic"])
 
-
 def main():
     os.makedirs(DATAABSPATH, exist_ok=True)
     os.makedirs(BUILDABSPATH, exist_ok=True)
@@ -223,6 +225,8 @@ def main():
         run_ctest_for_smack()
     if args.symbiotic:
         run_ctest_for_symbiotic()
+    if args.clam:
+        run_ctest_for_clam()
 
 
 if __name__ == "__main__":
@@ -232,6 +236,7 @@ def main():
     parser.add_argument('--seahorn', action='store_true', default=True)
     parser.add_argument('--klee', action='store_true', default=False)
     parser.add_argument('--symbiotic', action='store_true', default=False)
+    parser.add_argument('--clam', action='store_true', default=False)
     parser.add_argument('--bleed_edge', action='store_true', default=False)
     parser.add_argument('--debug', action='store_true', default=False)
     parser.add_argument('--timeout', type=int, default=2000,
@@ -262,4 +267,4 @@ def main():
         args.seahorn = False
     if args.symbiotic:
         args.seahorn = False
-    main()
+    main()

scripts/metrics.yaml

@@ -2,10 +2,12 @@ job_name: "job_name"
 Result: "result"
 bmc.circ_sz: "bmc_circuit_size"
 bmc.dag_sz: "bmc_dag_size"
-crab.isderef.not.solve: "crab.isderef.not.solve" # for crab
-crab.isderef.solve: "crab.isderef.solve" # for crab
+crab.opsem.isderef.not.solve: "opsem.isderef.not.solve" # for crab
+crab.opsem.isderef.solve: "opsem.isderef.solve" # for crab
 crab.pp.isderef.not.solve: "pp.isderef.not.solve"
 crab.pp.isderef.solve: "pp.isderef.solve"
+opsem.crab: "opsem_crab_time"
+seapp.crab: "pp_crab_time"
 BMC: "bmc_time"
 BMC.solve: "bmc_solve_time"
 Control dependence analysis: "cda_time"