Implemented portfolio solving

Added portfolio command line option. Implemented multi-threaded portfolio
solving.

Co-authored-by: Zvonimir <zvonimir@cs.utah.edu>
Co-authored-by: Joshua McMillan <jem@kornat.cs.utah.edu>

Author: 3 people

CMakeLists.txt

@@ -219,7 +219,7 @@ install(DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/share/smack
   USE_SOURCE_PERMISSIONS
   FILES_MATCHING PATTERN "*.py" PATTERN "*.h" PATTERN "*.c" PATTERN "Makefile"
     PATTERN "*.rs" PATTERN "*.f90" PATTERN "*.di" PATTERN "*.toml"
-    PATTERN "*.cpp" PATTERN "cassert"
+    PATTERN "*.cpp" PATTERN "cassert" PATTERN "*.yaml"
 )
 
 install(FILES

share/smack/default-portfolio.yaml

@@ -0,0 +1,17 @@
+---
+thread1:
+   verifier: "corral"
+
+thread2:
+   verifier: "corral"
+   verifier-options: "/bopt:proverOpt:O:smt.qi.eager_threshold=100"
+
+thread3:
+   verifier: "corral"
+   verifier-options: "/bopt:proverOpt:O:smt.arith.solver=2"
+
+thread4:
+   verifier: "corral"
+   verifier-options: "/bopt:proverOpt:O:smt.arith.solver=2
+                      /bopt:proverOpt:O:smt.qi.eager_threshold=100"
+

share/smack/frontend.py

@@ -3,7 +3,8 @@
 import re
 import json
 from .utils import temporary_file, try_command, temporary_directory,\
-    llvm_exact_bin
+    llvm_exact_bin, smack_root, smack_header_path, smack_headers,\
+    smack_lib
 from .versions import RUST_VERSION
 
 # Needed for cargo operations
@@ -68,24 +69,6 @@ def extra_libs():
     }
 
 
-def smack_root():
-    return os.path.dirname(os.path.dirname(os.path.abspath(sys.argv[0])))
-
-
-def smack_header_path():
-    return os.path.join(smack_root(), 'share', 'smack', 'include')
-
-
-def smack_headers(args):
-    paths = []
-    paths.append(smack_header_path())
-    return paths
-
-
-def smack_lib():
-    return os.path.join(smack_root(), 'share', 'smack', 'lib')
-
-
 def extern_entry_points(args, bcs):
     new_bcs = []
     for bc in bcs:

share/smack/top.py

@@ -6,10 +6,13 @@
 import subprocess
 import signal
 import functools
+import copy
+import multiprocessing
+import yaml
 from enum import Flag, auto
 from .svcomp.utils import verify_bpl_svcomp
 from .utils import temporary_file, try_command, remove_temp_files,\
-    llvm_exact_bin
+    llvm_exact_bin, smack_portfolio_path
 from .replay import replay_error_trace
 from .frontend import link_bc_files, frontends, languages, extra_libs
 from .errtrace import error_trace, json_output_str
@@ -536,6 +539,7 @@ def arguments():
         choices=[
             'boogie',
             'corral',
+            'portfolio',
             'symbooglix',
             'svcomp'],
         default='corral',
@@ -545,6 +549,14 @@ def arguments():
                                 choices=['z3', 'cvc4', "yices2"], default='z3',
                                 help='back-end SMT solver')
 
+    verifier_group.add_argument(
+        '--portfolio-config',
+        metavar='FILE',
+        default=smack_portfolio_path(),
+        action=FileAction,
+        type=str,
+        help='read portfolio configuration in YAML format from FILE')
+
     verifier_group.add_argument(
         '--unroll',
         metavar='N',
@@ -882,8 +894,8 @@ def verification_result(verifier_output, verifier):
                     line_no = int(boogie_af_msg.group(2))
                     with open(boogie_af_msg.group(1), 'r') as f:
                         assert_line = re.search(
-                                      attr_pat,
-                                      f.read().splitlines(True)[line_no - 1])
+                            attr_pat,
+                            f.read().splitlines(True)[line_no - 1])
                         if assert_line:
                             attr = assert_line.group(1)
         else:
@@ -901,6 +913,73 @@ def verification_result(verifier_output, verifier):
         return VResult.UNKNOWN
 
 
