Problem with compiling KLEE

Vinay T S (vinayts)

2013-12-29 09:53:15 UTC

Hello,

My setup details :

/root/bin/stp : compiled from STP r940 code base .

[***@vinayts-lab-lnx klee-master]# which llvm-gcc
/usr/bin/llvm-gcc
[***@vinayts-lab-lnx klee-master]# llvm-gcc --version
llvm-gcc (GCC) 4.2.1 (Based on Apple Inc. build 5658) (LLVM build 2.9)
Copyright (C) 2007 Free Software Foundation, Inc.
This is free software; see the source for copying conditions. There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

Could install ucLibC from the instructions provided at : http://ccadar.github.io/klee/GetStarted.html

[***@vinayts-lab-lnx klee-master]# uname -a
Linux vinayts-lab-lnx 2.6.18-194.8.1.el5 #1 SMP Wed Jun 23 10:52:51 EDT 2010 x86_64 x86_64 x86_64 GNU/Linux

[***@vinayts-lab-lnx klee-master]# gcc -v
Using built-in specs.
Target: x86_64-unknown-linux-gnu
Configured with: ../gcc-4.2.4/configure --prefix=/usr --libexecdir=/usr/lib --enable-shared --enable-threads=posix --enable-__cxa_atexit --enable-clocale=gnu --enable-languages=c,c++,fortran,java,objc,treelang
Thread model: posix
gcc version 4.2.4

Am trying to build KLEE now ( picked up the latest downloadable version from github) .

Ran into some issues :

[***@vinayts-lab-lnx klee-master]# pwd
/usr/local/src/klee-master

make ENABLE_OPTIMIZED=1 -j10

