Initial commit

LICENSE

@@ -0,0 +1,11 @@
+Copyright (c) 2022 flip. 
+
+Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

README.md

@@ -0,0 +1,7 @@
+# LTL Verifier for C FSM
+
+Kripkomat is a small utility which analyzes a C finite state machine
+and generates a NuSMV model.
+Properties are extracted automatically.
+
+This is very much a proof of concept.

analyze.py

@@ -0,0 +1,340 @@
+#-----------------------------------------------------------------
+# pycparser: dump_ast.py
+#
+# Basic example of parsing a file and dumping its parsed AST.
+#
+# Eli Bendersky [https://eli.thegreenplace.net/]
+# License: BSD
+#-----------------------------------------------------------------
+from __future__ import print_function
+import argparse
+import sys
+from modelbuilder import *
+
+# This is not required if you've installed pycparser into
+# your site-packages/ with setup.py
+sys.path.extend(['.', '..'])
+
+from pycparser import parse_file, c_ast
+
+func_table = {}
+enum_table = {}
+assign_table = []
+
+state_enums = []
+
+# A visitor with some state information (the funcname it's looking for)
+class FuncCallVisitor(c_ast.NodeVisitor):
+    def __init__(self, funcname):
+        self.funcname = funcname
+
+    def visit_FuncCall(self, node):
+        if node.name.name == self.funcname:
+            print('%s called at %s' % (self.funcname, node.name.coord))
+        # Visit args in case they contain more func calls.
+        if node.args:
+            self.visit(node.args)
+
+
+def show_func_calls(ast, funcname):
+    v = FuncCallVisitor(funcname)
+    v.visit(ast)
+
+class FuncDefVisitor(c_ast.NodeVisitor):
+    def visit_FuncDef(self, node):
+        print('%s at %s' % (node.decl.name, node.decl.coord))
+        func_table[node.decl.name] = node
+
+def show_func_defs(ast):
+    v = FuncDefVisitor()
+    v.visit(ast)
+
+class StateAssignmentVisitor(c_ast.NodeVisitor):
+    def __init__(self, state):
+        super().__init__()
+        self.state = state
+        self.assignments = []
+
+    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
+        #return '%s %s %s' % (self.visit(n.lvalue), n.op, rval_str)
+        if rval_str == self.state:
+            if isinstance(n.lvalue, c_ast.StructRef):
+                print(f"found struct assignment '{n.lvalue.children()[0][1].name}->{n.lvalue.children()[1][1].name}'<='{rval_str}'")
+            else:
+                print(f"found assignment '{n.lvalue.name}'<='{rval_str}'")
+            print(" -> at path '",end="")
+            for p in path:
+                print(p.__class__.__name__,end=",")
+            print("'")
+            self.assignments.append((n,path))
+            #print("+++")
+            #n.show()
+            #print("---")
+
+class EnumDefVisitor(c_ast.NodeVisitor):
+    def __init__(self, name):
+        super().__init__()
+        self._name = name
+
+    def visit_Enum(self, node):
+        print('enum %s at %s' % (node.name, node.coord))
+        enum_table[self._name] = node
+
+class TypedefVisitor(c_ast.NodeVisitor):
+    def visit_Typedef(self, node):
+        print(f"typedef {node.name} at {node.coord}")
+        print(f"---")
+        node.children()[0][1].show()
+        print("+++")
+        ev = EnumDefVisitor(node.name)
+        ev.visit(node)
+
+
+class EnumVisitor(c_ast.NodeVisitor):
+    def __init__(self):
+        super().__init__()
+        self.enum_names = []
+
+    def visit_Enumerator(self, node):
+        #print('enumerator %s at %s' % (node.name, node.coord))
+        self.enum_names.append(node.name)
+
+def find_longest_path(paths):
+    ms = 0
+    mp = None
+    for path in paths:
+        s = len(path)
+        if s > ms:
+            ms = s
+            mp = path
+    return mp
+
+def find_shortest_path(paths):
+    ms = 9000
+    mp = None
+    for path in paths:
+        s = len(path)
+        if s < ms:
+            ms = s
+            mp = path
+    return mp
+
+def find_common_ancestor(paths):
+    shortest_path = find_shortest_path(paths)
+    
+    last_common = None
+    for gen_i,_ in enumerate(shortest_path):
+        common = True
+        last_node = paths[0][gen_i]
+
+        for path in paths:
+            if last_node == path[gen_i]:
+                common = True
+                last_node = path[gen_i]
+            else:
+                common = False
+        if common:
+            last_common = last_node
+    return last_common
+        
+
+class SwitchCaseTermVisitor(c_ast.NodeVisitor):
+    def __init__(self, asm_node):
+        super().__init__()
+        self._asm_node = asm_node
+        self.hit = False
+
+    def visit_Assignment(self, node):
+        if node == self._asm_node:
+            self.hit = True
+
+class SwitchCaseTranVisitor(c_ast.NodeVisitor):
+    def __init__(self, asm_node):
+        super().__init__()
+        self._asm_node = asm_node
+        self.tran_table = []
+
+    def visit_Case(self, node):
+        sctv = SwitchCaseTermVisitor(self._asm_node)
+        sctv.visit(node)
+        if sctv.hit:
+            #print(f"Transition! {node.children()[0][1].name} -> {self._asm_node.rvalue.name}");
+            self.tran_table.append((node.children()[0][1].name, self._asm_node.rvalue.name))
+
+class SwitchCasePropertyVisitor(c_ast.NodeVisitor):
+    def __init__(self, state_asmts):
+        super().__init__()
+        self._sas = state_asmts
+        self.properties = []
+
+    def visit_Assignment(self, node):
+        if not(node in self._sas):
+            #print("Property:", node)
+            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}"
+            #print(f"found property '{prop}'")
+            self.properties.append(prop)
+
+
+class SwitchCaseCodePropertyVisitor(c_ast.NodeVisitor):
+    def __init__(self, case, state_asmts):
+        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
+
+if __name__ == "__main__":
+    argparser = argparse.ArgumentParser('Create a Kripke Structure Model from C Code')
+    argparser.add_argument('filename',
+                           default='examples/c_files/basic.c',
+                           nargs='?',
+                           help='name of file to parse')
+    argparser.add_argument('--coord', help='show coordinates in the dump',
+                           action='store_true')
+
+    argparser.add_argument('--func', help='process function')
+    argparser.add_argument('--enum', help='state enum')
+    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')
+    args = argparser.parse_args()
+
+    ast = parse_file(args.filename, use_cpp=False)
+    #ast.show(showcoord=args.coord)
+    show_func_defs(ast)
+    
+    enumvis = TypedefVisitor()
+    enumvis.visit(ast)
+
+    #func_table[args.func].show(showcoord=args.coord)
+    
+    # for name,node in enum_table.items():
+        # print(f"Enum '{name}'")
+        # print("---")
+        # node.show()
+        # print("+++")
+        # ev = EnumVisitor()
+        # ev.visit(node)
+    
+    state_asmts = []
+    
+    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
+    else:
+        print(f"state enum '{args.enum}' not found")
+
+    paths = []
+    for asm in state_asmts:
+        paths.append(asm[1])
+
+    common = find_common_ancestor(paths)
+    #print(f"common ancestor is {common}")
+    
+    tran_table = []
+
+    for sa in state_asmts:
+        #print(sa[0])
+        sctv = SwitchCaseTranVisitor(sa[0])
+        sctv.visit(common)
+        tran_table += sctv.tran_table
+
+    comp_tt = {}
+    print("Compacting Transition Table")
+    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]]
+    
+    pure_sa = [x[0] for x in state_asmts]
+    #print(pure_sa)
+    states = comp_tt.keys()
+    print("States: ", ",".join(states))
+    
+    props_by_state = {}
+    print("Compact Table:")
+    for n,ms in comp_tt.items():
+        print(n,end="->{")
+        for m in ms:
+            print(m,end=",")
+        print("}")
+
+        # find properties
+        sccpv = SwitchCaseCodePropertyVisitor(n, pure_sa)
+        sccpv.visit(common)
+        if len(sccpv.properties) > 0:
+            props_by_state[n] = sccpv.properties
+    
+    properties = {}
+    for state,props in props_by_state.items():
+        #print(f"{state} properties:")
+        for prop in props:
+            #print(f" - {prop}")
+            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}")
+    
+    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()
+    print("-------------------")
+    print(nusmv)
+
+    if args.output is not None:
+        with open(args.output, "wt") as f:
+            n = f.write(nusmv)

dump.py

@@ -0,0 +1,30 @@
+#-----------------------------------------------------------------
+# pycparser: dump_ast.py
+#
+# Basic example of parsing a file and dumping its parsed AST.
+#
+# Eli Bendersky [https://eli.thegreenplace.net/]
+# License: BSD
+#-----------------------------------------------------------------
+from __future__ import print_function
+import argparse
+import sys
+
+# This is not required if you've installed pycparser into
+# your site-packages/ with setup.py
+sys.path.extend(['.', '..'])
+
+from pycparser import parse_file
+
+if __name__ == "__main__":
+    argparser = argparse.ArgumentParser('Dump AST')
+    argparser.add_argument('filename',
+                           default='examples/c_files/basic.c',
+                           nargs='?',
+                           help='name of file to parse')
+    argparser.add_argument('--coord', help='show coordinates in the dump',
+                           action='store_true')
+    args = argparser.parse_args()
+
+    ast = parse_file(args.filename, use_cpp=False)
+    ast.show(showcoord=args.coord)

formulae.ltl

@@ -0,0 +1,3 @@
+X b
+F a
+G( a -> F(b))

model.smv

@@ -0,0 +1,27 @@
+
+MODULE main
+VAR
+state : { STATE_I,STATE_C,STATE_D,STATE_A,STATE_B };
+ASSIGN
+    init(state) := STATE_I;
+    next(state) :=
+        case
+            state = STATE_I : {STATE_A,STATE_B};
+            state = STATE_C : {STATE_A};
+            state = STATE_D : {STATE_B};
+            state = STATE_A : {STATE_C,STATE_D};
+            state = STATE_B : {STATE_C};
+        esac;
+DEFINE
+    -- Property "p_fsm->m_b<=true"
+    a := state = STATE_C | state = STATE_B;
+
+    -- Property "p_fsm->m_a<=true"
+    b := state = STATE_A | state = STATE_B;
+
+LTLSPEC
+    X b;
+LTLSPEC
+    F a;
+LTLSPEC
+    G( a -> F(b));

