Adapt existing Ruby scripts to Python framework

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

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
@@ -25,4 +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)
+        return AssertSummary(success, warning, error, unreachable)

gobexec/goblint/result.py

@@ -12,6 +12,7 @@ class RaceSummary(Result):
     safe: int
     vulnerable: int
     unsafe: int
+
     # total: int
 
     def __init__(self,
@@ -91,3 +92,144 @@ 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")
+
+    @staticmethod
+    async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'LineSummary':
+        stdout = cp.stdout.decode("utf-8")
+        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)
+
+
+@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)
+
+
+@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)
+
+
+@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))
+
+
+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) -> None:
+        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))

gobexec/goblint/tool.py

@@ -1,9 +1,10 @@
 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
+from gobexec.model.result import PrivPrecResult, ApronPrecResult
 from gobexec.model.tool import Tool
 
 ARGS_TOOL_KEY = "goblint-args"
@@ -13,17 +14,27 @@ class GoblintTool(Tool[Single, CompletedSubprocess]):
     name: str
     program: str
     args: List[str]
+    dump: str
+    validate: Optional["GoblintTool"]
+    assertion: Optional["GoblintTool"]
 
     def __init__(self,
                  name: str = "Goblint",
                  program: str = "goblint",
-                 args: List[str] = None
+                 args: List[str] = None,
+                 dump: str = '',
+                 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)
@@ -44,15 +55,88 @@ 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]
-            # print(args)
+                   [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"]
+            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
+                stderr=asyncio.subprocess.STDOUT,
+                cwd=benchmark.files[0].parent
             )
             out_file.seek(0)
             cp.stdout = out_file.read()  # currently for extractors
             return cp
+
+
+class PrivPrecTool(Tool[Single, PrivPrecResult]):
+    name: str
+    program: str
+    args: List[GoblintTool]
+
+    def __init__(self,
+                 name: str = "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)
+        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(
+                args[0],
+                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)
+        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(
+                args[0],
+                *args[1:],
+                stdout=out_file,
+                stderr=asyncio.subprocess.STDOUT,
+            )
+            return ApronPrecResult(str(path / 'out.txt'))

gobexec/model/result.py

@@ -99,3 +99,25 @@ def kind(self):
             return self.primary.kind
         else:
             return ResultKind.DEFAULT
+
+@dataclass(init=False)
+class PrivPrecResult(Result):
+    result_path: str
+
+    def __init__(self, result_path: str) -> None:
+        self.result_path = result_path
+
+    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')
+

gobexec/output/html/templates/apronprecresult.jinja

@@ -0,0 +1 @@
+<a href="{{this.result_path}}" target="_blank">compare</a>

gobexec/output/html/templates/asserttypesummary.jinja

@@ -0,0 +1,2 @@
+<span class="success" title="success" color="green">{{ this.success }}</span>,
+<span class="warning" title="warning" color="orange">{{ this.unknown }}</span>

gobexec/output/html/templates/concratresult.jinja

@@ -0,0 +1,4 @@
+<span class="safe"  style="color:green">{{this.safe}}</span>
+<span class="vulnerable"  style="color:orange">{{this.vulnerable}}</span>
+<span class="unsafe" style="color: red">{{this.unsafe}}</span>
+<span class="uncalled" style="color: magenta">{{this.uncalled}}</span>

gobexec/output/html/templates/linesummary.jinja

@@ -0,0 +1,3 @@
+<span class="live" title= "live lines" style="color:green">{{this.live}}</span>
+<span class="dead" title= "dead lines" style="color:red">{{this.dead}}</span>
+<span class="total" title= "total lines">{{this.total}}</span>