From acb433c8c4dc22521446001739f03d4455985240 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dominic=20H=C3=B6glinger?= Date: Sun, 20 Nov 2022 21:47:31 +0100 Subject: [PATCH] cleanup of dead code and comments, minor refactoring --- analyze.py | 117 +++++++++++------------------------------------- model.smv | 3 ++ modelbuilder.py | 3 ++ 3 files changed, 33 insertions(+), 90 deletions(-) diff --git a/analyze.py b/analyze.py index 2a557dc..a64f821 100644 --- a/analyze.py +++ b/analyze.py @@ -1,53 +1,20 @@ -#----------------------------------------------------------------- -# pycparser: dump_ast.py -# -# Basic example of parsing a file and dumping its parsed AST. -# -# Eli Bendersky [https://eli.thegreenplace.net/] -# License: BSD -#----------------------------------------------------------------- from __future__ import print_function import argparse import sys from modelbuilder import * -# This is not required if you've installed pycparser into -# your site-packages/ with setup.py -sys.path.extend(['.', '..']) - from pycparser import parse_file, c_ast func_table = {} enum_table = {} assign_table = [] - state_enums = [] -# A visitor with some state information (the funcname it's looking for) -class FuncCallVisitor(c_ast.NodeVisitor): - def __init__(self, funcname): - self.funcname = funcname - - def visit_FuncCall(self, node): - if node.name.name == self.funcname: - print('%s called at %s' % (self.funcname, node.name.coord)) - # Visit args in case they contain more func calls. - if node.args: - self.visit(node.args) - - -def show_func_calls(ast, funcname): - v = FuncCallVisitor(funcname) - v.visit(ast) - class FuncDefVisitor(c_ast.NodeVisitor): + def __init__(self): + self.func_table = {} def visit_FuncDef(self, node): - print('%s at %s' % (node.decl.name, node.decl.coord)) - func_table[node.decl.name] = node - -def show_func_defs(ast): - v = FuncDefVisitor() - v.visit(ast) + self.func_table[node.decl.name] = node class StateAssignmentVisitor(c_ast.NodeVisitor): def __init__(self, state): @@ -82,20 +49,8 @@ class StateAssignmentVisitor(c_ast.NodeVisitor): def visit_Assignment(self, n, path): rval_str = n.rvalue.name - #return '%s %s %s' % (self.visit(n.lvalue), n.op, rval_str) if rval_str == self.state: - if isinstance(n.lvalue, c_ast.StructRef): - print(f"found struct assignment '{n.lvalue.children()[0][1].name}->{n.lvalue.children()[1][1].name}'<='{rval_str}'") - else: - print(f"found assignment '{n.lvalue.name}'<='{rval_str}'") - print(" -> at path '",end="") - for p in path: - print(p.__class__.__name__,end=",") - print("'") self.assignments.append((n,path)) - #print("+++") - #n.show() - #print("---") class EnumDefVisitor(c_ast.NodeVisitor): def __init__(self, name): @@ -103,15 +58,10 @@ class EnumDefVisitor(c_ast.NodeVisitor): self._name = name def visit_Enum(self, node): - print('enum %s at %s' % (node.name, node.coord)) enum_table[self._name] = node class TypedefVisitor(c_ast.NodeVisitor): def visit_Typedef(self, node): - print(f"typedef {node.name} at {node.coord}") - print(f"---") - node.children()[0][1].show() - print("+++") ev = EnumDefVisitor(node.name) ev.visit(node) @@ -122,7 +72,6 @@ class EnumVisitor(c_ast.NodeVisitor): self.enum_names = [] def visit_Enumerator(self, node): - #print('enumerator %s at %s' % (node.name, node.coord)) self.enum_names.append(node.name) def find_longest_path(paths): @@ -136,7 +85,7 @@ def find_longest_path(paths): return mp def find_shortest_path(paths): - ms = 9000 + ms = float('inf') mp = None for path in paths: s = len(path) @@ -184,7 +133,6 @@ class SwitchCaseTranVisitor(c_ast.NodeVisitor): sctv = SwitchCaseTermVisitor(self._asm_node) sctv.visit(node) if sctv.hit: - #print(f"Transition! {node.children()[0][1].name} -> {self._asm_node.rvalue.name}"); self.tran_table.append((node.children()[0][1].name, self._asm_node.rvalue.name)) class SwitchCasePropertyVisitor(c_ast.NodeVisitor): @@ -195,13 +143,11 @@ class SwitchCasePropertyVisitor(c_ast.NodeVisitor): def visit_Assignment(self, node): if not(node in self._sas): - #print("Property:", node) prop = None if isinstance(node.lvalue, c_ast.StructRef): prop = f"{node.lvalue.children()[0][1].name}->{node.lvalue.children()[1][1].name}<={node.rvalue.name}"; else: prop = f"{node.lvalue.name}<={node.rvalue.name}" - #print(f"found property '{prop}'") self.properties.append(prop) @@ -238,21 +184,13 @@ if __name__ == "__main__": args = argparser.parse_args() ast = parse_file(args.filename, use_cpp=False) - #ast.show(showcoord=args.coord) - show_func_defs(ast) - + + fdv = FuncDefVisitor() + fdv.visit(ast) + func_table = fdv.func_table + enumvis = TypedefVisitor() enumvis.visit(ast) - - #func_table[args.func].show(showcoord=args.coord) - - # for name,node in enum_table.items(): - # print(f"Enum '{name}'") - # print("---") - # node.show() - # print("+++") - # ev = EnumVisitor() - # ev.visit(node) state_asmts = [] @@ -264,56 +202,52 @@ if __name__ == "__main__": sav.visit(func_table[args.func]) state_asmts += sav.assignments else: - print(f"state enum '{args.enum}' not found") + print(f"Initial State Enum '{args.enum}' not found") paths = [] for asm in state_asmts: paths.append(asm[1]) common = find_common_ancestor(paths) - #print(f"common ancestor is {common}") - + tran_table = [] for sa in state_asmts: - #print(sa[0]) sctv = SwitchCaseTranVisitor(sa[0]) sctv.visit(common) tran_table += sctv.tran_table comp_tt = {} - print("Compacting Transition Table") + print("Transitions") for t in tran_table: print(f"{t[0]}->{t[1]}") if t[0] in comp_tt: comp_tt[t[0]].append(t[1]) else: comp_tt[t[0]] = [t[1]] - + print("") + pure_sa = [x[0] for x in state_asmts] - #print(pure_sa) states = comp_tt.keys() print("States: ", ",".join(states)) - + print("") + props_by_state = {} - print("Compact Table:") + print("Compact Transition Table:") for n,ms in comp_tt.items(): - print(n,end="->{") - for m in ms: - print(m,end=",") - print("}") + sstr = ','.join(ms) + print(f"{n}->{{{sstr}}}") # find properties sccpv = SwitchCaseCodePropertyVisitor(n, pure_sa) sccpv.visit(common) if len(sccpv.properties) > 0: props_by_state[n] = sccpv.properties - + print("") + properties = {} for state,props in props_by_state.items(): - #print(f"{state} properties:") for prop in props: - #print(f" - {prop}") if prop in properties: properties[prop].append(state) else: @@ -323,7 +257,8 @@ if __name__ == "__main__": for prop,pstates in properties.items(): ss = ','.join(pstates) print(f" - '{prop}' when {ss}") - + print("") + ltls = [] if args.ltlfile is not None: with open(args.ltlfile) as f: @@ -332,9 +267,11 @@ if __name__ == "__main__": mod = ModelBuilder(states, args.initial, comp_tt, properties, ltls=ltls) nusmv = mod.generate() - print("-------------------") - print(nusmv) if args.output is not None: with open(args.output, "wt") as f: n = f.write(nusmv) + else: + print("-------------------") + print(nusmv) + diff --git a/model.smv b/model.smv index 1829c4c..d1975f5 100644 --- a/model.smv +++ b/model.smv @@ -1,4 +1,7 @@ +------------------------------------------------------------------------ +-- Generated using Kripkomat +------------------------------------------------------------------------ MODULE main VAR state : { STATE_I,STATE_C,STATE_D,STATE_A,STATE_B }; diff --git a/modelbuilder.py b/modelbuilder.py index cc74307..c213626 100644 --- a/modelbuilder.py +++ b/modelbuilder.py @@ -1,5 +1,8 @@ MODEL = """ +------------------------------------------------------------------------ +-- Generated using Kripkomat +------------------------------------------------------------------------ MODULE {name} VAR state : {{ {states} }};