46
J. ˇ
Svejda et al.
As the program executes, the WA progresses through its states until either
the execution ends or the error function is called. The latter we consider a
testament to the property violation, accepting the witness.
Implementing nitwit. An interpreter is a program that takes as input a program, parses it and executes commands as part of its own runtime instead of
producing machine code like a compiler. Interpreters translate programs directly
into the behavior they represent; they keep track of all variable values and execute statements based on results of expressions and control flow [21,1,20].
nitwit’s input is a C program. The choice of C interpreters is limited —
moreover, compiled C often widely outperforms interpreters in terms of speed,
due to extensive compiler optimizations and the unavoidable overhead in parsing
and program state management. Nonetheless, in a witness validation setting,
when a program only needs to be executed once, the advantage of machine
code speed can fade away, because compilation-based validators spend effort on
optimizations and translation, which is part of validation time. Furthermore, we
wanted to control the simulated program during runtime to alter variables and
track the position in source code, which is difficult after compilation.
Our requirements on an interpreter in the order of relevance were: (i) an
open-source license permitting free use and distribution of the source code, (ii) a
moderate learning curve because of the limited time for implementation, (iii) flexibility so that we can easily modify it, (iv) good coverage of C and (v) tested with
realistic C programs. We have chosen PicoC
4 , a portable interpreter written in
C with a very small code base originally built as a scripting language interpreter
for unmanned aerial vehicles (UAVs). In its original form, PicoC supports the
basics of ANSI C, but misses some important features like function pointers or
an implementation of const variables. For being able to execute C99-compliant
C code, which is common in the benchmarks of SV-COMP, we extended it with
new functionalities, such as goto constructs, function pointers, the double, long
long and const types, better parsing for numerical constants, variable shadowing, struct initialization and bit fields.
By using an interpreter, nitwit has full control over the simulation of a program. For our purposes, we have supplemented PicoC with function callbacks at
locations corresponding to places from which a verifier might extract control-flow
edges. During execution, the interpreter returns control to our witness automaton whenever it reaches a callback. The callbacks carry all of the necessary information like the current position, variable values, presence of non-determinism
or the selected branch in if-statements, loops and ternary operators.
The validator’s managing component stores the witness automaton and starts
the program’s simulation in PicoC. It also stores the current control state in the
witness and tries to progress to the error state whenever it receives a callback
and the source code and state-space guards match. If a state-space guard involves a nondeterministic variable, nitwit attempts to extract a value from the
given assumption. Upon success, the value is stored in the variable management
system.
4 https://gitlab.com/zsaleeba/picoc
J. ˇ
Svejda et al.
As the program executes, the WA progresses through its states until either
the execution ends or the error function is called. The latter we consider a
testament to the property violation, accepting the witness.
Implementing nitwit. An interpreter is a program that takes as input a program, parses it and executes commands as part of its own runtime instead of
producing machine code like a compiler. Interpreters translate programs directly
into the behavior they represent; they keep track of all variable values and execute statements based on results of expressions and control flow [21,1,20].
nitwit’s input is a C program. The choice of C interpreters is limited —
moreover, compiled C often widely outperforms interpreters in terms of speed,
due to extensive compiler optimizations and the unavoidable overhead in parsing
and program state management. Nonetheless, in a witness validation setting,
when a program only needs to be executed once, the advantage of machine
code speed can fade away, because compilation-based validators spend effort on
optimizations and translation, which is part of validation time. Furthermore, we
wanted to control the simulated program during runtime to alter variables and
track the position in source code, which is difficult after compilation.
Our requirements on an interpreter in the order of relevance were: (i) an
open-source license permitting free use and distribution of the source code, (ii) a
moderate learning curve because of the limited time for implementation, (iii) flexibility so that we can easily modify it, (iv) good coverage of C and (v) tested with
realistic C programs. We have chosen PicoC
4 , a portable interpreter written in
C with a very small code base originally built as a scripting language interpreter
for unmanned aerial vehicles (UAVs). In its original form, PicoC supports the
basics of ANSI C, but misses some important features like function pointers or
an implementation of const variables. For being able to execute C99-compliant
C code, which is common in the benchmarks of SV-COMP, we extended it with
new functionalities, such as goto constructs, function pointers, the double, long
long and const types, better parsing for numerical constants, variable shadowing, struct initialization and bit fields.
By using an interpreter, nitwit has full control over the simulation of a program. For our purposes, we have supplemented PicoC with function callbacks at
locations corresponding to places from which a verifier might extract control-flow
edges. During execution, the interpreter returns control to our witness automaton whenever it reaches a callback. The callbacks carry all of the necessary information like the current position, variable values, presence of non-determinism
or the selected branch in if-statements, loops and ternary operators.
The validator’s managing component stores the witness automaton and starts
the program’s simulation in PicoC. It also stores the current control state in the
witness and tries to progress to the error state whenever it receives a callback
and the source code and state-space guards match. If a state-space guard involves a nondeterministic variable, nitwit attempts to extract a value from the
given assumption. Upon success, the value is stored in the variable management
system.
4 https://gitlab.com/zsaleeba/picoc