UTBotCpp icon indicating copy to clipboard operation
UTBotCpp copied to clipboard

Pass pointer value to function

Open ladisgin opened this issue 3 years ago • 0 comments

Description Now UTBot create variable on stack and make this memory symbolic. But in this case, it doesn't generate tests that pass nullptr.

For function

int longptr_cmp(long *a, long *b) {
    return (*a == *b);
}

KLEE file

int klee_entry__lib_pointers_pointer_parameters_longptr_cmp__wrapped(int utbot_argc, char ** utbot_argv, char ** utbot_envp) {
    long a;
    klee_make_symbolic(&a, sizeof(a), "a");
    klee_prefer_cex(&a, a >= -10 & a <= 10);
    //////////////////////////////////////////// 
    long b;
    klee_make_symbolic(&b, sizeof(b), "b");
    klee_prefer_cex(&b, b >= -10 & b <= 10);
    //////////////////////////////////////////// 
    long a_post;
    klee_make_symbolic(&a_post, sizeof(a_post), "a_post");
    long b_post;
    klee_make_symbolic(&b_post, sizeof(b_post), "b_post");
    int utbot_result;
    klee_make_symbolic(&utbot_result, sizeof(utbot_result), "utbot_result");
    int utbot_tmp = longptr_cmp(&a, &b);
    klee_assume(utbot_tmp == utbot_result);
    klee_assume(a == a_post);
    klee_assume(b == b_post);
    return 0;
}

For solve this problem UTBot should generate symbolic pointer in KLEE and pass it to function.

KLEE file

int klee_entry__lib_pointers_pointer_parameters_longptr_cmp__wrapped(int utbot_argc, char ** utbot_argv, char ** utbot_envp) {
    long* a;
    klee_make_symbolic(&a, sizeof(a), "a");
    long* b;
    klee_make_symbolic(&b, sizeof(b), "b");
    int utbot_result;
    klee_make_symbolic(&utbot_result, sizeof(utbot_result), "utbot_result");
    int utbot_tmp = longptr_cmp(&a, &b);
    klee_assume(utbot_tmp == utbot_result);
    return 0;
}

In first implementation some problem can be ignored like

  1. Array
  2. Post value
  3. Parameter is reference to utbotInnerVar

ladisgin avatar Oct 28 '22 10:10 ladisgin