diff --git a/conf/svcomp26/level00.json b/conf/svcomp26/level00.json new file mode 100644 index 0000000000..23c4582663 --- /dev/null +++ b/conf/svcomp26/level00.json @@ -0,0 +1,108 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false + }, + "float": { + "interval": false, + "evaluate_math_functions": false + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "reduceAnalyses", + "mallocWrappers", + "noRecursiveIntervals", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/svcomp26/level01.json b/conf/svcomp26/level01.json new file mode 100644 index 0000000000..b9f447ffea --- /dev/null +++ b/conf/svcomp26/level01.json @@ -0,0 +1,114 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "reduceAnalyses", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "yaml": { + "enabled": true, + "sv-comp-true-only": false, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/svcomp26/level02.json b/conf/svcomp26/level02.json new file mode 100644 index 0000000000..e5d1824a00 --- /dev/null +++ b/conf/svcomp26/level02.json @@ -0,0 +1,129 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": true, + "congruence": true, + "bitfield":true, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless", + "affeq", + "apron" + ], + "apron": { + "domain": "octagon" + }, + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + }, + "structs": { + "domain": "sets" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "reduceAnalyses", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "solvers": { + "td3": { + "widen_gas": 30, + "side_widen_gas": 30 + } + }, + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/svcomp26/level03.json b/conf/svcomp26/level03.json new file mode 100644 index 0000000000..3963328e0c --- /dev/null +++ b/conf/svcomp26/level03.json @@ -0,0 +1,128 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": true, + "congruence": true, + "bitfield":true, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless", + "branchSet" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag", + "branchSet" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + }, + "structs": { + "domain": "sets" + } + + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "reduceAnalyses", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "solvers": { + "td3": { + "narrow-globs": { + "enabled": true + } + } + }, + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/svcomp26/level04.json b/conf/svcomp26/level04.json new file mode 100644 index 0000000000..46e9ffe8d0 --- /dev/null +++ b/conf/svcomp26/level04.json @@ -0,0 +1,123 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "congruence": true, + "bitfield":true, + "enums": true, + "interval": true, + "interval_threshold_widening": true + + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag", + "base" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "unroll", + "unrolling-factor": 16 + }, + "structs": { + "domain": "sets" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "reduceAnalyses", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true, + "unrolling-factor": 4 + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/svcomp26/seq.txt b/conf/svcomp26/seq.txt new file mode 100644 index 0000000000..e55c676415 --- /dev/null +++ b/conf/svcomp26/seq.txt @@ -0,0 +1,13 @@ +# Portfolio Configuration Sequence +# paths are relative to analyzer base directory +# +# minimalist run, basically only constants/def_exc +--conf conf/svcomp26/level00.json +# standard run based on svcomp 25 settings +--conf conf/svcomp26/level01.json +# apron/affeq run with enums,congruence, bitfield and sets for structs, sporting (side_)widen_gas 30 +--conf conf/svcomp26/level02.json +# branchset-pathsensitive run +--conf conf/svcomp26/level03.json +# base-pathsensitive run +--conf conf/svcomp26/level04.json \ No newline at end of file diff --git a/scripts/sv-comp/goblint_runner.py b/scripts/sv-comp/goblint_runner.py new file mode 100755 index 0000000000..d5aae51cd4 --- /dev/null +++ b/scripts/sv-comp/goblint_runner.py @@ -0,0 +1,102 @@ +#!/usr/bin/env python3 +import argparse +from dataclasses import dataclass + +import subprocess +from os import path +import logging + +class GoblintRunner: + + def __init__(self, logger): + self.logger = logger + self.current_path = path.dirname(__file__) + self.goblint_executable_path = path.join(self.current_path, "goblint") + if not path.exists(self.goblint_executable_path): + self.goblint_executable_path=path.join(self.current_path, "..", "..", "goblint") + if not path.exists(self.goblint_executable_path): + logger.error(f" Could not find goblint executable neither at {self.current_path} nor at {path.dirname(self.goblint_executable_path)}; did you build goblint with make?") + exit(1) + + parser = argparse.ArgumentParser( + description="""A facade in front of goblint to enable running a portfolio of configurations for SV-COMP. + All args apart from --portfolio-conf/-p are passed on to the actual goblint calls. + The portfolio config file is a plaintext file whose lines each consist of goblint parameters, in particular including + --conf followed by a path to a goblint config file (relative to the goblint base dir, or absolute). + Goblint is run with each parameterset in order of specification as long as goblint produces an unknown verdict or reaches the end of the list. + You may add comments to the portfolio config file by starting a line with #. + """ + ) + parser.add_argument("-p","--portfolio-conf", type=str, metavar="FILE",dest="portfolio", + help="a path to a portfolio configuration file (relative to goblint_runner.py)") + conf_args, self.other_args = parser.parse_known_args() + logger.debug(f"Portfolio-conf file: {conf_args.portfolio}") + logger.debug(f"Arguments passed on to goblint: {" ".join(self.other_args)}") + + self.configs = [] + if conf_args.portfolio: + if not path.exists(conf_args.portfolio): + logger.error(f" Could not find portfolio conf file at {conf_args.portfolio}") + exit(1) + with open(conf_args.portfolio, "r") as conflist_file: + self.configs = [c.strip() for c in conflist_file.readlines() if not c.strip().startswith("#")] + logger.info(f"Loaded goblint configs: {", ".join(self.configs)}") + + def run_with_config(self, config_str): + config_args = config_str.split(" ") + args = [*config_args] + self.other_args + self.logger.info(f"Config details: ./goblint {" ".join(args)}") + process = subprocess.Popen([self.goblint_executable_path, *args],stdout=subprocess.PIPE,stderr=subprocess.STDOUT) + continue_portfolio = False + for line in process.stdout: + decoded_line = line.decode("utf-8") + print(decoded_line, end="") + if decoded_line.startswith("SV-COMP result: "): + # remove "SV-COMP result: " prefix and any trailing whitespace + verdict = decoded_line[len("SV-COMP result: "):].strip() + if verdict == "unknown": + continue_portfolio = continue_portfolio or decoded_line.startswith("SV-COMP result: unknown") + process.wait() + return verdict,continue_portfolio + + def run_without_config(self): + subprocess.run([self.goblint_executable_path, *self.other_args]) + + def run(self): + if not self.configs: + self.run_without_config() + return + + for i, config in enumerate(self.configs): + logger.info(f"Starting config [{i}]") + verdict, go_on = self.run_with_config(config) + if not go_on: + logger.info(f"Stopping portfolio sequence with verdict [{verdict}] after config [{i}]") + break + if go_on: + logger.info("Reached end of portfolio sequence without definitive verdict.") + +class GoblintLikeFormatter(logging.Formatter): + LEVEL_NAMES = { + 'DEBUG': 'Debug', + 'INFO': 'Info', + 'WARNING': 'Warning', + 'ERROR': 'Error', + 'CRITICAL': 'Critical', + } + + def format(self, record): + levelname = self.LEVEL_NAMES.get(record.levelname, record.levelname) + record.levelname = levelname + return super().format(record) + +if __name__ == "__main__": + logger=logging.getLogger("goblintrunner") + logging.basicConfig(level=logging.INFO) + formatter=GoblintLikeFormatter('[%(levelname)s][%(name)s] %(message)s') + sh=logging.StreamHandler() + sh.setFormatter(formatter) + logger.addHandler(sh) + logger.propagate=False + goblint_runner = GoblintRunner(logger) + goblint_runner.run()