Option --full-slice is unsound

[peterschrammel]

add regression tests for C

@kroening, any observations what goes wrong with --full-slice at the moment?

[lucasccordeiro]

@kroening: can you also provide some starting point for this particular task? For example, which test cases should I consider (or if I have to create a test suite)? What is actually wrong with --full-slice and --all-properties? Which additional options should I use to test --full-slice and --all-properties (e.g., cbmc file.c --full-slice, cbmc file.c --all-properties)?

[lucasccordeiro]

@peterschrammel: which test suite can I add regression tests related to this issue? It seems that the --all-properties option is related to cbmc-incr. Is that correct? However, --full-slice option is not clear which test suite I can add test cases to.

[lucasccordeiro]

Just to keep the history.

@tautschnig: This is the example with pointers that I mentioned in your visit at DiffBlue.

void *malloc(__CPROVER_size_t);
void free(void *);
int main()
{
  int *p=malloc(sizeof(int));
  int *q=p;
  int i, x;
  i=x;
  if(i==4711) free(q);
  // should fail if i==4711
  *p=1;
}

I was getting a different verification result when verifying it with --full-slice.

Additionally, the full-slice option gives incorrect results for the following C programs from cbmc regression suite:

Running Fixedbv3/test.desc [FAILED]
Running Float3/test.desc [FAILED]
Running Float3/test.desc [FAILED]
Running Function5/test.desc [FAILED]
Running Function6/test.desc [FAILED]
Running Local_out_of_scope1/test.desc [FAILED]
Running Memory_leak1/test.desc [FAILED]
Running Overflow_Addition1/test.desc [FAILED]
Running Pointer_Arithmetic5/test.desc [FAILED]
Running Pointer_byte_extract5/test.desc [FAILED]
Running Sideeffects5/test.desc [FAILED]
Running Sideeffects6/test.desc [FAILED]
Running String2/test.desc [FAILED]
Running String6/test.desc [FAILED]
Running Undefined_Function1/test.desc [FAILED]
Running Undefined_Function2/test.desc [FAILED]
Running array-tests/test.desc [FAILED]
Running complex1/test.desc [FAILED]
Running equality_through_union3/test.desc [FAILED]
Running exit1/test.desc [FAILED]
Running gcc_vector2/test.descbash: line 1: 21193 Aborted (core dumped) ../../../src/cbmc/cbmc --full-slice main.c > main.out 2>&1
[FAILED]
Running realloc1/test.desc [FAILED]
Running realloc2/test.desc [FAILED]
Running realloc3/test.desc [FAILED]
Running struct6/test.desc [FAILED]

We believe that issue #327 should resolve part of these problems.

[lucasccordeiro]

We have made some progress with the full-slice option, but we are still facing issues about the functional call. Here is the current status of the CBMC regression suite when using the --full-slice option:

Fixedbv3/test.desc  [FAILED]
Float3/test.desc  [FAILED]
Function6/test.desc  [FAILED]
array-tests/test.desc  [FAILED]
equality_through_union3/test.desc  [FAILED]
realloc1/test.desc  [FAILED]
realloc2/test.desc  [FAILED]
realloc3/test.desc  [FAILED]

[lucasccordeiro]

@tautschnig: After integrating your work from #327 into my branch, most benchmarks fail due to "failed to find state". In particular, this part of the code in the ai.h:

  inline const domainT &operator[](locationt l) const
  {
    typename state_mapt::const_iterator it=state_map.find(l);
    if(it==state_map.end()) throw "failed to find state";
    return it->second;
  }

It must be some minor issue to solve, but I'm still unable to find the root cause. Do you have any suggestion?

[lucasccordeiro]

Some additional information about the debug process. It seems that we correctly build the CFG, fill the queue according to slicing criterion, and then compute the program dependence graph (and post-dominators). However, when we try computing the fixedpoint, we simply get "failed to find state" after adding the data / control dependencies for a given node.

[lucasccordeiro]

If we check whether a given state exists before we add data / control dependencies, then apparently it solves the problem; however, I'm unsure whether this fix is correct. This really needs further investigation. Here is the current status if I run CBMC regression suite using the full-slice option:

Memmove1/test.desc  [FAILED]
Recursion3/test.desc  [FAILED]
Recursion4/test.desc  [FAILED]
Recursion6/test.desc  [FAILED]
array-tests/test.desc  [FAILED]
equality_through_union3/test.desc  [FAILED]
realloc1/test.desc  [FAILED]
realloc2/test.desc  [FAILED]

[tautschnig]

Thanks lot for all the updates! Unfortunately I won't find time to properly look into this before Saturday, but any notes posted by then will be of help.

[lucasccordeiro]

@tautschnig: I was just wondering whether you had a chance to look at this issue? I'm going to create some issue in github so that I can get assistance to fix further bugs that I have found in the dependence graph (e.g., C programs with unions are not fully supported).

[lucasccordeiro]

@tautschnig: If we check for array_copy during the implicit call in the full slicer, then we can fix the issues related to the test cases realloc1 and realloc2.

static bool implicit(const namespacet &ns, goto_programt::const_targett target)
{
  // some variables are used during symbolic execution only

  const irep_idt &statement=target->code.get(ID_statement);
  if (statement==ID_array_copy) return true;
  ...
}

However, we still have 6 issues to fix in the CBMC regression suite as follows:

Memmove1/test.desc  [FAILED]
Recursion3/test.desc  [FAILED]
Recursion4/test.desc  [FAILED]
Recursion6/test.desc  [FAILED]
array-tests/test.desc  [FAILED]
equality_through_union3/test.desc  [FAILED]

I have open a ticket in github to further investigate the test case equality_through_union3 (#380).

I'll take a look at the other test cases that are failing.

[lucasccordeiro]

@kroening and @tautschnig: I have updated my branch with the latest version of the CBMC master branch. This particular commit starts breaking the full-slice option of CBMC:

fca6cd6 (make_top, make_bottom, make_entry are now are required)

In order to reproduce the problem, you can just compile and run the CBMC master branch as follows:

lucascordeiro@lucascordeiro:~/cbmc/regression/cbmc/equality_through_array1$ ~/cbmc/src/cbmc/cbmc main.c --full-slice
CBMC version 5.6 64-bit x86_64 linux
Parsing main.c
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Converting
Type-checking main
file main.c line 17 function main: function `assert' is not declared
file main.c line 19 function main: function has return void but a return statement returning signed int
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Performing a full slice
cbmc: ../analyses/dependence_graph.h:124: dep_graph_domaint::node_indext dep_graph_domaint::get_node_id() const: Assertion `node_id!=std::numeric_limits<node_indext>::max()' failed.
Aborted (core dumped)

I'm struggling for some days to find a solution for this particular problem as I don't understand very well this AI code. In the full slicer code, I'm unsure whether I'm incorrectly instantiating the program dependence graph after all those changes to the CBMC master:

  // compute program dependence graph (and post-dominators)
  dependence_grapht dep_graph(ns);
  dep_graph(goto_functions, ns);

I've also talked to @danpoe to get some help on the AI code, but this particular part of the code (i.e., the dependence graph) is also new for him.

I would appreciate any support from @kroening and @tautschnig since I have no idea about the root cause of the problem.

[danpoe]

I think I know what the problem is. get_state() is overridden to set the node id but initialize() then sets it to unsigned_max() again. I'll provide a fix.