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

[Nowack, Martin]

Hi Mingyi,

You’ve hit a bug in KLEE.
Thanks for your detailed description - I just opened PR based on your test case
https://github.com/klee/klee/pull/1407 that fixes the issue.

Feel free to apply those changes locally to try them out.

The test case is based on your example and works with the changes.

All the best,

Martin

On 5. Apr 2021, at 18:50, Liu, Mingyi <mingyiliu at gatech.edu<mailto:mingyiliu at gatech.edu>> wrote:

Hi all,

Could anyone help me understand the following differences?


Thanks,
Mingyi

________________________________
From: klee-dev-bounces at imperial.ac.uk<mailto:klee-dev-bounces at imperial.ac.uk> <klee-dev-bounces at imperial.ac.uk<mailto:klee-dev-bounces at imperial.ac.uk>> on behalf of Liu, Mingyi <mingyiliu at gatech.edu<mailto:mingyiliu at gatech.edu>>
Sent: Thursday, April 1, 2021 6:15 PM
To: klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk> <klee-dev at imperial.ac.uk<mailto: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
<Outlook-wxucu054.png>

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
<Outlook-idgtlb50.png>

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

-------------- next part --------------
HTML attachment scrubbed and removed