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" <[email protected]> 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 <[email protected]> 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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
