Merge 0054e94 into fac8369

include/klee/Core/Interpreter.h

@@ -140,7 +140,8 @@ class Interpreter {
   setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
             std::vector<std::unique_ptr<llvm::Module>> &libsModules,
             const ModuleOptions &opts,
-            const std::vector<std::string> &mainModuleFunctions,
+            const std::unordered_set<std::string> &mainModuleFunctions,
+            const std::unordered_set<std::string> &mainModuleGlobals,
             std::unique_ptr<InstructionInfoTable> origInfos) = 0;
 
   // supply a tree stream writer which the interpreter will use

include/klee/Core/TargetedExecutionReporter.h

@@ -30,8 +30,8 @@ ty min(ty left, ty right);
 }; // namespace confidence
 
 void reportFalsePositive(confidence::ty confidence,
-                         const std::set<ReachWithError> &errors, unsigned id,
-                         std::string whatToIncrease);
+                         const std::set<ReachWithError> &errors,
+                         const std::string &id, std::string whatToIncrease);
 
 } // namespace klee
 

include/klee/Core/TerminationTypes.h

@@ -62,6 +62,7 @@ enum Reason {
   MaxSteppedInstructions,
   MaxTime,
   MaxCycles,
+  MaxForks,
   CovCheck,
   NoMoreStates,
   ReachedTarget,

include/klee/Module/KModule.h

@@ -217,7 +217,9 @@ class KModule {
   // XXX change to KFunction
   std::set<llvm::Function *> escapingFunctions;
 
-  std::vector<std::string> mainModuleFunctions;
+  std::unordered_set<std::string> mainModuleFunctions;
+
+  std::unordered_set<std::string> mainModuleGlobals;
 
   InstructionInfoTable::Instructions origInfos;
 
@@ -253,7 +255,8 @@ class KModule {
   /// @param forceSourceOutput true if assembly.ll should be created
   ///
   // FIXME: ihandler should not be here
-  void manifest(InterpreterHandler *ih, bool forceSourceOutput);
+  void manifest(InterpreterHandler *ih, Interpreter::GuidanceKind guidance,
+                bool forceSourceOutput);
 
   /// Link the provided modules together as one KLEE module.
   ///
@@ -282,6 +285,8 @@ class KModule {
 
   bool inMainModule(llvm::Function *f);
 
+  bool inMainModule(const llvm::GlobalVariable &v);
+
   bool WithPOSIXRuntime() { return withPosixRuntime; }
 };
 } // namespace klee

include/klee/Module/SarifReport.h

@@ -46,7 +46,8 @@ namespace klee {
 enum ReachWithError {
   DoubleFree = 0,
   UseAfterFree,
-  NullPointerException,
+  MayBeNullPointerException,  // void f(int *x) { *x = 42; } - should it error?
+  MustBeNullPointerException, // MayBeNPE = yes, MustBeNPE = no
   NullCheckAfterDerefException,
   Reachable,
   None,
@@ -55,7 +56,8 @@ enum ReachWithError {
 static const char *ReachWithErrorNames[] = {
     "DoubleFree",
     "UseAfterFree",
-    "NullPointerException",
+    "MayBeNullPointerException",
+    "NullPointerException", // for backward compatibility with SecB
     "NullCheckAfterDerefException",
     "Reachable",
     "None",
@@ -104,10 +106,23 @@ struct Message {
   std::string text;
 };
 
+struct Fingerprints {
+  std::string cooddy_uid;
+};
+
+static void to_json(json &j, const Fingerprints &p) {
+  j = json{{"cooddy.uid", p.cooddy_uid}};
+}
+
+static void from_json(const json &j, Fingerprints &p) {
+  j.at("cooddy.uid").get_to(p.cooddy_uid);
+}
+
 struct ResultJson {
   optional<std::string> ruleId;
   optional<Message> message;
   optional<unsigned> id;
+  optional<Fingerprints> fingerprints;
   std::vector<LocationJson> locations;
   std::vector<CodeFlowJson> codeFlows;
 };
@@ -149,7 +164,8 @@ NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(CodeFlowJson, threadFlows)
 NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(Message, text)
 
 NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(ResultJson, ruleId, message, id,
-                                                codeFlows, locations)
+                                                fingerprints, codeFlows,
+                                                locations)
 
 NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(DriverJson, name)
 
@@ -257,7 +273,7 @@ struct RefLocationCmp {
 struct Result {
   std::vector<ref<Location>> locations;
   std::vector<optional<json>> metadatas;
-  unsigned id;
+  std::string id;
   std::set<ReachWithError> errors;
 };
 

include/klee/Module/Target.h

@@ -51,11 +51,12 @@ struct Target {
   KBlock *block;
   std::set<ReachWithError>
       errors;                  // None - if it is not terminated in error trace
-  unsigned id;                 // 0 - if it is not terminated in error trace
+  std::string id;              // "" - if it is not terminated in error trace
   optional<ErrorLocation> loc; // TODO(): only for check in reportTruePositive
 
-  explicit Target(const std::set<ReachWithError> &_errors, unsigned _id,
-                  optional<ErrorLocation> _loc, KBlock *_block)
+  explicit Target(const std::set<ReachWithError> &_errors,
+                  const std::string &_id, optional<ErrorLocation> _loc,
+                  KBlock *_block)
       : block(_block), errors(_errors), id(_id), loc(_loc) {}
 
   static ref<Target> getFromCacheOrReturn(Target *target);
@@ -66,8 +67,8 @@ struct Target {
   class ReferenceCounter _refCount;
 
   static ref<Target> create(const std::set<ReachWithError> &_errors,
-                            unsigned _id, optional<ErrorLocation> _loc,
-                            KBlock *_block);
+                            const std::string &_id,
+                            optional<ErrorLocation> _loc, KBlock *_block);
   static ref<Target> create(KBlock *_block);
 
   int compare(const Target &other) const;
@@ -89,7 +90,7 @@ struct Target {
   unsigned hash() const { return reinterpret_cast<uintptr_t>(block); }
 
   const std::set<ReachWithError> &getErrors() const { return errors; }
-  bool isThatError(ReachWithError err) const { return errors.count(err) != 0; }
+  bool isThatError(ReachWithError err) const;
   bool shouldFailOnThisTarget() const {
     return errors.count(ReachWithError::None) == 0;
   }
@@ -101,7 +102,7 @@ struct Target {
   /// to avoid solver calls
   bool mustVisitForkBranches(KInstruction *instr) const;
 
-  unsigned getId() const { return id; }
+  std::string getId() const { return id; }
 
   std::string toString() const;
   ~Target();

include/klee/Module/TargetForest.h

@@ -137,7 +137,7 @@ class TargetForest {
     }
 
     void collectHowManyEventsInTracesWereReached(
-        std::unordered_map<unsigned, std::pair<unsigned, unsigned>>
+        std::unordered_map<std::string, std::pair<unsigned, unsigned>>
             &traceToEventCount,
         unsigned reached, unsigned total) const;
 
@@ -191,7 +191,7 @@ class TargetForest {
       return getConfidence(confidence::MaxConfidence);
     }
     void collectHowManyEventsInTracesWereReached(
-        std::unordered_map<unsigned, std::pair<unsigned, unsigned>>
+        std::unordered_map<std::string, std::pair<unsigned, unsigned>>
             &traceToEventCount) const {
       collectHowManyEventsInTracesWereReached(traceToEventCount, 0, 0);
     }
@@ -328,7 +328,7 @@ class TargetForest {
     forest = forest->divideConfidenceBy(reachableStatesOfTarget);
   }
   void collectHowManyEventsInTracesWereReached(
-      std::unordered_map<unsigned, std::pair<unsigned, unsigned>>
+      std::unordered_map<std::string, std::pair<unsigned, unsigned>>
           &traceToEventCount) const {
     forest->collectHowManyEventsInTracesWereReached(traceToEventCount);
   }

lib/Core/AddressSpace.cpp

@@ -150,11 +150,44 @@ bool AddressSpace::resolveOneIfUnique(ExecutionState &state,
   return true;
 }
 
+class ResolvePredicate {
+  bool useTimestamps;
+  bool skipNotSymbolicObjects;
+  bool skipNotLazyInitialized;
+  bool skipLocal;
+  unsigned timestamp;
+  ExecutionState *state;
+
+public:
+  explicit ResolvePredicate(ExecutionState &state, ref<Expr> address)
+      : useTimestamps(UseTimestamps),
+        skipNotSymbolicObjects(SkipNotSymbolicObjects),
+        skipNotLazyInitialized(SkipNotLazyInitialized), skipLocal(SkipLocal),
+        timestamp(UINT_MAX), state(&state) {
+    auto base =
+        state.isGEPExpr(address) ? state.gepExprBases[address].first : address;
+    if (!isa<ConstantExpr>(address)) {
+      std::pair<ref<const MemoryObject>, ref<Expr>> moBasePair;
+      if (state.getBase(base, moBasePair)) {
+        timestamp = moBasePair.first->timestamp;
+      }
+    }
+  }
+
+  bool operator()(const MemoryObject *mo) const {
+    bool result = !useTimestamps || mo->timestamp <= timestamp;
+    result = result && (!skipNotSymbolicObjects || state->inSymbolics(mo));
+    result = result && (!skipNotLazyInitialized || mo->isLazyInitialized);
+    result = result && (!skipLocal || !mo->isLocal);
+    return result;
+  }
+};
+
 bool AddressSpace::resolveOne(ExecutionState &state, TimingSolver *solver,
                               ref<Expr> address, KType *objectType,
-                              IDType &result, MOPredicate predicate,
-                              bool &success,
+                              IDType &result, bool &success,
                               const std::atomic_bool &haltExecution) const {
+  ResolvePredicate predicate(state, address);
   if (ref<ConstantExpr> CE = dyn_cast<ConstantExpr>(address)) {
     if (resolveOne(CE, objectType, result)) {
       success = true;
@@ -227,45 +260,6 @@ bool AddressSpace::resolveOne(ExecutionState &state, TimingSolver *solver,
   return true;
 }
 
-bool AddressSpace::resolveOne(ExecutionState &state, TimingSolver *solver,
-                              ref<Expr> address, KType *objectType,
-                              IDType &result, bool &success,
-                              const std::atomic_bool &haltExecution) const {
-  MOPredicate predicate([](const MemoryObject *mo) { return true; });
-  if (UseTimestamps) {
-    ref<Expr> base =
-        state.isGEPExpr(address) ? state.gepExprBases[address].first : address;
-    unsigned timestamp = UINT_MAX;
-    if (!isa<ConstantExpr>(address)) {
-      std::pair<ref<const MemoryObject>, ref<Expr>> moBasePair;
-      if (state.getBase(base, moBasePair)) {
-        timestamp = moBasePair.first->timestamp;
-      }
-    }
-    predicate = [timestamp, predicate](const MemoryObject *mo) {
-      return predicate(mo) && mo->timestamp <= timestamp;
-    };
-  }
-  if (SkipNotSymbolicObjects) {
-    predicate = [&state, predicate](const MemoryObject *mo) {
-      return predicate(mo) && state.inSymbolics(mo);
-    };
-  }
-  if (SkipNotLazyInitialized) {
-    predicate = [predicate](const MemoryObject *mo) {
-      return predicate(mo) && mo->isLazyInitialized;
-    };
-  }
-  if (SkipLocal) {
-    predicate = [predicate](const MemoryObject *mo) {
-      return predicate(mo) && !mo->isLocal;
-    };
-  }
-
-  return resolveOne(state, solver, address, objectType, result, predicate,
-                    success, haltExecution);
-}
-
 int AddressSpace::checkPointerInObject(ExecutionState &state,
                                        TimingSolver *solver, ref<Expr> p,
                                        const ObjectPair &op, ResolutionList &rl,
@@ -303,8 +297,9 @@ int AddressSpace::checkPointerInObject(ExecutionState &state,
 
 bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
                            ref<Expr> p, KType *objectType, ResolutionList &rl,
-                           ResolutionList &rlSkipped, MOPredicate predicate,
-                           unsigned maxResolutions, time::Span timeout) const {
+                           ResolutionList &rlSkipped, unsigned maxResolutions,
+                           time::Span timeout) const {
+  ResolvePredicate predicate(state, p);
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(p)) {
     IDType res;
     if (resolveOne(CE, objectType, res)) {
@@ -363,44 +358,6 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
   return false;
 }
 
-bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
-                           ref<Expr> p, KType *objectType, ResolutionList &rl,
-                           ResolutionList &rlSkipped, unsigned maxResolutions,
-                           time::Span timeout) const {
-  MOPredicate predicate([](const MemoryObject *mo) { return true; });
-  if (UseTimestamps) {
-    ref<Expr> base = state.isGEPExpr(p) ? state.gepExprBases[p].first : p;
-    unsigned timestamp = UINT_MAX;
-    if (!isa<ConstantExpr>(p)) {
-      std::pair<ref<const MemoryObject>, ref<Expr>> moBasePair;
-      if (state.getBase(base, moBasePair)) {
-        timestamp = moBasePair.first->timestamp;
-      }
-    }
-    predicate = [timestamp, predicate](const MemoryObject *mo) {
-      return predicate(mo) && mo->timestamp <= timestamp;
-    };
-  }
-  if (SkipNotSymbolicObjects) {
-    predicate = [&state, predicate](const MemoryObject *mo) {
-      return predicate(mo) && state.inSymbolics(mo);
-    };
-  }
-  if (SkipNotLazyInitialized) {
-    predicate = [predicate](const MemoryObject *mo) {
-      return predicate(mo) && mo->isLazyInitialized;
-    };
-  }
-  if (SkipLocal) {
-    predicate = [predicate](const MemoryObject *mo) {
-      return predicate(mo) && !mo->isLocal;
-    };
-  }
-
-  return resolve(state, solver, p, objectType, rl, rlSkipped, predicate,
-                 maxResolutions, timeout);
-}
-
 // These two are pretty big hack so we can sort of pass memory back
 // and forth to externals. They work by abusing the concrete cache
 // store inside of the object states, which allows them to

lib/Core/AddressSpace.h

@@ -96,10 +96,6 @@ class AddressSpace {
   bool resolveOne(ExecutionState &state, TimingSolver *solver,
                   ref<Expr> address, KType *objectType, IDType &result,
                   bool &success, const std::atomic_bool &haltExecution) const;
-  bool resolveOne(ExecutionState &state, TimingSolver *solver,
-                  ref<Expr> address, KType *objectType, IDType &result,
-                  MOPredicate predicate, bool &success,
-                  const std::atomic_bool &haltExecution) const;
 
   /// @brief Tries to resolve the pointer in the concrete object
   /// if it value is unique.
@@ -124,10 +120,6 @@ class AddressSpace {
                KType *objectType, ResolutionList &rl, ResolutionList &rlSkipped,
                unsigned maxResolutions = 0,
                time::Span timeout = time::Span()) const;
-  bool resolve(ExecutionState &state, TimingSolver *solver, ref<Expr> p,
-               KType *objectType, ResolutionList &rl, ResolutionList &rlSkipped,
-               MOPredicate predicate, unsigned maxResolutions = 0,
-               time::Span timeout = time::Span()) const;
 
   /***/