Adapt existing Ruby scripts to Python framework

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

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,22 +55,29 @@ 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],
                 *args[1:],
                 # 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'))

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>

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])

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)
+gobexec.main.run(matrix, renderer)