diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 9c37230634..f993845017 100644 --- a/lib/Core/Executor.cpp +++ b/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 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 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 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}); } } diff --git a/lib/Solver/ConcretizingSolver.cpp b/lib/Solver/ConcretizingSolver.cpp index 1d2a75047c..d677f71dcd 100644 --- a/lib/Solver/ConcretizingSolver.cpp +++ b/lib/Solver/ConcretizingSolver.cpp @@ -384,7 +384,8 @@ bool ConcretizingSolver::check(const Query &query, } if (isa(result)) { - for (auto i : cast(result)->validityCore().constraints) { + auto validityCore = cast(result)->validityCore(); + for (auto i : validityCore.constraints) { if (!query.constraints.cs().count(i)) { return false; } diff --git a/test/Feature/SymbolicSizes/MinimizeSize.c b/test/Feature/SymbolicSizes/MinimizeSize.c index c767ff6a97..6ce771f2aa 100644 --- a/test/Feature/SymbolicSizes/MinimizeSize.c +++ b/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 @@ -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 diff --git a/test/regression/2024-07-12-symbolic-size-minimization.c b/test/regression/2024-07-12-symbolic-size-minimization.c new file mode 100644 index 0000000000..a4adf575d5 --- /dev/null +++ b/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; +}