Global variables subsumption

[rasoolmaghareh]

Considering our discussion yesterday, this is my suggestion for the algorithm of Global variables subsumption.

Assuming we are storing a subset of Pi, Mu and G, at the point of creating an interpolant:

1. A global variable a is added to G only if:

• It is the reason for an infeasibility.

• It does not appear in Mu.

  2. The parent nodes should be notified to add a to G as well.

Note: Since a is not in Mu, we know that the value of a has not changed in this path from the beginning.

At the subsumption point, we need to check if all the variables in G have the same value in the new state:

1. The variables might be in Mu at the subsumption point.
2. Or they may be in the GlobalVars data structure.

[rasoolmaghareh]

I am adding @sanghu1790 as the reviewer for this issue to check if the enhancement remains scalable on his test programs.

[xuanlinhha]

I think for some nodes, we cannot get the global values for the interpolant. For example, at 1 one node where infeasible happens because of global variable a, there are 2 possible cases for the current node:

1. a is not in miu => For this case, we can get value of a from Klee's structure and the same value of a needs to be added to G in parent nodes
2. a is already in miu => add the current value of a to G of the current node, but for the parent nodes, if a is not in miu, what is the value of a need to be added to G at those parent nodes? We don't keep those values.

The GlobalVars contains the addresses only, its value may be changed during execution, and we don't keep initial value of global variables.

[rasoolmaghareh]

For case 2, since a is in Mu there is no need to add a to G. However, for the parent nodes there are two possibilities:

1. a is not in Mu of the parent node, then add the value of a from GlobalVars to G.
2. a is in the Mu of the parent node, then no need to add a to G

And the same for the remainder of the parents.

[xuanlinhha]

But for the first case in your comment, the value in GlobalVars it is the updated value, I think that is not correct one @rasoolmaghareh

[rasoolmaghareh]

For the first case if a was changed then we would have a row in Mu for it.

[xuanlinhha]

but in the first case in your comment here: https://github.com/tracer-x/klee/issues/371#issuecomment-638610922 a is not in miu of the parent node. And a in GlobalVars is now the updated valued, that is not correct, the value need to be add to G of that node is the initial value of global variable but we don't keep those values

[xuanlinhha]

DP2-noswloop.c.txt

[rasoolmaghareh]

#include<stdio.h>
#include <klee/klee.h>

int l[2] = {0,0}, r[2] = {0,0};
// int l[2] , r[2];
int main() {
  // l[0] = l[1] = r[0] = r[1] = 0;
  int c1;
  klee_make_symbolic(&c1, sizeof(int), "c1");
  if(c1 == 0) {
    if (!r[1])
    {
      l[0] = 1; 
    }
  }
  else if(c1 == 1) {
    if (!l[1])
    {
      r[0] = 1;
    }
  }
  else if(c1 == 2) {
    if (l[0] == 1 && r[0] == 1)
    { 
      klee_assert(0);
    }
  }

  int c2;
  klee_make_symbolic(&c2, sizeof(int), "c2");
  if(c2 == 0) {
    if (!r[1])
    {
      l[0] = 1; 
    }
  }
  else if(c2 == 1) {
    if (!l[1])
    {
      r[0] = 1;
    }
  }
  else if(c2 == 2) {
    if (l[0] == 1 && r[0] == 1)
    {
      klee_assert(0);
    }
  }

  int c3;
  klee_make_symbolic(&c3, sizeof(int), "c3");
  if(c3 == 0) {
    if (!r[1])
    {
      l[0] = 1; 
    }
  }
  else if(c3 == 1) {
    if (!l[1])
    {
      r[0] = 1;
    }
  }
  else if(c3 == 2) {
    if (l[0] == 1 && r[0] == 1)
    { 
      klee_assert(0);
    }
  }
  return 0;
}

[xuanlinhha]

On my side the bug in the above program is fixed, but I found some duplication like this int the G:

KLEE: Storing entry for Node #6, Program Point 57216200
KLEE: ------------ Subsumption Table Entry ------------
Program point = 57216200
global = [creation depth: 7
address:
        function/value: @r = global [2 x i32] zeroinitializer, align 4
        stack: (empty)
        offset: 4
        address: 35965356
        base: 35965352
        pointer to location object: 37933040
        concrete offset bound: 8
        size: 8
content:
        a right interpolant value:
                branch infeasibility [main: Line 53]
        function/value: main/  %68 = load i32* getelementptr inbounds ([2 x i32]* @r, i32 0, i64 1), align 4, !dbg !193
        expression: 0
        pointer to location object: 36131728creation depth: 6
address:
        function/value: @l = global [2 x i32] zeroinitializer, align 4
        stack: (empty)
        offset: 0
        address: 35965336
        base: 35965336
        pointer to location object: 37931888
        concrete offset bound: 8
        size: 8
content:
        a right interpolant value:
                branch infeasibility [main: Line 44]
        function/value: main/  %53 = load i32* getelementptr inbounds ([2 x i32]* @l, i32 0, i64 0), align 4, !dbg !183
        expression: 0
        pointer to location object: 36129616creation depth: 9
address:
        function/value: @l = global [2 x i32] zeroinitializer, align 4
        stack: (empty)
        offset: 0
        address: 35965336
        base: 35965336
        pointer to location object: 37935968
        concrete offset bound: 8
        size: 8
content:
        a right interpolant value:
                branch infeasibility [main: Line 65]
        function/value: main/  %84 = load i32* getelementptr inbounds ([2 x i32]* @l, i32 0, i64 0), align 4, !dbg !211
        expression: 0
        pointer to location object: 36130496creation depth: 8
address:
        function/value: @l = global [2 x i32] zeroinitializer, align 4
        stack: (empty)
        offset: 4
        address: 35965340
        base: 35965336
        pointer to location object: 37933904
        concrete offset bound: 8
        size: 8
content:
        a right interpolant value:
                branch infeasibility [main: Line 59]
        function/value: main/  %76 = load i32* getelementptr inbounds ([2 x i32]* @l, i32 0, i64 1), align 4, !dbg !202
        expression: 0
        pointer to location object: 36131376]

There are 2 ref<TxStoreEntry> in the interpolation:

address:
        function/value: @l = global [2 x i32] zeroinitializer, align 4
        stack: (empty)
        offset: 0
        address: 35965336
        base: 35965336
        pointer to location object: 37931888
        concrete offset bound: 8
        size: 8
content:
        a right interpolant value:
                branch infeasibility [main: Line 44]
        function/value: main/  %53 = load i32* getelementptr inbounds ([2 x i32]* @l, i32 0, i64 0), align 4, !dbg !183
        expression: 0
        pointer to location object: 36129616creation depth: 9
address:
        function/value: @l = global [2 x i32] zeroinitializer, align 4
        stack: (empty)
        offset: 0
        address: 35965336
        base: 35965336
        pointer to location object: 37935968
        concrete offset bound: 8
        size: 8
content:
        a right interpolant value:
                branch infeasibility [main: Line 65]
        function/value: main/  %84 = load i32* getelementptr inbounds ([2 x i32]* @l, i32 0, i64 0), align 4, !dbg !211
        expression: 0
        pointer to location object: 36130496creation depth: 8

They have the same address but different contents I think they have the same address and offset, they should be the same.

[xuanlinhha]

Hi @rasoolmaghareh This is the original DP program, you can change the BOUND as you run.

#include<stdio.h>
#ifdef LLBMC
#include <llbmc.h>
#else
#include <klee/klee.h>
#endif
#define N 4 // processes 0, 1, 2, 3 each with 4 rules
#define M 4 // number of rules for each process
#define BOUND 3
int left[N], right[N];
int starve[N] = {0};
int eating = 0, caneat[N] = {1};
int main() {
int choice;
for (int i = 0 ; i < BOUND; i++) {
   klee_make_symbolic(&choice, sizeof(int), "choice");
   int c = choice % 16;
   switch (c) {
       // P0
       case 0:  if (!left[0] && !right[N-1]) left[0] = 1; break;
       case 1:  if (!right[0] && !left[1]) right[0] = 1; break;
       case 2:  if (left[0] == 1 && right[0] == 1 && caneat[0]) { caneat[0] = 0; eating++; starve[0]++; break;}
       case 3:  if (left[0] == 1 && right[0] == 1 && !caneat[0]) { caneat[0] = 0; eating++; starve[0]++; break;}
       // P1
       case 4:  if (!left[1] && !right[0]) left[1] = 1; break;
       case 5:  if (!right[1] && !left[2]) right[1] = 1; break;
       case 6:  if (left[1] == 1 && right[1] == 1 && caneat[1]) { caneat[1] = 0; eating++; starve[1]++; break;}
       case 7:  if (left[1] == 1 && right[1] == 1 && !caneat[1]) { caneat[1] = 1; eating--; left[1] = right[1] = 0; break;}
       // P2
       case 8:  if (!left[2] && !right[1]) left[2] = 1; break;
       case 9:  if (!right[2] && !left[3]) right[2] = 1; break;
       case 10: if (left[2] == 1 && right[2] == 1 && caneat[2]) { caneat[2] = 0; eating++; starve[2]++; break;}
       case 11: if (left[2] == 1 && right[2] == 1 && caneat[2]) { caneat[2] = 1; eating--; left[2] = right[1] = 0; break;}

       // add code for different N ....

   }
   klee_assert(eating <= N/2); // (1)
}
klee_assert(!starve[0]); // (2)
return 0;
}

And this is the modified version made by @sanghu1790

#include<stdio.h>
#include <klee/klee.h>

int l[2] = {0,0}, r[2] = {0,0};
// int l[2] , r[2];
int main() {
  // l[0] = l[1] = r[0] = r[1] = 0;
  int c;
  for (int i = 0 ; i < 3; i++) {
    klee_make_symbolic(&c, sizeof(int), "c");
    if(c == 0) {
      if (!r[1])
      {
        l[0] = 1; 
      }
    }
    else if(c == 1) {
      if (!l[1])
      {
        r[0] = 1; 
      }
    }
    else if(c == 2) {
      if (l[0] == 1 && r[0] == 1)
      { 
        klee_assert(0);
      }
    }
  }
  return 0;
}

[rasoolmaghareh]

Thanks

[rasoolmaghareh]

@sanghu1790 Do you need to check PR #375 on your test programs? I am checking and I want to approve the commit.

[rasoolmaghareh]

fixed in PR #375.