Question: "range of intervals"

[aytey]

Hi,

I just started playing around with crab (so I am very inexperienced here!) and I wanted to model something like this:

void foo(int x) {
  int y = 0;
  if (x >= 10 && x <= 20) {
    y = x;
  } else if (x >= -20 && x <= -10) {
    y = x;
  } else {
    y = 0;
  }

  // y = ([-20, -10], [0], [10, 20])

  ++y;

  // y = ([-10, -9], [1], [11, 21])
}

Using one of the examples, I got this far:

#include <crab/common/types.hpp>
#include <crab/config.h>
#include <crab/domains/wrapped_interval_domain.hpp>
#include <crab/numbers/wrapint.hpp>
#include <iostream>

using namespace std;
using namespace crab::domains;

typedef wrapped_interval<ikos::z_number> wrapped_interval_t;

int main(void) {
  wrapped_interval_t i1(crab::wrapint(10, 32), crab::wrapint(20, 32));
  wrapped_interval_t i2(crab::wrapint(-10, 32), crab::wrapint(-20, 32));
  crab::outs() << "i1 & i2: " << (i1 & i2) << "\n";
  return 0;
}

but this just seems to expand the domain to be [-20, 20], rather than join the "disjointly" (apologies for wrong terminology) -- that is, what I want is ([-20, -10], [10, 20]).

Is this something I can do with crab or are these just "disjoint intervals" not possible with the library?

Thanks!

[aytey]

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?

[caballa]

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

[aytey]

@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.

[aytey]

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

[caballa]

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

[aytey]

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]].

[aytey]

Urgh! Copy and paste error, I think!

[caballa]

You are adding the constraints to inv1 instead of inv2

[aytey]

You are adding the constraints to inv1 instead of inv2

Yep 🤦

[aytey]

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!

[aytey]

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?

[caballa]

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.

[caballa]

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.

[aytey]

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