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

[Cristian Cadar]

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
>