Change klee_get_taint_rule to klee_get_taint_hits, fix memory and som…

…e Pointer creations

configs/annotations.json

@@ -2326,5 +2326,16 @@
       []
     ],
     "properties": []
+  },
+  "printf": {
+    "name": "printf",
+    "annotation": [
+      [],
+      [
+        "TaintSink::FormatString",
+        "TaintSink::SensitiveDataLeak"
+      ]
+    ],
+    "properties": []
   }
 }

include/klee/Core/MockBuilder.h

@@ -53,7 +53,7 @@ class MockBuilder {
   llvm::CallInst *buildCallKleeTaintFunction(const std::string &functionName,
                                              llvm::Value *source, size_t taint,
                                              llvm::Type *returnType);
-  void buildCallKleeTaintHit(llvm::Value *taintRule);
+  void buildCallKleeTaintHit(llvm::Value *taintHits, size_t taintSink);
 
   void buildAnnotationTaintOutput(llvm::Value *elem,
                                   const Statement::Ptr &statement);

include/klee/Expr/Expr.h

@@ -396,6 +396,7 @@ class Expr {
   ref<ReadExpr> hasOrderedReads(bool stride) const;
   ref<ReadExpr> hasOrderedReads() const;
   ref<Expr> getValue() const;
+  ref<Expr> getTaint() const;
 
   /* Static utility methods */
 

include/klee/klee.h

@@ -61,19 +61,20 @@ void klee_clear_taint(void *array, size_t taint_source);
  */
 bool klee_check_taint_source(void *array, size_t taint_source);
 
-/* klee_get_taint_rule - Return taint rule id +1 if contents of the object pointer
- * to \arg addr causes a taint sink \arg taint_sink hit, else return 0.
+/* klee_get_taint_hits - Return taint hits if contents of the object pointer
+ * to \arg addr causes a taint sink \arg taint_sink hit.
  *
  * \arg addr - The start of the object.
  * \arg taint_sink - Taint sink.
  */
-uint64_t klee_get_taint_rule(void *array, size_t taint_sink);
+uint64_t klee_get_taint_hits(void *array, size_t taint_sink);
 
-/* klee_taint_hit - Execute taint hit with rule.
+/* klee_taint_hit - Execute taint hits.
  *
- * \arg rule - Taint rule id.
+ * \arg taint_hits - Actual taint hits.
+ * \arg taint_sink - Taint sink.
  */
-void klee_taint_hit(size_t rule);
+void klee_taint_hit(uint64_t taint_hits, size_t taint_sink);
 
 /* klee_range - Construct a symbolic value in the signed interval
  * [begin,end).

lib/Core/Executor.cpp

@@ -509,9 +509,9 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
       annotationsData(opts.AnnotationsFile, opts.TaintAnnotationsFile),
       interpreterHandler(ih), searcher(nullptr),
       externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0),
-      pathWriter(0), symPathWriter(0),
-      specialFunctionHandler(0), timers{time::Span(TimerInterval)},
-      guidanceKind(opts.Guidance), codeGraphInfo(new CodeGraphInfo()),
+      pathWriter(0), symPathWriter(0), specialFunctionHandler(0),
+      timers{time::Span(TimerInterval)}, guidanceKind(opts.Guidance),
+      codeGraphInfo(new CodeGraphInfo()),
       distanceCalculator(new DistanceCalculator(*codeGraphInfo)),
       targetCalculator(new TargetCalculator(*codeGraphInfo)),
       targetManager(new TargetManager(guidanceKind, *distanceCalculator,
@@ -5028,17 +5028,21 @@ void Executor::terminateStateOnTargetError(ExecutionState &state,
 }
 
 void Executor::terminateStateOnTargetTaintError(ExecutionState &state,
-                                                uint64_t rule) {
-  if (rule >= annotationsData.taintAnnotation.rules.size()) {
-    terminateStateOnUserError(state, "Incorrect rule id");
+                                                uint64_t hits, size_t sink) {
+  std::string error = "Taint error:";
+  const auto &sinkData = annotationsData.taintAnnotation.hits.at(sink);
+  for (size_t source = 0; source < annotationsData.taintAnnotation.sources.size(); source++) {
+    if ((hits >> source) & 1u) {
+      error += " " + annotationsData.taintAnnotation.rules[sinkData.at(source)];
+    }
   }
 
-  const std::string &ruleStr = annotationsData.taintAnnotation.rules[rule];
   reportStateOnTargetError(
-      state, ReachWithError(ReachWithErrorType::MaybeTaint, ruleStr));
+      state, ReachWithError(ReachWithErrorType::MaybeTaint, error));
 
-  terminateStateOnProgramError(state, ruleStr + " taint error",
-                               StateTerminationType::Taint);
+  terminateStateOnProgramError(
+      state, new ErrorEvent(locationOf(state), StateTerminationType::Taint,
+                            error));
 }
 
 void Executor::terminateStateOnError(ExecutionState &state,
@@ -5569,9 +5573,10 @@ void Executor::executeChangeTaintSource(ExecutionState &state,
 
       ObjectState *wos = it->second->addressSpace.getWriteable(mo, os.get());
       if (wos->readOnly) {
-        terminateStateOnProgramError(*(it->second),
-                                     "memory error: object read only",
-                                     StateTerminationType::ReadOnly);
+        terminateStateOnProgramError(
+            *(it->second), new ErrorEvent(locationOf(*(it->second)),
+                                          StateTerminationType::ReadOnly,
+                                          "memory error: object read only"));
       } else {
         wos->updateTaint(Expr::createTaintBySource(source), isAdd);
       }
@@ -5613,11 +5618,11 @@ void Executor::executeCheckTaintSource(ExecutionState &state,
   }
 }
 
-void Executor::executeGetTaintRule(ExecutionState &state,
+void Executor::executeGetTaintHits(ExecutionState &state,
                                    klee::KInstruction *target,
                                    ref<PointerExpr> address, uint64_t sink) {
   const auto &hitsBySink = annotationsData.taintAnnotation.hits[sink];
-  ref<Expr> hitsBySinkTaint = Expr::createEmptyTaint();
+  ref<ConstantExpr> hitsBySinkTaint = Expr::createEmptyTaint();
   for (const auto [source, rule] : hitsBySink) {
     hitsBySinkTaint =
         OrExpr::create(hitsBySinkTaint, Expr::createTaintBySource(source));
@@ -5637,7 +5642,7 @@ void Executor::executeGetTaintRule(ExecutionState &state,
   if (zeroPointer.second) {
     ExactResolutionList rl;
     resolveExact(*zeroPointer.second, address,
-                 typeSystemManager->getUnknownType(), rl, "getTaintRule");
+                 typeSystemManager->getUnknownType(), rl, "getTaintHits");
 
     for (Executor::ExactResolutionList::iterator it = rl.begin(), ie = rl.end();
          it != ie; ++it) {
@@ -5647,35 +5652,20 @@ void Executor::executeGetTaintRule(ExecutionState &state,
       ref<const ObjectState> os = op.second;
 
       ref<Expr> hits = AndExpr::create(os->readTaint(), hitsBySinkTaint);
-
-      auto curState = it->second;
-      for (size_t source = 0;
-           source < annotationsData.taintAnnotation.sources.size(); source++) {
-        ref<Expr> taintSource = ExtractExpr::create(hits, source, Expr::Bool);
-        StatePair taintSourceStates =
-            forkInternal(*curState, taintSource, BranchType::Taint);
-        if (taintSourceStates.first) {
-          bindLocal(target, *taintSourceStates.first,
-                    ConstantExpr::create(hitsBySink.at(source) + 1,
-                                         Expr::Int64)); // return (rule + 1)
-        }
-        if (taintSourceStates.second) {
-          curState = taintSourceStates.second;
-        }
-      }
-      bindLocal(target, *curState, ConstantExpr::create(0, Expr::Int64));
+      bindLocal(target, *it->second, hits);
     }
   }
 }
 
 bool Executor::resolveExact(ExecutionState &estate, ref<Expr> address,
                             KType *type, ExactResolutionList &results,
                             const std::string &name) {
-  ref<PointerExpr> pointer =
-      PointerExpr::create(address->getValue(), address->getValue());
+  ref<PointerExpr> pointer = PointerExpr::create(
+      address->getValue(), address->getValue(), address->getTaint());
   address = pointer->getValue();
   ref<Expr> base = pointer->getBase();
-  ref<PointerExpr> basePointer = PointerExpr::create(base, base);
+  ref<PointerExpr> basePointer =
+      PointerExpr::create(base, base, address->getTaint());
   ref<Expr> zeroPointer = PointerExpr::create(Expr::createPointer(0));
 
   if (SimplifySymIndices) {

lib/Core/Executor.h

@@ -370,7 +370,7 @@ class Executor : public Interpreter {
                                klee::KInstruction *target,
                                ref<PointerExpr> address, uint64_t source);
 
-  void executeGetTaintRule(ExecutionState &state, klee::KInstruction *target,
+  void executeGetTaintHits(ExecutionState &state, klee::KInstruction *target,
                            ref<PointerExpr> address, uint64_t sink);
 
   /// Serialize a landingpad instruction so it can be handled by the
@@ -646,7 +646,8 @@ class Executor : public Interpreter {
   /// Then just call `terminateStateOnError`
   void terminateStateOnTargetError(ExecutionState &state, ReachWithError error);
 
-  void terminateStateOnTargetTaintError(ExecutionState &state, uint64_t rule);
+  void terminateStateOnTargetTaintError(ExecutionState &state, uint64_t hits,
+                                        size_t sink);
 
   /// Call error handler and terminate state in case of program errors
   /// (e.g. free()ing globals, out-of-bound accesses)

lib/Core/Memory.cpp

@@ -41,6 +41,7 @@ DISABLE_WARNING_POP
 #include <cstddef>
 #include <functional>
 #include <sstream>
+#include <utility>
 
 namespace klee {
 llvm::cl::opt<MemoryType> MemoryBackend(
@@ -111,11 +112,10 @@ ObjectState::ObjectState(const MemoryObject *mo, const Array *array, KType *dt,
     : copyOnWriteOwner(0), object(mo), valueOS(ObjectStage(array, nullptr)),
       baseOS(ObjectStage(array->size, Expr::createPointer(0), false,
                          Context::get().getPointerWidth())),
-      taintOS(
-          ObjectStage(array->size, defaultTaintValue, false, Expr::TaintWidth)),
+      taintOS(ObjectStage(array->size, std::move(defaultTaintValue), false,
+                          Expr::TaintWidth)),
       lastUpdate(nullptr), size(array->size), dynamicType(dt), readOnly(false) {
   baseOS.initializeToZero();
-  taintOS.initializeToZero();
 }
 
 ObjectState::ObjectState(const MemoryObject *mo, KType *dt,
@@ -124,12 +124,11 @@ ObjectState::ObjectState(const MemoryObject *mo, KType *dt,
       valueOS(ObjectStage(mo->getSizeExpr(), nullptr)),
       baseOS(ObjectStage(mo->getSizeExpr(), Expr::createPointer(0), false,
                          Context::get().getPointerWidth())),
-      taintOS(ObjectStage(mo->getSizeExpr(), defaultTaintValue, false,
-                          Expr::TaintWidth)),
+      taintOS(ObjectStage(mo->getSizeExpr(), std::move(defaultTaintValue),
+                          false, Expr::TaintWidth)),
       lastUpdate(nullptr), size(mo->getSizeExpr()), dynamicType(dt),
       readOnly(false) {
   baseOS.initializeToZero();
-  taintOS.initializeToZero();
 }
 
 ObjectState::ObjectState(const ObjectState &os)
@@ -254,8 +253,7 @@ ref<Expr> ObjectState::readTaint8(ref<Expr> offset) const {
             dyn_cast<ConstantExpr>(object->getSizeExpr())) {
       auto moSize = sizeExpr->getZExtValue();
       if (object && moSize > 4096) {
-        std::string allocInfo;
-        object->getAllocInfo(allocInfo);
+        std::string allocInfo = object->getAllocInfo();
         klee_warning_once(nullptr,
                           "Symbolic memory access will send the following "
                           "array of %lu bytes to "
@@ -832,17 +830,29 @@ void ObjectStage::reset(ref<Expr> updateForDefault, bool isAdd) {
 }
 
 ref<Expr> ObjectStage::combineAll() const {
-  ref<Expr> result = knownSymbolics->defaultV();
+  ref<Expr> result = Expr::createEmptyTaint();
+  if (knownSymbolics->defaultV()) {
+    result = knownSymbolics->defaultV();
+  }
   for (auto [index, value] : knownSymbolics->storage()) {
     result = OrExpr::create(result, value);
   }
+  if (updates.root) {
+    if (ref<ConstantSource> constantSource =
+            cast<ConstantSource>(updates.root->source)) {
+      for (const auto &[index, value] :
+           constantSource->constantValues->storage()) {
+        result = OrExpr::create(result, value);
+      }
+    }
+  }
   for (const auto *un = updates.head.get(); un; un = un->next.get()) {
     result = OrExpr::create(result, un->value);
   }
   return result;
 }
 
-void ObjectStage::updateAll(ref<Expr> updateExpr, bool isAdd) {
+void ObjectStage::updateAll(const ref<ConstantExpr> &updateExpr, bool isAdd) {
   std::vector<std::pair<size_t, ref<Expr>>> newKnownSymbolics;
   for (auto [index, value] : knownSymbolics->storage()) {
     ref<Expr> newValue =
@@ -851,11 +861,13 @@ void ObjectStage::updateAll(ref<Expr> updateExpr, bool isAdd) {
     newKnownSymbolics.emplace_back(index, value);
   }
 
-  ref<Expr> oldDefault = knownSymbolics->defaultV();
-  ref<Expr> newDefault =
-      isAdd ? OrExpr::create(oldDefault, updateExpr)
-            : AndExpr::create(oldDefault, NotExpr::create(updateExpr));
-  knownSymbolics->reset(std::move(newDefault));
+  if (knownSymbolics->defaultV()) {
+    ref<Expr> oldDefault = knownSymbolics->defaultV();
+    ref<Expr> newDefault =
+        isAdd ? OrExpr::create(oldDefault, updateExpr)
+              : AndExpr::create(oldDefault, NotExpr::create(updateExpr));
+    knownSymbolics->reset(std::move(newDefault));
+  }
 
   for (auto [index, value] : newKnownSymbolics) {
     knownSymbolics->store(index, value);
@@ -868,7 +880,28 @@ void ObjectStage::updateAll(ref<Expr> updateExpr, bool isAdd) {
               : AndExpr::create(un->value, NotExpr::create(updateExpr));
     newUpdates.emplace_back(un->index, newValue);
   }
-  updates = UpdateList(nullptr, nullptr);
+
+  const Array *array = nullptr;
+  if (updates.root) {
+    if (ref<ConstantSource> constantSource =
+            cast<ConstantSource>(updates.root->source)) {
+      SparseStorage<ref<ConstantExpr>> *newStorage = constructStorage(
+          size, ConstantExpr::create(0, width), MaxFixedSizeStructureSize);
+
+      for (const auto &[index, value] :
+           constantSource->constantValues->storage()) {
+        ref<ConstantExpr> newValue =
+            isAdd ? OrExpr::create(value, updateExpr)
+                  : AndExpr::create(value, NotExpr::create(updateExpr));
+        newStorage->store(index, newValue);
+      }
+
+      array = Array::create(size, SourceBuilder::constant(newStorage),
+                            Expr::Int32, width);
+    }
+  }
+
+  updates = UpdateList(array, nullptr);
   for (auto [index, value] : newUpdates) {
     updates.extend(index, value);
   }

lib/Core/Memory.h

@@ -271,7 +271,7 @@ class ObjectStage {
   void reset(ref<Expr> updateForDefault, bool isAdd);
 
   ref<Expr> combineAll() const;
-  void updateAll(ref<Expr> updateExpr, bool isAdd);
+  void updateAll(const ref<ConstantExpr> &updateExpr, bool isAdd);
 
 private:
   const UpdateList &getUpdates() const;
@@ -361,8 +361,7 @@ class ObjectState {
   KType *getDynamicType() const;
 
   ref<Expr> readTaint() const { return taintOS.combineAll(); }
-  void updateTaint(ref<Expr> updateForTaint, bool isAdd) {
-    //    resetTaint(updateForTaint, isAdd);
+  void updateTaint(const ref<ConstantExpr> &updateForTaint, bool isAdd) {
     taintOS.updateAll(updateForTaint, isAdd);
   }