dominic/kripkomat
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

added conditional enum which must hold true for differenciating different sub-FSMs depending on configuration

Browse Source
This commit is contained in:
Dominic Höglinger 2022-11-22 22:32:40 +01:00
parent 57cb073ff4
commit ae98044d2c
2 changed files with 87 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
analyze.py
View File

@ -19,6 +19,7 @@ if __name__ == "__main__":
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('--func', help='process function')
argparser.add_argument('--enum', help='state enum')
argparser.add_argument('--initial', help='initial state')
@ -104,6 +105,33 @@ if __name__ == "__main__":
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()
@ -112,13 +140,13 @@ if __name__ == "__main__":
print(" - ",ename)
states.append(ename)
#for f in fsm_funcs:
sav = StateAssignmentVisitor(ast, ename)
sav = StateAssignmentVisitor(ast, ename, cond_blacklist, cond_whitelist)
#sav.visit(f)
sav.visit(proc_func)
state_asmts += sav.assignments
else:
print(f"Initial State Enum '{args.enum}' not found")
paths = []
for asm in state_asmts:
paths.append(asm[1])

66
astvisitors.py
View File

@ -1,4 +1,5 @@
from pycparser import c_ast
import re
from pycparser import c_ast, c_generator
from itertools import pairwise
def path_to_str(p):
@ -134,10 +135,12 @@ class FuncCallVisitor(c_ast.NodeVisitor):
self.func_calls.append(node.children()[0][1].name)
class StateAssignmentVisitor(NodeVisitorFuncCallForward):
def __init__(self, ast, state):
def __init__(self, ast, state, config_cond_blacklist=None, config_cond_whitelist=None):
super().__init__(ast)
self._method_cache = {}
self.state = state
self.ccb = config_cond_blacklist
self.ccw = config_cond_whitelist
self.assignments = []
def visit(self, node, path = None, invariants = None):
@ -172,7 +175,13 @@ class StateAssignmentVisitor(NodeVisitorFuncCallForward):
#print("CAL path", path_to_str(path))
cases = path_filter(path, c_ast.Case)
#print(cases)
new_invariants = [x.expr.name for x in cases]
#new_invariants = [x.expr.name for x in cases]
new_invariants = []
for x in cases:
clev = CaseLabelExtractionVisitor()
clev.visit(x.expr)
new_invariants.append(clev.label)
invariants = invariants.copy()
for ni in new_invariants:
if not(ni in invariants):
@ -218,14 +227,51 @@ class StateAssignmentVisitor(NodeVisitorFuncCallForward):
# conditional assignment detection
asm_if = path_select_last('If', path)
asm_case = path_select_last('Case', path)
asm_ifs = path_filter(path, c_ast.If)
asm_cases = path_filter(path, c_ast.Case)
subpath_case = path_slice_back(case_node, path)
is_exhaustive_conditional = True if asm_if is None else (asm_if.iftrue is not None) and (asm_if.iffalse is not None)
is_conditional = path_contains(subpath_case, c_ast.If) and not(is_exhaustive_conditional)
type_condition_antivalent = False
#if asm_case is not None:
for case in asm_cases:
elsv = ExprListSerializerVisitor()
elsv.visit(case.expr)
print("big case", elsv.serial[0])
if elsv.serial[0] in self.ccb:
type_condition_antivalent = True
break
if not(type_condition_antivalent):
for if_node in asm_ifs:
cg = c_generator.CGenerator()
if_expr = cg.visit(if_node.cond)
print("big if", if_expr)
for incl_cond in self.ccw:
match = re.search(f"(\!=|==)[\(\)\w\d\s]+{incl_cond}", if_expr)
if match is not None:
op = match.groups()[0]
if op == '!=':
type_condition_antivalent = True
break
for excl_cond in self.ccb:
match = re.search(f"(\!=|==)[\(\)\w\d\s]+{excl_cond}", if_expr)
if match is not None:
op = match.groups()[0]
if op == '==':
type_condition_antivalent = True
break
if type_condition_antivalent:
break
if not(isinstance(n.rvalue, c_ast.Constant) or isinstance(n.rvalue, c_ast.BinaryOp) or isinstance(n.rvalue, c_ast.TernaryOp)):
rval_str = n.rvalue.name
#print(f">>>> {rval_str} == {self.state}")
if rval_str == self.state:
print(f">>>> {rval_str} == {self.state} antivalent={type_condition_antivalent}")
if (rval_str == self.state) and not(type_condition_antivalent):
self.assignments.append((n,path,fallthrough_case_names,is_conditional,invariants))
class EnumDefVisitor(c_ast.NodeVisitor):
@ -321,10 +367,12 @@ class SwitchCasePropertyVisitor(c_ast.NodeVisitor):
else:
lvalue = node.lvalue.name
if isinstance(node.rvalue, c_ast.Constant):
rvalue = f"{node.rvalue.type }({node.rvalue.value})"
else:
rvalue = node.rvalue.name
#if isinstance(node.rvalue, c_ast.Constant):
# rvalue = f"{node.rvalue.type }({node.rvalue.value})"
#else:
# rvalue = node.rvalue.name
cg = c_generator.CGenerator()
rvalue = cg.visit(node.rvalue)
prop = f"{lvalue}<={rvalue}"
self.properties.append(prop)