Exporting Invariants?

[Gilbert Pajela]

How do I configure CPAchecker so that it will output the invariants that it generates? I am running CPAchecker-2.0. I tried using the option -setprop cpa.predicate.invariants.export=true along with the -kInduction-kipdrInvariants config on the program eq2.c from the paper "Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art". It generates the file invariants.txt in the output directory, but all it contains is the following:

loop__main__14:
(set-info :source |printed by MathSAT|)
(assert false)

The invariant for that program is y == z, so I'm looking for some way for CPAchecker to output at least that (plus hopefully some of the candidate invariants, if any, that it generated along the way). The output I got above was similar for other programs I tried.

I also tried the option cinvariants.export=true. That generated a file inv-eq2.c, but it was identical to the input program. That happened for each different program I tried except for the loop-lit/afnp2014_true-unreach-call.c.i benchmark (from SV-COMP’15), which caused CPAchecker to crash with the exception "Exception in thread "main" java.lang.UnsupportedOperationException: Unexpected operand". (Here, I used the -kInduction-kipdrdfInvariants config with the option cpa.invariants.useMod2Template=true.) The generated file inv-afnp2014_true-unreach-call.c.i was different from the input program -- it contained some assume statements, but it was not a complete program (presumably due to the crash).

Finally, I also tried the option cpa.predicate.invariants.dumpInvariantGenerationAutomata=true, but that didn't seem to do anything. Is there an option I missed, or perhaps some combination of options I need to enable to get CPAchecker to output the invariants that it generates? Any help is greatly appreciated.

Thanks,

Gilbert

[Martin Spießl]

Hi Gilbert,

Thanks for your interest in CPAchecker!

On 02.02.21 15:58, Gilbert Pajela wrote:
>
> How do I configure CPAchecker so that it will output the invariants that it generates? I am running CPAchecker-2.0. I tried using the option -setprop cpa.predicate.invariants.export=true along with
> the -kInduction-kipdrInvariants config on the program eq2.c from the paper "Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art". It generates the file
> invariants.txt in the output directory, but all it contains is the following:
>
> loop__main__14:
> (set-info :source |printed by MathSAT|)
> (assert false)

The options with cpa.predicate belongs to the Predicate Analysis (corresponds more or less to https://www.sosy-lab.org/research/pub/2010-FMCAD.Predicate_Abstraction_with_Adjustable-Block_Encoding.pdf).
While that code is also used inside the k-induction analysis, it does most likely not output anything meaningful in case you run k-induction.
You can of course run the predicateAnalysis, in which case the option you found will indeed give you what you wanted:

$ scripts/cpa.sh -predicateAnalysis ~/src/sv-benchmarks/c/loop-invariants/eq2.c -spec config/specification/sv-comp-reachability.spc -setprop cpa.predicate.invariants.export=true
[...]
Verification result: TRUE. No property violation found by chosen configuration.
[...]
$ cat output/invariants.txt
loop__main__16:

(set-info :source |printed by MathSAT|)

(declare-fun |main::z| () (_ BitVec 32))
(declare-fun |main::y| () (_ BitVec 32))
(assert (let ((.def_73 (= |main::z| |main::y|))).def_73))

The most promising way to get invariants from k-induction is probably to look at the correctness witness.
For eq2.c, we can do the following:

scripts/cpa.sh -kInduction-kipdrdfInvariants ~/src/sv-benchmarks/c/loop-invariants/eq2.c -spec config/specification/sv-comp-reachability.spc -setprop cpa.arg.proofWitness=witness.graphml -setprop
cpa.arg.compressWitness=false

This will write a correctness witness (https://www.sosy-lab.org/research/pub/2016-FSE.Correctness_Witnesses_Exchanging_Verification_Results_between_Verifiers.pdf) to output/witness.graphml
upon successful verification. That one contains the (rather lengthy) invariant from the invariant generator that lead to the inductive proof.

>
> The invariant for that program is y == z, so I'm looking for some way for CPAchecker to output at least that (plus hopefully some of the candidate invariants, if any, that it generated along the way).

Output of candidate invariants is currently not implemented afaik. In case you need this it should not be too hard to add that feature though.

> The output I got above was similar for other programs I tried.
>
> I also tried the option cinvariants.export=true. That generated a file inv-eq2.c, but it was identical to the input program.

For me it contains some _VERIFIER_assume calls for temporary variables and variables that have constant values. When looking at output/Report.html,
I can observe that the constructed ARG seems to contains states of a value analysis. This means the ARG from which the invariants are taken is the one of the k-induction analysis itself,
not the invariant generation that runs in parallel (one could view this as a bug/room for improvement). For k-induction we run the invariant generator at the same time as we to incremental k-induction.
Usually the ARG from the invariant generation is the one we would want to take for invariant generation, but cinvariants.export takes the ARG from the analysis which finishes first,
which here is the wrong one. For the witness of k-induction we do not rely on the ARG of the analysis that finishes first, because the witness here is generated directly
as part of the statistics of the BMCAlgorithm (the class that implements the k-induction analysis). Sorry to bore you with these implementation details,
I write this down mainly for documentation, since I now already analyzed everything.

That happened for each different program I tried except for the
> loop-lit/afnp2014_true-unreach-call.c.i benchmark (from SV-COMP’15), which caused CPAchecker to crash with the exception "Exception in thread "main" java.lang.UnsupportedOperationException: Unexpected
> operand". (Here, I used the -kInduction-kipdrdfInvariants config with the option cpa.invariants.useMod2Template=true.) The generated file inv-afnp2014_true-unreach-call.c.i was different from the
> input program -- it contained some assume statements, but it was not a complete program (presumably due to the crash).

Nice, you found a bug! Unfortunately I cannot reproduce it, would you mind listing the exact command line/files that you used for the crash. Ideally you report the bug in our issue tracker:
https://gitlab.com/sosy-lab/software/cpachecker/-/issues

>
> Finally, I also tried the option cpa.predicate.invariants.dumpInvariantGenerationAutomata=true, but that didn't seem to do anything.

Yeah that feature seems to be a bit older, not sure what the original intention here was. Seems it was last touched 2016 and is not currently used in any visible config.

> Is there an option I missed, or perhaps some combination of options
> I need to enable to get CPAchecker to output the invariants that it generates? Any help is greatly appreciated.

Witnesses for k-induction and cpa.predicate.invariants.export for predicate analysis will probably give you the best results (the witnesses for predicate analysis currently may lose some invariants,
issues for this exist, but the solution is not easy, i.e., don't expect it to be resolved soon: https://gitlab.com/sosy-lab/software/cpachecker/-/issues/786
https://gitlab.com/sosy-lab/software/cpachecker/-/issues/606).

Best,

Martin
--
Martin Spießl
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F012 - Tel.: 089/2180-9185