On 27 May 2017 at 01:36, Shehbaz Jaffer <shehbaz.jaf...@mail.utoronto.ca> wrote: > Hello KLEE developers, > > I am trying to understand how KLEE emulates environment variables. In > particular, how do functions like getopt_long get executed with KLEE, when we > give --sym-arg as an argument. getopt_long is found in unistd.h, and is > available in uclibc. For a coreutils file like groups.c where the following > line is encountered: > > while ((optc = getopt_long (argc, argv, "", longopts, NULL)) != -1) > > how would KLEE generate different inputs? for simplicity, consider the case > where we use --sym-arg 1 10 as a command line argument which leads to argv[1] > becoming a symbolic buffer of size 10, if my understanding is correct, when > getopt_long is called, one of the two things can happen: > > 1) argv[1] is declared as a symbolic buffer, we explore all paths of > getopt_long code in uclibc library, so all different if's / elses in > getopt_long code will get forked and execute to give different optc values. > 2) getopt_long is skipped, optc variable is made symbolic, and the main > function in groups.c treats optc as symbolic value. on any successive if/else > condition in groups.c containing optc, a new state is forked with new value > of optc.
Take a look at the `klee_init_env()` function [1]. When KLEE is called with --posix-runtime the program's `main()` is rewritten to call `klee_init_env()` at the beginning and change `argc` and `argv`. The `klee_init_env()` function introduces symbolic arguments if requested. From that point onwards execution of the program just proceeds as normal so `getopt_long()` will just be interpreted by KLEE just like any other function. [1] https://github.com/klee/klee/blob/bec4ceafe412a08de303678581e07451a1399e1f/runtime/POSIX/klee_init_env.c#L85 _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev