about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile6
-rw-r--r--Makefile.common10
-rw-r--r--Makefile.config.in2
-rw-r--r--autoconf/configure.ac54
-rwxr-xr-xconfigure48
-rw-r--r--include/klee/Config/config.h.in6
-rw-r--r--lib/Basic/Makefile1
-rwxr-xr-xlib/Core/Makefile1
-rw-r--r--lib/Expr/Makefile1
-rwxr-xr-xlib/Module/Makefile1
-rwxr-xr-xlib/Solver/Makefile3
-rw-r--r--lib/Support/Makefile1
-rw-r--r--runtime/Makefile4
-rw-r--r--runtime/klee-uclibc/Makefile53
-rw-r--r--tools/klee/main.cpp64
15 files changed, 190 insertions, 65 deletions
diff --git a/Makefile b/Makefile
index 1612efc1..2e02e578 100644
--- a/Makefile
+++ b/Makefile
@@ -14,6 +14,12 @@ LEVEL = .
 
 include $(LEVEL)/Makefile.config
 
+# The header files are normally installed
+# by the install-local target in the top-level
+# makefile. This disables installing anything
+# in the top-level makefile.
+NO_INSTALL=1
+
 DIRS = lib tools runtime
 EXTRA_DIST = include
 
diff --git a/Makefile.common b/Makefile.common
index 3f60bbec..e5e3c18a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -30,9 +30,17 @@ endif
 # Needed to build runtime library using clang (gnu89 is the gcc default)
 C.Flags += -std=gnu89
 
+# This is filename that KLEE will look for when trying to load klee-uclibc
+KLEE_UCLIBC_BCA_NAME="klee-uclibc.bca"
+
 LD.Flags += -L$(STP_ROOT)/lib
 CXX.Flags += -I$(STP_ROOT)/include
-CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\" -DKLEE_LIB_DIR=\"$(PROJ_libdir)\"
+CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\" -DKLEE_INSTALL_BIN_DIR=\"$(PROJ_bindir)\"
+CXX.Flags += -DKLEE_INSTALL_LIB_DIR=\"$(PROJ_libdir)\"
+
+ifeq ($(ENABLE_UCLIBC),1)
+	CXX.Flags += -DKLEE_UCLIBC_BCA_NAME=\"$(KLEE_UCLIBC_BCA_NAME)\"
+endif
 
 # For STP.
 CXX.Flags += -DEXT_HASH_MAP
diff --git a/Makefile.config.in b/Makefile.config.in
index 9e04711b..35f7bcfe 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -36,6 +36,8 @@ ENABLE_POSIX_RUNTIME := @ENABLE_POSIX_RUNTIME@
 ENABLE_STPLOG := @ENABLE_STPLOG@
 ENABLE_UCLIBC := @ENABLE_UCLIBC@
 
+KLEE_UCLIBC_BCA := @KLEE_UCLIBC_BCA@
+
 HAVE_SELINUX := @HAVE_SELINUX@
 
 RUNTIME_ENABLE_OPTIMIZED := @RUNTIME_ENABLE_OPTIMIZED@
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index fd249103..5a47e924 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -341,38 +341,52 @@ 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
+                 [Enable use of the klee uclibc at the given path (klee-uclibc root directory or libc.a file]),,)
 
 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}])
+   if test  -d ${with_uclibc}; then
+      dnl Support the legacy way of configuring with 
+      dnl klee-uclibc, i.e. the root klee-uclibc
+      dnl directory is passed as an argument.
+
+      dnl Make the path absolute
+      with_uclibc=`cd $with_uclibc 2> /dev/null; pwd`
+
+      dnl create path to libc file
+      KLEE_UCLIBC_BCA="${with_uclibc}/lib/libc.a"
+
+      if test ! -e "${KLEE_UCLIBC_BCA}"; then
+      AC_MSG_ERROR([Could not find file ${KLEE_UCLIBC_BCA}])
+      fi
+   elif test -f ${with_uclibc}; then
+      dnl Support the new way of configuring klee-uclibc
+      dnl i.e. the built bitcode archive is passed as the
+      dnl argument.
+
+      dnl Get absolute path to file
+      _kud=`dirname ${with_uclibc}`
+      _kud=`cd ${_kud}; pwd 2> /dev/null`
+      _kuf=`basename ${with_uclibc}`
+
+      KLEE_UCLIBC_BCA="${_kud}/${_kuf}" 
+   else
+      AC_MSG_ERROR([Could not detect klee-uclibc])
    fi
 
-   dnl Make the path absolute
-   with_uclibc=`cd $with_uclibc 2> /dev/null; pwd`
+   dnl FIXME: Validate the libc.a file
 
-   AC_MSG_RESULT([$with_uclibc])
+   AC_MSG_RESULT([$KLEE_UCLIBC_BCA])
+   AC_SUBST(ENABLE_UCLIBC,[[1]])
+   AC_SUBST(KLEE_UCLIBC_BCA)
+   AC_DEFINE(SUPPORT_KLEE_UCLIBC, [[1]], [klee-uclibc is supported])
 else
    AC_MSG_RESULT([no])
+   AC_SUBST(ENABLE_UCLIBC,[[0]])
 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
diff --git a/configure b/configure
index 6eda1243..85e7fec2 100755
--- a/configure
+++ b/configure
@@ -649,8 +649,8 @@ RUNTIME_DEBUG_SYMBOLS
 RUNTIME_DISABLE_ASSERTIONS
 RUNTIME_ENABLE_OPTIMIZED
 ENABLE_POSIX_RUNTIME
+KLEE_UCLIBC_BCA
 ENABLE_UCLIBC
-KLEE_UCLIBC
 KLEE_BITCODE_CXX_COMPILER
 KLEE_BITCODE_C_COMPILER
 clang_cxx
@@ -1374,6 +1374,7 @@ Optional Packages:
                           (Default: auto-detect). If set, --with-llvmcc= must
                           be set too.
   --with-uclibc           Enable use of the klee uclibc at the given path
+                          (klee-uclibc root directory or libc.a file
   --with-runtime          Select build configuration for runtime libraries
                           (default [Release+Asserts])
   --with-stp              Location of STP installation directory
@@ -2991,43 +2992,48 @@ if test "${with_uclibc+set}" = set; then :
 fi
 
 
-if (test X${with_uclibc} = X && test -d uclibc); then
-   with_uclibc=uclibc
-fi
-
 
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking uclibc" >&5
 $as_echo_n "checking uclibc... " >&6; }
 if (test X${with_uclibc} != X); then
-   if test ! -d ${with_uclibc}; then
-       as_fn_error $? "invalid uclibc directory: ${with_uclibc}" "$LINENO" 5
-   fi
+   if test  -d ${with_uclibc}; then
 
-      with_uclibc=`cd $with_uclibc 2> /dev/null; pwd`
+            with_uclibc=`cd $with_uclibc 2> /dev/null; pwd`
 
-   { $as_echo "$as_me:${as_lineno-$LINENO}: result: $with_uclibc" >&5
-$as_echo "$with_uclibc" >&6; }
-else
-   { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
-$as_echo "no" >&6; }
-fi
+            KLEE_UCLIBC_BCA="${with_uclibc}/lib/libc.a"
 
+      if test ! -e "${KLEE_UCLIBC_BCA}"; then
+      as_fn_error $? "Could not find file ${KLEE_UCLIBC_BCA}" "$LINENO" 5
+      fi
+   elif test -f ${with_uclibc}; then
+
+            _kud=`dirname ${with_uclibc}`
+      _kud=`cd ${_kud}; pwd 2> /dev/null`
+      _kuf=`basename ${with_uclibc}`
+
+      KLEE_UCLIBC_BCA="${_kud}/${_kuf}"
+   else
+      as_fn_error $? "Could not detect klee-uclibc" "$LINENO" 5
+   fi
 
-cat >>confdefs.h <<_ACEOF
-#define KLEE_UCLIBC "$with_uclibc"
-_ACEOF
 
+   { $as_echo "$as_me:${as_lineno-$LINENO}: result: $KLEE_UCLIBC_BCA" >&5
+$as_echo "$KLEE_UCLIBC_BCA" >&6; }
+   ENABLE_UCLIBC=1
 
 
-if test X${with_uclibc} != X ; then
-  ENABLE_UCLIBC=1
+
+$as_echo "#define SUPPORT_KLEE_UCLIBC 1" >>confdefs.h
 
 else
