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

[Eduardo R B Marques]

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 
-------------- next part --------------
HTML attachment scrubbed and removed