From 8fa8e6852533ee7b9d8ba7083069a425d999c8e9 Mon Sep 17 00:00:00 2001 From: Yurii Kostyukov Date: Mon, 2 Oct 2023 17:51:25 +0300 Subject: [PATCH] [fix] Tests for states with mocks --- lib/Core/ExecutionState.cpp | 20 ------ lib/Core/ExecutionState.h | 1 - lib/Core/Executor.cpp | 68 +++++++++++++++---- lib/Core/Executor.h | 1 + .../2023-10-02-test-from-mocked-global.c | 16 +++++ 5 files changed, 70 insertions(+), 36 deletions(-) create mode 100644 test/regression/2023-10-02-test-from-mocked-global.c diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index f1152938e77..5ee6b7c8dab 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -363,26 +363,6 @@ void ExecutionState::addUniquePointerResolution(ref address, } } -bool ExecutionState::resolveOnSymbolics(const ref &addr, - IDType &result) const { - uint64_t address = addr->getZExtValue(); - - for (const auto &res : symbolics) { - const auto &mo = res.memoryObject; - // Check if the provided address is between start and end of the object - // [mo->address, mo->address + mo->size) or the object is a 0-sized object. - ref size = cast( - constraints.cs().concretization().evaluate(mo->getSizeExpr())); - if ((size->getZExtValue() == 0 && address == mo->address) || - (address - mo->address < size->getZExtValue())) { - result = mo->id; - return true; - } - } - - return false; -} - /**/ llvm::raw_ostream &klee::operator<<(llvm::raw_ostream &os, diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index a40c6a09820..424dfc42485 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -428,7 +428,6 @@ class ExecutionState { unsigned size = 0); void addUniquePointerResolution(ref address, const MemoryObject *mo, unsigned size = 0); - bool resolveOnSymbolics(const ref &addr, IDType &result) const; void addConstraint(ref e, const Assignment &c); void addCexPreference(const ref &cond); diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 63130c38d8c..93503ec2aa9 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -6949,19 +6949,43 @@ void Executor::logState(const ExecutionState &state, int id, } } -void Executor::setInitializationGraph(const ExecutionState &state, - const Assignment &model, KTest &ktest) { +bool resolveOnSymbolics(const std::vector &symbolics, + const Assignment &assn, + const ref &addr, IDType &result) { + uint64_t address = addr->getZExtValue(); + + for (const auto &res : symbolics) { + const auto &mo = res.memoryObject; + // Check if the provided address is between start and end of the object + // [mo->address, mo->address + mo->size) or the object is a 0-sized object. + ref size = + cast(assn.evaluate(mo->getSizeExpr())); + if ((size->getZExtValue() == 0 && address == mo->address) || + (address - mo->address < size->getZExtValue())) { + result = mo->id; + return true; + } + } + + return false; +} + +void Executor::setInitializationGraph( + const ExecutionState &state, const std::vector &symbolics, + const Assignment &model, KTest &ktest) { std::map> pointers; std::map>> s; ExprHashMap>> resolvedPointers; std::unordered_map> idToSymbolics; - for (const auto &symbolic : state.symbolics) { + for (const auto &symbolic : symbolics) { ref mo = symbolic.memoryObject; idToSymbolics[mo->id] = mo; } - for (const auto &symbolic : state.symbolics) { + const klee::Assignment &assn = state.constraints.cs().concretization(); + + for (const auto &symbolic : symbolics) { KType *symbolicType = symbolic.type; if (!symbolicType->getRawType()) { continue; @@ -6989,7 +7013,7 @@ void Executor::setInitializationGraph(const ExecutionState &state, ref constantAddress = cast(addressInModel); IDType idResult; - if (state.resolveOnSymbolics(constantAddress, idResult)) { + if (resolveOnSymbolics(symbolics, assn, constantAddress, idResult)) { ref mo = idToSymbolics[idResult]; resolvedPointers[address] = std::make_pair(idResult, mo->getOffsetExpr(address)); @@ -7024,12 +7048,12 @@ void Executor::setInitializationGraph(const ExecutionState &state, // The objects have to be symbolic bool pointerFound = false, pointeeFound = false; size_t pointerIndex = 0, pointeeIndex = 0; - for (size_t i = 0; i < state.symbolics.size(); i++) { - if (state.symbolics[i].memoryObject == pointerResolution.first) { + for (size_t i = 0; i < symbolics.size(); i++) { + if (symbolics[i].memoryObject == pointerResolution.first) { pointerIndex = i; pointerFound = true; } - if (state.symbolics[i].memoryObject->id == pointer.second.first) { + if (symbolics[i].memoryObject->id == pointer.second.first) { pointeeIndex = i; pointeeFound = true; } @@ -7081,6 +7105,16 @@ Assignment Executor::computeConcretization(const ConstraintSet &constraints, return concretization; } +bool isIrreproducible(const klee::Symbolic &symb) { + auto arr = symb.array; + bool bad = IrreproducibleSource::classof(arr->source.get()); + if (bad) + klee_warning_once(arr->source.get(), + "A irreproducible symbolic %s reaches a test", + arr->getIdentifier().c_str()); + return bad; +} + bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) { solver->setTimeout(coreSolverTimeout); @@ -7117,10 +7151,14 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) { } } + std::vector symbolics(state.symbolics); + std::copy_if(state.symbolics.begin(), state.symbolics.end(), + std::back_inserter(symbolics), isIrreproducible); + std::vector> values; std::vector objects; - for (unsigned i = 0; i != state.symbolics.size(); ++i) - objects.push_back(state.symbolics[i].array); + for (unsigned i = 0; i != symbolics.size(); ++i) + objects.push_back(symbolics[i].array); bool success = solver->getInitialValues(extendedConstraints.cs(), objects, values, state.queryMetaData); solver->setTimeout(time::Span()); @@ -7131,11 +7169,11 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) { return false; } - res.objects = new KTestObject[state.symbolics.size()]; - res.numObjects = state.symbolics.size(); + res.objects = new KTestObject[symbolics.size()]; + res.numObjects = symbolics.size(); - for (unsigned i = 0; i != state.symbolics.size(); ++i) { - auto mo = state.symbolics[i].memoryObject; + for (unsigned i = 0; i != symbolics.size(); ++i) { + auto mo = symbolics[i].memoryObject; KTestObject *o = &res.objects[i]; o->name = const_cast(mo->name.c_str()); o->address = mo->address; @@ -7151,7 +7189,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) { model.bindings.insert(binding); } - setInitializationGraph(state, model, res); + setInitializationGraph(state, symbolics, model, res); return true; } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 1cd6c1c4a0a..26c2e9bba54 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -793,6 +793,7 @@ class Executor : public Interpreter { Interpreter::LogType logFormat = Interpreter::STP) override; void setInitializationGraph(const ExecutionState &state, + const std::vector &symbolics, const Assignment &model, KTest &tc); void logState(const ExecutionState &state, int id, diff --git a/test/regression/2023-10-02-test-from-mocked-global.c b/test/regression/2023-10-02-test-from-mocked-global.c new file mode 100644 index 00000000000..a62eeb9bba0 --- /dev/null +++ b/test/regression/2023-10-02-test-from-mocked-global.c @@ -0,0 +1,16 @@ +// Darwin does not support section attribute: `argument to 'section' attribute is not valid for this target: mach-o section specifier requires a segment whose length is between 1 and 16 characters` +// REQUIRES: not-darwin +// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --mock-all-externals --write-xml-tests --output-dir=%t.klee-out %t1.bc +// RUN: FileCheck --input-file %t.klee-out/test000001.xml %s + +extern void *__crc_mc44s803_attach __attribute__((__weak__)); +static unsigned long const __kcrctab_mc44s803_attach __attribute__((__used__, __unused__, + __section__("___kcrctab+mc44s803_attach"))) = (unsigned long const)((unsigned long)(&__crc_mc44s803_attach)); + +int main() { + return 0; +} + +// CHECK-NOT: