klee-uclibc detection is now a lot cleaner. KLEE now assumes

it can find klee-uclibc inside the same folder as the other
runtime libraries with the name "klee-uclibc.bca"

This is implemented as follows:

* When building, a sym-link is created to klee-uclibc's libc.a file
  in the same directory that the rest of KLEE's runtime libraries
  are built. This done so that if a developer changes klee-uclibc
  on their system then the correct version of klee-uclibc is used
  by KLEE.

* When installing, klee-uclibc's libc.a file is installed in the same
  directory that the rest of KLEE's runtime libraries are installed.

In addition the configure script argument --with-uclibc can now
operate in two ways. It can either be passed the path to the root
of klee-uclibc or it can be passed a path to the libc.a file built
by klee-uclibc. This new behaviour has been added to allow users
to potential use pre-built versions of klee-uclibc.

8 files changed, 144 insertions, 55 deletions

diff --git a/Makefile.common b/Makefile.common
index 21985db1..e5e3c18a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -30,11 +30,18 @@ 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_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/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 faf53439..f9698fdf 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -1006,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;
@@ -1030,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
@@ -1094,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");
 
 
@@ -1148,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
@@ -1281,7 +1284,7 @@ int main(int argc, char **argv, char **envp) {
   }
 
   case UcLibc:
-    mainModule = linkWithUclibc(mainModule);
+    mainModule = linkWithUclibc(mainModule, LibraryDir);
     break;
   }