Skip to content

Commit

Permalink
Merge some args for external calls
Browse files Browse the repository at this point in the history
  • Loading branch information
@ladisgin
ladisgin committed Nov 3, 2023
1 parent 635ef23 commit e8be3d8
Show file tree
Hide file tree
Showing 18 changed files with 107 additions and 150 deletions.
5 changes: 2 additions & 3 deletions configs/options.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,15 +24,14 @@
"--suppress-external-warnings",
"--libc=klee",
"--skip-not-lazy-initialized",
"--external-calls=all",
"--external-calls=mock",
"--output-source=false",
"--output-istats=false",
"--output-stats=false",
"--max-time=${maxTime}s",
"--max-sym-alloc=${maxSymAlloc}",
"--max-forks=${maxForks}",
"--max-solver-time=${maxSolverTime}s",
"--mock-all-externals",
"--smart-resolve-entry-function",
"--extern-calls-can-return-null",
"--align-symbolic-pointers=false",
Expand All @@ -49,4 +48,4 @@
]
}
]
}
}
17 changes: 10 additions & 7 deletions include/klee/Core/Interpreter.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,11 +68,14 @@ using FLCtoOpcode = std::unordered_map<
std::unordered_map<
unsigned, std::unordered_map<unsigned, std::unordered_set<unsigned>>>>;

enum class MockStrategy {
None, // No mocks are generated
Naive, // For each function call new symbolic value is generated
Deterministic, // Each function is treated as uninterpreted function in SMT.
// Compatible with Z3 solver only
/*** External call policy options ***/

enum class ExternalCallPolicy {
None, // No external calls allowed
Concrete, // Only external calls with concrete arguments allowed
All, // All external calls allowed
Mock, // For each function call new symbolic value is generated
MockDeterm, // Each function is treated as uninterpreted function in SMT.
};

class Interpreter {
Expand Down Expand Up @@ -135,11 +138,11 @@ class Interpreter {
unsigned MakeConcreteSymbolic;
GuidanceKind Guidance;
nonstd::optional<SarifReport> Paths;
enum MockStrategy MockStrategy;
enum ExternalCallPolicy ExternalCall;

InterpreterOptions(nonstd::optional<SarifReport> Paths)
: MakeConcreteSymbolic(false), Guidance(GuidanceKind::NoGuidance),
Paths(std::move(Paths)), MockStrategy(MockStrategy::None) {}
Paths(std::move(Paths)), ExternalCall(ExternalCallPolicy::None) {}
};

protected:
Expand Down
81 changes: 14 additions & 67 deletions lib/Core/Executor.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -289,30 +289,6 @@ cl::opt<bool>
"querying the solver (default=true)"),
cl::cat(SolvingCat));

/*** External call policy options ***/

enum class ExternalCallPolicy {
None, // No external calls allowed
Concrete, // Only external calls with concrete arguments allowed
All, // All external calls allowed
};

cl::opt<ExternalCallPolicy> ExternalCalls(
"external-calls", cl::desc("Specify the external call policy"),
cl::values(
clEnumValN(
ExternalCallPolicy::None, "none",
"No external function calls are allowed. Note that KLEE always "
"allows some external calls with concrete arguments to go through "
"(in particular printf and puts), regardless of this option."),
clEnumValN(ExternalCallPolicy::Concrete, "concrete",
"Only external function calls with concrete arguments are "
"allowed (default)"),
clEnumValN(ExternalCallPolicy::All, "all",
"All external function calls are allowed. This concretizes "
"any symbolic arguments in calls to external functions.")),
cl::init(ExternalCallPolicy::Concrete), cl::cat(ExtCallsCat));

cl::opt<bool> SuppressExternalWarnings(
"suppress-external-warnings", cl::init(false),
cl::desc("Supress warnings about calling external functions."),
Expand All @@ -332,10 +308,6 @@ cl::opt<bool>
"If false, fails on externall calls."),
cl::cat(ExtCallsCat));

cl::opt<bool> MockAllExternals("mock-all-externals", cl::init(false),
cl::desc("If true, all externals are mocked."),
cl::cat(ExtCallsCat));

/*** Seeding options ***/

