Skip to content

Commit f56f689

Browse files
portfolio of parameters instead of only config files
1 parent 61a35ff commit f56f689

File tree

3 files changed

+21
-10
lines changed

3 files changed

+21
-10
lines changed

conf/svcomp26/level01.json

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,6 @@
7878
"enums",
7979
"congruence",
8080
"wideningThresholds",
81-
"loopUnrollHeuristic",
8281
"memsafetySpecification",
8382
"noOverflows",
8483
"termination",

conf/svcomp26/seq.txt

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,7 @@
1+
# Portfolio Configuration Sequence
2+
# paths are relative to analyzer base directory
3+
#
14
# standard run based on svcomp 25 settings
2-
svcomp26/level00.json
5+
--conf conf/svcomp26/level00.json -v
36
# next level proof of concept
4-
svcomp26/level01.json
7+
--conf conf/svcomp26/level01.json

goblint_runner.py

Lines changed: 16 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,9 @@ def __init__(self, logger):
1919
parser = argparse.ArgumentParser(
2020
description="""A facade in front of goblint to enable running a portfolio of configurations for SV-COMP.
2121
All args apart from --portfolio-conf/-p are passed on to the actual goblint calls.
22-
The portfolio config file is a plaintext file whose lines each consist of a path to a
23-
goblint config file (relative to the goblint conf dir).
24-
Goblint is run with each config in order until one produces a verdict true or reaches the end of the list.
22+
The portfolio config file is a plaintext file whose lines each consist of goblint parameters, in particular including
23+
--conf followed by a path to a goblint config file (relative to the goblint base dir, or absolute).
24+
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.
2525
You may add comments to the portfolio config file by starting a line with #.
2626
"""
2727
)
@@ -37,12 +37,21 @@ def __init__(self, logger):
3737
logger.error(f" Could not find portfolio conf file at {conf_args.portfolio}")
3838
exit(1)
3939
with open(conf_args.portfolio, "r") as conflist_file:
40-
self.configs = [path.join(self.current_path, "conf", c.strip())
41-
for c in conflist_file.readlines() if not c.strip().startswith("#")]
40+
self.configs = [c.strip() for c in conflist_file.readlines() if not c.strip().startswith("#")]
4241
logger.info(f"Loaded goblint configs: {", ".join(self.configs)}")
4342

44-
def run_with_config(self, config_path):
45-
args = ["--conf", config_path] + self.other_args
43+
def run_with_config(self, config_str):
44+
config_args = config_str.split(" ")
45+
# in config_args, replace any relative paths with absolute paths
46+
pathparameters=["--conf"] # add more if needed
47+
for i in range(len(config_args)):
48+
if config_args[i] in pathparameters and i + 1 < len(config_args):
49+
conf_path = config_args[i + 1]
50+
if not path.isabs(conf_path):
51+
abs_conf_path = path.join(self.current_path, conf_path)
52+
config_args[i + 1] = abs_conf_path
53+
54+
args = [*config_args] + self.other_args
4655
self.logger.info(f"Running next shot: ./goblint {" ".join(args)}")
4756
process = subprocess.Popen([self.goblint_executable_path, *args],stdout=subprocess.PIPE,stderr=subprocess.STDOUT)
4857
continue_portfolio = False

0 commit comments

Comments
 (0)