From a7e3c59a94886c0dc73704f7aab7f2d5df0a2bba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dominic=20H=C3=B6glinger?= Date: Tue, 22 Nov 2022 11:21:27 +0100 Subject: [PATCH] added function calls as properties, now noting conditional state assignments as implicit self-transitions --- analyze.py | 28 ++++++++++++++----------- astvisitors.py | 55 ++++++++++++++++++++++++++++++++++++++++++++++++-- utils.py | 3 +++ 3 files changed, 72 insertions(+), 14 deletions(-) diff --git a/analyze.py b/analyze.py index 3fc5163..8bb1a77 100644 --- a/analyze.py +++ b/analyze.py @@ -109,7 +109,7 @@ if __name__ == "__main__": for sa in state_asmts: for f in fsm_funcs: - sctv = SwitchCaseTranVisitor(sa[0], states, sa[2]) + sctv = SwitchCaseTranVisitor(sa[0], states, sa[2], sa[3]) sctv.visit(f) tran_table += sctv.tran_table @@ -170,7 +170,12 @@ if __name__ == "__main__": ss = ','.join(pstates) print(f" - '{full_prop}' when {ss}") print("") - + + print("States shortform:") + states_prefix = os.path.commonprefix(states) + state_to_short = {} + for s in states: + state_to_short[s] = remove_prefix(s, states_prefix) ltls = [] if args.ltlfile is not None: with open(args.ltlfile) as f: @@ -189,21 +194,20 @@ if __name__ == "__main__": if args.dot is not None: g = gv.Digraph('G') - print(props_by_state) - print(property_alias) - for state in states: - shape = 'circle' + for state in reachable_states: + state_short = state_to_short[state] + shape = 'oval' if state == initial_state: - shape = 'doublecircle' + shape = 'doubleoctagon' if state in props_by_state: pstr = ",".join([property_alias[x] for x in props_by_state[state]]) - g.node(state, label=f"{state}\n\n{{{pstr}}}", shape=shape) + g.node(state_short, label=f"{state_short}\n\n{{{pstr}}}", shape=shape) else: - g.node(state, label=state, shape=shape) + g.node(state_short, label=state_short, shape=shape) - - for t in tran_table: - g.edge(t[0], t[1]) + for n,ms in comp_tt.items(): + for m in ms: + g.edge(state_to_short[n], state_to_short[m]) g.render(filename=args.dot) diff --git a/astvisitors.py b/astvisitors.py index 84b4f18..22ed012 100644 --- a/astvisitors.py +++ b/astvisitors.py @@ -10,6 +10,12 @@ def path_select_last(classname, p): return n return None +def path_contains(p, t): + for n in p: + if isinstance(n, t): + return True + return False + def path_select_parent(child, p): parent = None for n in p: @@ -18,6 +24,33 @@ def path_select_parent(child, p): parent = n return None +def path_slice_back(node, p): + s = [] + for n in reversed(p): + if n == node: + break + s.append(n) + return [x for x in reversed(s)] + +class ExprListSerializerVisitor(c_ast.NodeVisitor): + def __init__(self): + self.serial = [] + + def visit_Constant(self, node): + expr = node.value + self.serial.append(expr) + + def visit_ID(self, node): + expr = node.name + self.serial.append(expr) + + #todo: expand + +def expr_list_to_str(exprl): + elsv = ExprListSerializerVisitor() + elsv.visit(exprl) + return ','.join(elsv.serial) + class NodeVisitorWithParent(object): def __init__(self): self.current_parent = None @@ -85,6 +118,7 @@ class StateAssignmentVisitor(c_ast.NodeVisitor): self.visit(c, path) def visit_Assignment(self, n, path): + # fallthrough detection case_node = path_select_last('Case', path) fallthrough_case_names = [] if case_node is not None: @@ -113,10 +147,16 @@ class StateAssignmentVisitor(c_ast.NodeVisitor): fallthrough_case_names = sibling_names[slice_start-1:slice_end] rval_str = '' + # conditional assignment detection + asm_if = path_select_last('If', path) + subpath_case = path_slice_back(case_node, path) + is_exhaustive_conditional = True if asm_if is None else (asm_if.iftrue is not None) and (asm_if.iffalse is not None) + is_conditional = path_contains(subpath_case, c_ast.If) and not(is_exhaustive_conditional) + if not(isinstance(n.rvalue, c_ast.Constant) or isinstance(n.rvalue, c_ast.BinaryOp)): rval_str = n.rvalue.name if rval_str == self.state: - self.assignments.append((n,path,fallthrough_case_names)) + self.assignments.append((n,path,fallthrough_case_names,is_conditional)) class EnumDefVisitor(c_ast.NodeVisitor): def __init__(self, name): @@ -156,10 +196,11 @@ class SwitchCaseTermVisitor(c_ast.NodeVisitor): self.hit = True class SwitchCaseTranVisitor(c_ast.NodeVisitor): - def __init__(self, asm_node, states, fallthrough_states): + def __init__(self, asm_node, states, fallthrough_states, is_conditional): super().__init__() self.states = states self.fallthrough_states = fallthrough_states + self.is_conditional = is_conditional self._asm_node = asm_node self.tran_table = [] @@ -168,6 +209,10 @@ class SwitchCaseTranVisitor(c_ast.NodeVisitor): sctv = SwitchCaseTermVisitor(self._asm_node) sctv.visit(node) if sctv.hit and (state_from in self.states): + #if conditional, state remains in state sometimes + if self.is_conditional: + self.tran_table.append((state_from,state_from)) + # process state assignment self.tran_table.append((state_from, self._asm_node.rvalue.name)) for ft in self.fallthrough_states: self.tran_table.append((ft, self._asm_node.rvalue.name)) @@ -178,6 +223,12 @@ class SwitchCasePropertyVisitor(c_ast.NodeVisitor): self._sas = state_asmts self.properties = [] + def visit_FuncCall(self, node): + name = node.name.name + args = expr_list_to_str(node.args) if node.args is not None else "" + fcall = f"{name}({args})" + self.properties.append(fcall) + def visit_Assignment(self, node): if not(node in self._sas): lvalue = None diff --git a/utils.py b/utils.py index 9f30787..05bceda 100644 --- a/utils.py +++ b/utils.py @@ -25,6 +25,9 @@ def base_10_to_alphabet(number): for part in _decompose(number) )[::-1] +def remove_prefix(s, prefix): + return s[len(prefix):] if s.startswith(prefix) else s + def find_longest_path(paths): ms = 0 mp = None