add input ids
This commit is contained in:
parent
2a4c4b7660
commit
f428b1a45b
2
LICENSE
2
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:
|
||||
|
||||
|
||||
104
analyze.py
104
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)
|
||||
|
||||
mod = ModelBuilder(states, initial_state, tran_table, properties)
|
||||
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)
|
||||
|
||||
@ -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
|
||||
|
||||
@ -487,6 +488,16 @@ 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)
|
||||
|
||||
@ -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,10 +64,46 @@ 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():
|
||||
@ -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
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user