add input ids

or something, I'm no prof

good news is that state processing functions should work

LICENSE

@@ -1,4 +1,4 @@
-Copyright (c) 2022 flip. 
+Copyright (c) 2022 Dominic Hoeglinger.
 
 Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
 

analyze.py

@@ -1,21 +1,44 @@
 from __future__ import print_function
 import argparse
 import os,sys,io
-from pycparser import parse_file, c_ast, CParser
+from pycparser import parse_file, c_ast, CParser, c_generator
 from pcpp import Preprocessor
 import graphviz as gv
+import html
+from dataclasses import dataclass
 
 from modelbuilder import *
 from utils import *
 from astvisitors import *
 
+def parse_statevar(statevar):
+    r_struct = r'(\w+)(\.|->)(\w+)'
+    match = re.match(r_struct, statevar)
+    if match:
+        name,typ,field = match.groups()
+        return c_ast.StructRef(c_ast.ID(name), typ, c_ast.ID(field))
+    return c_ast.ID(statevar)
+
+@dataclass
+class PathAssignment:
+    lvalue:c_ast.Node
+    rvalue:c_ast.Node
+    condition:c_ast.Node
+
 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('-I', '--includedirs', nargs='+', default=[])
+    argparser.add_argument('-D', '--defines', nargs='+', default=[])
+    argparser.add_argument('-p', '--preprocess', help='output preprocessor file')
+    argparser.add_argument('-c', '--conditional', help='only count state assignment if this conditional applies on the path')
+    argparser.add_argument('--inputids', nargs='+', default=[])
     argparser.add_argument('--func', help='process function')
     argparser.add_argument('--enum', help='state enum')
+    argparser.add_argument('--statevar', help='state variable')
     argparser.add_argument('--initial', help='initial state')
     argparser.add_argument('--ltlfile', help='file containing LTL formulae')
     argparser.add_argument('-o', '--output', dest='output', help='output NuSMV file')
@@ -29,131 +52,293 @@ if __name__ == "__main__":
     
     p = Preprocessor()
     p.add_path('/usr/lib/gcc/x86_64-linux-gnu/12/include/')
+    for inc in args.includedirs:
+        #print(f"Include-Dir: {inc}")
+        p.add_path(inc)
+    
+    for define in args.defines:
+        name,value = define.split('=')
+        #print(f"Define: {name}={value}")
+        p.define(f"{name} {value}")
 
     p.parse(source)
     oh = io.StringIO()
     p.write(oh)
     prep_source = oh.getvalue()
     
-    #print(prep_source)
-    #exit()
-
+    if args.preprocess is not None:
+        with open(args.preprocess, "wt") as f:
+            n = f.write(prep_source)
+    
+    cg = CGenerator()
+    
     parser = CParser()
     ast = parser.parse(prep_source)
-    #ast = parse_file(args.filename, use_cpp=False)
+    ass = parse_statevar(args.statevar)
+    tg = TypedefGatherer()
+    tg.visit(ast)
+    typedefs = tg.typedefs
+    #print("Typedefs", typedefs.keys())
     
+    tast = TypedIdTransformer(typedefs).transform(ast)
+    #tast.show()
+    ast = tast
+
+    initial_state = args.initial
     assign_table = []
     state_enums = []
     func_table = {}
     enum_table = {}
     state_asmts = []
+    fsm_funcs = []
+    tran_table = []
+    properties = []
     
+    def get_rightmost_field(node):
+        if isinstance(node, c_ast.StructRef):
+            return get_rightmost_field(node.field)
+        return node
+    state_id = get_rightmost_field(ass).name
+    
+    #TMR
+    #input_ids = ['m_bIn', 'm_ulActTime']
+    #SLM
+    input_ids = ['m_bEnable', 'm_bCondition', 'm_ucEnableUnconditioned']
+    #conditional_ids = [*input_ids, 'm_ucTimerType']
+    input_ids = args.inputids
+
     fdv = FuncDefVisitor()
     fdv.visit(ast)
     func_table = fdv.func_table
+    proc_func = None
+    if not(args.func in func_table):
+        raise Exception(f"Function name '{args.func}' not found!")
+    else:
+        proc_func = func_table[args.func]
+    
+    fast = AstFuncCallInlinerTransformer(func_table).transform(ast)
+    ast = fast
 
     etv = EnumTypedefVisitor()
     etv.visit(ast)
     enum_table = etv.enums
+    states = []
     
+    # Update ProcFunc to unrolled form - TODO
+    fdv = FuncDefVisitor()
+    fdv.visit(ast)
+    func_table = fdv.func_table
+    proc_func = None
     if not(args.func in func_table):
         raise Exception(f"Function name '{args.func}' not found!")
+    else:
+        proc_func = func_table[args.func]
 
