Dear all,
Attached is a patch I would like to submit for committing. They are changes
motivated by compiling and running klee under Minix, w.r.t. the latest SVN
HEAD (r146265), which builds and works again thanks to the latest API
adjustment, thanks to arrowdodger.
They are pretty minor fixes so I hope it's OK to submit them all in one
patch. Explanation:
. ntohs: takes a uint16_t, and compiler knows about the general prototype;
otherwise compiling breaks with the inconsistent declaration.
. <unistd.h> added in 2 files fixes missing prototypes
. added a KLEE_LIB_DIR and USE_KLEE_LIB_DIR facility to distinguish
searching for klee generated library files in the klee source directory vs.
in the installed location; this lets me make a binary-only klee package
(together with our compiler, clang/llvm) that can be used standalone by
Minix users, without the build directories installed. I have a pkgsrc
package for it at
http://git.minix3.org/?p=pkgsrc.git;a=tree;f=minix/clangnew;h=f7a88a0c62f8c325c46e3860991bff731ad9c169;hb=refs/heads/minix-masterif
you're interested. This will install klee along with the compiler out
of
the box under Minix.
. no stat64 under Minix
. ignore resource limits if RUSAGE_SELF isn't defined, i.e. getrusage() not
available
. Minix doesn't support mmap()ed files currently, but theMMap seemed to be
unused, so I hope it's okay to remove it (cleanest solution if possible).
I am looking forward to exploring the possibilities of improving Minix code
and test coverage using klee, and this package is a first step. Committing
the above would reduce our patch load significantly and will hopefully also
facilitate compiling and packaging for other platforms. Thanks for Klee,
I'm excited about it!
--
Regards,
Ben
Index: runtime/klee-libc/htonl.c
===================================================================
--- runtime/klee-libc/htonl.c (revision 146265)
+++ runtime/klee-libc/htonl.c (working copy)
@@ -41,7 +41,7 @@
#endif
-uint16_t ntohs(uint32_t v) {
+uint16_t ntohs(uint16_t v) {
return htons(v);
}
uint32_t ntohl(uint32_t v) {
Index: tools/klee/main.cpp
===================================================================
--- tools/klee/main.cpp (revision 146265)
+++ tools/klee/main.cpp (working copy)
@@ -51,6 +51,7 @@
#include <fstream>
#include <cerrno>
#include <dirent.h>
+#include <unistd.h>
#include <errno.h>
#include <sys/stat.h>
#include <sys/wait.h>
@@ -1213,7 +1214,14 @@
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
Interpreter::ModuleOptions Opts(LibraryDir.c_str(),
/*Optimize=*/OptimizeModule,
/*CheckDivZero=*/CheckDivZero);
Index: tools/gen-random-bout/gen-random-bout.cpp
===================================================================
--- tools/gen-random-bout/gen-random-bout.cpp (revision 146265)
+++ tools/gen-random-bout/gen-random-bout.cpp (working copy)
@@ -9,7 +9,7 @@
#include "klee/Internal/ADT/KTest.h"
-#ifdef __FreeBSD__
+#if defined(__FreeBSD__) || defined(__minix)
#define stat64 stat
#endif
Index: Makefile.common
===================================================================
--- Makefile.common (revision 146265)
+++ Makefile.common (working copy)
@@ -36,7 +36,7 @@
LD.Flags += -L$(PROJ_SRC_ROOT)/stp/lib
CXX.Flags += -I$(PROJ_SRC_ROOT)/stp/include
endif
-CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\"
+CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\" -DKLEE_LIB_DIR=\"$(PROJ_libdir)\"
# For STP.
CXX.Flags += -DEXT_HASH_MAP
Index: stp/sat/Solver.h
===================================================================
--- stp/sat/Solver.h (revision 146265)
+++ stp/sat/Solver.h (working copy)
@@ -315,9 +315,14 @@
#include <sys/resource.h>
static inline double cpuTime(void) {
+#ifndef RUSAGE_SELF
+ return 0;
+#else
struct rusage ru;
getrusage(RUSAGE_SELF, &ru);
- return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000;
}
+ return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000;
+#endif
+ }
#if defined(__linux__) || defined(__CYGWIN__)
static inline int memReadStat(int field)
@@ -342,9 +347,14 @@
//defined(__FreeBSD__)
static inline int64 memUsed(void) {
+#ifndef RUSAGE_SELF
+ return 0;
+#else
struct rusage ru;
getrusage(RUSAGE_SELF, &ru);
- return ru.ru_maxrss*1024; }
+ return ru.ru_maxrss*1024;
+#endif
+ }
#endif
Index: lib/Core/Executor.cpp
===================================================================
--- lib/Core/Executor.cpp (revision 146265)
+++ lib/Core/Executor.cpp (working copy)
@@ -258,9 +258,6 @@
}
-static void *theMMap = 0;
-static unsigned theMMapSize = 0;
-
namespace klee {
RNG theRNG;
}
@@ -3267,11 +3264,6 @@
if (statsTracker)
statsTracker->done();
-
- if (theMMap) {
- munmap(theMMap, theMMapSize);
- theMMap = 0;
- }
}
unsigned Executor::getPathStreamID(const ExecutionState &state) {
Index: lib/Solver/Solver.cpp
===================================================================
--- lib/Solver/Solver.cpp (revision 146265)
+++ lib/Solver/Solver.cpp (working copy)
@@ -29,6 +29,7 @@
#include <vector>
#include <errno.h>
+#include <unistd.h>
#include <signal.h>
#include <sys/wait.h>
#include <sys/ipc.h>
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
