Hi Kumaresh,
Please ask KLEE-related questions on the klee-dev mailing list.
To answer your main question, as mentioned in our OSDI paper, objects
are required to have concrete sizes. When this is not the case, KLEE
"concretizes" the size, that is it chooses one possible concrete value.
This obviously can lead to missing paths, as it happens in your
example.
Note that this is a limitation common to all dynamic symbolic execution
tools like KLEE, and unfortunately I'm not aware of any general scalable
solution right now.
Cristian
On Thu, 2008-12-04 at 14:17 -0600, Kumaresh Pattabiraman wrote:
> Hi Christian,
>
> We are trying to use KLEE for testing a DNS server implementation
> (BIND). As a starting point, I am trying to look at how a string is
> symbolized and have shown below a sample code I am trying to run. I
> have two questions:
> 1) I get a KLEE: ERROR: concretized symbolic size, corresponding to
> the domainStrSize of 4 in a test case. I am not sure what this refers
> to by concretized symbolic size. Could you please explain this.
> 2) KLEE doesn't cover a test case which generates
> domainStr="google.com" and as a result, that path is not covered. I
> was trying to reason out why the coverage wouldn't be 100% in this
> case.
>
> 3) Also, I am thinking of writing a script that would replace parts of
> the DNS server implementation in C that change inputs into symbolic
> inputs - Are there similar attempts before and if so, could you point
> me to resources?
> 4) Finally, could you please give me more information about how I
> should interpret the .pc and .model.err files in the log?
>
> int main() {
> char *test = "google.com";
> int domainStrSize;
> klee_make_symbolic(&domainStrSize, sizeof(domainStrSize));
>
> if(domainStrSize < 1 || domainStrSize > 15) {
> printf(" Domain name too long or short\n"); exit(0);
> }
>
> char *domainStr;
> if(!(domainStr = malloc(sizeof(char)*domainStrSize))) {
> printf("Couldn't allocate enough space for characters\n");
> exit(-1);
> }
>
> klee_make_symbolic(domainStr,
> sizeof(char)*domainStrSize);
> domainStr[domainStrSize-1]='\0';
>
> if( strcmp(domainStr,test) == 0)
> printf("Google.com\n");
> else
> printf("Not Google.com\n");
> return 0;
> }
>
> Thanks for your help.
>
> Kumaresh
>
> --
> Kumaresh Pattabiraman
> Graduate Student, MS-CS
> University of Illinois, Urbana-Champaign
> http://www.cs.uiuc.edu/homes/kpattab2
>
