From 36c2600b91da7279d5a6892babe96c292415768d Mon Sep 17 00:00:00 2001 From: healthypunk Date: Tue, 14 Mar 2023 18:26:01 +0200 Subject: [PATCH 01/26] Split the time and values in output file --- gobexec/output/html/templates/matrix.jinja | 24 ++++++++-------------- gobexec/output/html/templates/multi.jinja | 14 ++++++++++++- test.py | 14 ++++--------- update_bench_traces.py | 0 4 files changed, 26 insertions(+), 26 deletions(-) create mode 100644 update_bench_traces.py diff --git a/gobexec/output/html/templates/matrix.jinja b/gobexec/output/html/templates/matrix.jinja index 1be603b..4adad17 100644 --- a/gobexec/output/html/templates/matrix.jinja +++ b/gobexec/output/html/templates/matrix.jinja @@ -1,13 +1,14 @@ {% set result = this %}

{{ this.matrix.name }}

+ {% for tool in result.tools %} - + {% endfor %} @@ -21,21 +22,14 @@ {% for benchmark_result in benchmark_results.results %} {% if benchmark_result.done() %} - {% if benchmark_result.result().result.kind == ResultKind.SUCCESS %} - + - {% else %} - + {% endif %} {% endfor %} diff --git a/gobexec/output/html/templates/multi.jinja b/gobexec/output/html/templates/multi.jinja index 9d09830..b2bfc86 100644 --- a/gobexec/output/html/templates/multi.jinja +++ b/gobexec/output/html/templates/multi.jinja @@ -1,3 +1,15 @@ {% for result in this.results %} -{{ result|template }} + {% if result.kind == ResultKind.SUCCESS %} + {% endfor %} \ No newline at end of file diff --git a/test.py b/test.py index be48d75..b7d2659 100644 --- a/test.py +++ b/test.py @@ -20,8 +20,8 @@ def index_tool_factory(name, args): goblint = GoblintTool( name=name, - program="/home/simmo/dev/goblint/sv-comp/goblint/goblint", - args=["--conf", "/home/simmo/dev/goblint/sv-comp/goblint/conf/traces-rel-toy.json", "--enable", "dbg.debug"] + args, + program="../analyzer/goblint", + args=["--conf", "../analyzer/conf/traces-rel-toy.json", "--enable", "dbg.debug"] + args, # args=["--conf", "/home/simmo/dev/goblint/sv-comp/goblint/conf/traces-rel.json", "--enable", "dbg.debug"], ) assert_summary_extractor = AssertSummaryExtractor(assert_counter) @@ -29,18 +29,12 @@ def index_tool_factory(name, args): goblint, TimeResult, assert_summary_extractor, - # AssertSummaryExtractor(), + #AssertSummaryExtractor(), # RaceSummary primary=assert_summary_extractor ) -duet = DuetTool( - program="/home/simmo/Desktop/duet/duet/duet.exe", - args=["-coarsen", "-inline", "-domain", "oct"], - assert_counter=assert_counter -) -matrix = txtindex.load(Path("/home/simmo/dev/goblint/sv-comp/goblint-bench/index/traces-rel-toy.txt"), index_tool_factory) +matrix = txtindex.load(Path("../bench/index/traces-rel-toy.txt"), index_tool_factory) # matrix = txtindex.load(Path("/home/simmo/dev/goblint/sv-comp/goblint-bench/index/traces-relational-watts.txt"), goblint) -matrix.tools.append(duet) # matrix.tools.append(assert_counter) matrix.tools.insert(0, assert_counter) diff --git a/update_bench_traces.py b/update_bench_traces.py new file mode 100644 index 0000000..e69de29 From e1fad6458ef80d2b25a126c08fdbc796e5d9e8a7 Mon Sep 17 00:00:00 2001 From: healthypunk Date: Thu, 23 Mar 2023 18:11:10 +0200 Subject: [PATCH 02/26] Added template for line summary as well as extraction class and line summary class --- gobexec/goblint/extractor.py | 14 +++++++++++++- gobexec/goblint/result.py | 14 ++++++++++++++ gobexec/output/html/templates/linesummary.jinja | 5 +++++ 3 files changed, 32 insertions(+), 1 deletion(-) create mode 100644 gobexec/output/html/templates/linesummary.jinja diff --git a/gobexec/goblint/extractor.py b/gobexec/goblint/extractor.py index c76c690..ba2494b 100644 --- a/gobexec/goblint/extractor.py +++ b/gobexec/goblint/extractor.py @@ -3,7 +3,7 @@ from typing import Any, Optional from gobexec.goblint.bench.tools import AssertCount -from gobexec.goblint.result import AssertSummary +from gobexec.goblint.result import AssertSummary, LineSummary from gobexec.model.context import ExecutionContext, CompletedSubprocess from gobexec.model.tool import Tool from gobexec.model.tools import ResultExtractor @@ -26,3 +26,15 @@ async def extract(self, ec: ExecutionContext[Any], cp: CompletedSubprocess) -> A else: unreachable = None return AssertSummary(success, warning, error, unreachable) + + +# class LineSummaryExtractor(ResultExtractor[LineSummary]): +# line_counter: ... +# def __init__(self): +# ... +# +# async def extract(self, ec: ExecutionContext[Any], cp: CompletedSubprocess) -> LineSummary: +# stdout = cp.stdout.decode("utf-8") +# live = len(re.findall(r"/live:[ ]*([0-9]*)/", stdout)) +# dead = len(re.findall(r"/dead:[ ]*([0-9]*)/", stdout)) +# total = live + dead \ No newline at end of file diff --git a/gobexec/goblint/result.py b/gobexec/goblint/result.py index 60ceaec..8ebc47b 100644 --- a/gobexec/goblint/result.py +++ b/gobexec/goblint/result.py @@ -82,3 +82,17 @@ def template(self, env): @staticmethod async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'Rusage': return Rusage(cp.rusage) + +@dataclass(init=False) +class LineSummary(Result): + live: int + dead: int + total: int + + def __init__(self, live: int, dead: int, total: int): + self.live = live + self.dead = dead + self.total = total + + def template(self, env): + return env.get_template("linesummary.jinja") \ No newline at end of file diff --git a/gobexec/output/html/templates/linesummary.jinja b/gobexec/output/html/templates/linesummary.jinja new file mode 100644 index 0000000..8eae00e --- /dev/null +++ b/gobexec/output/html/templates/linesummary.jinja @@ -0,0 +1,5 @@ +{# TODO: add colouring to values #} + +{{this.live}} +{{this.dead}} +{{this.total}} From 8f31b0b0bb027acd01d78ed4129ac60a5ab7e2e8 Mon Sep 17 00:00:00 2001 From: evaldasp Date: Fri, 24 Mar 2023 19:56:41 +0200 Subject: [PATCH 03/26] Changed line summary extraction method --- gobexec/goblint/extractor.py | 14 +------------- gobexec/goblint/result.py | 10 +++++++++- 2 files changed, 10 insertions(+), 14 deletions(-) diff --git a/gobexec/goblint/extractor.py b/gobexec/goblint/extractor.py index ba2494b..6509ed0 100644 --- a/gobexec/goblint/extractor.py +++ b/gobexec/goblint/extractor.py @@ -25,16 +25,4 @@ async def extract(self, ec: ExecutionContext[Any], cp: CompletedSubprocess) -> A unreachable = total - (success + warning + error) else: unreachable = None - return AssertSummary(success, warning, error, unreachable) - - -# class LineSummaryExtractor(ResultExtractor[LineSummary]): -# line_counter: ... -# def __init__(self): -# ... -# -# async def extract(self, ec: ExecutionContext[Any], cp: CompletedSubprocess) -> LineSummary: -# stdout = cp.stdout.decode("utf-8") -# live = len(re.findall(r"/live:[ ]*([0-9]*)/", stdout)) -# dead = len(re.findall(r"/dead:[ ]*([0-9]*)/", stdout)) -# total = live + dead \ No newline at end of file + return AssertSummary(success, warning, error, unreachable) \ No newline at end of file diff --git a/gobexec/goblint/result.py b/gobexec/goblint/result.py index 8ebc47b..dcd87b3 100644 --- a/gobexec/goblint/result.py +++ b/gobexec/goblint/result.py @@ -95,4 +95,12 @@ def __init__(self, live: int, dead: int, total: int): self.total = total def template(self, env): - return env.get_template("linesummary.jinja") \ No newline at end of file + return env.get_template("linesummary.jinja") + + @staticmethod + async def extract(self, ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'LineSummary': + stdout = cp.stdout.decode("utf-8") + live = len(re.findall(r"/live:[ ]*([0-9]*)/", stdout)) + dead = len(re.findall(r"/dead:[ ]*([0-9]*)/", stdout)) + total = live + dead + return LineSummary(live, dead, total) \ No newline at end of file From 1bb6a9b72023f55397f7b189d99833f4ed69a3a4 Mon Sep 17 00:00:00 2001 From: healthypunk Date: Tue, 28 Mar 2023 02:32:49 +0300 Subject: [PATCH 04/26] Added PrivPrecTool class with corresponding result class --- gobexec/goblint/result.py | 2 +- gobexec/goblint/tool.py | 22 +++++++++++++++++++++- gobexec/model/result.py | 11 +++++++++++ 3 files changed, 33 insertions(+), 2 deletions(-) diff --git a/gobexec/goblint/result.py b/gobexec/goblint/result.py index dcd87b3..4ca0689 100644 --- a/gobexec/goblint/result.py +++ b/gobexec/goblint/result.py @@ -83,7 +83,7 @@ def template(self, env): async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'Rusage': return Rusage(cp.rusage) -@dataclass(init=False) +@dataclass(init=False)#TODO: check correctness class LineSummary(Result): live: int dead: int diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index bc676ce..01eca67 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -13,15 +13,19 @@ class GoblintTool(Tool[Single, CompletedSubprocess]): name: str program: str args: List[str] + dump: bool + def __init__(self, name: str = "Goblint", program: str = "goblint", - args: List[str] = None + args: List[str] = None, + dump: bool = False ) -> None: self.name = name self.program = program self.args = args if args else [] + self.dump = dump # def run(self, benchmark: Single) -> str: # bench = Path("/home/simmo/dev/goblint/sv-comp/goblint-bench") @@ -56,3 +60,19 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Co out_file.seek(0) cp.stdout = out_file.read() # currently for extractors return cp + + +class PrivPrecTool([GoblintTool]):#TODO: check correctness + program: str + args: List[GoblintTool] + + + def __init__(self, + program: str = "./privPrecCompare", + args: List[GoblintTool] = None) -> None: + self.program = program + self.args = args if args else [] + + + async def run(self, ec: ExecutionContext[Single]) -> CompletedSubprocess: + path = ec.get_tool_data_path(self) diff --git a/gobexec/model/result.py b/gobexec/model/result.py index d670e9a..c544956 100644 --- a/gobexec/model/result.py +++ b/gobexec/model/result.py @@ -99,3 +99,14 @@ def kind(self): return self.primary.kind else: return ResultKind.DEFAULT + +@dataclass(init=False)#TODO: check correctness +class PrivPrecResult(Result): + result_path: str + + def __init__(self, result_path: str) -> None: + self.result_path = result_path + + def template(self, env: Environment) -> Template: + ...#TODO: Create template for privPrecCompare result + From 0f0ecc705ad5195e13cf171ccd524b8b6d29db2e Mon Sep 17 00:00:00 2001 From: evaldasp Date: Mon, 3 Apr 2023 17:13:48 +0300 Subject: [PATCH 05/26] Temporary fixes --- gobexec/goblint/result.py | 4 +++- gobexec/goblint/tool.py | 11 +++++------ 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/gobexec/goblint/result.py b/gobexec/goblint/result.py index 4ca0689..508feb8 100644 --- a/gobexec/goblint/result.py +++ b/gobexec/goblint/result.py @@ -12,6 +12,7 @@ class RaceSummary(Result): safe: int vulnerable: int unsafe: int + # total: int def __init__(self, @@ -68,6 +69,7 @@ def kind(self): return ResultKind.WARNING + @dataclass(init=False) class Rusage(Result): rusage: resource.struct_rusage @@ -103,4 +105,4 @@ async def extract(self, ec: ExecutionContext[Any], cp: CompletedSubprocess) -> ' live = len(re.findall(r"/live:[ ]*([0-9]*)/", stdout)) dead = len(re.findall(r"/dead:[ ]*([0-9]*)/", stdout)) total = live + dead - return LineSummary(live, dead, total) \ No newline at end of file + return LineSummary(live, dead, total) diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index 01eca67..9ad0778 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -4,6 +4,7 @@ from gobexec.model.benchmark import Single from gobexec.model.context import ExecutionContext, CompletedSubprocess +from gobexec.model.result import PrivPrecResult from gobexec.model.tool import Tool ARGS_TOOL_KEY = "goblint-args" @@ -15,7 +16,6 @@ class GoblintTool(Tool[Single, CompletedSubprocess]): args: List[str] dump: bool - def __init__(self, name: str = "Goblint", program: str = "goblint", @@ -62,10 +62,9 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Co return cp -class PrivPrecTool([GoblintTool]):#TODO: check correctness +class PrivPrecTool(Tool[Single, PrivPrecResult]): # TODO: check correctness program: str - args: List[GoblintTool] - + args: List[GoblintTool.] def __init__(self, program: str = "./privPrecCompare", @@ -73,6 +72,6 @@ def __init__(self, self.program = program self.args = args if args else [] - - async def run(self, ec: ExecutionContext[Single]) -> CompletedSubprocess: + async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> PrivPrecResult: path = ec.get_tool_data_path(self) + args = [self.program] + self.args \ No newline at end of file From c19f3409ed557d6c6fc7d85a967eedacf78d5a8b Mon Sep 17 00:00:00 2001 From: healthypunk Date: Thu, 6 Apr 2023 15:16:34 +0300 Subject: [PATCH 06/26] Temporary changes --- gobexec/goblint/tool.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index 9ad0778..88f0289 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -64,7 +64,7 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Co class PrivPrecTool(Tool[Single, PrivPrecResult]): # TODO: check correctness program: str - args: List[GoblintTool.] + args: List[GoblintTool] def __init__(self, program: str = "./privPrecCompare", @@ -74,4 +74,6 @@ def __init__(self, async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> PrivPrecResult: path = ec.get_tool_data_path(self) - args = [self.program] + self.args \ No newline at end of file + + args = [self.program] + [ ec.get_tool_data_path(tool) for tool in self.args] + cp = await ec.subprocess_exec() \ No newline at end of file From 1a3d89b956e7673abbaeddaba43efbeacacccfeb Mon Sep 17 00:00:00 2001 From: healthypunk Date: Fri, 7 Apr 2023 10:55:04 +0300 Subject: [PATCH 07/26] Added PrivPrecTool run function and added template for PrivPrecResult --- gobexec/goblint/tool.py | 11 ++++++++--- gobexec/output/html/templates/privprecresult.jinja | 0 2 files changed, 8 insertions(+), 3 deletions(-) create mode 100644 gobexec/output/html/templates/privprecresult.jinja diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index 88f0289..187346e 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -74,6 +74,11 @@ def __init__(self, async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> PrivPrecResult: path = ec.get_tool_data_path(self) - - args = [self.program] + [ ec.get_tool_data_path(tool) for tool in self.args] - cp = await ec.subprocess_exec() \ No newline at end of file + with(path / 'out.txt', 'w') as out_file: + args = [self.program] + [str(ec.get_tool_data_path(tool)) for tool in self.args] + cp = await ec.subprocess_exec( + args[0], + stdout = out_file, + stderr=asyncio.subprocess.STDOUT + ) + return PrivPrecResult(str(path / 'out.txt')) \ No newline at end of file diff --git a/gobexec/output/html/templates/privprecresult.jinja b/gobexec/output/html/templates/privprecresult.jinja new file mode 100644 index 0000000..e69de29 From 25ba44cf80712d37fbb4665541bc2c26204c9c45 Mon Sep 17 00:00:00 2001 From: healthypunk Date: Thu, 13 Apr 2023 08:01:37 +0300 Subject: [PATCH 08/26] Added a test file with some minor changes --- gobexec/goblint/result.py | 4 +- gobexec/goblint/tool.py | 9 +++-- gobexec/model/result.py | 4 +- .../html/templates/privprecresult.jinja | 1 + test.py | 2 +- update_bench_traces.py | 38 +++++++++++++++++++ 6 files changed, 50 insertions(+), 8 deletions(-) diff --git a/gobexec/goblint/result.py b/gobexec/goblint/result.py index 508feb8..d0a37c8 100644 --- a/gobexec/goblint/result.py +++ b/gobexec/goblint/result.py @@ -85,7 +85,7 @@ def template(self, env): async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'Rusage': return Rusage(cp.rusage) -@dataclass(init=False)#TODO: check correctness +@dataclass(init=False) class LineSummary(Result): live: int dead: int @@ -100,7 +100,7 @@ def template(self, env): return env.get_template("linesummary.jinja") @staticmethod - async def extract(self, ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'LineSummary': + async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'LineSummary': stdout = cp.stdout.decode("utf-8") live = len(re.findall(r"/live:[ ]*([0-9]*)/", stdout)) dead = len(re.findall(r"/dead:[ ]*([0-9]*)/", stdout)) diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index 187346e..eca0814 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -62,19 +62,22 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Co return cp -class PrivPrecTool(Tool[Single, PrivPrecResult]): # TODO: check correctness +class PrivPrecTool(Tool[Single, PrivPrecResult]): + name = str program: str args: List[GoblintTool] def __init__(self, - program: str = "./privPrecCompare", + name = "privPrecCompare", + program: str = "../analyzer/privPrecCompare", args: List[GoblintTool] = None) -> None: + self.name = name self.program = program self.args = args if args else [] async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> PrivPrecResult: path = ec.get_tool_data_path(self) - with(path / 'out.txt', 'w') as out_file: + with(path / 'out.txt').open("w") as out_file: args = [self.program] + [str(ec.get_tool_data_path(tool)) for tool in self.args] cp = await ec.subprocess_exec( args[0], diff --git a/gobexec/model/result.py b/gobexec/model/result.py index c544956..55ac263 100644 --- a/gobexec/model/result.py +++ b/gobexec/model/result.py @@ -100,7 +100,7 @@ def kind(self): else: return ResultKind.DEFAULT -@dataclass(init=False)#TODO: check correctness +@dataclass(init=False) class PrivPrecResult(Result): result_path: str @@ -108,5 +108,5 @@ def __init__(self, result_path: str) -> None: self.result_path = result_path def template(self, env: Environment) -> Template: - ...#TODO: Create template for privPrecCompare result + return env.get_template('privprecresult.jinja') diff --git a/gobexec/output/html/templates/privprecresult.jinja b/gobexec/output/html/templates/privprecresult.jinja index e69de29..7b0d2c6 100644 --- a/gobexec/output/html/templates/privprecresult.jinja +++ b/gobexec/output/html/templates/privprecresult.jinja @@ -0,0 +1 @@ +compare \ No newline at end of file diff --git a/test.py b/test.py index b7d2659..cae6714 100644 --- a/test.py +++ b/test.py @@ -30,7 +30,7 @@ def index_tool_factory(name, args): TimeResult, assert_summary_extractor, #AssertSummaryExtractor(), - # RaceSummary + RaceSummary, primary=assert_summary_extractor ) matrix = txtindex.load(Path("../bench/index/traces-rel-toy.txt"), index_tool_factory) diff --git a/update_bench_traces.py b/update_bench_traces.py index e69de29..c1ef96d 100644 --- a/update_bench_traces.py +++ b/update_bench_traces.py @@ -0,0 +1,38 @@ +from pathlib import Path + +import gobexec.main +from gobexec.goblint import tool +from gobexec.goblint.bench import txtindex +from gobexec.goblint.result import LineSummary +from gobexec.goblint.tool import GoblintTool + +from gobexec.model.result import TimeResult, PrivPrecResult +from gobexec.model.tools import ExtractTool, ResultExtractor +from gobexec.output.renderer import FileRenderer, ConsoleRenderer, MultiRenderer + + +def index_tool_factory(name, args): + goblint = GoblintTool( + name=name, + program="../analyzer/goblint", + args=["--conf", "../analyzer/conf/traces-rel-toy.json", "--enable", "dbg.debug"] + args, + dump= True + ) + + return ExtractTool( + goblint, + TimeResult, + LineSummary, + + + ) + +privprec = tool.PrivPrecTool() +matrix = txtindex.load(Path("../bench/index/traces-rel-toy.txt"),index_tool_factory) +matrix.tools.append(privprec) + +html_renderer = FileRenderer(Path("out.html")) +console_renderer = ConsoleRenderer() +renderer = MultiRenderer([html_renderer, console_renderer]) + +gobexec.main.run(matrix, renderer) \ No newline at end of file From 8020e892a490c828cc9bd2ba63c605a6af6ce3c2 Mon Sep 17 00:00:00 2001 From: healthypunk Date: Mon, 17 Apr 2023 09:56:55 +0300 Subject: [PATCH 09/26] Fixed output html --- gobexec/goblint/result.py | 11 +++++++---- gobexec/goblint/tool.py | 6 ++++-- gobexec/output/html/templates/linesummary.jinja | 6 +++--- gobexec/output/html/templates/matrix.jinja | 16 +++++++++++----- test.py | 2 +- update_bench_traces.py | 7 +++---- 6 files changed, 29 insertions(+), 19 deletions(-) diff --git a/gobexec/goblint/result.py b/gobexec/goblint/result.py index d0a37c8..ae53ce5 100644 --- a/gobexec/goblint/result.py +++ b/gobexec/goblint/result.py @@ -102,7 +102,10 @@ def template(self, env): @staticmethod async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'LineSummary': stdout = cp.stdout.decode("utf-8") - live = len(re.findall(r"/live:[ ]*([0-9]*)/", stdout)) - dead = len(re.findall(r"/dead:[ ]*([0-9]*)/", stdout)) - total = live + dead - return LineSummary(live, dead, total) + live = re.search(r"live:[ ]*([0-9]*)", stdout) + dead = re.search(r"dead:[ ]*([0-9]*)", stdout) + if live is None and dead is None: + return LineSummary(-1,-1,-1) + else: + total = int(live.group(1)) + int(dead.group(1)) + return LineSummary(int(live.group(1)), int(dead.group(1)), total) diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index eca0814..b775493 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -70,7 +70,8 @@ class PrivPrecTool(Tool[Single, PrivPrecResult]): def __init__(self, name = "privPrecCompare", program: str = "../analyzer/privPrecCompare", - args: List[GoblintTool] = None) -> None: + args: List[GoblintTool] = None, + ) -> None: self.name = name self.program = program self.args = args if args else [] @@ -79,8 +80,9 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Pr path = ec.get_tool_data_path(self) with(path / 'out.txt').open("w") as out_file: args = [self.program] + [str(ec.get_tool_data_path(tool)) for tool in self.args] - cp = await ec.subprocess_exec( + await ec.subprocess_exec( args[0], + *args[1:], stdout = out_file, stderr=asyncio.subprocess.STDOUT ) diff --git a/gobexec/output/html/templates/linesummary.jinja b/gobexec/output/html/templates/linesummary.jinja index 8eae00e..10518ac 100644 --- a/gobexec/output/html/templates/linesummary.jinja +++ b/gobexec/output/html/templates/linesummary.jinja @@ -1,5 +1,5 @@ {# TODO: add colouring to values #} -{{this.live}} -{{this.dead}} -{{this.total}} +{{this.live}} +{{this.dead}} +{{this.total}} diff --git a/gobexec/output/html/templates/matrix.jinja b/gobexec/output/html/templates/matrix.jinja index 4adad17..fe077c0 100644 --- a/gobexec/output/html/templates/matrix.jinja +++ b/gobexec/output/html/templates/matrix.jinja @@ -19,17 +19,23 @@ {% if loop.first %} {% endif %} - + {% for benchmark_result in benchmark_results.results %} {% if benchmark_result.done() %} {% if benchmark_result.result().result.kind == ResultKind.DEFAULT %} - - + + {% endif %} {% endfor %} diff --git a/test.py b/test.py index cae6714..1a75a8b 100644 --- a/test.py +++ b/test.py @@ -30,7 +30,7 @@ def index_tool_factory(name, args): TimeResult, assert_summary_extractor, #AssertSummaryExtractor(), - RaceSummary, + #RaceSummary, primary=assert_summary_extractor ) matrix = txtindex.load(Path("../bench/index/traces-rel-toy.txt"), index_tool_factory) diff --git a/update_bench_traces.py b/update_bench_traces.py index c1ef96d..baff036 100644 --- a/update_bench_traces.py +++ b/update_bench_traces.py @@ -15,7 +15,7 @@ def index_tool_factory(name, args): goblint = GoblintTool( name=name, program="../analyzer/goblint", - args=["--conf", "../analyzer/conf/traces-rel-toy.json", "--enable", "dbg.debug"] + args, + args=["--conf", "../analyzer/conf/traces.json", "--enable", "dbg.debug"] + args, dump= True ) @@ -23,14 +23,13 @@ def index_tool_factory(name, args): goblint, TimeResult, LineSummary, - + #PrivPrecResult ) +matrix = txtindex.load(Path("../bench/index/traces.txt"),index_tool_factory) privprec = tool.PrivPrecTool() -matrix = txtindex.load(Path("../bench/index/traces-rel-toy.txt"),index_tool_factory) matrix.tools.append(privprec) - html_renderer = FileRenderer(Path("out.html")) console_renderer = ConsoleRenderer() renderer = MultiRenderer([html_renderer, console_renderer]) From 23bc7ab146d6429cee82f379fc8945bdc24f495e Mon Sep 17 00:00:00 2001 From: evaldasp Date: Mon, 17 Apr 2023 15:09:54 +0300 Subject: [PATCH 10/26] Fixed html and PrivPrecTool output as well as added changing of directories for GoblintTool --- gobexec/goblint/tool.py | 14 +++++++++----- gobexec/output/html/templates/matrix.jinja | 2 +- update_bench_traces.py | 8 ++++---- 3 files changed, 14 insertions(+), 10 deletions(-) diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index b775493..213224e 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -49,13 +49,16 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Co self.args + \ benchmark.tool_data.get(ARGS_TOOL_KEY, []) + \ [str(file) for file in benchmark.files] + if self.dump is True: + args += ["--set", "exp.priv-prec-dump", data_path.absolute() / "priv.txt"] # print(args) cp = await ec.subprocess_exec( args[0], *args[1:], # capture_output=True, stdout=out_file, - stderr=asyncio.subprocess.STDOUT + stderr=asyncio.subprocess.STDOUT, + cwd = benchmark.files[0].parent ) out_file.seek(0) cp.stdout = out_file.read() # currently for extractors @@ -79,11 +82,12 @@ def __init__(self, async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> PrivPrecResult: path = ec.get_tool_data_path(self) with(path / 'out.txt').open("w") as out_file: - args = [self.program] + [str(ec.get_tool_data_path(tool)) for tool in self.args] + args = [self.program] + [str(ec.get_tool_data_path(tool)/"priv.txt") for tool in self.args] await ec.subprocess_exec( args[0], *args[1:], - stdout = out_file, - stderr=asyncio.subprocess.STDOUT + stdout=out_file, + stderr=asyncio.subprocess.STDOUT, + ) - return PrivPrecResult(str(path / 'out.txt')) \ No newline at end of file + return PrivPrecResult(str(path / 'out.txt')) diff --git a/gobexec/output/html/templates/matrix.jinja b/gobexec/output/html/templates/matrix.jinja index fe077c0..520507b 100644 --- a/gobexec/output/html/templates/matrix.jinja +++ b/gobexec/output/html/templates/matrix.jinja @@ -29,7 +29,7 @@ {% endif %} {% if loop.last %} -
Group Benchmark{{ tool.name }}{{ tool.name }}
{{ benchmark_results.benchmark.name }} - {% elif benchmark_result.result().result.kind == ResultKind.WARNING %} - - {% elif benchmark_result.result().result.kind == ResultKind.FAILURE %} - - {% elif benchmark_result.result().result.kind == ResultKind.ERROR %} - + {% if benchmark_result.result().result.kind == ResultKind.DEFAULT %} + + + {% endif %} + {{ benchmark_result.result().result|template }} {% else %} - - {% endif %} - {{ benchmark_result.result().result|template }} -
+ {% elif result.kind == ResultKind.WARNING %} + + {% elif result.kind == ResultKind.FAILURE %} + + {% elif result.kind == ResultKind.ERROR %} + + {% else %} + + {% endif %} + {{ result|template }} + {{ group_result.group.name }}{{ benchmark_results.benchmark.name }}{{ benchmark_results.benchmark.name }} - + {% if "asserts" in result.tools[0].name%} + + {% endif %} + + {% if loop.last %} + + {% endif %} + {% endif %} {{ benchmark_result.result().result|template }} {% else %} -
+ {% endif %} {% endif %} diff --git a/update_bench_traces.py b/update_bench_traces.py index baff036..3f88b6d 100644 --- a/update_bench_traces.py +++ b/update_bench_traces.py @@ -14,8 +14,8 @@ def index_tool_factory(name, args): goblint = GoblintTool( name=name, - program="../analyzer/goblint", - args=["--conf", "../analyzer/conf/traces.json", "--enable", "dbg.debug"] + args, + program=str(Path("../analyzer/goblint").absolute()), + args=["--conf", str(Path("../analyzer/conf/traces.json").absolute()), "--enable", "dbg.debug"] + args, dump= True ) @@ -27,8 +27,8 @@ def index_tool_factory(name, args): ) -matrix = txtindex.load(Path("../bench/index/traces.txt"),index_tool_factory) -privprec = tool.PrivPrecTool() +matrix = txtindex.load(Path("../bench/index/traces.txt").absolute(),index_tool_factory) +privprec = tool.PrivPrecTool(args= matrix.tools.copy()) matrix.tools.append(privprec) html_renderer = FileRenderer(Path("out.html")) console_renderer = ConsoleRenderer() From 961904abdd04f354a1c0b88af15acf2920afab5f Mon Sep 17 00:00:00 2001 From: healthypunk Date: Wed, 19 Apr 2023 12:42:45 +0300 Subject: [PATCH 11/26] Added ThreadSummary class as well as ApronPrecTool with result class and added corresponding templates and created a test file --- gobexec/goblint/result.py | 37 ++++++++++++++++++ gobexec/goblint/tool.py | 39 ++++++++++++++++--- gobexec/model/result.py | 11 ++++++ .../html/templates/apronprecresult.jinja | 1 + .../output/html/templates/linesummary.jinja | 6 +-- gobexec/output/html/templates/matrix.jinja | 2 +- .../output/html/templates/threadsummary.jinja | 5 +++ update_bench_traces.py | 4 +- update_bench_traces_rel.py | 39 +++++++++++++++++++ 9 files changed, 131 insertions(+), 13 deletions(-) create mode 100644 gobexec/output/html/templates/apronprecresult.jinja create mode 100644 gobexec/output/html/templates/threadsummary.jinja create mode 100644 update_bench_traces_rel.py diff --git a/gobexec/goblint/result.py b/gobexec/goblint/result.py index ae53ce5..81b3390 100644 --- a/gobexec/goblint/result.py +++ b/gobexec/goblint/result.py @@ -109,3 +109,40 @@ async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'LineSu else: total = int(live.group(1)) + int(dead.group(1)) return LineSummary(int(live.group(1)), int(dead.group(1)), total) + + +@dataclass(init=False) +class ThreadSummary(Result): + thread_id: int + unique_thread_id: int + max_protected: int + sum_protected: int + mutexes_count: int + + def __init__(self, thread_id: int, unique_thread_id: int, + max_protected: int, sum_protected: int, mutexes_count: int): + self.thread_id = thread_id + self.unique_thread_id = unique_thread_id + self.max_protected= max_protected + self.sum_protected = sum_protected + self.mutexes_count = mutexes_count + + def template(self, env): + return env.get_template("threadsummary.jinja") + + @staticmethod + async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'ThreadSummary': + stdout = cp.stdout.decode("utf-8") + thread_id = re.search(r"Encountered number of thread IDs \(unique\): ([0-9]*)",stdout) + thread_id = 0 if thread_id is None else int(thread_id.group(1)) + unique_thread_id = re.search(r"Encountered number of thread IDs \(unique\): [0-9]* \(([0-9]*)\)",stdout) + unique_thread_id = 0 if unique_thread_id is None else int(unique_thread_id.group(1)) + max_protected = re.search(r"Max number variables of protected by a mutex: ([0-9]*)",stdout) + max_protected = 0 if max_protected is None else int(max_protected.group(1)) + sum_protected = re.search(r"Total number of protected variables \(including duplicates\): ([0-9]*)",stdout) + sum_protected = 0 if sum_protected is None else int(sum_protected.group(1)) + mutexes_count = re.search(r"Number of mutexes: ([0-9]*)",stdout) + mutexes_count = 0 if mutexes_count is None else int(mutexes_count.group(1)) + + return ThreadSummary(thread_id,unique_thread_id,max_protected,sum_protected,mutexes_count) + diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index 213224e..0d4fce4 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -4,7 +4,7 @@ from gobexec.model.benchmark import Single from gobexec.model.context import ExecutionContext, CompletedSubprocess -from gobexec.model.result import PrivPrecResult +from gobexec.model.result import PrivPrecResult, ApronPrecResult from gobexec.model.tool import Tool ARGS_TOOL_KEY = "goblint-args" @@ -20,7 +20,7 @@ def __init__(self, name: str = "Goblint", program: str = "goblint", args: List[str] = None, - dump: bool = False + dump: str = '' ) -> None: self.name = name self.program = program @@ -49,8 +49,10 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Co self.args + \ benchmark.tool_data.get(ARGS_TOOL_KEY, []) + \ [str(file) for file in benchmark.files] - if self.dump is True: + if self.dump == "priv": args += ["--set", "exp.priv-prec-dump", data_path.absolute() / "priv.txt"] + elif self.dump == "apron": + args += ["--set", "exp.relation.prec-dump", data_path.absolute() / "apron.txt"] # print(args) cp = await ec.subprocess_exec( args[0], @@ -66,12 +68,12 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Co class PrivPrecTool(Tool[Single, PrivPrecResult]): - name = str + name: str program: str args: List[GoblintTool] def __init__(self, - name = "privPrecCompare", + name: str = "privPrecCompare", program: str = "../analyzer/privPrecCompare", args: List[GoblintTool] = None, ) -> None: @@ -85,9 +87,34 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Pr args = [self.program] + [str(ec.get_tool_data_path(tool)/"priv.txt") for tool in self.args] await ec.subprocess_exec( args[0], - *args[1:], stdout=out_file, stderr=asyncio.subprocess.STDOUT, ) return PrivPrecResult(str(path / 'out.txt')) + +class ApronPrecTool(Tool[Single,ApronPrecResult]): + name: str + program: str + args: List[GoblintTool] + + def __init__(self, + name: str = "apronPrecCompare", + program: str = "../analyzer/apronPrecCompare", + args: List[GoblintTool] = None, + ) -> None: + self.name = name + self.program = program + self.args = args + + async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> ApronPrecResult: + path = ec.get_tool_data_path(self) + with (path / 'out.txt').open('w') as out_file: + args = [self.program] + [str(ec.get_tool_data_path(tool)/'apron.txt') for tool in self.args] + await ec.subprocess_exec( + args[0], + *args[1:], + stdout = out_file, + stderr = asyncio.subprocess.STDOUT, + ) + return ApronPrecResult(str(path/'out.txt')) diff --git a/gobexec/model/result.py b/gobexec/model/result.py index 55ac263..19a8d96 100644 --- a/gobexec/model/result.py +++ b/gobexec/model/result.py @@ -110,3 +110,14 @@ def __init__(self, result_path: str) -> None: def template(self, env: Environment) -> Template: return env.get_template('privprecresult.jinja') + +@dataclass(init=False) +class ApronPrecResult(Result): + result_path: str + + def __init__(self,result_path: str) -> None: + self.result_path = result_path + + def template(self, env): + return env.get_template('apronprecresult.jinja') + diff --git a/gobexec/output/html/templates/apronprecresult.jinja b/gobexec/output/html/templates/apronprecresult.jinja new file mode 100644 index 0000000..7b0d2c6 --- /dev/null +++ b/gobexec/output/html/templates/apronprecresult.jinja @@ -0,0 +1 @@ +compare \ No newline at end of file diff --git a/gobexec/output/html/templates/linesummary.jinja b/gobexec/output/html/templates/linesummary.jinja index 10518ac..331ae04 100644 --- a/gobexec/output/html/templates/linesummary.jinja +++ b/gobexec/output/html/templates/linesummary.jinja @@ -1,5 +1,3 @@ -{# TODO: add colouring to values #} - -{{this.live}} -{{this.dead}} +{{this.live}} +{{this.dead}} {{this.total}} diff --git a/gobexec/output/html/templates/matrix.jinja b/gobexec/output/html/templates/matrix.jinja index 520507b..fe077c0 100644 --- a/gobexec/output/html/templates/matrix.jinja +++ b/gobexec/output/html/templates/matrix.jinja @@ -29,7 +29,7 @@ {% endif %} {% if loop.last %} - + {% endif %} {% endif %} diff --git a/gobexec/output/html/templates/threadsummary.jinja b/gobexec/output/html/templates/threadsummary.jinja new file mode 100644 index 0000000..b507946 --- /dev/null +++ b/gobexec/output/html/templates/threadsummary.jinja @@ -0,0 +1,5 @@ +{{this.thread_id}} +{{this.unique_thread_id}} +{{this.max_protected}} +{{this.sum_protected}} +{{this.mutexes_count}} \ No newline at end of file diff --git a/update_bench_traces.py b/update_bench_traces.py index 3f88b6d..31d2245 100644 --- a/update_bench_traces.py +++ b/update_bench_traces.py @@ -6,8 +6,8 @@ from gobexec.goblint.result import LineSummary from gobexec.goblint.tool import GoblintTool -from gobexec.model.result import TimeResult, PrivPrecResult -from gobexec.model.tools import ExtractTool, ResultExtractor +from gobexec.model.result import TimeResult +from gobexec.model.tools import ExtractTool from gobexec.output.renderer import FileRenderer, ConsoleRenderer, MultiRenderer diff --git a/update_bench_traces_rel.py b/update_bench_traces_rel.py new file mode 100644 index 0000000..9a325de --- /dev/null +++ b/update_bench_traces_rel.py @@ -0,0 +1,39 @@ +from pathlib import Path + +import gobexec.main +from gobexec.goblint import tool +from gobexec.goblint.bench import txtindex +from gobexec.goblint.result import ThreadSummary +from gobexec.goblint.tool import GoblintTool + +from gobexec.model.result import TimeResult +from gobexec.model.tools import ExtractTool +from gobexec.output.renderer import FileRenderer, ConsoleRenderer, MultiRenderer + + +def index_tool_factory(name, args): + goblint = GoblintTool( + name=name, + program=str(Path("../analyzer/goblint").absolute()), + args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug"] + args, + dump= 'apron' + ) + + return ExtractTool( + goblint, + TimeResult, + ThreadSummary, + #PrivPrecResult + + ) + +matrix = txtindex.load(Path("../bench/index/traces-relational.txt").absolute(),index_tool_factory) +apronprec = tool.ApronPrecTool(args= matrix.tools.copy()) +matrix.tools.append(apronprec) +# privprec = tool.PrivPrecTool(args= matrix.tools.copy()) +# matrix.tools.append(privprec) +html_renderer = FileRenderer(Path("out.html")) +console_renderer = ConsoleRenderer() +renderer = MultiRenderer([html_renderer, console_renderer]) + +gobexec.main.run(matrix, renderer) \ No newline at end of file From 94b6661ab6bb77be11868b75844b628989ecdc4f Mon Sep 17 00:00:00 2001 From: healthypunk Date: Fri, 21 Apr 2023 13:27:39 +0300 Subject: [PATCH 12/26] Added AssertTypeSummary class with template and created a testfile --- gobexec/goblint/result.py | 19 +++++++++ .../html/templates/asserttypesummary.jinja | 2 + udpate_bench_traces_rel_toy.py | 39 +++++++++++++++++++ 3 files changed, 60 insertions(+) create mode 100644 gobexec/output/html/templates/asserttypesummary.jinja create mode 100644 udpate_bench_traces_rel_toy.py diff --git a/gobexec/goblint/result.py b/gobexec/goblint/result.py index 81b3390..848bcab 100644 --- a/gobexec/goblint/result.py +++ b/gobexec/goblint/result.py @@ -146,3 +146,22 @@ async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'Thread return ThreadSummary(thread_id,unique_thread_id,max_protected,sum_protected,mutexes_count) + +@dataclass(init=False) +class AssertTypeSummary(Result): + success: int + unknown: int + + def __init__(self,success:int,unknown: int): + self.success = success + self.unknown = unknown + + def template(self, env): + return env.get_template("asserttypesummary.jinja") + + @staticmethod + async def extract(ec:ExecutionContext[Any],cp:CompletedSubprocess) -> 'AssertTypeSummary': + stdout = cp.stdout.decode("utf-8") + success = len(re.findall(r"\[Success\]\[Assert\]",stdout)) + unknown = len(re.findall(r"\[Warning\]\[Assert\]",stdout)) + return AssertTypeSummary(success,unknown) \ No newline at end of file diff --git a/gobexec/output/html/templates/asserttypesummary.jinja b/gobexec/output/html/templates/asserttypesummary.jinja new file mode 100644 index 0000000..b67b839 --- /dev/null +++ b/gobexec/output/html/templates/asserttypesummary.jinja @@ -0,0 +1,2 @@ +{{ this.success }}, +{{ this.unknown }} \ No newline at end of file diff --git a/udpate_bench_traces_rel_toy.py b/udpate_bench_traces_rel_toy.py new file mode 100644 index 0000000..6668a67 --- /dev/null +++ b/udpate_bench_traces_rel_toy.py @@ -0,0 +1,39 @@ +from pathlib import Path + +import gobexec.main +from gobexec.goblint import tool +from gobexec.goblint.bench import txtindex +from gobexec.goblint.result import AssertTypeSummary +from gobexec.goblint.tool import GoblintTool + +from gobexec.model.result import TimeResult +from gobexec.model.tools import ExtractTool +from gobexec.output.renderer import FileRenderer, ConsoleRenderer, MultiRenderer + + +def index_tool_factory(name, args): + goblint = GoblintTool( + name=name, + program=str(Path("../analyzer/goblint").absolute()), + args=["--conf", str(Path("../analyzer/conf/traces-rel-toy.json").absolute()), "--enable", "dbg.debug"] + args, + dump= 'apron' + ) + + return ExtractTool( + goblint, + TimeResult, + AssertTypeSummary, + #PrivPrecResult + + ) + +matrix = txtindex.load(Path("../bench/index/traces-rel-toy.txt").absolute(),index_tool_factory) +apronprec = tool.ApronPrecTool(args= matrix.tools.copy()) +matrix.tools.append(apronprec) +# privprec = tool.PrivPrecTool(args= matrix.tools.copy()) +# matrix.tools.append(privprec) +html_renderer = FileRenderer(Path("out.html")) +console_renderer = ConsoleRenderer() +renderer = MultiRenderer([html_renderer, console_renderer]) + +gobexec.main.run(matrix, renderer) \ No newline at end of file From 6115b6d11f08ba0a74b5972975643c0481e819e3 Mon Sep 17 00:00:00 2001 From: healthypunk Date: Wed, 26 Apr 2023 17:31:37 +0300 Subject: [PATCH 13/26] Added update_bench_traces_rel_assert.py, update_bench_traces_rel_ratcop.py, update_bench_traces_rel_watts.py, update_bench_traces_rel_yaml.py scripts --- gobexec/goblint/tool.py | 6 +-- test.py | 2 +- udpate_bench_traces_rel_toy.py | 71 ++++++++++++++---------------- update_bench_traces.py | 72 +++++++++++++++---------------- update_bench_traces_rel_assert.py | 33 ++++++++++++++ update_bench_traces_rel_ratcop.py | 33 ++++++++++++++ update_bench_traces_rel_watts.py | 34 +++++++++++++++ update_bench_traces_rel_yaml.py | 33 ++++++++++++++ 8 files changed, 206 insertions(+), 78 deletions(-) create mode 100644 update_bench_traces_rel_assert.py create mode 100644 update_bench_traces_rel_ratcop.py create mode 100644 update_bench_traces_rel_watts.py create mode 100644 update_bench_traces_rel_yaml.py diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index 0d4fce4..f6a0cb9 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -14,7 +14,7 @@ class GoblintTool(Tool[Single, CompletedSubprocess]): name: str program: str args: List[str] - dump: bool + dump: str def __init__(self, name: str = "Goblint", @@ -83,7 +83,7 @@ def __init__(self, async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> PrivPrecResult: path = ec.get_tool_data_path(self) - with(path / 'out.txt').open("w") as out_file: + with(path / 'priv_compare_out.txt').open("w") as out_file: args = [self.program] + [str(ec.get_tool_data_path(tool)/"priv.txt") for tool in self.args] await ec.subprocess_exec( args[0], @@ -110,7 +110,7 @@ def __init__(self, async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> ApronPrecResult: path = ec.get_tool_data_path(self) with (path / 'out.txt').open('w') as out_file: - args = [self.program] + [str(ec.get_tool_data_path(tool)/'apron.txt') for tool in self.args] + args = [self.program] + [str(ec.get_tool_data_path(tool).absolute()/'apron.txt') for tool in self.args] await ec.subprocess_exec( args[0], *args[1:], diff --git a/test.py b/test.py index 1a75a8b..06ad73f 100644 --- a/test.py +++ b/test.py @@ -20,7 +20,7 @@ def index_tool_factory(name, args): goblint = GoblintTool( name=name, - program="../analyzer/goblint", + program=str(Path("../analyzer/goblint").absolute()), args=["--conf", "../analyzer/conf/traces-rel-toy.json", "--enable", "dbg.debug"] + args, # args=["--conf", "/home/simmo/dev/goblint/sv-comp/goblint/conf/traces-rel.json", "--enable", "dbg.debug"], ) diff --git a/udpate_bench_traces_rel_toy.py b/udpate_bench_traces_rel_toy.py index 6668a67..995dee8 100644 --- a/udpate_bench_traces_rel_toy.py +++ b/udpate_bench_traces_rel_toy.py @@ -1,39 +1,34 @@ -from pathlib import Path - -import gobexec.main -from gobexec.goblint import tool -from gobexec.goblint.bench import txtindex -from gobexec.goblint.result import AssertTypeSummary -from gobexec.goblint.tool import GoblintTool - -from gobexec.model.result import TimeResult -from gobexec.model.tools import ExtractTool -from gobexec.output.renderer import FileRenderer, ConsoleRenderer, MultiRenderer - - -def index_tool_factory(name, args): - goblint = GoblintTool( - name=name, - program=str(Path("../analyzer/goblint").absolute()), - args=["--conf", str(Path("../analyzer/conf/traces-rel-toy.json").absolute()), "--enable", "dbg.debug"] + args, - dump= 'apron' - ) - - return ExtractTool( - goblint, - TimeResult, - AssertTypeSummary, - #PrivPrecResult - - ) - -matrix = txtindex.load(Path("../bench/index/traces-rel-toy.txt").absolute(),index_tool_factory) -apronprec = tool.ApronPrecTool(args= matrix.tools.copy()) -matrix.tools.append(apronprec) -# privprec = tool.PrivPrecTool(args= matrix.tools.copy()) -# matrix.tools.append(privprec) -html_renderer = FileRenderer(Path("out.html")) -console_renderer = ConsoleRenderer() -renderer = MultiRenderer([html_renderer, console_renderer]) - +from pathlib import Path + +import gobexec.main +from gobexec.goblint import tool +from gobexec.goblint.bench import txtindex +from gobexec.goblint.result import AssertTypeSummary +from gobexec.goblint.tool import GoblintTool + +from gobexec.model.result import TimeResult +from gobexec.model.tools import ExtractTool +from gobexec.output.renderer import FileRenderer, ConsoleRenderer, MultiRenderer + + +def index_tool_factory(name, args): + goblint = GoblintTool( + name=name, + program=str(Path("../analyzer/goblint").absolute()), + args=["--conf", str(Path("../analyzer/conf/traces-rel-toy.json").absolute()), "--enable", "dbg.debug"] + args, + dump= 'apron' + ) + + return ExtractTool( + goblint, + TimeResult, + AssertTypeSummary, + + ) + +matrix = txtindex.load(Path("../bench/index/traces-rel-toy.txt").absolute(),index_tool_factory) +html_renderer = FileRenderer(Path("out.html")) +console_renderer = ConsoleRenderer() +renderer = MultiRenderer([html_renderer, console_renderer]) + gobexec.main.run(matrix, renderer) \ No newline at end of file diff --git a/update_bench_traces.py b/update_bench_traces.py index 31d2245..384f136 100644 --- a/update_bench_traces.py +++ b/update_bench_traces.py @@ -1,37 +1,37 @@ -from pathlib import Path - -import gobexec.main -from gobexec.goblint import tool -from gobexec.goblint.bench import txtindex -from gobexec.goblint.result import LineSummary -from gobexec.goblint.tool import GoblintTool - -from gobexec.model.result import TimeResult -from gobexec.model.tools import ExtractTool -from gobexec.output.renderer import FileRenderer, ConsoleRenderer, MultiRenderer - - -def index_tool_factory(name, args): - goblint = GoblintTool( - name=name, - program=str(Path("../analyzer/goblint").absolute()), - args=["--conf", str(Path("../analyzer/conf/traces.json").absolute()), "--enable", "dbg.debug"] + args, - dump= True - ) - - return ExtractTool( - goblint, - TimeResult, - LineSummary, - #PrivPrecResult - - ) - -matrix = txtindex.load(Path("../bench/index/traces.txt").absolute(),index_tool_factory) -privprec = tool.PrivPrecTool(args= matrix.tools.copy()) -matrix.tools.append(privprec) -html_renderer = FileRenderer(Path("out.html")) -console_renderer = ConsoleRenderer() -renderer = MultiRenderer([html_renderer, console_renderer]) - +from pathlib import Path + +import gobexec.main +from gobexec.goblint import tool +from gobexec.goblint.bench import txtindex +from gobexec.goblint.result import LineSummary +from gobexec.goblint.tool import GoblintTool + +from gobexec.model.result import TimeResult +from gobexec.model.tools import ExtractTool +from gobexec.output.renderer import FileRenderer, ConsoleRenderer, MultiRenderer + + +def index_tool_factory(name, args): + goblint = GoblintTool( + name=name, + program=str(Path("../analyzer/goblint").absolute()), + args=["--conf", str(Path("../analyzer/conf/traces.json").absolute()), "--enable", "dbg.debug"] + args, + dump= "priv" + ) + + return ExtractTool( + goblint, + TimeResult, + LineSummary, + #PrivPrecResult + + ) + +matrix = txtindex.load(Path("../bench/index/traces.txt").absolute(),index_tool_factory) +privprec = tool.PrivPrecTool(args= matrix.tools.copy()) +matrix.tools.append(privprec) +html_renderer = FileRenderer(Path("out.html")) +console_renderer = ConsoleRenderer() +renderer = MultiRenderer([html_renderer, console_renderer]) + gobexec.main.run(matrix, renderer) \ No newline at end of file diff --git a/update_bench_traces_rel_assert.py b/update_bench_traces_rel_assert.py new file mode 100644 index 0000000..c3f169a --- /dev/null +++ b/update_bench_traces_rel_assert.py @@ -0,0 +1,33 @@ +from pathlib import Path + +import gobexec.main +from gobexec.goblint.bench import txtindex +from gobexec.goblint.result import AssertTypeSummary +from gobexec.goblint.tool import GoblintTool + +from gobexec.model.result import TimeResult +from gobexec.model.tools import ExtractTool +from gobexec.output.renderer import FileRenderer, ConsoleRenderer, MultiRenderer + + +def index_tool_factory(name, args): + goblint = GoblintTool( + name=name, + program=str(Path("../analyzer/goblint").absolute()), + args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug"] + args, + dump= 'apron' + ) + + return ExtractTool( + goblint, + TimeResult, + AssertTypeSummary, + + ) + +matrix = txtindex.load(Path("../bench/index/traces-rel-assert.txt").absolute(),index_tool_factory) +html_renderer = FileRenderer(Path("out.html")) +console_renderer = ConsoleRenderer() +renderer = MultiRenderer([html_renderer, console_renderer]) + +gobexec.main.run(matrix, renderer) \ No newline at end of file diff --git a/update_bench_traces_rel_ratcop.py b/update_bench_traces_rel_ratcop.py new file mode 100644 index 0000000..abcfbc4 --- /dev/null +++ b/update_bench_traces_rel_ratcop.py @@ -0,0 +1,33 @@ +from pathlib import Path + +import gobexec.main +from gobexec.goblint.bench import txtindex +from gobexec.goblint.result import AssertTypeSummary +from gobexec.goblint.tool import GoblintTool + +from gobexec.model.result import TimeResult +from gobexec.model.tools import ExtractTool +from gobexec.output.renderer import FileRenderer, ConsoleRenderer, MultiRenderer + + +def index_tool_factory(name, args): + goblint = GoblintTool( + name=name, + program=str(Path("../analyzer/goblint").absolute()), + args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug"] + args, + dump= 'apron' + ) + + return ExtractTool( + goblint, + TimeResult, + AssertTypeSummary, + + ) + +matrix = txtindex.load(Path("../bench/index/traces-rel-ratcop.txt").absolute(),index_tool_factory) +html_renderer = FileRenderer(Path("out.html")) +console_renderer = ConsoleRenderer() +renderer = MultiRenderer([html_renderer, console_renderer]) + +gobexec.main.run(matrix, renderer) \ No newline at end of file diff --git a/update_bench_traces_rel_watts.py b/update_bench_traces_rel_watts.py new file mode 100644 index 0000000..b60d73d --- /dev/null +++ b/update_bench_traces_rel_watts.py @@ -0,0 +1,34 @@ +import asyncio +from pathlib import Path + +import gobexec.main +from gobexec.goblint.bench import txtindex, tools +from gobexec.goblint.extractor import AssertSummaryExtractor +from gobexec.goblint.tool import GoblintTool +from gobexec.model.result import TimeResult +from gobexec.model.tools import ExtractTool +from gobexec.output.renderer import FileRenderer, ConsoleRenderer, MultiRenderer + +assert_counter = tools.AssertCounter() + +def index_tool_factory(name, args): + goblint = GoblintTool( + name=name, + program=str(Path("../analyzer/goblint").absolute()), + args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug"] + args, + ) + assert_summary_extractor = AssertSummaryExtractor(assert_counter) + return ExtractTool( + goblint, + TimeResult, + assert_summary_extractor, + primary=assert_summary_extractor + ) +matrix = txtindex.load(Path("../bench/index/traces-relational-watts.txt"), index_tool_factory) +matrix.tools.insert(0, assert_counter) + +html_renderer = FileRenderer(Path("out.html")) +console_renderer = ConsoleRenderer() +renderer = MultiRenderer([html_renderer, console_renderer]) + +gobexec.main.run(matrix, renderer) \ No newline at end of file diff --git a/update_bench_traces_rel_yaml.py b/update_bench_traces_rel_yaml.py new file mode 100644 index 0000000..51f9e52 --- /dev/null +++ b/update_bench_traces_rel_yaml.py @@ -0,0 +1,33 @@ +from pathlib import Path + +import gobexec.main +from gobexec.goblint.bench import txtindex +from gobexec.goblint.result import AssertTypeSummary +from gobexec.goblint.tool import GoblintTool + +from gobexec.model.result import TimeResult +from gobexec.model.tools import ExtractTool +from gobexec.output.renderer import FileRenderer, ConsoleRenderer, MultiRenderer + + +def index_tool_factory(name, args): + goblint = GoblintTool( + name=name, + program=str(Path("../analyzer/goblint").absolute()), + args=["--conf", str(Path("../analyzer/conf/traces-rel-toy.json").absolute()), "--enable", "dbg.debug"] + args, + dump= 'apron' + ) + + return ExtractTool( + goblint, + TimeResult, + AssertTypeSummary, + + ) + +matrix = txtindex.load(Path("../bench/index/traces-rel-yaml.txt").absolute(),index_tool_factory) +html_renderer = FileRenderer(Path("out.html")) +console_renderer = ConsoleRenderer() +renderer = MultiRenderer([html_renderer, console_renderer]) + +gobexec.main.run(matrix, renderer) \ No newline at end of file From d0082dfa65b3d7e2f186cb20dce5fd7dbef69b20 Mon Sep 17 00:00:00 2001 From: evaldasp Date: Tue, 2 May 2023 15:50:13 +0300 Subject: [PATCH 14/26] Minor fixes --- gobexec/goblint/result.py | 24 ++++++++++++++++++- gobexec/goblint/tool.py | 14 +++++++++-- .../output/html/templates/yamlsummary.jinja | 2 ++ update_bench_traces_rel_assert.py | 2 +- update_bench_traces_rel_ratcop.py | 6 +++-- update_bench_traces_rel_watts.py | 2 +- update_bench_traces_rel_yaml.py | 9 +++---- 7 files changed, 48 insertions(+), 11 deletions(-) create mode 100644 gobexec/output/html/templates/yamlsummary.jinja diff --git a/gobexec/goblint/result.py b/gobexec/goblint/result.py index 848bcab..00778da 100644 --- a/gobexec/goblint/result.py +++ b/gobexec/goblint/result.py @@ -163,5 +163,27 @@ def template(self, env): async def extract(ec:ExecutionContext[Any],cp:CompletedSubprocess) -> 'AssertTypeSummary': stdout = cp.stdout.decode("utf-8") success = len(re.findall(r"\[Success\]\[Assert\]",stdout)) + unknown = len(re.findall(r"\[Warning\]\[Assert\]",stdout)) - return AssertTypeSummary(success,unknown) \ No newline at end of file + return AssertTypeSummary(success,unknown) + +@dataclass(init=False) +class YamlSummary(Result): + confirmed: int + unconfirmed: int + + def __init__(self,success:int,unknown: int): + self.success = success + self.unknown = unknown + + def template(self, env): + return env.get_template("yamlsummary.jinja") + + @staticmethod + async def extract(ec:ExecutionContext[Any],cp:CompletedSubprocess) -> 'AssertTypeSummary': + stdout = cp.stdout.decode("utf-8") + confirmed = re.search(r" confirmed:[ ]*([0-9]*)",stdout) + confirmed = 0 if confirmed is None else confirmed.group(1) + unconfirmed = re.search(r" unconfirmed:[ ]*([0-9]*)",stdout) + unconfirmed = 0 if unconfirmed is None else unconfirmed.group(1) + return AssertTypeSummary(int(confirmed),int(unconfirmed)) \ No newline at end of file diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index f6a0cb9..584d736 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -15,17 +15,20 @@ class GoblintTool(Tool[Single, CompletedSubprocess]): program: str args: List[str] dump: str + validate: bool def __init__(self, name: str = "Goblint", program: str = "goblint", args: List[str] = None, - dump: str = '' + dump: str = '', + validate: bool = False ) -> None: self.name = name self.program = program self.args = args if args else [] self.dump = dump + self.validate = validate # def run(self, benchmark: Single) -> str: # bench = Path("/home/simmo/dev/goblint/sv-comp/goblint-bench") @@ -53,7 +56,10 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Co args += ["--set", "exp.priv-prec-dump", data_path.absolute() / "priv.txt"] elif self.dump == "apron": args += ["--set", "exp.relation.prec-dump", data_path.absolute() / "apron.txt"] - # print(args) + + if self.validate is True: + args += ["--set", "witness.yaml.validate", str(benchmark.files[0].parent / (str(benchmark.files[0].name)[:-2] + "_traces_rel.yml"))] + cp = await ec.subprocess_exec( args[0], *args[1:], @@ -83,6 +89,8 @@ def __init__(self, async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> PrivPrecResult: path = ec.get_tool_data_path(self) + for tool in self.args: + await ec.get_tool_result(tool) with(path / 'priv_compare_out.txt').open("w") as out_file: args = [self.program] + [str(ec.get_tool_data_path(tool)/"priv.txt") for tool in self.args] await ec.subprocess_exec( @@ -109,6 +117,8 @@ def __init__(self, async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> ApronPrecResult: path = ec.get_tool_data_path(self) + for tool in self.args: + await ec.get_tool_result(tool) with (path / 'out.txt').open('w') as out_file: args = [self.program] + [str(ec.get_tool_data_path(tool).absolute()/'apron.txt') for tool in self.args] await ec.subprocess_exec( diff --git a/gobexec/output/html/templates/yamlsummary.jinja b/gobexec/output/html/templates/yamlsummary.jinja new file mode 100644 index 0000000..fce5a0e --- /dev/null +++ b/gobexec/output/html/templates/yamlsummary.jinja @@ -0,0 +1,2 @@ +{{ this.success }}, +{{ this.unknown }} \ No newline at end of file diff --git a/update_bench_traces_rel_assert.py b/update_bench_traces_rel_assert.py index c3f169a..5c6638d 100644 --- a/update_bench_traces_rel_assert.py +++ b/update_bench_traces_rel_assert.py @@ -14,7 +14,7 @@ def index_tool_factory(name, args): goblint = GoblintTool( name=name, program=str(Path("../analyzer/goblint").absolute()), - args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug"] + args, + args=["-v", "--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug"] + args, dump= 'apron' ) diff --git a/update_bench_traces_rel_ratcop.py b/update_bench_traces_rel_ratcop.py index abcfbc4..544777b 100644 --- a/update_bench_traces_rel_ratcop.py +++ b/update_bench_traces_rel_ratcop.py @@ -2,7 +2,8 @@ import gobexec.main from gobexec.goblint.bench import txtindex -from gobexec.goblint.result import AssertTypeSummary +from gobexec.goblint.extractor import AssertSummaryExtractor +from gobexec.goblint.result import AssertTypeSummary, LineSummary from gobexec.goblint.tool import GoblintTool from gobexec.model.result import TimeResult @@ -21,7 +22,8 @@ def index_tool_factory(name, args): return ExtractTool( goblint, TimeResult, - AssertTypeSummary, + LineSummary, + AssertSummaryExtractor(), ) diff --git a/update_bench_traces_rel_watts.py b/update_bench_traces_rel_watts.py index b60d73d..d95af80 100644 --- a/update_bench_traces_rel_watts.py +++ b/update_bench_traces_rel_watts.py @@ -24,7 +24,7 @@ def index_tool_factory(name, args): assert_summary_extractor, primary=assert_summary_extractor ) -matrix = txtindex.load(Path("../bench/index/traces-relational-watts.txt"), index_tool_factory) +matrix = txtindex.load(Path("../bench/index/traces-relational-watts.txt").absolute(), index_tool_factory) matrix.tools.insert(0, assert_counter) html_renderer = FileRenderer(Path("out.html")) diff --git a/update_bench_traces_rel_yaml.py b/update_bench_traces_rel_yaml.py index 51f9e52..7fdf527 100644 --- a/update_bench_traces_rel_yaml.py +++ b/update_bench_traces_rel_yaml.py @@ -2,7 +2,7 @@ import gobexec.main from gobexec.goblint.bench import txtindex -from gobexec.goblint.result import AssertTypeSummary +from gobexec.goblint.result import AssertTypeSummary, YamlSummary from gobexec.goblint.tool import GoblintTool from gobexec.model.result import TimeResult @@ -14,14 +14,15 @@ def index_tool_factory(name, args): goblint = GoblintTool( name=name, program=str(Path("../analyzer/goblint").absolute()), - args=["--conf", str(Path("../analyzer/conf/traces-rel-toy.json").absolute()), "--enable", "dbg.debug"] + args, - dump= 'apron' + args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug"] + args, + dump= 'apron', + validate= True ) return ExtractTool( goblint, TimeResult, - AssertTypeSummary, + YamlSummary, ) From f63f1adc2cebcf6e1c592e26b2fcd72221859b6e Mon Sep 17 00:00:00 2001 From: evaldasp Date: Wed, 10 May 2023 18:14:41 +0300 Subject: [PATCH 15/26] Added update_bench_concrat.py script --- gobexec/goblint/result.py | 75 ++++++++++++++----- .../output/html/templates/concratresult.jinja | 4 + update_bench_concrat.py | 29 +++++++ 3 files changed, 89 insertions(+), 19 deletions(-) create mode 100644 gobexec/output/html/templates/concratresult.jinja create mode 100644 update_bench_concrat.py diff --git a/gobexec/goblint/result.py b/gobexec/goblint/result.py index 00778da..eec63d8 100644 --- a/gobexec/goblint/result.py +++ b/gobexec/goblint/result.py @@ -69,7 +69,6 @@ def kind(self): return ResultKind.WARNING - @dataclass(init=False) class Rusage(Result): rusage: resource.struct_rusage @@ -85,6 +84,7 @@ def template(self, env): async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'Rusage': return Rusage(cp.rusage) + @dataclass(init=False) class LineSummary(Result): live: int @@ -105,7 +105,7 @@ async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'LineSu live = re.search(r"live:[ ]*([0-9]*)", stdout) dead = re.search(r"dead:[ ]*([0-9]*)", stdout) if live is None and dead is None: - return LineSummary(-1,-1,-1) + return LineSummary(-1, -1, -1) else: total = int(live.group(1)) + int(dead.group(1)) return LineSummary(int(live.group(1)), int(dead.group(1)), total) @@ -123,7 +123,7 @@ def __init__(self, thread_id: int, unique_thread_id: int, max_protected: int, sum_protected: int, mutexes_count: int): self.thread_id = thread_id self.unique_thread_id = unique_thread_id - self.max_protected= max_protected + self.max_protected = max_protected self.sum_protected = sum_protected self.mutexes_count = mutexes_count @@ -133,18 +133,18 @@ def template(self, env): @staticmethod async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'ThreadSummary': stdout = cp.stdout.decode("utf-8") - thread_id = re.search(r"Encountered number of thread IDs \(unique\): ([0-9]*)",stdout) + thread_id = re.search(r"Encountered number of thread IDs \(unique\): ([0-9]*)", stdout) thread_id = 0 if thread_id is None else int(thread_id.group(1)) - unique_thread_id = re.search(r"Encountered number of thread IDs \(unique\): [0-9]* \(([0-9]*)\)",stdout) + unique_thread_id = re.search(r"Encountered number of thread IDs \(unique\): [0-9]* \(([0-9]*)\)", stdout) unique_thread_id = 0 if unique_thread_id is None else int(unique_thread_id.group(1)) - max_protected = re.search(r"Max number variables of protected by a mutex: ([0-9]*)",stdout) + max_protected = re.search(r"Max number variables of protected by a mutex: ([0-9]*)", stdout) max_protected = 0 if max_protected is None else int(max_protected.group(1)) - sum_protected = re.search(r"Total number of protected variables \(including duplicates\): ([0-9]*)",stdout) + sum_protected = re.search(r"Total number of protected variables \(including duplicates\): ([0-9]*)", stdout) sum_protected = 0 if sum_protected is None else int(sum_protected.group(1)) - mutexes_count = re.search(r"Number of mutexes: ([0-9]*)",stdout) + mutexes_count = re.search(r"Number of mutexes: ([0-9]*)", stdout) mutexes_count = 0 if mutexes_count is None else int(mutexes_count.group(1)) - return ThreadSummary(thread_id,unique_thread_id,max_protected,sum_protected,mutexes_count) + return ThreadSummary(thread_id, unique_thread_id, max_protected, sum_protected, mutexes_count) @dataclass(init=False) @@ -152,7 +152,7 @@ class AssertTypeSummary(Result): success: int unknown: int - def __init__(self,success:int,unknown: int): + def __init__(self, success: int, unknown: int): self.success = success self.unknown = unknown @@ -160,19 +160,20 @@ def template(self, env): return env.get_template("asserttypesummary.jinja") @staticmethod - async def extract(ec:ExecutionContext[Any],cp:CompletedSubprocess) -> 'AssertTypeSummary': + async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'AssertTypeSummary': stdout = cp.stdout.decode("utf-8") - success = len(re.findall(r"\[Success\]\[Assert\]",stdout)) + success = len(re.findall(r"\[Success\]\[Assert\]", stdout)) + + unknown = len(re.findall(r"\[Warning\]\[Assert\]", stdout)) + return AssertTypeSummary(success, unknown) - unknown = len(re.findall(r"\[Warning\]\[Assert\]",stdout)) - return AssertTypeSummary(success,unknown) @dataclass(init=False) class YamlSummary(Result): confirmed: int unconfirmed: int - def __init__(self,success:int,unknown: int): + def __init__(self, success: int, unknown: int): self.success = success self.unknown = unknown @@ -180,10 +181,46 @@ def template(self, env): return env.get_template("yamlsummary.jinja") @staticmethod - async def extract(ec:ExecutionContext[Any],cp:CompletedSubprocess) -> 'AssertTypeSummary': + async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'AssertTypeSummary': stdout = cp.stdout.decode("utf-8") - confirmed = re.search(r" confirmed:[ ]*([0-9]*)",stdout) + confirmed = re.search(r" confirmed:[ ]*([0-9]*)", stdout) confirmed = 0 if confirmed is None else confirmed.group(1) - unconfirmed = re.search(r" unconfirmed:[ ]*([0-9]*)",stdout) + unconfirmed = re.search(r" unconfirmed:[ ]*([0-9]*)", stdout) unconfirmed = 0 if unconfirmed is None else unconfirmed.group(1) - return AssertTypeSummary(int(confirmed),int(unconfirmed)) \ No newline at end of file + return AssertTypeSummary(int(confirmed), int(unconfirmed)) + + +dataclass(init=False) + + +class ConcratSummary(Result): + safe: int + vulnerable: int + unsafe: int + uncalled: int + + def __init__(self, safe: int, vulnerable: int, unsafe: int, uncalled: int): + self.safe = safe + self.vulnerable = vulnerable + self.unsafe = unsafe + self.uncalled = uncalled + + def template(self, env): + return env.get_template("concratresult.jinja") + + @staticmethod + async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> "ConcratSummary": + stdout = cp.stdout.decode("utf-8") + safe = re.search(r"[^n]safe:[ ]*([0-9]*)", stdout) + safe = -1 if safe is None else safe.group(1) + vulnerable = re.search(r"vulnerable:[ ]*([0-9]*)", stdout) + vulnerable = -1 if vulnerable is None else vulnerable.group(1) + unsafe = re.search(r"unsafe:[ ]*([0-9]*)", stdout) + unsafe = -1 if unsafe is None else unsafe.group(1) + uncalled = re.findall(r"will never be called", stdout) + for elem in uncalled: + if bool(re.search(r"__check", elem)): + continue + else: + uncalled.remove(elem) + return ConcratSummary(safe, vulnerable, unsafe, len(uncalled)) diff --git a/gobexec/output/html/templates/concratresult.jinja b/gobexec/output/html/templates/concratresult.jinja new file mode 100644 index 0000000..853f726 --- /dev/null +++ b/gobexec/output/html/templates/concratresult.jinja @@ -0,0 +1,4 @@ +{{this.safe}} +{{this.vulnerable}} +{{this.unsafe}} +{{this.uncalled}} \ No newline at end of file diff --git a/update_bench_concrat.py b/update_bench_concrat.py new file mode 100644 index 0000000..da159c7 --- /dev/null +++ b/update_bench_concrat.py @@ -0,0 +1,29 @@ +from pathlib import Path + +import gobexec.main +from gobexec.goblint.bench import txtindex +from gobexec.goblint.result import ConcratSummary +from gobexec.goblint.tool import GoblintTool +from gobexec.model.result import TimeResult +from gobexec.model.tools import ExtractTool +from gobexec.output.renderer import FileRenderer, ConsoleRenderer, MultiRenderer + + +def index_tool_factory(name, args): + goblint = GoblintTool( + name=name, + program=str(Path("../analyzer/goblint").absolute()), + ) + + return ExtractTool( + goblint, + TimeResult, + ConcratSummary, + ) + +matrix = txtindex.load(Path("../bench/index/concrat.txt").absolute(),index_tool_factory) +html_renderer = FileRenderer(Path("out.html")) +console_renderer = ConsoleRenderer() +renderer = MultiRenderer([html_renderer, console_renderer]) + +gobexec.main.run(matrix, renderer) \ No newline at end of file From 07b225281219b90a484503de354ef590c7c4f96e Mon Sep 17 00:00:00 2001 From: healthypunk <73522653+healthypunk@users.noreply.github.com> Date: Tue, 20 Jun 2023 17:25:01 +0300 Subject: [PATCH 16/26] Update README.md --- README.md | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index ff85b17..c5ad945 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,16 @@ # GobExec -GobExec – because BenchExec isn't enough +GobExec – because BenchExec is not enough + +## Installing +1. Ensure that you are using [Python 3.10](https://www.python.org/downloads/release/python-3100/) or higher. +2. Install [Goblint](https://github.com/goblint/analyzer#installing). +3. Install [Goblint benchmark suite](https://github.com/goblint/bench#readme). + +## Running + +To ensure that you have installed everything correctly, run ``test.py`` within the GobExec directory +``` + python3 test.py +``` + +The generated output file ``GobExec/out.html`` can be viewed via your browser of choice From bd4310482594de3fac8a6574f62cb598278512b1 Mon Sep 17 00:00:00 2001 From: evaldasp Date: Sun, 3 Mar 2024 15:49:20 +0200 Subject: [PATCH 17/26] Added yaml file generation for update_bench_traces_rel_yaml.py as well as C file generation for update_bench_traces_rel_assert.py --- gobexec/goblint/result.py | 2 +- gobexec/goblint/tool.py | 42 +++++++++++++------- gobexec/output/html/templates/progress.jinja | 2 +- update_bench_traces_rel_assert.py | 12 +++++- update_bench_traces_rel_yaml.py | 19 +++++++-- 5 files changed, 54 insertions(+), 23 deletions(-) diff --git a/gobexec/goblint/result.py b/gobexec/goblint/result.py index a547b49..56a53c8 100644 --- a/gobexec/goblint/result.py +++ b/gobexec/goblint/result.py @@ -208,7 +208,7 @@ class ConcratSummary(Result): unsafe: int uncalled: int - def __init__(self, safe: int, vulnerable: int, unsafe: int, uncalled: int): + def __init__(self, safe: int, vulnerable: int, unsafe: int, uncalled: int) -> None: self.safe = safe self.vulnerable = vulnerable self.unsafe = unsafe diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index 584d736..70d9458 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -1,6 +1,6 @@ import asyncio import tempfile -from typing import List +from typing import List, Optional from gobexec.model.benchmark import Single from gobexec.model.context import ExecutionContext, CompletedSubprocess @@ -15,22 +15,26 @@ class GoblintTool(Tool[Single, CompletedSubprocess]): program: str args: List[str] dump: str - validate: bool + validate: Optional["GoblintTool"] + assertion: Optional["GoblintTool"] def __init__(self, name: str = "Goblint", program: str = "goblint", args: List[str] = None, dump: str = '', - validate: bool = False + validate: Optional["GoblintTool"] = None, + assertion: Optional["GoblintTool"] = None ) -> None: self.name = name self.program = program self.args = args if args else [] self.dump = dump self.validate = validate + self.assertion = assertion + + # def run(self, benchmark: Single) -> str: - # def run(self, benchmark: Single) -> str: # bench = Path("/home/simmo/dev/goblint/sv-comp/goblint-bench") # args = ["/home/simmo/dev/goblint/sv-comp/goblint/goblint"] + self.args + benchmark.tool_data.get(ARGS_TOOL_KEY, []) + [str(bench / file) for file in benchmark.files] # print(args) @@ -51,14 +55,21 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Co ["--set", "goblint-dir", goblint_dir.absolute()] + \ self.args + \ benchmark.tool_data.get(ARGS_TOOL_KEY, []) + \ - [str(file) for file in benchmark.files] + [str(file) for file in benchmark.files] if self.assertion is None else [ec.get_tool_data_path(self.assertion).absolute() / "out.c"] if self.dump == "priv": args += ["--set", "exp.priv-prec-dump", data_path.absolute() / "priv.txt"] elif self.dump == "apron": args += ["--set", "exp.relation.prec-dump", data_path.absolute() / "apron.txt"] - - if self.validate is True: - args += ["--set", "witness.yaml.validate", str(benchmark.files[0].parent / (str(benchmark.files[0].name)[:-2] + "_traces_rel.yml"))] + elif self.dump == "witness": + args += ["--set", "witness.yaml.path", data_path.absolute() / "witness.yaml"] + elif self.dump == "assert": + args += ["--set", "trans.output",data_path.absolute() / "out.c"] + if self.validate is not None: + await ec.get_tool_result(self.validate) + args += ["--set", "witness.yaml.validate", + ec.get_tool_data_path(self.validate).absolute() / "witness.yaml"] + if self.assertion is not None: + await ec.get_tool_result(self.assertion) cp = await ec.subprocess_exec( args[0], @@ -66,7 +77,7 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Co # capture_output=True, stdout=out_file, stderr=asyncio.subprocess.STDOUT, - cwd = benchmark.files[0].parent + cwd=benchmark.files[0].parent ) out_file.seek(0) cp.stdout = out_file.read() # currently for extractors @@ -92,7 +103,7 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Pr for tool in self.args: await ec.get_tool_result(tool) with(path / 'priv_compare_out.txt').open("w") as out_file: - args = [self.program] + [str(ec.get_tool_data_path(tool)/"priv.txt") for tool in self.args] + args = [self.program] + [str(ec.get_tool_data_path(tool) / "priv.txt") for tool in self.args] await ec.subprocess_exec( args[0], stdout=out_file, @@ -101,7 +112,8 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Pr ) return PrivPrecResult(str(path / 'out.txt')) -class ApronPrecTool(Tool[Single,ApronPrecResult]): + +class ApronPrecTool(Tool[Single, ApronPrecResult]): name: str program: str args: List[GoblintTool] @@ -120,11 +132,11 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Ap for tool in self.args: await ec.get_tool_result(tool) with (path / 'out.txt').open('w') as out_file: - args = [self.program] + [str(ec.get_tool_data_path(tool).absolute()/'apron.txt') for tool in self.args] + args = [self.program] + [str(ec.get_tool_data_path(tool).absolute() / 'apron.txt') for tool in self.args] await ec.subprocess_exec( args[0], *args[1:], - stdout = out_file, - stderr = asyncio.subprocess.STDOUT, + stdout=out_file, + stderr=asyncio.subprocess.STDOUT, ) - return ApronPrecResult(str(path/'out.txt')) + return ApronPrecResult(str(path / 'out.txt')) diff --git a/gobexec/output/html/templates/progress.jinja b/gobexec/output/html/templates/progress.jinja index ed9b70d..f479d14 100644 --- a/gobexec/output/html/templates/progress.jinja +++ b/gobexec/output/html/templates/progress.jinja @@ -2,7 +2,7 @@ {% block title %}Results ({{ progress.done }}/{{ progress.total }}){% endblock %} {% block head %} {{ super() }} - + {##} {% endblock %} {% block body %}

diff --git a/update_bench_traces_rel_assert.py b/update_bench_traces_rel_assert.py index 5c6638d..a6e55cd 100644 --- a/update_bench_traces_rel_assert.py +++ b/update_bench_traces_rel_assert.py @@ -9,13 +9,20 @@ from gobexec.model.tools import ExtractTool from gobexec.output.renderer import FileRenderer, ConsoleRenderer, MultiRenderer +goblint_assert = GoblintTool( + name="goblint_assert", + program=str(Path("../analyzer/goblint").absolute()), + args=["-v", "--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug","--set", "trans.activated[+]", "assert"], + dump = "assert" +) def index_tool_factory(name, args): goblint = GoblintTool( name=name, program=str(Path("../analyzer/goblint").absolute()), args=["-v", "--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug"] + args, - dump= 'apron' + dump= 'apron', + assertion = goblint_assert ) return ExtractTool( @@ -25,7 +32,8 @@ def index_tool_factory(name, args): ) -matrix = txtindex.load(Path("../bench/index/traces-rel-assert.txt").absolute(),index_tool_factory) +matrix = txtindex.load(Path("../bench/index/traces-rel-yaml.txt").absolute(),index_tool_factory) +matrix.tools.insert(0,ExtractTool(goblint_assert)) html_renderer = FileRenderer(Path("out.html")) console_renderer = ConsoleRenderer() renderer = MultiRenderer([html_renderer, console_renderer]) diff --git a/update_bench_traces_rel_yaml.py b/update_bench_traces_rel_yaml.py index 7fdf527..ffe0e1e 100644 --- a/update_bench_traces_rel_yaml.py +++ b/update_bench_traces_rel_yaml.py @@ -9,14 +9,23 @@ from gobexec.model.tools import ExtractTool from gobexec.output.renderer import FileRenderer, ConsoleRenderer, MultiRenderer +goblint_witness = GoblintTool( + name="witness_gen", + program=str(Path("../analyzer/goblint").absolute()), + args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug", "--enable", + "witness.yaml.enabled"], + dump='witness' + +) + def index_tool_factory(name, args): goblint = GoblintTool( name=name, program=str(Path("../analyzer/goblint").absolute()), args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug"] + args, - dump= 'apron', - validate= True + dump='apron', + validate= goblint_witness ) return ExtractTool( @@ -26,9 +35,11 @@ def index_tool_factory(name, args): ) -matrix = txtindex.load(Path("../bench/index/traces-rel-yaml.txt").absolute(),index_tool_factory) + +matrix = txtindex.load(Path("../bench/index/traces-rel-yaml.txt").absolute(), index_tool_factory) +matrix.tools.insert(0,ExtractTool(goblint_witness)) html_renderer = FileRenderer(Path("out.html")) console_renderer = ConsoleRenderer() renderer = MultiRenderer([html_renderer, console_renderer]) -gobexec.main.run(matrix, renderer) \ No newline at end of file +gobexec.main.run(matrix, renderer) From 19ec7cc883b7b84c461cf3accd9edd80a7c2123a Mon Sep 17 00:00:00 2001 From: evaldasp Date: Thu, 14 Mar 2024 14:18:56 +0200 Subject: [PATCH 18/26] Fixed update_bench_traces_rel_assert.py throwing an error --- gobexec/goblint/tool.py | 8 ++++++-- update_bench_traces_rel_assert.py | 3 ++- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index 70d9458..54fead8 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -54,8 +54,8 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Co args = [self.program] + \ ["--set", "goblint-dir", goblint_dir.absolute()] + \ self.args + \ - benchmark.tool_data.get(ARGS_TOOL_KEY, []) + \ - [str(file) for file in benchmark.files] if self.assertion is None else [ec.get_tool_data_path(self.assertion).absolute() / "out.c"] + benchmark.tool_data.get(ARGS_TOOL_KEY, []) + #[str(file) for file in benchmark.files] if self.assertion is None else [ec.get_tool_data_path(self.assertion).absolute() / "out.c"] if self.dump == "priv": args += ["--set", "exp.priv-prec-dump", data_path.absolute() / "priv.txt"] elif self.dump == "apron": @@ -68,7 +68,11 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Co await ec.get_tool_result(self.validate) args += ["--set", "witness.yaml.validate", ec.get_tool_data_path(self.validate).absolute() / "witness.yaml"] + if self.assertion is None: + args += [str(file) for file in benchmark.files] if self.assertion is not None: + args += [ec.get_tool_data_path(self.assertion).absolute() / "out.c"] + args += ["--enable", "ana.sv-comp.functions"] await ec.get_tool_result(self.assertion) cp = await ec.subprocess_exec( diff --git a/update_bench_traces_rel_assert.py b/update_bench_traces_rel_assert.py index a6e55cd..5b42b47 100644 --- a/update_bench_traces_rel_assert.py +++ b/update_bench_traces_rel_assert.py @@ -12,7 +12,8 @@ goblint_assert = GoblintTool( name="goblint_assert", program=str(Path("../analyzer/goblint").absolute()), - args=["-v", "--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug","--set", "trans.activated[+]", "assert"], + args=["-v", "--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug","--set", "trans.activated[+]", "assert", + "--set" ,"ana.activated[+]" ,"apron" ,"--set" ,"ana.path_sens[+]" ,"threadflag", "--set" ,"ana.relation.privatization", "mutex-meet-tid-cluster12"], dump = "assert" ) From 1f93bb47c05a2a89c3d67d94dcc97a3127bee248 Mon Sep 17 00:00:00 2001 From: healthypunk Date: Mon, 25 Mar 2024 15:23:59 +0200 Subject: [PATCH 19/26] Created initial Incremental benchmark class and GoblintToolFromScratch, GoblintToolIncremental classes --- gobexec/goblint/tool.py | 94 +++++++++++++++++++++++++++++++++++-- gobexec/model/benchmark.py | 9 ++++ update_bench_incremental.py | 0 3 files changed, 99 insertions(+), 4 deletions(-) create mode 100644 update_bench_incremental.py diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index 54fead8..19f4102 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -1,8 +1,10 @@ import asyncio import tempfile from typing import List, Optional - -from gobexec.model.benchmark import Single +import shutil +import os +from glob import glob +from gobexec.model.benchmark import Single, Incremental from gobexec.model.context import ExecutionContext, CompletedSubprocess from gobexec.model.result import PrivPrecResult, ApronPrecResult from gobexec.model.tool import Tool @@ -10,6 +12,90 @@ ARGS_TOOL_KEY = "goblint-args" +class GoblintToolFromScratch(Tool[Incremental, CompletedSubprocess]): + name: str + program: str + args: List[str] + + def __init__(self, + name: str = "Goblint", + program: str = "goblint", + args: List[str] = None, + ) -> None: + self.name = name + self.program = program + self.args = args if args else [] + + async def run_async(self, ec: ExecutionContext[Incremental], benchmark: Incremental) -> CompletedSubprocess: + data_path = ec.get_tool_data_path(self) + goblint_dir = data_path / ".goblint" + goblint_dir.mkdir(parents=True, exist_ok=True) + shutil.copy(benchmark.files, data_path) + with (data_path / "out.txt").open("w+b") as out_file: + args = [self.program] + \ + ["--conf", "index/conf/td3.json", "--enable incremental.save", "--set", "incremental.save-dir", + goblint_dir.absolute(), "-v", glob("/*.c", recursive=False)[0]] + \ + self.args + \ + benchmark.tool_data.get(ARGS_TOOL_KEY, []) + + cp = await ec.subprocess_exec( + args[0], + *args[1:], + # capture_output=True, + stdout=out_file, + stderr=asyncio.subprocess.STDOUT, + cwd=benchmark.files[0].parent + ) + out_file.seek(0) + cp.stdout = out_file.read() # currently for extractors + + await ec.subprocess_exec(["patch", "-b", glob("/*.c", recursive=False)[0], benchmark.patch]) + return cp + + +class GoblintToolIncremental(Tool[Incremental, CompletedSubprocess]): + name: str + program: str + args: List[str] + from_scratch_path: str + + def __init__(self, + name: str = "Goblint", + program: str = "goblint", + args: List[str] = None, + from_scratch_path: str = "" + ) -> None: + self.name = name + self.program = program + self.args = args if args else [] + self.from_scratch_path = from_scratch_path + + async def run_async(self, ec: ExecutionContext[Incremental], benchmark: Incremental) -> CompletedSubprocess: + data_path = ec.get_tool_data_path(self) + goblint_dir = data_path / ".goblint" + goblint_dir.mkdir(parents=True, exist_ok=True) + shutil.copy(benchmark.files, data_path) + with (data_path / "out.txt").open("w+b") as out_file: + args = [self.program] + \ + ["--conf", "index/conf/td3.json", "--enable incremental.load", "--set", "incremental.load-dir", + goblint_dir.absolute(), "-v", glob("/*.c", recursive=False)[0]] + \ + self.args + \ + benchmark.tool_data.get(ARGS_TOOL_KEY, []) + + cp = await ec.subprocess_exec( + args[0], + *args[1:], + # capture_output=True, + stdout=out_file, + stderr=asyncio.subprocess.STDOUT, + cwd=benchmark.files[0].parent + ) + out_file.seek(0) + cp.stdout = out_file.read() # currently for extractors + + return cp + + class GoblintTool(Tool[Single, CompletedSubprocess]): name: str program: str @@ -55,7 +141,7 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Co ["--set", "goblint-dir", goblint_dir.absolute()] + \ self.args + \ benchmark.tool_data.get(ARGS_TOOL_KEY, []) - #[str(file) for file in benchmark.files] if self.assertion is None else [ec.get_tool_data_path(self.assertion).absolute() / "out.c"] + # [str(file) for file in benchmark.files] if self.assertion is None else [ec.get_tool_data_path(self.assertion).absolute() / "out.c"] if self.dump == "priv": args += ["--set", "exp.priv-prec-dump", data_path.absolute() / "priv.txt"] elif self.dump == "apron": @@ -63,7 +149,7 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Co elif self.dump == "witness": args += ["--set", "witness.yaml.path", data_path.absolute() / "witness.yaml"] elif self.dump == "assert": - args += ["--set", "trans.output",data_path.absolute() / "out.c"] + args += ["--set", "trans.output", data_path.absolute() / "out.c"] if self.validate is not None: await ec.get_tool_result(self.validate) args += ["--set", "witness.yaml.validate", diff --git a/gobexec/model/benchmark.py b/gobexec/model/benchmark.py index 339789c..b14371e 100644 --- a/gobexec/model/benchmark.py +++ b/gobexec/model/benchmark.py @@ -13,6 +13,15 @@ class Single: tool_data: Dict[str, Any] +@dataclass +class Incremental: + name: str + description: str + files: Path + patch: Path + tool_data: Dict[str, Any] + + @dataclass class Group(Generic[B]): name: str diff --git a/update_bench_incremental.py b/update_bench_incremental.py new file mode 100644 index 0000000..e69de29 From 2e4406e4a7fea272a52f9b8264449dce9e43e343 Mon Sep 17 00:00:00 2001 From: evaldasp Date: Mon, 1 Apr 2024 20:56:13 +0300 Subject: [PATCH 20/26] Fixed GoblintToolFromScratch and GoblintToolIncremental classes and made test matrix --- gobexec/goblint/tool.py | 31 ++++++++++++----------- update_bench_incremental.py | 50 +++++++++++++++++++++++++++++++++++++ 2 files changed, 67 insertions(+), 14 deletions(-) diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index 19f4102..79044b4 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -1,5 +1,6 @@ import asyncio import tempfile +from pathlib import Path from typing import List, Optional import shutil import os @@ -28,13 +29,14 @@ def __init__(self, async def run_async(self, ec: ExecutionContext[Incremental], benchmark: Incremental) -> CompletedSubprocess: data_path = ec.get_tool_data_path(self) - goblint_dir = data_path / ".goblint" + goblint_dir = data_path goblint_dir.mkdir(parents=True, exist_ok=True) shutil.copy(benchmark.files, data_path) with (data_path / "out.txt").open("w+b") as out_file: args = [self.program] + \ - ["--conf", "index/conf/td3.json", "--enable incremental.save", "--set", "incremental.save-dir", - goblint_dir.absolute(), "-v", glob("/*.c", recursive=False)[0]] + \ + ["--set", "goblint-dir", goblint_dir.absolute()] + \ + ["--conf", str(Path("../bench/index/conf/td3.json").absolute()), "--enable","incremental.save", "--set", "incremental.save-dir", + goblint_dir.absolute(), "-v", str(Path(data_path/benchmark.files.name).absolute())] + \ self.args + \ benchmark.tool_data.get(ARGS_TOOL_KEY, []) @@ -44,12 +46,12 @@ async def run_async(self, ec: ExecutionContext[Incremental], benchmark: Incremen # capture_output=True, stdout=out_file, stderr=asyncio.subprocess.STDOUT, - cwd=benchmark.files[0].parent + cwd=benchmark.files.parent ) out_file.seek(0) cp.stdout = out_file.read() # currently for extractors - await ec.subprocess_exec(["patch", "-b", glob("/*.c", recursive=False)[0], benchmark.patch]) + await ec.subprocess_exec("patch", "-b", str(Path(data_path/benchmark.files.name).absolute()), benchmark.patch) return cp @@ -57,28 +59,30 @@ class GoblintToolIncremental(Tool[Incremental, CompletedSubprocess]): name: str program: str args: List[str] - from_scratch_path: str + from_scratch: Optional[GoblintToolFromScratch] def __init__(self, name: str = "Goblint", program: str = "goblint", args: List[str] = None, - from_scratch_path: str = "" + from_scratch: Optional[GoblintToolFromScratch] = None ) -> None: self.name = name self.program = program self.args = args if args else [] - self.from_scratch_path = from_scratch_path + self.from_scratch = from_scratch async def run_async(self, ec: ExecutionContext[Incremental], benchmark: Incremental) -> CompletedSubprocess: + await ec.get_tool_result(self.from_scratch) data_path = ec.get_tool_data_path(self) - goblint_dir = data_path / ".goblint" + goblint_dir = data_path goblint_dir.mkdir(parents=True, exist_ok=True) - shutil.copy(benchmark.files, data_path) + with (data_path / "out.txt").open("w+b") as out_file: args = [self.program] + \ - ["--conf", "index/conf/td3.json", "--enable incremental.load", "--set", "incremental.load-dir", - goblint_dir.absolute(), "-v", glob("/*.c", recursive=False)[0]] + \ + ["--set", "goblint-dir", goblint_dir.absolute()] + \ + ["--conf", "../bench/index/conf/td3.json", "--enable","incremental.load", "--set", "incremental.load-dir", + str(Path(ec.get_tool_data_path(self.from_scratch)).absolute()), "-v", str(Path(ec.get_tool_data_path(self.from_scratch)/benchmark.files.name).absolute())] + \ self.args + \ benchmark.tool_data.get(ARGS_TOOL_KEY, []) @@ -88,7 +92,7 @@ async def run_async(self, ec: ExecutionContext[Incremental], benchmark: Incremen # capture_output=True, stdout=out_file, stderr=asyncio.subprocess.STDOUT, - cwd=benchmark.files[0].parent + cwd=benchmark.files.parent ) out_file.seek(0) cp.stdout = out_file.read() # currently for extractors @@ -141,7 +145,6 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Co ["--set", "goblint-dir", goblint_dir.absolute()] + \ self.args + \ benchmark.tool_data.get(ARGS_TOOL_KEY, []) - # [str(file) for file in benchmark.files] if self.assertion is None else [ec.get_tool_data_path(self.assertion).absolute() / "out.c"] if self.dump == "priv": args += ["--set", "exp.priv-prec-dump", data_path.absolute() / "priv.txt"] elif self.dump == "apron": diff --git a/update_bench_incremental.py b/update_bench_incremental.py index e69de29..eda7918 100644 --- a/update_bench_incremental.py +++ b/update_bench_incremental.py @@ -0,0 +1,50 @@ +from gobexec.goblint.tool import GoblintToolFromScratch, GoblintToolIncremental +from pathlib import Path + +import gobexec.main +from gobexec.goblint import tool +from gobexec.goblint.bench import txtindex +from gobexec.goblint.result import ThreadSummary +from gobexec.goblint.tool import GoblintTool +from gobexec.model.benchmark import Incremental, Group + +from gobexec.model.result import TimeResult +from gobexec.model.scenario import Matrix +from gobexec.model.tools import ExtractTool +from gobexec.output.renderer import FileRenderer, ConsoleRenderer, MultiRenderer + +from_scratch = GoblintToolFromScratch( + name="from_scratch", + program=str(Path("../analyzer/goblint").absolute()), + +) + +incremental = GoblintToolIncremental( + name="incremental", + program=str(Path("../analyzer/goblint").absolute()), + from_scratch=from_scratch +) + +bench = Incremental( + name="aget", + description="", + files=Path("../bench/pthread/aget_comb.c").absolute(), + patch=Path("../bench/pthread/aget_comb02.patch").absolute(), + tool_data={} +) +group = Group( + name="test", + benchmarks=[bench] +) + +matrix = Matrix( + name="test", + groups=[group], + tools=[from_scratch, incremental] +) + +html_renderer = FileRenderer(Path("out.html")) +console_renderer = ConsoleRenderer() +renderer = MultiRenderer([html_renderer, console_renderer]) + +gobexec.main.run(matrix, renderer) From 0eb4f5c2f7cb62df882866ef4eedf11d3ac05e35 Mon Sep 17 00:00:00 2001 From: evaldasp Date: Thu, 4 Apr 2024 17:59:45 +0300 Subject: [PATCH 21/26] Fixed GoblintToolFromScratch and GoblintToolIncremental and added code for incremental benchmark result retrieval --- gobexec/goblint/result.py | 19 +++++++++++++++++++ gobexec/goblint/tool.py | 2 +- gobexec/model/tools.py | 2 +- .../output/html/templates/incremental.jinja | 2 ++ update_bench_incremental.py | 16 ++++++++++++++-- update_bench_traces.py | 2 +- 6 files changed, 38 insertions(+), 5 deletions(-) create mode 100644 gobexec/output/html/templates/incremental.jinja diff --git a/gobexec/goblint/result.py b/gobexec/goblint/result.py index 56a53c8..4ef8405 100644 --- a/gobexec/goblint/result.py +++ b/gobexec/goblint/result.py @@ -233,3 +233,22 @@ async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> "Concra else: uncalled.remove(elem) return ConcratSummary(safe, vulnerable, unsafe, len(uncalled)) + + +@dataclass(init=False) +class IncrementalSummary(Result): + vars: int + evals: int + + def __init__(self, vars: int, evals: int): + self.vars = vars + self.evals = evals + + def template(self, env): + return env.get_template("incremental.jinja") + + @staticmethod + async def extract(ec: ExecutionContext, cp: CompletedSubprocess): + stdout = cp.stdout.decode("utf-8") + data = re.search(r"\[\w+]\s\w+.{3}(\d+)\s+\w+.{3}(\d+)\s+\w+.{3}(\d+)", stdout) + return IncrementalSummary(data.group(1), data.group(2)) diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index 79044b4..1bc0ef3 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -51,7 +51,7 @@ async def run_async(self, ec: ExecutionContext[Incremental], benchmark: Incremen out_file.seek(0) cp.stdout = out_file.read() # currently for extractors - await ec.subprocess_exec("patch", "-b", str(Path(data_path/benchmark.files.name).absolute()), benchmark.patch) + await ec.subprocess_exec("patch", str(Path(data_path/benchmark.files.name).absolute()), benchmark.patch) return cp diff --git a/gobexec/model/tools.py b/gobexec/model/tools.py index 269c6f4..79378b6 100644 --- a/gobexec/model/tools.py +++ b/gobexec/model/tools.py @@ -32,7 +32,7 @@ def name(self): return self.delegate.name async def run_async(self, ec: ExecutionContext[B], benchmark: B) -> R: - cp = await self.delegate.run_async(ec, benchmark) + cp = await ec.get_tool_result(self.delegate) results = await asyncio.gather(*[extractor.extract(ec, cp) for extractor in self.extractors]) if self.primary: primary_result = results[self.extractors.index(self.primary)] # TODO: something better than index-based diff --git a/gobexec/output/html/templates/incremental.jinja b/gobexec/output/html/templates/incremental.jinja new file mode 100644 index 0000000..869cdf8 --- /dev/null +++ b/gobexec/output/html/templates/incremental.jinja @@ -0,0 +1,2 @@ +{{this.vars}} +{{this.evals}} \ No newline at end of file diff --git a/update_bench_incremental.py b/update_bench_incremental.py index eda7918..75ccf3c 100644 --- a/update_bench_incremental.py +++ b/update_bench_incremental.py @@ -4,7 +4,7 @@ import gobexec.main from gobexec.goblint import tool from gobexec.goblint.bench import txtindex -from gobexec.goblint.result import ThreadSummary +from gobexec.goblint.result import ThreadSummary, IncrementalSummary from gobexec.goblint.tool import GoblintTool from gobexec.model.benchmark import Incremental, Group @@ -40,9 +40,21 @@ matrix = Matrix( name="test", groups=[group], - tools=[from_scratch, incremental] + tools=[] ) +extractor = ExtractTool( + from_scratch, + TimeResult, + IncrementalSummary +) +extractor2 = ExtractTool( + incremental, + TimeResult, + IncrementalSummary +) +matrix.tools.insert(0,extractor) +matrix.tools.insert(1,extractor2) html_renderer = FileRenderer(Path("out.html")) console_renderer = ConsoleRenderer() renderer = MultiRenderer([html_renderer, console_renderer]) diff --git a/update_bench_traces.py b/update_bench_traces.py index 384f136..fd26525 100644 --- a/update_bench_traces.py +++ b/update_bench_traces.py @@ -15,7 +15,7 @@ def index_tool_factory(name, args): goblint = GoblintTool( name=name, program=str(Path("../analyzer/goblint").absolute()), - args=["--conf", str(Path("../analyzer/conf/traces.json").absolute()), "--enable", "dbg.debug"] + args, + args=["--conf", str(Path("../analyzer/conf/traces.json").absolute()), "--enable", "warn.debug"] + args, dump= "priv" ) From 77320c70612e62814433a199a8aabf22d26814c2 Mon Sep 17 00:00:00 2001 From: healthypunk Date: Fri, 19 Apr 2024 12:45:04 +0300 Subject: [PATCH 22/26] Added ToolFactory class and load function to yamlindex.py. --- gobexec/goblint/bench/yamlindex.py | 37 +++++++++++++++++++++++++++++- 1 file changed, 36 insertions(+), 1 deletion(-) diff --git a/gobexec/goblint/bench/yamlindex.py b/gobexec/goblint/bench/yamlindex.py index c79e15c..2519335 100644 --- a/gobexec/goblint/bench/yamlindex.py +++ b/gobexec/goblint/bench/yamlindex.py @@ -1,11 +1,46 @@ +import shlex from dataclasses import dataclass from pathlib import Path -from typing import Optional, List, Dict, Any + +from typing import Optional, List, Dict, Any, Protocol import yaml +from gobexec.goblint.tool import ARGS_TOOL_KEY +from gobexec.model.benchmark import Incremental, Group +from gobexec.model.scenario import Matrix +from gobexec.model.tool import Tool, R + + # TODO: inline and remove all dataclasses, construct Matrix directly +class ToolFactory(Protocol): + def __call__(self, name: str, args: List[str]) -> Tool[Incremental, R]: + ... + + +def load(def_path: Path, set_path: List[Path], tool_factory: ToolFactory) -> Matrix[Incremental, R]: + defsets_ = DefSets.from_paths(def_path, set_path) + groups: List[Group[Incremental]] = [] + tool: Tool[Incremental,R] = tool_factory(args=defsets_.def_.confs) + for set_ in defsets_.sets: + groups.append(Group(name=set_.name, benchmarks=[])) + for bench in set_.benchmarks: + groups[-1].benchmarks.append(Incremental( + name=bench.name, + description=bench.info, + files=bench.path, + patch=bench.path.with_suffix("."+"patch"), + tool_data={ + ARGS_TOOL_KEY: shlex.split(bench.param) if bench.param else [] + })) + return Matrix( + name=def_path.stem, + tools=[tool], + groups=groups, + ) + + @dataclass class Benchmark: name: str From 729ac8a2ecd0be540d8332023d195eb8a688df67 Mon Sep 17 00:00:00 2001 From: healthypunk Date: Wed, 24 Apr 2024 12:36:47 +0300 Subject: [PATCH 23/26] Changed update_bench_incremental.py to use yamlindex.py --- update_bench_incremental.py | 83 ++++++++++++++++++++++--------------- 1 file changed, 49 insertions(+), 34 deletions(-) diff --git a/update_bench_incremental.py b/update_bench_incremental.py index 75ccf3c..a4477c0 100644 --- a/update_bench_incremental.py +++ b/update_bench_incremental.py @@ -3,7 +3,7 @@ import gobexec.main from gobexec.goblint import tool -from gobexec.goblint.bench import txtindex +from gobexec.goblint.bench import txtindex, yamlindex from gobexec.goblint.result import ThreadSummary, IncrementalSummary from gobexec.goblint.tool import GoblintTool from gobexec.model.benchmark import Incremental, Group @@ -19,42 +19,57 @@ ) -incremental = GoblintToolIncremental( - name="incremental", - program=str(Path("../analyzer/goblint").absolute()), - from_scratch=from_scratch -) -bench = Incremental( - name="aget", - description="", - files=Path("../bench/pthread/aget_comb.c").absolute(), - patch=Path("../bench/pthread/aget_comb02.patch").absolute(), - tool_data={} -) -group = Group( - name="test", - benchmarks=[bench] -) +def index_tool_factory(name, args): + incremental = GoblintToolIncremental( + name=name, + program=str(Path("../analyzer/goblint").absolute()), + from_scratch=from_scratch + ) + return ExtractTool( + incremental, + TimeResult, + IncrementalSummary + ) -matrix = Matrix( - name="test", - groups=[group], - tools=[] -) -extractor = ExtractTool( - from_scratch, - TimeResult, - IncrementalSummary -) -extractor2 = ExtractTool( - incremental, - TimeResult, - IncrementalSummary -) -matrix.tools.insert(0,extractor) -matrix.tools.insert(1,extractor2) +# incremental = GoblintToolIncremental( +# name="incremental", +# program=str(Path("../analyzer/goblint").absolute()), +# from_scratch=from_scratch +# ) +# +# bench = Incremental( +# name="aget", +# description="", +# files=Path("../bench/pthread/aget_comb.c").absolute(), +# patch=Path("../bench/pthread/aget_comb02.patch").absolute(), +# tool_data={} +# ) +# group = Group( +# name="test", +# benchmarks=[bench] +# ) +# +# matrix = Matrix( +# name="test", +# groups=[group], +# tools=[] +# ) + +# extractor = ExtractTool( +# from_scratch, +# TimeResult, +# IncrementalSummary +# ) +# extractor2 = ExtractTool( +# incremental, +# TimeResult, +# IncrementalSummary +# ) +matrix = yamlindex.load(Path("")) +matrix.tools.insert(0, extractor) +matrix.tools.insert(1, extractor2) html_renderer = FileRenderer(Path("out.html")) console_renderer = ConsoleRenderer() renderer = MultiRenderer([html_renderer, console_renderer]) From d92d246588283474967bf41a27f385a25b421f53 Mon Sep 17 00:00:00 2001 From: healthypunk Date: Wed, 24 Apr 2024 15:18:17 +0300 Subject: [PATCH 24/26] Fixed update_bench_incremental.py to use yamlindex.py --- gobexec/goblint/bench/yamlindex.py | 11 ++++++++--- update_bench_incremental.py | 7 ++++--- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/gobexec/goblint/bench/yamlindex.py b/gobexec/goblint/bench/yamlindex.py index 2519335..e9af60e 100644 --- a/gobexec/goblint/bench/yamlindex.py +++ b/gobexec/goblint/bench/yamlindex.py @@ -22,15 +22,20 @@ def __call__(self, name: str, args: List[str]) -> Tool[Incremental, R]: def load(def_path: Path, set_path: List[Path], tool_factory: ToolFactory) -> Matrix[Incremental, R]: defsets_ = DefSets.from_paths(def_path, set_path) groups: List[Group[Incremental]] = [] - tool: Tool[Incremental,R] = tool_factory(args=defsets_.def_.confs) + tool: Tool[Incremental,R] = tool_factory(name= "",args=defsets_.def_.confs) for set_ in defsets_.sets: groups.append(Group(name=set_.name, benchmarks=[])) for bench in set_.benchmarks: + patch_path = Path("../bench")/bench.path.with_suffix("."+"patch") + parts = list(patch_path.parts) + temp = parts[3].split(".") + parts[3] = temp[0]+"01."+temp[1] + patch_path = Path(*parts) groups[-1].benchmarks.append(Incremental( name=bench.name, description=bench.info, - files=bench.path, - patch=bench.path.with_suffix("."+"patch"), + files=Path("../bench")/bench.path, + patch= patch_path, tool_data={ ARGS_TOOL_KEY: shlex.split(bench.param) if bench.param else [] })) diff --git a/update_bench_incremental.py b/update_bench_incremental.py index a4477c0..1812b17 100644 --- a/update_bench_incremental.py +++ b/update_bench_incremental.py @@ -67,9 +67,10 @@ def index_tool_factory(name, args): # TimeResult, # IncrementalSummary # ) -matrix = yamlindex.load(Path("")) -matrix.tools.insert(0, extractor) -matrix.tools.insert(1, extractor2) +matrix = yamlindex.load(Path("../bench/index/defs/incremental.yaml"),[Path("../bench/index/sets/posix.yaml")],index_tool_factory) +matrix.tools.insert(0,ExtractTool(from_scratch,TimeResult,IncrementalSummary)) +# matrix.tools.insert(0, extractor) +# matrix.tools.insert(1, extractor2) html_renderer = FileRenderer(Path("out.html")) console_renderer = ConsoleRenderer() renderer = MultiRenderer([html_renderer, console_renderer]) From 531a711b66c7120391a9f11f0e234d8a927af778 Mon Sep 17 00:00:00 2001 From: evaldasp Date: Mon, 6 May 2024 10:46:29 +0300 Subject: [PATCH 25/26] Fixed minor errors in update_bench_incremental.py and yamlindex.py --- gobexec/goblint/bench/yamlindex.py | 22 ++++++++++++++-------- update_bench_incremental.py | 5 ++++- 2 files changed, 18 insertions(+), 9 deletions(-) diff --git a/gobexec/goblint/bench/yamlindex.py b/gobexec/goblint/bench/yamlindex.py index e9af60e..717d748 100644 --- a/gobexec/goblint/bench/yamlindex.py +++ b/gobexec/goblint/bench/yamlindex.py @@ -22,26 +22,32 @@ def __call__(self, name: str, args: List[str]) -> Tool[Incremental, R]: def load(def_path: Path, set_path: List[Path], tool_factory: ToolFactory) -> Matrix[Incremental, R]: defsets_ = DefSets.from_paths(def_path, set_path) groups: List[Group[Incremental]] = [] - tool: Tool[Incremental,R] = tool_factory(name= "",args=defsets_.def_.confs) + tools: [Tool[Incremental, R]] = [] for set_ in defsets_.sets: groups.append(Group(name=set_.name, benchmarks=[])) for bench in set_.benchmarks: - patch_path = Path("../bench")/bench.path.with_suffix("."+"patch") + patch_path = Path("../bench") / bench.path.with_suffix("." + "patch") parts = list(patch_path.parts) temp = parts[3].split(".") - parts[3] = temp[0]+"01."+temp[1] + parts[3] = temp[0] + "01." + temp[1] patch_path = Path(*parts) groups[-1].benchmarks.append(Incremental( name=bench.name, description=bench.info, - files=Path("../bench")/bench.path, - patch= patch_path, + files=Path("../bench") / bench.path, + patch=patch_path, tool_data={ - ARGS_TOOL_KEY: shlex.split(bench.param) if bench.param else [] - })) + ARGS_TOOL_KEY: shlex.split(bench.param) if bench.param else [] + })) + for conf in defsets_.def_.confs[1:]: + if conf.param is not None: + tools.append(tool_factory(name=conf.name,args= ["--conf", (Path("../bench") / Path(defsets_.def_.baseconf)).absolute()] + shlex.split(conf.param) )) + else: + tools.append(tool_factory(name=conf.name, args=["--conf", (Path("../bench") / Path(defsets_.def_.baseconf)).absolute()])) + return Matrix( name=def_path.stem, - tools=[tool], + tools=tools, groups=groups, ) diff --git a/update_bench_incremental.py b/update_bench_incremental.py index 1812b17..99fe03c 100644 --- a/update_bench_incremental.py +++ b/update_bench_incremental.py @@ -16,6 +16,7 @@ from_scratch = GoblintToolFromScratch( name="from_scratch", program=str(Path("../analyzer/goblint").absolute()), + args=["--conf", Path("../bench/index/conf/td3.json").absolute()] ) @@ -24,7 +25,9 @@ def index_tool_factory(name, args): incremental = GoblintToolIncremental( name=name, program=str(Path("../analyzer/goblint").absolute()), - from_scratch=from_scratch + from_scratch=from_scratch, + args=args + ) return ExtractTool( incremental, From 6e373d567a84d88f9f3759a5bf4ff56b51bcc191 Mon Sep 17 00:00:00 2001 From: evaldasp Date: Mon, 13 May 2024 23:52:54 +0300 Subject: [PATCH 26/26] Fixed minor errors in update_bench_traces_rel_assert.py and update_bench_traces_rel_yaml.py --- update_bench_traces_rel_assert.py | 4 ++-- update_bench_traces_rel_yaml.py | 7 ++++--- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/update_bench_traces_rel_assert.py b/update_bench_traces_rel_assert.py index 5b42b47..799b359 100644 --- a/update_bench_traces_rel_assert.py +++ b/update_bench_traces_rel_assert.py @@ -12,7 +12,7 @@ goblint_assert = GoblintTool( name="goblint_assert", program=str(Path("../analyzer/goblint").absolute()), - args=["-v", "--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug","--set", "trans.activated[+]", "assert", + args=["-v", "--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "warn.debug","--set", "trans.activated[+]", "assert", "--set" ,"ana.activated[+]" ,"apron" ,"--set" ,"ana.path_sens[+]" ,"threadflag", "--set" ,"ana.relation.privatization", "mutex-meet-tid-cluster12"], dump = "assert" ) @@ -21,7 +21,7 @@ def index_tool_factory(name, args): goblint = GoblintTool( name=name, program=str(Path("../analyzer/goblint").absolute()), - args=["-v", "--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug"] + args, + args=["-v", "--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "warn.debug"] + args, dump= 'apron', assertion = goblint_assert ) diff --git a/update_bench_traces_rel_yaml.py b/update_bench_traces_rel_yaml.py index ffe0e1e..70d1fe8 100644 --- a/update_bench_traces_rel_yaml.py +++ b/update_bench_traces_rel_yaml.py @@ -12,8 +12,9 @@ goblint_witness = GoblintTool( name="witness_gen", program=str(Path("../analyzer/goblint").absolute()), - args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug", "--enable", - "witness.yaml.enabled"], + args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "warn.debug", "--enable", + "witness.yaml.enabled","--set" ,"ana.activated[+]" ,"apron" ,"--set" ,"ana.path_sens[+]" ,"threadflag", "--set" ,"ana.relation.privatization", "mutex-meet-tid-cluster12", + "--set", "witness.yaml.entry-types[-]", "invariant_set"], dump='witness' ) @@ -23,7 +24,7 @@ def index_tool_factory(name, args): goblint = GoblintTool( name=name, program=str(Path("../analyzer/goblint").absolute()), - args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "dbg.debug"] + args, + args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "warn.debug"] + args, dump='apron', validate= goblint_witness )