+    def discover_cals(func):
+        funcs = []
+        child_funcs = []
+        fcv = FuncCallVisitor()
+        fcv.visit(func)
+        for fc in fcv.func_calls:
+            if fc in func_table:
+                funcs.append(func_table[fc])
+                child_funcs += discover_cals(func_table[fc])
+        return funcs + child_funcs
+
+    # discover FSM functions
+    fsm_funcs.append(proc_func)
+    fsm_funcs += discover_cals(proc_func)
+    #fsm_funcs += [ func_table[x] for x in fcv.func_calls ]
+    
+    print("Function Table")
+    for f in fsm_funcs:
+        print(f" - {f.decl.name} {'<<< entry' if (f.decl.name == args.func) else ''}")
+    print("")
+
+    config_cond = None
+    cond_blacklist = []
+    cond_whitelist = []
+    if args.conditional is not None:
+        config_cond = args.conditional
+        print(f"Configuration Conditional {config_cond}")
+        config_type = None
+        config_enums = None
+        for name,enum_type in enum_table.items():
+            ev = EnumVisitor()
+            ev.visit(enum_type)
+            if config_cond in ev.enum_names:
+                config_type = name
+                config_enums = ev.enum_names
+                break
+        if config_type is not None:
+            print(f" - Type is {config_type}")
+            cond_whitelist.append(config_cond)
+            print( " - Enum Blacklist is")
+            for enum in config_enums:
+                if enum != config_cond:
+                    print(f"   * {enum}")
+                    cond_blacklist.append(enum)
+        else:
+            print("No type found for conditional, ignoring")
+        print("")
+
+    print("Enum Table")
     if args.enum in enum_table:
         ev = EnumVisitor()
         ev.visit(enum_table[args.enum])
         for ename in ev.enum_names:
-            sav = StateAssignmentVisitor(ename)
-            sav.visit(func_table[args.func])
-            state_asmts += sav.assignments
+            print(" - ",ename)
+            states.append(ename)
     else:
         print(f"Initial State Enum '{args.enum}' not found")
-
-    paths = []
-    for asm in state_asmts:
-        paths.append(asm[1])
-
-    common = find_common_ancestor(paths)
-
-    tran_table = []
-
-    for sa in state_asmts:
-        sctv = SwitchCaseTranVisitor(sa[0])
-        sctv.visit(common)
-        tran_table += sctv.tran_table
-
-    comp_tt = {}
-    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]
-    states = comp_tt.keys()
-    print("States: ", ",".join(states))
-    print("")
+    print("Extracting State Transitions")
+    sav = StateAssignmentVisitor(func_table, ass)
+    sav.visit(proc_func)
+    for assignment in sav.assignments:
+        state_to = assignment.state
+        cpa = ConditionalPathAnalyzer()
+        #print("Path", path_to_str(assignment.path))
+        cpa.analyze(reversed(assignment.path))
+        cond_chain = []
+        conds_state = []
+        state_from_expr = None
+        disregard_transition = False
+        for c in cpa.condition_chain:
+            # filter by conditional enum
+            # this is far from correct
+            cond_blacklist_visitor = ContainsOneOfIdVisitor(cond_blacklist)
+            cond_blacklist_visitor.visit(c)
+            if cond_blacklist_visitor.hit:
+                disregard_transition = True
+                break
+            conditional_visitor = ContainsOneOfIdVisitor(input_ids)
+            conditional_visitor.visit(c)
+            if conditional_visitor.hit:
+                cond_chain.append(c)
+            state_condition_visitor = ContainsOneOfIdVisitor([state_id])
+            state_condition_visitor.visit(c)
+            if state_condition_visitor.hit:
+                conds_state.append(c)
 
-    props_by_state = {}
-    print("Compact Transition Table:")
-    for n,ms in comp_tt.items():
-        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():
-        for prop in props:
-            if prop in properties:
-                properties[prop].append(state)
-            else:
-                properties[prop] = [state]
-    
-    print("Properties")
-    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:
-            ltls = [line.rstrip() for line in f]
-
-
-    mod = ModelBuilder(states, args.initial, comp_tt, properties, ltls=ltls)
-    nusmv = mod.generate()
-
-    if args.output is not None:
-        with open(args.output, "wt") as f:
-            n = f.write(nusmv)
-    else:
-        print("-------------------")
-        print(nusmv)
-    
-    if args.dot is not None:
-        g = gv.Digraph('G')
-        
-        for state in states:
-            if state in props_by_state:
-                pstr = ",".join(props_by_state[state])
-                if state == args.initial:
-                    g.attr('node', shape='doublecircle')
-                else:
-                    g.attr('node', shape='circle')
-                g.node(state, label=state, xlabel=f"{{{pstr}}}")
-              
+        if not(disregard_transition):
+            if len(conds_state) != 1:
+                cond_exprs = [cg.visit(x) for x in cpa.condition_chain]
+                print("OOPS")
+                print(cond_exprs, conds_state)
+                raise Exception("No or too many state conditions found")
+            # find out from which state the assignment transitions
+            current_state_visitor = ContainsOneOfIdVisitor(states)
+            current_state_visitor.visit(conds_state[0])
+            if not(current_state_visitor.hit):
+                raise Exception("State assignment does not assign state enum")
+            state_from = current_state_visitor.name
+            condition = None
+            if len(cond_chain) == 1:
+                condition = cond_chain[0]
+            elif len(cond_chain) > 1:
+                condition = cond_chain[0]
+                for expr in cond_chain[1:len(cond_chain)]:
+                    condition = c_ast.BinaryOp('&&', expr, condition)
                 
-        
-        for t in tran_table:
-            g.edge(t[0], t[1])
-        g.render(filename=args.dot)
+            cond_exprs = [cg.visit(x) for x in cond_chain]
+            cond_expr = cg.visit(condition)
+            
+            tf = NuSmvConditionTransformer()
+            cond_mod = tf.transform(condition)
+            mod_expr = cg.visit(cond_mod)
+            if cond_mod is None:
+                print(f" - {state_from} -> {state_to} unconditional")
+            else:
+                print(f" - {state_from} -> {state_to} on {mod_expr}")
+            tran_table.append(StateTransition(state_from, state_to, condition))
+    print("")
+
+
+    # Extract properties
+    av = AssignmentVisitor(func_table)
+    av.visit(proc_func)
+    path_assigments = []
+    
+    for a in av.assignments:
+        if a.node.op == '=':
+            if isinstance(a.node.lvalue, c_ast.StructRef):
+                if not(check_structref_equivalence(a.node.lvalue, ass)):
+                    path_assigments.append(a)
+    assignments = {}
+    for a in path_assigments:
+        cpa = ConditionalPathAnalyzer()
+        #print("Path", path_to_str(assignment.path))
+        cpa.analyze(reversed(a.path))
+        cond_chain = []
+        conds_state = []
+        state_from_expr = None
+        disregard_assignment = False
+        for c in cpa.condition_chain:
+            # filter by conditional enum
+            # this is far from correct
+            cond_blacklist_visitor = ContainsOneOfIdVisitor(cond_blacklist)
+            cond_blacklist_visitor.visit(c)
+            if cond_blacklist_visitor.hit:
+                disregard_assignment = True
+                break
+            conditional_visitor = ContainsOneOfIdVisitor(input_ids)
+            conditional_visitor.visit(c)
+            if conditional_visitor.hit:
+                cond_chain.append(c)
+            state_condition_visitor = ContainsOneOfIdVisitor([state_id])
+            state_condition_visitor.visit(c)
+            if state_condition_visitor.hit:
+                conds_state.append(c)
+
+        if not(disregard_assignment):
+            conds_state_tf = []
+            # transform state conditions to output format
+            for state_cond in conds_state:
+                current_state_visitor = ContainsOneOfIdVisitor(states)
+                current_state_visitor.visit(conds_state[0])
+                if not(current_state_visitor.hit):
+                    raise Exception("State assignment does not assign state enum")
+                state_from = current_state_visitor.name
+                conds_state_tf.append(c_ast.BinaryOp('==', c_ast.ID("state"), c_ast.ID(state_from)))
+            conds_state = conds_state_tf
+            state_cond = None
+            condition = None
+            if len(conds_state) == 1:
+                state_cond = conds_state[0]
+            elif len(conds_state) > 1:
+                state_cond = conds_state[0]
+                for expr in cond_chain[1:len(conds_state)]:
+                    condition = c_ast.BinaryOp('||', expr, state_cond)
+            
+            if len(cond_chain) == 1:
+                condition = cond_chain[0]
+            elif len(cond_chain) > 1:
+                condition = cond_chain[0]
+                for expr in cond_chain[1:len(conds_state)]:
+                    condition = c_ast.BinaryOp('&&', expr, condition)
+            
+            if condition is None and state_cond is not None:
+                condition = state_cond
+            elif condition is not None and state_cond is not None:
+                condition = c_ast.BinaryOp('&&', condition, state_cond)
+            
+            cond_exprs = cg.visit(condition)
+            #state_cond_exprs = cg.visit(state_cond)
+            variable = cg.visit(NuSmvConditionTransformer().transform(a.node.lvalue))
+            if variable in assignments:
+                assignments[variable].append(PathAssignment(a.node.lvalue, a.node.rvalue, condition))
+            else:
+                assignments[variable] = [PathAssignment(a.node.lvalue, a.node.rvalue, condition)]
+            #print(f" - {cg.visit(a.node)} {cond_exprs}")
+    
+    print("Assignments")
+    for var,assigns in assignments.items():
+        print(f" - {var}")
+        for assign in assigns:
+            print(f"   -> '{cg.visit(assign.rvalue)}' on {cg.visit(assign.condition)}")
+
+    mod = ModelBuilder(states, initial_state, tran_table, assignments)
+    nusmv = mod.generate()
+    print(nusmv)

astvisitors.py

@@ -1,46 +1,24 @@
-from pycparser import c_ast
+import re
+from pycparser import c_ast, c_generator
+from itertools import pairwise
+from dataclasses import dataclass
+
+def path_to_str(p):
+    return "->".join([str(n.__class__.__name__) for n in p])
 
 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 = []
+class FuncCallVisitor(c_ast.NodeVisitor):
+    def __init__(self):
+        self.func_calls = []
 
-    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))
+    def visit_FuncCall(self, node):
+        self.func_calls.append(node.children()[0][1].name)
 
 class EnumDefVisitor(c_ast.NodeVisitor):
     def __init__(self, name):
@@ -69,56 +47,581 @@ class EnumVisitor(c_ast.NodeVisitor):
     def visit_Enumerator(self, node):
         self.enum_names.append(node.name)        
 
