feat: config yamls and fix scripts

Author: Yusen Su

scripts/get_exper_brunch_stat.py

@@ -3,7 +3,7 @@
 import csv
 import argparse
 import yaml
-import glob
+import glob, os
 from collections import defaultdict
 
 METRICS_FILE = "metrics.yaml"
@@ -25,6 +25,8 @@ def read_brunchstat_from_log(log_file_name):
             # remove _unsat_test
             cur_test = test_name[:-12]
             new_test_data['job_name'] = cur_test
+            new_test_data['pp_loc'] = get_loc_info(cur_test, True)
+            new_test_data['opsem_loc'] = get_loc_info(cur_test, False)
             data.append(new_test_data)
         elif line.startswith("BRUNCH_STAT"):
             stat = line.split()
@@ -37,6 +39,27 @@ def read_brunchstat_from_log(log_file_name):
     log_file.close()
     return data
 
+def get_loc_info(file_name, is_pp):
+    # Directory where the files are located
+    directory_path = "/tmp/verify-c-common/"
+
+    ir_name = f"{file_name}.ir.peel.fat.pp.ms.bc" if is_pp else f"{file_name}.ir.peel.fat.pp.ms.crab.o.ul.cut.o.bc"
+
+    # Construct the full path to the file with its pattern
+    full_path = os.path.join(directory_path, ir_name)
+    
+    # Get the LOC of the file
+    LOC = 'n/a'
+    with open(full_path, 'r') as file:
+        lines = file.readlines()
+        start = False
+        for line in lines:
+            if start:
+                LOC += 1
+            if '@main' in line:
+                LOC = 0
+                start = True
+    return LOC
 
 def read_symbiotic_bruchstat_from_log(log_file_name, xml_file_dir, time_out):
     log_file = open(log_file_name, 'r')
@@ -115,6 +138,7 @@ def write_brunchstat_into_csv(data, out_file):
         for job_data in data:
             row = (job_data[k] for k, _ in metric_serlz)
             writer.writerow(row)
+    print(f'[Statistics] Please find stat csv file at {out_file}')
 
 
 # def read_timimg_results(result_dir):

scripts/get_exper_res.py

@@ -5,8 +5,7 @@
 import glob
 import subprocess
 import argparse
-from get_exper_brunch_stat import read_brunchstat_from_log, write_brunchstat_into_csv
-
+from get_exper_brunch_stat import *
 BUILDABSPATH = os.path.abspath('../build/')
 DATAABSPATH = os.path.abspath('../') + "/data"
 SEAHORN_ROOT = '/home/yusen/seawork/seahorn/build/run'  # Put your seahorn root dir here
@@ -62,7 +61,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=OFF\
+    -DSEA_WITH_BLEEDING_EDGE={use_bleeding_edge} -DSEA_ENABLE_CRAB=ON\
     -DSEA_ENABLE_SYMBIOTIC={use_symbiotic} -DSEAHORN_ROOT={SEAHORN_ROOT} ../ -GNinja'
 
 
@@ -96,7 +95,7 @@ def collect_res_from_ctest(file_name):
     read_data_from_xml(res_data)
     write_data_into_csv(
         "{dir}/{file}".format(dir="../data", file=file_name), res_data)
-    print("Done, find result csv file at: %s" % file_name)
+    print(f'[Results] Please find result csv file at: {os.path.abspath("../data")}')
 
 
 def run_ctest_for_seahorn():
@@ -108,7 +107,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 12 -D ExperimentalTest -R . --timeout {args.timeout}']
+                   f'{set_env} ctest -j 1 -D ExperimentalTest -R . --timeout {args.timeout}']
     make_build_path(extra)
     cddir = "cd " + BUILDABSPATH
     for strcmd in command_lst:

scripts/metrics.yaml

@@ -1,12 +1,16 @@
 job_name: "job_name"
 Result: "result"
+pp_loc: "pp_loc"
+opsem_loc: "opsem_loc"
 bmc.circ_sz: "bmc_circuit_size"
 bmc.dag_sz: "bmc_dag_size"
 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"
