diff --git a/analyze.py b/analyze.py index 4eeadcf..a698712 100644 --- a/analyze.py +++ b/analyze.py @@ -1,16 +1,11 @@ from __future__ import print_function import argparse import sys -import re from pycparser import parse_file, c_ast, CParser import graphviz as gv from modelbuilder import * - -func_table = {} -enum_table = {} -assign_table = [] -state_enums = [] +from utils import * class FuncDefVisitor(c_ast.NodeVisitor): def __init__(self): @@ -58,14 +53,19 @@ class EnumDefVisitor(c_ast.NodeVisitor): def __init__(self, name): super().__init__() self._name = name + self.enums = {} def visit_Enum(self, node): - enum_table[self._name] = node + self.enums[self._name] = node + +class EnumTypedefVisitor(c_ast.NodeVisitor): + def __init__(self): + self.enums = {} -class TypedefVisitor(c_ast.NodeVisitor): def visit_Typedef(self, node): ev = EnumDefVisitor(node.name) ev.visit(node) + self.enums = {**self.enums, **ev.enums} class EnumVisitor(c_ast.NodeVisitor): @@ -74,46 +74,7 @@ class EnumVisitor(c_ast.NodeVisitor): self.enum_names = [] def visit_Enumerator(self, node): - self.enum_names.append(node.name) - -def find_longest_path(paths): - ms = 0 - mp = None - for path in paths: - s = len(path) - if s > ms: - ms = s - mp = path - return mp - -def find_shortest_path(paths): - ms = float('inf') - mp = None - for path in paths: - s = len(path) - if s < ms: - ms = s - mp = path - return mp - -def find_common_ancestor(paths): - shortest_path = find_shortest_path(paths) - - last_common = None - for gen_i,_ in enumerate(shortest_path): - common = True - last_node = paths[0][gen_i] - - for path in paths: - if last_node == path[gen_i]: - common = True - last_node = path[gen_i] - else: - common = False - if common: - last_common = last_node - return last_common - + self.enum_names.append(node.name) class SwitchCaseTermVisitor(c_ast.NodeVisitor): def __init__(self, asm_node): @@ -159,7 +120,6 @@ class SwitchCaseCodePropertyVisitor(c_ast.NodeVisitor): self._case = case self._sas = state_asmts self.properties = [] - def visit_Case(self, node): label = node.children()[0][1] @@ -169,27 +129,11 @@ class SwitchCaseCodePropertyVisitor(c_ast.NodeVisitor): scpv.visit(block) self.properties += scpv.properties -def comment_remover(text): - def replacer(match): - s = match.group(0) - if s.startswith('/'): - return "" - else: - return s - pattern = re.compile( - r'//.*?$|/\*.*?\*/|\'(?:\\.|[^\\\'])*\'|"(?:\\.|[^\\"])*"', - re.DOTALL | re.MULTILINE - ) - return re.sub(pattern, replacer, text) - if __name__ == "__main__": argparser = argparse.ArgumentParser('Create a Kripke Structure Model from C Code') argparser.add_argument('filename', nargs='?', help='name of file to parse') - argparser.add_argument('--coord', help='show coordinates in the dump', - action='store_true') - argparser.add_argument('--func', help='process function') argparser.add_argument('--enum', help='state enum') argparser.add_argument('--initial', help='initial state') @@ -197,7 +141,7 @@ if __name__ == "__main__": argparser.add_argument('-o', '--output', dest='output', help='output NuSMV file') argparser.add_argument('--dot', help='output dot file') args = argparser.parse_args() - + source = "" with open(args.filename, "r") as f: #read whole file to a string @@ -206,16 +150,22 @@ if __name__ == "__main__": parser = CParser() ast = parser.parse(comment_remover(source)) #ast = parse_file(args.filename, use_cpp=False) + + assign_table = [] + state_enums = [] + func_table = {} + enum_table = {} fdv = FuncDefVisitor() fdv.visit(ast) func_table = fdv.func_table - enumvis = TypedefVisitor() - enumvis.visit(ast) + etv = EnumTypedefVisitor() + etv.visit(ast) + enum_table = etv.enums state_asmts = [] - + if args.enum in enum_table: ev = EnumVisitor() ev.visit(enum_table[args.enum]) @@ -297,7 +247,6 @@ if __name__ == "__main__": print("-------------------") print(nusmv) - if args.dot is not None: g = gv.Digraph('G') diff --git a/test.c b/test.c index f46f5b6..40b0451 100644 --- a/test.c +++ b/test.c @@ -17,7 +17,14 @@ typedef struct bool m_b; } testfsm_t; -void process(testfsm_t *p_fsm, const bool input) +typedef struct +{ + bool m_i; + bool m_oa; + bool m_ob +} testfsm_pd_t; + +void process_internal(testfsm_t *p_fsm, const bool input) { testfsm_state_t nextState = p_fsm->m_state; @@ -56,6 +63,8 @@ void process(testfsm_t *p_fsm, const bool input) p_fsm->m_state = nextState; } +void process_outputs(testfsm_t *p_fsm, const bool input + bool randbool(int throws) { bool stillTrue = true; diff --git a/utils.py b/utils.py new file mode 100644 index 0000000..08c525a --- /dev/null +++ b/utils.py @@ -0,0 +1,55 @@ +import re + +def find_longest_path(paths): + ms = 0 + mp = None + for path in paths: + s = len(path) + if s > ms: + ms = s + mp = path + return mp + +def find_shortest_path(paths): + ms = float('inf') + mp = None + for path in paths: + s = len(path) + if s < ms: + ms = s + mp = path + return mp + +def find_common_ancestor(paths): + if len(paths) == 0: + return None + + shortest_path = find_shortest_path(paths) + + last_common = None + for gen_i,_ in enumerate(shortest_path): + common = True + last_node = paths[0][gen_i] + + for path in paths: + if last_node == path[gen_i]: + common = True + last_node = path[gen_i] + else: + common = False + if common: + last_common = last_node + return last_common + +def comment_remover(text): + def replacer(match): + s = match.group(0) + if s.startswith('/'): + return "" + else: + return s + pattern = re.compile( + r'//.*?$|/\*.*?\*/|\'(?:\\.|[^\\\'])*\'|"(?:\\.|[^\\"])*"', + re.DOTALL | re.MULTILINE + ) + return re.sub(pattern, replacer, text)