-class SwitchCaseTermVisitor(c_ast.NodeVisitor):
-    def __init__(self, asm_node):
+class PathVisitor(object):
+    def __init__(self):
+        self._method_cache = {}
+
+    def visit(self, node, path = None):
+        if path is None:
+            path = []
+
+        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):
+        path = path.copy()
+        path.append(node)
+        for c in node:
+            self.visit(c, path)
+
+class FuncCallDeferPathVisitor(PathVisitor):
+    def __init__(self, func_table):
         super().__init__()
-        self._asm_node = asm_node
+        self.func_table = func_table
+    
+    def visit_FuncCall(self, node, path):
+        fcall = node.name.name
+        if fcall in self.func_table:
+            self.visit(self.func_table[fcall], path)
+
+def check_node_equivalence(lhs, rhs):
+    return str(lhs) == str(rhs)
+
+def check_structref_equivalence(lhs:c_ast.StructRef, rhs:c_ast.StructRef):
+    if lhs.name.name != rhs.name.name:
+        return False
+    if lhs.field.name != rhs.field.name:
+        return False
+    return True
+
+@dataclass
+class PathStateAssignment:
+    path:list[c_ast.Node]
+    node:c_ast.Assignment
+    state:str
+
+class StateAssignmentVisitor(FuncCallDeferPathVisitor):
+    def __init__(self, func_table, variable):
+        super().__init__(func_table)
+        self.variable = variable
+        self.assignments = []
+
+    def visit_Assignment(self, n, path):
+        if check_structref_equivalence(self.variable, n.lvalue):
+            if isinstance(n.rvalue, c_ast.ID):
+                self.assignments.append(PathStateAssignment(path, n, n.rvalue.name))
+            elif isinstance(n.rvalue, c_ast.TernaryOp):
+                #print("TOP", n.rvalue)
+                pass
+        
+
+@dataclass
+class PathAssignment:
+    path:list[c_ast.Node]
+    node:c_ast.Assignment
+
+class AssignmentVisitor(FuncCallDeferPathVisitor):
+    def __init__(self, func_table):
+        super().__init__(func_table)
+        self.assignments = []
+
+    def visit_Assignment(self, n, path):
+        self.assignments.append(PathAssignment(path, n))
+        
+
+class PathAnalyzer(object):
+    def __init__(self):
+        self._method_cache = {}
+
+    def analyze(self, path):
+        trace = []
+        for node in path:
+            self._invoke_visitor(node, trace)
+            trace.append(node)
+
+    def _invoke_visitor(self, node, trace):
+        visitor = self._method_cache.get(node.__class__.__name__, None)
+        if visitor is None:
+            method = 'visit_' + node.__class__.__name__
+            visitor = getattr(self, method, None)
+            self._method_cache[node.__class__.__name__] = visitor
+
+        if visitor is not None:
+            visitor(node, trace)
+
+@dataclass
+class GeneralizedCase:
+    exprs:list[c_ast.Node]
+    stmts:list[c_ast.Node]
+
+class ConditionalPathAnalyzer(PathAnalyzer):
+    def __init__(self):
+        super().__init__()
+        self.condition_chain = []
+
+    def visit_If(self, node, trace):
+        p = trace[-1]
+        #print("If", node)
+        if node.iftrue == p:
+            #print("->iftrue")
+            self.condition_chain.append(node.cond)
+        elif node.iffalse == p:
+            #print("->iffalse")
+            neg = c_ast.UnaryOp('!', node.cond)
+            self.condition_chain.append(neg)
+        else:
+            pass
+
+    def visit_Switch(self, node, trace):
+        p_case = trace[-2]
+        expr_fallthrough = []
+        gencases = []
+        cond = node.cond
+        block_items = node.stmt.block_items
+        parent_case_idx = None
+        #print("Switch", cond)
+        #print("P:", p_case)
+        #print("CI", block_items)
+        # lump together fallthrough cases
+        for case in block_items:
+            if p_case == case:
+                parent_case_idx = len(gencases)
+            if not isinstance(case, c_ast.Default):
+                expr_fallthrough.append(case.expr)
+                if len(case.stmts) != 0 and isinstance(case.stmts[-1], c_ast.Break):
+                    gencases.append(GeneralizedCase(expr_fallthrough, case.stmts))
+                    expr_fallthrough = []
+        #print("Generalized P-Case", gencases[parent_case_idx].exprs)
+        # does not account for default, which needs the entire set of cases
+        # checked for unequals and and-ed
+        eqops = [c_ast.BinaryOp('==', cond, expr) for expr in gencases[parent_case_idx].exprs]
+        if len(eqops) == 1:
+            self.condition_chain.append(eqops[0])
+        elif len(eqops) > 1:
+            orop = eqops[0]
+            for expr in eqops[1:len(eqops)]:
+                orop = c_ast.BinaryOp('||', expr, orop)
+            self.condition_chain.append(orop)
+        else:
+            raise Exception("Unexpected number of expressions")
+
+class ContainsOneOfIdVisitor(c_ast.NodeVisitor):
+    def __init__(self, ids):
+        self.ids = ids
         self.hit = False
