Open theyoucheng opened 8 years ago
General observations:
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:
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()
Good luck!
On Tue, 23 Aug 2016 11:37:46 -0700 Martin notifications@github.com wrote
General observations:
- The code in solvers/flattening/boolbv_quantifier.cpp is not used in the cases that work. It is out of date and broken.
- 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 || 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 } } '''
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/
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,
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.
As far as I know, little has changed. Michael wrote 38fd81ac26a62e48e4f74c8580297404a88ad4fc 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.
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.
With the SMT backend, so far I haven't encountered any unsoundness related to this, but there is an issue with counterexample extraction: https://github.com/diffblue/cbmc/issues/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?
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.
When
__CPROVER_assume
and__CPROVER_forall
are used together, it may simply not work. Let us consider the following program, namelymain.c
.If we try to apply
cbmc
on it:cbmc main.c
, we will getand the assertion _fails_.
On the other hand, if we we replace
assert(x[0]>0)
with the trivial assertionassert(1)
, then, together with the VERIFICATION SUCCESSFUL, there will be _no warning_.