handleICMPForLazyInit refactored

staticafi · May 23, 2022 · 327c8bd · 327c8bd
1 parent 58afb56
commit 327c8bd
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 23 deletions.
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
@@ -2405,7 +2405,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
           checkWidthMatch(left, right);
         }
       }
-    } else if (LazyInitialization) {
+    }
+    if (LazyInitialization) {
       handleICMPForLazyInit(predicate, state, left, right);
       checkWidthMatch(left, right);
     }
@@ -2928,38 +2929,41 @@ void Executor::checkWidthMatch(KValue &left, KValue &right) const {
     }
   }
 }
+
+void Executor::handleICMPForLazyMO(ExecutionState &state,
+                                      KValue &value) {
+  auto segment = value.getSegment();
+
+  if (!isa<ConstantExpr>(segment)) {
+    return;
+  }
+
+  uint64_t segmentConstant = cast<ConstantExpr>(segment)->getZExtValue();
+
+  //look if segment belongs to lazy MO, and if it was never written to
+  auto result = state.addressSpace.lazilyInitializedOffsets.find(segmentConstant);
+  if (result != state.addressSpace.lazilyInitializedOffsets.end()) {
+    if (result->second.empty()) {
+      getSymbolicAddressForConstantSegment(state, value);
+    }
+  }
+}
+
 void Executor::handleICMPForLazyInit(const CmpInst::Predicate &predicate,
                                      ExecutionState &state, KValue &left,
                                      KValue &right) {
   bool leftSegmentZero = left.getSegment()->isZero();
   bool rightSegmentZero = right.getSegment()->isZero();
-  bool isOtherZero = leftSegmentZero ? left.value->isZero() : right.value->isZero();
-  if ((leftSegmentZero && rightSegmentZero) || !isOtherZero || (predicate != CmpInst::ICMP_EQ && predicate != CmpInst::ICMP_NE)) {
-    return;
-  }
 
-  KValue value = leftSegmentZero ? right : left;
-  ObjectPair lookupResult;
-  bool success = state.addressSpace.resolveOneConstantSegment(value, lookupResult);
-  if (!success) {
-    return;
-  }
+  bool bothSegmentsAreZero = leftSegmentZero && rightSegmentZero;
+  bool isICMPEqualityComparison = predicate == CmpInst::ICMP_EQ || predicate == CmpInst::ICMP_NE;
 
-  uint64_t segment = cast<ConstantExpr>(value.getSegment())->getZExtValue();
-  auto it = state.addressSpace.lazilyInitializedOffsets.find(segment);
-  if (it == state.addressSpace.lazilyInitializedOffsets.end()) {
-    return;
-  }
-  if (!it->second.empty()) {
+  if (bothSegmentsAreZero || !isICMPEqualityComparison) {
     return;
   }
 
-  const MemoryObject* mo = lookupResult.first;
-  if (!mo->isLazyInitialized) {
-    return;
-  }
-  getSymbolicAddressForConstantSegment(state, value);
-  leftSegmentZero ? right = value : left = value;
+  handleICMPForLazyMO(state, left);
+  handleICMPForLazyMO(state, right);
 }
 
 void Executor::getSymbolicAddressForConstantSegment(ExecutionState &state, KValue &value) {

diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
@@ -600,6 +600,7 @@ class Executor : public Interpreter {
                              ExecutionState &state, KValue &left,
                              KValue &right);
   void checkWidthMatch(KValue &left, KValue &right) const;
+  void handleICMPForLazyMO(ExecutionState &state, KValue &value);
 };
 
 } // End klee namespace