Combining Verifiers

It may happen that a verifier does not terminate. In this case we can try to use another verifier and start from scratch. Instead of starting from scratch, it might be promising to reuse some of the work that the first verifier did.

Conditional Model Checking

In Conditional Model Checking, the first verifier outputs a condition in form of an assumption automaton. This automaton contains the information about the parts of the state space that do still need to be considered by the second verifier. The second verifier then gets uses this information and might therefore be able to solve the problem faster than without the information passed from the first verifier. The exchange format for the conditions is supported by different verifiers, e.g. CPAchecker or Ultimate.

CPachecker can be used to output such conditions, e.g. in the case the time limit specified by the user is exceeded. It can also use conditions provided by another verifier (or CPAchecker itself).

Example

We now look at a short example of how this can be done with CPAchecker.

The program cmc-example.c that we use can be seen in the following listing:

extern void __VERIFIER_error() __attribute__ ((__noreturn__)); int computeDiscount(unsigned int day, int isThursday) { int discount; if (isThursday) { discount=5; } else { discount=day%7; } if(discount<0 || discount>7) { ERROR: __VERIFIER_error(); } return discount; }

(for such a program without main function, CPAchecker will call the function with nondeterministic values for the arguments)

Step/Verifier 1: CPAchecker with Value Analysis

We will first try to solve it using a value analysis. For that, we use a special configuration file that tells CPAchecker to generate the conditions under output/AssumptionsAutomaton.txt in case the analysis is not successful. Note that we could also provide these additional options directely on the commandline or create our own configuration file in case we want to do the same for an analysis different than value analysis. Here is our command:

scripts/cpa.sh -config config/components/valueAnalysis-generate-cmc-condition.properties \
               -spec config/properties/unreach-call.prp \
               examples/cmc-example.c

And here is the corresponding output:

[...]
Error: Error path found, but identified as infeasible by counterexample check
with CPACHECKER. (CounterexampleCheckAlgorithm.run, SEVERE)

Verification result: UNKNOWN, incomplete analysis.
More details about the verification run can be found in the directory "./output".
Graphical representation included in the file "./output/Report.html".

The value analysis found a counterexample but it turned out to be infeasible. In this case, the value analysis aborts and also outputs the assumption automaton atoutput/AssumptionsAutomaton.txt.

Step/Verifier 2: CPAchecker with Predicate Analysis

We can now run a different analysis and pass the assumption automaton in order to reuse the information that the value analysis was able to collect before it aborted: As before, there is a configuration file that already contains the additional options we need for telling CPAchecker to use the conditions in output/AssumptionsAutomaton.txt.

We execute the following command:

scripts/cpa.sh -config config/components/predicateAnalysis-use-cmc-condition.properties \
               -spec config/properties/unreach-call.prp \
               examples/cmc-example.c

The output tells us that the predicate analysis successfully proved the program to be correct:

[...]
Verification result: TRUE. No property violation found by chosen configuration.
More details about the verification run can be found in the directory "./output".
Graphical representation included in the file "./output/Report.html".

Combining both Steps

Note that there is also a configuration that allows us to do the previous two steps in one call:

scripts/cpa.sh -combinations-value10+pred-cmc \
               -spec config/properties/unreach-call.prp \
               examples/cmc-example.c

Reducer-Based Construction of Conditional Verifiers

For performing CMC like seen in the last section, the first verifier needs to be able to output the conditions in the right format (assumption automaton) and the second verifier needs to be able to take these conditions as input. The requirements for the second verifier can be lifted if we can somehow add the information from the assumption automaton in the program itself. this can be realized by a so-called reducer that takes a program and a corresponding assumption automaton as input and outputs a new, residual program. The reducer makes sure that the semantics of the residual program is the same as the semantics of the old program provided the conditions generated by the first verifier hold. The residual program can now be given to any verifier that is able to handle C programs. This allows us to also use verifiers in the second step that do not support CMC.

Example

We will now try the same as we did before with cmc-example.c, except instead of passing the information via AssumptionsAutomaton.txt from the first verifier to the second verifier, we generate a residual program.

Step 1: CPAchecker with Value Analysis (as before)

This step is no different than what we did in the example for CMC:

scripts/cpa.sh -config config/components/valueAnalysis-generate-cmc-condition.properties \
               -spec config/properties/unreach-call.prp \
               examples/cmc-example.c

The value analysis aborts because of an infeasible counterexample and outputs the conditions in output/AssumptionsAutomaton.txt.

Step 2: Reducer (new)

We generate a residual program using the original program and the conditions derived by the first analysis:

scripts/cpa.sh -residualProgramGenerator \
               -spec config/properties/unreach-call.prp \
               examples/cmc-example.c

By default, it is assumed that the assumption-automaton-file resides at output/AssumptionsAutomaton.txt. If this is not the case, add the option -setprop AssumptionAutomaton.cpa.automaton.inputFile=PATH/TO/FILE where PATH/TO/FILE is the path to your automaton file.

The command generates a residual program at output/residual_program.c, which will look similar to this:

int __return_main; void __VERIFIER_error(); int computeDiscount(unsigned int day, int isThursday); int __return_20; int computeDiscount(unsigned int day, int isThursday) { int discount; if (isThursday == 0) { discount = 5; if (discount < 0) { return __return_main; } else { if (discount > 7) { return __return_main; } else { label_15:; __return_20 = discount; return __return_20; } } } else { discount = day % 7; if (discount < 0) { label_13:; __VERIFIER_error(); return __return_main; } else { if (discount > 7) { goto label_13; } else { goto label_15; } } } }

Step 3: CPAchecker with Predicate Analysis (now unaware of CMC)

As a last step, we can now verify the residual program we just generated with a predicate analysis:

scripts/cpa.sh -predicateAnalysis \
               -spec config/properties/unreach-call.prp \
                output/residual_program.c

As before, the predicate analysis manages to prove the program correct. The big difference is that we used the default configuration (-predicateAnalysis) for the predicate analysis without the need to instruct the verifier to read in any assumption automaton. So while we used CPAchecker as the second verifier in this example, we could pass our residual program to any of the verifiers that participated in SV-COMP 2018

results matching ""

    No results matching ""