Fix

Author: mamaria-k

lib/Core/Executor.cpp

@@ -5030,8 +5030,9 @@ void Executor::terminateStateOnTargetError(ExecutionState &state,
 void Executor::terminateStateOnTargetTaintError(ExecutionState &state,
                                                 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++) {
+  const auto &sinkData = annotationsData.taintAnnotation.hits[sink];
+  for (size_t source = 0;
+       source < annotationsData.taintAnnotation.sources.size(); source++) {
     if ((hits >> source) & 1u) {
       error += " " + annotationsData.taintAnnotation.rules[sinkData.at(source)];
     }
@@ -5041,8 +5042,8 @@ void Executor::terminateStateOnTargetTaintError(ExecutionState &state,
       state, ReachWithError(ReachWithErrorType::MaybeTaint, error));
 
   terminateStateOnProgramError(
-      state, new ErrorEvent(locationOf(state), StateTerminationType::Taint,
-                            error));
+      state,
+      new ErrorEvent(locationOf(state), StateTerminationType::Taint, error));
 }
 
 void Executor::terminateStateOnError(ExecutionState &state,
@@ -5550,6 +5551,8 @@ void Executor::executeChangeTaintSource(ExecutionState &state,
                                         ref<PointerExpr> address,
                                         uint64_t source, bool isAdd) {
   address = optimizer.optimizeExpr(address, true);
+  ref<PointerExpr> base = PointerExpr::create(
+      address->getBase(), address->getBase(), address->getTaint());
   ref<Expr> isNullPointer = Expr::createIsZero(address->getValue());
   StatePair zeroPointer =
       forkInternal(state, isNullPointer, BranchType::ResolvePointer);
@@ -5562,8 +5565,8 @@ void Executor::executeChangeTaintSource(ExecutionState &state,
   }
   if (zeroPointer.second) { // address != 0
     ExactResolutionList rl;
-    resolveExact(*zeroPointer.second, address,
-                 typeSystemManager->getUnknownType(), rl, "сhangeTaintSource");
+    resolveExact(*zeroPointer.second, base, typeSystemManager->getUnknownType(),
+                 rl, "сhangeTaintSource");
     for (Executor::ExactResolutionList::iterator it = rl.begin(), ie = rl.end();
          it != ie; ++it) {
       const MemoryObject *mo = it->first;
@@ -5589,6 +5592,8 @@ void Executor::executeCheckTaintSource(ExecutionState &state,
                                        ref<PointerExpr> address,
                                        uint64_t source) {
   address = optimizer.optimizeExpr(address, true);
+  ref<PointerExpr> base = PointerExpr::create(
+      address->getBase(), address->getBase(), address->getTaint());
   ref<Expr> isNullPointer = Expr::createIsZero(address->getValue());
   StatePair zeroPointer =
       forkInternal(state, isNullPointer, BranchType::ResolvePointer);
@@ -5601,8 +5606,8 @@ void Executor::executeCheckTaintSource(ExecutionState &state,
   }
   if (zeroPointer.second) {
     ExactResolutionList rl;
-    resolveExact(*zeroPointer.second, address,
-                 typeSystemManager->getUnknownType(), rl, "checkTaintSource");
+    resolveExact(*zeroPointer.second, base, typeSystemManager->getUnknownType(),
+                 rl, "checkTaintSource");
 
     for (Executor::ExactResolutionList::iterator it = rl.begin(), ie = rl.end();
          it != ie; ++it) {
@@ -5629,6 +5634,8 @@ void Executor::executeGetTaintHits(ExecutionState &state,
   }
 
   address = optimizer.optimizeExpr(address, true);
+  ref<PointerExpr> base = PointerExpr::create(
+      address->getBase(), address->getBase(), address->getTaint());
   ref<Expr> isNullPointer = Expr::createIsZero(address->getValue());
   StatePair zeroPointer =
       forkInternal(state, isNullPointer, BranchType::ResolvePointer);
@@ -5641,8 +5648,8 @@ void Executor::executeGetTaintHits(ExecutionState &state,
   }
   if (zeroPointer.second) {
     ExactResolutionList rl;
-    resolveExact(*zeroPointer.second, address,
-                 typeSystemManager->getUnknownType(), rl, "getTaintHits");
+    resolveExact(*zeroPointer.second, base, typeSystemManager->getUnknownType(),
+                 rl, "getTaintHits");
 
     for (Executor::ExactResolutionList::iterator it = rl.begin(), ie = rl.end();
          it != ie; ++it) {

lib/Core/MockBuilder.cpp

@@ -684,10 +684,10 @@ void MockBuilder::buildAnnotationForExternalFunctionArgs(
             klee_error("Annotation: TaintOutput arg is not pointer");
           }
 
-          if (!isMocked) {
-            buildCallKleeMakeMockAll(elem, mockName);
-            isMocked = true;
-          }
+//          if (!isMocked) {
+//            buildCallKleeMakeMockAll(elem, mockName);
+//            isMocked = true;
+//          }
           buildAnnotationTaintOutput(elem, statement);
           break;
         }
@@ -696,10 +696,10 @@ void MockBuilder::buildAnnotationForExternalFunctionArgs(
             klee_error("Annotation: TaintPropagation arg is not pointer");
           }
 
-          if (!isMocked) {
-            buildCallKleeMakeMockAll(elem, mockName);
-            isMocked = true;
-          }
+//          if (!isMocked) {
+//            buildCallKleeMakeMockAll(elem, mockName);
+//            isMocked = true;
+//          }
           buildAnnotationTaintPropagation(elem, statement, func,
                                           "_arg_" + std::to_string(i) + "_");
           break;

runtime/Runtest/intrinsics.c

@@ -165,7 +165,7 @@ void klee_make_mock(void *ret_array, size_t ret_nbytes, const char *fname) {
 }
 
 // TODO: add for tests
-//void klee_make_mock_all(void *ret_array, const char *fname);
+//void klee_make_mock_all(void *ret_array, const char *fname) {}
 //void klee_add_taint(void *array, size_t taint_source) {}
 //void klee_clear_taint(void *array, size_t taint_source) {}
 //bool klee_check_taint_source(void *array, size_t taint_source) {}