cl::opt<bool> AlwaysOutputSeeds(
Expand Down Expand Up @@ -496,7 +468,7 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
inhibitForking(false), coverOnTheFly(false),
haltExecution(HaltExecution::NotHalt), ivcEnabled(false),
debugLogBuffer(debugBufferString) {
if (interpreterOpts.MockStrategy == MockStrategy::Deterministic &&
if (interpreterOpts.ExternalCall == ExternalCallPolicy::MockDeterm &&
CoreSolverToUse != Z3_SOLVER) {
klee_error("Deterministic mocks can be generated with Z3 solver only.\n");
}
Expand Down Expand Up @@ -573,8 +545,8 @@ llvm::Module *Executor::setModule(
assert(!kmodule && !userModules.empty() &&
"can only register one module"); // XXX gross

if (ExternalCalls == ExternalCallPolicy::All &&
interpreterOpts.MockStrategy != MockStrategy::None) {
if (interpreterOpts.ExternalCall == ExternalCallPolicy::Mock ||
interpreterOpts.ExternalCall == ExternalCallPolicy::MockDeterm) {
llvm::Function *mainFn =
userModules.front()->getFunction(opts.MainCurrentName);
if (!mainFn) {
Expand Down Expand Up @@ -608,8 +580,8 @@ llvm::Module *Executor::setModule(
kmodule->instrument(opts);
}

if ((ExternalCalls == ExternalCallPolicy::All &&
interpreterOpts.MockStrategy != MockStrategy::None) ||
if (interpreterOpts.ExternalCall == ExternalCallPolicy::Mock ||
interpreterOpts.ExternalCall == ExternalCallPolicy::MockDeterm ||
!opts.AnnotationsFile.empty()) {
MockBuilder mockBuilder(kmodule->module.get(), opts, ignoredExternals,
redefinitions, interpreterHandler);
Expand Down Expand Up @@ -975,11 +947,7 @@ void Executor::initializeGlobalObjects(ExecutionState &state) {
} else {
addr = externalDispatcher->resolveSymbol(v.getName().str());
}
if (MockAllExternals && !addr) {
executeMakeSymbolic(
state, mo, typeSystemManager->getWrappedType(v.getType()),
SourceBuilder::irreproducible("mockExternGlobalObject"), false);
} else if (!addr) {
if (!addr) {
klee_error("Unable to load symbol(%.*s) while initializing globals",
static_cast<int>(v.getName().size()), v.getName().data());
} else {
Expand Down Expand Up @@ -2887,7 +2855,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {

if (auto *asmValue =
dyn_cast<InlineAsm>(fp)) { // TODO: move to `executeCall`
if (ExternalCalls != ExternalCallPolicy::None) {
if (interpreterOpts.ExternalCall != ExternalCallPolicy::None) {
KInlineAsm callable(asmValue);
callExternalFunction(state, ki, &callable, arguments);
} else {
Expand Down Expand Up @@ -4882,36 +4850,14 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
return;
}

if (ExternalCalls == ExternalCallPolicy::None &&
if (interpreterOpts.ExternalCall == ExternalCallPolicy::None &&
!okExternals.count(callable->getName().str())) {
klee_warning("Disallowed call to external function: %s\n",
callable->getName().str().c_str());
terminateStateOnUserError(state, "external calls disallowed");
return;
}

if (ExternalCalls == ExternalCallPolicy::All && MockAllExternals) {
std::string TmpStr;
llvm::raw_string_ostream os(TmpStr);
os << "calling external: " << callable->getName().str() << "(";
for (unsigned i = 0; i < arguments.size(); i++) {
os << arguments[i];
if (i != arguments.size() - 1)
os << ", ";
}
os << ") at " << state.pc->getSourceLocationString();

if (AllExternalWarnings)
klee_warning("%s", os.str().c_str());
else if (!SuppressExternalWarnings)
klee_warning_once(callable->getValue(), "%s", os.str().c_str());

if (target->inst->getType()->isSized()) {
prepareMockValue(state, "mockExternResult", target);
}
return;
}

// normal external function handling path
// allocate 512 bits for each argument (+return value) to support
// fp80's and SIMD vectors as parameters for external calls;
Expand All @@ -4931,8 +4877,9 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
for (std::vector<ref<Expr>>::iterator ai = arguments.begin(),
ae = arguments.end();
ai != ae; ++ai) {
if (ExternalCalls ==
ExternalCallPolicy::All) { // don't bother checking uniqueness
if (interpreterOpts.ExternalCall == ExternalCallPolicy::All ||
interpreterOpts.ExternalCall == ExternalCallPolicy::Mock ||
interpreterOpts.ExternalCall == ExternalCallPolicy::MockDeterm) { // don't bother checking uniqueness
*ai = optimizer.optimizeExpr(*ai, true);
ref<ConstantExpr> ce;
bool success = solver->getValue(state.constraints.cs(), *ai, ce,
Expand Down Expand Up @@ -6082,10 +6029,10 @@ void Executor::executeMemoryOperation(

ref<SolverResponse> response;
solver->setTimeout(coreSolverTimeout);
bool success = solver->getResponse(state->constraints.cs(), inBounds,
response, state->queryMetaData);
bool solverResponse = solver->getResponse(state->constraints.cs(), inBounds,
response, state->queryMetaData);
solver->setTimeout(time::Span());
if (!success) {
if (!solverResponse) {
state->pc = state->prevPC;
terminateStateOnSolverError(*state, "Query timed out (bounds check).");
return;
Expand Down
17 changes: 11 additions & 6 deletions lib/Core/SpecialFunctionHandler.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -991,16 +991,14 @@ void SpecialFunctionHandler::handleMakeMock(ExecutionState &state,

if (res) {
ref<SymbolicSource> source;
switch (executor.interpreterOpts.MockStrategy) {
case MockStrategy::None:
klee_error("klee_make_mock is not allowed when mock strategy is none");
break;
case MockStrategy::Naive:
switch (executor.interpreterOpts.ExternalCall) {
case ExternalCallPolicy::Mock: {
source =
SourceBuilder::mockNaive(executor.kmodule.get(), *kf->function,
executor.updateNameVersion(state, name));
break;
case MockStrategy::Deterministic:
}
case ExternalCallPolicy::MockDeterm: {
std::vector<ref<Expr>> args(kf->getNumArgs());
for (size_t i = 0; i < kf->getNumArgs(); i++) {
args[i] = executor.getArgumentCell(state, kf, i).value;
Expand All @@ -1009,6 +1007,13 @@ void SpecialFunctionHandler::handleMakeMock(ExecutionState &state,
*kf->function, args);
break;
}
case ExternalCallPolicy::Concrete:
case ExternalCallPolicy::All:
case ExternalCallPolicy::None: {
klee_error("klee_make_mock is not allowed when mock strategy is none");
break;
}
}
executor.executeMakeSymbolic(state, mo, old->getDynamicType(), source,
false);
} else {
Expand Down
14 changes: 6 additions & 8 deletions lib/Solver/Z3Builder.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -266,18 +266,16 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) {
} else if (ref<MockDeterministicSource> mockDeterministicSource =
dyn_cast<MockDeterministicSource>(root->source)) {
size_t num_args = mockDeterministicSource->args.size();
// TODO looks like too much vectors
std::vector<Z3ASTHandle> argsHandled(num_args);
std::vector<Z3SortHandle> argsSortHandled(num_args);
std::vector<Z3_ast> args(num_args);
std::vector<Z3_sort> argsSort(num_args);
for (size_t i = 0; i < num_args; i++) {
ref<Expr> kid = mockDeterministicSource->args[i];
int kidWidth = kid->getWidth();
argsHandled[i] = construct(kid, &kidWidth);
args[i] = argsHandled[i];
argsSortHandled[i] = Z3SortHandle(Z3_get_sort(ctx, args[i]), ctx);
argsSort[i] = argsSortHandled[i];
Z3ASTHandle argsHandle = construct(kid, &kidWidth);
args[i] = argsHandle;
Z3SortHandle z3SortHandle =
Z3SortHandle(Z3_get_sort(ctx, args[i]), ctx);
argsSort[i] = z3SortHandle;
}

Z3SortHandle domainSort = getBvSort(root->getDomain());
Expand All @@ -295,7 +293,7 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) {
ctx);
array_expr =
Z3ASTHandle(Z3_mk_app(ctx, func, num_args, args.data()), ctx);
} else {
} else {
array_expr =
buildArray(unique_name.c_str(), root->getDomain(), root->getRange());
}
Expand Down
8 changes: 4 additions & 4 deletions test/Feature/Annotation/AllocSource.c
View file
Original file line number Diff line number Diff line change
@@ -1,19 +1,19 @@
// REQUIRES: z3
// RUN: %clang -DAllocSource1 %s -g -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t1.klee-out-1
// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/AllocSource.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE1
// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/AllocSource.json --external-calls=mock --mock-modeled-functions -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE1

// RUN: %clang -DAllocSource2 %s -g -emit-llvm %O0opt -c -o %t2.bc
// RUN: rm -rf %t2.klee-out-1
// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/AllocSource.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE2
// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/AllocSource.json --external-calls=mock --mock-modeled-functions -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE2

// RUN: %clang -DAllocSource3 %s -g -emit-llvm %O0opt -c -o %t3.bc
// RUN: rm -rf %t3.klee-out-1
// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/AllocSource.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE3
// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/AllocSource.json --external-calls=mock --mock-modeled-functions -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE3

// RUN: %clang -DAllocSource4 %s -g -emit-llvm %O0opt -c -o %t4.bc
// RUN: rm -rf %t4.klee-out-1
// RUN: %klee --solver-backend=z3 --output-dir=%t4.klee-out-1 --annotations=%S/AllocSource.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t4.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE4
// RUN: %klee --solver-backend=z3 --output-dir=%t4.klee-out-1 --annotations=%S/AllocSource.json --external-calls=mock --mock-modeled-functions -emit-all-errors=true %t4.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE4

#include <assert.h>

Expand Down
16 changes: 8 additions & 8 deletions test/Feature/Annotation/Deref.c
View file
Original file line number Diff line number Diff line change
@@ -1,36 +1,36 @@
// REQUIRES: z3
// RUN: %clang -DDeref1 %s -g -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t1.klee-out-1
// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF1
// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/Deref.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF1

// RUN: %clang -DDeref2 %s -g -emit-llvm %O0opt -c -o %t2.bc
// RUN: rm -rf %t2.klee-out-1
// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF2
// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/Deref.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF2

// RUN: %clang -DDeref3 %s -g -emit-llvm %O0opt -c -o %t3.bc
// RUN: rm -rf %t3.klee-out-1
// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF3
// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/Deref.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF3

// RUN: %clang -DDeref4 %s -g -emit-llvm %O0opt -c -o %t4.bc
// RUN: rm -rf %t4.klee-out-1
// RUN: %klee --solver-backend=z3 --output-dir=%t4.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t4.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF4
// RUN: %klee --solver-backend=z3 --output-dir=%t4.klee-out-1 --annotations=%S/Deref.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t4.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF4

// RUN: %clang -DDeref5 %s -g -emit-llvm %O0opt -c -o %t5.bc
// RUN: rm -rf %t5.klee-out-1
// RUN: %klee --solver-backend=z3 --output-dir=%t5.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t5.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF5
// RUN: %klee --solver-backend=z3 --output-dir=%t5.klee-out-1 --annotations=%S/Deref.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t5.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF5

// RUN: %clang -DDeref6 %s -g -emit-llvm %O0opt -c -o %t6.bc
// RUN: rm -rf %t6.klee-out-1
// RUN: %klee --solver-backend=z3 --output-dir=%t6.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t6.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF6
// RUN: %klee --solver-backend=z3 --output-dir=%t6.klee-out-1 --annotations=%S/Deref.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t6.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF6

// RUN: %clang -DHASVALUE -DDeref1 -DDeref2 -DDeref3 -DDeref4 -DDeref5 -DDeref6 %s -g -emit-llvm %O0opt -c -o %t7.bc
// RUN: rm -rf %t7.klee-out-1
// RUN: %klee --solver-backend=z3 --output-dir=%t7.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t7.bc 2>&1 | FileCheck %s -check-prefix=CHECK-NODEREF
// RUN: %klee --solver-backend=z3 --output-dir=%t7.klee-out-1 --annotations=%S/Deref.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t7.bc 2>&1 | FileCheck %s -check-prefix=CHECK-NODEREF
// CHECK-NODEREF-NOT: memory error: null pointer exception

// RUN: %clang -DDeref1 -DDeref2 -DDeref3 -DDeref4 -DDeref5 -DDeref6 %s -g -emit-llvm %O0opt -c -o %t8.bc
// RUN: rm -rf %t8.klee-out-1
// RUN: %klee --solver-backend=z3 --output-dir=%t8.klee-out-1 --annotations=%S/EmptyAnnotation.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t8.bc 2>&1 | FileCheck %s -check-prefix=CHECK-EMPTY
// RUN: %klee --solver-backend=z3 --output-dir=%t8.klee-out-1 --annotations=%S/EmptyAnnotation.json --external-calls=mock --mock-modeled-functions --emit-all-errors=true %t8.bc 2>&1 | FileCheck %s -check-prefix=CHECK-EMPTY
// CHECK-EMPTY-NOT: memory error: null pointer exception
// CHECK-EMPTY: partially completed paths = 0
// CHECK-EMPTY: generated tests = 1
Expand Down
Loading

0 comments on commit e8be3d8

Please sign in to comment.