New Object domain

[LinerSu]

Introduce a new object domain based on DSA node and cache operation.

[LinerSu]

@agurfinkel About how object domain compared with VSTTE, I walked through this example.

entry:
  region_init(V_i:region(int));
  region_init(V_x:region(int));
  region_init(V_y:region(int));
  i := make_ref(V_i:region(int),4,as_0);
  x := make_ref(V_x:region(int),4,as_1);
  y := make_ref(V_y:region(int),4,as_2);
  store_to_ref(V_i:region(int),i:ref,0:int32);
  store_to_ref(V_x:region(int),x:ref,1:int32);
  store_to_ref(V_y:region(int),y:ref,0:int32);
  goto bb1;
bb1:
  goto bb1_t,bb1_f;
bb1_t:
  *i:int32 := load_from_ref(V_i:region(int),i:ref);
  assume(*i <= 99);
  goto bb2;
bb2:
  *x:int32 := load_from_ref(V_x:region(int),x:ref);
  *y:int32 := load_from_ref(V_y:region(int),y:ref);
  *x = *x+*y;
  store_to_ref(V_x:region(int),x:ref,*x:int32);
  *y:int32 := load_from_ref(V_y:region(int),y:ref);
  *y = *y+1;
  store_to_ref(V_y:region(int),y:ref,*y:int32);
  *i:int32 := load_from_ref(V_i:region(int),i:ref);
  *i = *i+1;
  store_to_ref(V_i:region(int),i:ref,*i:int32);
  goto bb2_end;
bb2_end:
  goto bb1;
bb1_f:
  *i:int32 := load_from_ref(V_i:region(int),i:ref);
  assume(-*i <= -100);
  goto bb3;
bb3:
  *x:int32 := load_from_ref(V_x:region(int),x:ref);
  *y:int32 := load_from_ref(V_y:region(int),y:ref);
  goto ret;
ret:
  assert(-*x+*y <= 0);

I use splitDBM for region domain and object domain, the VSTTE can prove assertion in ret block. The object domain does not. The invariants for object domain are:

entry={}
bb1=Base = {i-objA<=0, x-objA<=4, y-objA<=8, objA-i<=0, x-i<=4, y-i<=8, objA-x<=-4, i-x<=-4, y-x<=4, x-y<=-4, objA-y<=-8, i-y<=-8},
Object( V_i V_x V_y ) = {V_i -> [0, +oo], V_x -> [1, +oo], V_y -> [0, +oo]}

bb1_f=Base = {i-objA<=0, x-objA<=4, y-objA<=8, objA-i<=0, x-i<=4, y-i<=8, objA-x<=-4, i-x<=-4, y-x<=4, x-y<=-4, objA-y<=-8, i-y<=-8},
Object( V_i V_x V_y ) = {V_i -> [0, +oo], V_x -> [1, +oo], V_y -> [0, +oo]}

bb3=Base = {*i -> [100, +oo], i-objA<=0, x-objA<=4, y-objA<=8, objA-i<=0, x-i<=4, y-i<=8, objA-x<=-4, i-x<=-4, y-x<=4, x-y<=-4, objA-y<=-8, i-y<=-8},
Object( V_i V_x V_y ) = {V_i -> [0, +oo], V_x -> [1, +oo], V_y -> [0, +oo]}

ret=Base = {*i -> [100, +oo], *x -> [1, +oo], *y -> [0, +oo], i-objA<=0, x-objA<=4, y-objA<=8, objA-i<=0, x-i<=4, y-i<=8, objA-x<=-4, i-x<=-4, y-x<=4, x-y<=-4, objA-y<=-8, i-y<=-8},
Object( V_i V_x V_y ) = {V_i -> [0, +oo], V_x -> [1, +oo], V_y -> [0, +oo]}

bb1_t=Base = {i-objA<=0, x-objA<=4, y-objA<=8, objA-i<=0, x-i<=4, y-i<=8, objA-x<=-4, i-x<=-4, y-x<=4, x-y<=-4, objA-y<=-8, i-y<=-8},
Object( V_i V_x V_y ) = {V_i -> [0, +oo], V_x -> [1, +oo], V_y -> [0, +oo]}

bb2=Base = {*i -> [0, 99], i-objA<=0, x-objA<=4, y-objA<=8, objA-i<=0, x-i<=4, y-i<=8, objA-x<=-4, i-x<=-4, y-x<=4, x-y<=-4, objA-y<=-8, i-y<=-8},
Object( V_i V_x V_y ) = {V_i -> [0, +oo], V_x -> [1, +oo], V_y -> [0, +oo]}

Here, we lost V_i == V_x in fields domain or *i == *x in base domain. One reason I think is we lost V_i == *i and V_x == *x because the load_ref or store_ref is assigning intervals instead of keeping equality in a domain.

[agurfinkel]

@LinerSu looks cool. At this point, I only care about performance. Precision is expected to be very low.

[igcontreras]

It seems that you are adding new commits by @caballa and others to master, can you update so that we only see the changes of your commits in the review?