From f428b1a45b8b0ba02fedfdbd7a421b346ccc2bc8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dominic=20H=C3=B6glinger?= Date: Wed, 14 May 2025 21:31:45 +0200 Subject: [PATCH] add input ids --- LICENSE | 2 +- analyze.py | 104 +++++++++++++++++++++++++++++++++++++++--------- astvisitors.py | 40 +++++++++++++------ modelbuilder.py | 60 +++++++++++++++++++++++++--- 4 files changed, 168 insertions(+), 38 deletions(-) diff --git a/LICENSE b/LICENSE index ccb516a..ddc1e4b 100644 --- a/LICENSE +++ b/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: diff --git a/analyze.py b/analyze.py index c95af24..cfe3a9c 100644 --- a/analyze.py +++ b/analyze.py @@ -19,6 +19,12 @@ def parse_statevar(statevar): 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', @@ -29,6 +35,7 @@ if __name__ == "__main__": 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') @@ -87,12 +94,18 @@ if __name__ == "__main__": tran_table = [] properties = [] - state_id = 'm_tState' + 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'] - input_ids = ['cbEnable', 'cbCondition', 'm_ucEnableUnconditioned'] + #SLM + input_ids = ['m_bEnable', 'm_bCondition', 'm_ucEnableUnconditioned'] #conditional_ids = [*input_ids, 'm_ucTimerType'] + input_ids = args.inputids fdv = FuncDefVisitor() fdv.visit(ast) @@ -111,6 +124,16 @@ if __name__ == "__main__": 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 = [] @@ -203,9 +226,8 @@ if __name__ == "__main__": if len(conds_state) != 1: cond_exprs = [cg.visit(x) for x in cpa.condition_chain] print("OOPS") - print(cond_exprs) + 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]) @@ -226,36 +248,40 @@ if __name__ == "__main__": tf = NuSmvConditionTransformer() cond_mod = tf.transform(condition) mod_expr = cg.visit(cond_mod) - - print(f" - {state_from} -> {state_to} on {mod_expr}") + 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) - assigments = [] - print("Assignments") + 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)): - assigments.append(a) - - for a in assigments: + 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_transition = False + 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_transition = True + disregard_assignment = True break conditional_visitor = ContainsOneOfIdVisitor(input_ids) conditional_visitor.visit(c) @@ -266,11 +292,53 @@ if __name__ == "__main__": if state_condition_visitor.hit: conds_state.append(c) - if not(disregard_transition): - cond_exprs = [cg.visit(x) for x in cond_chain] - state_cond_exprs = [cg.visit(x) for x in conds_state] - print(f" - {cg.visit(a.node)} {cond_exprs} {state_cond_exprs}") + 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, properties) + mod = ModelBuilder(states, initial_state, tran_table, assignments) nusmv = mod.generate() print(nusmv) diff --git a/astvisitors.py b/astvisitors.py index bd7440e..d4b5afd 100644 --- a/astvisitors.py +++ b/astvisitors.py @@ -371,17 +371,18 @@ class TypedIdTransformer(AstPathTransformer): funcdef = None if funcdef is not None: id_type = 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) + 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 @@ -475,7 +476,7 @@ class AstFuncCallInlinerTransformer(object): paramname = tdec.declname idtable[paramname] = callarg #print("idtable", idtable) - tfnode = self.transform(self.func_table[fcall], idtable) + tfnode = self.transform(self.func_table[fcall].body, idtable) return tfnode return node @@ -486,7 +487,17 @@ class AstFuncCallInlinerTransformer(object): 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): @@ -554,6 +565,9 @@ class NuSmvConditionTransformer(AstTransformer): 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) diff --git a/modelbuilder.py b/modelbuilder.py index 91bcfd0..674b225 100644 --- a/modelbuilder.py +++ b/modelbuilder.py @@ -15,6 +15,7 @@ ASSIGN {transitions} TRUE : state; esac; +{varassigns} DEFINE {properties} """ @@ -22,6 +23,16 @@ DEFINE 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}; """ @@ -32,16 +43,16 @@ LTL_FORM = """LTLSPEC """ 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 def generate(self): - cg = c_generator.CGenerator() + cg = CGenerator() cond_tf = NuSmvConditionTransformer() # build model @@ -53,11 +64,47 @@ class ModelBuilder: for tran in self._tran: cond = cond_tf.transform(tran.condition) - expr = cg.visit(cond) + 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) - varextract.visit(tran.condition) - + 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)) @@ -73,6 +120,7 @@ class ModelBuilder: variables="\n".join(variables), initial=self._initial, transitions="\n".join(transitions), + varassigns="\n".join(varassigns), properties="\n".join(properties)) # add LTL formulas