-  ENABLE_UCLIBC=0
+   { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+   ENABLE_UCLIBC=0
 
 fi
 
 
+
 # Check whether --enable-posix-runtime was given.
 if test "${enable_posix_runtime+set}" = set; then :
   enableval=$enable_posix_runtime;
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index 0a94de8f..3f6da802 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -45,9 +45,6 @@
 /* Define to 1 if you have the <unistd.h> header file. */
 #undef HAVE_UNISTD_H
 
-/* Path to KLEE's uClibc */
-#undef KLEE_UCLIBC
-
 /* LLVM version is release (instead of development) */
 #undef LLVM_IS_RELEASE
 
@@ -81,6 +78,9 @@
 /* Define to 1 if you have the ANSI C header files. */
 #undef STDC_HEADERS
 
+/* klee-uclibc is supported */
+#undef SUPPORT_KLEE_UCLIBC
+
 /* Supporting metaSMT API */
 #undef SUPPORT_METASMT
 
diff --git a/lib/Basic/Makefile b/lib/Basic/Makefile
index d4481e7f..e72399a2 100644
--- a/lib/Basic/Makefile
+++ b/lib/Basic/Makefile
@@ -12,5 +12,6 @@ LEVEL=../..
 LIBRARYNAME=kleeBasic
 DONT_BUILD_RELINKED=1
 BUILD_ARCHIVE=1
+NO_INSTALL=1
 
 include $(LEVEL)/Makefile.common
diff --git a/lib/Core/Makefile b/lib/Core/Makefile
index 4da3c7ea..f34f699d 100755
--- a/lib/Core/Makefile
+++ b/lib/Core/Makefile
@@ -12,5 +12,6 @@ LEVEL=../..
 LIBRARYNAME=kleeCore
 DONT_BUILD_RELINKED=1
 BUILD_ARCHIVE=1
+NO_INSTALL=1
 
 include $(LEVEL)/Makefile.common
diff --git a/lib/Expr/Makefile b/lib/Expr/Makefile
index b80569b3..25557600 100644
--- a/lib/Expr/Makefile
+++ b/lib/Expr/Makefile
@@ -12,5 +12,6 @@ LEVEL=../..
 LIBRARYNAME=kleaverExpr
 DONT_BUILD_RELINKED=1
 BUILD_ARCHIVE=1
+NO_INSTALL=1
 
 include $(LEVEL)/Makefile.common
diff --git a/lib/Module/Makefile b/lib/Module/Makefile
index bfd7c469..091a7d45 100755
--- a/lib/Module/Makefile
+++ b/lib/Module/Makefile
@@ -12,5 +12,6 @@ LEVEL=../..
 LIBRARYNAME=kleeModule
 DONT_BUILD_RELINKED=1
 BUILD_ARCHIVE=1
+NO_INSTALL=1
 
 include $(LEVEL)/Makefile.common
diff --git a/lib/Solver/Makefile b/lib/Solver/Makefile
index 2be74c01..a44b4f6e 100755
--- a/lib/Solver/Makefile
+++ b/lib/Solver/Makefile
@@ -12,6 +12,7 @@ LEVEL=../..
 LIBRARYNAME=kleaverSolver
 DONT_BUILD_RELINKED=1
 BUILD_ARCHIVE=1
+NO_INSTALL=1
 
 include $(LEVEL)/Makefile.common
 
@@ -22,4 +23,4 @@ ifeq ($(ENABLE_METASMT),1)
   CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags))
   CXX.Flags += $(metaSMT_CXXFLAGS)
   CXX.Flags += $(metaSMT_INCLUDES)
-endif
\ No newline at end of file
+endif
diff --git a/lib/Support/Makefile b/lib/Support/Makefile
index a1b46f3c..67272908 100644
--- a/lib/Support/Makefile
+++ b/lib/Support/Makefile
@@ -12,5 +12,6 @@ LEVEL=../..
 LIBRARYNAME=kleeSupport
 DONT_BUILD_RELINKED=1
 BUILD_ARCHIVE=1
