warning: ignoring forall

[theyoucheng]

When __CPROVER_assume and __CPROVER_forall are used together, it may simply not work. Let us consider the following program, namely main.c.

#include <assert.h>
int main()
{
  unsigned x[5];

  __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==> x[i]>=1 });

 assert(x[0]>0);

 return 0; 
}

If we try to apply cbmcon it: cbmc main.c, we will get

warning: ignoring forall

and the assertion _fails_.

On the other hand, if we we replace assert(x[0]>0) with the trivial assertion assert(1), then, together with the VERIFICATION SUCCESSFUL, there will be _no warning_.

[martin-cs]

General observations:

1. The code in solvers/flattening/boolbv_quantifier.cpp is not used in the cases that work. It is out of date and broken.
2. The case that work, do so by a different means. forall in assertions is negated and then converted to an new variable. This is done before we get to anything in solvers/ . Consider:

int main (void) {
  int zero_array[10];

  __CPROVER_assert(__CPROVER_forall { int i; (i>=0 && i<10) ==> zero_array[i]==0 }, "quantifier");

  return 0;
}

The quantifier is alive and well in the goto-program.

cbmc --show-goto-functions ~/tmp/can-delete/quantifier-trace.c 
<snip>
main /* main */
        // 0 file /home/martin/tmp/can-delete/quantifier-trace.c line 2 function main
        signed int zero_array[10l];
        // 1 file /home/martin/tmp/can-delete/quantifier-trace.c line 4 function main
        ASSERT forall { signed int i; i >= 0 && i < 10 ==> zero_array[(signed long int)i] == 0 } // quantifier
        // 2 file /home/martin/tmp/can-delete/quantifier-trace.c line 6 function main
        main#return_value = 0;
        // 3 file /home/martin/tmp/can-delete/quantifier-trace.c line 6 function main
        dead zero_array;
        // 4 file /home/martin/tmp/can-delete/quantifier-trace.c line 7 function main
        END_FUNCTION

But has been converted by the time we've got to a decision procedure:

./cbmc/cbmc --show-vcc ~/tmp/can-delete/quantifier-trace.c 
<snip>
VERIFICATION CONDITIONS:

file /home/martin/tmp/can-delete/quantifier-trace.c line 4 function main
quantifier
<snip>
|--------------------------
{1} zero_array!0@1#1[(signed long int)i!0#1] == 0 || i!0#1 >= 10 || !(i!0#1 >= 0)

Note that simplify() does not handle quantifiers, so it isn't there. It's almost certainly somewhere in symex.

Update : it's goto_symext::rewrite_quantifiers; am stupid for not realising this earlier.

Youcheng, while we were chatting earlier you said you were interested in trying to fix this. I think the plan would be:

1. Rewrite solvers/flattening/boolbv_quantifier.cpp completely. It should do something like:

if (expr.id() == ID_exists) {
  //kind of what goto_symext::rewrite_quantifiers does
  create a free variable
  replace the quantified variable with it
  flatten as normal
} else {
  if (expr if of the form  "(const1 <= quantifier && quantifier <= const2) ==> thing") {
    instantiate for all values between const1 and const2 in the way post_process_quantifiers does
  } else {
    print "We only handle guarded quantifiers"
    die horribly
 }
}

The fiddly bit is how to recognise if it is a guarded quantifier as it will have been simplified()

1. Add support to the quantifier for ! forall -> exists ! and ! exists -> forall !.
2. Remove goto_symext::rewrite_quantifiers because that really shouldn't be done there.

Good luck!

[theyoucheng]

On Tue, 23 Aug 2016 11:37:46 -0700 Martin notifications@github.com wrote

General observations:

1. The code in solvers/flattening/boolbv_quantifier.cpp is not used in the
   cases that work. It is out of date and broken.
2. The case that work, do so by a different means. forall in assertions is
   negated and then converted to an new variable. This is done before we get to
   anything in solvers/ . Consider:

'''
int main (void) {
int zero_array[10];

__CPROVER_assert(__CPROVER_forall { int i; (i>=0 && i<10) ==>
zero_array[i]==0 }, "quantifier");

return 0;
}
'''

The quantifier is alive and well in the goto-program.

'''
cbmc --show-goto-functions ~/tmp/can-delete/quantifier-trace.c

main /* main */
// 0 file /home/martin/tmp/can-delete/quantifier-trace.c line 2
function main signed int zero_array[10l];
// 1 file /home/martin/tmp/can-delete/quantifier-trace.c line 4
function main ASSERT forall { signed int i; i >= 0 && i < 10 ==>
zero_array[(signed long int)i] == 0 } // quantifier // 2 file
/home/martin/tmp/can-delete/quantifier-trace.c line 6 function main
main#return_value = 0;
// 3 file /home/martin/tmp/can-delete/quantifier-trace.c line 6
function main dead zero_array;
// 4 file /home/martin/tmp/can-delete/quantifier-trace.c line 7
function main END_FUNCTION
'''

But has been converted by the time we've got to a decision procedure:

'''
./cbmc/cbmc --show-vcc ~/tmp/can-delete/quantifier-trace.c

VERIFICATION CONDITIONS:

file /home/martin/tmp/can-delete/quantifier-trace.c line 4 function main
quantifier

{1} zero_array!0@1#1[(signed long int)i!0#1] == 0

= 0) '''

Note that simplify() does not handle quantifiers, so it isn't there. It's
almost certainly somewhere in symex.

Update : it's goto_symext::rewrite_quantifiers; am stupid for not realising
this earlier.

Youcheng, while we were chatting earlier you said you were interested in
trying to fix this. I think the plan would be:

1. Rewrite solvers/flattening/boolbv_quantifier.cpp completely. It should
   do something like:

'''
if (expr.id() == ID_exists) {
//kind of what goto_symext::rewrite_quantifiers does
create a free variable
replace the quantified variable with it
flatten as normal
} else {
if (expr if of the form "(const1 <= quantifier && quantifier <= const2)
==> thing") { instantiate for all values between const1 and const2 in the
way post_process_quantifiers does } else {
print "We only handle guarded quantifiers"
die horribly
}
}
'''

Let us still consider the example C program, by replacing __CPROVER_assert
with __CPROVER_assume. Now I reach something like

i!0#1 >= 10 || zero_array!0@1#1[(signed long int)i!0#1] == 0 || !(i!0#1 >= 0)

Suppose that I can get the upper/lower bounds (i.e., 0 and 10). Now what I plan
is to 
(1) create (or obtain) the variable for each element in the array zero_array
(2) construct the assumption "zero_array[0]==0 && ... && zero_array[9]==0"

Well, I am not sure how to solve the (1) point... any suggestion?

Best,
Youcheng


> 
> The fiddly bit is how to recognise if it is a guarded quantifier as it will
> have been simplified() 
>
> 2. Add support to the quantifier for ! forall -> exists !  and ! exists ->
> forall !. 
>
> 3. Remove goto_symext::rewrite_quantifiers because that really shouldn't be
> done there. 
>
> Good luck!
> 
> 
> -- 
> You are receiving this because you authored the thread.
> Reply to this email directly or view it on GitHub:
> https://github.com/diffblue/cbmc/issues/203#issuecomment-241832097


Youcheng Sun
Research Assistant
Department of Computer Science
University of Oxford
Wolfson Building, Parks Road
Oxford OX1 3QD
https://sites.google.com/site/theyoucheng/

[martin-cs]

On Thu, 2016-08-25 at 04:01 -0700, Youcheng Sun wrote:

On Tue, 23 Aug 2016 11:37:46 -0700 Martin notifications@github.com wrote

Youcheng, while we were chatting earlier you said you were interested in
trying to fix this. I think the plan would be:

1. Rewrite solvers/flattening/boolbv_quantifier.cpp completely. It should
   do something like:

'''
if (expr.id() == ID_exists) {
//kind of what goto_symext::rewrite_quantifiers does
create a free variable
replace the quantified variable with it
flatten as normal
} else {
if (expr if of the form "(const1 <= quantifier && quantifier <= const2)
==> thing") { instantiate for all values between const1 and const2 in the
way post_process_quantifiers does } else {
print "We only handle guarded quantifiers"
die horribly
}
}
'''

Let us still consider the example C program, by replacing __CPROVER_assert
with __CPROVER_assume. Now I reach something like

i!0#1 >= 10 || zero_array!0@1#1[(signed long int)i!0#1] == 0 || !(i!0#1 >= 0)

Suppose that I can get the upper/lower bounds (i.e., 0 and 10).

Yes; really we need a unification algorithm to do this here but for now
a simple recognition will do.

Now what I plan
is to
(1) create (or obtain) the variable for each element in the array zero_array
(2) construct the assumption "zero_array[0]==0 && ... && zero_array[9]==0"

Well, I am not sure how to solve the (1) point... any suggestion?

Look at post_process_quantifiers, lines 78--99. In psuedo-code:

for ( inst = the instantiations 0 ... 10 ) {
instantiation = replace_expr(quantified_variable, inst, body)
}

and instantiations together

HTH

Cheers,

• Martin

[polgreen]

Could anyone give me an update on this? I am managing to create verification cases where the quantifiers are ignored and the verification spuriously passes, but I'm not sure if that is down to the way I'm building my exprt's, or something related to this issue.

[martin-cs]

As far as I know, little has changed. Michael wrote 38fd81a at the start of the year which should tidy things a bit but the architecture remains the same. The native CPROVER back-end can only solve existential problems. Have you tried with any of the SMT back-ends? Are you are still getting the warning: ignoring forall message? On older versions this did indicate that you would it probably generate incorrect results.

For me this is a kind of won't fix issue. If we want to be able to handle quantifiers in a meaningful way then we will need MBQI, CEGQI, FMF, etc. as a base-line. We are probably ... 5-7 years behind the state-of-the-art here (CVC4 / Andy's work) and I'm not (at the moment, I am very open to being convinced I am wrong) seeing the use-case that is worth that much effort when we could just use one of the SMT solvers that already has it. I suggested this as an approach to handling strings but the string solver went a different way.

[SaswatPadhi]

Just wanted to ping here and revive this issue.

In our on-going work on function and loop contracts, we find the need to be able to assume universally quantified expressions in many cases (e.g. functions/loops that deal with arrays). Hopefully with the new thrust on switching the backend to SMT, we would have be able to handle these cases properly now? 🤞 Just wanted to bump this issue and put it on your radar. CVC4 uses CEGQI and usually does well with quantifiers.

[SaswatPadhi]

With the SMT backend, so far I haven't encountered any unsoundness related to this, but there is an issue with counterexample extraction: #5970.

For the SAT backend, may I suggest rejecting the program (i.e. throw an error) instead of just showing a warning (which can be easily overlooked) and unsound verification results?

[martin-cs]

I would support throwing an error but late in the process (i.e. in solver). As described above there are cases where we can convert forall into exists and we should probably support that. Limited, static instantiation of loops would be nice but passed that we should probably just throw an error.