+        self.name = None
 
-    def visit_Assignment(self, node):
-        if node == self._asm_node:
+    def visit_ID(self, node):
+        if node.name in self.ids:
             self.hit = True
+            self.name = node.name
 
-class SwitchCaseTranVisitor(c_ast.NodeVisitor):
-    def __init__(self, asm_node):
+    def visit_TypedID(self, node):
+        return self.visit_ID(node)
+
+@dataclass
+class StateTransition:
+    state_from:str
+    state_to:str
+    condition:c_ast.Node
+
+class TypedefGatherer(c_ast.NodeVisitor):
+    def __init__(self):
+        self.typedefs = {}
+
+    def visit_Typedef(self, node):
+        self.typedefs[node.name] = node
+
+
+class AstTransformer(object):
+    def __init__(self):
+        self._method_cache = {}
+
+    def transform(self, node):
+        visitor = self._method_cache.get(node.__class__.__name__, None)
+        if visitor is None:
+            method = 'transform_' + node.__class__.__name__
+            visitor = getattr(self, method, self._transform_generic)
+            self._method_cache[node.__class__.__name__] = visitor
+        
+        return visitor(node)
+
+    def _transform_Node(self, node):
+        new_c = []
+        for c_name in node.__slots__[0:-1]:
+            c = getattr(node, c_name)
+            new_c.append(self.transform(c))
+        node_constructor = node.__class__
+        return node_constructor(*new_c)
+
+    def _transform_generic(self, node):
+        if isinstance(node, c_ast.Node):
+            return self._transform_Node(node)
+        elif isinstance(node, list):
+            return [self.transform(x) for x in node]
+        else:
+            return node
+
+class AstPathTransformer(object):
+    def __init__(self):
+        self._method_cache = {}
+
+    def transform(self, node, path = None):
+        if path is None:
+            path = [node]
+        else:
+            path = path.copy()
+            path.append(node)
+
+        visitor = self._method_cache.get(node.__class__.__name__, None)
+        if visitor is None:
+            method = 'transform_' + node.__class__.__name__
+            visitor = getattr(self, method, self._transform_generic)
+            self._method_cache[node.__class__.__name__] = visitor
+        
+        return visitor(node, path)
+
+    def _transform_Node(self, node, path):
+        new_c = []
+        for c_name in node.__slots__[0:-1]:
+            c = getattr(node, c_name)
+            new_c.append(self.transform(c, path))
+        node_constructor = node.__class__
+        return node_constructor(*new_c)
+
+    def _transform_generic(self, node, path):
+        if isinstance(node, c_ast.Node):
+            return self._transform_Node(node, path)
+        elif isinstance(node, list):
+            return [self.transform(x, path) for x in node]
+        else:
+            return node
+
+
+
+class TypedID(c_ast.ID):
+    __slots__ = ('name', 'type', 'coord')
+    def __init__(self, name, type=None, coord=None):
+        super().__init__(name, coord)
+        self.type = type
+
+    def children(self):
+        nodelist = []
+        return tuple(nodelist)
+
+    def __iter__(self):
+        return
+        yield
+
+    attr_names = ('name', 'type' )
+
+class CGenerator(c_generator.CGenerator):
+    def __init__(self):
         super().__init__()
-        self._asm_node = asm_node
-        self.tran_table = []
+    
+    def visit_TypedID(self, n):
+        return n.name
 
-    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):
+class TypeDeclFinder(c_ast.NodeVisitor):
+    def __init__(self, declname):
+        self.declname = declname
+        self.decl = None
+
+    def visit_TypeDecl(self, node):
+        if node.declname == self.declname:
+            self.decl = node
+
+class DeclFinder(c_ast.NodeVisitor):
+    def __init__(self, declname):
+        self.declname = declname
+        self.decl = None
+
+    def visit_Decl(self, node):
+        if node.name == self.declname:
+            self.decl = node
+
+class IdentifierTypeFinder(c_ast.NodeVisitor):
+    def __init__(self, declname):
+        self.type = None
+
+    def visit_Decl(self, node):
+            self.decl = node
+
+
+class TypeFinder(object):
+    def __init__(self, t):
+        self.type = t
+        self.result = []
+
+    def visit(self, node):
+        if node.__class__.__name__ == self.type.__name__:
+            self.result.append(node)
+        
+        for c in node:
+            self.visit(c)
+    
+
+class TypedIdTransformer(AstPathTransformer):
+    def __init__(self, type_dict):
         super().__init__()
-        self._sas = state_asmts
-        self.properties = []
+        self.type_dict = type_dict
 