+NO_INSTALL=1
 
 include $(LEVEL)/Makefile.common
diff --git a/runtime/Makefile b/runtime/Makefile
index 24824d08..7eb02d3f 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -23,4 +23,8 @@ ifeq ($(ENABLE_POSIX_RUNTIME),1)
 PARALLEL_DIRS += POSIX
 endif
 
+ifeq ($(ENABLE_UCLIBC),1)
+PARALLEL_DIRS += klee-uclibc
+endif
+
 include $(LEVEL)/Makefile.common
diff --git a/runtime/klee-uclibc/Makefile b/runtime/klee-uclibc/Makefile
new file mode 100644
index 00000000..1e848264
--- /dev/null
+++ b/runtime/klee-uclibc/Makefile
@@ -0,0 +1,53 @@
+#===-- runtime/klee-uclibc/Makefile --------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+# Note klee-uclibc does not really live here.  This makefile just manages the
+# location of the klee-uclibc bitcode archive when building and when installing
+# KLEE.
+
+LEVEL=../..
+
+# We're not really building a bytecode library here
+# but we need to set this so that $(BuildMode) is
+# set appropriately
+BYTECODE_LIBRARY=1
+
+include $(LEVEL)/Makefile.common
+
+# The purpose of setting up this symbolic link is
+# so that KLEE can always look for klee-uclibc
+# in the same place it looks for all the other
+# run time libraries
+uclibc_symlink:=$(PROJ_OBJ_ROOT)/$(BuildMode)/lib/$(KLEE_UCLIBC_BCA_NAME)
+#
+# Force our extra rules to run
+all-local:: $(uclibc_symlink)
+
+$(uclibc_symlink):
+	@echo "Setting up symbolic link to klee-uclibc"
+	$(Verb) ln -s -f $(KLEE_UCLIBC_BCA) $(uclibc_symlink)
+
+# The reasons for copying over klee-uclibc on install are
+#
+# * KLEE can look for klee-uclibc in the same place it looks for all other run
+#   time libraries. 
+# * KLEE can be more easily distributed with klee-uclibc
+
+install:: copy_klee_uclibc
+uninstall:: remove_klee_uclibc
+
+.PHONY: copy_klee_uclibc remove_klee_uclibc
+
+copy_klee_uclibc:
+	@echo "Installing klee-uclibc archive"
+	$(Verb) $(CP) $(KLEE_UCLIBC_BCA) $(DESTDIR)$(PROJ_libdir)/$(KLEE_UCLIBC_BCA_NAME)
+
+remove_klee_uclibc:
+	@echo "Removing klee-uclibc archive"
+	$(Verb) $(RM) $(DESTDIR)$(PROJ_libdir)/$(KLEE_UCLIBC_BCA_NAME)
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 3616bfa6..f9698fdf 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -34,6 +34,7 @@
 #include "llvm/Support/FileSystem.h"
 #include "llvm/Bitcode/ReaderWriter.h"
 #include "llvm/Support/CommandLine.h"
+#include "llvm/Support/Debug.h"
 #include "llvm/Support/ManagedStatic.h"
 #include "llvm/Support/MemoryBuffer.h"
 
@@ -257,6 +258,8 @@ public:
 
   static void getOutFiles(std::string path,
 			  std::vector<std::string> &results);
+
+  static llvm::sys::Path getRunTimeLibraryPath(const char* argv0, void *MainExecAddr);
 };
 
 KleeHandler::KleeHandler(int argc, char **argv) 
@@ -569,6 +572,32 @@ void KleeHandler::getOutFiles(std::string path,
   }
 }
 
