test(clam): add configuration for clam

Author: LinerSu

scripts/get_exper_res.py

@@ -17,6 +17,7 @@
     "--cex": "seahorn(cex).csv",
     "--cex --horn-bmc-solver=smt-y2": "seahorn(cex, smt-y2).csv",
     "klee": "klee.csv"}
+LLVM_VERSION=14
 
 
 def extra_to_filename(extra, suffix='.csv', prefix=''):
@@ -59,8 +60,8 @@ def make_new_cmake_conf():
         -DSMACK_ENABLE_NO_MEM_SPLIT={smack_enable_no_mem_split}'
     else:
         smack_args = ""
-    return f'cmake -DSEA_LINK=llvm-link-10 -DCMAKE_C_COMPILER=clang-10\
-    -DCMAKE_CXX_COMPILER=clang++-10 -DSEA_ENABLE_KLEE={use_klee} {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}\
     -DSEAHORN_ROOT={SEAHORN_ROOT} ../ -GNinja'
 

seahorn/CMakeLists.txt

@@ -344,6 +344,7 @@ separate_arguments(VERIFY_FLAGS)
 
 function(sea_add_unsat_test TARGET)
   sea_get_file_name(BC ${TARGET}.ir)
+  add_test(NAME "${TARGET}_clam_test" COMMAND ${VERIFY_CMD} --clam ${BC})
   add_test(NAME "${TARGET}_unsat_test" COMMAND ${VERIFY_CMD} ${VERIFY_FLAGS} --expect=unsat ${BC})
 endfunction()
 
@@ -395,6 +396,7 @@ configure_file(sea_crab_base.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)
+configure_file(clam_base.yaml clam.base.yaml @ONLY)
 
 # compilation recipes for aws-c-common library
 add_subdirectory(aws-c-common-stubs)
@@ -660,3 +662,4 @@ if(SEA_ENABLE_CRAB_JOBS)
   add_subdirectory(jobs_crab/byte_buf_advance_crab)
   add_subdirectory(jobs_crab/byte_buf_append_crab)
 endif()
+# add_subdirectory(jobs_unsafe/hash_table_mem_leak)

seahorn/clam_base.yaml

@@ -0,0 +1,43 @@
+clam_options:
+# CLANG
+#
+  '-g' : ''
+# Optimization level for seaopt  
+  '-O3': ''
+  save-temps: ''
+  temp-dir: /tmp/vc-crab
+#   
+# PREPROCESSING
+#
+  lower-unsigned-icmp : ''
+  llvm-peel-loops: '1'
+  devirt-functions: 'sea-dsa'
+  crab-name-values: false
+#  
+# ANALYSIS
+#
+  crab-dom : 'int'
+  crab-inter : ''
+  crab-inter-recursive-functions : true
+  crab-inter-exact-summary-reuse : false
+  crab-inter-max-summaries : '9999999'
+  crab-inter-entry-main : true
+  crab-track : 'mem'
+  crab-singleton-aliases : ''
+  crab-heap-analysis : 'cs-sea-dsa-types'
+  crab-narrowing-iterations: '1'
+  crab-widening-delay: '2'
+  crab-widening-jump-set: '0'
+  crab-preserve-invariants: false
+  crab-dom-param: "region.is_dereferenceable=true:object.reduce_everywhere=true"
+  crab-check: 'bounds'
+#
+# OUTPUT
+#
+# crab-sanity-checks : ''
+  crab-disable-warnings: ''
+# crab-print-invariants: false
+# crab-stats: ''
+  # crab-verbose: 5
+  # log: 'object-print:inter:object-forget:object-project:object-leq:object-meet:inter:object-join:object-copy:inter-group'
+  # ocrab: 'clam.crabir'

verify.py.in

@@ -61,6 +61,8 @@ def main(argv):
                               help='Path condition mode')
             argp.add_argument('--crab', action='store_true', default=False,
                               help='Using crab')
+            argp.add_argument('--clam', action='store_true', default=False,
+                              help='Using clam as front end')
             argp.add_argument('input_file', nargs=1)
             argp.add_argument('--dry-run', dest='dry_run',
                               action='store_true', default=False,
@@ -125,6 +127,13 @@ def main(argv):
                 cmd.append('--dry-run')
 
             cmd.append(args.command)
+            # Clam config
+            if args.clam:
+                cmd = ['/home/ljgy/Works/seahorn/clam/build/run/bin/clam-yaml.py']
+                clam_config = os.path.join(script_dir, 'seahorn', 
+                                          'clam.base.yaml')
+                cmd.extend(['-y', clam_config])
+
             cmd.extend(extra)
             cmd.append(input_file)