Re: [klee-dev] Klee-uclibc.bca Error when Running Coreutils

2017-05-07 Thread Dan Liew 
On 7 May 2017 at 06:27, Zhiyi Zhang  wrote:
> Hi,
>
>
> I have installed klee on Ubuntu(version, 14.04 64 bit) with LLVM-3.4,and I
> successfully run the tutorial 1 & 2. However, I met a problem when I run
> Coreutils 6.11. I used the same options which are showed on "OSDI'08
> Coreutils Experiments", and klee showed an error message as following,
>
>
>
> KLEE: ERROR: Link with library
> /home/jcklee/jc/jcnewklee/klee/Release+Asserts/lib/klee-uclibc.bca failed:
> Invalid valueLoading module failed : Invalid value
>
>
> Could you give me some suggestions to solve this problem? Thank you very
> much.

It is likely that you incorrectly compiled klee-uclibc. You need to
ensure that you compile it using a Clang version that matches the LLVM
version (in your case that is Clang 3.4 and LLVM 3.4) that you link
KLEE against.

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[klee-dev] I am so sorry for my mistake made in my previous post titled as " Excuse me??i maybe find an error which is in the implementation of KLEE"

2017-05-07 Thread ???? 
Hi, all,  Just a few hours ago, i send a post titled as " Excuse me??i 
maybe find an error which is in the implementation of KLEE".
 i know what is the mistake i made. That is, valgrind cannot check memory 
error about allocated array which is statically allocated in stack like the 
form as below, so cannot find the out of bound error.
 int main()
 {
   int re[7];
   re[7]=100;
 }
 Best wishes for you!___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[klee-dev] Excuse me??i maybe find an error which is in the implementation of KLEE

2017-05-07 Thread ???? 
Hi, all, 
 
   I have followed the tutorial below which is used to test the function 
"match" , but i found that the generated tests cannot cause memory errors.
 
 Second tutorial: Testing a simple regular expression library. 

 (the website is: http://klee.github.io/tutorials/testing-regex/)

the main code is: 

int main() {

  // The input regular expression.

  char re[SIZE];

// Make the input symbolic. 

  klee_make_symbolic(re, sizeof re, "re");

  // Try to match against a constant string "hello".

  match(re, "hello");

  return 0;



}
 
the output is:
 
KLEE: Using STP solver backend
   
KLEE: ERROR:   
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp.c:23: memory   
error: out of bound pointer
   
KLEE: NOTE: now ignoring this error at   this location
   
KLEE: ERROR:   
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp.c:25: memory 
error:   out of bound pointer
   
KLEE: NOTE: now ignoring this error at   this location
   
KLEE: done: total instructions = 4598603
   
KLEE: done: completed paths = 7438
   
KLEE: done: generated tests = 16
 
  
As reported, there are two errors occured.

And the error information is in two files in the below:
 

 
The data in test07.ktest is:
 

 
I read the source code of ktest-tool and know the following bytes in red circle 
are the data which are generated to assign the array "re".
 

 
So I change the file Regexp.c as below
 
int main() {
   
// The input regular expression.
   
char re[SIZE];
   
  re[0]=0x5E;
   
  re[1]=0x01;
   
  re[2]=0x2A;
   
  re[3]=0x01;
   
  re[4]=0x2A;
   
  re[5]=0x01;
   
  re[6]=0x2A;
   
// Make the input symbolic. 
   
//klee_make_symbolic(re, sizeof re, "re");
   
//klee_assume(re[SIZE - 1] == '\0');
   
 
   
// Try to match against a constant string "hello".
   
match(re, "hello");
   
 
   
return 0;
   
}
 
  
After compiling using gcc, i use valgrind to check it, the result is:
 
valgrind --tool=memcheck   --leak-check=full ./Regexp3 
   
==19827== Memcheck, a memory error   detector
   
==19827== Copyright (C) 2002-2015, and   GNU GPL'd, by Julian Seward et al.
   
==19827== Using Valgrind-3.12.0 and   LibVEX; rerun with -h for copyright info
   
==19827== Command: ./Regexp3
   
==19827== 
   
==19827== Conditional jump or move   depends on uninitialised value(s)
   
==19827==at 0x4005EF: matchhere (in   
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp3)
   
==19827==by 0x400680: matchhere (in   
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp3)
   
==19827==by 0x400582: matchstar (in 
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp3)
   
==19827==by 0x400610: matchhere (in   
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp3)
   
==19827==by 0x400582: matchstar (in   
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp3)
   
==19827==by 0x400610: matchhere (in   
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp3)
   
==19827==by 0x4006BB: match (in   
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp3)
   
==19827==by 0x400739: main (in 
/home/klee/xiaojiework/kleeexperiment/examples/regexp/Regexp3)
   
==19827== 
   
==19827== 
   
==19827== HEAP SUMMARY:
   
==19827== in use at exit: 0 bytes in 0 blocks
   
==19827==   total heap usage: 0 allocs, 0 frees, 0   bytes allocated
   
==19827== 
   
==19827== All heap blocks were freed --   no leaks are possible
   
==19827== 
   
==19827== For counts of detected and   suppressed errors, rerun with: -v
   
==19827== Use --track-origins=yes to see   where uninitialised values come from
   
==19827== ERROR SUMMARY: 1 errors from 1   contexts (suppressed: 0 from 0)
   
klee@ubuntu:~/xiaojiework/kleeexperiment/examples/regexp$
 
  
Nothing about out of bound pointer is found. only one error which is about 
using uninitialised value(s).
 
I doubt that maybe I was wrong in some steps. So I use the following script 
which is offered by the klee website
 
export   
LD_LIBRARY_PATH=/home/klee/xiaojiework/klee-xiaojie/build/debug/lib/:$LD_LIBRARY_PATH
   
gcc -L   /home/klee/xiaojiework/klee-xiaojie/build/debug/lib/ Regexp.c 
-lkleeRuntest
   
valgrind --tool=memcheck ./a.out
 
  
During execution, it needs to type in the ktest file path manually.

The result is as below and nothing wrong about out of bound pointer is found. 
 
==19176== Memcheck, a memory error   detector
   
==19176== Copyright (C) 2002-2015, and   GNU GPL'd, by Julian Seward et al.
   
==19176== Using Valgrind-3.12.0 and   LibVEX; rerun with -h for copyright info
   
==19176== Command: ./a.out   KTEST_FILE=klee-last/test07.ktest
   
==19176== 
   
KLEE-RUNTIME: KTEST_FILE not set, please   enter .ktest path: 
klee-last/test07.ktest
   
==19176== Conditional jump or move   depends on uninitialised value(s)
   
==19176==at 0x400796: matchhere (in