diff --git a/analyze.py b/analyze.py index a698712..263d64d 100644 --- a/analyze.py +++ b/analyze.py @@ -6,128 +6,7 @@ import graphviz as gv from modelbuilder import * from utils import * - -class FuncDefVisitor(c_ast.NodeVisitor): - def __init__(self): - self.func_table = {} - def visit_FuncDef(self, node): - self.func_table[node.decl.name] = node - -class StateAssignmentVisitor(c_ast.NodeVisitor): - def __init__(self, state): - super().__init__() - self.state = state - self.assignments = [] - - def visit(self, node, path = None): - """ Visit a node. - """ - if path is None: - path = [] - if self._method_cache is None: - self._method_cache = {} - - visitor = self._method_cache.get(node.__class__.__name__, None) - if visitor is None: - method = 'visit_' + node.__class__.__name__ - visitor = getattr(self, method, self.generic_visit) - self._method_cache[node.__class__.__name__] = visitor - - return visitor(node, path) - - def generic_visit(self, node, path): - """ Called if no explicit visitor function exists for a - node. Implements preorder visiting of the node. - """ - path = path.copy() - path.append(node) - for c in node: - self.visit(c, path) - - def visit_Assignment(self, n, path): - rval_str = n.rvalue.name - if rval_str == self.state: - self.assignments.append((n,path)) - -class EnumDefVisitor(c_ast.NodeVisitor): - def __init__(self, name): - super().__init__() - self._name = name - self.enums = {} - - def visit_Enum(self, node): - self.enums[self._name] = node - -class EnumTypedefVisitor(c_ast.NodeVisitor): - def __init__(self): - self.enums = {} - - def visit_Typedef(self, node): - ev = EnumDefVisitor(node.name) - ev.visit(node) - self.enums = {**self.enums, **ev.enums} - - -class EnumVisitor(c_ast.NodeVisitor): - def __init__(self): - super().__init__() - self.enum_names = [] - - def visit_Enumerator(self, node): - self.enum_names.append(node.name) - -class SwitchCaseTermVisitor(c_ast.NodeVisitor): - def __init__(self, asm_node): - super().__init__() - self._asm_node = asm_node - self.hit = False - - def visit_Assignment(self, node): - if node == self._asm_node: - self.hit = True - -class SwitchCaseTranVisitor(c_ast.NodeVisitor): - def __init__(self, asm_node): - super().__init__() - self._asm_node = asm_node - self.tran_table = [] - - def visit_Case(self, node): - sctv = SwitchCaseTermVisitor(self._asm_node) - sctv.visit(node) - if sctv.hit: - self.tran_table.append((node.children()[0][1].name, self._asm_node.rvalue.name)) - -class SwitchCasePropertyVisitor(c_ast.NodeVisitor): - def __init__(self, state_asmts): - super().__init__() - self._sas = state_asmts - self.properties = [] - - def visit_Assignment(self, node): - if not(node in self._sas): - 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}" - self.properties.append(prop) - - -class SwitchCaseCodePropertyVisitor(c_ast.NodeVisitor): - def __init__(self, case, state_asmts): - super().__init__() - self._case = case - self._sas = state_asmts - self.properties = [] - - def visit_Case(self, node): - label = node.children()[0][1] - block = node - if label.name == self._case: - scpv = SwitchCasePropertyVisitor(self._sas) - scpv.visit(block) - self.properties += scpv.properties +from astvisitors import * if __name__ == "__main__": argparser = argparse.ArgumentParser('Create a Kripke Structure Model from C Code') diff --git a/astvisitors.py b/astvisitors.py new file mode 100644 index 0000000..b66a3de --- /dev/null +++ b/astvisitors.py @@ -0,0 +1,124 @@ +from pycparser import c_ast + +class FuncDefVisitor(c_ast.NodeVisitor): + def __init__(self): + self.func_table = {} + def visit_FuncDef(self, node): + self.func_table[node.decl.name] = node + +class StateAssignmentVisitor(c_ast.NodeVisitor): + def __init__(self, state): + super().__init__() + self.state = state + self.assignments = [] + + def visit(self, node, path = None): + """ Visit a node. + """ + if path is None: + path = [] + if self._method_cache is None: + self._method_cache = {} + + visitor = self._method_cache.get(node.__class__.__name__, None) + if visitor is None: + method = 'visit_' + node.__class__.__name__ + visitor = getattr(self, method, self.generic_visit) + self._method_cache[node.__class__.__name__] = visitor + + return visitor(node, path) + + def generic_visit(self, node, path): + """ Called if no explicit visitor function exists for a + node. Implements preorder visiting of the node. + """ + path = path.copy() + path.append(node) + for c in node: + self.visit(c, path) + + def visit_Assignment(self, n, path): + rval_str = n.rvalue.name + if rval_str == self.state: + self.assignments.append((n,path)) + +class EnumDefVisitor(c_ast.NodeVisitor): + def __init__(self, name): + super().__init__() + self._name = name + self.enums = {} + + def visit_Enum(self, node): + self.enums[self._name] = node + +class EnumTypedefVisitor(c_ast.NodeVisitor): + def __init__(self): + self.enums = {} + + def visit_Typedef(self, node): + ev = EnumDefVisitor(node.name) + ev.visit(node) + self.enums = {**self.enums, **ev.enums} + + +class EnumVisitor(c_ast.NodeVisitor): + def __init__(self): + super().__init__() + self.enum_names = [] + + def visit_Enumerator(self, node): + self.enum_names.append(node.name) + +class SwitchCaseTermVisitor(c_ast.NodeVisitor): + def __init__(self, asm_node): + super().__init__() + self._asm_node = asm_node + self.hit = False + + def visit_Assignment(self, node): + if node == self._asm_node: + self.hit = True + +class SwitchCaseTranVisitor(c_ast.NodeVisitor): + def __init__(self, asm_node): + super().__init__() + self._asm_node = asm_node + self.tran_table = [] + + def visit_Case(self, node): + sctv = SwitchCaseTermVisitor(self._asm_node) + sctv.visit(node) + if sctv.hit: + self.tran_table.append((node.children()[0][1].name, self._asm_node.rvalue.name)) + +class SwitchCasePropertyVisitor(c_ast.NodeVisitor): + def __init__(self, state_asmts): + super().__init__() + self._sas = state_asmts + self.properties = [] + + def visit_Assignment(self, node): + if not(node in self._sas): + 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}" + self.properties.append(prop) + + +class SwitchCaseCodePropertyVisitor(c_ast.NodeVisitor): + def __init__(self, case, state_asmts): + super().__init__() + self._case = case + self._sas = state_asmts + self.properties = [] + + def visit_Case(self, node): + label = node.children()[0][1] + block = node + if label.name == self._case: + scpv = SwitchCasePropertyVisitor(self._sas) + scpv.visit(block) + self.properties += scpv.properties +