Commit 6f290d8f authored by Daniel Dunbar's avatar Daniel Dunbar
Browse files

Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8
parent a55960ed
......@@ -11,8 +11,7 @@ Developed by:
klee Team
Stanford Checking Group: Daniel Dunbar, Cristian Cadar, Peter
Pawlowki, Dawson Engler.
Stanford Checking Group
http://klee.llvm.org
......@@ -30,10 +29,10 @@ so, subject to the following conditions:
this list of conditions and the following disclaimers in the
documentation and/or other materials provided with the distribution.
* Neither the names of the LLVM Team, University of Illinois at
Urbana-Champaign, nor the names of its contributors may be used to
endorse or promote products derived from this Software without specific
prior written permission.
* Neither the names of the klee Team, Stanford University, nor the
names of its contributors may be used to endorse or promote
products derived from this Software without specific prior
written permission.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
......@@ -50,10 +49,9 @@ This file will describe the copyrights, license, and restrictions which apply
to that code.
The disclaimer of warranty in the University of Illinois Open Source License
applies to all code in the klee Distribution, and nothing in any of the
other licenses gives permission to use the names of the klee Team or the
University of Illinois to endorse or promote products derived from this
Software.
applies to all code in the klee Distribution, and nothing in any of the other
licenses gives permission to use the names of the klee Team or Stanford
University to endorse or promote products derived from this Software.
The following pieces of software have additional or alternate copyrights,
licenses, and/or restrictions:
......@@ -61,4 +59,5 @@ licenses, and/or restrictions:
Program Directory
------- ---------
STP klee/stp
klee-libc runtime/klee-libc
#===-- klee/Makefile ---------------------------------------*- Makefile -*--===#
#
# The KLEE Symbolic Virtual Machine
#
# This file is distributed under the University of Illinois Open Source
# License. See LICENSE.TXT for details.
#
#===------------------------------------------------------------------------===#
#
# Indicates our relative path to the top of the project's root directory.
#
LEVEL = .
DIRS = stp lib tools runtime
EXTRA_DIST = include
# Only build support directories when building unittests.
ifeq ($(MAKECMDGOALS),unittests)
DIRS := $(filter-out tools runtime, $(DIRS)) unittests
OPTIONAL_DIRS :=
endif
#
# Include the Master Makefile that knows how to build all.
#
include $(LEVEL)/Makefile.common
.PHONY: doxygen
doxygen:
doxygen docs/doxygen.cfg
.PHONY: cscope.files
cscope.files:
find \
lib include stp tools runtime examples unittests \
-name Makefile -or \
-name \*.in -or \
-name \*.c -or \
-name \*.cpp -or \
-name \*.exp -or \
-name \*.inc -or \
-name \*.h | sort > cscope.files
test::
-(cd test/ && make)
.PHONY: klee-cov
klee-cov:
rm -rf klee-cov
zcov-scan --look-up-dirs=1 klee.zcov .
zcov-genhtml --root $$(pwd) klee.zcov klee-cov
clean::
$(MAKE) -C test clean
$(MAKE) -C unittests clean
rm -rf docs/doxygen
# -*- Makefile -*-
include $(LEVEL)/Makefile.config
# Include LLVM's Master Makefile config and rules.
include $(LLVM_OBJ_ROOT)/Makefile.config
ifeq ($(BYTECODE_LIBRARY), 1)
#
# Override make variables based on the runtime configuration. We want
# to override whatever the user may have said on the command line,
# hence the use of override.
#
override ENABLE_OPTIMIZED := $(RUNTIME_ENABLE_OPTIMIZED)
override DISABLE_ASSERTIONS := $(RUNTIME_DISABLE_ASSERTIONS)
override ENABLE_PROFILING := $(RUNTIME_ENABLE_PROFILING)
override ENABLE_COVERAGE := $(RUNTIME_ENABLE_COVERAGE)
endif
include $(LLVM_OBJ_ROOT)/Makefile.rules
LD.Flags += -L$(PROJ_SRC_ROOT)/stp/lib
CXX.Flags += -DLLVM_23
CXX.Flags += -I$(PROJ_SRC_ROOT)/stp/include
CXX.Flags += -DKLEE_DIR=\"$(PROJ_SRC_ROOT)\"
# -*- Makefile -*-
# Set the name of the project here
PROJECT_NAME := klee
PROJ_VERSION := 0.01
# Set this variable to the top of the LLVM source tree.
LLVM_SRC_ROOT = @LLVM_SRC@
# Set this variable to the top level directory where LLVM was built
# (this is *not* the same as OBJ_ROOT as defined in LLVM's Makefile.config).
LLVM_OBJ_ROOT = @LLVM_OBJ@
# Set the directory root of this project's source files
PROJ_SRC_ROOT := $(subst //,/,@abs_top_srcdir@)
# Set the root directory of this project's object files
PROJ_OBJ_ROOT := $(subst //,/,@abs_top_objdir@)
# Set the root directory of this project's install prefix
PROJ_INSTALL_ROOT := @prefix@
ENABLE_POSIX_RUNTIME := @ENABLE_POSIX_RUNTIME@
ENABLE_STPLOG := @ENABLE_STPLOG@
ENABLE_UCLIBC := @ENABLE_UCLIBC@
HAVE_SELINUX := @HAVE_SELINUX@
RUNTIME_ENABLE_OPTIMIZED := @RUNTIME_ENABLE_OPTIMIZED@
RUNTIME_DISABLE_ASSERTIONS :=
RUNTIME_ENABLE_COVERAGE :=
RUNTIME_ENABLE_PROFILING :=
# A list of "features" which tests can check for in XFAIL:
TEST_FEATURE_LIST :=
ifeq ($(HAVE_SELINUX_SELINUX_H),1)
TEST_FEATURE_LIST += have-selinux
else
TEST_FEATURE_LIST += no-selinux
endif
CFLAGS := @CFLAGS@
CXXFLAGS := @CXXFLAGS@
LDFLAGS := @LDFLAGS@
//===----------------------------------------------------------------------===//
// Klee Symbolic Virtual Machine
//===----------------------------------------------------------------------===//
Daniel Dunbar
klee is a symbolic virtual machine built on top of the LLVM compiler
infrastructure. Currently, there are two primary components.
infrastructure. Currently, there are two primary components:
1. The core symbolic virtual machine engine; this is responsible for
executing LLVM bitcode modules with support for symbolic values. This
is comprised of the code in lib/.
1. The core symbolic virtual machine engine; this is responsible for
executing LLVM bitcode modules with support for symbolic
values. This is comprised of the code in lib/.
2. An emulation layer for the Linux system call interface, with
additional support for making parts of the operating environment
symbolic. This is found in models/simple.
2. A POSIX/Linux emulation layer oriented towards supporting uClibc,
with additional support for making parts of the operating system
environment symbolic.
Additionally, there is a simple library in runtime/ which supports
replaying computed inputs on native code. There is a more complicated
library in replay/ which supports running inputs computed as part of
the system call emulation layer natively -- setting up files, pipes,
etc. on the native system to match the inputs that the emulation layer
provided.
Additionally, there is a simple library for replaying computed inputs
on native code (for closed programs). There is also a more complicated
infrastructure for replaying the inputs generated for the POSIX/Linux
emulation layer, which handles running native programs in an
environment that matches a computed test input, including setting up
files, pipes, environment variables, and passing command line
arguments.
For further information, see the docs in www/.
For further information, see the webpage or docs in www/.
TODO
--
Build System / Configure / Release Cleanups
--
o Rename .bout to .ktest (klee test)
o Rename .pc to .kquery (kleaver query)
o Configure doesn't check for bison / flex, we don't really use these
for anything important (just the command line STP tool), it would
be nice if they weren't required.
o Need a way to hide LLVM options in "klee --help".
Klee Internal
--
o Make sure that namespaces and .cpp locations match with reorganized
include locations.
o Add replay framework for POSIX model tests.
Kleaver Internal
--
o We need to fix the constants-in-exprs problem, this makes
separating out a Kleaver expr library much more difficult. There
are two parts:
1. Pull fast (pure constant) path operations out of Expr.cpp,
into Executor.cpp.
2. Lift constants-are-immediate optimization out of ref<Expr>
into Cell. Expressions in memory already have the concrete
cache, so we get that part for free.
We will need a way to distinguish if a cell has an expr or a
constant. Incidentally, this gives us an extra sentinel value
(is-expr == true and Expr* == null) we can use to mark
uninitialized-value of a register.
It may be worth sinking Expr construction into a Builder class
while we are at it.
There is a also a nice cleanup/perf win where we can work with
registers (Cells) directly, now that we build the constant table,
it might be worth doing this at the same time. This exposes a win
for IVC where it can write back a constant value into a register,
which needs to be done with care but would be a big improvement for
IVC.
o The stpArray field of an UpdateNode needs to die. This isn't as
easy as dropping it from the map, because we also need a
notification to free it. I think probably what we should do is
introduce an ExprContext can be used to deal with such things.
o The ExprContext could also have the default builder, for
example, which would make it easy to swap in an optimizing
builder.
#!/bin/sh
if ([ "$#" != 1 ] ||
[ ! -d "$1" ] ||
[ ! -d "$1/autoconf/m4" ]); then
echo "usage: $0 <llvmsrc-dir>" 1>& 2
exit 1
fi
llvm_src_root=$(cd $1; pwd)
llvm_m4=$llvm_src_root/autoconf/m4
die () {
echo "$@" 1>&2
exit 1
}
test -d autoconf && test -f autoconf/configure.ac && cd autoconf
test -f configure.ac || die "Can't find 'autoconf' dir; please cd into it first"
autoconf --version | egrep '2\.60' > /dev/null
if test $? -ne 0 ; then
die "Your autoconf was not detected as being 2.60"
fi
# Patch LLVM_SRC_ROOT in configure.ac
sed -e "s#^LLVM_SRC_ROOT=.*#LLVM_SRC_ROOT=\"$llvm_src_root\"#" \
configure.ac > configure.tmp.ac
echo "Regenerating aclocal.m4 with aclocal"
rm -f aclocal.m4
echo aclocal -I $llvm_m4 -I "$llvm_m4/.." || die "aclocal failed"
aclocal -I $llvm_m4 -I "$llvm_m4/.." || die "aclocal failed"
echo "Regenerating configure with autoconf 2.60"
echo autoconf --warnings=all -o ../configure configure.tmp.ac || die "autoconf failed"
autoconf --warnings=all -o ../configure configure.tmp.ac || die "autoconf failed"
cp ../configure ../configure.bak
sed -e "s#^LLVM_SRC_ROOT=.*#LLVM_SRC_ROOT=\".\"#" \
../configure.bak > ../configure
cd ..
echo "Regenerating config.h.in with autoheader"
autoheader --warnings=all \
-I autoconf -I autoconf/m4 \
autoconf/configure.tmp.ac || die "autoheader failed"
rm -f autoconf/configure.tmp.ac configure.bak
exit 0
This diff is collapsed.
This diff is collapsed.
dnl **************************************************************************
dnl * Initialize
dnl **************************************************************************
AC_INIT([[KLEE]],[[0.01]],[daniel@minormatter.com])
dnl Identify where LLVM source tree is (this is patched by
dnl AutoRegen.sh)
LLVM_SRC_ROOT=XXX
dnl Tell autoconf that the auxilliary files are actually located in
dnl the LLVM autoconf directory, not here.
AC_CONFIG_AUX_DIR($LLVM_SRC_ROOT/autoconf)
dnl Tell autoconf that this is an LLVM project being configured
dnl This provides the --with-llvmsrc and --with-llvmobj options
LLVM_CONFIG_PROJECT("","")
dnl Verify that the source directory is valid
AC_CONFIG_SRCDIR(["Makefile.config.in"])
dnl Configure a common Makefile
AC_CONFIG_FILES(Makefile.config)
AC_CONFIG_FILES(stp/Makefile.common)
dnl Configure project makefiles
dnl List every Makefile that exists within your source tree
AC_CONFIG_HEADERS([include/klee/Config/config.h])
dnl FIXME: Make out of tree builds work.
AC_LANG([C++])
dnl **************************************************************************
dnl Find the host
AC_CANONICAL_TARGET
dnl Determine the platform type and cache its value. This helps us configure
dnl the System library to the correct build platform.
AC_CACHE_CHECK([type of operating system we're going to host on],
[klee_cv_os_type],
[case $host in
*-*-linux*)
host_supports_posix_runtime=yes ;;
*)
host_supports_posix_runtime=no ;;
esac])
dnl **************************************************************************
dnl Verify that we can find llvm
dnl --with-llvm is a shortcut for setting srcdir and objdir.
AC_ARG_WITH(llvm,
AS_HELP_STRING([--with-llvm],
[Location of LLVM Source and Object code]),,)
AC_MSG_CHECKING([llvm source dir])
if test X${with_llvm} != X; then
dnl Verify that --with-llvm{src,obj} were not given.
if test X${with_llvmsrc} != X; then
AC_MSG_ERROR([--with-llvmsrc cannot be specified when using --with-llvm])
fi
if test X${with_llvmobj} != X; then
AC_MSG_ERROR([--with-llvmobj cannot be specified when using --with-llvm])
fi
with_llvmsrc=$with_llvm
with_llvmobj=$with_llvm
fi
dnl If one of with_llvmsrc or with_llvmobj was given, we must have both.
if (test X${with_llvmsrc} != X || test X${with_llvmobj} != X); then
dnl Verify that with_llvmobj was given as well.
if test X${with_llvmsrc} = X; then
AC_MSG_ERROR([--with-llvmsrc must be specified when using --with-llvmobj])
fi
if test X${with_llvmobj} = X; then
AC_MSG_ERROR([--with-llvmobj must be specified when using --with-llvmsrc])
fi
else
dnl Otherwise try and use llvm-config to find.
llvm_version=`llvm-config --version`
if test X${llvm_version} = X; then
AC_MSG_ERROR([unable to find llvm, use --with-llvmsrc and --with-llvmobj])
fi
with_llvmsrc=`llvm-config --src-root`
with_llvmobj=`llvm-config --obj-root`
fi
dnl Try to validate directories
if test ! -f ${with_llvmsrc}/Makefile.rules; then
AC_MSG_ERROR([invalid llvmsrc directory: ${with_llvmsrc}])
fi
if test ! -f ${with_llvmobj}/Makefile.config; then
AC_MSG_ERROR([invalid llvmobj directory: ${with_llvmobj}])
fi
dnl Make the paths absolute
llvm_src=`cd $with_llvmsrc 2> /dev/null; pwd`
llvm_obj=`cd $with_llvmobj 2> /dev/null; pwd`
AC_MSG_RESULT([$llvm_src])
dnl Report obj dir as well.
AC_MSG_CHECKING([llvm obj dir])
AC_MSG_RESULT([$llvm_obj])
AC_SUBST(LLVM_SRC,$llvm_src)
AC_SUBST(LLVM_OBJ,$llvm_obj)
dnl **************************************************************************
dnl User option to enable uClibc support.
AC_ARG_WITH(uclibc,
AS_HELP_STRING([--with-uclibc],
[Enable use of the klee uclibc at the given path]),,)
dnl If uclibc wasn't given, check for a uclibc in the current
dnl directory.
if (test X${with_uclibc} = X && test -d uclibc); then
with_uclibc=uclibc
fi
dnl Validate uclibc if given.
AC_MSG_CHECKING([uclibc])
if (test X${with_uclibc} != X); then
if test ! -d ${with_uclibc}; then
AC_MSG_ERROR([invalid uclibc directory: ${with_uclibc}])
fi
dnl Make the path absolute
with_uclibc=`cd $with_uclibc 2> /dev/null; pwd`
AC_MSG_RESULT([$with_uclibc])
else
AC_MSG_RESULT([no])
fi
AC_DEFINE_UNQUOTED(KLEE_UCLIBC, "$with_uclibc", [Path to KLEE's uClibc])
AC_SUBST(KLEE_UCLIBC)
if test X${with_uclibc} != X ; then
AC_SUBST(ENABLE_UCLIBC,[[1]])
else
AC_SUBST(ENABLE_UCLIBC,[[0]])
fi
dnl **************************************************************************
dnl User option to enable the POSIX runtime
AC_ARG_ENABLE(posix-runtime,
AS_HELP_STRING([--enable-posix-runtime],
[Enable the POSIX runtime]),
,enableval=default)
AC_MSG_CHECKING([POSIX runtime])
if test ${enableval} = "default" ; then
if test X${with_uclibc} != X; then
enableval=$host_supports_posix_runtime
if test ${enableval} = "yes"; then
AC_MSG_RESULT([default (enabled)])
else
AC_MSG_RESULT([default (disabled, unsupported target)])
fi
else
enableval="no"
AC_MSG_RESULT([default (disabled, no uclibc)])
fi
else
if test ${enableval} = "yes" ; then
AC_MSG_RESULT([yes])
else
AC_MSG_RESULT([no])
fi
fi
if test ${enableval} = "yes" ; then
AC_SUBST(ENABLE_POSIX_RUNTIME,[[1]])
else
AC_SUBST(ENABLE_POSIX_RUNTIME,[[0]])
fi
dnl **************************************************************************
dnl User option to select runtime version
AC_ARG_WITH(runtime,
AS_HELP_STRING([--with-runtime],
[Select build configuration for runtime libraries (default [Release])]),,
withval=default)
if test X"${withval}" = Xdefault; then
with_runtime=Release
fi
AC_MSG_CHECKING([runtime configuration])
if test X${with_runtime} = XRelease; then
AC_MSG_RESULT([Release])
AC_SUBST(RUNTIME_ENABLE_OPTIMIZED,[[1]])
elif test X${with_runtime} = XDebug; then
AC_MSG_RESULT([Debug])
AC_SUBST(RUNTIME_ENABLE_OPTIMIZED,[[0]])
else
AC_MSG_ERROR([invalid configuration: ${with_runtime}])
fi
AC_DEFINE_UNQUOTED(RUNTIME_CONFIGURATION, "$with_runtime", [Configuration for runtime libraries])
AC_SUBST(RUNTIME_CONFIGURATION)
dnl **************************************************************************
dnl See if we should support __ctype_b_loc externals.
dnl FIXME: Do the proper test if we continue to need this.
case $host in
*-*-linux*)
AC_DEFINE_UNQUOTED(HAVE_CTYPE_EXTERNALS, 1, [Does the platform use __ctype_b_loc, etc.])
esac
dnl **************************************************************************
dnl Checks for header files.
dnl NOTE: This is mostly just to force autoconf to make CFLAGS defines
dnl for us.
AC_LANG_PUSH([C])
AC_CHECK_HEADERS([sys/acl.h])
AC_LANG_POP([C])
AC_CHECK_HEADERS([selinux/selinux.h],
AC_SUBST(HAVE_SELINUX, 1),
AC_SUBST(HAVE_SELINUX, 0))
dnl User option to use stplog.
AC_ARG_ENABLE(stplog,
AS_HELP_STRING([--enable-stplog],
[Compile with the stplog library [[disabled]]]),
,enableval=no)
if test ${enableval} = "yes" ; then
AC_SUBST(ENABLE_STPLOG,[[1]])
else
AC_SUBST(ENABLE_STPLOG,[[0]])
fi
AC_DEFINE_UNQUOTED([ENABLE_STPLOG],$ENABLE_STPLOG,[Define if stplog enabled])
dnl **************************************************************************
dnl * Create the output files
dnl **************************************************************************
dnl This must be last
AC_OUTPUT
#!/bin/sh
# install - install a program, script, or datafile
scriptversion=2004-09-10.20
# This originates from X11R5 (mit/util/scripts/install.sh), which was
# later released in X11R6 (xc/config/util/install.sh) with the
# following copyright and license.
#
# Copyright (C) 1994 X Consortium
#
# Permission is hereby granted, free of charge, to any person obtaining a copy
# of this software and associated documentation files (the "Software"), to
# deal in the Software without restriction, including without limitation the
# rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
# sell copies of the Software, and to permit persons to whom the Software is
# furnished to do so, subject to the following conditions:
#
# The above copyright notice and this permission notice shall be included in
# all copies or substantial portions of the Software.
#
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
# X CONSORTIUM BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
# AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNEC-
# TION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
#
# Except as contained in this notice, the name of the X Consortium shall not
# be used in advertising or otherwise to promote the sale, use or other deal-
# ings in this Software without prior written authorization from the X Consor-
# tium.
#
#
# FSF changes to this file are in the public domain.
#
# Calling this script install-sh is preferred over install.sh, to prevent
# `make' implicit rules from creating a file called install from it
# when there is no Makefile.
#
# This script is compatible with the BSD install script, but was written
# from scratch. It can only install one file at a time, a restriction
# shared with many OS's install programs.
# set DOITPROG to echo to test this script
# Don't use :- since 4.3BSD and earlier shells don't like it.
doit="${DOITPROG-}"
# put in absolute paths if you don't have them in your path; or use env. vars.
mvprog="${MVPROG-mv}"
cpprog="${CPPROG-cp}"
chmodprog="${CHMODPROG-chmod}"
chownprog="${CHOWNPROG-chown}"
chgrpprog="${CHGRPPROG-chgrp}"
stripprog="${STRIPPROG-strip}"
rmprog="${RMPROG-rm}"
mkdirprog="${MKDIRPROG-mkdir}"
chmodcmd="$chmodprog 0755"
chowncmd=
chgrpcmd=
stripcmd=
rmcmd="$rmprog -f"
mvcmd="$mvprog"
src=
dst=
dir_arg=
dstarg=
no_target_directory=
usage="Usage: $0 [OPTION]... [-T] SRCFILE DSTFILE