SelectExpr simplifying and constant size lazy initialization

configs/options.json

@@ -7,7 +7,11 @@
         "maxSolverTime" : "5",
         "maxForks" : "200",
         "maxSymAlloc" : "32",
-        "symbolicAllocationThreshhold" : "2048"
+        "SymbolicAllocationThreshold" : "2048",
+        "minNumberElements" : "4",
+        "maxCycles" : 10,
+        "useSymbolicSizeLI" : false,
+        "writeKpaths": false
     },
     "configurations": [
         {
@@ -33,10 +37,13 @@
                 "--extern-calls-can-return-null",
                 "--align-symbolic-pointers=false",
                 "--write-no-tests",
-                "--write-kpaths",
+                "--write-kpaths=${writeKpaths}",
                 "--use-lazy-initialization=only",
+                "--min-number-elements-li=${minNumberElements}",
+                "--use-sym-size-li=${useSymbolicSizeLI}",
+                "--max-cycles=${maxCycles}",
                 "--rewrite-equalities=simple",
-                "--symbolic-allocation-threshhold=${symbolicAllocationThreshhold}",
+                "--symbolic-allocation-threshold=${SymbolicAllocationThreshold}",
                 "--analysis-reproduce=${sarifTracesFilePath}",
                 "${bytecodeFilePath}"
             ]

include/klee/Core/TerminationTypes.h

@@ -33,17 +33,17 @@
   TTYPE(ReadOnly, 17U, "read_only.err")                                        \
   TTYPE(ReportError, 18U, "report_error.err")                                  \
   TTYPE(UndefinedBehavior, 19U, "undefined_behavior.err")                      \
-  TTYPE(InternalOutOfMemory, 20U, "out_of_memory.er")                          \
-  MARK(PROGERR, 20U)                                                           \
+  TTYPE(InternalOutOfMemory, 20U, "out_of_memory.err")                         \
+  TTYPE(MissedAllTargets, 21U, "miss_all_targets.err")                         \
+  MARK(PROGERR, 21U)                                                           \
   TTYPE(User, 23U, "user.err")                                                 \
   MARK(USERERR, 23U)                                                           \
   TTYPE(Execution, 25U, "exec.err")                                            \
   TTYPE(External, 26U, "external.err")                                         \
   MARK(EXECERR, 26U)                                                           \
   TTYPE(Replay, 27U, "")                                                       \
   TTYPE(SilentExit, 28U, "")                                                   \
-  TTYPE(MissedAllTargets, 29U, "")                                             \
-  MARK(END, 29U)
+  MARK(END, 28U)
 
 ///@brief Reason an ExecutionState got terminated.
 enum class StateTerminationType : std::uint8_t {
@@ -61,6 +61,7 @@ enum Reason {
   MaxInstructions,
   MaxSteppedInstructions,
   MaxTime,
+  MaxCycles,
   CovCheck,
   NoMoreStates,
   ReachedTarget,

include/klee/Expr/Expr.h

@@ -321,6 +321,9 @@ class Expr {
   /// isZero - Is this a constant zero.
   bool isZero() const;
 
+  /// isZero - Is this a constant one.
+  bool isOne() const;
+
   /// isTrue - Is this the true expression.
   bool isTrue() const;
 
@@ -1553,6 +1556,12 @@ inline bool Expr::isZero() const {
   return false;
 }
 
+inline bool Expr::isOne() const {
+  if (const ConstantExpr *CE = dyn_cast<ConstantExpr>(this))
+    return CE->isOne();
+  return false;
+}
+
 inline bool Expr::isTrue() const {
   assert(getWidth() == Expr::Bool && "Invalid isTrue() call!");
   if (const ConstantExpr *CE = dyn_cast<ConstantExpr>(this))

include/klee/Expr/ExprVisitor.h

@@ -137,10 +137,9 @@ class ExprVisitor {
   virtual Action visitFNeg(const FNegExpr &);
   virtual Action visitFRint(const FRintExpr &);
 
-protected:
-  VisitorHash visited;
-
 private:
+  typedef ExprHashMap<ref<Expr>> visited_ty;
+  visited_ty visited;
   bool recursive;
 
   ref<Expr> visitActual(const ref<Expr> &e);

include/klee/Module/TargetForest.h

@@ -218,12 +218,35 @@ class TargetForest {
     static EquivTargetsHistoryHashSet cachedHistories;
     static TargetsHistoryHashSet histories;
     unsigned hashValue;
+    unsigned sizeValue;
 
     explicit History(ref<Target> _target, ref<History> _visitedTargets)
         : target(_target), visitedTargets(_visitedTargets) {
       computeHash();
     }
 
+    void computeHash() {
+      unsigned res = 0;
+      if (target) {
+        res = target->hash() * Expr::MAGIC_HASH_CONSTANT;
+      }
+      if (visitedTargets) {
+        res ^= visitedTargets->hash() * Expr::MAGIC_HASH_CONSTANT;
+      }
+      hashValue = res;
+    }
+
+    void computeSize() {
+      unsigned res = 0;
+      if (target) {
+        ++res;
+      }
+      if (visitedTargets) {
+        res += visitedTargets->size();
+      }
+      sizeValue = res;
+    }
+
   public:
     const ref<Target> target;
     const ref<History> visitedTargets;
@@ -238,21 +261,11 @@ class TargetForest {
     }
 
     unsigned hash() const { return hashValue; }
+    unsigned size() const { return sizeValue; }
 
     int compare(const History &h) const;
     bool equals(const History &h) const;
 
-    void computeHash() {
-      unsigned res = 0;
-      if (target) {
-        res = target->hash() * Expr::MAGIC_HASH_CONSTANT;
-      }
-      if (visitedTargets) {
-        res ^= visitedTargets->hash() * Expr::MAGIC_HASH_CONSTANT;
-      }
-      hashValue = res;
-    }
-
     void dump() const;
 
     ~History();

include/klee/Solver/SolverCmdLine.h

@@ -70,7 +70,7 @@ extern llvm::cl::opt<CoreSolverType> DebugCrossCheckCoreSolverWith;
 
 extern llvm::cl::opt<bool> ProduceUnsatCore;
 
-extern llvm::cl::opt<unsigned> SymbolicAllocationThreshhold;
+extern llvm::cl::opt<unsigned> SymbolicAllocationThreshold;
 
 #ifdef ENABLE_METASMT
 

lib/Core/AddressSpace.cpp

@@ -274,12 +274,8 @@ int AddressSpace::checkPointerInObject(ExecutionState &state,
   // mustBeTrue before mayBeTrue for the first result. easy
   // to add I just want to have a nice symbolic test case first.
   const MemoryObject *mo = op.first;
-  ref<Expr> base = state.isGEPExpr(p) ? state.gepExprBases.at(p).first : p;
   ref<Expr> inBounds = mo->getBoundsCheckPointer(p);
-  inBounds = AndExpr::create(
-      inBounds,
-      mo->getBoundsCheckPointer(base)); // FIXME: remove when segmented memory
-                                        // model will be implemented
+
   bool mayBeTrue;
   if (!solver->mayBeTrue(state.constraints.cs(), inBounds, mayBeTrue,
                          state.queryMetaData)) {