In KLEE, symbolic data carries no notion of signedness with it. Signedness is given by the context, so 'klee_assume(p1->f2 < 10U)' means that the bytes referenced by p1->f2, interpreted as typeof(p1->f2), should be less than 10U. You may very well add another constraint where the same bytes are interpreted as a signed type.
One last thing: your klee_make_symbolic should probably read klee_make_symbolic(f, 1000); Paul On 13 Jan 2014, at 01:11, Lei Zhang <[email protected]> wrote: > Thanks for the answer, Paul! > > BTW, would you mind tell me how the signed/unsigned type is handled in klee? > For example, > > struct A { > int f1; // 4 bytes > unsigned f2; // 4 byte > bool f3[10]; // 10 bytes > }; > > void *f = malloc(1000); > klee_make_symbolic(f, sizeof(f)); > struct A *p1 = (struct A *) f; > klee_assume(p1->f2 < 10U); > // will this make sure that f2 is greater than or equal to 0 > automatically? > > For the above case, f2 is only explicitly forced to be less than 10. However, > since f2 is an unsigned int, it should be greater than or equal to 0. Will >= > 0 be automatically enforced? Or, the 5th-8th byte of f can be combined to > represent a negative number (with the most significant bit as 1, which is > interpreted as a very large number for unsigned int)? > > > On Sun, Jan 12, 2014 at 11:48 AM, Paul Marinescu > <[email protected]> wrote: > The answer is indeed yes to both questions. > > Regarding the origin of the term 'counterexample', it's likely related to the > fact that a that a solution from KLEE's point of view is a counterexample > from STP's point of view (because STP decides validity while KLEE looks for > satisfiability). > > Paul > > On 12 Jan 2014, at 02:51, Lei Zhang <[email protected]> wrote: > >> Hi All, >> >> I am reading KLEE's source code in order to add some functionalities for it. >> After struggling with the details for a long time, I still have difficulties >> with the following questions. Can somebody shed light on it? Any explanation >> will be highly appreciated. Thanks! >> >> 1) Lots of places use "counter example (cex)" as parts of the names. For me, >> counter examples mean instances that disprove a statement. However, from my >> understanding of the code, couter examples just mean "some assignments that >> satisfy a set of constraints" or "no solution", which is quite the opposite. >> If this is actually the case, why is the misleading "counter example" used? >> Maybe it is better to change it? >> >> Besides, klee_prefer_cex() only gives "preference" of the argument >> constraint without forcing it (meaning test cases violate the constraint can >> also be generated), while klee_assume() forces the argument constraint to be >> true. Is this right? >> >> 2) If I first klee_make_symbolic() a large range of memory, and then doing >> lots of pointer calculation and klee_assume(), will this actually enforce >> the constraints on the underlying memory? For example, for the following >> code, >> >> struct A { >> int f1; // 4 bytes >> bool f2; // 1 byte >> bool f3[10]; // 10 bytes >> }; >> >> void *f = malloc(1000); >> klee_make_symbolic(f, sizeof(f)); >> struct A *p1 = (struct A *) f; >> klee_assume(p1->f2 == 0); >> // will this make the 5th byte of f to be 0? >> struct A *p2 = (struct A *) ( (char *) f + sizeof(struct A) + 3 ); >> klee_assume(p2->f3[0] == 1); >> // will this make the (15 + 3 + 6)th byte of f to be 1? >> >> By working through how the code handles the statements, I think the answer >> to the above question are both yes. But my code just does not behave as I >> expected. So I just need to double check my understanding. >> >> Thanks in advance! >> >> -- >> Best regards, >> Lei Zhang >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > > > > -- > Best regards, > Lei Zhang
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
