[klee-dev] The symbolic values for variables

[Zhongqiu Gao]

Hi,

I am confused about how the symbolic variables are stored with constraints in memory. For example, we have the following program:




int sum(int a, int b, int c) {
  if(a == b - 6){
      return a + b - c;
  }
  else if(c == a - b + 1){
    return a + b + c;
  }
  else{
    return a + b + c + 1;
  }
}


int main() {
  int a, b, c;
  klee_make_symbolic(&a, sizeof(a), "x");
  klee_make_symbolic(&b, sizeof(b), "y");
  klee_make_symbolic(&c, sizeof(c), "z");
  sum(a, b, c);
  return 0;
} 


So for the executionState of  first branch where a == b-6, the symbolic variable a should be x0, and b should be x0 + 6. So for symbolic variable "y", does klee store y's symbolic value y0 as x0 + 6 in memoryObject? Or it just stores y0, separately with the constraints? 


I am able to print the constraints out at the end of each execution, but I still want to print the symbolic variables with their symbolic values, such as a==x0, b==x0+6, c==z0. So I want to know if executionState stores the relations of symbolic values in memory. I think the solver deals with the relations in the end before generating test cases, but I am not sure. 


What I want to print for the first branch is:
constraints: a == b - 6
symbolic values: a==x0, b==x0+6, c==z0




We can take the picture for example. I want to know if memoryObject stores information like in the table such as X: α1+α2

Thank you very much!




Best,

Zhongqiu Gao
-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: symbolicValues.png
Type: image/png
Size: 94947 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20190127/38dab246/attachment.png>