From 15fff27593880eb5700e8a2cb3dc591059fb3e26 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 3 May 2023 16:15:04 +0300 Subject: [PATCH 01/15] Reduce default job count --- gobexec/main.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gobexec/main.py b/gobexec/main.py index 916acd0..c12648c 100644 --- a/gobexec/main.py +++ b/gobexec/main.py @@ -14,7 +14,7 @@ async def main(): data_path = Path("out") data_path.mkdir(parents=True, exist_ok=True) - cpu_sem = asyncio.BoundedSemaphore(14) + cpu_sem = asyncio.BoundedSemaphore(10) ec = RootExecutionContext(data_path, cpu_sem, rusage_child_watcher) result = await matrix.execute(ec, lambda: renderer.render(result, ec.progress)) # tying the knot! await result.join() From 77e2489581fde2d18400a251400c698ec9a564ba Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 3 May 2023 16:15:33 +0300 Subject: [PATCH 02/15] Add missing update_bench_traces args --- update_bench_traces.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/update_bench_traces.py b/update_bench_traces.py index 384f136..6b19344 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", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, dump= "priv" ) From 5f8b45422b5816df2205e3d8dca675a47fbcb80d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 3 May 2023 16:15:48 +0300 Subject: [PATCH 03/15] Fix PrivPrecTool output path --- gobexec/goblint/tool.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index 584d736..0931375 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -91,7 +91,7 @@ async def run_async(self, ec: ExecutionContext[Single], benchmark: Single) -> Pr 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: + with(path / '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], From 9bca4cc5d1c7cd4b0d63d3502aa695117b25051d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 3 May 2023 16:15:59 +0300 Subject: [PATCH 04/15] Fix PrivPrecTool input path arguments --- gobexec/goblint/tool.py | 1 + 1 file changed, 1 insertion(+) diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py index 0931375..9338e32 100644 --- a/gobexec/goblint/tool.py +++ b/gobexec/goblint/tool.py @@ -95,6 +95,7 @@ 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, From ae5c8285b95082b53298f13cb4214fc33aaae14f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 3 May 2023 16:31:23 +0300 Subject: [PATCH 05/15] Add missing update_bench_traces_rel* args --- udpate_bench_traces_rel_toy.py | 2 +- update_bench_traces_rel.py | 2 +- update_bench_traces_rel_assert.py | 64 +++++++++++++++---------------- update_bench_traces_rel_ratcop.py | 2 +- update_bench_traces_rel_watts.py | 2 +- update_bench_traces_rel_yaml.py | 2 +- 6 files changed, 37 insertions(+), 37 deletions(-) diff --git a/udpate_bench_traces_rel_toy.py b/udpate_bench_traces_rel_toy.py index 995dee8..9505a87 100644 --- a/udpate_bench_traces_rel_toy.py +++ b/udpate_bench_traces_rel_toy.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-rel-toy.json").absolute()), "--enable", "dbg.debug"] + args, + args=["--conf", str(Path("../analyzer/conf/traces-rel-toy.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, dump= 'apron' ) diff --git a/update_bench_traces_rel.py b/update_bench_traces_rel.py index 9a325de..e97950a 100644 --- a/update_bench_traces_rel.py +++ b/update_bench_traces_rel.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-rel.json").absolute()), "--enable", "dbg.debug"] + args, + args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, dump= 'apron' ) diff --git a/update_bench_traces_rel_assert.py b/update_bench_traces_rel_assert.py index 5c6638d..9741703 100644 --- a/update_bench_traces_rel_assert.py +++ b/update_bench_traces_rel_assert.py @@ -1,33 +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=["-v", "--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]) - +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=["-v", "--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + 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 index 544777b..589e320 100644 --- a/update_bench_traces_rel_ratcop.py +++ b/update_bench_traces_rel_ratcop.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-rel.json").absolute()), "--enable", "dbg.debug"] + args, + args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, dump= 'apron' ) diff --git a/update_bench_traces_rel_watts.py b/update_bench_traces_rel_watts.py index d95af80..b0f31d9 100644 --- a/update_bench_traces_rel_watts.py +++ b/update_bench_traces_rel_watts.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-rel.json").absolute()), "--enable", "dbg.debug"] + args, + args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, ) assert_summary_extractor = AssertSummaryExtractor(assert_counter) return ExtractTool( diff --git a/update_bench_traces_rel_yaml.py b/update_bench_traces_rel_yaml.py index 7fdf527..9bd9611 100644 --- a/update_bench_traces_rel_yaml.py +++ b/update_bench_traces_rel_yaml.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=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, dump= 'apron', validate= True ) From 6858a7f77a84403c33efd93faf8fd890a9af845b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 3 May 2023 16:59:14 +0300 Subject: [PATCH 06/15] Remove AssertTypeSummary usage --- udpate_bench_traces_rel_toy.py | 66 +++++++++++++++---------------- update_bench_traces_rel_assert.py | 5 ++- 2 files changed, 36 insertions(+), 35 deletions(-) diff --git a/udpate_bench_traces_rel_toy.py b/udpate_bench_traces_rel_toy.py index 9505a87..27f7c6d 100644 --- a/udpate_bench_traces_rel_toy.py +++ b/udpate_bench_traces_rel_toy.py @@ -1,34 +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", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + 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]) - +from pathlib import Path + +import gobexec.main +from gobexec.goblint import tool +from gobexec.goblint.bench import txtindex +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 + + +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", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, + dump= 'apron' + ) + + return ExtractTool( + goblint, + TimeResult, + AssertSummaryExtractor(), + + ) + +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_rel_assert.py b/update_bench_traces_rel_assert.py index 9741703..026eba8 100644 --- a/update_bench_traces_rel_assert.py +++ b/update_bench_traces_rel_assert.py @@ -2,7 +2,7 @@ import gobexec.main from gobexec.goblint.bench import txtindex -from gobexec.goblint.result import AssertTypeSummary +from gobexec.goblint.extractor import AssertSummaryExtractor from gobexec.goblint.tool import GoblintTool from gobexec.model.result import TimeResult @@ -21,7 +21,8 @@ def index_tool_factory(name, args): return ExtractTool( goblint, TimeResult, - AssertTypeSummary, + # TODO: indicate failed via crash + AssertSummaryExtractor(), ) From 0375d24a77219184bc4f9a167cb90aa11f197fa8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 3 May 2023 16:59:43 +0300 Subject: [PATCH 07/15] Remove Apron dumping when not comparing --- udpate_bench_traces_rel_toy.py | 1 - update_bench_traces_rel_assert.py | 1 - update_bench_traces_rel_ratcop.py | 67 +++++++++++++++---------------- update_bench_traces_rel_yaml.py | 65 +++++++++++++++--------------- 4 files changed, 65 insertions(+), 69 deletions(-) diff --git a/udpate_bench_traces_rel_toy.py b/udpate_bench_traces_rel_toy.py index 27f7c6d..3f6c831 100644 --- a/udpate_bench_traces_rel_toy.py +++ b/udpate_bench_traces_rel_toy.py @@ -16,7 +16,6 @@ def index_tool_factory(name, args): name=name, program=str(Path("../analyzer/goblint").absolute()), args=["--conf", str(Path("../analyzer/conf/traces-rel-toy.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, - dump= 'apron' ) return ExtractTool( diff --git a/update_bench_traces_rel_assert.py b/update_bench_traces_rel_assert.py index 026eba8..4a34e3d 100644 --- a/update_bench_traces_rel_assert.py +++ b/update_bench_traces_rel_assert.py @@ -15,7 +15,6 @@ def index_tool_factory(name, args): name=name, program=str(Path("../analyzer/goblint").absolute()), args=["-v", "--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, - dump= 'apron' ) return ExtractTool( diff --git a/update_bench_traces_rel_ratcop.py b/update_bench_traces_rel_ratcop.py index 589e320..6e55d14 100644 --- a/update_bench_traces_rel_ratcop.py +++ b/update_bench_traces_rel_ratcop.py @@ -1,35 +1,34 @@ -from pathlib import Path - -import gobexec.main -from gobexec.goblint.bench import txtindex -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 -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", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, - dump= 'apron' - ) - - return ExtractTool( - goblint, - TimeResult, - LineSummary, - AssertSummaryExtractor(), - - ) - -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]) - +from pathlib import Path + +import gobexec.main +from gobexec.goblint.bench import txtindex +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 +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", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, + ) + + return ExtractTool( + goblint, + TimeResult, + LineSummary, + AssertSummaryExtractor(), + + ) + +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_yaml.py b/update_bench_traces_rel_yaml.py index 9bd9611..5a13604 100644 --- a/update_bench_traces_rel_yaml.py +++ b/update_bench_traces_rel_yaml.py @@ -1,34 +1,33 @@ -from pathlib import Path - -import gobexec.main -from gobexec.goblint.bench import txtindex -from gobexec.goblint.result import AssertTypeSummary, YamlSummary -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", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, - dump= 'apron', - validate= True - ) - - return ExtractTool( - goblint, - TimeResult, - YamlSummary, - - ) - -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]) - +from pathlib import Path + +import gobexec.main +from gobexec.goblint.bench import txtindex +from gobexec.goblint.result import AssertTypeSummary, YamlSummary +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", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, + validate= True + ) + + return ExtractTool( + goblint, + TimeResult, + YamlSummary, + + ) + +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 663d9a99a785c1ecda3283fcd0e5259bb9fbb65a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 3 May 2023 17:00:07 +0300 Subject: [PATCH 08/15] Add TODOs to update_bench_traces* scripts --- udpate_bench_traces_rel_toy.py | 2 ++ update_bench_traces.py | 1 + update_bench_traces_rel.py | 3 +++ update_bench_traces_rel_assert.py | 2 ++ update_bench_traces_rel_ratcop.py | 2 ++ update_bench_traces_rel_watts.py | 3 +++ update_bench_traces_rel_yaml.py | 2 ++ 7 files changed, 15 insertions(+) diff --git a/udpate_bench_traces_rel_toy.py b/udpate_bench_traces_rel_toy.py index 3f6c831..650c642 100644 --- a/udpate_bench_traces_rel_toy.py +++ b/udpate_bench_traces_rel_toy.py @@ -25,6 +25,8 @@ def index_tool_factory(name, args): ) +# TODO: HTML columns broken + matrix = txtindex.load(Path("../bench/index/traces-rel-toy.txt").absolute(),index_tool_factory) html_renderer = FileRenderer(Path("out.html")) console_renderer = ConsoleRenderer() diff --git a/update_bench_traces.py b/update_bench_traces.py index 6b19344..cc34854 100644 --- a/update_bench_traces.py +++ b/update_bench_traces.py @@ -22,6 +22,7 @@ def index_tool_factory(name, args): return ExtractTool( goblint, TimeResult, + # TODO: uncalled functions LineSummary, #PrivPrecResult diff --git a/update_bench_traces_rel.py b/update_bench_traces_rel.py index e97950a..c08130e 100644 --- a/update_bench_traces_rel.py +++ b/update_bench_traces_rel.py @@ -23,10 +23,13 @@ def index_tool_factory(name, args): goblint, TimeResult, ThreadSummary, + # TODO: average protecting #PrivPrecResult ) +# TODO: separate precision dump run to exclude dumping time + matrix = txtindex.load(Path("../bench/index/traces-relational.txt").absolute(),index_tool_factory) apronprec = tool.ApronPrecTool(args= matrix.tools.copy()) matrix.tools.append(apronprec) diff --git a/update_bench_traces_rel_assert.py b/update_bench_traces_rel_assert.py index 4a34e3d..ad5a448 100644 --- a/update_bench_traces_rel_assert.py +++ b/update_bench_traces_rel_assert.py @@ -25,6 +25,8 @@ def index_tool_factory(name, args): ) +# TODO: HTML columns broken + matrix = txtindex.load(Path("../bench/index/traces-rel-assert.txt").absolute(),index_tool_factory) html_renderer = FileRenderer(Path("out.html")) console_renderer = ConsoleRenderer() diff --git a/update_bench_traces_rel_ratcop.py b/update_bench_traces_rel_ratcop.py index 6e55d14..5d67dc6 100644 --- a/update_bench_traces_rel_ratcop.py +++ b/update_bench_traces_rel_ratcop.py @@ -26,6 +26,8 @@ def index_tool_factory(name, args): ) +# TODO: HTML columns broken + matrix = txtindex.load(Path("../bench/index/traces-rel-ratcop.txt").absolute(),index_tool_factory) html_renderer = FileRenderer(Path("out.html")) console_renderer = ConsoleRenderer() diff --git a/update_bench_traces_rel_watts.py b/update_bench_traces_rel_watts.py index b0f31d9..9bc63c3 100644 --- a/update_bench_traces_rel_watts.py +++ b/update_bench_traces_rel_watts.py @@ -24,6 +24,9 @@ def index_tool_factory(name, args): assert_summary_extractor, primary=assert_summary_extractor ) + +# TODO: add asserts etc totals to HTML + matrix = txtindex.load(Path("../bench/index/traces-relational-watts.txt").absolute(), index_tool_factory) matrix.tools.insert(0, assert_counter) diff --git a/update_bench_traces_rel_yaml.py b/update_bench_traces_rel_yaml.py index 5a13604..14333cf 100644 --- a/update_bench_traces_rel_yaml.py +++ b/update_bench_traces_rel_yaml.py @@ -25,6 +25,8 @@ def index_tool_factory(name, args): ) +# TODO: HTML columns broken + matrix = txtindex.load(Path("../bench/index/traces-rel-yaml.txt").absolute(),index_tool_factory) html_renderer = FileRenderer(Path("out.html")) console_renderer = ConsoleRenderer() From 3a507735686221e11215098b38fbf292ccc55fe4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 3 May 2023 17:17:04 +0300 Subject: [PATCH 09/15] Fix update_bench_traces_rel_toy name --- udpate_bench_traces_rel_toy.py => update_bench_traces_rel_toy.py | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename udpate_bench_traces_rel_toy.py => update_bench_traces_rel_toy.py (100%) diff --git a/udpate_bench_traces_rel_toy.py b/update_bench_traces_rel_toy.py similarity index 100% rename from udpate_bench_traces_rel_toy.py rename to update_bench_traces_rel_toy.py From 984bbd36e93cae4b5fb9eb765ab643203a6b5009 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 29 Apr 2024 12:13:31 +0000 Subject: [PATCH 10/15] Fix dbg.debug -> warn.debug in Goblint options --- test.py | 4 ++-- update_bench_traces_rel.py | 2 +- update_bench_traces_rel_assert.py | 4 ++-- update_bench_traces_rel_ratcop.py | 2 +- update_bench_traces_rel_toy.py | 2 +- update_bench_traces_rel_watts.py | 2 +- update_bench_traces_rel_yaml.py | 4 ++-- 7 files changed, 10 insertions(+), 10 deletions(-) diff --git a/test.py b/test.py index 06ad73f..530e52a 100644 --- a/test.py +++ b/test.py @@ -21,8 +21,8 @@ def index_tool_factory(name, args): goblint = GoblintTool( name=name, 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"], + args=["--conf", "../analyzer/conf/traces-rel-toy.json", "--enable", "warn.debug"] + args, + # args=["--conf", "/home/simmo/dev/goblint/sv-comp/goblint/conf/traces-rel.json", "--enable", "warn.debug"], ) assert_summary_extractor = AssertSummaryExtractor(assert_counter) return ExtractTool( diff --git a/update_bench_traces_rel.py b/update_bench_traces_rel.py index c08130e..733e022 100644 --- a/update_bench_traces_rel.py +++ b/update_bench_traces_rel.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-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, + args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "warn.debug", "-v"] + args, dump= 'apron' ) diff --git a/update_bench_traces_rel_assert.py b/update_bench_traces_rel_assert.py index 2767fec..4257908 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", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, + args=["-v", "--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "warn.debug", "-v"] + args, dump= 'apron', assertion = goblint_assert ) diff --git a/update_bench_traces_rel_ratcop.py b/update_bench_traces_rel_ratcop.py index 5d67dc6..b161062 100644 --- a/update_bench_traces_rel_ratcop.py +++ b/update_bench_traces_rel_ratcop.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-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, + args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "warn.debug", "-v"] + args, ) return ExtractTool( diff --git a/update_bench_traces_rel_toy.py b/update_bench_traces_rel_toy.py index 650c642..1bc5da9 100644 --- a/update_bench_traces_rel_toy.py +++ b/update_bench_traces_rel_toy.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-rel-toy.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, + args=["--conf", str(Path("../analyzer/conf/traces-rel-toy.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "warn.debug", "-v"] + args, ) return ExtractTool( diff --git a/update_bench_traces_rel_watts.py b/update_bench_traces_rel_watts.py index 9bc63c3..52f160d 100644 --- a/update_bench_traces_rel_watts.py +++ b/update_bench_traces_rel_watts.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-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, + args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "warn.debug", "-v"] + args, ) assert_summary_extractor = AssertSummaryExtractor(assert_counter) return ExtractTool( diff --git a/update_bench_traces_rel_yaml.py b/update_bench_traces_rel_yaml.py index 0a357b9..a8b19e3 100644 --- a/update_bench_traces_rel_yaml.py +++ b/update_bench_traces_rel_yaml.py @@ -12,7 +12,7 @@ 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", + args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "warn.debug", "--enable", "witness.yaml.enabled"], dump='witness' @@ -23,7 +23,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", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "dbg.debug", "-v"] + args, + args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "warn.debug", "-v"] + args, dump='apron', validate=goblint_witness ) From 0ae91fea792a0fbcce576f72980281890c09ba2a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 29 Apr 2024 12:15:26 +0000 Subject: [PATCH 11/15] Uncomment HTML progress auto-refresh --- gobexec/output/html/templates/progress.jinja | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gobexec/output/html/templates/progress.jinja b/gobexec/output/html/templates/progress.jinja index f479d14..ed9b70d 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 %}

