345 lines
12 KiB
Python
345 lines
12 KiB
Python
from __future__ import print_function
|
|
import argparse
|
|
import os,sys,io
|
|
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')
|
|
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
|
|
source = f.read()
|
|
|
|
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()
|
|
|
|
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)
|
|
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:
|
|
print(" - ",ename)
|
|
states.append(ename)
|
|
else:
|
|
print(f"Initial State Enum '{args.enum}' not found")
|
|
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)
|
|
|
|
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)
|
|
|
|
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)
|