Interpretation-Based Violation Witness Validation for C: NITWIT
45
code 107. This signals the successful validation of a witness, because the error
was reached.
FShell-witness2test This tool does not rely on an existing software model
checker. It begins with reading the specification and parses the program with
pycparser
2 – a Python library for C, which constructs an abstract syntax tree
(AST). This AST is traversed to find uninitialized variables and uses of nondeterministic functions. This yields watch points, indicating where variable(s)
need to be resolved in order to find the right concrete path. Once watch points
are established, the tool reads the provided witness and obtains a sequence of
control states from program start to the error state. Further on, states of the
sequence are matched to the found watch points. For any such match, the tool
tries to determine the watch point value from a corresponding assumption in the
witness. Finally, these values are added to a test vector, which is transformed
into a test harness prepared for compilation. If the function VERIFIER error
is called during execution, then the witness is accepted.
4 Interpretation-based Witness Validation
This section presents a new interpretation-based validator for violation witnesses
of C programs with an embedded
3 reachability safety property. The validator is named Nitwit Validator (or nitwit for short) as a shorthand for
iNterpretation-based vIolaTion WITness Validator. The programs must designate the error location by a function call to VERIFIER error in order for
nitwit to recognize that a program violates the invariant “begin in main and
never call VERIFIER error”. nitwit is restricted to these programs.
A bird’s eye view on nitwit. Our implementation approach consists of combining an existing C interpreter with a witness automaton that provides witness
assumptions used for resolving variables according to the current position (l i , v i )
in the program execution. The WA is fed with information from the interpreter,
which executes the C program step by step. For validations both source code
and state-space guards are taken into account. When a state-space guard (an
assumption) does not hold for the current variable values, then the WA does not
proceed. To illustrate, suppose an integer variable x initiated to one and incremented on every line (numbered from one). A witness control edge consisting of
an assumption x = 7 matches only on line seven and will block the WA until then
if no other edge is satisfied. If, however, the assumption concerns nondeterministic variables, then we extract a value from it and resolve the nondeterminism in
the interpreter. E.g., if x is not initialized at all, then assumption x = 7 assigns
it the value 7 already on line one.
2 https://github.com/eliben/pycparser
3 The program is enhanced with error location(s) VERIFIER error, assume statements VERIFIER assume with conditions and calls to VERIFIER nondet functions,
which return nondeterministic values.
45
code 107. This signals the successful validation of a witness, because the error
was reached.
FShell-witness2test This tool does not rely on an existing software model
checker. It begins with reading the specification and parses the program with
pycparser
2 – a Python library for C, which constructs an abstract syntax tree
(AST). This AST is traversed to find uninitialized variables and uses of nondeterministic functions. This yields watch points, indicating where variable(s)
need to be resolved in order to find the right concrete path. Once watch points
are established, the tool reads the provided witness and obtains a sequence of
control states from program start to the error state. Further on, states of the
sequence are matched to the found watch points. For any such match, the tool
tries to determine the watch point value from a corresponding assumption in the
witness. Finally, these values are added to a test vector, which is transformed
into a test harness prepared for compilation. If the function VERIFIER error
is called during execution, then the witness is accepted.
4 Interpretation-based Witness Validation
This section presents a new interpretation-based validator for violation witnesses
of C programs with an embedded
3 reachability safety property. The validator is named Nitwit Validator (or nitwit for short) as a shorthand for
iNterpretation-based vIolaTion WITness Validator. The programs must designate the error location by a function call to VERIFIER error in order for
nitwit to recognize that a program violates the invariant “begin in main and
never call VERIFIER error”. nitwit is restricted to these programs.
A bird’s eye view on nitwit. Our implementation approach consists of combining an existing C interpreter with a witness automaton that provides witness
assumptions used for resolving variables according to the current position (l i , v i )
in the program execution. The WA is fed with information from the interpreter,
which executes the C program step by step. For validations both source code
and state-space guards are taken into account. When a state-space guard (an
assumption) does not hold for the current variable values, then the WA does not
proceed. To illustrate, suppose an integer variable x initiated to one and incremented on every line (numbered from one). A witness control edge consisting of
an assumption x = 7 matches only on line seven and will block the WA until then
if no other edge is satisfied. If, however, the assumption concerns nondeterministic variables, then we extract a value from it and resolve the nondeterminism in
the interpreter. E.g., if x is not initialized at all, then assumption x = 7 assigns
it the value 7 already on line one.
2 https://github.com/eliben/pycparser
3 The program is enhanced with error location(s) VERIFIER error, assume statements VERIFIER assume with conditions and calls to VERIFIER nondet functions,
which return nondeterministic values.