[klee-dev] Use of -sym-stdin/stdout

[Eduardo R B Marques]

> 1) printf is run concretely by default (you can add -DKLEE_SYM_PRINTF when compiling KLEE's uclibc to change this)

Ok, this is not a major issue, printf can be replaced by fprintf (assuming the latter is supported).

> 2) you should only use —sym-sdout if you need to symbolically analyze the contents of stdout, otherwise don't set it


Yes, that’s right, I do want to “analyze the contents of stdout”. But how can it be done? As I mentioned, the ktest files do not 
seem to contain the symbolic “stdout”. 

Also, regarding my other question, I assume that —libc=uclibc is a requirement for using -sym-stdin/sym-stdout ? 

Thanks, best regards,
Eduarrod

> On 9 Feb 2021, at 11:33, Cristian Cadar <c.cadar at imperial.ac.uk> wrote:
> 
> Hi Eduardo,
> 
> Indeed, we need better documentation here.  But in a nutshell:
> 
> 1) printf is run concretely by default (you can add -DKLEE_SYM_PRINTF when compiling KLEE's uclibc to change this)
> 
> 2) you should only use —sym-sdout if you need to symbolically analyze the contents of stdout, otherwise don't set it
> 
> Best,
> Cristian
> 
> On 06/02/2021 20:28, Eduardo R B Marques wrote:
>> Hi,
>> I have a few questions regarding the use of the -sym-stdin / -sym-stdout options. Consider the following simple program in a file named foo.c:
>> *#include <stdio.h>*
>> *
>> int main(int argc, char** argv) {
>>   int c = getchar();
>>   if (c >= 'a' && c <= 'z')
>>     printf("lower case\n");
>>   else if (c >= 'A' && c <= 'Z')
>>     printf("upper case\n");
>>   else printf("Other\n");
>>   return 0;
>> }*
>> Using the klee 2.1  docker image I compile it as follows:
>> *clang -emit-llvm -std=c89 foo.c -c -o foo.bc*
>> then execute it using:
>> *klee -posix-runtime --libc=uclibc foo.bc -sym-stdin 1 -sym-stdout*
>> I obtain a few warnings that do not seem (at first) too relevant regarding the use printf (external function), but that’s all.
>> 5 paths are explored in total.
>> My questions arise when I consider variations of this overall setup:
>> 1) Suppose I change the first printf call
>> *  printf("lower case\n”);*
>> to
>> *printf("lower case %c\n”, c);*
>> *
>> *
>> Then, during symbolic execution I get the following error:
>> *KLEE: ERROR: (location information missing) external call with symbolic argument: printf*
>> It puzzles me as to why getchar() is not “external” but printf is ?  If I use  putchar(c)  or puts() then klee works fine.
>> 2) If I specify *—libc=klee * in place of *—libc=uclibc* it seems “stdin” is not symbolic anymore, i.e. I have to type in the input character.
>> Why does this happen? I guess I should assume —libc=uclibc is a requirement for using —sym-stdin ?
>> 3) When —sym-sdout  is on I see that .ktest files contain a stdout variable ("object 2)", in a similar way to stdin ("object 0"). However they do not seem to correspond to the actual output.
>> For instance, consider this simpler program:
>> *#include <stdio.h>
>> int main(int argc, char** argv) {
>>   int c = getchar();
>>   if (c >= 'a' && c <= 'z')
>>     putchar(c);
>>   return 0;
>> }*
>> Three ktest files are generated containing the stdin data:
>> *object 0: data: b'\x00'
>> object 0: data: b'{'
>> object 0: data: b'a'*
>> but the stdout data is always an array with size 1024 filled with zeros. This should not be the case for input ‘a’, right?
>> Best,
>> Eduardo
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev