Performance with temporary variables #7013

zhassan-aws · 2022-07-18T23:31:35Z

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 model-checking/kani#1351 difficult to solve even though the Rust program itself does not involve temporary variables.

The text was updated successfully, but these errors were encountered:

martin-cs · 2022-07-19T13:33:59Z

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:

cbmc/src/goto-symex/goto_state.h

Line 64 in d69761e

// Map L1 names to (L2) constants. Values will be evicted from this map

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 · 2022-07-19T14:42:58Z

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 · 2022-07-19T15:38:11Z

@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

cbmc/src/analyses/constant_propagator.h

Line 9 in d69761e

/// \file

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 · 2022-07-20T09:06:23Z

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 · 2022-07-20T09:43:43Z

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

tautschnig · 2022-07-20T09:52:02Z

"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 · 2022-07-21T06:57:49Z

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 · 2022-10-06T15:30:47Z

Notes as just discussed out-of-band:

The SAT back-end will avoid generating fresh symbols for temporary variables in many (but not necessarily: all) cases.
A more general caching than the hack mentioned in Performance with temporary variables #7013 (comment) would be to cache all Tseitin encoding steps. This may reduce formula size substantially, but cache lookups could prove costly. Needs to be implemented and measured.
The problem is more specific than the subject might suggest: if there is no multiplication involved, then there will likely not be a problem either. Multiplication is provably hard. We can try to do a bit better, but that's a way bigger task (with no firm promises on results to be made).
It may be that --refine-arithmetic addresses the problem to some extent, but really the refinement code is in need of love.

remi-delmas-3000 · 2025-01-23T19:26:29Z

with kissat v4.0.1 this is solved in under two seconds thanks to clausal congruence closure and sweeping

VERIFICATION SUCCESSFUL
cbmc mul.c --external-sat-solver kissat  1.89s user 0.09s system 96% cpu 2.054 total

#include <assert.h>

int main() {
    int x;
    __CPROVER_assume(-46340 <= x && x <= 46340);
    int y;
    __CPROVER_assume(-46340 <= y && y <= 46340);
    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;
}

c [congruence-1] found 6501 AND gates (6492 extracted 100% + 9 matched 0%)
c [congruence-1] found 2364 XOR gates (2355 extracted 100% + 9 matched 0%)
c [congruence-1] found 446 ITE gates (446 extracted 100% + 0 matched 0%)
c [congruence-1] found 9311 gates (54.16% variables)
c [congruence-1] found 6368 matchable variables 37%
c [congruence-1] subsumed 6600 clauses out of 49380 tried 13%
c [congruence-1] merged 5084 equivalent variables 29.57%
c [congruence-2] found 1283 AND gates (1283 extracted 100% + 0 matched 0%)
c [congruence-2] found 621 XOR gates (621 extracted 100% + 0 matched 0%)
c [congruence-2] found 0 ITE gates (0 extracted 0% + 0 matched 0%)
c [congruence-2] found 1904 gates (26.27% variables)
c [congruence-2] found 160 matchable variables 3%
c [congruence-2] subsumed 8 clauses out of 1027 tried 1%
c [congruence-2] merged 92 equivalent variables 1.50%
c [congruence-3] found 831 AND gates (820 extracted 99% + 11 matched 1%)
c [congruence-3] found 445 XOR gates (445 extracted 100% + 0 matched 0%)
c [congruence-3] found 0 ITE gates (0 extracted 0% + 0 matched 0%)
c [congruence-3] found 1276 gates (24.59% variables)
c [congruence-3] found 6 matchable variables 0%
c [congruence-3] subsumed 5 clauses out of 156 tried 3%
c [congruence-3] merged 3 equivalent variables 0.06%
c [congruence-4] found 366 AND gates (297 extracted 81% + 69 matched 19%)
c [congruence-4] found 132 XOR gates (126 extracted 95% + 6 matched 5%)
c [congruence-4] found 0 ITE gates (0 extracted 0% + 0 matched 0%)
c [congruence-4] found 498 gates (24.51% variables)
c [congruence-4] merged 0 equivalent variables 0.00%
c           0.07    5.81 %  congruence
c [sweep-1] scheduled 9063 variables 100% (0 rescheduled 0%, 0 incomplete 0%)
c [sweep-1] found 817 equivalences and 0 units
c [sweep-1] swept 1145 variables (8207 remain 91%)
c [sweep-2] scheduled 5593 variables 100% (5593 rescheduled 100%, 5593 incomplete 100%)
c [sweep-2] found 79 equivalences and 0 units
c [sweep-2] swept 198 variables (5396 remain 96%)
c [sweep-3] scheduled 2684 variables 95% (2684 rescheduled 100%, 2684 incomplete 100%)
c [sweep-3] found 209 equivalences and 1 units
c [sweep-3] swept 229 variables (2338 remain 87%)
c [sweep-4] scheduled 1974 variables 91% (1974 rescheduled 100%, 1974 incomplete 100%)
c [sweep-4] found 334 equivalences and 7 units
c [sweep-4] swept 336 variables (1678 remain 85%)
c [sweep-5] scheduled 1546 variables 76% (1546 rescheduled 100%, 1544 incomplete 100%)
c [sweep-5] found 577 equivalences and 8 units
c [sweep-5] swept 475 variables (1089 remain 70%)
c [sweep-6] scheduled 532 variables 59% (532 rescheduled 100%, 530 incomplete 100%)
c [sweep-6] found 141 equivalences and 6 units
c [sweep-6] swept 458 variables (112 remain 21%)
c [sweep-7] scheduled 122 variables 14% (122 rescheduled 100%, 112 incomplete 92%)
c [sweep-7] found 20 equivalences and 7 units
c [sweep-7] swept 142 variables (0 remain 0%)
c           0.23   17.71 %  sweep
c sweep:                                    7             2566    interval
c sweep_completed:                          1                7.00 sweeps
c sweep_equivalences:                    2177               13 %  variables
c sweep_solved:                         23858               87 %  kitten_solved
c sweep_units:                             29                0 %  variables

kroening · 2025-01-23T19:30:08Z

with kissat v4.0.1 this is solved in under two seconds thanks to clausal congruence closure and sweeping

Impressive!

zhassan-aws · 2025-01-23T21:27:36Z

The same applies to the upstream Kani example:

$ kani repeat.rs --solver kissat
...
SUMMARY:
 ** 0 of 2 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.79529274s

celinval added Performance Optimisations aws Bugs or features of importance to AWS CBMC users aws-high Kani Bugs or features of importance to Kani Rust Verifier labels Jul 18, 2022

tautschnig self-assigned this Sep 2, 2022

tautschnig removed their assignment Oct 6, 2022

tautschnig removed the aws-high label Oct 7, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Performance with temporary variables #7013

Performance with temporary variables #7013

zhassan-aws commented Jul 18, 2022

martin-cs commented Jul 19, 2022

remi-delmas-3000 commented Jul 19, 2022

martin-cs commented Jul 19, 2022

tautschnig commented Jul 20, 2022

kroening commented Jul 20, 2022

tautschnig commented Jul 20, 2022

rladydpf1 commented Jul 21, 2022 •

edited

Loading

tautschnig commented Oct 6, 2022

remi-delmas-3000 commented Jan 23, 2025 •

edited

Loading

kroening commented Jan 23, 2025

zhassan-aws commented Jan 23, 2025

Performance with temporary variables #7013

Performance with temporary variables #7013

Comments

zhassan-aws commented Jul 18, 2022

martin-cs commented Jul 19, 2022

remi-delmas-3000 commented Jul 19, 2022

martin-cs commented Jul 19, 2022

tautschnig commented Jul 20, 2022

kroening commented Jul 20, 2022

tautschnig commented Jul 20, 2022

rladydpf1 commented Jul 21, 2022 • edited Loading

tautschnig commented Oct 6, 2022

remi-delmas-3000 commented Jan 23, 2025 • edited Loading

kroening commented Jan 23, 2025

zhassan-aws commented Jan 23, 2025

rladydpf1 commented Jul 21, 2022 •

edited

Loading

remi-delmas-3000 commented Jan 23, 2025 •

edited

Loading