Covered new error option, fix for building pointers

lib/Core/Executor.cpp

@@ -63,6 +63,7 @@
 #include "klee/Solver/Common.h"
 #include "klee/Solver/Solver.h"
 #include "klee/Solver/SolverCmdLine.h"
+#include "klee/Solver/SolverUtil.h"
 #include "klee/Statistics/TimerStatIncrementer.h"
 #include "klee/Support/Casting.h"
 #include "klee/Support/ErrorHandling.h"
@@ -136,6 +137,15 @@ cl::OptionCategory TestGenCat("Test generation options",
 cl::OptionCategory LazyInitCat("Lazy initialization option",
                                "These options configure lazy initialization.");
 
+cl::OptionCategory
+    TestComp("TestComp options",
+             "These options configure execution on \"TestComp\" competition.");
+
+cl::opt<bool> UseCoveredNewError(
+    "use-covered-new-error",
+    cl::desc("Do not output tests leading to the same \"abort\" errors."),
+    cl::init(false), cl::cat(TestComp));
+
 cl::opt<bool> UseAdvancedTypeSystem(
     "use-advanced-type-system",
     cl::desc("Use advanced information about type system from "
@@ -4741,7 +4751,8 @@ void Executor::initializeTypeManager() {
 
 static bool shouldWriteTest(const ExecutionState &state, bool isError = false) {
   state.updateCoveredNew();
-  bool coveredNew = isError ? state.isCoveredNewError() : state.isCoveredNew();
+  bool coveredNew = isError ? !UseCoveredNewError || state.isCoveredNewError()
+                            : state.isCoveredNew();
   return !OnlyOutputStatesCoveringNew || coveredNew;
 }
 
@@ -5094,7 +5105,8 @@ void Executor::terminateStateOnError(ExecutionState &state,
 
   if ((EmitAllErrors ||
        emittedErrors.insert(std::make_pair(lastInst, message)).second) &&
-      shouldWriteTest(state, true)) {
+      (terminationType != StateTerminationType::Abort ||
+       shouldWriteTest(state, true))) {
     std::string filepath = ki->getSourceFilepath();
     if (!filepath.empty()) {
       klee_message("ERROR: %s:%zu: %s", filepath.c_str(), ki->getLine(),
@@ -6701,7 +6713,7 @@ ref<const MemoryObject> Executor::lazyInitializeObject(
 
     addConstraint(state, AndExpr::create(lowerBound, upperBound));
     conditionExpr =
-        AddExpr::create(conditionExpr, AndExpr::create(lowerBound, upperBound));
+        AndExpr::create(conditionExpr, AndExpr::create(lowerBound, upperBound));
   } else {
     sizeExpr = Expr::createPointer(concreteSize);
   }
@@ -7563,7 +7575,8 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
     if (success) {
       Assignment symcreteModel = Assignment(symcreteObjects, symcreteValues);
 
-      for (auto &i : model.diffWith(symcreteModel).bindings) {
+      auto diffAssignment = model.diffWith(symcreteModel).bindings;
+      for (auto &i : diffAssignment) {
         model.bindings.replace({i.first, i.second});
       }
     }

lib/Solver/ConcretizingSolver.cpp

@@ -384,7 +384,8 @@ bool ConcretizingSolver::check(const Query &query,
   }
 
   if (isa<ValidResponse>(result)) {
-    for (auto i : cast<ValidResponse>(result)->validityCore().constraints) {
+    auto validityCore = cast<ValidResponse>(result)->validityCore();
+    for (auto i : validityCore.constraints) {
       if (!query.constraints.cs().count(i)) {
         return false;
       }

test/Feature/SymbolicSizes/MinimizeSize.c

@@ -1,6 +1,8 @@
 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --use-sym-size-alloc --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --use-sym-size-alloc --use-merged-pointer-dereference=true --symbolic-allocation-threshold=0 %t1.bc >%t.log 2>&1
+// RUN: %ktest-tool %t.klee-out/test*.ktest >>%t.log
+// RUN: FileCheck %s -input-file=%t.log
 
 #include "klee/klee.h"
 #include <stdlib.h>
@@ -12,11 +14,14 @@ int main() {
     storage[0] = 'a';
     storage[1] = 'b';
     storage[2] = 'c';
-    // CHECK: MinimizeSize.c:[[@LINE+1]]: memory error: out of bound pointer
+    // CHECK-DAG: MinimizeSize.c:[[@LINE+1]]: memory error: out of bound pointer
     storage[3] = 'd';
   }
 }
 
-// CHECK: KLEE: done: completed paths = 2
-// CHECK: KLEE: done: partially completed paths = 2
-// CHECK: KLEE: done: generated tests = 4
+// CHECK-DAG: KLEE: done: completed paths = 2
+// CHECK-DAG: KLEE: done: partially completed paths = 2
+// CHECK-DAG: KLEE: done: generated tests = 4
+
+// Check that exists at least one test with size = 5
+// CHECK-DAG: int: 5

test/regression/2024-07-12-symbolic-size-minimization.c

@@ -0,0 +1,50 @@
+// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --skip-not-lazy-initialized --use-sym-size-li --min-number-elements-li=1 --only-output-states-covering-new  --skip-not-symbolic-objects --symbolic-allocation-threshold=0 %t.bc >%t.log 2>&1
+// RUN: %ktest-tool %t.klee-out/test*.ktest >>%t.log
+// RUN: FileCheck %s -input-file=%t.log
+
+#include "klee/klee.h"
+
+struct AB {
+  int a;
+  int b;
+  int *c;
+  int **d;
+};
+
+int *sum(int *a, int *b, int c, struct AB ab, struct AB ab2) {
+  // CHECK-DAG: 2024-07-12-symbolic-size-minimization.c:[[@LINE+1]]: memory error: null pointer exception
+  *a += *b + c + ab.a + *ab2.c + **ab.d;
+  // CHECK-DAG: 2024-07-12-symbolic-size-minimization.c:[[@LINE+1]]: memory error: out of bound pointer
+  if (a[7] == 12) {
+    *a += 12;
+  }
+
+  // Check that exists at least one path with size exactly 32
+  // CHECK-DAG: name: 'unnamed'
+  // CHECK-DAG: size: 32
+  return a;
+}
+
+int main() {
+  int *a;
+  klee_make_symbolic(&a, sizeof(a), "a");
+  ////////////////////////////////////////////
+  int *b;
+  klee_make_symbolic(&b, sizeof(b), "b");
+  ////////////////////////////////////////////
+  int c;
+  klee_make_symbolic(&c, sizeof(c), "c");
+  ////////////////////////////////////////////
+  struct AB ab;
+  klee_make_symbolic(&ab, sizeof(ab), "ab");
+  ////////////////////////////////////////////
+  struct AB ab2;
+  klee_make_symbolic(&ab2, sizeof(ab2), "ab2");
+  ////////////////////////////////////////////
+  int *utbot_result;
+  klee_make_symbolic(&utbot_result, sizeof(utbot_result), "utbot_result");
+  utbot_result = sum(a, b, c, ab, ab2);
+  return 0;
+}