modelbuilder.py

@@ -0,0 +1,89 @@
+
+MODEL = """
+MODULE {name}
+VAR
+state : {{ {states} }};
+ASSIGN
+    init(state) := {initial};
+    next(state) :=
+        case
+{transitions}
+        esac;
+DEFINE
+{properties}
+"""
+
+TRAN = "            state = {n} : {{{ms}}};"
+PROP = """    -- Property "{prop}"
+    {alias} := {logic};
+"""
+PROP_LOGIC = "state = {state}"
+
+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"):
+        self._name = name
+        self._states = states
+        self._initial = initial
+        self._tran = transitions
+        self._props = properties
+        self._ltls = ltls
+        
+        self._propalias = {}
+        for no,prop in enumerate(properties.keys()):
+            self._propalias[prop] = base_10_to_alphabet(no + 1)
+
+    def generate(self):
+        # build model
+        states_decl = ",".join(self._states)
+        transitions = []
+
+        for n,ms in self._tran.items():
+            transition = TRAN.format(n=n, ms=",".join(ms))
+            transitions.append(transition)
+
+        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)
+
+        out = MODEL.format(name=self._name,
+                            states=states_decl,
+                            initial=self._initial,
+                            transitions="\n".join(transitions),
+                            properties="\n".join(properties))
+
+        # add LTL formulas
+        for ltl in self._ltls:
+            out += LTL_FORM.format(ltl=ltl)
+        return out

out_exp.smv

@@ -0,0 +1,24 @@
+MODULE main
+VAR
+state : {STATE_I,STATE_A,STATE_B,STATE_C,STATE_D};
+ASSIGN
+    init(state) := STATE_I;
+    next(state) :=
+        case
+            state = STATE_I : {STATE_A,STATE_B};
+            state = STATE_A : {STATE_C,STATE_D};
+            state = STATE_B : {STATE_C};
+            state = STATE_C : {STATE_A};
+            state = STATE_D : {STATE_B};
+        esac;
+DEFINE
+    a := state = STATE_A | state = STATE_B;
+    b := state = STATE_C;
+
+LTLSPEC
+    X a;
+LTLSPEC
+    F b;
+LTLSPEC
+    G( b -> F(a))
+

test.c

@@ -0,0 +1,82 @@
+typedef char bool;
+
+typedef enum
+{
+    STATE_I = 0,
+    STATE_A,
+    STATE_B,
+    STATE_C,
+    STATE_D
+}
+testfsm_state_t;
+
+typedef struct
+{
+    testfsm_state_t m_state;
+    bool m_a;
+    bool m_b;
+} testfsm_t;
+
+void process(testfsm_t *p_fsm, const bool input)
+{
+    testfsm_state_t nextState = p_fsm->m_state;
+
+    p_fsm->m_a = false;
+    p_fsm->m_b = false;
+
+    switch(p_fsm->m_state)
+    {
+        case STATE_I:
+            if (!input)
+                nextState = STATE_A;
+            else
+                nextState = STATE_B;
+            break;
+        case STATE_A:
+            p_fsm->m_a = true;
+            if (!input)
+                nextState = STATE_D;
+            else
+                nextState = STATE_C;
+            break;
+        case STATE_B:
+            p_fsm->m_a = true;
+            p_fsm->m_b = true;
+            nextState = STATE_C;
+            break;
+        case STATE_C:
+            p_fsm->m_b = true;
+            nextState = STATE_A;
+            break;
+        case STATE_D:
+            nextState = STATE_B;
+            break;
+    }
+
+    p_fsm->m_state = nextState;
+}
+
+bool randbool(int throws)
+{
+    bool stillTrue = true;
+    for (int i = 0; i < throws; ++i)
+    {
+        stillTrue &= rand() & 1;
+    }
+    return stillTrue;
+}
+
+int main()
+{
+    testfsm_t fsm = { .m_state = STATE_I, .m_a = false, .m_b = false };
+    bool input = false;
+
+    srand(0);
+    for (int j = 0; j < 100; ++j)
+    {
+        input = randbool(1);
+        process(&fsm, input);
+    }
+
+    return 0;
+}