Skip to content

Commit ba0a8c1

Browse files
committed
fix tests and format
1 parent f225510 commit ba0a8c1

12 files changed

Lines changed: 188 additions & 74 deletions

File tree

CMakeLists.txt

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -305,7 +305,7 @@ endif()
305305
################################################################################
306306
# Detect SQLite3
307307
################################################################################
308-
find_package(SQLite3 REQUIRED)
308+
find_package(SQLite3)
309309
if (NOT SQLite3_FOUND)
310310
message( FATAL_ERROR "SQLite3 not found, please install" )
311311
endif()
@@ -665,6 +665,8 @@ option(ENABLE_XML_ANNOTATION "Enable XML annotation" ON)
665665

666666
if (ENABLE_XML_ANNOTATION)
667667
message(STATUS "XML annotation is enabled")
668+
file(COPY "${CMAKE_SOURCE_DIR}/submodules/pugiconfig.hpp"
669+
DESTINATION "${CMAKE_SOURCE_DIR}/submodules/pugixml/src")
668670
include_directories("${CMAKE_SOURCE_DIR}/submodules/pugixml/src")
669671
else()
670672
message(STATUS "XML annotation is disabled")

include/klee/Module/Annotation.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -66,17 +66,17 @@ bool operator==(const Ptr &first, const Ptr &second);
6666

6767
// Annotation format: https://github.com/UnitTestBot/klee/discussions/92
6868
struct Annotation {
69-
70-
bool operator==(const Annotation &other) const;
71-
7269
std::string functionName;
7370
std::vector<Statement::Ptr> returnStatements;
7471
std::vector<std::vector<Statement::Ptr>> argsStatements;
7572
std::set<Statement::Property> properties;
73+
74+
bool operator==(const Annotation &other) const;
7675
};
7776

7877
using AnnotationsMap = std::map<std::string, Annotation>;
7978

79+
AnnotationsMap parseAnnotationsJson(const json &annotationsJson);
8080
AnnotationsMap parseAnnotations(const std::string &path, const llvm::Module *m);
8181
} // namespace klee
8282

lib/Core/CMakeLists.txt

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -45,10 +45,8 @@ target_link_libraries(kleeCore PRIVATE
4545
kleeSupport
4646
)
4747

48-
find_package(SQLite3 REQUIRED)
49-
5048
llvm_config(kleeCore "${USE_LLVM_SHARED}" core executionengine mcjit native support)
51-
target_link_libraries(kleeCore PRIVATE sqlite3)
49+
target_link_libraries(kleeCore PRIVATE ${SQLite3_LIBRARIES})
5250
target_include_directories(kleeCore PRIVATE ${KLEE_INCLUDE_DIRS} ${LLVM_INCLUDE_DIRS} ${SQLite3_INCLUDE_DIRS})
5351
target_compile_options(kleeCore PRIVATE ${KLEE_COMPONENT_CXX_FLAGS})
5452
target_compile_definitions(kleeCore PRIVATE ${KLEE_COMPONENT_CXX_DEFINES})

lib/Core/ExecutionState.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,6 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS
2626
#include "llvm/IR/Function.h"
2727
#include "llvm/Support/CommandLine.h"
2828
#include "llvm/Support/raw_ostream.h"
29-
#include "klee/Support/ErrorHandling.h"
3029
DISABLE_WARNING_POP
3130

3231
#include <cassert>

lib/Core/Executor.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -581,9 +581,10 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
581581
// TODO: move this to function
582582
std::map<std::string, llvm::Type *> externals =
583583
getAllExternals(ignoredExternals);
584-
MockBuilder builder(kmodule->module.get(), opts.MainCurrentName,
585-
opts.MainNameAfterMock, externals, opts.AnnotationsFile);
586-
std::unique_ptr<llvm::Module> mockModule = builder.build();
584+
MockBuilder mockBuilder(kmodule->module.get(), opts.MainCurrentName,
585+
opts.MainNameAfterMock, externals,
586+
opts.AnnotationsFile);
587+
std::unique_ptr<llvm::Module> mockModule = mockBuilder.build();
587588
if (!mockModule) {
588589
klee_error("Unable to generate mocks");
589590
}
@@ -597,7 +598,7 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
597598