+def invoke_boogie(args):
+    command = ["boogie"]
+    command += [args.bpl_file]
+    command += ["/doModSetAnalysis"]
+    command += ["/useArrayTheory"]
+    command += ["/timeLimit:%s" % args.time_limit]
+    command += ["/errorLimit:%s" % args.max_violations]
+    if not args.modular:
+        command += ["/loopUnroll:%d" % args.unroll]
+    if args.solver == 'cvc4':
+        command += ["/proverOpt:SOLVER=cvc4"]
+    elif args.solver == 'yices2':
+        command += ["/proverOpt:SOLVER=Yices2"]
+    return command
+
+
+def invoke_corral(args):
+    command = ["corral"]
+    command += [args.bpl_file]
+    command += ["/tryCTrace", "/noTraceOnDisk", "/printDataValues:1"]
+    command += ["/k:%d" % args.context_bound]
+    command += ["/useProverEvaluate"]
+    command += ["/timeLimit:%s" % args.time_limit]
+    command += ["/cex:%s" % args.max_violations]
+    command += ["/maxStaticLoopBound:%d" % args.loop_limit]
+    command += ["/recursionBound:%d" % args.unroll]
+    if args.solver == 'cvc4':
+        command += ["/bopt:proverOpt:SOLVER=cvc4"]
+    elif args.solver == 'yices2':
+        command += ["/bopt:proverOpt:SOLVER=Yices2"]
+    return command
+
+
+def invoke_symbooglix(args):
+    command = ['symbooglix']
+    command += [args.bpl_file]
+    command += ["--file-logging=0"]
+    command += ["--entry-points=%s" % ",".join(args.entry_points)]
+    command += ["--timeout=%d" % args.time_limit]
+    command += ["--max-loop-depth=%d" % args.unroll]
+    return command
+
+
+def process_verifier_output(args, verifier_output):
+    verifier_output = transform_out(args, verifier_output)
+    result = verification_result(verifier_output, args.verifier)
+
+    if args.json_file:
+        with open(args.json_file, 'w') as f:
+            f.write(json_output_str(result, verifier_output, args.verifier))
+
+    if result in VResult.ERROR:
+        error = error_trace(verifier_output, args.verifier)
+
+        if args.error_file:
+            with open(args.error_file, 'w') as f:
+                f.write(error)
+
+        if not args.quiet:
+            print(error)
+
+        if args.replay:
+            replay_error_trace(verifier_output, args)
+    print(result.message(args))
+    return result.return_code()
+
+
 def verify_bpl(args):
     """Verify the Boogie source file with a back-end verifier."""
 
@@ -909,85 +988,140 @@ def verify_bpl(args):
         return
 
     elif args.verifier == 'boogie' or args.modular:
-        command = ["boogie"]
-        command += [args.bpl_file]
-        command += ["/doModSetAnalysis"]
-        command += ["/useArrayTheory"]
-        command += ["/timeLimit:%s" % args.time_limit]
-        command += ["/errorLimit:%s" % args.max_violations]
+        command = invoke_boogie(args)
         command += ["/proverOpt:O:smt.array.extensional=false"]
         command += ["/proverOpt:O:smt.qi.eager_threshold=100"]
         command += ["/proverOpt:O:smt.arith.solver=2"]
-        if not args.modular:
-            command += ["/loopUnroll:%d" % args.unroll]
-        if args.solver == 'cvc4':
-            command += ["/proverOpt:SOLVER=cvc4"]
-        elif args.solver == 'yices2':
-            command += ["/proverOpt:SOLVER=Yices2"]
 
     elif args.verifier == 'corral':
-        command = ["corral"]
-        command += [args.bpl_file]
-        command += ["/tryCTrace", "/noTraceOnDisk", "/printDataValues:1"]
-        command += ["/k:%d" % args.context_bound]
-        command += ["/useProverEvaluate"]
-        command += ["/timeLimit:%s" % args.time_limit]
-        command += ["/cex:%s" % args.max_violations]
-        command += ["/maxStaticLoopBound:%d" % args.loop_limit]
-        command += ["/recursionBound:%d" % args.unroll]
-        command += ["/bopt:proverOpt:O:smt.qi.eager_threshold=100"]
-        command += ["/bopt:proverOpt:O:smt.arith.solver=2"]
-        if args.solver == 'cvc4':
-            command += ["/bopt:proverOpt:SOLVER=cvc4"]
-        elif args.solver == 'yices2':
-            command += ["/bopt:proverOpt:SOLVER=Yices2"]
+        command = invoke_corral(args)
+        args.verifier_options += (
+            " /bopt:proverOpt:O:smt.qi.eager_threshold=100"
+            " /bopt:proverOpt:O:smt.arith.solver=2")
 
     elif args.verifier == 'symbooglix':
-        command = ['symbooglix']
-        command += [args.bpl_file]
-        command += ["--file-logging=0"]
-        command += ["--entry-points=%s" % ",".join(args.entry_points)]
-        command += ["--timeout=%d" % args.time_limit]
-        command += ["--max-loop-depth=%d" % args.unroll]
+        command = invoke_symbooglix(args)
 
     if args.verifier_options:
         command += args.verifier_options.split()
 
     verifier_output = try_command(command, timeout=args.time_limit)
