search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
827 stars 260 forks source link

Performance with temporary variables #7013

Open zhassan-aws opened 2 years ago

zhassan-aws commented 2 years ago

CBMC version: 5.61.0 Operating system: Ubuntu 20.04

CBMC manages to solve the following program quickly:

#include <assert.h>

int main() {
    int x;
    int y;
    int o1 = x * y;
    int o2 = x * y;
    assert(o1 == o2);
    return 0;
}
$ /usr/bin/time -p cbmc repeat_no_temp_vars.c 
CBMC version 5.61.0 (cbmc-5.61.0) 64-bit x86_64 linux
Parsing repeat_no_temp_vars.c
<snip>
** Results:
repeat_no_temp_vars.c function main
[main.assertion.1] line 8 assertion o1 == o2: SUCCESS

** 0 of 1 failed (1 iterations)
VERIFICATION SUCCESSFUL
real 0.02
user 0.01
sys 0.00

But if I inject temporary variables:

#include <assert.h>

int main() {
    int x;
    int y;
    int t1 = x;
    int t2 = y;
    int o1 = t1 * t2;
    int t3 = x;
    int t4 = y;
    int o2 = t3 * t4;
    assert(o1 == o2);
    return 0;
}

it runs for >10 minutes without terminating.

Are there possible optimizations/reductions that would allow discovering that the two expressions are equivalent?

Such an optimization would particularly be helpful for Kani because its codegen flow produces lots of temporary variables (e.g. due to SSA). This makes programs like this one https://github.com/model-checking/kani/issues/1351 difficult to solve even though the Rust program itself does not involve temporary variables.

martin-cs commented 2 years ago

Short answer : use an SMT solver as a back-end. Improving "constant" propagation can probably fix this case but I am not sure that it will fix everything like this.

Long answer: If we use --show-vcc we can see what equations are generated. --slice-formula helps remove the noise.

$ ./cbmc/cbmc ~/tmp/can-delete/cbmc-7013-1.c --show-vcc --slice-formula
CBMC version 5.56.0 (cbmc-5.56.0-21-g531c9534db-dirty) 64-bit x86_64 linux
Parsing /home/martin/tmp/can-delete/cbmc-7013-1.c
Converting
Type-checking cbmc-7013-1
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00380649s
size of program expression: 42 steps
slicing removed 19 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 0.000118102s
VERIFICATION CONDITIONS:

file /home/martin/tmp/can-delete/cbmc-7013-1.c line 8 function main
assertion o1 == o2
{-1} main::1::o1!0@1#2 = main::1::x!0@1#1 * main::1::y!0@1#1
{-2} main::1::o2!0@1#2 = main::1::x!0@1#1 * main::1::y!0@1#1
├──────────────────────────
{1} main::1::o1!0@1#2 = main::1::o2!0@1#2

$ ./cbmc/cbmc ~/tmp/can-delete/cbmc-7013-2.c --show-vcc --slice-formula
CBMC version 5.56.0 (cbmc-5.56.0-21-g531c9534db-dirty) 64-bit x86_64 linux
Parsing /home/martin/tmp/can-delete/cbmc-7013-2.c
Converting
Type-checking cbmc-7013-2
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00248683s
size of program expression: 50 steps
slicing removed 23 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 7.8182e-05s
VERIFICATION CONDITIONS:

file /home/martin/tmp/can-delete/cbmc-7013-2.c line 12 function main
assertion o1 == o2
{-1} main::1::t1!0@1#2 = main::1::x!0@1#1
{-2} main::1::t2!0@1#2 = main::1::y!0@1#1
{-3} main::1::o1!0@1#2 = main::1::t1!0@1#2 * main::1::t2!0@1#2
{-4} main::1::t3!0@1#2 = main::1::x!0@1#1
{-5} main::1::t4!0@1#2 = main::1::y!0@1#1
{-6} main::1::o2!0@1#2 = main::1::t3!0@1#2 * main::1::t4!0@1#2. 
├──────────────────────────
{1} main::1::o1!0@1#2 = main::1::o2!0@1#2

Let's break down what is happening a bit:

A. Symex aims to generate one equation per assignment. Each assignment creates a new solver variable for the value of a program variable after the assignment. This makes it easy to generate the trace but can (normally a small amount but in rare cases, a lot) make the formula bigger than strictly necessary.

B. Rewriting is applied when it is being generated. This is what allows us to determine when for (int i = 0; i < 10; ++i) { ... } terminates. It also reduces formula.

C. To help improve the rewriting, we have a step known (misleadingly) as constant propagation. According to a heuristic it will sometimes replace a solver variable with it's value when building the assignment. For example:

#include <assert.h>

int main() {
    int x = 1;
    int y = x + 1;
    int z = y + 1;

    while (z != 3) {
      ++z;
      assert(z != 4);
    }

    return 0;
}

will not even generate any VCs because of constant propagation.

D. When the SAT back-end bit-blasts expressions, it caches them based on a structural hash. This can lead to simplifications when the same expression is used twice.

So what is happening in the first case is that the assignments generate two different variables, the back-end bit-blasts the multiply for one assignment and then uses that cached one for the second, the equality simplifies away and the whole thing is trivial.

In the second case the assignments are generated but the values are not constant propagated, so the multiplies are structurally different and it can't be simplified. Due to $REASONS, the SAT solver can't handle this expression and it times out.

Proper solution : use an SMT solver. They will compute a union-find closure of equivalent variables, substitute and rewrite. That's enough to handle all of this kind of issue.

Hacky work-around : Have a look at the propagation map and the code that adds to it: https://github.com/diffblue/cbmc/blob/d69761e962e0181ef50c5b31c807d2514028493c/src/goto-symex/goto_state.h#L64 Get direct assignments of the form x = y to add rename(y) as the value of x. Be prepared to hunt some strange downstream bugs and to have to do a substantial amount of benchmarking to see what it does to performance. Talk to @tautschnig before attempting.

Sounds like a good idea but is a lot : Add the union find and substitute (and rewrite) loop to the back-end solver.

Hope that helps.

remi-delmas-3000 commented 2 years ago

For simple cases like this where a fresh variable is assigned only once and is not dirty wouldn't it be safe to propagate/substitute it in a single forward pass on the goto program, statically before SymEx ?

martin-cs commented 2 years ago

@remi-delmas-3000 in principle it should work but in practice I would not advise it because:

A. Adding extra passes, esp. those that mean --show-goto-functions is not what is processed is a non-trivial cost. B. This is harder and more fiddly than it sounds. @peterschrammel wrote https://github.com/diffblue/cbmc/blob/d69761e962e0181ef50c5b31c807d2514028493c/src/analyses/constant_propagator.h#L9 to do something like this for https://github.com/diffblue/2ls you need to handle a lot more fiddly edge cases than you would think to get consistent performance and it is hard to do this in a way that is sound without tracking pointers... C. ... which is what goto-analyzer --vsd --simplify does but more importantly what is done during symex. The information you need to tell when things are safe is already there during.

If you want to do something like that I would recommend going the route of strengthening what propagation does. But really definitely talk to @tautschnig first as he has been playing with patches to do this since ... 2013?

tautschnig commented 2 years ago

In addition to what @martin-cs said: I am contemplating adding a circuit cache that should pick up the equality despite the temporary variables. But ultimately multiplication is fundamentally hard, and it will always be easy to construct an example that is very hard to solve.

kroening commented 2 years ago

Perhaps mostly for entertainment: backwards substitution also solves problems like this trivially.

tautschnig commented 2 years ago

"Cache expensive circuits for given input bvts" in #7001 now implements such a circuit cache, which indeed makes the provided example trivial to solve.

rladydpf1 commented 2 years ago

I have a similar problem.

CBMC version: 5.43.0 Operating system: Ubuntu 20.04

#include <assert.h>
void assume_abort_if_not(signed int cond);
float f(float x);
float fp(float x);
void reach_error();

extern float __VERIFIER_nondet_float();
float f(float x) {
    return (((x - (((x * x) * x) / 6.0f)) + (((((x * x) * x) * x) * x) / 120.0f)) + (((((((x * x) * x) * x) * x) * x) * x) / 5040.0f));
}
float fp(float x) {
    return ((((float)(1) - ((x * x) / 2.0f)) + ((((x * x) * x) * x) / 24.0f)) + ((((((x * x) * x) * x) * x) * x) / 720.0f));
}
void reach_error() {
    assert((0 != 0));
}
void assume_abort_if_not(signed int cond) {
    __CPROVER_assume(((signed int)((cond != 0)) == 1));
}
int main() {
    float IN = __VERIFIER_nondet_float();

    assume_abort_if_not((signed int)(((IN > -0.8f) && (IN < 0.8f))));
    float x;
    float return_value_f = f(IN);
    x = (IN - (return_value_f / fp(IN)));
    __CPROVER_assume(((signed int)(((double)(x) < 0.1)) == 0));
    reach_error();
}

the variable 'IN' is initialized by '__VERIFIER_nondet_float()'; its CBMC result: 

> cbmc init.c
... 
Solving with MiniSAT 2.2.1 with simplifier
55383 variables, 254544 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 3.94365s
Runtime decision procedure: 4.00351s

And this is not initialized version,

#include <assert.h>
void assume_abort_if_not(signed int cond);
float f(float x);
float fp(float x);
void reach_error();

extern float __VERIFIER_nondet_float();

float f(float x) {
    return (((x - (((x * x) * x) / 6.0f)) + (((((x * x) * x) * x) * x) / 120.0f)) + (((((((x * x) * x) * x) * x) * x) * x) / 5040.0f));
}
float fp(float x) {
    return ((((float)(1) - ((x * x) / 2.0f)) + ((((x * x) * x) * x) / 24.0f)) + ((((((x * x) * x) * x) * x) * x) / 720.0f));
}
void reach_error() {
    assert((0 != 0));
}
void assume_abort_if_not(signed int cond) {
    __CPROVER_assume(((signed int)((cond != 0)) == 1));
}

int main() {
    float IN;
    IN = __VERIFIER_nondet_float();

    assume_abort_if_not((signed int)(((IN > -0.8f) && (IN < 0.8f))));
    float x;
    x = (IN - (f(IN) / fp(IN)));
    __CPROVER_assume(((signed int)(((double)(x) < 0.1)) == 0));
    reach_error();
}

which the variable 'IN' is not initialized. its CBMC result:

> cbmc not_init.c
... 
Solving with MiniSAT 2.2.1 with simplifier
55351 variables, 254544 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 13.6643s
Runtime decision procedure: 13.7251s

After applying the '--slice-formula' option, the reuslt was:

> cbmc not_init.c --slice-formula
... 
Solving with MiniSAT 2.2.1 with simplifier
55231 variables, 254511 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 5.30144s
Runtime decision procedure: 5.36152s
tautschnig commented 1 year ago

Notes as just discussed out-of-band: