Merge pull request #1 from healthypunk/concrat

Added update_bench_concrat.py script

gobexec/goblint/result.py

@@ -69,7 +69,6 @@ def kind(self):
             return ResultKind.WARNING
 
 
-
 @dataclass(init=False)
 class Rusage(Result):
     rusage: resource.struct_rusage
@@ -85,6 +84,7 @@ def template(self, env):
     async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'Rusage':
         return Rusage(cp.rusage)
 
+
 @dataclass(init=False)
 class LineSummary(Result):
     live: int
@@ -105,7 +105,7 @@ async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'LineSu
         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)
+            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)
@@ -123,7 +123,7 @@ 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.max_protected = max_protected
         self.sum_protected = sum_protected
         self.mutexes_count = mutexes_count
 
@@ -133,57 +133,94 @@ def template(self, env):
     @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 = 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 = 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 = 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 = 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 = 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)
+        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):
+    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':
+    async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'AssertTypeSummary':
         stdout = cp.stdout.decode("utf-8")
-        success = len(re.findall(r"\[Success\]\[Assert\]",stdout))
+        success = len(re.findall(r"\[Success\]\[Assert\]", stdout))
+
+        unknown = len(re.findall(r"\[Warning\]\[Assert\]", stdout))
+        return AssertTypeSummary(success, unknown)
 
-        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):
+    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':
+    async def extract(ec: ExecutionContext[Any], cp: CompletedSubprocess) -> 'AssertTypeSummary':
         stdout = cp.stdout.decode("utf-8")
-        confirmed = re.search(r"  confirmed:[ ]*([0-9]*)",stdout)
+        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 = re.search(r"  unconfirmed:[ ]*([0-9]*)", stdout)
         unconfirmed = 0 if unconfirmed is None else unconfirmed.group(1)
-        return AssertTypeSummary(int(confirmed),int(unconfirmed))
+        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):
+        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/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>

update_bench_concrat.py

@@ -0,0 +1,29 @@
+from pathlib import Path
+
+import gobexec.main
+from gobexec.goblint.bench import txtindex
+from gobexec.goblint.result import ConcratSummary
+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()),
+    )
+
+    return ExtractTool(
+        goblint,
+        TimeResult,
+        ConcratSummary,
+    )
+
+matrix = txtindex.load(Path("../bench/index/concrat.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)