Open rladydpf1 opened 2 years ago
My hunch is that we’re missing return-value removal before doing constant propagation.
Strong suggestion @tautschnig , I would not be at all surprised if that is the case.
@rladydpf1 please could you try two options, each instead of using goto-instrument --constant-propagator
:
A. goto-analyzer test --simplify test1 --constants
B. goto-analyzer test --simplify test1 --vsd --vsd-value constants
I am pretty sure they handle return-value removal correctly so if A works, it was that. If A fails but B works then it is a problem with the constants domain.
goto-analyzer test --simplify test1 --constants
goto-instrument test1 --dump-c test1.c
It does work, test1.c : (Case A)
signed int f(signed int x)
{
ab = 4;
bc = 0;
return 4;
}
signed int main()
{
signed int a=-4;
signed int b;
nondet();
b = nondet_signed_int();
f(-4);
a = 4;
/* assertion !(0 <= a && a < 5 && 0 <= b && b < 5) */
assert(!(b >= 0) || b >= 5);
}
however, fibo_25-1.c has stll the same error.
goto-cc sv-benchmarks/c/recursive-simple/fibo_25-1.c fibo
goto-analyzer test --simplify fibo --constants
goto-instrument fibo --dump-c fibo.c
fibo.c : (Case A)
signed int fibo(signed int n)
{
signed int return_value_fibo=fibo(24);
signed int return_value_fibo$0=fibo(n + -2);
return return_value_fibo + return_value_fibo$0;
}
// main
// file data/cbmc/sv-benchmarks/c/recursive-simple/fibo_25-1.c line 25
signed int main(void)
{
signed int x=25;
signed int result;
signed int return_value_fibo=fibo(25);
result = return_value_fibo;
if(result == 75025)
{
ERROR:
;
reach_error();
__CPROVER_assume(0);
}
return 0;
}
// reach_error
// file data/cbmc/sv-benchmarks/c/recursive-simple/fibo_25-1.c line 4
void reach_error()
{
/* assertion 0 */
assert(0);
}
The case B does work:
goto-cc sv-benchmarks/c/recursive-simple/fibo_25-1.c fibo
goto-analyzer fibo --simplify fibo --vsd --vsd-values constants
goto-instrument fibo --dump-c fibo.c
fibo.c : (Case B)
signed int fibo(signed int n)
{
if(!(n >= 1))
return 0;
else
if(n == 1)
return 1;
else
{
signed int return_value_fibo=fibo(n - 1);
signed int return_value_fibo$0=fibo(n - 2);
return return_value_fibo + return_value_fibo$0;
}
}
// main
// file data/cbmc/sv-benchmarks/c/recursive-simple/fibo_25-1.c line 25
signed int main(void)
{
signed int x=25;
signed int result;
signed int return_value_fibo=fibo(25);
result = return_value_fibo;
if(result == 75025)
{
ERROR:
;
reach_error();
__CPROVER_assume(0);
}
return 0;
}
// reach_error
// file data/cbmc/sv-benchmarks/c/recursive-simple/fibo_25-1.c line 4
void reach_error()
{
/* assertion 0 */
assert(0);
}
@rladydpf1 thanks for testing this out. If A works but goto-instrument
doesn't then it is probably an issues like @tautschnig suggests. I have an in-progress patch set that deprecates the functionality in goto-instrument
in favour of goto-analyze
. Would using A or (probably better) B work for you?
As regards the recursive example, there is a bug in how our abstract interpreter handles recursive programs. We are working on a fix. If you have urgent use-cases then it would be good to know as it would increase the priority.
Isn't this a soundness issue? (Adding soundness label).
Confirmed that this is an issue in the current version 5.63
@jimgrundy It is certainly a "this can trash your program and give you wrong results" bugs.
@rladydpf1 does the workaround work for you? How urgent are the recursive examples?
I have raised this PR to handle the initial issue with remove returns - https://github.com/diffblue/cbmc/pull/7105
However I notice the doxygen for this particular constant propagator describes it as "A simple, unsound constant propagator." - https://github.com/diffblue/cbmc/blob/develop/src/analyses/constant_propagator.h#L12 Is this an indication that this constant propagator should not be used if "soundness" is of concern, even after the bug with recursion is addressed?
@thomasspriggs Yes. This is why I suggested using goto-analyzer
specifically with --vsd --vsd-value constants
which should be (fixable to be) sound.
@thomasspriggs Yes. This is why I suggested using
goto-analyzer
specifically with--vsd --vsd-value constants
which should be (fixable to be) sound.
Ah! Thank you for the explanation. I hadn't previously understood that your suggested alternate command line was using entirely separate code to do the constant propagation. I have a couple of further followup questions -
goto-instrument --constant-propagator
today if there is a plan to replace it?My apologies for not being clearer!
Can we at least drive this as far as giving people a stern warning (and perhaps the recommendation of what to do instead). Then we could drop the "soundness" tag as our users were appropriately warned.
I have raised a PR solely to add the warning. I haven't included information in the warning about alternatives because (A) Symex already performs its own constant propagation by default and (B) Martin's suggestion of using goto-analyzer test --simplify test1 --vsd --vsd-value constants
also needs fixing for the recursive case.
@thomasspriggs please forgive me if I am telling you things you already know but both the constant propagation and --vsd --vsd-value constants
will be broken in some recursive cases because the issue is in common code. VSD should be strictly less broken than the constant propagator.
@thomasspriggs please forgive me if I am telling you things you already know but both the constant propagation and
--vsd --vsd-value constants
will be broken in some recursive cases because the issue is in common code. VSD should be strictly less broken than the constant propagator.
That was also my understanding. I am happy to have confirmation that our understandings match.
I have yet to work on the variable sensitivity domain code (or the abstract interpreter). However I am interested in learning, so that I can help maintain it, given that it is merged into the CBMC repository. My intuition is that back edges of loops and recursive functions calls will represent similar challenges, but that one may work while the other does not due to implementation differences.
AI/VSD : I will be doing an onboarding session soon-ish for one of our new recruits, will be in person but have an online "you are welcome to join in", drop me an e-mail if you want to be on the invite list.
Loops/Recursion : yes, at some formal level a loop is just a degenerate case of a recursive function, so, yes they are conceptually the same problem. However at the level that the abstract interpreter is working the differences in how they work and things like "how many back-edges do they have" and "how hard is it to recognise a back edge" matter. The recursion bug is a problem with the algorithm we have and that it can handle (probably most) loops but isn't quite complete in the case of recursion. I have been through all of the obvious fixes. They are all either incomplete or very costly. We fundamentally have to change how the abstractions are computed. I think I know how but it is a non-trivial amount of work, esp. to do in a backwards compatabile (w.r.t. to performance and accuracy) way.
If you have room for more folks to join in do let us know and maybe some folks might travel from further afield to join.
Can we at least drive this as far as giving people a stern warning (and perhaps the recommendation of what to do instead). Then we could drop the "soundness" tag as our users were appropriately warned.
@jimgrundy The PR adding the soundness warning is now merged.
CBMC version: 5.43.0 Operating system: Ubuntu 20.04.4 LTS Exact command line resulting in the issue:
What happened instead: test.c :
and test1.c:
The "assert(1);" is invalid.
and another bug case with a recursive function: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/recursive-simple/fibo_25-1.c
the fibo.c:
"signed int return_value_fibo=fibo(24);" : In this case, you shouldn't have propagate the constant.