Thanks a lot for the answer! I think I get your idea. By "given by the context", you mean that we want to interpret p1->f2 as an unsigned int. And we want it to be less than 10U. These two together determines the bytes referenced by p1->f2 can only be in the range [0, 10). Latter we can make other pointers pointing to the same bytes and enforce more constraints. It all depends on how you interpret it.
Yes, I lost a dereference in my example. Thanks for reminding! On Mon, Jan 13, 2014 at 9:51 PM, Paul Marinescu < [email protected]> wrote: > 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 > > > -- Best regards, Lei Zhang
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
