diff --git a/scripts/get_exper_res.py b/scripts/get_exper_res.py index 1a33163c..b3be3e69 100644 --- a/scripts/get_exper_res.py +++ b/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' diff --git a/seahorn/CMakeLists.txt b/seahorn/CMakeLists.txt index fafb5fdd..73f7666d 100644 --- a/seahorn/CMakeLists.txt +++ b/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) diff --git a/seahorn/clam_base.yaml b/seahorn/clam_base.yaml new file mode 100644 index 00000000..d6c7270d --- /dev/null +++ b/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' \ No newline at end of file diff --git a/verify.py.in b/verify.py.in index 3a61bc8f..1ea9dc8d 100755 --- a/verify.py.in +++ b/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)