+
+llvm::sys::Path KleeHandler::getRunTimeLibraryPath(const char* argv0, void* MainExecAddr)
+{
+  llvm::sys::Path toolRoot = llvm::sys::Path::GetMainExecutable(argv0, MainExecAddr);
+  toolRoot.eraseComponent(); // Strip off executable so we have a directory path
+
+  llvm::sys::Path libDir;
+
+  if ( strcmp(toolRoot.c_str(), KLEE_INSTALL_BIN_DIR ) == 0)
+  {
+    DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() <<
+                    "Using installed KLEE library runtime: ");
+    libDir = llvm::sys::Path( KLEE_INSTALL_LIB_DIR );
+  }
+  else
+  {
+    DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() <<
+                    "Using build directory KLEE library runtime :");
+    libDir = llvm::sys::Path(KLEE_DIR "/" RUNTIME_CONFIGURATION "/lib");
+  }
+
+  DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() <<
+                  libDir.c_str() << "\n");
+  return libDir;
+}
+
 //===----------------------------------------------------------------------===//
 // main Driver function
 //
@@ -977,8 +1006,8 @@ static char *format_tdiff(char *buf, long seconds)
   return buf;
 }
 
-#ifndef KLEE_UCLIBC
-static llvm::Module *linkWithUclibc(llvm::Module *mainModule) {
+#ifndef SUPPORT_KLEE_UCLIBC
+static llvm::Module *linkWithUclibc(llvm::Module *mainModule, llvm::sys::Path libDir) {
   fprintf(stderr, "error: invalid libc, no uclibc support!\n");
   exit(1);
   return 0;
@@ -1001,12 +1030,15 @@ static void replaceOrRenameFunction(llvm::Module *module,
   }
 }
 
-static llvm::Module *linkWithUclibc(llvm::Module *mainModule) {
-  // Ensure that KLEE_UCLIBC exists
-  bool uclibcRootExists=false;
-  llvm::sys::fs::is_directory(KLEE_UCLIBC, uclibcRootExists);
-  if (!uclibcRootExists)
-    klee_error("Cannot link with uclibc. KLEE_UCLIBC (\"" KLEE_UCLIBC "\") is not a directory.");
+static llvm::Module *linkWithUclibc(llvm::Module *mainModule, llvm::sys::Path libDir) {
+  // Ensure that klee-uclibc exists
+  llvm::sys::Path uclibcBCA(libDir);
+  uclibcBCA.appendComponent(KLEE_UCLIBC_BCA_NAME);
+
+  bool uclibcExists=false;
+  llvm::sys::fs::exists(uclibcBCA.c_str(), uclibcExists);
+  if (!uclibcExists)
+    klee_error("Cannot find klee-uclibc : %s", uclibcBCA.c_str());
 
   Function *f;
   // force import of __uClibc_main
@@ -1065,8 +1097,7 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule) {
     }
   }
   
-  mainModule = klee::linkWithLibrary(mainModule, 
-                                     KLEE_UCLIBC "/lib/libc.a");
+  mainModule = klee::linkWithLibrary(mainModule, uclibcBCA.c_str());
   assert(mainModule && "unable to link with uclibc");
 
 
@@ -1119,6 +1150,7 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule) {
   
   new UnreachableInst(getGlobalContext(), bb);
 
+  klee_message("NOTE: Using klee-uclibc : %s", uclibcBCA.c_str());
   return mainModule;
 }
 #endif
@@ -1227,14 +1259,8 @@ int main(int argc, char **argv, char **envp) {
       return r;
   }
 
-#if defined(KLEE_LIB_DIR) && defined(USE_KLEE_LIB_DIR)
-  /* KLEE_LIB_DIR is the lib dir of installed files as opposed to 
-   * where libs in the klee source tree are generated.
-   */
-  llvm::sys::Path LibraryDir(KLEE_LIB_DIR);
-#else
-  llvm::sys::Path LibraryDir(KLEE_DIR "/" RUNTIME_CONFIGURATION "/lib");
-#endif
+  llvm::sys::Path LibraryDir = KleeHandler::getRunTimeLibraryPath(argv[0], 
+                              reinterpret_cast<void*>(main));
   Interpreter::ModuleOptions Opts(LibraryDir.c_str(),
                                   /*Optimize=*/OptimizeModule, 
                                   /*CheckDivZero=*/CheckDivZero,
@@ -1258,7 +1284,7 @@ int main(int argc, char **argv, char **envp) {
   }
 
   case UcLibc:
-    mainModule = linkWithUclibc(mainModule);
+    mainModule = linkWithUclibc(mainModule, LibraryDir);
     break;
   }
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-22 22:38:59 +0000