Type cast fails with cpa.predicate.encodeFloatAs=RATIONAL.

[ryanw...@gmail.com]

Hi CPAChecker developers,

Our research group is using CPAChecker for program verification, and uses -predicateAnalysis along with -setprop cpa.predicate.encodeFloatAs=RATIONAL to encode floats as reals (otherwise it will run forever to verify our programs).

However, we noticed that type casts are handled very imprecisely, if you look at the following example:

extern void __VERIFIER_assume(int);

extern void __assert_fail();

#define __VERIFIER_assert(cond) { if(!(cond)) { __assert_fail(); } }

    

int test( )

{

    int i = 3;

    float j = (float)i;

    __VERIFIER_assert (j == 3.0);

}

It will report a counterexample stating that `i=3, j=0` if we use ` -predicateAnalysis -setprop cpa.predicate.encodeFloatAs=RATIONAL`.

Are there other ways to get around this issue instead of using the bit-precise version? We're using the released cpachecker v1.8. Any suggestions are greatly appreciated, thanks!

Ryan

[Philipp Wendler]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Dear Ryan,

Am 28.03.19 um 22:20 schrieb ryanw...@gmail.com:

> Our research group is using CPAChecker for program verification,
> and uses -predicateAnalysis along with -setprop
> cpa.predicate.encodeFloatAs=RATIONAL to encode floats as reals
> (otherwise it will run forever to verify our programs).
>
> However, we noticed that type casts are handled very imprecisely,
> if you look at the following example:

Indeed. Type conversions are mostly implemented for float<->bv and
only in a few other cases, because float<->bv is what is used most.
There are more cases that could be implemented, but it would need some
work. I filed an issue here:
https://github.com/sosy-lab/java-smt/issues/152

For now, you might have more success in approximating bitvectors with
integers if you approximate floats with rationals, because the
int->rational conversion is easier.
I added support for this case just now in revision 30894.

Greetings, Philipp
- --
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEGdWhCy2XiNh8vuXtYsD3jDGp3owFAlyd7OgACgkQYsD3jDGp
3oz0rQ/7BNBfvUbL8dZl2NJBIXOp0a3huzgIvfCdiCNXmg2EOvGbU5DLmjJ5c0uS
0/tJJNrDEs79YslrDazoJ0FsVd/WTeSVl+4SvBnCJRu93qPqd5PqQiSeuFmxhjz8
aDEmAt1Pdsn8CPB9/WIGFUPCYAPRafvhSpmYlIYNd8IlZeJfvrccnVIyej+XkpiS
+cGAXbc+M5pna1/CLBsN6O5sGtVix2jOhDNdTD2TqzjiStOKpMbcbU66DcEre1xt
v03rvkDPjjR+XZcuASq5QgsmLpyq//fFJKCpF/e8ZNDr42sWHSar0X7A09N5aZjy
PqeP6Db2hHQWMhDtl4iXVkTBRDUPaSMq1QsfjsYI10tP2e18tyJ5/dalmyv0YqpD
febBTxc61ssqlKXq8ImX59MVPf6mAZgsAG7M3fBUCgML8KdNETAo+gqPZGj+jHg8
TwDSva0xC/aXsTw8hxeBZEs/1+j1AAA/rQ11JbwfOW7mOWIfYT0yjMxkwBGXoU3o
xoYWPY39Z6yXyLdPnLXMRDQkb+hUonQnzX4ro6OfSA/QLGwx0NC8DNad91UBQa1l
sbJE/CKVa5+k1DK0oQqJcyGagFcIdGpabgWxK0UEDfQt86Ais7sFtrW7EKI3h3BC
CIA7u+5s0/UQUqPrwDimC5p841n/n/x8DhZd/5jiF2GJp6yyQyY=
=QMsq
-----END PGP SIGNATURE-----

[ryanw...@gmail.com]

Hi Phillipp,

Thanks for the reply, I can confirm that the latest cpachecker fixes this issue.

Can you help me on another simple example? I failed to verify this simple program:

extern void __VERIFIER_error() __attribute__ ((__noreturn__));

extern int __VERIFIER_nondet_float(void);

extern int __VERIFIER_nondet_int();

extern void __VERIFIER_assume(int);

extern void __assert_fail();

#define __VERIFIER_assert(cond) { if(!(cond)) { __assert_fail(); } }

    

int test(int total, float value)