598599
std::vector<std::unique_ptr<llvm::Module>> mockModules;
599600
mockModules.push_back(std::move(mockModule));
600-
kmodule->link(mockModules, 0);
601+
kmodule->link(mockModules, 1);
601602

602603
for (auto &global : kmodule->module->globals()) {
603604
if (global.isDeclaration()) {

lib/Core/MockBuilder.cpp

Lines changed: 36 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,12 @@
11
#include "klee/Core/MockBuilder.h"
22

3+
#include "klee/Config/Version.h"
34
#include "klee/Module/Annotation.h"
45
#include "klee/Support/ErrorHandling.h"
6+
57
#include "llvm/IR/IRBuilder.h"
68
#include "llvm/IR/Module.h"
7-
#include <llvm/Support/raw_ostream.h>
9+
#include "llvm/Support/raw_ostream.h"
810

911
#include <memory>
1012
#include <utility>
@@ -98,8 +100,19 @@ void MockBuilder::buildExternalGlobalsDefinitions() {
98100
}
99101
}
100102

101-
// TODO: discuss should we annotate not external function
102103
void MockBuilder::buildExternalFunctionsDefinitions() {
104+
bool mockAllAnnotation = true;
105+
106+
if (mockAllAnnotation) {
107+
for (const auto &i : annotations) {
108+
llvm::Function *func = userModule->getFunction(i.first);
109+
auto ext = externals.find(i.first);
110+
if (ext == externals.end()) {
111+
externals[i.first] = func->getType();
112+
}
113+
}
114+
}
115+
103116
for (const auto &it : externals) {
104117
if (!it.second->isFunctionTy()) {
105118
continue;
@@ -133,7 +146,9 @@ void MockBuilder::buildExternalFunctionsDefinitions() {
133146
annotation.returnStatements);
134147
buildAnnotationForExternalFunctionProperties(func, annotation.properties);
135148
} else {
136-
buildAnnotationForExternalFunctionReturn(func, {});
149+
// Default annotation for externals return
150+
buildAnnotationForExternalFunctionReturn(
151+
func, {std::make_shared<Statement::InitNull>()});
137152
}
138153
}
139154
}
@@ -172,7 +187,8 @@ MockBuilder::goByOffset(llvm::Value *value,
172187
if (!current->getType()->isPointerTy()) {
173188
klee_error("Incorrect annotation offset.");
174189
}
175-
current = builder->CreateLoad(current);
190+
current = builder->CreateLoad(current->getType()->getPointerElementType(),
191+
current);
176192
} else if (inst == "&") {
177193
auto addr = builder->CreateAlloca(current->getType());
178194
current = builder->CreateStore(current, addr);
@@ -236,7 +252,15 @@ bool tryAlign(llvm::Function *func,
236252
}
237253

238254
for (size_t i = 0, j = 0; j < func->arg_size() && i < statements.size();) {
239-
while (isCorrectStatements(statements[i], func->getArg(j))) {
255+
while (true) {
256+
#if LLVM_VERSION_CODE >= LLVM_VERSION(10, 0)
257+
auto arg = func->getArg(j);
258+
#else
259+
auto arg = &func->arg_begin()[j];
260+
#endif
261+
if (isCorrectStatements(statements[i], arg)) {
262+
break;
263+
}
240264
res.emplace_back();
241265
j++;
242266
if (j >= func->arg_size()) {
@@ -264,7 +288,11 @@ void MockBuilder::buildAnnotationForExternalFunctionArgs(
264288
return;
265289
}
266290
for (size_t i = 0; i < statements.size(); i++) {
291+
#if LLVM_VERSION_CODE >= LLVM_VERSION(10, 0)
267292
const auto arg = func->getArg(i);
293+
#else
294+
const auto arg = &func->arg_begin()[i];
295+
#endif
268296
for (const auto &statement : statements[i]) {
269297
llvm::Value *elem = goByOffset(arg, statement->offset);
270298
switch (statement->getKind()) {
@@ -288,7 +316,7 @@ void MockBuilder::buildAnnotationForExternalFunctionArgs(
288316
mockModule->getContext(), derefCondName, newFunc);
289317
llvm::BasicBlock *contBB = llvm::BasicBlock::Create(
290318
mockModule->getContext(), "continue_" + derefCondName);
291-
auto brValue = builder->CreateLoad(derefCond);
319+
auto brValue = builder->CreateLoad(intType, derefCond);
292320
builder->CreateCondBr(brValue, derefBB, contBB);
293321

294322
builder->SetInsertPoint(derefBB);
@@ -320,7 +348,8 @@ void MockBuilder::buildAnnotationForExternalFunctionReturn(
320348
auto *loadInst =
321349
builder->CreateLoad(func->getReturnType(), mockReturnValue, retName);
322350

323-
bool initNull = false;
351+
// For non pointer type do nothing, same as InitNull
352+
bool initNull = !returnType->isPointerTy();
324353

325354
for (const auto &statement : statements) {
326355
switch (statement->getKind()) {
@@ -329,9 +358,6 @@ void MockBuilder::buildAnnotationForExternalFunctionReturn(
329358
func->getName().str().c_str());
330359
break;
331360
case Statement::Kind::InitNull: {
332-
if (!returnType->isPointerTy()) {
333-
klee_error("incorrect type for InitNull");
334-
}
335361
initNull = true;
336362
break;
337363
}

lib/Core/SpecialFunctionHandler.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -957,10 +957,8 @@ void SpecialFunctionHandler::handleMakeMock(ExecutionState &state,
957957
return;
958958
}
959959

960-
961960
KFunction *kf = target->parent->parent;
962961

963-
964962
Executor::ExactResolutionList rl;
965963
executor.resolveExact(state, arguments[0],
966964
executor.typeSystemManager->getUnknownType(), rl,
@@ -998,8 +996,9 @@ void SpecialFunctionHandler::handleMakeMock(ExecutionState &state,
998996
klee_error("klee_make_mock is not allowed when mock strategy is none");
999997
break;
1000998
case MockStrategy::Naive:
1001-
source = SourceBuilder::mockNaive(executor.kmodule.get(), *kf->function,
1002-
executor.updateNameVersion(state, name));
999+
source =
1000+
SourceBuilder::mockNaive(executor.kmodule.get(), *kf->function,
1001+
executor.updateNameVersion(state, name));
10031002
break;
10041003
case MockStrategy::Deterministic:
10051004
std::vector<ref<Expr>> args(kf->numArgs);
@@ -1010,10 +1009,11 @@ void SpecialFunctionHandler::handleMakeMock(ExecutionState &state,
10101009
*kf->function, args);
10111010
break;
10121011
}
1013-
executor.executeMakeSymbolic(state, mo, old->getDynamicType(), source, false);
1012+
executor.executeMakeSymbolic(state, mo, old->getDynamicType(), source,
1013+
false);
10141014
} else {
1015-
executor.terminateStateOnUserError(
1016-
*s, "Wrong size given to klee_make_mock");
1015+
executor.terminateStateOnUserError(*s,
1016+
"Wrong size given to klee_make_mock");
10171017
}
10181018
}
10191019
}

lib/Module/Annotation.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,8 @@ inline Statement::Kind stringToKind(const std::string &str) {
9696
}
9797

9898
Ptr stringToKindPtr(const std::string &str) {
99-
switch (stringToKind(toLower(str))) {
99+
std::string statementStr = toLower(str.substr(0, str.find(':')));
100+
switch (stringToKind(statementStr)) {
100101
case Statement::Kind::Unknown:
101102
return std::make_shared<Unknown>(str);
102103
case Statement::Kind::Deref:
@@ -287,6 +288,9 @@ AnnotationsMap parseAnnotationsXml(const pugi::xml_document &annotationsXml,
287288

288289
AnnotationsMap parseAnnotations(const std::string &path,
289290
const llvm::Module *m) {
291+
if (path.empty()) {
292+
return {};
293+
}
290294
std::ifstream annotationsFile(path);
291295
if (!annotationsFile.good()) {
292296
klee_error("Annotation: Opening %s failed.", path.c_str());

submodules/pugiconfig.hpp

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
/**
2+
* pugixml parser - version 1.13
3+
* --------------------------------------------------------
4+
* Copyright (C) 2006-2022, by Arseny Kapoulkine (arseny.kapoulkine@gmail.com)
5+
* Report bugs and download new versions at https://pugixml.org/
6+
*
7+
* This library is distributed under the MIT License. See notice at the end
8+
* of this file.
9+
*
10+
* This work is based on the pugxml parser, which is:
11+
* Copyright (C) 2003, by Kristen Wegner (kristen@tima.net)
12+
*/
13+
14+
#ifndef HEADER_PUGICONFIG_HPP
15+
#define HEADER_PUGICONFIG_HPP
16+
17+
// Uncomment this to enable wchar_t mode
18+
// #define PUGIXML_WCHAR_MODE
19+
20+
// Uncomment this to enable compact mode
21+
// #define PUGIXML_COMPACT
22+
23+
// Uncomment this to disable XPath
24+
// #define PUGIXML_NO_XPATH
25+
26+
// Uncomment this to disable STL
27+
// #define PUGIXML_NO_STL
28+
29+
// Uncomment this to disable exceptions
30+
#define PUGIXML_NO_EXCEPTIONS
31+
32+
// Set this to control attributes for public classes/functions, i.e.:
33+
// to export all public symbols from DLL
34+
// #define PUGIXML_API __declspec(dllexport)
35+
// to import all classes from DLL
36+
// #define PUGIXML_CLASS __declspec(dllimport)
37+
// to set calling conventions to all public functions to fastcall
38+
// #define PUGIXML_FUNCTION __fastcall
39+
// In absence of PUGIXML_CLASS/PUGIXML_FUNCTION definitions PUGIXML_API
40+
// is used instead
41+
42+
// Tune these constants to adjust memory-related behavior
43+
// #define PUGIXML_MEMORY_PAGE_SIZE 32768
44+
// #define PUGIXML_MEMORY_OUTPUT_STACK 10240
45+
// #define PUGIXML_MEMORY_XPATH_PAGE_SIZE 4096
46+
47+
// Tune this constant to adjust max nesting for XPath queries
48+
// #define PUGIXML_XPATH_DEPTH_LIMIT 1024
49+
50+
// Uncomment this to switch to header-only version
51+
// #define PUGIXML_HEADER_ONLY
52+
53+
// Uncomment this to enable long long support
54+
// #define PUGIXML_HAS_LONG_LONG
55+
56+
#endif
57+
58+
/**
59+
* Copyright (c) 2006-2022 Arseny Kapoulkine
60+
*
61+
* Permission is hereby granted, free of charge, to any person
62+
* obtaining a copy of this software and associated documentation
63+
* files (the "Software"), to deal in the Software without
64+
* restriction, including without limitation the rights to use,
65+
* copy, modify, merge, publish, distribute, sublicense, and/or sell
66+
* copies of the Software, and to permit persons to whom the
67+
* Software is furnished to do so, subject to the following
68+
* conditions:
69+
*
70+
* The above copyright notice and this permission notice shall be
71+
* included in all copies or substantial portions of the Software.
72+
*
73+
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
74+
* EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
75+
* OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
76+
* NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
77+
* HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
78+
* WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
79+
* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
80+
* OTHER DEALINGS IN THE SOFTWARE.
81+
*/

test/Feature/MockPointersDeterministic.c

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@
55
// RUN: %klee --solver-backend=z3 --output-dir=%t.klee-out-1 --skip-not-lazy-initialized --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-1
66
// CHECK-1: memory error: null pointer exception
77
// CHECK-1: KLEE: done: completed paths = 1
8-
// CHECK-1: KLEE: done: partially completed paths = 2
9-
// CHECK-1: KLEE: done: generated tests = 3
8+
// CHECK-1: KLEE: done: partially completed paths = 1
9+
// CHECK-1: KLEE: done: generated tests = 2
1010

1111
#include <assert.h>
1212

@@ -20,4 +20,4 @@ int main() {
2020
assert(0 && "age is deterministic");
2121
}
2222
return *age();
23-
}
23+
}

0 commit comments

Comments
 (0)