Question: "range of intervals" about crab HOT 14 CLOSED

You are adding the constraints to inv1 instead of inv2

from crab.

Okay, so it looks like I can use dis_interval for this, but is there a way to use crab::wrapint (at a certain bit-width) vs. using z_number?

from crab.

It's possible. You can represent disjoint wrapped intervals by using the powerset domain:

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

There is another domain you can use that represents disjunction of classical intervals:

using z_boxes_domain = boxes_domain<z_number, varname_t>;

The powerset construction is very expensive while the boxes domain is usually more more efficient.
The advantage of the powerset domain is that it can be applied to any domain. The boxes domain only works for intervals

from crab.

@caballa thanks!

So I'm trying to cheat here and I'd like to hand-roll some use of the interval domains -- so I'd like to avoid varname_t.

Is this something that's along the right lines:

typedef wrapped_interval<ikos::z_number> wrapped_interval_t;
using powerset_of_z_wrapped_intervals = powerset_domain<wrapped_interval_t>;

int main(void) {
  crab::wrapint start(10, 32);
  crab::wrapint end(20, 32);
  wrapped_interval_t i1(start, end);
  powerset_of_z_wrapped_intervals w(i1); // <-- this doesn't feel right, or compile
  return 0;
}

?

I'm interested in the bit-width-specified "underlying domain", because I'd like these to saturate towards MIN_INT/MAX_INT.

from crab.

Another question: what's the difference between the box/powerset domain and dis_interval domain?

from crab.

The powerset domain takes as parameter another domain. So you cannot use wrapped_interval. you need wrapped_interval_domain. You can use std::string as varname_t

from crab.

Aha!

So does:

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

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

  powerset_of_z_wrapped_intervals inv1;
  inv1 += (y >= 10);
  inv1 += (y <= 20);

  powerset_of_z_wrapped_intervals inv2;
  inv1 += (y >= -20);
  inv1 += (y <= -10);

  powerset_of_z_wrapped_intervals inv3 = inv1 | inv2;
  crab::outs() << inv3 << "\n";

  return 0;
}

look more reasonable to you?

What's weird with this it that it gives top for inv3, when I was really hoping for [[-20, -10], [10, 20]].

from crab.

Urgh! Copy and paste error, I think!

from crab.

You are adding the constraints to inv1 instead of inv2

Yep 🤦

from crab.

Thanks, @caballa -- you really helped!!!

Here's where I ended-up with:

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

  powerset_of_z_wrapped_intervals inv1;
  inv1 += (y >= 10);
  inv1 += (y <= 20);
  inv1.assign(z, y);

  powerset_of_z_wrapped_intervals inv2;
  inv2 += (y >= -20);
  inv2 += (y <= -10);
  inv2.assign(z, y);

  powerset_of_z_wrapped_intervals inv3;
  inv3.assign(z, 0);

  powerset_of_z_wrapped_intervals inv4 = inv1 | inv2 | inv3;
  crab::outs() << inv4 << "\n";
  inv4.apply(OP_MULTIPLICATION, z, z, 1000000000);
  crab::outs() << inv4 << "\n";
  return 0;
}

If you have suggestions for improvement, they're truly welcome!

Two quick questions:

1. When printing an interval to stdout, it there a way to restrict it to one variable? If I do inv4[z], then this seems to completely flatten the range (rather than keeping it as the disjoint sections)

2. The multiplication I've got at the end is showing a weird effect: before doing the multiplication, I have the three ranges for z -- after doing the multiplication, I only have the one for 0. If I multiply by a smaller factor (say, 100000000), then I get three ranges for z. This surprises me, as I expected the value to hit MIN/MAX_INT and "saturate" (or maybe give top).

Thanks again for your help so far!

from crab.

3. weirdly, changing my multiplication to be inv4.apply(OP_MULTIPLICATION, z, z, y); gives top for inv4, and we lose any information on y (even though the multiplication isn't changing y) -- am I missing something?

from crab.

The problem is that you join inv1, inv2, and inv3. The result is in inv4. Then, you multiply z := z * k.
In inv3 the value of z is 0 but in inv1 and inv2 the value of z is top (nothing is known).
Therefore, the join will lose any information of z. This is how the join is supposed to work.

from crab.

The operator[](variable v) returns the projection on v as an interval.
If you just want to project then use the operation project. It takes a vector of variable and project the abstract state on those variables so the output is still an abstract state.

from crab.

Hi @caballa!

Okay, thanks -- I think I'm all good now!

Bit of a learning curve for me (so apologies for the rudimentary questions), but I think I now have my head around what crab does in certain circumstances (e.g., in inv3, y has no constraints, so that's why everything hits top after the multiplication).

Thanks again -- cheers,

Andrew

from crab.