[klee-dev] Fw: question on different outputs when running under klee and with ktest file

[Liu, Mingyi]

Hi all,

Could anyone help me understand the following differences?


Thanks,
Mingyi

________________________________
From: klee-dev-bounces at imperial.ac.uk <klee-dev-bounces at imperial.ac.uk> on behalf of Liu, Mingyi <mingyiliu at gatech.edu>
Sent: Thursday, April 1, 2021 6:15 PM
To: klee-dev at imperial.ac.uk <klee-dev at imperial.ac.uk>
Subject: [klee-dev] question on different outputs when running under klee and with ktest file

Hi klee-dev members,

I made a simple program below and observed different outputs when running under klee and verifying with the ktest file.

#include <stdio.h>
#include "klee/klee.h"

int main() {

  int a;
  int b;
  int c;

  klee_make_symbolic(&a, sizeof(a), "a");
  klee_make_symbolic(&b, sizeof(b), "b");
  klee_make_symbolic(&c, sizeof(c), "c");

  printf("before: a = %d b = %d c = %d\n", a, b, c);

  if (a == 2 && b == 3) {
    printf("%s%s%n\n", &a, &b, &c);
    printf("after: a = %d b = %d c = %d\n", a, b, c);
  }

  return 0;

}

To be specific, I used the following commands and got three paths/testcases as expected. What I am confused about is the output for the c value ("after: a = 2 b = 3 c = 0"), should that be 2? Why it is 0 here?

command: $ clang-9 -I ../klee/include -c -emit-llvm -g -O0 logic_or.c
                  $ ../klee/build/bin/klee -external-calls=all logic_or.bc
[cid:4493b7ad-e1f8-433a-acfd-1f0477862675]

I then compiled the program and ran it with the third testcase above, the results are all as expected as c is 2 this time.
command: $ gcc -I ../klee/include logic_or.c -lkleeRuntest -L ../klee/build/lib -o logic_or
                  $ KTEST_FILE=klee-last/test000003.ktest ./logic_or
[cid:10eb545b-fc10-4eaf-95ef-062b4f7247f4]


Could you please explain why the output values for c are different? Is it intended?



klee version information:

KLEE 2.3-pre (https://klee.github.io)
  Build mode: RelWithDebInfo (Asserts: ON)
  Build revision: 36780583dd78865100114b02627a3418b2d56deb

LLVM (http://llvm.org/):
  LLVM version 9.0.1

  Optimized build.
  Default target: x86_64-pc-linux-gnu
  Host CPU: skylake

Thanks,
Mingyi
-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Outlook-wxucu054.png
Type: image/png
Size: 19688 bytes
Desc: Outlook-wxucu054.png
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20210405/223cf25c/attachment.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Outlook-idgtlb50.png
Type: image/png
Size: 6494 bytes
Desc: Outlook-idgtlb50.png
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20210405/223cf25c/attachment-0001.png>