Interval Analysis not working correctly in goto-analyzer

[thk123]

The intervals analysis of goto-analyze doesn't work for regressions: intervals2 and intervals4. Both of these use && in an assertion that should be knowable.

[lucasccordeiro]

@kroening: These two test cases pass with the code in https://github.com/lucasccordeiro/cbmc/tree/aisimplifier. A very long time ago, I had a PR related to the implementation of the abstract interpretation simplifier (#173).

I can check the difference between my branch and CBMC master to identify the piece of code that fixes the bug related to intervals2 and intervals4. However, I think @martin-cs and @danpoe have further extended and improved the code in https://github.com/lucasccordeiro/cbmc/tree/aisimplifier.

How should we proceed in this case? I'm happy to fix this bug, but I would like just to make sure that it does not overlap with the work from @martin-cs and @danpoe.

[martin-cs]

Short version : the situation is under control.

When I first created the branch that became:

https://github.com/martin-cs/cbmc/tree/goto-analyzer-4

I started from @lucasccordeiro fixes and reworked them. Due to needing to sleep occasionally I handed this over to @danpoe and I believe the code is now:

https://github.com/danpoe/cbmc/tree/goto-analyzer

which is now part of the toyota release and will (hopefully) (soon) be merged into trunk.

[hannes-steffenhagen-diffblue]

The interval domain shows some rather odd behaviour overall, consider this:

#include <assert.h>

int main(void)
{
  int some_condition;
  int ten = 10;
  assert(ten <= 10 && ten >= 10);
  assert(ten == 10);
  float y = 10.0f;
  assert(y <= 10.0f && y >= 10.0f);
  assert(y == 10.0f);
  float x;
  if(some_condition)
  {
    x = 1.0f;
    // x = 2.0f
  }
  else
  {
    x = 2.0f;
    // x = 2.5f
  }
  // 2.0f <= x <= 2.5f
  assert(x < 3.0f); // also true
  assert(x <= 3.0f);
}

Running this against goto-analyzer --verify --intervals gives us this output:

GOTO-ANALYSER version 5.8 64-bit x86_64 linux
Parsing float.c
Converting
Type-checking float
Generating GOTO Program
Removing function pointers and virtual functions
Partial Inlining
Selecting abstract domain
Computing abstract states
Performing task
Checking assertions
******** Function main
[main.assertion.1] file float.c line 7 function main, assertion ten <= 10 && ten >= 10: Success
[main.assertion.2] file float.c line 8 function main, assertion ten == 10: Unknown
[main.assertion.3] file float.c line 10 function main, assertion y <= 10.0f && y >= 10.0f: Success
[main.assertion.4] file float.c line 11 function main, assertion y == 10.0f: Unknown
[main.assertion.5] file float.c line 24 function main, assertion x < 3.0f: Unknown
[main.assertion.6] file float.c line 25 function main, assertion x <= 3.0f: Unknown

So it's not actually able to tell that x is in [1.0f,2.0f]. What's even weirder is that it can't do equality, but has no problem checking the equivalent condition with two inequalities and &&.

Besides that, the interval domain currently has no handling of arithmetic at all.