[klee-dev] Problems compiling KLEE/STP

[Daniel Liew]

It's actually no longer a requirement for llvm-gcc to be in your PATH
when building LLVM. It is only needed in your PATH when building KLEE.
See [1] . I need to update the documentation to reflect this.

Looking at the error message, I see Luis is having issues with the
mess that is klee-uclibc.

@Luis: If you're feeling brave you can try using [2] and make sure you
use the klee_0_9_29 branch. It is an improved (history is cleaner)
version of klee-uclibc that has an improved configure script that does
not rely on the llvm-gcc being detected at LLVM configure time. To
build make sure llvm-gcc, llvm-ar and llvm-dis (must be version 2.9)
are in your path then do

$ ./configure -l
$ make

This version of klee-uclibc hasn't been tested much but it passes all
the KLEE tests on 64-bit, is a lot easier to build and even supports
clang! Note you need python >=2.7 for the configure script to work.


[1] https://github.com/ccadar/klee/commit/dbe21a488ca0f99d77df6bc1c11107b12cc00d8d
[2] https://github.com/ccadar/klee-uclibc/tree/klee_0_9_29

Thanks,
Dan.

On 2 December 2013 17:13, Urmas Repinski <urrimus at hotmail.com> wrote:
> Hi Luis.
>
> According to installation manual,
> http://ccadar.github.io/klee/GetStarted.html
> In order to install LLVM-29, first, necessary to install llvm-gcc first.
> It is important to do this first so that llvm-gcc is found in subsequent
> configure steps. llvm-gcc will be used later to compile programs that KLEE
> can execute.
>
> So possibly llvm-gcc were installed with error or wrong version of llvm-gcc
> were downloaded.
> Try to download fresh copy - GCC of LLVM Version 2.9. There is different
> GCC-s are available to download so possibly you choosed 32-bit version
> instead of 64-bit, or vise versa.
>
> Try to reinstall then LLVM with new GCC version, if problem is with LLVM-GCC
> installation, then problem is there.
>
> I used
>
> LLVM-GCC 4.2 Front End Binaries for FreeBSD8/x86 (23M) (.sig)
>
>
> for my installation, and it worked fine.
>
> Urmas Repinski.
> ________________________________
> Date: Mon, 2 Dec 2013 09:41:33 -0700
> Subject: Re: [klee-dev] Problems compiling KLEE/STP
> From: lumi.martinez at gmail.com
> To: urrimus at hotmail.com; klee-dev at imperial.ac.uk
>
> Urmas,
> Thanks for your help. I was able to build STP.
>
> However, I'm still having trouble with building Klee and re-building LLVM.
>
> Let me start with a question: Should llvm-2.9 be built with the normal GCC
> or with llvm-gcc? What about klee?
>
> When I tried compiling KLEE, I get the emit-llvm error. Here's the output:
> /bin/sh: 0: Illegal option --
> make: --emit-llvm: Command not found
> make: --emit-llvm: Command not found
> ./extra/scripts/conf-header.sh .config > include/bits/uClibc_config.h
> /bin/sh: 0: Illegal option --
> make[1]: --emit-llvm: Command not found
> make[1]: --emit-llvm: Command not found
> extra/scripts/gen_bits_syscall_h.sh: 30:
> extra/scripts/gen_bits_syscall_h.sh: --emit-llvm: not found
> extra/scripts/gen_bits_syscall_h.sh: 26:
> extra/scripts/gen_bits_syscall_h.sh: --emit-llvm: not found
>   CC libcrypt/crypt.os
> /bin/sh: 1: --emit-llvm: not found
> make: *** [libcrypt/crypt.os] Error 127
>
> I googled it and found that the problem is related to the fact that I am not
> compiling with llvm-gcc. For sure, llvm-gcc is in the path:
>
> /home/lumi/Development/llvm-gcc4.2-2.9-x86_64-linux/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games
>
> Any ideas how to solve this?
>
> Help is really appreciated.
>
> Luis
>
>
>
> On Tue, Nov 26, 2013 at 4:46 AM, Urmas Repinski <urrimus at hotmail.com> wrote:
>
> Hi Luis.
>
> I had reached several errors during my klee installation, and, fortunately,
> i have script, that allows to install klee on 64-bit Linux Mint 13 OS with
> no errors, attaching script to the letter.
>
> During step 3 i had made following modifications:
>
> STP="stp"
> # change revision number to  1180 on 64 bit system, 940 on 32 bit system
> # --with-fpic configure option is required on 64 bit machines
>
> echo " Package $STP"
> svn co -r 1180
> https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp
> $INSTALLDIR/$STP
> (cd $INSTALLDIR/$STP; ./scripts/configure    --with-fpic  ; make
> OPTIMIZE=-O2 CFLAGS_M32= install ; ulimit -s unlimited  )
>
> I used revision 1190 of STP instead of 940 for 64 bit machine, used
> CFLAGS_M32=install flag for make, used flag --with-fpic for configure.
>
> Hope this helps.
>
> Urmas.
>
>
> ________________________________
> Date: Mon, 25 Nov 2013 15:52:37 -0700
> From: lumi.martinez at gmail.com
> To: klee-dev at keeda.stanford.edu
> Subject: [klee-dev] Problems compiling KLEE/STP
>
>
> Hi guys,
> I'm having trouble compiling STP as instructed by
> http://ccadar.github.io/klee/GetStarted.html
> (step 3)
>
> I am running in a Ubuntu 12.04 LTS Linux 64-bit machine.
>
> After failing to build with my default toolchain GCC 4.6.3, I installed
> version 3.4.6 of gcc, gcc-base, g++, cpp, libstdc++6 via:
> $ wget http://old-releases.ubuntu.com/ubuntu/pool/universe/g/gcc-3.4/*.deb
> (I put each separately)
> $ sudo dpkg -i *.deb
>
> I didn't update binutils nor make.
>
> I ran...
> $ ./scripts/configure --with-prefix=/home/(myname)/stp
> --with-cryptominisat2, and...
> $ make CC=gcc-3.4 CXX=g++-3.4 OPTIMIZE=-O2 CFLAGS_M32=
>
> But still I get lots of warnings and an error that I print below:
>
> In file included from Gaussian.h:32,
>                  from Logger.cpp:36:
> PackedMatrix.h: In member function `MINISAT::PackedRow
> MINISAT::PackedMatrix::iterator::operator*()':
> PackedRow.h:224: error: `MINISAT::PackedRow::PackedRow(uint32_t, uint64_t*)'
> is private
> PackedMatrix.h:141: error: within this context
> Logger.cpp: In member function `void
> MINISAT::Logger::end(MINISAT::Logger::finish_type)':
> Logger.cpp:375: warning: cast to pointer from integer of different size
> make[2]: *** [Logger.o] Error 1
> make[2]: Leaving directory
> `/home/(myname)/llvm-2.9/stp/src/sat/cryptominisat2'
> make[1]: *** [cryptominisat2] Error 2
> make[1]: Leaving directory `/home/(myname)/llvm-2.9/stp/src/sat'
> make: *** [all] Error 2
>
> Any ideas of what this error is and how to resolve it?
>
> Help is truly appreciated.
>
> Thanks,
> Luis
>
>
> _______________________________________________ klee-dev mailing list
> klee-dev at imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>