Symbolic execution expression forwarding * but not +

[martin-cs]

Given the following structurally equivalent functions...

#include <assert.h>

void add (void) {
int x;
int y;

int z = x + y;

assert(z);

return;
}

void multiply (void) {
int x;
int y;

int z = x * y;

assert(z);

return;
}

We get two different sets of VCs

$ cbmc ~/tmp/can-delete/expression-forwarding.c --function multiply --show-vcc
CBMC version 5.6 64-bit x86_64 linux
Parsing /home/martin/tmp/can-delete/expression-forwarding.c
Converting
Type-checking expression-forwarding
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 35 steps
simple slicing removed 4 assignments
Generated 1 VCC(s), 1 remaining after simplification

VERIFICATION CONDITIONS:

file /home/martin/tmp/can-delete/expression-forwarding.c line 21 function multiply
assertion z
{-1} __CPROVER_dead_object#1 == NULL
{-2} __CPROVER_deallocated#1 == NULL
{-3} __CPROVER_malloc_is_new_array#1 == FALSE
{-4} __CPROVER_malloc_object#1 == NULL
{-5} __CPROVER_malloc_size#1 == 0ul
{-6} __CPROVER_memory_leak#1 == NULL
{-7} __CPROVER_next_thread_id#1 == 0ul
{-8} __CPROVER_pipe_count#1 == 0u
{-9} __CPROVER_rounding_mode!0#1 == 0
{-10} __CPROVER_thread_id!0#1 == 0ul
{-11} __CPROVER_threads_exited#1 == ARRAY_OF(FALSE)

{-12} z!0@1#2 == x!0@1#1 * y!0@1#1
{1} !(x!0@1#1 * y!0@1#1 == 0)

$ cbmc ~/tmp/can-delete/expression-forwarding.c --function add --show-vcc
CBMC version 5.6 64-bit x86_64 linux
Parsing /home/martin/tmp/can-delete/expression-forwarding.c
Converting
Type-checking expression-forwarding
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 35 steps
simple slicing removed 4 assignments
Generated 1 VCC(s), 1 remaining after simplification

VERIFICATION CONDITIONS:

file /home/martin/tmp/can-delete/expression-forwarding.c line 9 function add
assertion z
{-1} __CPROVER_dead_object#1 == NULL
{-2} __CPROVER_deallocated#1 == NULL
{-3} __CPROVER_malloc_is_new_array#1 == FALSE
{-4} __CPROVER_malloc_object#1 == NULL
{-5} __CPROVER_malloc_size#1 == 0ul
{-6} __CPROVER_memory_leak#1 == NULL
{-7} __CPROVER_next_thread_id#1 == 0ul
{-8} __CPROVER_pipe_count#1 == 0u
{-9} __CPROVER_rounding_mode!0#1 == 0
{-10} __CPROVER_thread_id!0#1 == 0ul
{-11} __CPROVER_threads_exited#1 == ARRAY_OF(FALSE)

{-12} z!0@1#2 == x!0@1#1 + y!0@1#1
{1} !(z!0@1#2 == 0)

That these two are handled differently seems strange, thus I'm raising this as an issue. Right now having the add behaviour (i.e. not expression forwarding) for the multiply case would be super handy so if anyone could point me in the direction of where this happens I'm happy to patch / hack this as appropriate.

[martin-cs]

So I've found this:

https://github.com/diffblue/cbmc/blob/master/src/goto-symex/goto_symex_state.cpp#L168

which seems to give the hack I need but ... is there any justification for this code other than ... it seems to help / do the right thing?

[tautschnig]

I believe it's just a plain bug, because the expr.id()==ID_mult is just an overly complicated way of saying return true.

[david-k]

Hi, I stumbled upon the same problem (multiplications always being forwarded) and wanted to ask what the current state of this issue is. It seems it should be easy to fix, but I don't really understand the special case for ID_C_c_sizeof_type so I should probably not touch the code.

[tautschnig]

To what extent is it a "problem" for people? The code is strange and, in a way, wrong, but what is it that elevates this to an observable problem?

FWIW, the correct code should be:

  else if(expr.id()==ID_mult)
  {
    // propagate stuff with sizeof in it
    forall_operands(it, expr)
    {
      if(it->find(ID_C_c_sizeof_type).is_not_nil())
        return true;
      else if(!constant_propagation(*it))
        return false;
    }

    return true;
  }

[david-k]

Thank you!
We use CBMC to separately compile functions to circuits. If function A computes a * b and passes the result to another function B, then B would compute the multiplication again if a * b is being forwarded.

EDIT: Will this code be committed?

[tautschnig]

I'll try to find time to put in a pull request in the next hours.

[david-k]

No hurry, and thanks again.

[tautschnig]

@david-k See #1099.