{

  __VERIFIER_assume(value > 0);

  __VERIFIER_assume(total > 0);

  float sum = 0;

  int count = 0;

  while (count < total)

  {

    sum = sum + value;

    count = count + 1;

  }

  __VERIFIER_assert(sum <= total * value);

}

The argument I'm using is 

-predicateAnalysis -preprocess test.c -setprop solver.nonLinearArithmetic=USE -setprop cpa.predicate.encodeFloatAs=RATIONAL -setprop cpa.predicate.encodeBitvectorAs=INTEGER -setprop solver.solver=MATHSAT5

However, MATHSAT5 returns 'cannot build ie-local' and z3 returns 'smt tactic failed'. Similar error message shows up  if I drop the approximation arguments. 

Do you know the correct configuration I should use to verify this simple-loop program? I tried bounding the `value` variable but cannot succeed either.

Thanks,

Ryan

[Philipp Wendler]

Dear Ryan,

Am 10.04.19 um 21:14 schrieb ryanw...@gmail.com:

The problem is that this program needs non-linear arithmetic to be
proven. The error message you get from Z3 means that it just gave up
because of this.

MathSAT seems to suffer from incomplete interpolation here.

There are two things to try here:
1. Use an approach that does not rely on interpolation. You can specify
-kInduction instead of -predicateAnalysis to see how that works (the
remaining arguments can stay the same, and you can also try both solvers).

2. Provide predicates to the verifier such that interpolation is not
necessary to find the loop invariant. I attached a file with predicates
that should be sufficient, add
-setprop cpa.predicate.abstraction.initialPredicates=predmap.txt
to the command line (with the original -predicateAnalysis).
Z3 still gives up, but the MathSAT interpolation problem goes away.

I tried running the remaining three variants for a short time,
and while they were not able to produce a result in this time,
they also did not fail.
So you can try whether they produce a result if given more time.


Note that I guess that the assertion in your program actually does not
hold, if you use the proper float semantics instead of rational
approximation. The rounding errors could probably add up in the loop and
make sum larger than total * value.
So if you remove cpa.predicate.encodeFloatAs=RATIONAL you might find a
counterexample.

Greetings, Philipp

[ryanw...@gmail.com]

Hi Phillipp,

Thanks for the suggestions, however kInduction and predicateAnalysis with the predmap.txt you provided doesn't finish with several hours.

Is there a way to provide stronger hints to cpachecker so that this can be verified? in your predmap.txt I see the loop invariant is provided but it does not include the assumptions (value > 0 and total > 0). 

What else do you suggest I write in predmap.txt?

Thanks for your time!

-Ryan

[ryanw...@gmail.com]

Hi Phillipp,

It turns out we need `count <= total` as a loop invariant as well, adding that into the predmap.txt makes cpachecker with z3 verify.

Now with this technique I'm considering a new program:

extern void __VERIFIER_error() __attribute__ ((__noreturn__));

extern int __VERIFIER_nondet_float(void);

extern int __VERIFIER_nondet_int();

extern void __VERIFIER_assume(int);

extern void __assert_fail();

#define __VERIFIER_assert(cond) { if(!(cond)) { __assert_fail(); } }

    

int test(int NN, float epsilon)

{

  __VERIFIER_assume(epsilon > 0);

  __VERIFIER_assume(NN > 0);

  float cost = 0;

  int count = 0;

  while (count < NN)

  {

    cost = cost + epsilon * (0.5 / NN);

    count = count + 1;

  }

  __VERIFIER_assert(cost <= 0.5 * epsilon);

}

And I've attached the premap.txt I'm using but z3 gives up. I believe the loop invariants are sufficient to prove because I used the same invariants on Dafny (which I believe uses z3 as backend) and it verifies this program.

I've read some posts about non-linear arithmetic about z3 (https://stackoverflow.com/questions/13898175/how-does-z3-handle-non-linear-integer-arithmetic). It turns out using different tactics might solve the problem, but I cannot find configurations of cpachecker to use different tactics, do you know the correct way to specify the tactics for cpachecker?

Any suggestions are appreciated!

-Ryan

[Philipp Wendler]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Hi Ryan,

Am 14.04.19 um 22:59 schrieb ryanw...@gmail.com:

> It turns out we need `count <= total` as a loop invariant as well,
> adding that into the predmap.txt makes cpachecker with z3 verify.

Nice to hear.

CPAchecker just calls "checks-sat on the SMT solver through a
solver-independent API. AFAIK there is currently no way to specify
tactics.

Is MathSAT able to solve this case?

Greetings,
Philipp
- --

Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181

-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEGdWhCy2XiNh8vuXtYsD3jDGp3owFAly0DckACgkQYsD3jDGp
3oyBEg//eYt/H0vR4Q3U5ugwHbSGXZXm6RfNJxszuUm5QPm+Y+ewN0hcLKgvXq33
nDyhheRsAjrkiV2zeAoMeaCccGwJ5FmiLYRygRWiv8k07Mvgh7FE1+ErOIlN9THT
YWHbBDdYsa1kCdYA0QIzoD4vR+0VFNygZT8CTFZ3qCuAfdQc2VKaMQqzP3heQXwh
Ib1LpqKNE4y6EB9BNBQd54LVUTCwPkgATIPA2Bmz2+aZgV0+z+pColTgvh5meGw2
hIslnSx/1tSHKTwy6D+6WvayaVAigIc6hkqLNM6F3l1n0W3y6gwfT2AEcWe1Z8sx
vkz2blTBHoXRz4NRoHyDg3PRx7yLeqoreE7RCcW/e/zS011Gb6v3T9yPh/PbsIkK
xWFY5BIsZoGaGbQA7G+r+hI11zWOPaWyKwPrzNy5F8Qa0MfmdzFiVUCy7V+PecRC
eEXHwbohRUorrYrl0Z+XUwpcuPjJBoi4c8MRwx9SwwlGbbiVr4Wq/Nae4tDwFN1K
LJY1JVmAJ/xtVa5ARCMyaCI8O2fo3fQCKmQUl9BjpBtpFMnAyYJ66Rbdvq/sD8yj
bYBDPkiEwfEBPWk33uzk4US4ITwHZ18vr4Z1e7aKI0mtKOBau2iiTwPzy+y6wYum
29Ee9ipdoR3K+Ryi5hY8DlLeydTArrQ09VuU34SLxC48WGqhabo=
=f3jC
-----END PGP SIGNATURE-----

[ryanw...@gmail.com]

Hi Phillipp,

Unfortunately Mathsat runs forever in this case. 

Never mind, I found out I still need `cost >= 0` as a loop invariant, not sure why Dafny doesn't require such, though.

Do you have any plans for implementing tactic selections? I think this is implemented in java-smt (according to https://github.com/sosy-lab/java-smt/issues/3), I have a feeling that z3 could be much more powerful with different tactics (I've never had success with cpachecker w/ z3 for my verification tasks). 

Thanks!

-Ryan

[Philipp Wendler]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Dear Ryan,

Am 15.04.19 um 16:24 schrieb ryanw...@gmail.com:

> Never mind, I found out I still need `cost >= 0` as a loop
> invariant, not sure why Dafny doesn't require such, though.

Dafny automatically guesses some (parts of) loop invariants based on
heuristics like this case.
CPAchecker has this too, but the heuristics are much weaker because
typically the SMT solver can find them via interpolation.

> Do you have any plans for implementing tactic selections? I think
> this is implemented in java-smt (according to
> https://github.com/sosy-lab/java-smt/issues/3), I have a feeling
> that z3 could be much more powerful with different tactics (I've
> never had success with cpachecker w/ z3 for my verification tasks).
>

JavaSMT just offers tactics for quantifier elimination and some
formula rewritings, I don't think they are useful here.

But in general, the problem is not the API, but when should we use
which tactic?

Consider the common case, where we just have a formula that needs to
be solved: Which tactic should CPAchecker apply before solving?

Greetings

Philipp
- --
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEGdWhCy2XiNh8vuXtYsD3jDGp3owFAly0pBAACgkQYsD3jDGp
3owQyw//azTaSubh/SYrtM5TlF/5z6fmyKZ/SsNzE8bXY9mWXEYaQIQ383LBZAfF
EWcrxkLnm7FWlc+PKlDU6G3/Rb/0rLlqtII/xA1yOBWE9n7mRt4eDWV5SVLmP9Fw
qbBtUtkIj/oasxUYt2bjXfxn2xNuqSBzEQE5PN3YyvEq7DkUJfZ5+PjFppIsvQ0M
iJlJpFnzNU+KVCbNijrb1/qpEUiyYxqPYBBAF2EV7N4HxNOVhQA9LMCJq29CJxo+
8WexoaPuAZiYQBjBClWrfyVRFezqwUN4pHmCGSP+Kj5Yc5ThfYiDUAzsKCzTUjj1
uhugXZlvPfoa3ENWfViJUapd3WU9YT4DYmoomEDxaYXXatAycjNLSQD7M07t99fe
MkGPHjz+Dg8M9WnQu7+oWWMr+RstDm401SpG9rHWgXXi0jrKYtTHQxYqOPlu33UV
M58+0J9FChGYwBWYNyVZcXPoy9+ercHiYWqHHn15URj6nW51SdFDKWqKDiqMZcu8
fyomEx1XHBDHxcHJh2afUcfts5fqNQcqFG042KCrJEhR6s8yCXyiiSDJnI0/FqHK
HSJUjHIMN5gwH9tWuhSGBtyC++trt322zBM7MvkxjFpQ7rRM2EtnH7UbVLzlNSvB
VBZ80G12orBNxw04LdylsYbuPnyl40Uypt+M/Bls/+P+EAWn95w=
=2xEL
-----END PGP SIGNATURE-----

[ryanw...@gmail.com]

Hi Phillipp,

Thanks for the explanations!

I see your concern. Can we hand over the selection to the end-user? like adding an configuration option, if none is given, we use the default otherwise we invoke  (check-sat-using ...).

-Ryan

[Philipp Wendler]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Dear Ryan,

Am 15.04.19 um 18:05 schrieb ryanw...@gmail.com:

>
> I see your concern. Can we hand over the selection to the end-user?
> like adding an configuration option, if none is given, we use the
> default otherwise we invoke (check-sat-using ...).

Ah, now I understand better.
I was confused about Z3 tactics and the reference to
https://github.com/sosy-lab/java-smt/issues/3, which is about using
tactics for formula rewriting.

I did not know that Z3 also has tactics for solving, which of course
makes much more sense.
So I added https://github.com/sosy-lab/java-smt/issues/154 as a
feature request for JavaSMT, feel free to add any information there or
correct me if I got something wrong.

Once this is implemented, we can immediately use it in CPAchecker,
that will be trivial.

Greetings
Philipp

- --
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEGdWhCy2XiNh8vuXtYsD3jDGp3owFAly1lLAACgkQYsD3jDGp
3owMZhAA0v+wZK+lTWZn7s+xXOxzFkxrtKvVwE+bI8KCMbQHvp0WVHnq1bwSQCEy
UEccW0WQEDBk7KiQWogWQ6BUOaETdQmDbOGxby8CTSPD6ZniZ97G6OCl7NHm8tzs
vAdAkT8+/E1hQrqsRmoLlbcwrNwijJFlA3QxBIHM0iU7YWG79vfqVBVesB6eKujq
QG8QTUrSUYG1cgAB2QQu32YA0N4JrZ30rxybzF9ihsoF32JS66kR/8j/cZhLkUau
TYbbVp05UyBCkxBCRlqaXHLQHbIlcKJwVJQI2xMlIhxMmq0IHQ11qh/g4Qh/yE24
3fNKQiSs8LAIUbo7t4bcn2nUjht0Z6ykyrgfUTuAumxU2OR4eJ6oDnDjijBh2hUF
t84nGvKqw5HuBTQIUrSt1LsIJDcix6Eqd820pBMsHgby53Y1Cc9GWc30m6jKT+0o
kqf2m2uqL3cG+Q1Gjyc5sefxx1XxYBIayaOUuy9zBspbcTGAil+cGylyerI2PKJ1
Akqk1ncRm/5QiulpPqt+cI8wYmD4SBxRyEO4MKqO0h1h2tlX6ROrBqmeJvswWbYg
oGlKjJojuzmoCc0epiOmKrqpOJsf2ozNhQ69bWrzLg82GSwpUXqe+65UDg2hD2NV
8pX17BQD9N8HSqiL1g1pqfOJes5HHhHAHMoa4meFLyrDLQOkays=
=Ln89
-----END PGP SIGNATURE-----

[Yuxin (Ryan) Wang]

Hi Phillipp,

Sorry for the confusion, I’m new to this field. Great to know that this is now being considered! Would love to try out this feature! Thanks!

-Ryan

--
You received this message because you are subscribed to the Google Groups "CPAchecker Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cpachecker-use...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--

Best,
Yuxin