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.ca...@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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