+opsem.crab.solve: "opsem_crab_solve_time"
+pp.crab.solve: "pp_crab_solve_time"
 seapp.crab: "pp_crab_time"
 BMC: "bmc_time"
 BMC.solve: "bmc_solve_time"

seahorn/CMakeLists.txt

@@ -438,8 +438,12 @@ add_definitions(
   )
 
 configure_file(include/config.h.in ${PROJECT_BINARY_DIR}/include/config.h)
-configure_file(sea.yaml sea.yaml @ONLY)
-configure_file(sea_crab_base.yaml sea.crab.yaml @ONLY)
+if(SEA_ENABLE_CRAB)
+  configure_file(sea_crab_base.yaml sea.yaml @ONLY)
+else()
+  configure_file(sea.yaml sea.yaml @ONLY)
+endif()
+configure_file(sea_crab.yaml sea.crab.yaml @ONLY)
 configure_file(sea_cex_base.yaml sea.cex.yaml @ONLY)
 configure_file(sea_vac.yaml sea.vac.yaml @ONLY)
 configure_file(sea_pcond.yaml sea.pcond.yaml @ONLY)

seahorn/include/bounds.h

@@ -40,6 +40,5 @@ size_t fuzz_max_array_list_item_size(void);
  */
 size_t fuzz_max_array_list_len(void);
 
-size_t crab_max_array_size(void);
 
 SEAHORN_EXTERN_C_END

seahorn/lib/bounds.c

@@ -8,5 +8,4 @@ size_t sea_max_array_list_item_size(void) { return MAX_ITEM_SIZE; }
 size_t sea_max_array_list_len(void) { return MAX_INITIAL_ITEM_ALLOCATION; }
 size_t fuzz_max_array_list_len(void) { return MAX_INITIAL_ITEM_ALLOCATION_FUZZ; }
 size_t fuzz_max_array_list_item_size(void) { return MAX_ITEM_SIZE_FUZZ; }
-size_t sea_max_table_size(void) { return MAX_TABLE_SIZE; }
-size_t crab_max_array_size(void) { return MAX_ARRAY_SIZE; }
+size_t sea_max_table_size(void) { return MAX_TABLE_SIZE; }

seahorn/sea.yaml

@@ -0,0 +1 @@
+sea_base.yaml

seahorn/sea.yaml

@@ -11,7 +11,7 @@ verify_options:
   externalize-addr-taken-functions: ''
   no-kill-vaarg: ''
   with-arith-overflow: true
-  horn-unify-assumes: true
+  horn-unify-assumes: false
   horn-gsa: ''
 # do not instrument library functions with memory assertions 
   no-fat-fns: 'bcmp,memcpy,assert_bytes_match,ensure_linked_list_is_allocated,sea_aws_linked_list_is_valid'
@@ -23,9 +23,9 @@ verify_options:
   bmc: opsem
   horn-vcgen-use-ite: ''
 # ignore control flow
-  horn-vcgen-only-dataflow: true
+  horn-vcgen-only-dataflow: false
 # reduce by data dependence
-  horn-bmc-coi: true
+  horn-bmc-coi: false
 # static allocator supports symbolic allocation size
   sea-opsem-allocator: static
 # stack allocation from a symbolic starting point
@@ -43,4 +43,5 @@ verify_options:
   temp-dir: /tmp/verify-c-common
 # time and result stats
   horn-stats: true
-  ignore-define-verifier-fns: ''
+  # seapp-peel-loops: 1
+  ignore-define-verifier-fns: ''

seahorn/sea_base.yaml

@@ -7,7 +7,7 @@
 #
 verify_options:
 # Optimization lelel. Lower to O1 for clearer counterexamples
-  '-O1': ''
+  '-O3': ''
 # 
 # PREPROCESSING
 #
@@ -38,7 +38,7 @@ verify_options:
 # stack allocation from a symbolic starting point
   horn-explicit-sp0: false
 # lambdas for memory
-  horn-bv2-lambdas: true
+  horn-bv2-lambdas: ''
 # use z3 simplifier during vcgen
   horn-bv2-simplify: true
 # wide memory manager to track pointer sizes

seahorn/sea_cex_base.yaml

@@ -0,0 +1,18 @@
+verify_options:
+# Use crab infer bounds / range (before loop unrolling)
+  seapp-crab-lower-is-deref: true
+  seapp-crab-dom: 'zones'
+  seapp-crab-stats: true
+  seapp-crab-disable-warning: true
+  seapp-crab-obj-reduction: 'OPT'
+# Use crab infer bounds(after loop unrolling)
+  horn-bv2-crab-check-is-deref: ''
+  horn-bmc-crab-dom: 'zones'
+  horn-bv2-crab-obj-reduction: 'OPT'
+  # log: 'opsem-crab'
+  # log: 'opsem-crab-ir'
+  crab-disable-warning: true
+# Statistics
+  # crab-show-stats: ''
+  # horn-bv2-crab-stats: ''
+  # log: 'opsem-crab-ir:opsem-crab:seapp-crab-ir:seapp-crab'

seahorn/sea_crab.yaml

@@ -1,30 +1,48 @@
 verify_options:
+# Optimization level.
+  '-O3': ''
+# 
+# PREPROCESSING
+#
+  inline: ''
+  enable-loop-idiom: ''
+  enable-indvar: ''
+  no-lower-gv-init-struct: ''
+  externalize-addr-taken-functions: ''
+  no-kill-vaarg: ''
+  with-arith-overflow: true
+  # disable program transformation to single assume
   horn-unify-assumes: false
+# do not instrument library functions with memory assertions
+  no-fat-fns: 'bcmp,memcpy,assert_bytes_match,ensure_linked_list_is_allocated,sea_aws_linked_list_is_valid'
   horn-gsa: false
+# context-sensitive type-aware alias analysis 
+  dsa: sea-cs-t
+# weak support for function pointers. sea-dsa is better but less stable
+  devirt-functions: 'types'
+# bit-precise memory-precise operational semantics
+  bmc: opsem
+  horn-vcgen-use-ite: ''
 # ignore control flow
   horn-vcgen-only-dataflow: false
 # reduce by data dependence
   horn-bmc-coi: false
-# Use crab solve sea.is_deref
-  horn-bv2-crab-check-is-deref: ''
-# reduce used by object domain
-  # horn-bv2-crab-reduce: ''
-# loop peeling
-  seapp-peel-loops: 1
-# Use crab infer bounds / range (after loop unrolling)
-  # horn-bv2-crab-rng: ''
-  horn-bmc-crab-dom: 'zones'
-  horn-bv2-crab-obj-reduction: 'OPT'
-  # horn-bv2-crab-stats: ''
-  # log: 'opsem-crab'
-  # log: 'opsem-crab-ir'
-  crab-disable-warning: true
-# Statistics
-  # horn-bv2-crab-stats: ''
-# Use crab infer bounds / range (before loop unrolling)
-  seapp-crab-lower-is-deref: true
-  seapp-crab-dom: 'zones'
-  seapp-crab-stats: true
-  seapp-crab-disable-warning: true
-  seapp-crab-obj-reduction: 'OPT'
-  # log: 'opsem-crab-ir:opsem-crab:seapp-crab-ir:seapp-crab'
+# static allocator supports symbolic allocation size
+  sea-opsem-allocator: static
+# stack allocation from a symbolic starting point
+  horn-explicit-sp0: false
+# lambdas for memory
+  horn-bv2-lambdas: ''
+# use z3 simplifier during vcgen
+  horn-bv2-simplify: true
+# wide memory manager to track pointer sizes
+  horn-bv2-extra-widemem: ''
+# intermediate results in human readable form for debugging
+  '-S': ''
+# keep intermediate results for debugging 
+  keep-temps: ''
+  temp-dir: /tmp/verify-c-common
+# time and result stats
+  horn-stats: true
+# ignore converting function with prefix sea_nd to nd function
+  ignore-define-verifier-fns: ''