> 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 <[email protected]> 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 >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