-    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)
+    def transform_ID(self, node, path):
+        #print("node[", node.name, "]")
+        #print("pstr[", node.name, "]", path_to_str(path))
+        try:
+            funcdef = next(filter(lambda x:isinstance(x, c_ast.FuncDef), path))
+        except:
+            funcdef = None
+        if funcdef is not None:
+            id_type = None
+            if funcdef.decl.type.args is not None:
+                param_decl = funcdef.decl.type.args.params
+                #print("Param Decl", param_decl)
+                for decl in param_decl:
+                    declfinder = TypeDeclFinder(node.name)
+                    declfinder.visit(decl)
+                    if declfinder.decl is not None:
+                        id_type = self.type_dict.get(declfinder.decl.type.names[0], declfinder.decl.type.names[0])
+                        break
+                if id_type is not None:
+                    #print("pid[", node.name, "]", id_type)
+                    return TypedID(node.name, id_type)
+            
+        return node
+        
+    def transform_StructRef(self, node, path):
+        if isinstance(node.name, c_ast.ID):
+            funcdef = next(filter(lambda x:isinstance(x, c_ast.FuncDef), path))
+            struct_type = None
+            param_decl = funcdef.decl.type.args.params
+            for decl in param_decl:
+                declfinder = TypeDeclFinder(node.name.name)
+                declfinder.visit(decl)
+                if declfinder.decl is not None:
+                    struct_type = self.type_dict.get(declfinder.decl.type.names[0], None)
+                    break
+            name_node = node.name
+            field_node = node.field
+            if struct_type is not None: 
+                name_node = TypedID(node.name.name, struct_type)
+                # find member type
+                declfinder = DeclFinder(field_node.name)
+                declfinder.visit(struct_type)
+                tf = TypeFinder(c_ast.IdentifierType)
+                tf.visit(declfinder.decl.type.type)
+                idtype_str = " ".join(tf.result[0].names)
+                #print("idtype", idtype_str)
+                idtype = self.type_dict.get(idtype_str, idtype_str)
+                field_node = TypedID(node.field.name, idtype)
+            
+            return c_ast.StructRef(name_node, node.type, field_node, node.coord)
+        
+        name_node = self.transform(node.name, path)
+        field_node = self.transform(node.field, path)
+        struct_type = name_node.field.type
+        declfinder = DeclFinder(field_node.name)
+        declfinder.visit(struct_type)
+        tf = TypeFinder(c_ast.IdentifierType)
+        tf.visit(declfinder.decl.type.type)
+        idtype_str = " ".join(tf.result[0].names)
+        idtype = self.type_dict.get(idtype_str, idtype_str)
+        field_node = TypedID(node.field.name, idtype)
+        
+        return c_ast.StructRef(name_node, node.type, field_node, node.coord)
 
+class AstFuncCallInlinerTransformer(object):
+    def __init__(self, func_table):
+        self._method_cache = {}
+        self.func_table = func_table
 
-class SwitchCaseCodePropertyVisitor(c_ast.NodeVisitor):
-    def __init__(self, case, state_asmts):
+    def transform(self, node, idtable = None):
+        if idtable is None:
+            idtable = {}
+
+        visitor = self._method_cache.get(node.__class__.__name__, None)
+        if visitor is None:
+            method = 'transform_' + node.__class__.__name__
+            visitor = getattr(self, method, self._transform_generic)
+            self._method_cache[node.__class__.__name__] = visitor
+        
+        return visitor(node, idtable)
+
+    def _transform_Node(self, node, idtable):
+        new_c = []
+        for c_name in node.__slots__[0:-1]:
+            c = getattr(node, c_name)
+            new_c.append(self.transform(c, idtable))
+        node_constructor = node.__class__
+        return node_constructor(*new_c)
+
+    def _transform_generic(self, node, idtable):
+        if isinstance(node, c_ast.Node):
+            return self._transform_Node(node, idtable)
+        elif isinstance(node, list):
+            return [self.transform(x, idtable) for x in node]
+        else:
+            return node
+
+    def transform_FuncCall(self, node, idtable):
+        fcall = node.name.name
+        if fcall in self.func_table:
+            funcdef_args = self.func_table[fcall].decl.type.args.params
+            fcall_args = node.args.exprs
+            if len(fcall_args) != len(funcdef_args):
+                raise Exception("Func Call does not match argument number")
+            # update ID table
+            idtable = idtable.copy()
+            for callarg,defarg in zip(fcall_args, funcdef_args):
+                tdec_finder = TypeFinder(c_ast.TypeDecl)
+                tdec_finder.visit(defarg)
+                if len(tdec_finder.result) == 1:
+                    tdec = tdec_finder.result[0]
+                    paramname = tdec.declname
+                    idtable[paramname] = callarg
+                #print("idtable", idtable)
+            tfnode = self.transform(self.func_table[fcall].body, idtable)
+            return tfnode
+        return node
+    
+    def transform_ID(self, node, idtable):
+        if node.name in idtable:
+            return idtable[node.name]
+        return node
+
+    def transform_TypedID(self, node, idtable):
+        return self.transform_ID(node, idtable)
+    
+    def transform_Assignment(self, node, idtable):
+        op = node.op
+        lvalue = self.transform(node.lvalue, idtable)
+        rvalue = self.transform(node.rvalue, idtable)
+        if op == '-=' or op == '+=' or op == '/=' or op == '*=':
+            operand = op[0]
+            rvalue = c_ast.BinaryOp(operand, lvalue, rvalue)
+            op = '='
+            
+        return c_ast.Assignment(op, lvalue, rvalue, node.coord)
+
+def find_type_of_branch(node):
+    if isinstance(node, c_ast.StructRef):
+        return find_type_of_branch(node.field)
+    elif isinstance(node, TypedID):
+        return node.type
+    else:
+        pass
+    return None
+
+class NuSmvConditionTransformer(AstTransformer):
+    def __init__(self):
         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
+    def transform_BinaryOp(self, node):
+        op = node.op
+        match op:
+            case '&&':
+                op = '&'
+            case '||':
+                op = '|'
+            case '==':
+                op = '='
+            case _:
+                op = op
+    
+        lhs = node.left
+        rhs = node.right
 
+        lhs_type = find_type_of_branch(lhs)
+        rhs_type = find_type_of_branch(rhs)
+
+        #print("l type:", lhs_type)
+        #print("r type:", rhs_type)
+        #print("l node:", lhs)
+        #print("r node:", rhs)
+        lhs_is_bool = lhs_type == '_Bool'
+        rhs_is_bool = rhs_type == '_Bool'
+        lhs_is_constant = isinstance(lhs, c_ast.Constant)
+        rhs_is_constant = isinstance(rhs, c_ast.Constant)
+        if lhs_is_bool and rhs_is_constant:
+            rhs = c_ast.ID("FALSE" if rhs.value == '0' else "TRUE")
+        elif rhs_is_bool and lhs_is_constant:
+            lhs = c_ast.ID("FALSE" if lhs.value == '0' else "TRUE")
+        
+        lhs = self.transform(lhs)
+        rhs = self.transform(rhs)
+
+        return c_ast.BinaryOp(op, lhs, rhs)
+
+    def transform_ID(self, node):
+        return c_ast.ID(node.name)
+
+    def transform_TypedID(self, node):
+        return c_ast.ID(node.name)
+
+    def transform_StructRef(self, node):
+        def srtf(node):
+            if isinstance(node, c_ast.StructRef):
+                return f"{srtf(node.name)}_{srtf(node.field)}"
+            elif isinstance(node, TypedID) or isinstance(node, c_ast.ID):
+                return node.name
+            return node
+
+        full = srtf(node)
+        return c_ast.ID(full)
+
+    def transform_Cast(self, node):
+        return self.transform(node.expr)
+
+    def transform_Constant(self, node):
+        value = re.sub(r'([a-zA-Z]+)$', '', node.value)
+        return c_ast.Constant(node.type, value)
+
+    def transform_UnaryOp(self, node):
+        return c_ast.UnaryOp(node.op, self.transform(node.expr))
+
+class NuSmvVariableExtractor(c_ast.NodeVisitor):
+    SHORT_TYPE = '−32767..32767'
+    USHORT_TYPE = '0..65535'
+    INT_TYPE = '−32767..32767'
+    UINT_TYPE = '0..65535'
+    TYPE_LUT = {
+        '_Bool':'boolean',
+        'char':'0..255',
+        'signed char':'-127..127',
+        'unsigned char':'0..255',
+        'short':SHORT_TYPE,
+        'short int':SHORT_TYPE,
+        'signed short':SHORT_TYPE,
+        'signed short int':SHORT_TYPE,
+        'unsigned short':USHORT_TYPE,
+        'unsigned short int':USHORT_TYPE,
+        'int':INT_TYPE,
+        'signed':INT_TYPE,
+        'signed int':INT_TYPE,
+        'unsigned':UINT_TYPE,
+        'unsigned int':UINT_TYPE
+    }
+    def __init__(self):
+        self.variables = {}
+    
+    def visit_TypedID(self, node):
+        smvtype = self.TYPE_LUT.get(node.type, None)
+        if smvtype is None:
+            raise Exception(f"Type '{node.type}' is not supported")
+        self.variables[node.name] = smvtype
+
+    def visit_StructRef(self, node):
+        def findfield(node):
+            if isinstance(node, c_ast.StructRef):
+                return findfield(node.field)
+            return node
+        
+        def srtf(node):
+            if isinstance(node, c_ast.StructRef):
+                return f"{srtf(node.name)}_{srtf(node.field)}"
+            elif isinstance(node, TypedID) or isinstance(node, c_ast.ID):
+                return node.name
+            return node
+        field = findfield(node)
+        full = srtf(node)
+        smvtype = self.TYPE_LUT.get(field.type, None)
+        if smvtype is None:
+            raise Exception(f"Type '{field.type}' is not supported")
+        self.variables[full] = smvtype
+        

modelbuilder.py

@@ -1,3 +1,4 @@
+from astvisitors import *
 
 MODEL = """
 ------------------------------------------------------------------------
@@ -5,18 +6,33 @@ MODEL = """
 ------------------------------------------------------------------------
 MODULE {name}
 VAR
-state : {{ {states} }};
+    state : {{ {states} }};
+{variables}
 ASSIGN
     init(state) := {initial};
     next(state) :=
         case
 {transitions}
+            TRUE : state;
         esac;