-    verifier_output = transform_out(args, verifier_output)
-    result = verification_result(verifier_output, args.verifier)
+    return process_verifier_output(args, verifier_output)
 
-    if args.json_file:
-        with open(args.json_file, 'w') as f:
-            f.write(json_output_str(result, verifier_output, args.verifier))
 
-    if result in VResult.ERROR:
-        error = error_trace(verifier_output, args.verifier)
+def thread_verify_bpl(args, args_to_add):
 
-        if args.error_file:
-            with open(args.error_file, 'w') as f:
-                f.write(error)
+    if 'verifier' in args_to_add:
+        if args_to_add['verifier'] == 'portfolio':
+            raise RuntimeError(
+                "portfolio is not a valid verifier specification"
+                " within the portfolio configuration")
+        else:
+            print(
+                "Warning: SMACK is using argument verifier from"
+                " the chosen portfolio configuration")
+            args.verifier = args_to_add['verifier']
+    else:
+        raise RuntimeError(
+            "verifier is a required argument"
+            " in the portfolio configuration file")
+
+    if 'modular' in args_to_add:
+        if args.modular:
+            raise RuntimeError(
+                "argument modular specified in both"
+                " command line and portfolio configuration")
+        else:
+            print(
+                "Warning: SMACK is using argument modular from"
+                " the chosen portfolio configuration")
+            args.modular = args_to_add['modular']
+
+    if (args.verifier != 'boogie') and args.modular:
+        raise RuntimeError(
+            "Incompatible arguments modular"
+            " and non-boogie verifier were specified")
+
+    if 'verifier-options' in args_to_add:
+        if args.verifier_options:
+            raise RuntimeError(
+                "argument verifier-options specified in both"
+                " command line and portfolio configuration")
+        else:
+            print(
+                "Warning: SMACK is using argument verifier-"
+                "options from the chosen portfolio configuration")
+            args.verifier_options = args_to_add['verifier-options']
+
+    if 'solver' in args_to_add:
+        if args.solver != 'z3':  # better check than not default?
+            raise RuntimeError(
+                "argument solver specified in both command"
+                " line and portfolio configuration")
+        else:
+            print(
+                "Warning: SMACK is using argument solver from"
+                " the chosen portfolio configuration")
+            args.solver = args_to_add['solver']
 
-        if not args.quiet:
-            print(error)
+    if args.verifier == 'boogie' or args.modular:
+        command = invoke_boogie(args)
 
-        if args.replay:
-            replay_error_trace(verifier_output, args)
-    print(result.message(args))
-    return result.return_code()
+    elif args.verifier == 'corral':
+        command = invoke_corral(args)
+
+    elif args.verifier == 'symbooglix':
+        command = invoke_symbooglix(args)
+
+    if args.verifier_options:
+        command += args.verifier_options.split()
+
+    verifier_output = try_command(command, timeout=args.time_limit)
+    return args, verifier_output
+
+
+def verify_bpl_portfolio(args):
+
+    portfolio_config = yaml.load(open(args.portfolio_config, 'r'))
+    p = multiprocessing.Pool()
+    results = {}  # map of process -> thread name
+
+    for thread in list(portfolio_config.keys()):
+        async_result = p.apply_async(thread_verify_bpl,
+                                     args=(copy.deepcopy(args),
+                                     portfolio_config[thread]))
+        results[async_result] = thread
+
+    # TODO: revisit this loop to improve efficiency
+    while True:
+        for result in list(results.keys()):
+            if result.ready():
+                p.terminate()
+                args, verifier_output = result.get()
+                verifier_output = process_verifier_output(
+                    args, verifier_output)
+                thread_name = results[result]
+                print(f'SMACK portfolio {thread_name} terminated')
+                return verifier_output
 
 
 def clean_up_upon_sigterm(main):
     def handler(signum, frame):
+        remove_temp_files_lock.acquire()
         remove_temp_files()
+        remove_temp_files_lock.release()
         sys.exit(0)
+
     signal.signal(signal.SIGTERM, handler)
     return main
 
 
 @clean_up_upon_sigterm
 def main():
     try:
+        global remove_temp_files_lock
+        remove_temp_files_lock = multiprocessing.Lock()
+
         global args
         args = arguments()
 
@@ -1002,7 +1136,10 @@ def main():
             if not args.quiet:
                 print("SMACK generated %s" % args.bpl_file)
         else:
-            return_code = verify_bpl(args)
+            if args.verifier == 'portfolio':
+                return_code = verify_bpl_portfolio(args)
+            else:
+                return_code = verify_bpl(args)
             sys.exit(return_code)
 
     except KeyboardInterrupt: