A bug with --constant-propagator and --dump-c

[rladydpf1]

CBMC version: 5.43.0
Operating system: Ubuntu 20.04.4 LTS
Exact command line resulting in the issue:

goto-cc test.c -o test
goto-instrument test --constant-propagator test
goto-instrument test --dump-c test1.c

What happened instead:
test.c :

#include <assert.h>
int ab, bc;
int f(int x) {
    ab = 1 + 1 + 1 + 1;
    bc = ab + x;
    return ab + bc;
}
int main() {
    int a;
    a = -4;
    int b;
    b = nondet();
    a = f(a);
    assert(!(0 <= a && a < 5 && 0 <= b && b < 5));
}

and test1.c:

#include <assert.h>

// f
// file test.c line 5
signed int f(signed int x);
// nondet
// file test.c line 15 function main
signed int nondet(void);

// ab
// file test.c line 3
signed int ab;
// bc
// file test.c line 3
signed int bc;

// f
// file test.c line 5
signed int f(signed int x)
{
  ab = 4;
  bc = 0;
  return ab + bc;
}

// main
// file test.c line 11
signed int main()
{
  signed int a=-4;
  signed int b=nondet();
  a=f(-4);
  /* assertion !(0 <= a && a < 5 && 0 <= b && b < 5) */
  assert(1);
}

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

goto-cc sv-benchmarks/c/recursive-simple/fibo_25-1.c -o fibo
goto-instrument fibo --constant-propagator fibo
goto-instrument fibo --dump-c fibo.c

the fibo.c:

#include <assert.h>
#include <stdlib.h>

// fibo
// file data/cbmc/sv-benchmarks/c/recursive-simple/fibo_25-1.c line 7
signed int fibo(signed int n);
// reach_error
// file data/cbmc/sv-benchmarks/c/recursive-simple/fibo_25-1.c line 4
void reach_error();

// fibo
// file data/cbmc/sv-benchmarks/c/recursive-simple/fibo_25-1.c line 7
signed int fibo(signed int n)
{
  goto __CPROVER_DUMP_L1;
  return 0;

__CPROVER_DUMP_L1:
  ;
  goto __CPROVER_DUMP_L2;
  return 1;

__CPROVER_DUMP_L2:
  ;
  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();
    abort();
  }

  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);
}

"signed int return_value_fibo=fibo(24);" : In this case, you shouldn't have propagate the constant.

[tautschnig]

My hunch is that we’re missing return-value removal before doing constant propagation.

[martin-cs]

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.

[rladydpf1]

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);
}

[martin-cs]

@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.

[jimgrundy]

Isn't this a soundness issue? (Adding soundness label).

[jimgrundy]

Confirmed that this is an issue in the current version 5.63

[martin-cs]

@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?

[thomasspriggs]

I have raised this PR to handle the initial issue with remove returns - #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?

[martin-cs]

@thomasspriggs Yes. This is why I suggested using goto-analyzer specifically with --vsd --vsd-value constants which should be (fixable to be) sound.

[thomasspriggs]

@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 -

1. Is there a reason why we shouldn't add a deprecation / unsoundness warning to goto-instrument --constant-propagator today if there is a plan to replace it?
2. Would it be reasonable to (temporarily) add a filter to these passes with recursion issues such that functions which are part of recursive call chains are not updated in order to make this sound? Or would that in itself be unsound or likely to be more involved than just fixing the issue with recursion?

[martin-cs]

My apologies for not being clearer!

1. TBH I have two half-completed PRs which will simply remove it and give a warning with the new suggested command-line.
2. The recursion issue is A Pain. As it can affect the values that are returned from / modified by recursive functions it is not clear that workarounds will be less work than fixing it.

[jimgrundy]

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.

[thomasspriggs]

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.

[martin-cs]

#7120 also resolves this problem by removing the functionality completely.

[martin-cs]

@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]

@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.

[martin-cs]

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.

[jimgrundy]

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.

[thomasspriggs]

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.