Merge pull request #23 from goblint/healthypunk-master-fix

Fix ported scripts
goblint · Jul 28, 2024 · c04103f · c04103f
2 parents e033a69 + aefe3c2
commit c04103f
Show file tree

Hide file tree

Showing 11 changed files with 100 additions and 87 deletions.
diff --git a/gobexec/goblint/tool.py b/gobexec/goblint/tool.py
@@ -123,8 +123,7 @@ def __init__(self,
         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)
@@ -195,10 +194,11 @@ 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],
+                *args[1:],
                 stdout=out_file,
                 stderr=asyncio.subprocess.STDOUT,
 

diff --git 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()

diff --git 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() }}
-    {#<meta http-equiv="refresh" content="1">#}
+    <meta http-equiv="refresh" content="1">
 {% endblock %}
 {% block body %}
     <p>

diff --git 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.py b/update_bench_traces.py
@@ -15,13 +15,14 @@ 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", "warn.debug"] + args,
+        args=["--conf", str(Path("../analyzer/conf/traces.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "warn.debug", "-v"] + args,
         dump= "priv"
     )
 
     return ExtractTool(
         goblint,
         TimeResult,
+        # TODO: uncalled functions
         LineSummary,
         #PrivPrecResult
 

diff --git a/update_bench_traces_rel.py b/update_bench_traces_rel.py
@@ -15,18 +15,22 @@ 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", "warn.debug", "-v"] + args,
         dump= 'apron'
     )
 
     return ExtractTool(
         goblint,
         TimeResult,
+        # TODO: total logical lines
         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
@@ -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,18 +21,21 @@ 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", "warn.debug"] + args,
-        dump= 'apron',
+        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
     )
 
     return ExtractTool(
         goblint,
         TimeResult,
-        AssertTypeSummary,
+        # TODO: indicate failed via crash
+        AssertSummaryExtractor(),
 
     )
 
+# 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_ratcop.py b/update_bench_traces_rel_ratcop.py
@@ -1,35 +1,36 @@
-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", "dbg.debug"] + 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", "warn.debug", "-v"] + args,
+    )
+
+    return ExtractTool(
+        goblint,
+        TimeResult,
+        LineSummary,
+        AssertSummaryExtractor(),
+
+    )
+
+# 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()
+renderer = MultiRenderer([html_renderer, console_renderer])
+
 gobexec.main.run(matrix, renderer)
diff --git a/udpate_bench_traces_rel_toy.py → update_bench_traces_rel_toy.py b/udpate_bench_traces_rel_toy.py → update_bench_traces_rel_toy.py
@@ -1,34 +1,35 @@
-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])
-
+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", "warn.debug", "-v"] + args,
+    )
+
+    return ExtractTool(
+        goblint,
+        TimeResult,
+        AssertSummaryExtractor(),
+
+    )
+
+# 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()
+renderer = MultiRenderer([html_renderer, console_renderer])
+
 gobexec.main.run(matrix, renderer)
diff --git a/update_bench_traces_rel_watts.py b/update_bench_traces_rel_watts.py
@@ -15,15 +15,19 @@ 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", "warn.debug", "-v"] + args,
     )
     assert_summary_extractor = AssertSummaryExtractor(assert_counter)
     return ExtractTool(
         goblint,
         TimeResult,
+        # TODO: total logical lines
         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
@@ -13,8 +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","--set" ,"ana.activated[+]" ,"apron" ,"--set" ,"ana.path_sens[+]" ,"threadflag", "--set" ,"ana.relation.privatization", "mutex-meet-tid-cluster12",
-          "--set", "witness.yaml.entry-types[-]", "invariant_set"],
+          "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'
 
 )
@@ -24,9 +23,8 @@ 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", "warn.debug"] + args,
-        dump='apron',
-        validate= goblint_witness
+        args=["--conf", str(Path("../analyzer/conf/traces-rel.json").absolute()), "--enable", "allglobs", "--enable", "dbg.timing.enabled", "--enable", "warn.debug", "-v"] + args,
+        validate=goblint_witness
     )
 
     return ExtractTool(
@@ -36,11 +34,12 @@ def index_tool_factory(name, args):
 
     )
 
+# TODO: HTML columns broken
 
 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)
+gobexec.main.run(matrix, renderer)