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

[Cristian Cadar]

On 09/02/2021 14:09, Eduardo R B Marques wrote:
>> 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”.
Note that this makes sense: stdout is only written into.
To analyze its contents, you will have to manipulate directly the stdout 
buffer used by the POSIX runtime; unfortunately there is no better 
interface right now.

> Also, regarding my other question, I assume that —libc=uclibc is a requirement for using -sym-stdin/sym-stdout ?
No, it's not.  It can be used independently.  However, the issues you 
run into are related to the fact that you use libc functions that 
manipulate stdin/stdout, which are called as external functions without 
-—libc=uclibc.

Best,
Cristian

> 
> 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
>