How to correctly represent "else" when manually working with `powerset_domain`

[aytey]

Current situation

Following on from #34, I am able to successfully represent something like:

void foo(int y) {
  int w = 0;
  if (y > 10) {
    w = 1;
  } else {
    w = 2;
  }
}

which I can correctly encode and obtain:

{y -> [[11, 2147483647]]_32; w -> [[2, 2]]_32} or
{y -> [[-2147483648, 10]]_32; w -> [[3, 3]]_32}

My code looks like this like:

using z_wrapped_interval_domain = wrapped_interval_domain<z_number, varname_t>;
using powerset_of_z_wrapped_intervals =
    powerset_domain<z_wrapped_interval_domain>;

using analysis_domain = powerset_of_z_wrapped_intervals;

int main(void) {
  variable_factory_t vfac;
  z_var y(vfac["y"], crab::INT_TYPE, 32);
  z_var w(vfac["w"], crab::INT_TYPE, 32);

  analysis_domain start;
  start.assign(w, 0);

  analysis_domain tt_1 = start;
  tt_1 += (y > 10);
  tt_1.assign(w, 1);

  analysis_domain ff_1 = start;
  ff_1 += (y <= 10);
  ff_1.assign(w, 2);

  analysis_domain after1 = tt_1 | ff_1;
  crab::outs() << after1 << "\n\n\n";
 
  return 0;
}

Current issue

However, I am not sure how to encode things when the condition in the false branch is "more complicated":

void foo(int y) {
  int w = 0;
  if (y > 10 && y < 20) {
    w = 1;
  } else {
    w = 2;
  }
}

(notice the if now contains a conjunction)

While encoding the true branch is fine:

  analysis_domain tt_1 = start;
  tt_1 += (y > 10);
  tt_1 += (y < 20);
  tt_1.assign(w, 1);

the false branch is more complicated:

  analysis_domain ff_1 = start;
  ff_1 += (y <= 10);
  ff_1 += (y >= 20);
  ff_1.assign(w, 2);

because it seems that crab says that this is bottom.

Question

What is the best way to represent the negation of a conditional that contains Booleans when working with crab?

Is there a simple way to build up a Boolean expression, and then use that both positively and then negate it (to represent an else)? It is fine if I need to manually build-up the else, but I'm really unsure about how to encode it.

[caballa]

Probably the best way is to split the else branch into two more
branches so the disjunction is handled directly by the join abstract
operator. So what I'm suggesting is to apply the abstract operations
for this equivalent code:

if (y > 10 && y < 20) {
  w=1;
} else if (y <= 10) {
  w=2;
} else if (y >= 20) {
  w=2;
}

Crab has also abstract operations for boolean operations that you can
use them to encode the disjunction of the else branch. So you can also do:

abs_val.assign_cst(b1, y <= 10); // b1 := (y <=10);
abs_val.assign_cst(b2, y >= 10); // b2 := (y >=20); 
abs_val.apply_binary_bool(crab::OP_BOR, b3, b1, b2);  // b3 := b1 or b2;
abs_val.assume_bool(b3, false /*meaning that b3 is not negated*/);

where b1, b2, and b3 are declared as boolean variables:

  z_var b1(vfac["b1"], crab::BOOL_TYPE, 1);
  z_var b2(vfac["b2"], crab::BOOL_TYPE, 1);
  z_var b3(vfac["b3"], crab::BOOL_TYPE, 1);

The problem is that there is no way to get around disjunctions. Most
of the domains will ignore the third abstract operation (i.e., the OR abstract operator).

So if you are using the powerset domain, follow the first approach. If you are ok with non-wrapped intervals, then you can use the boxes domain that represents precisely boolean combinations of interval constraints, and thus, it should be precise with boolean operations, included OR operations.

[aytey]

Ah, okay, I would have never thought about doing that!

I guess for the case when it is a conjunction, you can just create the permutation of possibilities (excluding the true case), and then create a "duplicate branch" for each false evaluation. For disjunction, you could try to enumerate all true/false solutions using something like an ALLSAT solver, and then encode all of these with the corresponding true/false outcome. It would probably be enough just to encode a proposition skeleton to the solver, and then let crab tell you it is bottom if the outcome is "impossible".

I tried to play around with assign_cst, but this seems to work in neither of master or dev :(

[caballa]

Did you tried assign_cst with the boxes domain? The wrapped interval domain completely ignores boolean operations. In crab, there is a reduced product (a pair of domains) of a simple domain for booleans (called flat_boolean_domain) with an arbitrary numerical domain. It's called flat_boolean_numerical_domain. That one does something but nothing really with boolean ORs.

[aytey]

Maybe I'm crazy, but I couldn't even find a definition of that method:

[avj@tempvm master]$ pwd
/home/avj/clones/crab/master
[avj@tempvm master]$ ag "assign_cst\("
include/crab/cfg/cfg.hpp
311:  bool is_bool_assign_cst() const { return (m_stmt_code == BOOL_ASSIGN_CST); }
1527:  bool_assign_cst(variable_t lhs, linear_constraint_t rhs)

[aytey]

(also, I think because I have a "domain" then what's in the cfg namespace won't work for me -- maybe I missed the point 😬 )

[caballa]

Sorry I meant bool_assign_cst.

[aytey]

Do you expect bool_assign_cst to work with:

using z_wrapped_interval_domain = wrapped_interval_domain<z_number, varname_t>;
using powerset_of_z_wrapped_intervals =
    powerset_domain<z_wrapped_interval_domain>;

?

[aytey]

Btw, I didn't ignore:

So if you are using the powerset domain, follow the first approach.

I had just presumed it would work just not with disjunction ...

[caballa]

Do you expect bool_assign_cst to work with:

using z_wrapped_interval_domain = wrapped_interval_domain<z_number, varname_t>;
using powerset_of_z_wrapped_intervals =
    powerset_domain<z_wrapped_interval_domain>;

?

Only flat_boolean_numerical_domain and boxes will do something with bool_assign_cst.
So you can do powerset_domain<flat_boolean_numerical_domain<z_wrapped_interval_domain>>