Re: [klee-dev] One question about external dispatcher

2017-01-30 Thread Qiuping Yi
Thanks. You are right. I solved the problem.


Best regards,

Qiuping Yi
Parasol Laboratory
Department of Computer Science and Engineering
Texas A University
College Station
TX 77843

On Sat, Jan 28, 2017 at 4:12 AM, Dan Liew <d...@su-root.co.uk> wrote:

> On 27 January 2017 at 04:18, Qiuping Yi <yiqiup...@gmail.com> wrote:
> > Dear all,
> >
> > I encountered a strange problem when testing the next code snippet:
> >
> > 1 if (pw = getpwuid(getuid()) == NULL)
> > 2   return ;
> >
> > 3 .. = pw->pw_dir;
>
> Please use the correct mailing list (klee-dev@imperial.ac.uk) instead
> of the old klee-...@keeda.stanford.edu mailing list.
>
> It would be better if you provided a small complete example. Like this.
>
> ```
> #include 
> #include 
> #include 
> #include 
> #include 
>
> int main(int arc, char** argv) {
>   struct passwd* pw;
>   uid_t uid = getuid();
>   printf("uid is %d\n", uid);
>   if (pw = getpwuid(getuid()) == NULL) {
> printf("Failed\n");
> return 1;
>   }
>   assert(pw && "pw cannot be NULL");
>
>   char* pw_dir = pw->pw_dir;
>   printf("pw_dir: %s\n", pw_dir);
>   return 0;
> }
> ```
>
> Your code is wrong.
>
> if (pw = getpwuid(getuid()) == NULL)
>
> is doing this
>
> if ( pw = ( getpwuid(getuid()) == NULL )
>
> so a pointer is returned by `getpwuid()` and then we compare with NULL
> which is false so then `pw` gets assigned the value zero.
>
> However once I fix your code to
>
> if ((pw = getpwuid(getuid())) == NULL) {
>
> then I can reproduce the problem if I just run `klee program.bc`
>
> I suspect it's to do with the fact `getpwuid()` returns a pointer to
> "real memory" which does not point to anything in KLEE's own model of
> the memory (i.e. the address space of the program under).
>
> To fix this you need not call `getpwuid()` as an external function but
> instead call it from klee-uclibc so that it can be symbolically
> executed.
>
> If you run
>
> ```
> klee -libc=uclibc program.bc
> ```
>
> no out of bounds access is reported.
>
> HTH,
> Dan.
>
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


[klee-dev] One question about external dispatcher

2017-01-26 Thread Qiuping Yi
Dear all,

I encountered a strange problem when testing the next code snippet:

1 if (pw = getpwuid(getuid()) == NULL)
2   return ;

3 .. = pw->pw_dir;

When handling line 1, KLEE firstly invokes *externalDispatcher->executeCall*
which will invoke *runProtectedCall* to execute the external function and
store
the result to a given memory location. Then, it will invoke *fromMemory* to
get the
return value from the location. However, it encounters an "out of bound"
error
when handling line 3. I printed the value of variable *pw* at line 1, and
got something like *139894903382656*, which definitely does not equal to '
*null*',
thus it will arrive line 3. Actually, *139894903382656* seems an invalid
address.

So why does this strange situation happen?

Thank you all in advance.

Best regards,

Qiuping Yi
Parasol Laboratory
Department of Computer Science and Engineering
Texas A University
College Station
TX 77843
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


Re: [klee-dev] Strange behavior of KLEE when evaluating NULL pointer

2014-05-14 Thread Qiuping Yi
Hi, Paul

Next is my whole test code:

1void test2(int *p) {
2   if (p == NULL)
3p = malloc(sizeof(*p));

4   *p = 1;
  }

5 int main() {
6   int *p;
7   test(p);
8   return 0;
   }

This code was executed without any error after compiled with gcc. However, when
I applied KLEE to this code, it encountered an 'out of bound pointer'
error. If I replace line 6 to 'int *p = NULL', no error happened. So KLEE
needs to explicitly initialize each variable, containing the pointers,
right?




Qiuping Yi
Institute Of Software
Chinese Academy of Sciences


On Tue, May 13, 2014 at 6:50 PM, Paul Thomson pault...@gmail.com wrote:

 Please can you provide the code that calls test?

 Or, please try using something like:

 int main()
 {
 int *p = NULL;
 test(p);
 return 0;
 }


 Thanks,
 Paul


 On 13 May 2014 11:09, Qiuping Yi yiqiup...@gmail.com wrote:

  Hi, everyone

 I found a strange behavior of KLEE.

 When I applied KLEE to the next code snippet, a out-of-bound-pointer
 error happened at line 3. However, this code snippet explicitly allocates
 space for pointer p at line 2 when it is evaluated to NULL. So what's wrong?

 0 void test (int *p) {
 1if (p == NULL)
 2p = malloc(sizeof(*p));

 3   *p = 2;
 }

 Best Regards!

 
 Qiuping Yi
 Institute Of Software
 Chinese Academy of Sciences

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



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


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


Re: [klee-dev] Strange behavior of KLEE when evaluating NULL pointer

2014-05-14 Thread Qiuping Yi
Hi Oscar, Hongxu,

Thank you for you comment.

Yes, you are right. In practice, my test code have an uninitialized error.
But now I am considering some variables from external environment. These
variables may be uninitialized, so I use pointer p in function 'test' to
describe such a simple situation. I want to use the if-statement at line 2
to judge whether the external pointer p is NULL, if it is I want to
explicitly allocate some space to it at line 3. But now I know KLEE cannot
judge on an uninitialized pointer.




Qiuping Yi
Institute Of Software
Chinese Academy of Sciences


On Wed, May 14, 2014 at 10:51 PM, Oscar Soria Dustmann 
oscar.soriadustm...@comsys.rwth-aachen.de wrote:

 Hi Qiuping,

 your code exhibits undefined behaviour as you read from uninitialised
 memory. The reason it doesn't fail when run natively is implementation
 defined and pure luck. It's not that KLEE needs the initialisation; The
 C standard demands it (reason behind it: Stack variables are not
 default-initialised for performance reasons).

 I'd actually consider it desired behaviour for a testtool to throw you
 an error.

 Cheers,
 Oscar

 On 14/05/14 15:43, Qiuping Yi wrote:
  Hi, Paul
 
  Next is my whole test code:
 
  1void test2(int *p) {
  2   if (p == NULL)
  3p = malloc(sizeof(*p));
 
  4   *p = 1;
}
 
  5 int main() {
  6   int *p;
  7   test(p);
  8   return 0;
 }
 
  This code was executed without any error after compiled with gcc.
 However, when
  I applied KLEE to this code, it encountered an 'out of bound pointer'
  error. If I replace line 6 to 'int *p = NULL', no error happened. So KLEE
  needs to explicitly initialize each variable, containing the pointers,
  right?
 
 
 
  
  Qiuping Yi
  Institute Of Software
  Chinese Academy of Sciences
 
 
  On Tue, May 13, 2014 at 6:50 PM, Paul Thomson pault...@gmail.com
 wrote:
 
  Please can you provide the code that calls test?
 
  Or, please try using something like:
 
  int main()
  {
  int *p = NULL;
  test(p);
  return 0;
  }
 
 
  Thanks,
  Paul
 
 
  On 13 May 2014 11:09, Qiuping Yi yiqiup...@gmail.com wrote:
 
   Hi, everyone
 
  I found a strange behavior of KLEE.
 
  When I applied KLEE to the next code snippet, a out-of-bound-pointer
  error happened at line 3. However, this code snippet explicitly
 allocates
  space for pointer p at line 2 when it is evaluated to NULL. So what's
 wrong?
 
  0 void test (int *p) {
  1if (p == NULL)
  2p = malloc(sizeof(*p));
 
  3   *p = 2;
  }
 
  Best Regards!
 
  
  Qiuping Yi
  Institute Of Software
  Chinese Academy of Sciences
 
  ___
  klee-dev mailing list
  klee-dev@imperial.ac.uk
  https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
 
 
 
  ___
  klee-dev mailing list
  klee-dev@imperial.ac.uk
  https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
 
 
 
 
 
  ___
  klee-dev mailing list
  klee-dev@imperial.ac.uk
  https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
 

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

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


[klee-dev] Invitation to connect on LinkedIn

2014-05-14 Thread Qiuping Yi
LinkedIn




I'd like to add you to my professional network on LinkedIn.

- Qiuping

Qiuping Yi
--
China

Confirm that you know Qiuping Yi:
https://www.linkedin.com/e/fwmsg6-hv7cmrb6-2i/isd/5872510063670738944/1temtXms/?hs=falsetok=1O_Jrw8fFq4mg1

--
You are receiving Invitation to Connect emails. Click to unsubscribe:
http://www.linkedin.com/e/fwmsg6-hv7cmrb6-2i/eFPC4J5Rz7QQtXHa3b6Rb1PEH6bj6NMYmSof/goo/klee-dev%40imperial%2Eac%2Euk/20061/I7078372816_1/?hs=falsetok=0uOyfM9vZq4mg1

(c) 2012 LinkedIn Corporation. 2029 Stierlin Ct, Mountain View, CA 94043, USA.


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


[klee-dev] Invitation to connect on LinkedIn

2014-05-14 Thread Qiuping Yi
LinkedIn




I'd like to add you to my professional network on LinkedIn.

- Qiuping

Qiuping Yi
--
China

Confirm that you know Qiuping Yi:
https://www.linkedin.com/e/-8mnz76-hv7cmk5x-63/isd/5872510076471758848/Kko2r6sn/?hs=falsetok=2gU_XTtn5q4mg1

--
You are receiving Invitation to Connect emails. Click to unsubscribe:
http://www.linkedin.com/e/-8mnz76-hv7cmk5x-63/vqX3hpfgkANPlqlepZu0pdf9_QcPAz40Hmv3R5zl8S/goo/klee-dev%40keeda%2Estanford%2Eedu/20061/I7078372851_1/?hs=falsetok=01Z8LeSqpq4mg1

(c) 2012 LinkedIn Corporation. 2029 Stierlin Ct, Mountain View, CA 94043, USA.


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


[klee-dev] Strange behavior of KLEE when evaluating NULL pointer

2014-05-13 Thread Qiuping Yi
Hi, everyone

I found a strange behavior of KLEE.

When I applied KLEE to the next code snippet, a out-of-bound-pointer error
happened at line 3. However, this code snippet explicitly allocates space
for pointer p at line 2 when it is evaluated to NULL. So what's wrong?

0 void test (int *p) {
1if (p == NULL)
2p = malloc(sizeof(*p));

3   *p = 2;
}

Best Regards!


Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


Re: [klee-dev] Strange error when compiling 'bash-4.0' using klee-gcc

2014-03-27 Thread Qiuping Yi
Hi, Dan Liew,

Thank you for your advice. Now I can use *wllvm *to generate bash.bc
successfully based on the next steps:

$ export LLVM_COMPILER=llvm-gcc
$ export LLVM_GCC_PREFIX=llvm-
$ cd bash-4.0
$ ./configure --disable-nls CFLAGS=-g
$ make CC=wllvm
$ extract-bc bash

however, I cannot run klee on the generated 'bash.bc'.

when I carry out:

$ klee *--libc=uclibc --posix-runtime *./bash.sh test.sh

I got the next error messag:

KLEE: ERROR: unable to load symbol(PC) while initializing globals.

Could you tell me what should I do then? Thank you very much.






Qiuping Yi
Institute Of Software
Chinese Academy of Sciences


On Mon, Mar 24, 2014 at 7:49 PM, Daniel Liew daniel.l...@imperial.ac.ukwrote:

  /home/guest/installed/klee/scripts/klee-gcc  -DPROGRAM='bash'
  -DCONF_HOSTTYPE='x86_64' -DCONF_OSTYPE='linux-gnu'
  -DCONF_MACHTYPE='x86_64-unknown-linux-gnu' -DCONF_VENDOR='unknown'
  -DLOCALEDIR='/usr/local/share/locale' -DPACKAGE='bash' -DSHELL
  -DHAVE_CONFIG_H   -I.  -I. -I./include -I./lib   -g  -o mksyntax
  ./mksyntax.c
  /tmp/cc1H53KR.o: file not recognized: File format not recognized
  collect2: ld returned 1 exit status
  make: *** [mksyntax] Error 1

 It looks like the script is trying to invoke your system's native
 linker to build a native executable. That won't work because
 /tmp/cc1H53KR.o is probably an LLVM bitcode file so the linker does
 not know what to do with it.

 You probably should be using the '-c' flag so you do not invoke the
 linker. This approach is really only feasible with single file
 programs.

  Furthermore, it's strange that the not recognized file keeping changed
 if I
  execute 'make' again and again. For example, the second time I encounter
 the
  next error message:
 
  /tmp/ccaJGvTn.o: file not recognized: File format not recognized

 It's not strange at all, the compiler is creating temporary files
 during the compilation process.

  BUT I found both file /tmp/cc1H53KR.o and /tmp/ccaJGvTn.o do not exist.

 These files are deleted automatically by the compiler because they are
 temporary intermediate files.

  What's wrong? What should I do?

 I've already explained above what is wrong.

 I do not know much about bash's build system but I would expect it to
 be more complex that coreutil's. klee-gcc is a bit of a hack so you
 should probably either

 - Use wllvm [1]. This is also a hack but is considerably better than
 klee-gcc and can link together multi file programs.
 - Use LLVM gold [2] so you can link together a multi-file program to a
 bitcode module.


 [1] https://github.com/klee/whole-program-llvm
 [2] http://llvm.org/docs/GoldPlugin.html

 Thanks,
 Dan Liew.

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


[klee-dev] Strange error when compiling 'bash-4.0' using klee-gcc

2014-03-22 Thread Qiuping Yi
Hi, everyone

I want to compile 'bash-4.0' with klee-gcc following the next commands
(like compiling coreutils http://klee.github.io/klee/TestingCoreutils.html
):

$ ../configure --disable-nls CFLAGS=-g
$ make CC=/home/guest/installed/klee/scripts/klee-gcc

However, I encountered an error when 'make', which the following error
message:

/home/guest/installed/klee/scripts/klee-gcc  -DPROGRAM='bash'
-DCONF_HOSTTYPE='x86_64' -DCONF_OSTYPE='linux-gnu'
-DCONF_MACHTYPE='x86_64-unknown-linux-gnu' -DCONF_VENDOR='unknown'
-DLOCALEDIR='/usr/local/share/locale' -DPACKAGE='bash' -DSHELL
-DHAVE_CONFIG_H   -I.  -I. -I./include -I./lib   -g  -o mksyntax
./mksyntax.c
*/tmp/cc1H53KR.o: file not recognized: File format not recognized*
collect2: ld returned 1 exit status
make: *** [mksyntax] Error 1

Furthermore, it's strange that the not recognized file keeping changed if I
execute 'make' again and again. For example, the second time I encounter
the next error message:

*/tmp/ccaJGvTn.o: file not recognized: File format not recognized*

BUT I found both file */tmp/cc1H53KR.o and **/tmp/ccaJGvTn.o *do not exist.

What's wrong? What should I do?


Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


[klee-dev] why different traces are generated under the same input?

2013-11-02 Thread Qiuping Yi
Hi,

I ran klee on 'findutils' under the same input without any symbolic
variable, and want to get a determinate execution. However, I get two
different executions randomly(one path with a bigger probability).  Why?
How can I get a determinate execution? Thank you very much.



Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


[klee-dev] How to preserve program variables?

2013-11-01 Thread Qiuping Yi
I am using klee-gcc to compile 'findutils', but I don't know why the
variables are all replaced with temp variables(such as %10), how can I
generate the bytecode and reserve the program variables. I used the next
commands without any optimization options:


   1.

   $ ../configure --disable-nls CFLAGS=-g
   2.

   $ make CC=/home/guest/installed/klee/scripts/klee-gcc



Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


Re: [klee-dev] How to preserve program variables?

2013-11-01 Thread Qiuping Yi
*I found the bytecode before linking had program variables, but the
generated target object had non. why?*
*
*
*Because during the 'make' step, I encountered an error: *

/home/guest/installed/klee/scripts/klee-gcc -Wdeclaration-after-statement
-Wall -g   -o find ftsfind.o ./libfindtools.a ../lib/libfind.a
../gnulib/lib/libgnulib.a  -lrt -lm -lm
/usr/bin/ld.bfd.real: cannot find crt1.o: No such file or directory
/usr/bin/ld.bfd.real: cannot find crti.o: No such file or directory
ftsfind.o: file not recognized: File format not recognized
collect2: ld returned 1 exit status

*so I use the next command by hand instead:*
llvm-ld -o find ftsfind.o ./libfindtools.a ../lib/libfind.a
../gnulib/lib/libgnulib.a  -L /usr/lib32/ -lrt -lm -lm

*when '-disable-opt' was added, the same output was generated. *

llvm-ld -disable-opt -o find ftsfind.o ./libfindtools.a ../lib/libfind.a
../gnulib/lib/libgnulib.a  -L /usr/lib32/ -lrt -lm -lm

*Does some error in my llvm-ld command? *





Qiuping Yi
Institute Of Software
Chinese Academy of Sciences


On Fri, Nov 1, 2013 at 4:20 PM, Qiuping Yi yiqiup...@gmail.com wrote:

 I am using klee-gcc to compile 'findutils', but I don't know why the
 variables are all replaced with temp variables(such as %10), how can I
 generate the bytecode and reserve the program variables. I used the next
 commands without any optimization options:


1.

$ ../configure --disable-nls CFLAGS=-g
2.

$ make CC=/home/guest/installed/klee/scripts/klee-gcc


 
 Qiuping Yi
 Institute Of Software
 Chinese Academy of Sciences

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


Re: [klee-dev] how to compile gnu utility 'find' using klee-gcc?

2013-10-31 Thread Qiuping Yi
Thank you, we have solved this problem following your instructions.



Qiuping Yi
Institute Of Software
Chinese Academy of Sciences


On Thu, Oct 31, 2013 at 10:04 AM, Hongxu Chen leftcopy@gmail.comwrote:

 Hi Yi,

I guess you need to read the original makefile and do some wrapper
 yourself instead of using klee-gcc.

From KLEE's coreutils case study page, Step 2(
 http://ccadar.github.io/klee/TestingCoreutils.html), There are such
 sentences:

  It depends on the actual project what the best way to do this is. For
 coreutils, we use a helper script klee-gcc, which acts like llvm-gcc but
 adds additional arguments to cause it  to emit LLVM bitcode files and to
 call llvm-ld to link executables. This is *not* a general solution, and
 your mileage may vary.

klee-gcc is a python script specified for coreutils bitcode generation.

To build bc instead of native code for general purpose, I think you can
 try wllvm.

 Thanks,
 Hongxu Chen



 On Thu, Oct 31, 2013 at 9:28 AM, Yi Zhou zhouyi198...@gmail.com wrote:

 Hi,

 I want to compile gnu utility 'find' to get an executed *.bc file, so I
 use the following commands:

 ./configure CC=/path/to/klee-gcc LD=/path/to/llvm-ld
 make
 make install

 However, at the end I did not get any *.bc file, and the generated file
 'find' is said to Invalid bitcode signature,but I can use the similar
 configure command to compile bosybox successfully. where is the error, and
 what should I do? Thank you all.

 Yi Zhou
 Institute Of Software
 Chinese Academy of Sciences

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



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


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


Re: [klee-dev] how to get a new copy of execution state?

2012-10-30 Thread Qiuping Yi
Thank you for your replay!

I want the constraints collected in b don't appear in a, and the changes on
the constraints of b don't affect a. I try the branch(), fork(), and its
constructors, but they don't work.


Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
___
klee-dev mailing list
klee-dev@keeda.stanford.edu
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev


[klee-dev] strange update on refExpr

2012-10-30 Thread Qiuping Yi
Hello, everyone

I got lost on the management of refExpr, my problem is followed:

Now I want to replace a kid of an Expr object with a new Expr, so I
implemented a new method Expr::setKid(int i, refExpr e), which replace
the i-th kid with e. It worked all right at first. But when I want to
update a Expr use its own value, for example, when i is increased with 1, I
want to update the old Expr (i+1) to ((i+1)+1):

(i+1)-
(Add w32 1
 (ReadLSB W32 0 i) )  to

((i+1)+1)---
(Add w32 1
 (Add w32 1
  (ReadLSB W32 0 i) ),

But I got a wrong Expr

N0:(Add w32 1 N0)

Why I can not get the right Expr through function setKid(). It seems that
Expr (i+1) (which was updated) and Expr (i+1) (the new value of i) shared
the same memory, how can I explicitly make these two refExpr have
different memory to solve this question. Thank you!


Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
___
klee-dev mailing list
klee-dev@keeda.stanford.edu
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev


[klee-dev] how to get a new copy of execution state?

2012-10-28 Thread Qiuping Yi
Hi,

Who can tell me how to clone a new ExecutionState b of an exist
ExecutionState a,
and the change on b won't affect a?

when I tried to use  ExecutionState *b = new ExecutionState(a);  to get a
copy b of a, and did
some change on b, I found a is also changed.


Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
___
klee-dev mailing list
klee-dev@keeda.stanford.edu
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev


Re: [klee-dev] error in Coreutils Case Study

2012-09-14 Thread Qiuping Yi
Hi,

yes, you are right!

I rebuilt my llvm and klee, now it's OK. Thank you very much!


Qiuping Yi
Institute Of Software
Chinese Academy of Sciences


2012/9/14 Delcypher delcyp...@gmail.com

 Hi,

 I'm not sure if the fact that your target triple i386-pc-linux-gnu is a
 problem as x86_64 as far as I know is a super set of i386. However it is
 surprising that your version of llvm-gcc is doing this which leads me to
 believe you might of downloaded the 32-bit version of llvm-gcc by mistake.

 If you run

 $ llvm-gcc -dumpmachine
 x86_64-unknown-linux-gnu

 And don't get x86_64-unknown-linux-gnu you know you have the wrong version
 (you can also run llvm-gcc --verbose to find out what options your
 compiler was built with too). The x86_64 version of llvm-gcc is here...
 http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2

 If it is the case that you had the 32-bit version of llvm-gcc I would
 advise rebuilding uclibc, llvm and KLEE from scratch using your 64-bit
 llvm-gcc compiler just to be sure nothing gets messed up.

 Hope that helps,

 Regards,
 Dan Liew.


 On 14 September 2012 03:28, Qiuping Yi yiqiup...@gmail.com wrote:

 Dear Dan Liew,

 Thanks for your detailed info.
 I followed you instructions, but I still have the error. And I got the
 next information.

 $ llvm-ld --version
 Low Level Virtual Machine (http://llvm.org/):
   llvm version 2.9
   Optimized build with assertions.
   Built Aug 12 2012 (10:31:59).
   Host: x86_64-unknown-linux-gnu
   Host CPU: penryn

   Registered Targets:
 (none)

 $ lli --version
 Low Level Virtual Machine (http://llvm.org/):
   llvm version 2.9
   Optimized build with assertions.
   Built Aug 12 2012 (10:31:59).
   Host: x86_64-unknown-linux-gnu
   Host CPU: penryn

   Registered Targets:
 x86- 32-bit X86: Pentium-Pro and above
 x86-64 - 64-bit X86: EM64T and AMD64

 *I checked the readable form of cat.bc, and I found the target triple is
 i386-pc-linux-gnu not **x86_64-unknown-linux-gnu*. I think it is the
 problem, how can I generate cat whose target triple is *
 x86_64-unknown-linux-gnu*?

 $ file /sbin/init
 /sbin/init: ELF 64-bit LSB shared object, x86-64, version 1 (SYSV),
 dynamically linked (uses shared libs), for GNU/Linux 2.6.24,
 BuildID[sha1]=0x029d6e45c81ad4eee2627f676b7580c9ed5fde47, stripped

 
 Qiuping Yi
 Institute Of Software
 Chinese Academy of Sciences


 2012/9/12 Delcypher delcyp...@gmail.com

 Hi,
 Could you make sure you reply to the mailing rather than just me, else
 no one else but me will see your problem!

 I'm sorry but I don't know why you're getting this new error message. I
 never had that problem but you could try the following

 0. Verify that you don't have multiple versions of LLVM installed. So
 verify that your output is similar to this...
 $ llvm-gcc --version
 llvm-gcc (GCC) 4.2.1 (Based on Apple Inc. build 5658) (LLVM build 2.9)

 $ llvm-ldd --version
 Low Level Virtual Machine (http://llvm.org/):
   llvm version 2.9
   Optimized build with assertions.

 $ lli --version
 Low Level Virtual Machine (http://llvm.org/):
   llvm version 2.9
   Optimized build with assertions.
   Built Jul 20 2012 (11:49:59).
   Host: x86_64-unknown-linux-gnu
   Host CPU: penryn

   Registered Targets:
 x86- 32-bit X86: Pentium-Pro and above
 x86-64 - 64-bit X86: EM64T and AMD64

 If lli doesn't have any registered targets then you will have
 problems! You will also have problems if your machines architecture is not
 listed.

 1. delete the obj-llvm directory
 2. Make sure LLVM_LIB_SEARCH_PATH is set
 3. Now make the obj-llvm directory. Make sure this folder is NOT in
 the source tree for core-utils, in the instructions it seems to be. I
 prefer having something like core-utils/src and core-utils/obj-llvm as the
 source code and build directories respectively.
 $ mkdir obj-llvm
 $ cd obj-llvm/
 $ ../src/configure --disable-nls CFLAGS=-g
 4. Run make
 $ make CC=/path/to/klee-gcc
 5. Now try again running cat again.

 If that fails inspect the produced bit code files (*.bc)

 $ llvm-dis cat.bc

 This will produce a cat.ll file. Which is the Bitcode file in human
 readable form, take a look and check your target triple is something like 
 x86_64-unknown-linux-gnu

 Other than that I have nothing more to suggest because I don't know much
 about LLVM.

 Thanks,
 Dan Liew.


 On 11 September 2012 15:28, Qiuping Yi yiqiup...@gmail.com wrote:

 yes, you are right. But after I executed *make
 CC=/full/path/to/klee/scripts/klee-gcc* successfully, I cannot
 successfully execute */cat --version* following the guide, and I got
 the next error information.

 qiu@qiu:~/installed/coreutils-6.11/obj-llvm/src$ ./cat --version
 lli: JITEmitter.cpp:1141: void
 {anonymous}::JITEmitter::emitJumpTableInfo(llvm::MachineJumpTableInfo*):
 Assertion `MJTI-getEntrySize(*TheJIT-getTargetData()) == sizeof(void*) 
 Cross JIT'ing?' failed.
 0  lli

Re: [klee-dev] error in Coreutils Case Study

2012-09-13 Thread Qiuping Yi
Dear Dan Liew,

Thanks for your detailed info.
I followed you instructions, but I still have the error. And I got the next
information.

$ llvm-ld --version
Low Level Virtual Machine (http://llvm.org/):
  llvm version 2.9
  Optimized build with assertions.
  Built Aug 12 2012 (10:31:59).
  Host: x86_64-unknown-linux-gnu
  Host CPU: penryn

  Registered Targets:
(none)

$ lli --version
Low Level Virtual Machine (http://llvm.org/):
  llvm version 2.9
  Optimized build with assertions.
  Built Aug 12 2012 (10:31:59).
  Host: x86_64-unknown-linux-gnu
  Host CPU: penryn

  Registered Targets:
x86- 32-bit X86: Pentium-Pro and above
x86-64 - 64-bit X86: EM64T and AMD64

*I checked the readable form of cat.bc, and I found the target triple is
i386-pc-linux-gnu not **x86_64-unknown-linux-gnu*. I think it is the
problem, how can I generate cat whose target triple is *
x86_64-unknown-linux-gnu*?

$ file /sbin/init
/sbin/init: ELF 64-bit LSB shared object, x86-64, version 1 (SYSV),
dynamically linked (uses shared libs), for GNU/Linux 2.6.24,
BuildID[sha1]=0x029d6e45c81ad4eee2627f676b7580c9ed5fde47, stripped


Qiuping Yi
Institute Of Software
Chinese Academy of Sciences


2012/9/12 Delcypher delcyp...@gmail.com

 Hi,
 Could you make sure you reply to the mailing rather than just me, else no
 one else but me will see your problem!

 I'm sorry but I don't know why you're getting this new error message. I
 never had that problem but you could try the following

 0. Verify that you don't have multiple versions of LLVM installed. So
 verify that your output is similar to this...
 $ llvm-gcc --version
 llvm-gcc (GCC) 4.2.1 (Based on Apple Inc. build 5658) (LLVM build 2.9)

 $ llvm-ldd --version
 Low Level Virtual Machine (http://llvm.org/):
   llvm version 2.9
   Optimized build with assertions.

 $ lli --version
 Low Level Virtual Machine (http://llvm.org/):
   llvm version 2.9
   Optimized build with assertions.
   Built Jul 20 2012 (11:49:59).
   Host: x86_64-unknown-linux-gnu
   Host CPU: penryn

   Registered Targets:
 x86- 32-bit X86: Pentium-Pro and above
 x86-64 - 64-bit X86: EM64T and AMD64

 If lli doesn't have any registered targets then you will have problems!
 You will also have problems if your machines architecture is not listed.

 1. delete the obj-llvm directory
 2. Make sure LLVM_LIB_SEARCH_PATH is set
 3. Now make the obj-llvm directory. Make sure this folder is NOT in the
 source tree for core-utils, in the instructions it seems to be. I prefer
 having something like core-utils/src and core-utils/obj-llvm as the source
 code and build directories respectively.
 $ mkdir obj-llvm
 $ cd obj-llvm/
 $ ../src/configure --disable-nls CFLAGS=-g
 4. Run make
 $ make CC=/path/to/klee-gcc
 5. Now try again running cat again.

 If that fails inspect the produced bit code files (*.bc)

 $ llvm-dis cat.bc

 This will produce a cat.ll file. Which is the Bitcode file in human
 readable form, take a look and check your target triple is something like 
 x86_64-unknown-linux-gnu

 Other than that I have nothing more to suggest because I don't know much
 about LLVM.

 Thanks,
 Dan Liew.


 On 11 September 2012 15:28, Qiuping Yi yiqiup...@gmail.com wrote:

 yes, you are right. But after I executed *make
 CC=/full/path/to/klee/scripts/klee-gcc* successfully, I cannot
 successfully execute */cat --version* following the guide, and I got
 the next error information.

 qiu@qiu:~/installed/coreutils-6.11/obj-llvm/src$ ./cat --version
 lli: JITEmitter.cpp:1141: void
 {anonymous}::JITEmitter::emitJumpTableInfo(llvm::MachineJumpTableInfo*):
 Assertion `MJTI-getEntrySize(*TheJIT-getTargetData()) == sizeof(void*) 
 Cross JIT'ing?' failed.
 0  lli 0x00b6edff
 1  lli 0x00b6f309
 2  libpthread.so.0 0x7f3595437cb0
 3  libc.so.6   0x7f359468d445 gsignal + 53
 4  libc.so.6   0x7f3594690bab abort + 379
 5  libc.so.6   0x7f359468610e
 6  libc.so.6   0x7f35946861b2
 7  lli 0x0078e8a6
 8  lli 0x0054dfc0
 9  lli 0x00b00acf
 llvm::FPPassManager::runOnFunction(llvm::Function) + 591
 10 lli 0x00b0150d
 llvm::FunctionPassManagerImpl::run(llvm::Function) + 141
 11 lli 0x00b016cd
 llvm::FunctionPassManager::run(llvm::Function) + 173
 12 lli 0x00780d8e
 llvm::JIT::jitTheFunction(llvm::Function*, llvm::MutexGuard const) + 46
 13 lli 0x0078114c
 llvm::JIT::runJITOnFunctionUnlocked(llvm::Function*, llvm::MutexGuard
 const) + 28
 14 lli 0x00781440
 llvm::JIT::getPointerToFunction(llvm::Function*) + 576
 15 lli 0x0077f677
 llvm::JIT::runFunction(llvm::Function*, std::vectorllvm::GenericValue,
 std::allocatorllvm::GenericValue  const) + 71
 16 lli 0x00a0f292
 llvm::ExecutionEngine::runFunctionAsMain(llvm::Function

[klee-dev] error in Coreutils Case Study

2012-09-11 Thread Qiuping Yi
Dear everyone,

I am a new user of klee, today I began to test the coreutils case study
following the
instructions in klee.llvm.org/TestingCoreutils.html. In the second step
(build coreutils with llvm),
I got the next error information when I executed *obj-llvm$ make
CC=/full/path/to/klee/scripts/klee-gcc* .
What should I do to correct the error? Thank you all very much!

/home/yq/installed/klee/scripts/klee-gcc  -g  -Wl,--as-needed -o chmod
chmod.o ../lib/libcoreutils.a  ../lib/libcoreutils.a
/home/yq/installed/klee/scripts/klee-gcc  -I. -I../../src -I../lib
 -I../../lib   -g -MT cp.o -MD -MP -MF .deps/cp.Tpo -c -o cp.o
../../src/cp.c
mv -f .deps/cp.Tpo .deps/cp.Po
/home/yq/installed/klee/scripts/klee-gcc  -I. -I../../src -I../lib
 -I../../lib   -g -MT copy.o -MD -MP -MF .deps/copy.Tpo -c -o copy.o
../../src/copy.c
mv -f .deps/copy.Tpo .deps/copy.Po
/home/yq/installed/klee/scripts/klee-gcc  -I. -I../../src -I../lib
 -I../../lib   -g -MT cp-hash.o -MD -MP -MF .deps/cp-hash.Tpo -c -o
cp-hash.o ../../src/cp-hash.c
mv -f .deps/cp-hash.Tpo .deps/cp-hash.Po
/home/yq/installed/klee/scripts/klee-gcc  -g  -Wl,--as-needed -o cp cp.o
copy.o cp-hash.o ../lib/libcoreutils.a  ../lib/libcoreutils.a
/home/yq/installed/klee/scripts/klee-gcc  -I. -I../../src -I../lib
 -I../../lib   -g -MT dd.o -MD -MP -MF .deps/dd.Tpo -c -o dd.o
../../src/dd.c
mv -f .deps/dd.Tpo .deps/dd.Po
/home/yq/installed/klee/scripts/klee-gcc  -g  -Wl,--as-needed -o dd dd.o
../lib/libcoreutils.a  ../lib/libcoreutils.a -lrt
llvm-ld: error: Cannot find library 'rt'
make[3]: *** [dd] Error 1
make[3]: Leaving directory `/home/qiu/installed/coreutils-6.11/obj-llvm/src'
make[2]: *** [all] Error 2
make[2]: Leaving directory `/home/qiu/installed/coreutils-6.11/obj-llvm/src'
make[1]: *** [all-recursive] Error 1
make[1]: Leaving directory `/home/qiu/installed/coreutils-6.11/obj-llvm'

Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
___
klee-dev mailing list
klee-dev@keeda.stanford.edu
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev