Merge pull request #17 from healthypunk/master

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/bench/yamlindex.py

@@ -1,11 +1,57 @@
+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]] = []
+    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")
+            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=Path("../bench") / bench.path,
+                patch=patch_path,
+                tool_data={
+                    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=tools,
+        groups=groups,
+    )
+
+
 @dataclass
 class Benchmark:
     name: str

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,163 @@ 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))
+
+
+@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))