diff --git a/gobexec/goblint/result.py b/gobexec/goblint/result.py index 00778da..eec63d8 100644 --- a/gobexec/goblint/result.py +++ b/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,18 +133,18 @@ 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) @@ -152,7 +152,7 @@ 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 @@ -160,19 +160,20 @@ 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 @@ -180,10 +181,46 @@ 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)) \ No newline at end of file + 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)) diff --git a/gobexec/output/html/templates/concratresult.jinja b/gobexec/output/html/templates/concratresult.jinja new file mode 100644 index 0000000..853f726 --- /dev/null +++ b/gobexec/output/html/templates/concratresult.jinja @@ -0,0 +1,4 @@ +{{this.safe}} +{{this.vulnerable}} +{{this.unsafe}} +{{this.uncalled}} \ No newline at end of file diff --git a/update_bench_concrat.py b/update_bench_concrat.py new file mode 100644 index 0000000..da159c7 --- /dev/null +++ b/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) \ No newline at end of file