make[1]: Entering directory `/usr/local/src/klee-master/lib'
make[2]: Entering directory `/usr/local/src/klee-master/lib/Support'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/lib/Support'
make[2]: Entering directory `/usr/local/src/klee-master/lib/Basic'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/lib/Basic'
make[2]: Entering directory `/usr/local/src/klee-master/lib/Solver'
make[2]: Entering directory `/usr/local/src/klee-master/lib/Expr'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/lib/Expr'
llvm[2]: Compiling STPBuilder.cpp for Release+Asserts build
llvm[2]: Compiling Solver.cpp for Release+Asserts build
make[2]: Entering directory `/usr/local/src/klee-master/lib/Module'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/lib/Module'
make[2]: Entering directory `/usr/local/src/klee-master/lib/Core'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/lib/Core'
In file included from STPBuilder.h:14,
from Solver.cpp:14:
/usr/local/src/klee-master/include/klee/util/ArrayExprHash.h:135:7: warning: no newline at end of file
In file included from STPBuilder.h:14,
from STPBuilder.cpp:10:
/usr/local/src/klee-master/include/klee/util/ArrayExprHash.h:135:7: warning: no newline at end of file
llvm[2]: Building Release+Asserts Archive Library libkleaverSolver.a
make[2]: Leaving directory `/usr/local/src/klee-master/lib/Solver'
make[1]: Leaving directory `/usr/local/src/klee-master/lib'
make[1]: Entering directory `/usr/local/src/klee-master/tools'
make[2]: Entering directory `/usr/local/src/klee-master/tools/klee-stats'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/tools/klee-stats'
make[2]: Entering directory `/usr/local/src/klee-master/tools/ktest-tool'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/tools/ktest-tool'
make[2]: Entering directory `/usr/local/src/klee-master/tools/gen-random-bout'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/tools/gen-random-bout'
make[2]: Entering directory `/usr/local/src/klee-master/tools/klee-replay'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/tools/klee-replay'
perl: warning: Setting locale failed.
perl: warning: Please check that your locale settings:
LANGUAGE = (unset),
LC_ALL = (unset),
LC_CTYPE = "UTF-8",
LANG = "en_US.UTF-8"
are supported and installed on your system.
perl: warning: Falling back to the standard locale ("C").
perl: warning: Setting locale failed.
perl: warning: Please check that your locale settings:
LANGUAGE = (unset),
LC_ALL = (unset),
LC_CTYPE = "UTF-8",
LANG = "en_US.UTF-8"
are supported and installed on your system.
perl: warning: Falling back to the standard locale ("C").
perl: warning: Setting locale failed.
perl: warning: Please check that your locale settings:
LANGUAGE = (unset),
LC_ALL = (unset),
LC_CTYPE = "UTF-8",
LANG = "en_US.UTF-8"
are supported and installed on your system.
perl: warning: Falling back to the standard locale ("C").
perl: warning: Setting locale failed.
perl: warning: Please check that your locale settings:
LANGUAGE = (unset),
LC_ALL = (unset),
LC_CTYPE = "UTF-8",
LANG = "en_US.UTF-8"
are supported and installed on your system.
perl: warning: Falling back to the standard locale ("C").
make[2]: Entering directory `/usr/local/src/klee-master/tools/kleaver'
llvm[2]: Linking Release+Asserts executable kleaver (without symbols)
make[2]: Entering directory `/usr/local/src/klee-master/tools/klee'
llvm[2]: Compiling main.cpp for Release+Asserts build
In file included from /usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
from /usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
from main.cpp:32:
/usr/local/src/llvm-2.9/include/llvm/Config/config.h:641:1: warning: "PACKAGE_BUGREPORT" redefined
In file included from /usr/local/src/klee-master/include/klee/Config/Version.h:13,
from /usr/local/src/klee-master/include/klee/util/Bits.h:13,
from /usr/local/src/klee-master/include/klee/Expr.h:13,
from /usr/local/src/klee-master/include/klee/Constraints.h:13,
from /usr/local/src/klee-master/include/klee/ExecutionState.h:13,
from main.cpp:6:
/usr/local/src/klee-master/include/klee/Config/config.h:59:1: warning: this is the location of the previous definition
In file included from /usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
from /usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
from main.cpp:32:
/usr/local/src/llvm-2.9/include/llvm/Config/config.h:644:1: warning: "PACKAGE_NAME" redefined
In file included from /usr/local/src/klee-master/include/klee/Config/Version.h:13,
from /usr/local/src/klee-master/include/klee/util/Bits.h:13,
from /usr/local/src/klee-master/include/klee/Expr.h:13,
from /usr/local/src/klee-master/include/klee/Constraints.h:13,
from /usr/local/src/klee-master/include/klee/ExecutionState.h:13,
from main.cpp:6:
/usr/local/src/klee-master/include/klee/Config/config.h:62:1: warning: this is the location of the previous definition
In file included from /usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
from /usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
from main.cpp:32:
/usr/local/src/llvm-2.9/include/llvm/Config/config.h:647:1: warning: "PACKAGE_STRING" redefined
In file included from /usr/local/src/klee-master/include/klee/Config/Version.h:13,
from /usr/local/src/klee-master/include/klee/util/Bits.h:13,
from /usr/local/src/klee-master/include/klee/Expr.h:13,
from /usr/local/src/klee-master/include/klee/Constraints.h:13,
from /usr/local/src/klee-master/include/klee/ExecutionState.h:13,
from main.cpp:6:
/usr/local/src/klee-master/include/klee/Config/config.h:65:1: warning: this is the location of the previous definition
In file included from /usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
from /usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
from main.cpp:32:
/usr/local/src/llvm-2.9/include/llvm/Config/config.h:650:1: warning: "PACKAGE_TARNAME" redefined
In file included from /usr/local/src/klee-master/include/klee/Config/Version.h:13,
from /usr/local/src/klee-master/include/klee/util/Bits.h:13,
from /usr/local/src/klee-master/include/klee/Expr.h:13,
from /usr/local/src/klee-master/include/klee/Constraints.h:13,
from /usr/local/src/klee-master/include/klee/ExecutionState.h:13,
from main.cpp:6:
/usr/local/src/klee-master/include/klee/Config/config.h:68:1: warning: this is the location of the previous definition
In file included from /usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
from /usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
from main.cpp:32:
/usr/local/src/llvm-2.9/include/llvm/Config/config.h:653:1: warning: "PACKAGE_VERSION" redefined
In file included from /usr/local/src/klee-master/include/klee/Config/Version.h:13,
from /usr/local/src/klee-master/include/klee/util/Bits.h:13,
from /usr/local/src/klee-master/include/klee/Expr.h:13,
from /usr/local/src/klee-master/include/klee/Constraints.h:13,
from /usr/local/src/klee-master/include/klee/ExecutionState.h:13,
from main.cpp:6:
/usr/local/src/klee-master/include/klee/Config/config.h:74:1: warning: this is the location of the previous definition
llvm[2]: ======= Finished Linking Release+Asserts Executable kleaver (without symbols)
make[2]: Leaving directory `/usr/local/src/klee-master/tools/kleaver'
main.cpp: In function 'void parseArguments(int, char**)':
main.cpp:653: warning: cast from type 'const char**' to type 'char**' casts away constness
main.cpp: In function 'int main(int, char**, char**)':
main.cpp:1263: error: ISO C++ forbids taking address of function '::main'
main.cpp:1263: warning: ISO C++ forbids casting between pointer-to-function and pointer-to-object
make[2]: *** [/usr/local/src/klee-master/tools/klee/Release+Asserts/main.o] Error 1
make[2]: Leaving directory `/usr/local/src/klee-master/tools/klee'
make[1]: *** [klee/.makeall] Error 2
make[1]: Leaving directory `/usr/local/src/klee-master/tools'
make: *** [all] Error 1

On examining line 1263 :

1262 : llvm::sys::Path LibraryDir = KleeHandler::getRunTimeLibraryPath(argv[0],
1263 : reinterpret_cast<void*>(main));
1264 : Interpreter::ModuleOptions Opts(LibraryDir.c_str(),

Seems like gcc 4.2.4 does not like this ( in line 1263) . I am not too good at C++, wanted to check how to get around this compilation issue .

Thanks
Vinay

Daniel Liew

2013-12-29 12:43:45 UTC

Permalink

Hi Vinay,

This is due to a change I added recently. I need to replace it with
something because the LLVM API I used is deprecated and taking the
address of main isn't supposed to be allowed in ISO C++.

Provided you only run KLEE from the build directory (i.e. you do not
try to install it and then run the installed version) then you can
checkout a slightly older copy without support for KLEE running from
an install directory which doesn't have the code which is causing you
issues.

$ cd klee-src-directory/
$ git checkout 857831d18708ada4590c511494d3ae5f94cf6a6a

Could you add this issue to our issue tracker [1]. I need to fix this
at some point.

[1] https://github.com/ccadar/klee/issues

Thanks,
Dan.

Post by Vinay T S (vinayts)
Hello,
/root/bin/stp : compiled from STP r940 code base .
/usr/bin/llvm-gcc
llvm-gcc (GCC) 4.2.1 (Based on Apple Inc. build 5658) (LLVM build 2.9)
Copyright (C) 2007 Free Software Foundation, Inc.
This is free software; see the source for copying conditions. There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
http://ccadar.github.io/klee/GetStarted.html
Linux vinayts-lab-lnx 2.6.18-194.8.1.el5 #1 SMP Wed Jun 23 10:52:51 EDT 2010
x86_64 x86_64 x86_64 GNU/Linux
Using built-in specs.
Target: x86_64-unknown-linux-gnu
Configured with: ../gcc-4.2.4/configure --prefix=/usr --libexecdir=/usr/lib
--enable-shared --enable-threads=posix --enable-__cxa_atexit
--enable-clocale=gnu --enable-languages=c,c++,fortran,java,objc,treelang
Thread model: posix
gcc version 4.2.4
Am trying to build KLEE now ( picked up the latest downloadable version from
github) .
/usr/local/src/klee-master
make ENABLE_OPTIMIZED=1 -j10
make[1]: Entering directory `/usr/local/src/klee-master/lib'
make[2]: Entering directory `/usr/local/src/klee-master/lib/Support'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/lib/Support'
make[2]: Entering directory `/usr/local/src/klee-master/lib/Basic'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/lib/Basic'
make[2]: Entering directory `/usr/local/src/klee-master/lib/Solver'
make[2]: Entering directory `/usr/local/src/klee-master/lib/Expr'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/lib/Expr'
llvm[2]: Compiling STPBuilder.cpp for Release+Asserts build
llvm[2]: Compiling Solver.cpp for Release+Asserts build
make[2]: Entering directory `/usr/local/src/klee-master/lib/Module'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/lib/Module'
make[2]: Entering directory `/usr/local/src/klee-master/lib/Core'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/lib/Core'
In file included from STPBuilder.h:14,
no newline at end of file
In file included from STPBuilder.h:14,
no newline at end of file
llvm[2]: Building Release+Asserts Archive Library libkleaverSolver.a
make[2]: Leaving directory `/usr/local/src/klee-master/lib/Solver'
make[1]: Leaving directory `/usr/local/src/klee-master/lib'
make[1]: Entering directory `/usr/local/src/klee-master/tools'
make[2]: Entering directory `/usr/local/src/klee-master/tools/klee-stats'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/tools/klee-stats'
make[2]: Entering directory `/usr/local/src/klee-master/tools/ktest-tool'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/tools/ktest-tool'
make[2]: Entering directory
`/usr/local/src/klee-master/tools/gen-random-bout'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory
`/usr/local/src/klee-master/tools/gen-random-bout'
make[2]: Entering directory `/usr/local/src/klee-master/tools/klee-replay'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/usr/local/src/klee-master/tools/klee-replay'
perl: warning: Setting locale failed.
LANGUAGE = (unset),
LC_ALL = (unset),
LC_CTYPE = "UTF-8",
LANG = "en_US.UTF-8"
are supported and installed on your system.
perl: warning: Falling back to the standard locale ("C").
perl: warning: Setting locale failed.
LANGUAGE = (unset),
LC_ALL = (unset),
LC_CTYPE = "UTF-8",
LANG = "en_US.UTF-8"
are supported and installed on your system.
perl: warning: Falling back to the standard locale ("C").
perl: warning: Setting locale failed.
LANGUAGE = (unset),
LC_ALL = (unset),
LC_CTYPE = "UTF-8",
LANG = "en_US.UTF-8"
are supported and installed on your system.
perl: warning: Falling back to the standard locale ("C").
perl: warning: Setting locale failed.
LANGUAGE = (unset),
LC_ALL = (unset),
LC_CTYPE = "UTF-8",
LANG = "en_US.UTF-8"
are supported and installed on your system.
perl: warning: Falling back to the standard locale ("C").
make[2]: Entering directory `/usr/local/src/klee-master/tools/kleaver'
llvm[2]: Linking Release+Asserts executable kleaver (without symbols)
make[2]: Entering directory `/usr/local/src/klee-master/tools/klee'
llvm[2]: Compiling main.cpp for Release+Asserts build
In file included from
/usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
from
/usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
"PACKAGE_BUGREPORT" redefined
In file included from
/usr/local/src/klee-master/include/klee/Config/Version.h:13,
from
/usr/local/src/klee-master/include/klee/util/Bits.h:13,
from /usr/local/src/klee-master/include/klee/Expr.h:13,
from
/usr/local/src/klee-master/include/klee/Constraints.h:13,
from
/usr/local/src/klee-master/include/klee/ExecutionState.h:13,
/usr/local/src/klee-master/include/klee/Config/config.h:59:1: warning: this
is the location of the previous definition
In file included from
/usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
from
/usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
"PACKAGE_NAME" redefined
In file included from
/usr/local/src/klee-master/include/klee/Config/Version.h:13,
from
/usr/local/src/klee-master/include/klee/util/Bits.h:13,
from /usr/local/src/klee-master/include/klee/Expr.h:13,
from
/usr/local/src/klee-master/include/klee/Constraints.h:13,
from
/usr/local/src/klee-master/include/klee/ExecutionState.h:13,
/usr/local/src/klee-master/include/klee/Config/config.h:62:1: warning: this
is the location of the previous definition
In file included from
/usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
from
/usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
"PACKAGE_STRING" redefined
In file included from
/usr/local/src/klee-master/include/klee/Config/Version.h:13,
from
/usr/local/src/klee-master/include/klee/util/Bits.h:13,
from /usr/local/src/klee-master/include/klee/Expr.h:13,
from
/usr/local/src/klee-master/include/klee/Constraints.h:13,
from
/usr/local/src/klee-master/include/klee/ExecutionState.h:13,
/usr/local/src/klee-master/include/klee/Config/config.h:65:1: warning: this
is the location of the previous definition
In file included from
/usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
from
/usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
"PACKAGE_TARNAME" redefined
In file included from
/usr/local/src/klee-master/include/klee/Config/Version.h:13,
from
/usr/local/src/klee-master/include/klee/util/Bits.h:13,
from /usr/local/src/klee-master/include/klee/Expr.h:13,
from
/usr/local/src/klee-master/include/klee/Constraints.h:13,
from
/usr/local/src/klee-master/include/klee/ExecutionState.h:13,
/usr/local/src/klee-master/include/klee/Config/config.h:68:1: warning: this
is the location of the previous definition
In file included from
/usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
from
/usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
"PACKAGE_VERSION" redefined
In file included from
/usr/local/src/klee-master/include/klee/Config/Version.h:13,
from
/usr/local/src/klee-master/include/klee/util/Bits.h:13,
from /usr/local/src/klee-master/include/klee/Expr.h:13,
from
/usr/local/src/klee-master/include/klee/Constraints.h:13,
from
/usr/local/src/klee-master/include/klee/ExecutionState.h:13,
/usr/local/src/klee-master/include/klee/Config/config.h:74:1: warning: this
is the location of the previous definition
llvm[2]: ======= Finished Linking Release+Asserts Executable kleaver
(without symbols)
make[2]: Leaving directory `/usr/local/src/klee-master/tools/kleaver'
main.cpp:653: warning: cast from type 'const char**' to type 'char**' casts
away constness
main.cpp:1263: error: ISO C++ forbids taking address of function '::main'
main.cpp:1263: warning: ISO C++ forbids casting between pointer-to-function
and pointer-to-object
make[2]: *** [/usr/local/src/klee-master/tools/klee/Release+Asserts/main.o]
Error 1
make[2]: Leaving directory `/usr/local/src/klee-master/tools/klee'
make[1]: *** [klee/.makeall] Error 2
make[1]: Leaving directory `/usr/local/src/klee-master/tools'
make: *** [all] Error 1
1262 : llvm::sys::Path LibraryDir =
KleeHandler::getRunTimeLibraryPath(argv[0],
1263 : reinterpret_cast<void*>(main));
1264 : Interpreter::ModuleOptions Opts(LibraryDir.c_str(),
Seems like gcc 4.2.4 does not like this ( in line 1263) . I am not too good
at C++, wanted to check how to get around this compilation issue .
Thanks
Vinay