Question regarding "cyclic" encoding and propagation of analysis results
MarcoGrochowski opened this issue · 9 comments
I want to analyze PLC programs which exhibit "cyclic" behavior using symbolic execution but sometimes the code is written poorly and there are unreachable branches. For this purpose I need some kind of value-set analysis, but I stumbled upon a few problems. Here is an example of a simple program as a crab cfg:
void declare main()
initialization:
cycle = 0;
x = 0;
goto main_entry;
main_entry:
assume(cycle <= 100);
goto cycle_entry;
cycle_entry:
cycle = cycle+1;
goto main_body;
main_body:
x_res:int32 = call increment(x:int32);
goto cycle_exit;
cycle_exit:
x = x_res;
goto main_entry,main_exit;
main_exit:
assume(-cycle < -100);
x_out:int32 declare increment(x_in:int32)
entry:
goto body;
body:
x_out = x_in+1;
goto exit;
exit:
The program should simply increment the value of x by 1 through the use of a function call in each "iteration" for a couple of "cycles".
Using the top-down interprocedural analyzer with the boxes domain of the ldd library I get the following invariants:
Callgraph=
main--> increment
=================================
void declare main()
cycle_exit={-cycle <= -1; cycle <= 101; -x <= -1; -x_res <= -1}
main_exit={-cycle <= -101; cycle <= 101; -x <= -1; -x_res <= -1}
main_body={-cycle <= -2; cycle <= 101; -x <= -1; -x_res <= -1} or
{-cycle <= -1; cycle <= 1; -x <= 0; x <= 0; -x_res <= -1}
cycle_entry={-cycle <= -2; cycle <= 101; -x <= -1; -x_res <= -1} or
{-cycle <= -1; cycle <= 1; -x <= 0; x <= 0}
main_entry={-cycle <= -1; cycle <= 100; -x <= -1; -x_res <= -1} or
{-cycle <= 0; cycle <= 0; -x <= 0; x <= 0}
initialization={-cycle <= 0; cycle <= 0; -x <= 0; x <= 0}
=================================
x_out:int32 declare increment(x_in:int32)
exit={-x_in <= 0; -x_out <= -1}
body={-x_in <= 0; -x_out <= -1}
entry={-x_in <= 0}
=================================
I would have expected that the value of x is propagated, e.g., main_exit={x>=1;x<=101,...} and that the generated function summary holds must summaries for each valuation of x_in, e.g., x_in = 0, x_in = 1, x_in = 2, ....
What is wrong with my encoding?
Hi @MarcoGrochowski ,
Thank you for using Crab. I think using abstract interpretation for verification of PLC programs is an interesting direction since AFIK most of the verifiers are model checkers.
I think your encoding is right and the results are the expected ones.
After first application of widening, this is the abstract state before
the call:
{ cycle = 2; x=1} or { cycle = 1; x = 0}
During the unification between callsite parameters (x) and increment's
formal parameters (x_in), we get:
{ cycle = 2; x=1; x_in=1} or { cycle = 1; x = 0; x_in=0}
And then, we project out any variable that it's not part of
increment (i.e., we eliminate cycle and x):
{x_in=1} or {x_in=0}
But this equivalent to:
{0<= x_in <=1}
That's the reason why the disjunct dissappear from the summary of
increment. Each time, increment will be analyzed with a single
disjunct: {0<= x_in <=1}, {0<= x_in <=2}, and eventually with only
{0 <= x_in} after widening throws away the upper-bound for x in
the main loop.
In case you wonder why boxes cannot infer that x <= 101 the answer has to
do with narrowing. Since the domain doesn't track a relationship
between cycle and x the widening loses the upper bounds for cycle and x. Narrowing recovers the upper bound for cycle due to the statement assume (cycle <= 100) but it cannot recover the bounds for x.
A simple strategy of widening with thresholds would fix the
problem. Alternatively, a relational domain such as Zones
(split_dbm) would also infer a precise upper bound for x.
I attach my encoding of your program in td_inter_9a.cc. The other program td_inter_9b.cc is equivalent but it passes cycle to increment which simply returns it without modifying it. This example produces the summary that you were asking for.
programs.zip
Hello @caballa, thank you for your response, you helped me a lot!
Indeed, the relational domain split_dbm gives me the correct results and if I delay the widening (e.g., after 100 cycles) in td_inter_9b.cc I get precise bounds.
However, I still have to use the boxes domain because I need to split on boolean values in other benchmarks. I changed my encoding to couple the cycle variable into the callees and modeled the state of the callees as input/output which seems to work :)
Hello @caballa, I've noticed that for bigger examples such as the one depicted below, LDD is rehashing a lot hence not terminating in reasonable time. I've used the boxes domain, the other domains (split_dbm, zones, ...) terminate, but fail to produce a precise analysis result w.r.t. the boolean variables (e.g., unreachability of certain bbs).
Increasing the table size from 642 to 653
garbage collecting (146083 dead BDD nodes out of 871842, min 149248)... (0 dead ZDD nodes out of 0)... done
rehashing layer 247: keys 1025 dead 1010 new size 512
rehashing layer 248: keys 1025 dead 1010 new size 512
rehashing layer 247: keys 2049 dead 2027 new size 1024
rehashing layer 248: keys 2049 dead 2027 new size 1024
rehashing layer 20: keys 1025 dead 1019 new size 512
rehashing layer 19: keys 1025 dead 1019 new size 512
rehashing layer 20: keys 2049 dead 2046 new size 1024
rehashing layer 19: keys 2049 dead 2046 new size 1024
rehashing layer 238: keys 2049 dead 310 new size 1024
rehashing layer 237: keys 2049 dead 310 new size 1024
rehashing layer 224: keys 2049 dead 341 new size 1024
rehashing layer 223: keys 2049 dead 338 new size 1024
rehashing layer 252: keys 2049 dead 323 new size 1024
rehashing layer 251: keys 2049 dead 323 new size 1024
rehashing layer 436: keys 2049 dead 245 new size 1024
rehashing layer 435: keys 2049 dead 245 new size 1024
rehashing layer 444: keys 1025 dead 184 new size 512
rehashing layer 182: keys 4097 dead 421 new size 2048
rehashing layer 181: keys 4097 dead 421 new size 2048
rehashing layer 178: keys 4097 dead 421 new size 2048
rehashing layer 177: keys 4097 dead 421 new size 2048
rehashing layer 176: keys 4097 dead 421 new size 2048
rehashing layer 175: keys 4097 dead 421 new size 2048
rehashing layer 174: keys 4097 dead 421 new size 2048
rehashing layer 173: keys 4097 dead 421 new size 2048
garbage collecting (166682 dead BDD nodes out of 935917, min 152576)... (0 dead ZDD nodes out of 0)... done
If you want I can attach the encoding of the graph as .cc -- is there a way to export/import a crab cfg / cg, else I have to manually encode it as the above example was generated programmatically.
I've played a little bit with the parameters but that didn't seem to help :/
Unfortunately, there is no a way to export/import crab CFG. I would love to but we don't have it at the moment. However, notice that you can write your program in C and use Clam (https://github.com/seahorn/clam) to produce the Crab CFG. I saw that PLC programs can be translated relatively easy to C. Perhaps it's what you do already. Either way, I would like to look at your program and see if things can be done better although keep in mind that boxes is an expensive domain.
I directly work on the PLC code by using an IR, hence I had to encode the crab CFG manually. Attached you can find the depicted CFG as an executable test case in crab and the original PLC code: crab questions.zip
Do note that I perform a series of transformations such as basic block encoding, three-address code transformation which adds temporary variables temp and a call-transformation pass to follow crab requirements that inputs should be written at the entry and only read afterwards. Also I have an SSA-pass, however, I push the PHI-nodes back into the respective locations after the transformation for crab. This all causes some bloat (in variables), but it is required by the IR of crab, isn't it?
Have you tried in release mode? I think you are trying in debug mode because you mentioned messages like rehasing layer ...
I have a fast machine but I tried in Release mode and boxes finishes in less than one second. Note that printing invariants is also very slow (it took me 17 seconds) but you shouldn't need to print.
Yes I've built and ran crab in debug, however, using the release build (without printing) does not terminate for me either (I've set a timeout of about 10 minutes on openSUSE 15.3, Intel(R) Core(TM) i5-6600K CPU @ 3.50GHz, 16GB DDR3 RAM, SSD for the attached td_inter_10.cc file).
Is there anything I can do to improve my encoding? E.g., remove the cyclic dependency and havoc all initial valuations? I am solely interested in the (un)reachability of basic blocks for my subsequent symbolic execution in order to not manually asses if a basic block is "truly" unreachable.
Are you still delaying widening 100 iterations? If yes, then that's the reason. That won't scale. In my test, I just delayed 1 iteration widening.
The boxes domain is sensitive to the number of "splits" on each variable. Splits come from joins and also from boolean and bitwise operations. So for instance, simplifying the CFG by reducing the number of basic blocks (e.g., similar to what pass cfg-simplify in LLVM compiler does) will help. Simplifying/removing boolean and bitwise operations will also help.
Since you just care about which basic block is definitely unreachable, I would try first to abstract your program by removing (i.e., havocing) statements that cannot affect the control flow of the program. It might be the case that you have complex bitwise operations that boxes will try to model precisely by introducing splits (ie.., disjunctions) but they might be irrelevant to know which blocks are unreachable. If you go in that direction, crab has dataflow analyses that might help. But if all statements can affect the evaluation of all branches then there is no much you can do. Just run boxes with a low widening delay.
I used the default configuration for the parameters in td_inter_10.cc (and even set widening_delay = 1), no success.
inter_analyzer_parameters()
: only_main_as_entry(false), widening_delay(2),
descending_iters(2 /*UINT_MAX*/), thresholds_size(20 /*0*/),
live_map(nullptr), wto_map(nullptr),
run_checker(true), checker_verbosity(0), keep_cc_invariants(false),
keep_invariants(true), max_call_contexts(UINT_MAX),
analyze_recursive_functions(false), exact_summary_reuse(true) {}
The boxes domain is sensitive to the number of "splits" on each variable. Splits come from joins and also from boolean and bitwise operations. So for instance, simplifying the CFG by reducing the number of basic blocks (e.g., similar to what pass cfg-simplify in LLVM compiler does) will help. Simplifying/removing boolean and bitwise operations will also help.
I've tried removing the boolean variables by replacing them with (crab::variable_type_kind::INT_TYPE, 1), however I do not know how to "translate" certain statements. For example, EQUALITY as in bb.bool_assign(variable, lin_exp_t(left_operand_variable) == right_operand_variable); can not be expressed in the "non-boolean" version of assign such as bb.assign(variable, (left_operand_variable - right_operand_variable) = 0), as it requires a linear_expression as argument instead of a linear_constraint. Same goes for, e.g. BOOLEAN_OR, bb.assign(variable, (left_operand_variable + right_operand_variable) > 1) is not expressible and I am also fully aware of why this is not supported ^_^"
Since you just care about which basic block is definitely unreachable, I would try first to abstract your program by removing (i.e., havocing) statements that cannot affect the control flow of the program. It might be the case that you have complex bitwise operations that boxes will try to model precisely by introducing splits (ie.., disjunctions) but they might be irrelevant to know which blocks are unreachable. If you go in that direction, crab has dataflow analyses that might help. But if all statements can affect the evaluation of all branches then there is no much you can do. Just run boxes with a low widening delay.
I've tried and experimented with slicing using RDA/LVA information but it only helps partially -- it does not generalize well due to the cyclic nature of the programs and their inter-dependencies.
I think we can close this discussion, thank you for your help! Unless there is any way I can use a less expensive domain without sacrificing precision w.r.t. (un)reachability (I don't mind intervals being -inf to inf) I don't think I can get much value out of crab, unfortunately :(