[klee-dev] The format of generated smt files

[Zhongqiu Gao]

Hi Richard,
Thanks for the reply. The whole path constraints are:
 [(! (0 == x)), 
   (! (0 == y)), 
   (! ( y < x)),
   (! (0 ==( y - x))), 
   (! (( y - x) < x)), 
   (0 ==(( y - x) - x)) ]
The solver gives x=0x8000fffe, and y=0x0001fffc, which in decimal, is x==2147549180 and y==131068.
It is correct when x==2147549180(as I said in the last email) but since x has been overflowed as an integer, I consider it as an unsigned int. Converted it to integer, we have x = -65534.
And y is a positive number, y - x - x should also be a positive number, not 0. The values satisfy the constraints because of arithmetic operation overflows. I am wondering if there is a way to let the solver generate values which don't have arithmetic operation overflows. For example y == 10 and x == 5 is perfect. I thought it would be good if the values are declared as integers instead of bit vectors.
I've asked the similar question on https://stackoverflow.com/questions/57937374/is-there-a-way-to-specify-the-the-domain-of-a-variable-when-defining-it-using-an
The core question is, I want to generate value like y==10 and x==5, but the solver keeps giving me the overflowed results, which is not correct at the integer level.
For example, the code
/--------------------code------------------/

void gcd(int x, int y){
   if(x==0){
      return;
   }
   while(y != 0){
      if(x > y)
         x = x - y;
      else
         y = y - x;
   }
   return;
}
/--------------------code------------------/
There is a path with the path constraints I mentioned in the beginning of the email. x==5 and y==10 is totally fine, but x==-65534 and y==131068 won't cover this path.


Thanks,
Zhongqiu Gao



At 2019-09-18 01:51:10, "Richard Rutledge" <rrutledge3 at gatech.edu> wrote:

Declaring x and y as 32-bit integers would not prohibit the solver from generating your example values.  Fixed width integers can always overflow. 


For (y = 131068 and x = 2147549180) y - 2x == 0, not just in the solver, but on the machine as well.
Why is that solution not satisfactory?  Does x and y have some additional constraints in your expectations?


│⚙ Cheers!
│Richard Rutledge
└────────────────────

On Tue, Sep 17, 2019 at 1:26 PM, Zhongqiu Gao <zhongqiu_gao at 126.com> wrote:

Hi,
I am trying to use 
--write-smt2s 
to write the path constraints into smt files. But all of the variables are defined as an array of bit vector. Is there a way to let klee specify the variable type when generating the smt files?
For example, in the source file, if x is declared as an integer, then in the smt file, it should also be defined as an integer, not an array of bit vector.
I am trying to let the solver read the smt files and generate a value, and sometimes the values it generate are overflowed. For example, we want y - 2x == 0, and it turns out
y = 131068 and x = 2147549180.
y - x - x  = -4294967296. It's not zero, but is considered 0 by the solver because 4294967296 is
1 00000000 00000000 00000000 0000000
as binary and "1" is eliminated due to overflow.


Thanks,
Zhongqiu Gao




 





 
-------------- next part --------------
HTML attachment scrubbed and removed