+{varassigns}
 DEFINE
 {properties}
 """
 
-TRAN = "            state = {n} : {{{ms}}};"
+VARIABLE = "    {n}:{t};"
+
+TRAN = "            (state = {n}) & ({cond}) : {m};"
+CASE = "            {cond} : {value};"
+VARASSIGN = """
+    init({name}) := {initial};
+    next({name}) :=
+        case
+{cases}
+            TRUE : {name};
+        esac;
+"""
+
 PROP = """    -- Property "{prop}"
     {alias} := {logic};
 """
@@ -26,64 +42,85 @@ LTL_FORM = """LTLSPEC
     {ltl};
 """
 
-A_UPPERCASE = ord('a')
-ALPHABET_SIZE = 26
-
-
-def _decompose(number):
-    """Generate digits from `number` in base alphabet, least significants
-    bits first.
-
-    Since A is 1 rather than 0 in base alphabet, we are dealing with
-    `number - 1` at each iteration to be able to extract the proper digits.
-    """
-
-    while number:
-        number, remainder = divmod(number - 1, ALPHABET_SIZE)
-        yield remainder
-
-
-def base_10_to_alphabet(number):
-    """Convert a decimal number to its base alphabet representation"""
-
-    return ''.join(
-            chr(A_UPPERCASE + part)
-            for part in _decompose(number)
-    )[::-1]
-
 class ModelBuilder:
-    def __init__(self, states, initial, transitions, properties, ltls=[], name="main"):
+    def __init__(self, states, initial, transitions, assigns, ltls=[], name="main"):
         self._name = name
         self._states = states
         self._initial = initial
         self._tran = transitions
-        self._props = properties
+        self._assigns = assigns
         self._ltls = ltls
-        
-        self._propalias = {}
-        for no,prop in enumerate(properties.keys()):
-            self._propalias[prop] = base_10_to_alphabet(no + 1)
 
     def generate(self):
+        cg = CGenerator()
+        cond_tf = NuSmvConditionTransformer()
+
         # build model
         states_decl = ",".join(self._states)
         transitions = []
-
-        for n,ms in self._tran.items():
-            transition = TRAN.format(n=n, ms=",".join(ms))
+        
+        # find variables in the condition
+        varextract = NuSmvVariableExtractor()
+        
+        for tran in self._tran:
+            cond = cond_tf.transform(tran.condition)
+            if cond is not None:
+                expr = cg.visit(cond)
+            else:
+                expr = 'TRUE'
+            transition = TRAN.format(n=tran.state_from, m=tran.state_to, cond=expr)
             transitions.append(transition)
+            if tran.condition is not None:
+                varextract.visit(tran.condition)
+        varassigns = []
+        for var,assigns in self._assigns.items():
+            cases = []
+            var_label = var
+            vartype = None
+            for a in assigns:
+                assign_varextract = NuSmvVariableExtractor()
+                #todo convert rvalue to type
+                assign_varextract.visit(a.lvalue)
+                varname, vartype = list(assign_varextract.variables.items())[0]
+                var_label = varname
+                cond = cond_tf.transform(a.condition)
+                cond_expr = cg.visit(cond)
+                varextract.visit(a.condition)
+                varextract.visit(a.lvalue)
+                varextract.visit(a.rvalue)
+                lvalue = var
+                rvalue = cg.visit(cond_tf.transform(a.rvalue))
+                if vartype == 'boolean':
+                    if rvalue == '0':
+                        rvalue = 'FALSE'
+                    elif rvalue == '1':
+                        rvalue = 'TRUE'
+                    else:
+                        pass
+                cases.append(CASE.format(cond=cond_expr, value=rvalue))
+                initial = '0'
+                if vartype == 'boolean':
+                    initial = 'FALSE'
+            varassigns.append(VARASSIGN.format(name=var_label, cases="\n".join(cases),
+                                               initial=initial))
+            #print(cases)
 
+        variables = []
+        for v,t in varextract.variables.items():
+            variables.append(VARIABLE.format(n=v, t=t))
+        
         properties = []
-        for prop,states in self._props.items():
-            alias = self._propalias[prop]
-            logic = " | ".join([PROP_LOGIC.format(state=x) for x in states])
-            prop_str = PROP.format(prop=prop, alias=alias, logic=logic)
-            properties.append(prop_str)
+        #for alias,(states,prop) in self._props.items():
+        #    logic = " | ".join([PROP_LOGIC.format(state=x) for x in states])
+        #    prop_str = PROP.format(prop=prop, alias=alias, logic=logic)
+        #    properties.append(prop_str)
 
         out = MODEL.format(name=self._name,
                             states=states_decl,
+                            variables="\n".join(variables),
                             initial=self._initial,
                             transitions="\n".join(transitions),
+                            varassigns="\n".join(varassigns),
                             properties="\n".join(properties))
 
         # add LTL formulas

utils.py

@@ -1,5 +1,33 @@
 import re
 
+A_UPPERCASE = ord('a')
+ALPHABET_SIZE = 26
+
+
+def _decompose(number):
+    """Generate digits from `number` in base alphabet, least significants
+    bits first.
+
+    Since A is 1 rather than 0 in base alphabet, we are dealing with
+    `number - 1` at each iteration to be able to extract the proper digits.
+    """
+
+    while number:
+        number, remainder = divmod(number - 1, ALPHABET_SIZE)
+        yield remainder
+
+
+def base_10_to_alphabet(number):
+    """Convert a decimal number to its base alphabet representation"""
+
+    return ''.join(
+            chr(A_UPPERCASE + part)
+            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