Post CBMC-5.5 changes in return variables causes a regression in the dependence-graph computation

[martin-cs]

The following program shows the issue but I think it is a lot more general:

$ cat ~/tmp/can-delete/loop.c
#include <assert.h>

int main (void) {
int x;
int i;

if (x > 0) {
    for (i = 0; i < x; ++i) {
        // Do nothing;
    }
} else {
    x = 1;
}

assert(x >= 1);

return 0;
}

It looks commit 1218856 works:

$ ./cbmc/cbmc --full-slice --unwind 1 ~/tmp/can-delete/loop.c
CBMC version 5.5 64-bit x86_64 linux
Parsing /home/martin/tmp/can-delete/loop.c
Converting
Type-checking loop
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Performing a full slice
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
Not unwinding loop main.0 iteration 1 (1 max) file /home/martin/tmp/can-delete/loop.c line 8 function main thread 0
size of program expression: 26 steps
simple slicing removed 2 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
199 variables, 464 clauses
SAT checker: instance is UNSATISFIABLE
Runtime decision procedure: 0.003s

** Results:
[main.assertion.1] assertion x >= 1: SUCCESS

** 0 of 1 failed (1 iteration)
VERIFICATION SUCCESSFUL

but the next commit e26d20e doesn't:

$ ./cbmc/cbmc --full-slice --unwind 1 ~/tmp/can-delete/loop.c
CBMC version 5.5 64-bit x86_64 linux
Parsing /home/martin/tmp/can-delete/loop.c
Converting
Type-checking loop
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Performing a full slice
code

• type: code
• statement: output
• #source_location:
  • file: /home/martin/tmp/can-delete/loop.c
  • line: 17
  • function: main
  • working_directory: /home/martin/working-copies/cbmc-git/src
    0: address_of
    • type: pointer
      0: signedbv
      * width: 8
      * #c_type: char
      0: index
      • type: signedbv
        • width: 8
        • #c_type: char
          0: string_constant
        • type: array
          • size: constant
            • type: signedbv
              • width: 64
              • #c_type: signed_long_int
            • value: 0000000000000000000000000000000000000000000000000000000000000111
              0: signedbv
            • width: 8
            • #c_type: char
        • value: return
          1: constant
        • type: signedbv
          • width: 64
          • #c_type: signed_long_int
        • value: 0000000000000000000000000000000000000000000000000000000000000000
          1: symbol
    • type: signedbv
      • width: 32
      • #c_type: signed_int
    • identifier: return'
      value_set_fit: unexpected statement: output

The backtrace is interesting because the problem is actually triggered in the value set analysis, despite the changes being to the expression creation:

(gdb) backtrace
#0 0x00007ffff7b2fdbd in __cxa_throw () from /usr/lib/x86_64-linux-gnu/libstdc++.so.6
#1 0x0000000000425c2e in value_set_fit::apply_code(exprt const&, namespacet const&) ()
#2 0x000000000041baa2 in value_set_domain_fit::transform(namespacet const&, std::_List_const_iterator<goto_program_templatet<codet, exprt>::instructiont>, std::_List_const_iterator<goto_program_templatet<codet, exprt>::instructiont>) ()
#3 0x00000000004515b5 in flow_insensitive_analysis_baset::visit(std::_List_const_iterator<goto_program_templatet<codet, exprt>::instructiont>, std::priority_queue<std::_List_const_iterator<goto_program_templatet<codet, exprt>::instructiont>, std::vector<std::_List_const_iterator<goto_program_templatet<codet, exprt>::instructiont>, std::allocator<std::_List_const_iterator<goto_program_templatet<codet, exprt>::instructiont> > >, std::less<std::_List_const_iterator<goto_program_templatet<codet, exprt>::instructiont> > >&, goto_programt const&, goto_functionst const&) ()
#4 0x00000000004518d3 in flow_insensitive_analysis_baset::fixedpoint(goto_programt const&, goto_functionst const&) ()
#5 0x0000000000452eee in flow_insensitive_analysis_baset::fixedpoint(goto_functionst const&) ()
#6 0x0000000000449643 in reaching_definitions_analysist::initialize(goto_functionst const&) ()
#7 0x0000000000433ff6 in full_slicert::operator()(goto_functionst&, namespacet const&, slicing_criteriont&) ()
#8 0x0000000000434e15 in full_slicer(goto_functionst&, namespacet const&) ()
#9 0x00000000004ac1c8 in cbmc_parse_optionst::process_goto_program(optionst const&, goto_functionst&) ()
#10 0x00000000004ab80f in cbmc_parse_optionst::get_goto_program(optionst const&, bmct&, goto_functionst&) ()
#11 0x00000000004acd8c in cbmc_parse_optionst::doit() ()
#12 0x000000000040bbbd in main ()

which makes me concerned that the value set analysis might not be the only bit of code that makes these assumptions about expressions that are broken by this change.

@lucasccordeiro : person who said they'd work on it
@peterschrammel : person who wrote the original patch
@kroening : person who merged this

[martin-cs]

PS
6dcd02a 31/08/16 broken
2cc583f 24/08/16 broken
2ad9f7b 22/08/16 broken
a986020 22/08/16 broken
e26d20e 21/08/16 broken
1218856 20/08/16 works
51b6ab7 20/08/16 (cbmc-5.5) works
970b994 07/08/16 works
d4a7cc3 01/07/16 works
2737ce3 29/04/16 works

[lucasccordeiro]

@martin-cs: Many thanks for reporting this bug. It seems that we can correctly verify this program from the code in: https://github.com/lucasccordeiro/cbmc/tree/siemens_fix260

If you like, you can review all commits in that branch and give us feedback. With the support from Anna, we were able to fix some bugs, but not all of them. For example, take a look at this program that we discussed yesterday in the uni:

#include <assert.h>
int n=2, i, s, a = 0;
void main()
{
i = 1;
s = 1;
if (a > 0)
s = 0;
while (i <= n)
{
if (a > 0)
s += 2;
else
s *= 2;
i++;
}
assert(s>0);
}

If we declare "n" as a global variable, then CBMC unwinds the while loop forever. However, if "n" is declared as local variable, then it works fine.

Let us know if you have some thought about this.

[lucasccordeiro]

The problem seems to be related to __CPROVER_initialize. When we enable the option --full-slice, the original __CPROVER_initialize:

__CPROVER_initialize /* __CPROVER_initialize */
// 17 no location
// Labels: __CPROVER_HIDE
SKIP
// 18 file line 39
__CPROVER_dead_object = NULL;
// 19 file line 38
__CPROVER_deallocated = NULL;
// 20 file line 42
__CPROVER_malloc_is_new_array = 0 != 0;
// 21 file line 40
__CPROVER_malloc_object = NULL;
// 22 file line 41
__CPROVER_malloc_size = 0ul;
// 23 file line 43
__CPROVER_memory_leak = NULL;
// 24 file line 31
__CPROVER_next_thread_id = (unsigned long int)0;
// 25 file line 85
__CPROVER_pipe_count = (unsigned int)0;
// 26 file line 65
__CPROVER_rounding_mode = 0;
// 27 file line 29
__CPROVER_thread_id = (unsigned long int)0;
// 28 file line 30
__CPROVER_threads_exited = ARRAY_OF(FALSE);
// 29 file /home/lucascordeiro/Documents/slice09/main.c line 2
a = 0;
// 30 file /home/lucascordeiro/Documents/slice09/main.c line 2
i = 0;
// 31 file /home/lucascordeiro/Documents/slice09/main.c line 2
n = 2;
// 32 file /home/lucascordeiro/Documents/slice09/main.c line 2
s = 0;
// 33 no location
END_FUNCTION

becomes:

__CPROVER_initialize /* __CPROVER_initialize */
// 16 no location
// Labels: __CPROVER_HIDE
SKIP
// 17 file line 65 column ins:31 req by:31
__CPROVER_rounding_mode = 0;
// 18 no location
END_FUNCTION

[lucasccordeiro]

Before computing the dependency graph, the slicer fills a queue according to slicing criterion. In particular, it checks for some variables are used during symbolic execution as follows:

void full_slicert::operator()(
goto_functionst &goto_functions,
const namespacet &ns,
slicing_criteriont &criterion)
{
...
if(criterion(e_it->first))
add_to_queue(queue, e_it->second, e_it->first);
else if(implicit(ns,e_it->first))
add_to_queue(queue, e_it->second, e_it->first);
...
}

static bool implicit(goto_programt::const_targett target)
{
// some variables are used during symbolic execution only
if(!target->is_assign()) return false;

const code_assignt &a=to_code_assign(target->code);
if(a.lhs().id()!=ID_symbol) return false;

const symbol_exprt &s=to_symbol_expr(a.lhs());

return s.get_identifier()==CPROVER_PREFIX "rounding_mode";
}

As a result, the slicer was just considering the __CPROVER_rounding_mode and disregarding all other CPROVER_PREFIX and assignments (to global variables) used in the __CPROVER_initialize. However, depending on the property being checked, those variables are actually needed; otherwise we get incorrect verification results. In the branch siemens_fix260, there is one possible fix for this particular issue, but we have to review/investigate it further to check whether it is the correct way to fix the issue.

I have also included 10 test cases into cbmc-slice suite, taken from papers and reports, in order to test the full-slice option.

[martin-cs]

This is all useful but I don't see how it is connected to the problem I reported. Perhaps it should go under another issue? If it's removing assignments to global variables that changes relevant behaviour then that should be regarded as a bug and just disabling the slicer for one function will likely not fix it. This seems a verify different issue from a particular patch of Peter's that causes the value set analysis to crash.

[lucasccordeiro]

There is already one (general) issue created for testing and repairing the full-slice option:
Test and repair --full-slice and --all-properties #260

[martin-cs]

This problem is connected to return statements. If the return type of the function is void and there are no return statements it is not triggered.

[martin-cs]

Peter says "add a case for ID_output to value_set_fit::apply_code and all will be well".

[martin-cs]

Have implemented Peter's suggestion and it seems to work.

Lucas : sorry if this is duplicating work but I need (just) this fix ASAP.

[martin-cs]

Closed with merge.