Comments (7)
caballa
commented on July 24, 2024
Hi Marco,
Thanks for trying Crab!
Yes, the flat boolean numerical domain is not precise enough for this example. This example requires to split on the value of P.activate_1003 and the flat boolean domain does not split. For this example, you should try the boxes domain. This domain is a precise disjunctive interval domain that can be also fully precise on Boolean operations.
Btw, I think you mean that bb_6 is reachable but the statement assume(not(P.temp_3)) should evaluate to false.
I've split b6 in two blocks (b6 and b6.2) so that we can see when the abstract state becomes bottom. The goal is that the invariants at the entry of b6.2 should be bottom (i.e., unreachable):
entry:
havoc(P.activate_1003);
goto b1;
b1:
P.v_bool_1001 = true;
P.b_1002 = P.v_bool_1001;
goto b2;
b2:
P.temp_0 = not(P.activate_1003);
P.temp_1 = P.temp_0&P.b_1002;
goto b3,b4;
b3:
assume(P.temp_1);
P.v_int_1004 = 0;
P.y_1005 = P.v_int_1004;
goto exit;
exit:
b4:
assume(not(P.temp_1));
P.temp_2 = not(P.b_1002);
P.temp_3 = P.activate_1003|P.temp_2;
goto b5,b6;
b5:
assume(P.temp_3);
P.v_int_1006 = 1;
P.y_1007 = P.v_int_1006;
goto exit;
b6:
assume(not(P.temp_3));
P.v_int_1008 = 2;
P.y_1009 = P.v_int_1008;
goto b6.2;
b6.2: // we want to see this block being unreachable
goto exit;
These are the invariants with the boxes domain:
entry={}
b1={}
b2={-P.v_bool_1001 <= -1; P.v_bool_1001 <= 1; -P.b_1002 <= -1; P.b_1002 <= 1}
b4={-P.v_bool_1001 <= -1; P.v_bool_1001 <= 1; -P.b_1002 <= -1; P.b_1002 <= 1; -P.activate_1003 <= -1; P.activate_1003 <= 1; -P.temp_0 <= 0; P.temp_0 <= 0; -P.temp_1 <= 0; P.temp_1 <= 0} or
{-P.v_bool_1001 <= -1; P.v_bool_1001 <= 1; -P.b_1002 <= -1; P.b_1002 <= 1; -P.activate_1003 <= 0; P.activate_1003 <= 0; -P.temp_0 <= -1; P.temp_0 <= 1; -P.temp_1 <= -1; P.temp_1 <= 1}
b6={-P.v_bool_1001 <= -1; P.v_bool_1001 <= 1; -P.b_1002 <= -1; P.b_1002 <= 1; -P.activate_1003 <= -1; P.activate_1003 <= 1; -P.temp_0 <= 0; P.temp_0 <= 0; -P.temp_1 <= 0; P.temp_1 <= 0; -P.temp_2 <= 0; P.temp_2 <= 0; -P.temp_3 <= -1; P.temp_3 <= 1}
b6.2=_|_
exit={-P.v_bool_1001 <= -1; P.v_bool_1001 <= 1; -P.b_1002 <= -1; P.b_1002 <= 1; -P.activate_1003 <= -1; P.activate_1003 <= 1; -P.temp_0 <= 0; P.temp_0 <= 0; -P.temp_1 <= 0; P.temp_1 <= 0; -P.temp_2 <= 0; P.temp_2 <= 0; -P.temp_3 <= -1; P.temp_3 <= 1; -P.v_int_1006 <= -1; P.v_int_1006 <= 1; -P.y_1007 <= -1; P.y_1007 <= 1} or
{-P.v_bool_1001 <= -1; P.v_bool_1001 <= 1; -P.b_1002 <= -1; P.b_1002 <= 1; -P.activate_1003 <= 0; P.activate_1003 <= 0; -P.temp_0 <= -1; P.temp_0 <= 1; -P.temp_1 <= -1; P.temp_1 <= 1; -P.v_int_1004 <= 0; P.v_int_1004 <= 0; -P.y_1005 <= 0; P.y_1005 <= 0}
b5={-P.v_bool_1001 <= -1; P.v_bool_1001 <= 1; -P.b_1002 <= -1; P.b_1002 <= 1; -P.activate_1003 <= -1; P.activate_1003 <= 1; -P.temp_0 <= 0; P.temp_0 <= 0; -P.temp_1 <= 0; P.temp_1 <= 0; -P.temp_2 <= 0; P.temp_2 <= 0; -P.temp_3 <= -1; P.temp_3 <= 1}
b3={-P.v_bool_1001 <= -1; P.v_bool_1001 <= 1; -P.b_1002 <= -1; P.b_1002 <= 1; -P.activate_1003 <= -1; P.activate_1003 <= 1; -P.temp_0 <= 0; P.temp_0 <= 0; -P.temp_1 <= 0; P.temp_1 <= 0} or
{-P.v_bool_1001 <= -1; P.v_bool_1001 <= 1; -P.b_1002 <= -1; P.b_1002 <= 1; -P.activate_1003 <= 0; P.activate_1003 <= 0; -P.temp_0 <= -1; P.temp_0 <= 1; -P.temp_1 <= -1; P.temp_1 <= 1}
So, you can see that the invariant for b6.2 is bottom.
Let me know if I'm missing something.
from crab.
MarcoGrochowski
commented on July 24, 2024
Hey Jorge,
thank you for your quick response! My git submodule was behind commit 55757a1, but I figured it out now and can reproduce the same invariants using the boxes domain, thanks! I also appreciate the convenient bool_assign_not(), however just to nitpick I would rename it to bool_not_assign() to be consistent with bool_assume() / bool_not_assume().
Yes, I meant the unreachability of the false branch in bb_6, sorry for the unclarity. Is it in general a good idea to instrument the crab cfg to use these intermediate basic blocks?
How do I extract the invariants to use them as asserts?
I tested the boxes domain on bigger benchmarks -- currently I struggle a little bit because there are some phi expressions over integers, which I pushed into the predecessors. Somehow the following reduced example gives me incorrect information with the boxes domain, where did I go wrong with the encoding?
The SSA encoding:
TAC'ed with pushed PHI assignments:
Marshalled crab CFG:
cycle_entry:
havoc(cycle);
goto entry;
entry:
assume(cycle);
havoc(P.Activate_1001);
goto bb_1;
bb_1:
P.temp_0 = not(P.Activate_1001);
P.DiagCode_1008 = P.DiagCode_1004;
goto bb_2,bb_3;
bb_2:
assume(P.temp_0);
P.v_int_1002 = 0;
P.DiagCode_1003 = P.v_int_1002;
P.DiagCode_1008 = P.DiagCode_1003;
goto bb_6;
bb_6:
assume(not(P.temp_1));
assume(not(P.Activate_1001));
P.v_int_1009 = 0;
P.temp_2 = (P.DiagCode_1008-P.v_int_1009 = 0);
goto bb_7,bb_9;
bb_7:
assume(P.temp_2);
P.v_bool_1010 = false;
P.Ready_1011 = P.v_bool_1010;
goto bb_8;
bb_8:
P.v_bool_1012 = false;
P.S_TwoHandOut_1013 = P.v_bool_1012;
goto exit;
exit:
assume(not(P.temp_4));
goto entry,cycle_exit;
cycle_exit:
assume(not(cycle));
bb_9:
assume(not(P.temp_2));
P.v_int_1014 = 32768;
P.temp_3 = (P.DiagCode_1008-P.v_int_1014 = 0);
goto bb_10,bb_12;
bb_10:
assume(P.temp_3);
P.v_bool_1015 = true;
P.Ready_1016 = P.v_bool_1015;
goto bb_11;
bb_11:
P.v_bool_1017 = true;
P.S_TwoHandOut_1018 = P.v_bool_1017;
goto exit;
bb_12:
assume(not(P.temp_3));
P.v_int_1019 = 32769;
P.temp_4 = (P.DiagCode_1008-P.v_int_1019 = 0);
goto bb_13,exit;
bb_13:
assume(P.temp_4);
P.v_bool_1020 = true;
P.Ready_1021 = P.v_bool_1020;
goto bb_14;
bb_14:
P.v_bool_1022 = false;
P.S_TwoHandOut_1023 = P.v_bool_1022;
goto exit;
bb_3:
assume(not(P.temp_0));
P.v_int_1005 = 0;
P.temp_1 = (P.DiagCode_1004-P.v_int_1005 = 0);
goto bb_4,bb_6;
bb_4:
assume(P.temp_1);
goto bb_5,bb_6;
bb_5:
assume(P.Activate_1001);
P.v_int_1006 = 32769;
P.DiagCode_1007 = P.v_int_1006;
P.DiagCode_1008 = P.DiagCode_1007;
goto bb_6;
For reproduction, I also added code that can be reused to execut the resulting encoding:
variable_factory_t vfac;
var_t temp_0(vfac["temp_0"], crab::BOOL_TYPE);
var_t temp_1(vfac["temp_1"], crab::BOOL_TYPE);
var_t temp_2(vfac["temp_2"], crab::BOOL_TYPE);
var_t temp_3(vfac["temp_3"], crab::BOOL_TYPE);
var_t temp_4(vfac["temp_4"], crab::BOOL_TYPE);
var_t Activate_1001(vfac["Activate_1001"], crab::BOOL_TYPE);
var_t DiagCode_1003(vfac["DiagCode_1003"], crab::INT_TYPE, 32);
var_t DiagCode_1004(vfac["DiagCode_1004"], crab::INT_TYPE, 32);
var_t DiagCode_1007(vfac["DiagCode_1007"], crab::INT_TYPE, 32);
var_t DiagCode_1008(vfac["DiagCode_1008"], crab::INT_TYPE, 32);
var_t v_int_1002(vfac["v_int_1002"], crab::INT_TYPE, 32);
var_t v_int_1005(vfac["v_int_1005"], crab::INT_TYPE, 32);
var_t v_int_1006(vfac["v_int_1006"], crab::INT_TYPE, 32);
var_t v_int_1009(vfac["v_int_1009"], crab::INT_TYPE, 32);
var_t v_int_1014(vfac["v_int_1014"], crab::INT_TYPE, 32);
var_t v_int_1019(vfac["v_int_1019"], crab::INT_TYPE, 32);
var_t v_bool_1010(vfac["v_bool_1010"], crab::BOOL_TYPE);
var_t v_bool_1012(vfac["v_bool_1012"], crab::BOOL_TYPE);
var_t v_bool_1015(vfac["v_bool_1015"], crab::BOOL_TYPE);
var_t v_bool_1017(vfac["v_bool_1017"], crab::BOOL_TYPE);
var_t v_bool_1020(vfac["v_bool_1020"], crab::BOOL_TYPE);
var_t v_bool_1022(vfac["v_bool_1022"], crab::BOOL_TYPE);
var_t Ready_1011(vfac["Ready_1011"], crab::BOOL_TYPE);
var_t Ready_1016(vfac["Ready_1016"], crab::BOOL_TYPE);
var_t Ready_1021(vfac["Ready_1021"], crab::BOOL_TYPE);
var_t S_TwoHandOut_1013(vfac["S_TwoHandOut_1013"], crab::BOOL_TYPE);
var_t S_TwoHandOut_1018(vfac["S_TwoHandOut_1018"], crab::BOOL_TYPE);
var_t S_TwoHandOut_1023(vfac["S_TwoHandOut_1023"], crab::BOOL_TYPE);
cfg_t prog("entry", "exit");
basic_block_t& entry = prog.insert("entry");
basic_block_t& L1 = prog.insert("L1");
basic_block_t& L2 = prog.insert("L2");
basic_block_t& L3 = prog.insert("L3");
basic_block_t& L4 = prog.insert("L4");
basic_block_t& L5 = prog.insert("L5");
basic_block_t& L6 = prog.insert("L6");
basic_block_t& L7 = prog.insert("L7");
basic_block_t& L8 = prog.insert("L8");
basic_block_t& L9 = prog.insert("L9");
basic_block_t& L10 = prog.insert("L10");
basic_block_t& L11 = prog.insert("L11");
basic_block_t& L12 = prog.insert("L12");
basic_block_t& L13 = prog.insert("L13");
basic_block_t& L14 = prog.insert("L14");
basic_block_t& exit = prog.insert("exit");
entry.add_succ(L1);
L1.add_succ(L2);
L1.add_succ(L3);
L2.add_succ(L6);
L3.add_succ(L4);
L3.add_succ(L6);
L4.add_succ(L5);
L4.add_succ(L6);
L5.add_succ(L6);
L6.add_succ(L7);
L6.add_succ(L9);
L7.add_succ(L8);
L8.add_succ(exit);
L9.add_succ(L10);
L9.add_succ(L12);
L10.add_succ(L11);
L11.add_succ(exit);
L12.add_succ(L13);
L12.add_succ(exit);
L13.add_succ(L14);
L14.add_succ(exit);
entry.havoc(Activate_1001);
// L1
L1.bool_assign_not(temp_0, Activate_1001);
L1.assign(DiagCode_1008, DiagCode_1004);
L2.bool_assume(temp_0);
L3.bool_not_assume(temp_0);
// L2
L2.assign(v_int_1002, 0);
L2.assign(DiagCode_1003, v_int_1002);
L2.assign(DiagCode_1008, DiagCode_1003);
// L3
L3.assign(v_int_1005, 0);
L3.bool_assign(temp_1, lin_exp_t(DiagCode_1004) == v_int_1005);
L4.bool_assume(temp_1);
L6.bool_not_assume(temp_1);
// L4
L5.bool_assume(Activate_1001);
L6.bool_not_assume(Activate_1001);
// L5
L5.assign(v_int_1006, 32769);
L5.assign(DiagCode_1007, v_int_1006);
L5.assign(DiagCode_1008, DiagCode_1007);
L5.assign(DiagCode_1008, v_int_1006);
// L6
L6.assign(v_int_1009, 0);
L6.bool_assign(temp_2, lin_exp_t(DiagCode_1008) == v_int_1009);
L7.bool_assume(temp_2);
L9.bool_not_assume(temp_2);
// L7
L7.bool_assign(v_bool_1010, lin_cst_t::get_false());
L7.bool_assign(Ready_1011, v_bool_1010);
// L8
L8.bool_assign(v_bool_1012, lin_cst_t::get_false());
L8.bool_assign(S_TwoHandOut_1013, v_bool_1012);
// L9
L9.assign(v_int_1014, 32768);
L9.bool_assign(temp_3, lin_exp_t(DiagCode_1008) == v_int_1014);
L10.bool_assume(temp_3);
L12.bool_not_assume(temp_3);
// L10
L10.bool_assign(v_bool_1015, lin_cst_t::get_true());
L10.bool_assign(Ready_1016, v_bool_1015);
// L11
L11.bool_assign(v_bool_1017, lin_cst_t::get_true());
L11.bool_assign(S_TwoHandOut_1018, v_bool_1017);
// L12
L12.assign(v_int_1019, 32769);
L12.bool_assign(temp_4, lin_exp_t(DiagCode_1008) == v_int_1019);
L13.bool_assume(temp_4);
exit.bool_not_assume(temp_4);
// L13
L13.bool_assign(v_bool_1020, lin_cst_t::get_true());
L13.bool_assign(Ready_1021, v_bool_1020);
// L14
L14.bool_assign(v_bool_1022, lin_cst_t::get_false());
L14.bool_assign(S_TwoHandOut_1023, v_bool_1022);
crab::outs() << prog << "\n";
auto print_invariants = [&prog](const fwd_analyzer_t &analyzer) {
for (auto &bb : prog) {
std::string bb_name = bb.label();
auto inv = analyzer.get_pre(bb_name);
crab::outs() << bb_name << ":" << inv << "\n";
}
};
z_boxes_domain_t bd;
unsigned widening_delay = 1;
unsigned narrowing_iterations = 1;
fwd_analyzer_t analyzer(prog, bd, nullptr, nullptr,
widening_delay, narrowing_iterations, 0);
analyzer.run();
crab::outs() << "Invariants using bool intervals\n";
print_invariants(analyzer);
Which results in the following invariants for me:
cycle_exit:{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= 0; P.Activate_1001 <= 0; -P.temp_0 <= -1; P.temp_0 <= 1; -P.temp_1 <= 0; P.temp_1 <= 0; -P.DiagCode_1008 <= 0; P.DiagCode_1008 <= 0; -P.v_int_1002 <= 0; P.v_int_1002 <= 0; -P.DiagCode_1003 <= 0; P.DiagCode_1003 <= 0; -P.v_int_1009 <= 0; P.v_int_1009 <= 0; -P.temp_2 <= -1; P.temp_2 <= 1; -P.v_bool_1010 <= 0; P.v_bool_1010 <= 0; -P.Ready_1011 <= 0; P.Ready_1011 <= 0; -P.v_bool_1012 <= 0; P.v_bool_1012 <= 0; -P.S_TwoHandOut_1013 <= 0; P.S_TwoHandOut_1013 <= 0; -P.temp_4 <= 0; P.temp_4 <= 0}
bb_13:_|_
entry:{}
exit:{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= 0; P.Activate_1001 <= 0; -P.temp_0 <= -1; P.temp_0 <= 1; -P.temp_1 <= 0; P.temp_1 <= 0; -P.DiagCode_1008 <= 0; P.DiagCode_1008 <= 0; -P.v_int_1002 <= 0; P.v_int_1002 <= 0; -P.DiagCode_1003 <= 0; P.DiagCode_1003 <= 0; -P.v_int_1009 <= 0; P.v_int_1009 <= 0; -P.temp_2 <= -1; P.temp_2 <= 1; -P.v_bool_1010 <= 0; P.v_bool_1010 <= 0; -P.Ready_1011 <= 0; P.Ready_1011 <= 0; -P.v_bool_1012 <= 0; P.v_bool_1012 <= 0; -P.S_TwoHandOut_1013 <= 0; P.S_TwoHandOut_1013 <= 0}
bb_8:{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= 0; P.Activate_1001 <= 0; -P.temp_0 <= -1; P.temp_0 <= 1; -P.temp_1 <= 0; P.temp_1 <= 0; -P.DiagCode_1008 <= 0; P.DiagCode_1008 <= 0; -P.v_int_1002 <= 0; P.v_int_1002 <= 0; -P.DiagCode_1003 <= 0; P.DiagCode_1003 <= 0; -P.v_int_1009 <= 0; P.v_int_1009 <= 0; -P.temp_2 <= -1; P.temp_2 <= 1; -P.v_bool_1010 <= 0; P.v_bool_1010 <= 0; -P.Ready_1011 <= 0; P.Ready_1011 <= 0}
cycle_entry:{}
bb_1:{-cycle <= -1; cycle <= 1}
bb_9:{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= 0; P.Activate_1001 <= 0; -P.temp_0 <= -1; P.temp_0 <= 1; -P.temp_1 <= 0; P.temp_1 <= 0; -P.DiagCode_1008 <= 0; P.DiagCode_1008 <= 0; -P.v_int_1002 <= 0; P.v_int_1002 <= 0; -P.DiagCode_1003 <= 0; P.DiagCode_1003 <= 0; -P.v_int_1009 <= 0; P.v_int_1009 <= 0; -P.temp_2 <= -1; P.temp_2 <= 1}
bb_4:{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= -1; P.Activate_1001 <= 1; -P.temp_0 <= 0; P.temp_0 <= 0; -P.v_int_1005 <= 0; P.v_int_1005 <= 0; -P.DiagCode_1004 <= -1; -P.temp_1 <= 0; P.temp_1 <= 0} or
{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= -1; P.Activate_1001 <= 1; -P.temp_0 <= 0; P.temp_0 <= 0; -P.v_int_1005 <= 0; P.v_int_1005 <= 0; -P.DiagCode_1004 <= 0; P.DiagCode_1004 <= 0; -P.temp_1 <= -1; P.temp_1 <= 1} or
{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= -1; P.Activate_1001 <= 1; -P.temp_0 <= 0; P.temp_0 <= 0; -P.v_int_1005 <= 0; P.v_int_1005 <= 0; P.DiagCode_1004 <= -1; -P.temp_1 <= 0; P.temp_1 <= 0}
bb_14:_|_
bb_12:_|_
bb_3:{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= -1; P.Activate_1001 <= 1; -P.temp_0 <= 0; P.temp_0 <= 0} or
{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= 0; P.Activate_1001 <= 0; -P.temp_0 <= -1; P.temp_0 <= 1}
bb_2:{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= -1; P.Activate_1001 <= 1; -P.temp_0 <= 0; P.temp_0 <= 0} or
{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= 0; P.Activate_1001 <= 0; -P.temp_0 <= -1; P.temp_0 <= 1}
bb_7:{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= 0; P.Activate_1001 <= 0; -P.temp_0 <= -1; P.temp_0 <= 1; -P.temp_1 <= 0; P.temp_1 <= 0; -P.DiagCode_1008 <= 0; P.DiagCode_1008 <= 0; -P.v_int_1002 <= 0; P.v_int_1002 <= 0; -P.DiagCode_1003 <= 0; P.DiagCode_1003 <= 0; -P.v_int_1009 <= 0; P.v_int_1009 <= 0; -P.temp_2 <= -1; P.temp_2 <= 1}
bb_5:{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= -1; P.Activate_1001 <= 1; -P.temp_0 <= 0; P.temp_0 <= 0; -P.v_int_1005 <= 0; P.v_int_1005 <= 0; -P.DiagCode_1004 <= 0; P.DiagCode_1004 <= 0; -P.temp_1 <= -1; P.temp_1 <= 1}
bb_11:_|_
bb_6:{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= -1; P.Activate_1001 <= 1; -P.temp_0 <= 0; P.temp_0 <= 0; -P.v_int_1005 <= 0; P.v_int_1005 <= 0; -P.DiagCode_1004 <= -1; -P.temp_1 <= 0; P.temp_1 <= 0} or
{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= -1; P.Activate_1001 <= 1; -P.temp_0 <= 0; P.temp_0 <= 0; -P.v_int_1005 <= 0; P.v_int_1005 <= 0; -P.DiagCode_1004 <= 0; P.DiagCode_1004 <= 0; -P.temp_1 <= -1; P.temp_1 <= 1} or
{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= -1; P.Activate_1001 <= 1; -P.temp_0 <= 0; P.temp_0 <= 0; -P.v_int_1005 <= 0; P.v_int_1005 <= 0; P.DiagCode_1004 <= -1; -P.temp_1 <= 0; P.temp_1 <= 0} or
{-cycle <= -1; cycle <= 1; -P.Activate_1001 <= 0; P.Activate_1001 <= 0; -P.temp_0 <= -1; P.temp_0 <= 1; -P.DiagCode_1008 <= 0; P.DiagCode_1008 <= 0; -P.v_int_1002 <= 0; P.v_int_1002 <= 0; -P.DiagCode_1003 <= 0; P.DiagCode_1003 <= 0}
bb_10:_|_
What bothers me is bb_12:_|_, bb_13:_|_ and bb_14:_|_, any ideas?
from crab.
caballa
commented on July 24, 2024
What do you mean by
Is it in general a good idea to instrument the crab cfg to use these intermediate basic blocks?
How do I extract the invariants to use them as asserts?
Do you mean printing invariants before/after each statement?
from crab.
caballa
commented on July 24, 2024
These are the invariants at different locations in L6:
L6:
{ Activate_1001 = 1; temp_0 = 0 ; v_int_1005 = 0; DiagCode_1004 >= 1; temp_1 = 0; } or // L3 -> L6
{ Activate_1001 = 1; temp_0 = 0; v_int_1005 = 0; DiagCode_1004 = 0; temp_1 = 1} or // L4 -> L6
{ Activate_1001 = 1; temp_0 = 0; v_int_1005 = 0; DiagCode_1004 <= -1; temp_1 = 0;} or // L5 -> L6
{ Activate_1001 = 0; temp_0 = 1; DiagCode_1008 = 0; v_int_1002 = 0; DiagCode_1003 = 0} // from L2 -> L6
assume(not(temp_1));
assume(not(Activate_1001));
{ Activate_1001 = 0; temp_0 = 1; DiagCode_1008 = 0; v_int_1002 = 0; DiagCode_1003 = 0}
v_int_1009 = 0;
temp_2 = (DiagCode_1008 == 0);
{ Activate_1001 = 0; temp_0 = 1; DiagCode_1008 = 0; v_int_1002 = 0; DiagCode_1003 = 0; ; temp_2 == 1}
goto L7,L9;
L9:
{ Activate_1001 = 0; temp_0 = 1; DiagCode_1008 = 0; v_int_1002 = 0; DiagCode_1003 = 0; ; temp_2 = 1}
assume(not(temp_2)); // this evaluates to false because temp_2 = 1
// so the rest is bottom
Note that L6 is reachable from L2, L3, L4, and L5. If L6 is reachable
from L3,L4 or L5 then Activate must be true. At L6 we have
assume(not(Activate_1001)). So if an execution reaches the end of L6
then it must be the case that only the edge from L2 to L6 is feasible
killing the other ones. So I think the invariants are ok wrt to the crab program.
Take a look at the those labels L2-L6 to see if there is something wrong in
your translation to Crab or perphaps the original program has the same
behavior?
from crab.
MarcoGrochowski
commented on July 24, 2024
What do you mean by
Is it in general a good idea to instrument the crab cfg to use these intermediate basic blocks? How do I extract the invariants to use them as asserts?
Do you mean printing invariants before/after each statement?
Adding intermediate basic blocks after each branch, such as b.6_1 for the true branch and b.6_2 for the false branch which only hold the respective assumes and a goto to the succeeding basic blocks.
I would like to retrieve the values of the boxes, such as -Activate_1001 <= -1; Activate_1001 <= 1; to annotate my cfg representation or at least retrieve the information that at a certain location the invariant is _|_. Will naively accessing the invariant returned by analyzer.get_pre(...) using the operator[] suffice? Sometimes it seems to be too imprecise because the invariant can not be captured by one interval. The ultimate goal is to use the static analysis as a pre-analysis for symbolic execution to facilitate the detection of unreachable branches
These are the invariants at different locations in
L6:L6: { Activate_1001 = 1; temp_0 = 0 ; v_int_1005 = 0; DiagCode_1004 >= 1; temp_1 = 0; } or // L3 -> L6 { Activate_1001 = 1; temp_0 = 0; v_int_1005 = 0; DiagCode_1004 = 0; temp_1 = 1} or // L4 -> L6 { Activate_1001 = 1; temp_0 = 0; v_int_1005 = 0; DiagCode_1004 <= -1; temp_1 = 0;} or // L5 -> L6 { Activate_1001 = 0; temp_0 = 1; DiagCode_1008 = 0; v_int_1002 = 0; DiagCode_1003 = 0} // from L2 -> L6 assume(not(temp_1)); assume(not(Activate_1001)); { Activate_1001 = 0; temp_0 = 1; DiagCode_1008 = 0; v_int_1002 = 0; DiagCode_1003 = 0} v_int_1009 = 0; temp_2 = (DiagCode_1008 == 0); { Activate_1001 = 0; temp_0 = 1; DiagCode_1008 = 0; v_int_1002 = 0; DiagCode_1003 = 0; ; temp_2 == 1} goto L7,L9; L9: { Activate_1001 = 0; temp_0 = 1; DiagCode_1008 = 0; v_int_1002 = 0; DiagCode_1003 = 0; ; temp_2 = 1} assume(not(temp_2)); // this evaluates to false because temp_2 = 1 // so the rest is bottomNote that
L6is reachable fromL2,L3,L4, andL5. IfL6is reachable
fromL3,L4orL5thenActivatemust be true. AtL6we have
assume(not(Activate_1001)). So if an execution reaches the end ofL6
then it must be the case that only the edge fromL2toL6is feasible
killing the other ones. So I think the invariants are ok wrt to the crab program.Take a look at the those labels
L2-L6to see if there is something wrong in
your translation to Crab or perphaps the original program has the same
behavior?
Thank you! You are right about crab's output being correct w.r.t to my encoding and that my encoding is simply wrong. The depicted cfg and the reason for the multiple predecessors in L6 is due to a lowering of switch/case statements to if statements. I made a mistake by collecting all assumes from its predecessors at the merge point L6. Your response got me thinking whether I should in general instrument the program by adding an intermediate block holding the branch condition between the source and the destination of the respective edge. When doing so, I get the correct invariants for each basic block when additionally also constraining the values for some variables in my example, thank you :)!
from crab.
caballa
commented on July 24, 2024
Great!
Yes, the operator[] will return an interval so it will lose precision for boxes.
What you want is to use the project operation that doesn't lose precision (i.e., keep the disjunctions).
from crab.
MarcoGrochowski
commented on July 24, 2024
Thank you very much, I really appreciate the help!
from crab.
Related Issues (20)
- Add widening with thresholds in apron domains
- g++-8: HOT 4
- Make generic weights of adaptative sparse graph
- More precise bitwise AND HOT 1
- Valgrind warnings HOT 1
- none-optional dereference on array-expansion domain with elina-pk HOT 3
- Elina does not compile on mac: `'stdlib.h' file not found` HOT 4
- Enhance top-down inter-procedural analysis HOT 1
- CMake Options
- Does crab support running on MacOS? HOT 8
- Reaching Definitions Analysis HOT 5
- Question: "range of intervals" HOT 14
- How to correctly represent "else" when manually working with `powerset_domain` HOT 9
- Compiler warning with `dev` HOT 1
- "compress" `powerset_domain` domain after projection HOT 4
- General question on "backward_assign_operations" HOT 1
- Create tree expressions and adapt abstract domains to use them
- Question regarding "cyclic" encoding and propagation of analysis results HOT 9
- What is the difference between the wrapped_interval implemented in crab and the one implemented in TOPLAS15 paper? HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from crab.