[feat] Add UninitMemoryTestMultiplier`

Author: misonijnik

include/klee/ADT/KTest.h

@@ -46,6 +46,7 @@ struct KTest {
 
   unsigned numObjects;
   KTestObject *objects;
+  unsigned uninitCoeff;
 };
 
 /* returns the current .ktest file format version */

lib/Core/Executor.cpp

@@ -255,6 +255,13 @@ cl::opt<unsigned> DelayCoverOnTheFly(
              "(default=10000)"),
     cl::cat(TestGenCat));
 
+cl::opt<unsigned> UninitMemoryTestMultiplier(
+    "uninit-memory-test-multiplier", cl::init(6),
+    cl::desc("Generate additional number of duplicate tests due to "
+             "irreproducibility of uninitialized memory "
+             "(default=6)"),
+    cl::cat(TestGenCat));
+
 /* Constraint solving options */
 
 cl::opt<unsigned> MaxSymArraySize(
@@ -7122,6 +7129,15 @@ bool isReproducible(const klee::Symbolic &symb) {
   return !bad;
 }
 
+bool isUninitialized(const klee::Array *array) {
+  bool bad = isa<UninitializedSource>(array->source);
+  if (bad)
+    klee_warning_once(array->source.get(),
+                      "A uninitialized array %s reaches a test",
+                      array->getIdentifier().c_str());
+  return bad;
+}
+
 bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
   solver->setTimeout(coreSolverTimeout);
 
@@ -7158,6 +7174,13 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
     }
   }
 
+  std::vector<const Array *> allObjects;
+  findSymbolicObjects(state.constraints.cs().cs().begin(),
+                      state.constraints.cs().cs().end(), allObjects);
+  std::vector<const Array *> uninitObjects;
+  std::copy_if(allObjects.begin(), allObjects.end(),
+               std::back_inserter(uninitObjects), isUninitialized);
+
   std::vector<klee::Symbolic> symbolics;
   std::copy_if(state.symbolics.begin(), state.symbolics.end(),
                std::back_inserter(symbolics), isReproducible);
@@ -7180,6 +7203,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
 
   res.numObjects = symbolics.size();
   res.objects = new KTestObject[res.numObjects];
+  res.uninitCoeff = uninitObjects.empty() ? 0 : UninitMemoryTestMultiplier;
 
   {
     size_t i = 0;