From 9c402a4d11c4bd15e8d6c82853beacb3e2af5459 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 29 Apr 2024 12:49:32 +0000 Subject: [PATCH 12/15] Add some TODOs to traces_rel* --- update_bench_traces_rel.py | 1 + update_bench_traces_rel_assert.py | 1 + update_bench_traces_rel_watts.py | 1 + 3 files changed, 3 insertions(+) diff --git a/update_bench_traces_rel.py b/update_bench_traces_rel.py index 733e022..244420e 100644 --- a/update_bench_traces_rel.py +++ b/update_bench_traces_rel.py @@ -22,6 +22,7 @@ def index_tool_factory(name, args): return ExtractTool( goblint, TimeResult, + # TODO: total logical lines ThreadSummary, # TODO: average protecting #PrivPrecResult diff --git a/update_bench_traces_rel_assert.py b/update_bench_traces_rel_assert.py index 4257908..6121d0f 100644 --- a/update_bench_traces_rel_assert.py +++ b/update_bench_traces_rel_assert.py @@ -36,6 +36,7 @@ def index_tool_factory(name, args): # TODO: HTML columns broken +# TODO index/traces-rel-assert.txt has fewer, but need original paths from yaml for transformation 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")) diff --git a/update_bench_traces_rel_watts.py b/update_bench_traces_rel_watts.py index 52f160d..bf3462e 100644 --- a/update_bench_traces_rel_watts.py +++ b/update_bench_traces_rel_watts.py @@ -21,6 +21,7 @@ def index_tool_factory(name, args): return ExtractTool( goblint, TimeResult, + # TODO: total logical lines assert_summary_extractor, primary=assert_summary_extractor ) From b4541630de5d012f606b8f5bd71def16f32ef9cf Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 29 Apr 2024 12:49:44 +0000 Subject: [PATCH 13/15] Remove Apron dumping when not comparing again --- update_bench_traces_rel_assert.py | 1 - update_bench_traces_rel_yaml.py | 1 - 2 files changed, 2 deletions(-) diff --git a/update_bench_traces_rel_assert.py b/update_bench_traces_rel_assert.py index 6121d0f..d77333b 100644 --- a/update_bench_traces_rel_assert.py +++ b/update_bench_traces_rel_assert.py @@ -22,7 +22,6 @@ def index_tool_factory(name, args): name=name, program=str(Path("../analyzer/goblint").absolute()), args=["-v", "--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "warn.debug", "-v"] + args, - dump= 'apron', assertion = goblint_assert ) diff --git a/update_bench_traces_rel_yaml.py b/update_bench_traces_rel_yaml.py index a8b19e3..ccb0d82 100644 --- a/update_bench_traces_rel_yaml.py +++ b/update_bench_traces_rel_yaml.py @@ -24,7 +24,6 @@ def index_tool_factory(name, args): name=name, program=str(Path("../analyzer/goblint").absolute()), args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "warn.debug", "-v"] + args, - dump='apron', validate=goblint_witness ) From 9fe2ecff5339dbef1d7c00253a969a37ff643bf8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 29 Apr 2024 14:02:16 +0000 Subject: [PATCH 14/15] Add witness generation precision arguments to traces_rel_yaml --- update_bench_traces_rel_yaml.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/update_bench_traces_rel_yaml.py b/update_bench_traces_rel_yaml.py index ccb0d82..585ef28 100644 --- a/update_bench_traces_rel_yaml.py +++ b/update_bench_traces_rel_yaml.py @@ -13,7 +13,7 @@ name="witness_gen", program=str(Path("../analyzer/goblint").absolute()), args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "warn.debug", "--enable", - "witness.yaml.enabled"], + "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' ) From b7bbf5526e0af229e402c01221aee5e55454aac8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 30 Apr 2024 16:16:16 +0300 Subject: [PATCH 15/15] Enable ana.sv-comp.functions for traces_rel_assert --- update_bench_traces_rel_assert.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/update_bench_traces_rel_assert.py b/update_bench_traces_rel_assert.py index d77333b..d19e41c 100644 --- a/update_bench_traces_rel_assert.py +++ b/update_bench_traces_rel_assert.py @@ -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", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "warn.debug", "-v"] + args, + args=["-v", "--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "ana.sv-comp.functions", "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "warn.debug", "-v"] + args, assertion = goblint_assert )