Interpretation-Based Violation Witness Validation for C: NITWIT
47
For the assumption evaluation we execute assumptions (recall a WA-transition
may have multiple of them) as conditions in the program context and if any one
of them fails, then the control edge is considered as non-matching. If an assumption resolves a nondeterministic variable (e.g. the assumption x = 2 resolves the
nondeterministic variable x), then we automatically accept it and store the given
variable value. A variable becomes nondeterministic if it has no initialization or
if it is assigned a nondeterministic value (for example from a VERIFIER nondet
function). Analogously, it becomes deterministic when a deterministic value is
assigned to it, e.g., as a result from an expression involving only deterministic
variables and constants. Moreover, if in the assumption evaluator an assumption
involving a nondeterministic variable occurs and is resolved, then the variable
gets assigned the new value and is registered as being deterministic.
5 Evaluation
5.1 Benchmarks
Primarily, we have tested nitwit on witnesses produced during SV-COMP
2019 [6], however, as data from the current edition were already available to
us, we present the results attained during SV-COMP 2020. The set of all witnesses produced is available at [9]. It consists of the witnesses and index files that
contain information about the witness producer, date of creation, corresponding
program file and its hash value (that can be used to find the program in the
SV-COMP program repository), the programming language, specification, type
of witness and so on. The witnesses and programs cover a large spectrum of
possible language features in a variety of applications and settings. We used the
dataset of the previous edition [7] to evaluate nitwit extensively and prepare it
for competing in 2020.
During the competition nitwit was executed only on witnesses in the category ReachSafety with a known specification violation as our validator targets
only reachability safety violations. This amounts to a set of 11 533 violation
witnesses produced by 17 different verifiers.
The witnesses were not manually reviewed to check for each if the language
of the WA indeed contains a violating path. This would be a laborious task —
doing it automatically is a better fit, which in fact is precisely what validators
are designed for. Nevertheless, this means that we cannot claim that our or other
validators are incorrect when they do not find a violation, because the witness
may steer them inappropriately. As the dataset does not exclusively contain
exact witnesses, some witnesses might not resolve enough nondeterminism for
nitwit to find a violation based on the selected single execution.
Witnesses show a lot of heterogeneity based on their producer. Whilst some
are very detailed, like in the case of Pinaka and Map2Check with approximately 23 and 13 thousand nodes on average respectively, others tend to keep the
WA more succinct or even minimal. For example, tools like Brick or DIVINE
usually provide the least verbose witnesses. The average number of edges typically lies near the average number of nodes due to the fact that witness producers
47
For the assumption evaluation we execute assumptions (recall a WA-transition
may have multiple of them) as conditions in the program context and if any one
of them fails, then the control edge is considered as non-matching. If an assumption resolves a nondeterministic variable (e.g. the assumption x = 2 resolves the
nondeterministic variable x), then we automatically accept it and store the given
variable value. A variable becomes nondeterministic if it has no initialization or
if it is assigned a nondeterministic value (for example from a VERIFIER nondet
function). Analogously, it becomes deterministic when a deterministic value is
assigned to it, e.g., as a result from an expression involving only deterministic
variables and constants. Moreover, if in the assumption evaluator an assumption
involving a nondeterministic variable occurs and is resolved, then the variable
gets assigned the new value and is registered as being deterministic.
5 Evaluation
5.1 Benchmarks
Primarily, we have tested nitwit on witnesses produced during SV-COMP
2019 [6], however, as data from the current edition were already available to
us, we present the results attained during SV-COMP 2020. The set of all witnesses produced is available at [9]. It consists of the witnesses and index files that
contain information about the witness producer, date of creation, corresponding
program file and its hash value (that can be used to find the program in the
SV-COMP program repository), the programming language, specification, type
of witness and so on. The witnesses and programs cover a large spectrum of
possible language features in a variety of applications and settings. We used the
dataset of the previous edition [7] to evaluate nitwit extensively and prepare it
for competing in 2020.
During the competition nitwit was executed only on witnesses in the category ReachSafety with a known specification violation as our validator targets
only reachability safety violations. This amounts to a set of 11 533 violation
witnesses produced by 17 different verifiers.
The witnesses were not manually reviewed to check for each if the language
of the WA indeed contains a violating path. This would be a laborious task —
doing it automatically is a better fit, which in fact is precisely what validators
are designed for. Nevertheless, this means that we cannot claim that our or other
validators are incorrect when they do not find a violation, because the witness
may steer them inappropriately. As the dataset does not exclusively contain
exact witnesses, some witnesses might not resolve enough nondeterminism for
nitwit to find a violation based on the selected single execution.
Witnesses show a lot of heterogeneity based on their producer. Whilst some
are very detailed, like in the case of Pinaka and Map2Check with approximately 23 and 13 thousand nodes on average respectively, others tend to keep the
WA more succinct or even minimal. For example, tools like Brick or DIVINE
usually provide the least verbose witnesses. The average number of edges typically lies near the average number of nodes due to the fact that witness producers