From 1b329b87fe2f3218a71637b799092f88eb676469 Mon Sep 17 00:00:00 2001 From: Sergey Morozov Date: Tue, 25 Jul 2023 13:26:25 +0300 Subject: [PATCH 1/6] [feat] tc support --- include/klee/Module/Target.h | 3 + include/klee/Support/OptionCategories.h | 1 + lib/Core/Executor.cpp | 41 +- lib/Module/Target.cpp | 9 + lib/Module/TargetForest.cpp | 7 +- ...or2c-lazyMod.adding.1.prop1-back-serstep.c | 565 ++++++++++++++++++ tools/klee/main.cpp | 294 ++++++--- 7 files changed, 831 insertions(+), 89 deletions(-) create mode 100644 test/Industry/wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c diff --git a/include/klee/Module/Target.h b/include/klee/Module/Target.h index 80bf7e0c1d..98eb3c900a 100644 --- a/include/klee/Module/Target.h +++ b/include/klee/Module/Target.h @@ -41,6 +41,9 @@ struct ErrorLocation { unsigned int endLine; optional startColumn; optional endColumn; + + ErrorLocation(const klee::ref &loc); + ErrorLocation(const KInstruction *ki); }; class ReproduceErrorTarget; diff --git a/include/klee/Support/OptionCategories.h b/include/klee/Support/OptionCategories.h index c03128f3d9..da1d0d4934 100644 --- a/include/klee/Support/OptionCategories.h +++ b/include/klee/Support/OptionCategories.h @@ -21,6 +21,7 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS DISABLE_WARNING_POP namespace klee { +extern llvm::cl::OptionCategory TestCompCat; extern llvm::cl::OptionCategory ExecCat; extern llvm::cl::OptionCategory DebugCat; extern llvm::cl::OptionCategory ExecCat; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 4af041d3ba..63130c38d8 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -217,6 +217,10 @@ llvm::cl::opt MinNumberElementsLazyInit( "initialization (default 4)"), llvm::cl::init(4), llvm::cl::cat(LazyInitCat)); +cl::opt FunctionCallReproduce( + "function-call-reproduce", cl::init(""), + cl::desc("Marks mentioned function as target for error-guided mode."), + cl::cat(ExecCat)); } // namespace klee namespace { @@ -509,10 +513,6 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, EqualitySubstitution); initializeSearchOptions(); - if (OnlyOutputStatesCoveringNew && !StatsTracker::useIStats()) - klee_error("To use --only-output-states-covering-new, you need to enable " - "--output-istats."); - if (DebugPrintInstructions.isSet(FILE_ALL) || DebugPrintInstructions.isSet(FILE_COMPACT) || DebugPrintInstructions.isSet(FILE_SRC)) { @@ -585,6 +585,13 @@ Executor::setModule(std::vector> &userModules, preservedFunctions.push_back("memcmp"); preservedFunctions.push_back("memmove"); + if (FunctionCallReproduce != "") { + // prevent elimination of the function + auto f = kmodule->module->getFunction(FunctionCallReproduce); + if (f) + f->addFnAttr(Attribute::OptimizeNone); + } + kmodule->optimiseAndPrepare(opts, preservedFunctions); kmodule->checkModule(); @@ -6635,7 +6642,8 @@ void Executor::clearMemory() { void Executor::runFunctionAsMain(Function *f, int argc, char **argv, char **envp) { - if (guidanceKind == GuidanceKind::ErrorGuidance && + if (FunctionCallReproduce == "" && + guidanceKind == GuidanceKind::ErrorGuidance && (!interpreterOpts.Paths.has_value() || interpreterOpts.Paths->empty())) { klee_warning("No targets found in error-guided mode"); return; @@ -6646,9 +6654,26 @@ void Executor::runFunctionAsMain(Function *f, int argc, char **argv, std::vector states; if (guidanceKind == GuidanceKind::ErrorGuidance) { - auto &paths = interpreterOpts.Paths.value(); - auto prepTargets = targetedExecutionManager->prepareTargets( - kmodule.get(), std::move(paths)); + std::map, + klee::TargetedExecutionManager::KFunctionLess> + prepTargets; + if (FunctionCallReproduce == "") { + auto &paths = interpreterOpts.Paths.value(); + prepTargets = targetedExecutionManager->prepareTargets(kmodule.get(), + std::move(paths)); + } else { + /* Find all calls to function specified in .prp file + * and combine them to single target forest */ + KFunction *kEntryFunction = kmodule->functionMap.at(f); + ref forest = new TargetForest(kEntryFunction); + auto kfunction = kmodule->functionNameMap.at(FunctionCallReproduce); + KBlock *kCallBlock = kfunction->entryKBlock; + forest->add(ReproduceErrorTarget::create( + {ReachWithError::Reachable}, "", + ErrorLocation(kCallBlock->getFirstInstruction()), kCallBlock)); + prepTargets.emplace(kEntryFunction, forest); + } + if (prepTargets.empty()) { klee_warning( "No targets found in error-guided mode after prepare targets"); diff --git a/lib/Module/Target.cpp b/lib/Module/Target.cpp index 916e73f0e8..7e6cfab36d 100644 --- a/lib/Module/Target.cpp +++ b/lib/Module/Target.cpp @@ -26,6 +26,15 @@ llvm::cl::opt LocationAccuracy( cl::desc("Check location with line and column accuracy (default=false)")); } +ErrorLocation::ErrorLocation(const klee::ref &loc) + : startLine(loc->startLine), endLine(loc->endLine), + startColumn(loc->startColumn), endColumn(loc->endColumn) {} + +ErrorLocation::ErrorLocation(const KInstruction *ki) { + startLine = (endLine = ki->info->line); + startColumn = (endColumn = ki->info->line); +} + std::string ReproduceErrorTarget::toString() const { std::ostringstream repr; repr << "Target " << getId() << ": "; diff --git a/lib/Module/TargetForest.cpp b/lib/Module/TargetForest.cpp index 0a95f3754f..cb2f8a907e 100644 --- a/lib/Module/TargetForest.cpp +++ b/lib/Module/TargetForest.cpp @@ -117,11 +117,8 @@ void TargetForest::Layer::addTrace( for (auto block : it->second) { ref target = nullptr; if (i == result.locations.size() - 1) { - target = ReproduceErrorTarget::create( - result.errors, result.id, - ErrorLocation{loc->startLine, loc->endLine, loc->startColumn, - loc->endColumn}, - block); + target = ReproduceErrorTarget::create(result.errors, result.id, + ErrorLocation(loc), block); } else { target = ReachBlockTarget::create(block); } diff --git a/test/Industry/wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c b/test/Industry/wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c new file mode 100644 index 0000000000..7a6d4ff09c --- /dev/null +++ b/test/Industry/wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c @@ -0,0 +1,565 @@ +// REQUIRES: z3 +// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false --solver-backend=z3 -max-memory=6008 --optimize=true --skip-not-lazy-initialized -output-source=true --output-stats=false --output-istats=false --write-xml-tests --write-ktests=false --xml-metadata-programfile=wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c --xml-metadata-programhash=a18daeacf63b42ad6e1cb490555b7cdecd71ad6e58b167ed0f5626c03bc3d772 --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --function-call-reproduce=reach_error --dump-states-on-halt=false -exit-on-error-type=Assert --search=dfs --search=random-path -max-time=20 %t1.bc 2>&1 | FileCheck -check-prefix=CHECK-VERDICT %s + +// RUN: test -f %t.klee-out/test000001.xml +// RUN: not test -f %t.klee-out/test000001.ktest + +// CHECK-VERDICT: KLEE: WARNING: 100.00% Reachable Reachable at trace + +//RUN: FileCheck %s -input-file=%t.klee-out/assembly.ll +// the only forking br is in __VERIFIER_assert +// that is, all ternary ifs are turned into `select` instructions +// CHECK: {{call.*reach_error}} +// CHECK-COUNT-11: {{ phi }} + + + + + + +// This file is part of the SV-Benchmarks collection of verification tasks: +// https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks +// +// SPDX-FileCopyrightText: 2007 - 2022 Radek Pelánek +// SPDX-FileCopyrightText: 2022 The SV-Benchmarks Community +// +// SPDX-License-Identifier: Apache-2.0 + +// This C program is converted from Btor2 by Btor2C version bfcfb8b +// with arguments: { architecture=64, lazy_modulo=true, use_memmove=false, unroll_inner_loops=false, shortest_type=true, diff_type=true, decimal_constant=true, zero_init=false, sra_extend_sign=true } +// Comments from the original Btor2 file: +// ; source: http://fmv.jku.at/hwmcc19/beem_btor.tar.xz +// ; Model in BTOR format generated by stepout.py 0.41 +#include "klee-test-comp.c" +extern void abort(void); +void reach_error() {} + +extern unsigned char __VERIFIER_nondet_uchar(); +extern unsigned short __VERIFIER_nondet_ushort(); +extern unsigned int __VERIFIER_nondet_uint(); +extern unsigned long __VERIFIER_nondet_ulong(); +void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: { reach_error(); abort(); } } } +void assume_abort_if_not(int cond) { if (!cond) { abort(); } } +int main() { + // Defining sorts ... + typedef unsigned char SORT_1; // BV with 1 bits + const SORT_1 mask_SORT_1 = (SORT_1)-1 >> (sizeof(SORT_1) * 8 - 1); + const SORT_1 msb_SORT_1 = (SORT_1)1 << (1 - 1); + typedef unsigned char SORT_2; // BV with 5 bits + const SORT_2 mask_SORT_2 = (SORT_2)-1 >> (sizeof(SORT_2) * 8 - 5); + const SORT_2 msb_SORT_2 = (SORT_2)1 << (5 - 1); + typedef unsigned short SORT_3; // BV with 16 bits + const SORT_3 mask_SORT_3 = (SORT_3)-1 >> (sizeof(SORT_3) * 8 - 16); + const SORT_3 msb_SORT_3 = (SORT_3)1 << (16 - 1); + typedef unsigned int SORT_4; // BV with 32 bits + const SORT_4 mask_SORT_4 = (SORT_4)-1 >> (sizeof(SORT_4) * 8 - 32); + const SORT_4 msb_SORT_4 = (SORT_4)1 << (32 - 1); + // Initializing constants ... + const SORT_3 var_5 = 0; + const SORT_1 var_12 = 0; + const SORT_3 var_34 = 1; + const SORT_3 var_37 = 0; + const SORT_1 var_62 = 1; + const SORT_4 var_65 = 20; + const SORT_3 var_66 = 0; + const SORT_4 var_68 = 16; + const SORT_4 var_171 = 17; + // Collecting input declarations ... + SORT_3 input_44; + SORT_3 input_46; + SORT_3 input_48; + SORT_1 input_50; + SORT_1 input_52; + SORT_1 input_54; + SORT_1 input_56; + SORT_1 input_58; + SORT_1 input_60; + SORT_1 input_64; + SORT_1 input_74; + SORT_1 input_78; + SORT_1 input_81; + SORT_1 input_96; + SORT_1 input_100; + // Collecting state declarations ... + SORT_3 state_6 = __VERIFIER_nondet_ushort() & mask_SORT_3; + SORT_3 state_8 = __VERIFIER_nondet_ushort() & mask_SORT_3; + SORT_3 state_10 = __VERIFIER_nondet_ushort() & mask_SORT_3; + SORT_1 state_13 = __VERIFIER_nondet_uchar() & mask_SORT_1; + SORT_1 state_15 = __VERIFIER_nondet_uchar() & mask_SORT_1; + SORT_1 state_17 = __VERIFIER_nondet_uchar() & mask_SORT_1; + SORT_1 state_19 = __VERIFIER_nondet_uchar() & mask_SORT_1; + SORT_1 state_21 = __VERIFIER_nondet_uchar() & mask_SORT_1; + SORT_1 state_23 = __VERIFIER_nondet_uchar() & mask_SORT_1; + SORT_1 state_25 = __VERIFIER_nondet_uchar() & mask_SORT_1; + SORT_1 state_27 = __VERIFIER_nondet_uchar() & mask_SORT_1; + // Initializing states ... + SORT_3 init_7_arg_1 = var_5; + state_6 = init_7_arg_1; + SORT_3 init_9_arg_1 = var_5; + state_8 = init_9_arg_1; + SORT_3 init_11_arg_1 = var_5; + state_10 = init_11_arg_1; + SORT_1 init_14_arg_1 = var_12; + state_13 = init_14_arg_1; + SORT_1 init_16_arg_1 = var_12; + state_15 = init_16_arg_1; + SORT_1 init_18_arg_1 = var_12; + state_17 = init_18_arg_1; + SORT_1 init_20_arg_1 = var_12; + state_19 = init_20_arg_1; + SORT_1 init_22_arg_1 = var_12; + state_21 = init_22_arg_1; + SORT_1 init_24_arg_1 = var_12; + state_23 = init_24_arg_1; + SORT_1 init_26_arg_1 = var_12; + state_25 = init_26_arg_1; + SORT_1 init_28_arg_1 = var_12; + state_27 = init_28_arg_1; + for (;;) { + // Getting external input values ... + input_44 = __VERIFIER_nondet_ushort(); + input_44 = input_44 & mask_SORT_3; + input_46 = __VERIFIER_nondet_ushort(); + input_46 = input_46 & mask_SORT_3; + input_48 = __VERIFIER_nondet_ushort(); + input_48 = input_48 & mask_SORT_3; + input_50 = __VERIFIER_nondet_uchar(); + input_50 = input_50 & mask_SORT_1; + input_52 = __VERIFIER_nondet_uchar(); + input_52 = input_52 & mask_SORT_1; + input_54 = __VERIFIER_nondet_uchar(); + input_54 = input_54 & mask_SORT_1; + input_56 = __VERIFIER_nondet_uchar(); + input_56 = input_56 & mask_SORT_1; + input_58 = __VERIFIER_nondet_uchar(); + input_58 = input_58 & mask_SORT_1; + input_60 = __VERIFIER_nondet_uchar(); + input_60 = input_60 & mask_SORT_1; + input_64 = __VERIFIER_nondet_uchar(); + input_64 = input_64 & mask_SORT_1; + input_74 = __VERIFIER_nondet_uchar(); + input_74 = input_74 & mask_SORT_1; + input_78 = __VERIFIER_nondet_uchar(); + input_78 = input_78 & mask_SORT_1; + input_81 = __VERIFIER_nondet_uchar(); + input_81 = input_81 & mask_SORT_1; + input_96 = __VERIFIER_nondet_uchar(); + input_96 = input_96 & mask_SORT_1; + input_100 = __VERIFIER_nondet_uchar(); + input_100 = input_100 & mask_SORT_1; + // Assuming invariants ... + // Asserting properties ... + SORT_1 var_29_arg_0 = state_13; + SORT_1 var_29_arg_1 = ~state_15; + var_29_arg_1 = var_29_arg_1 & mask_SORT_1; + SORT_1 var_29 = var_29_arg_0 & var_29_arg_1; + SORT_1 var_30_arg_0 = var_29; + SORT_1 var_30_arg_1 = ~state_17; + var_30_arg_1 = var_30_arg_1 & mask_SORT_1; + SORT_1 var_30 = var_30_arg_0 & var_30_arg_1; + SORT_1 var_31_arg_0 = var_30; + SORT_1 var_31_arg_1 = state_19; + SORT_1 var_31 = var_31_arg_0 & var_31_arg_1; + SORT_1 var_32_arg_0 = var_31; + SORT_1 var_32_arg_1 = ~state_21; + var_32_arg_1 = var_32_arg_1 & mask_SORT_1; + SORT_1 var_32 = var_32_arg_0 & var_32_arg_1; + SORT_1 var_33_arg_0 = var_32; + SORT_1 var_33_arg_1 = ~state_23; + var_33_arg_1 = var_33_arg_1 & mask_SORT_1; + SORT_1 var_33 = var_33_arg_0 & var_33_arg_1; + SORT_3 var_35_arg_0 = var_34; + SORT_3 var_35_arg_1 = state_6; + SORT_1 var_35 = var_35_arg_0 == var_35_arg_1; + SORT_1 var_36_arg_0 = var_33; + SORT_1 var_36_arg_1 = var_35; + SORT_1 var_36 = var_36_arg_0 & var_36_arg_1; + SORT_3 var_38_arg_0 = var_37; + SORT_3 var_38_arg_1 = state_8; + SORT_1 var_38 = var_38_arg_0 == var_38_arg_1; + SORT_1 var_39_arg_0 = var_36; + SORT_1 var_39_arg_1 = var_38; + SORT_1 var_39 = var_39_arg_0 & var_39_arg_1; + SORT_3 var_40_arg_0 = var_37; + SORT_3 var_40_arg_1 = state_10; + SORT_1 var_40 = var_40_arg_0 == var_40_arg_1; + SORT_1 var_41_arg_0 = var_39; + SORT_1 var_41_arg_1 = var_40; + SORT_1 var_41 = var_41_arg_0 & var_41_arg_1; + SORT_1 var_42_arg_0 = state_27; + SORT_1 var_42_arg_1 = var_41; + SORT_1 var_42 = var_42_arg_0 & var_42_arg_1; + var_42 = var_42 & mask_SORT_1; + SORT_1 bad_43_arg_0 = var_42; + __VERIFIER_assert(!(bad_43_arg_0)); + // Computing next states ... + SORT_3 next_45_arg_1 = input_44; + SORT_3 next_47_arg_1 = input_46; + SORT_3 next_49_arg_1 = input_48; + SORT_1 next_51_arg_1 = input_50; + SORT_1 next_53_arg_1 = input_52; + SORT_1 next_55_arg_1 = input_54; + SORT_1 next_57_arg_1 = input_56; + SORT_1 next_59_arg_1 = input_58; + SORT_1 next_61_arg_1 = input_60; + SORT_1 next_63_arg_1 = var_62; + SORT_3 var_67_arg_0 = input_44; + SORT_3 var_67_arg_1 = var_66; + SORT_4 var_67 = ((SORT_4)var_67_arg_0 << 16) | var_67_arg_1; + SORT_4 var_69_arg_0 = var_67; + var_69_arg_0 = (var_69_arg_0 & msb_SORT_4) ? (var_69_arg_0 | ~mask_SORT_4) : (var_69_arg_0 & mask_SORT_4); + SORT_4 var_69_arg_1 = var_68; + SORT_4 var_69 = (int)var_69_arg_0 >> var_69_arg_1; + var_69 = (var_69_arg_0 & msb_SORT_4) ? (var_69 | ~(mask_SORT_4 >> var_69_arg_1)) : var_69; + var_69 = var_69 & mask_SORT_4; + SORT_4 var_70_arg_0 = var_65; + SORT_4 var_70_arg_1 = var_69; + SORT_1 var_70 = var_70_arg_0 <= var_70_arg_1; + SORT_1 var_71_arg_0 = input_50; + SORT_1 var_71_arg_1 = ~var_70; + var_71_arg_1 = var_71_arg_1 & mask_SORT_1; + SORT_1 var_71 = var_71_arg_0 & var_71_arg_1; + SORT_1 var_72_arg_0 = ~input_64; + var_72_arg_0 = var_72_arg_0 & mask_SORT_1; + SORT_1 var_72_arg_1 = var_71; + SORT_1 var_72 = var_72_arg_0 | var_72_arg_1; + SORT_1 var_73_arg_0 = input_52; + SORT_1 var_73_arg_1 = input_64; + SORT_1 var_73 = var_73_arg_0 | var_73_arg_1; + SORT_1 var_75_arg_0 = var_73; + SORT_1 var_75_arg_1 = ~input_74; + var_75_arg_1 = var_75_arg_1 & mask_SORT_1; + SORT_1 var_75 = var_75_arg_0 | var_75_arg_1; + SORT_1 var_76_arg_0 = var_72; + SORT_1 var_76_arg_1 = var_75; + SORT_1 var_76 = var_76_arg_0 & var_76_arg_1; + SORT_1 var_77_arg_0 = input_54; + SORT_1 var_77_arg_1 = input_74; + SORT_1 var_77 = var_77_arg_0 | var_77_arg_1; + SORT_1 var_79_arg_0 = var_77; + SORT_1 var_79_arg_1 = ~input_78; + var_79_arg_1 = var_79_arg_1 & mask_SORT_1; + SORT_1 var_79 = var_79_arg_0 | var_79_arg_1; + SORT_1 var_80_arg_0 = var_76; + SORT_1 var_80_arg_1 = var_79; + SORT_1 var_80 = var_80_arg_0 & var_80_arg_1; + SORT_1 var_82_arg_0 = input_64; + SORT_3 var_82_arg_1 = input_44; + SORT_3 var_82_arg_2 = input_46; + SORT_3 var_82 = var_82_arg_0 ? var_82_arg_1 : var_82_arg_2; + SORT_3 var_83_arg_0 = var_82; + SORT_3 var_83_arg_1 = var_66; + SORT_4 var_83 = ((SORT_4)var_83_arg_0 << 16) | var_83_arg_1; + SORT_4 var_84_arg_0 = var_83; + var_84_arg_0 = (var_84_arg_0 & msb_SORT_4) ? (var_84_arg_0 | ~mask_SORT_4) : (var_84_arg_0 & mask_SORT_4); + SORT_4 var_84_arg_1 = var_68; + SORT_4 var_84 = (int)var_84_arg_0 >> var_84_arg_1; + var_84 = (var_84_arg_0 & msb_SORT_4) ? (var_84 | ~(mask_SORT_4 >> var_84_arg_1)) : var_84; + SORT_4 var_85_arg_0 = var_69; + SORT_4 var_85_arg_1 = var_84; + SORT_4 var_85 = var_85_arg_0 + var_85_arg_1; + SORT_4 var_86_arg_0 = var_85; + SORT_3 var_86 = var_86_arg_0 >> 0; + SORT_1 var_87_arg_0 = input_74; + SORT_3 var_87_arg_1 = var_86; + SORT_3 var_87_arg_2 = var_82; + SORT_3 var_87 = var_87_arg_0 ? var_87_arg_1 : var_87_arg_2; + var_87 = var_87 & mask_SORT_3; + SORT_1 var_88_arg_0 = input_78; + SORT_3 var_88_arg_1 = var_87; + SORT_3 var_88_arg_2 = input_44; + SORT_3 var_88 = var_88_arg_0 ? var_88_arg_1 : var_88_arg_2; + SORT_3 var_89_arg_0 = var_88; + SORT_3 var_89_arg_1 = var_66; + SORT_4 var_89 = ((SORT_4)var_89_arg_0 << 16) | var_89_arg_1; + SORT_4 var_90_arg_0 = var_89; + var_90_arg_0 = (var_90_arg_0 & msb_SORT_4) ? (var_90_arg_0 | ~mask_SORT_4) : (var_90_arg_0 & mask_SORT_4); + SORT_4 var_90_arg_1 = var_68; + SORT_4 var_90 = (int)var_90_arg_0 >> var_90_arg_1; + var_90 = (var_90_arg_0 & msb_SORT_4) ? (var_90 | ~(mask_SORT_4 >> var_90_arg_1)) : var_90; + var_90 = var_90 & mask_SORT_4; + SORT_4 var_91_arg_0 = var_65; + SORT_4 var_91_arg_1 = var_90; + SORT_1 var_91 = var_91_arg_0 <= var_91_arg_1; + SORT_1 var_92_arg_0 = input_56; + SORT_1 var_92_arg_1 = ~var_91; + var_92_arg_1 = var_92_arg_1 & mask_SORT_1; + SORT_1 var_92 = var_92_arg_0 & var_92_arg_1; + SORT_1 var_93_arg_0 = ~input_81; + var_93_arg_0 = var_93_arg_0 & mask_SORT_1; + SORT_1 var_93_arg_1 = var_92; + SORT_1 var_93 = var_93_arg_0 | var_93_arg_1; + SORT_1 var_94_arg_0 = var_80; + SORT_1 var_94_arg_1 = var_93; + SORT_1 var_94 = var_94_arg_0 & var_94_arg_1; + SORT_1 var_95_arg_0 = input_58; + SORT_1 var_95_arg_1 = input_81; + SORT_1 var_95 = var_95_arg_0 | var_95_arg_1; + SORT_1 var_97_arg_0 = var_95; + SORT_1 var_97_arg_1 = ~input_96; + var_97_arg_1 = var_97_arg_1 & mask_SORT_1; + SORT_1 var_97 = var_97_arg_0 | var_97_arg_1; + SORT_1 var_98_arg_0 = var_94; + SORT_1 var_98_arg_1 = var_97; + SORT_1 var_98 = var_98_arg_0 & var_98_arg_1; + SORT_1 var_99_arg_0 = input_60; + SORT_1 var_99_arg_1 = input_96; + SORT_1 var_99 = var_99_arg_0 | var_99_arg_1; + SORT_1 var_101_arg_0 = var_99; + SORT_1 var_101_arg_1 = ~input_100; + var_101_arg_1 = var_101_arg_1 & mask_SORT_1; + SORT_1 var_101 = var_101_arg_0 | var_101_arg_1; + SORT_1 var_102_arg_0 = var_98; + SORT_1 var_102_arg_1 = var_101; + SORT_1 var_102 = var_102_arg_0 & var_102_arg_1; + SORT_1 var_103_arg_0 = input_64; + SORT_1 var_103_arg_1 = input_74; + SORT_1 var_103 = var_103_arg_0 | var_103_arg_1; + SORT_1 var_104_arg_0 = input_78; + SORT_1 var_104_arg_1 = var_103; + SORT_1 var_104 = var_104_arg_0 | var_104_arg_1; + SORT_1 var_105_arg_0 = input_81; + SORT_1 var_105_arg_1 = var_104; + SORT_1 var_105 = var_105_arg_0 | var_105_arg_1; + SORT_1 var_106_arg_0 = input_96; + SORT_1 var_106_arg_1 = var_105; + SORT_1 var_106 = var_106_arg_0 | var_106_arg_1; + SORT_1 var_107_arg_0 = input_100; + SORT_1 var_107_arg_1 = var_106; + SORT_1 var_107 = var_107_arg_0 | var_107_arg_1; + SORT_1 var_108_arg_0 = var_102; + SORT_1 var_108_arg_1 = var_107; + SORT_1 var_108 = var_108_arg_0 & var_108_arg_1; + SORT_1 var_109_arg_0 = input_50; + SORT_1 var_109_arg_1 = input_52; + SORT_1 var_109 = var_109_arg_0 & var_109_arg_1; + SORT_1 var_110_arg_0 = input_50; + SORT_1 var_110_arg_1 = input_52; + SORT_1 var_110 = var_110_arg_0 | var_110_arg_1; + SORT_1 var_111_arg_0 = input_54; + SORT_1 var_111_arg_1 = var_110; + SORT_1 var_111 = var_111_arg_0 & var_111_arg_1; + SORT_1 var_112_arg_0 = var_109; + SORT_1 var_112_arg_1 = var_111; + SORT_1 var_112 = var_112_arg_0 | var_112_arg_1; + SORT_1 var_113_arg_0 = input_54; + SORT_1 var_113_arg_1 = var_110; + SORT_1 var_113 = var_113_arg_0 | var_113_arg_1; + SORT_1 var_114_arg_0 = ~var_112; + var_114_arg_0 = var_114_arg_0 & mask_SORT_1; + SORT_1 var_114_arg_1 = var_113; + SORT_1 var_114 = var_114_arg_0 & var_114_arg_1; + SORT_1 var_115_arg_0 = input_56; + SORT_1 var_115_arg_1 = input_58; + SORT_1 var_115 = var_115_arg_0 & var_115_arg_1; + SORT_1 var_116_arg_0 = input_56; + SORT_1 var_116_arg_1 = input_58; + SORT_1 var_116 = var_116_arg_0 | var_116_arg_1; + SORT_1 var_117_arg_0 = input_60; + SORT_1 var_117_arg_1 = var_116; + SORT_1 var_117 = var_117_arg_0 & var_117_arg_1; + SORT_1 var_118_arg_0 = var_115; + SORT_1 var_118_arg_1 = var_117; + SORT_1 var_118 = var_118_arg_0 | var_118_arg_1; + SORT_1 var_119_arg_0 = var_114; + SORT_1 var_119_arg_1 = ~var_118; + var_119_arg_1 = var_119_arg_1 & mask_SORT_1; + SORT_1 var_119 = var_119_arg_0 & var_119_arg_1; + SORT_1 var_120_arg_0 = input_60; + SORT_1 var_120_arg_1 = var_116; + SORT_1 var_120 = var_120_arg_0 | var_120_arg_1; + SORT_1 var_121_arg_0 = var_119; + SORT_1 var_121_arg_1 = var_120; + SORT_1 var_121 = var_121_arg_0 & var_121_arg_1; + SORT_1 var_122_arg_0 = var_108; + SORT_1 var_122_arg_1 = var_121; + SORT_1 var_122 = var_122_arg_0 & var_122_arg_1; + SORT_1 var_123_arg_0 = var_73; + SORT_1 var_123_arg_1 = ~input_74; + var_123_arg_1 = var_123_arg_1 & mask_SORT_1; + SORT_1 var_123 = var_123_arg_0 & var_123_arg_1; + var_123 = var_123 & mask_SORT_1; + SORT_1 var_124_arg_0 = input_50; + SORT_1 var_124_arg_1 = ~input_64; + var_124_arg_1 = var_124_arg_1 & mask_SORT_1; + SORT_1 var_124 = var_124_arg_0 & var_124_arg_1; + SORT_1 var_125_arg_0 = var_124; + SORT_1 var_125_arg_1 = input_78; + SORT_1 var_125 = var_125_arg_0 | var_125_arg_1; + var_125 = var_125 & mask_SORT_1; + SORT_1 var_126_arg_0 = var_123; + SORT_1 var_126_arg_1 = var_125; + SORT_1 var_126 = var_126_arg_0 & var_126_arg_1; + SORT_1 var_127_arg_0 = var_77; + SORT_1 var_127_arg_1 = ~input_78; + var_127_arg_1 = var_127_arg_1 & mask_SORT_1; + SORT_1 var_127 = var_127_arg_0 & var_127_arg_1; + var_127 = var_127 & mask_SORT_1; + SORT_1 var_128_arg_0 = var_123; + SORT_1 var_128_arg_1 = var_125; + SORT_1 var_128 = var_128_arg_0 | var_128_arg_1; + SORT_1 var_129_arg_0 = var_127; + SORT_1 var_129_arg_1 = var_128; + SORT_1 var_129 = var_129_arg_0 & var_129_arg_1; + SORT_1 var_130_arg_0 = var_126; + SORT_1 var_130_arg_1 = var_129; + SORT_1 var_130 = var_130_arg_0 | var_130_arg_1; + SORT_1 var_131_arg_0 = var_127; + SORT_1 var_131_arg_1 = var_128; + SORT_1 var_131 = var_131_arg_0 | var_131_arg_1; + SORT_1 var_132_arg_0 = ~var_130; + var_132_arg_0 = var_132_arg_0 & mask_SORT_1; + SORT_1 var_132_arg_1 = var_131; + SORT_1 var_132 = var_132_arg_0 & var_132_arg_1; + SORT_1 var_133_arg_0 = var_95; + SORT_1 var_133_arg_1 = ~input_96; + var_133_arg_1 = var_133_arg_1 & mask_SORT_1; + SORT_1 var_133 = var_133_arg_0 & var_133_arg_1; + var_133 = var_133 & mask_SORT_1; + SORT_1 var_134_arg_0 = input_56; + SORT_1 var_134_arg_1 = ~input_81; + var_134_arg_1 = var_134_arg_1 & mask_SORT_1; + SORT_1 var_134 = var_134_arg_0 & var_134_arg_1; + SORT_1 var_135_arg_0 = var_134; + SORT_1 var_135_arg_1 = input_100; + SORT_1 var_135 = var_135_arg_0 | var_135_arg_1; + var_135 = var_135 & mask_SORT_1; + SORT_1 var_136_arg_0 = var_133; + SORT_1 var_136_arg_1 = var_135; + SORT_1 var_136 = var_136_arg_0 & var_136_arg_1; + SORT_1 var_137_arg_0 = var_99; + SORT_1 var_137_arg_1 = ~input_100; + var_137_arg_1 = var_137_arg_1 & mask_SORT_1; + SORT_1 var_137 = var_137_arg_0 & var_137_arg_1; + var_137 = var_137 & mask_SORT_1; + SORT_1 var_138_arg_0 = var_133; + SORT_1 var_138_arg_1 = var_135; + SORT_1 var_138 = var_138_arg_0 | var_138_arg_1; + SORT_1 var_139_arg_0 = var_137; + SORT_1 var_139_arg_1 = var_138; + SORT_1 var_139 = var_139_arg_0 & var_139_arg_1; + SORT_1 var_140_arg_0 = var_136; + SORT_1 var_140_arg_1 = var_139; + SORT_1 var_140 = var_140_arg_0 | var_140_arg_1; + SORT_1 var_141_arg_0 = var_132; + SORT_1 var_141_arg_1 = ~var_140; + var_141_arg_1 = var_141_arg_1 & mask_SORT_1; + SORT_1 var_141 = var_141_arg_0 & var_141_arg_1; + SORT_1 var_142_arg_0 = var_137; + SORT_1 var_142_arg_1 = var_138; + SORT_1 var_142 = var_142_arg_0 | var_142_arg_1; + SORT_1 var_143_arg_0 = var_141; + SORT_1 var_143_arg_1 = var_142; + SORT_1 var_143 = var_143_arg_0 & var_143_arg_1; + SORT_1 var_144_arg_0 = var_122; + SORT_1 var_144_arg_1 = var_143; + SORT_1 var_144 = var_144_arg_0 & var_144_arg_1; + SORT_1 var_145_arg_0 = input_81; + SORT_3 var_145_arg_1 = var_88; + SORT_3 var_145_arg_2 = input_48; + SORT_3 var_145 = var_145_arg_0 ? var_145_arg_1 : var_145_arg_2; + SORT_3 var_146_arg_0 = var_145; + SORT_3 var_146_arg_1 = var_66; + SORT_4 var_146 = ((SORT_4)var_146_arg_0 << 16) | var_146_arg_1; + SORT_4 var_147_arg_0 = var_146; + var_147_arg_0 = (var_147_arg_0 & msb_SORT_4) ? (var_147_arg_0 | ~mask_SORT_4) : (var_147_arg_0 & mask_SORT_4); + SORT_4 var_147_arg_1 = var_68; + SORT_4 var_147 = (int)var_147_arg_0 >> var_147_arg_1; + var_147 = (var_147_arg_0 & msb_SORT_4) ? (var_147 | ~(mask_SORT_4 >> var_147_arg_1)) : var_147; + SORT_4 var_148_arg_0 = var_90; + SORT_4 var_148_arg_1 = var_147; + SORT_4 var_148 = var_148_arg_0 + var_148_arg_1; + SORT_4 var_149_arg_0 = var_148; + SORT_3 var_149 = var_149_arg_0 >> 0; + SORT_1 var_150_arg_0 = input_96; + SORT_3 var_150_arg_1 = var_149; + SORT_3 var_150_arg_2 = var_145; + SORT_3 var_150 = var_150_arg_0 ? var_150_arg_1 : var_150_arg_2; + var_150 = var_150 & mask_SORT_3; + SORT_1 var_151_arg_0 = input_100; + SORT_3 var_151_arg_1 = var_150; + SORT_3 var_151_arg_2 = var_88; + SORT_3 var_151 = var_151_arg_0 ? var_151_arg_1 : var_151_arg_2; + var_151 = var_151 & mask_SORT_3; + SORT_3 var_152_arg_0 = var_151; + SORT_3 var_152_arg_1 = state_6; + SORT_1 var_152 = var_152_arg_0 == var_152_arg_1; + SORT_1 var_153_arg_0 = var_144; + SORT_1 var_153_arg_1 = var_152; + SORT_1 var_153 = var_153_arg_0 & var_153_arg_1; + SORT_3 var_154_arg_0 = var_87; + SORT_3 var_154_arg_1 = state_8; + SORT_1 var_154 = var_154_arg_0 == var_154_arg_1; + SORT_1 var_155_arg_0 = var_153; + SORT_1 var_155_arg_1 = var_154; + SORT_1 var_155 = var_155_arg_0 & var_155_arg_1; + SORT_3 var_156_arg_0 = var_150; + SORT_3 var_156_arg_1 = state_10; + SORT_1 var_156 = var_156_arg_0 == var_156_arg_1; + SORT_1 var_157_arg_0 = var_155; + SORT_1 var_157_arg_1 = var_156; + SORT_1 var_157 = var_157_arg_0 & var_157_arg_1; + SORT_1 var_158_arg_0 = var_125; + SORT_1 var_158_arg_1 = state_13; + SORT_1 var_158 = var_158_arg_0 == var_158_arg_1; + SORT_1 var_159_arg_0 = var_157; + SORT_1 var_159_arg_1 = var_158; + SORT_1 var_159 = var_159_arg_0 & var_159_arg_1; + SORT_1 var_160_arg_0 = var_123; + SORT_1 var_160_arg_1 = state_15; + SORT_1 var_160 = var_160_arg_0 == var_160_arg_1; + SORT_1 var_161_arg_0 = var_159; + SORT_1 var_161_arg_1 = var_160; + SORT_1 var_161 = var_161_arg_0 & var_161_arg_1; + SORT_1 var_162_arg_0 = var_127; + SORT_1 var_162_arg_1 = state_17; + SORT_1 var_162 = var_162_arg_0 == var_162_arg_1; + SORT_1 var_163_arg_0 = var_161; + SORT_1 var_163_arg_1 = var_162; + SORT_1 var_163 = var_163_arg_0 & var_163_arg_1; + SORT_1 var_164_arg_0 = var_135; + SORT_1 var_164_arg_1 = state_19; + SORT_1 var_164 = var_164_arg_0 == var_164_arg_1; + SORT_1 var_165_arg_0 = var_163; + SORT_1 var_165_arg_1 = var_164; + SORT_1 var_165 = var_165_arg_0 & var_165_arg_1; + SORT_1 var_166_arg_0 = var_133; + SORT_1 var_166_arg_1 = state_21; + SORT_1 var_166 = var_166_arg_0 == var_166_arg_1; + SORT_1 var_167_arg_0 = var_165; + SORT_1 var_167_arg_1 = var_166; + SORT_1 var_167 = var_167_arg_0 & var_167_arg_1; + SORT_1 var_168_arg_0 = var_137; + SORT_1 var_168_arg_1 = state_23; + SORT_1 var_168 = var_168_arg_0 == var_168_arg_1; + SORT_1 var_169_arg_0 = var_167; + SORT_1 var_169_arg_1 = var_168; + SORT_1 var_169 = var_169_arg_0 & var_169_arg_1; + SORT_1 var_170_arg_0 = var_169; + SORT_1 var_170_arg_1 = state_27; + SORT_1 var_170 = var_170_arg_0 & var_170_arg_1; + SORT_4 var_172_arg_0 = var_171; + SORT_4 var_172_arg_1 = var_69; + SORT_1 var_172 = var_172_arg_0 == var_172_arg_1; + SORT_1 var_173_arg_0 = state_25; + SORT_1 var_173_arg_1 = var_170; + SORT_1 var_173_arg_2 = var_172; + SORT_1 var_173 = var_173_arg_0 ? var_173_arg_1 : var_173_arg_2; + SORT_1 next_174_arg_1 = var_173; + // Assigning next states ... + state_6 = next_45_arg_1; + state_8 = next_47_arg_1; + state_10 = next_49_arg_1; + state_13 = next_51_arg_1; + state_15 = next_53_arg_1; + state_17 = next_55_arg_1; + state_19 = next_57_arg_1; + state_21 = next_59_arg_1; + state_23 = next_61_arg_1; + state_25 = next_63_arg_1; + state_27 = next_174_arg_1; + } + return 0; +} \ No newline at end of file diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index b1dee0fb34..a0f0e8fd59 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -89,6 +89,11 @@ cl::opt cl::desc("Do not generate any test files (default=false)"), cl::cat(TestCaseCat)); +cl::opt WriteKTests( + "write-ktests", cl::init(true), + cl::desc("Write .ktest files for each test case (default=true)"), + cl::cat(TestCaseCat)); + cl::opt WriteCVCs("write-cvcs", cl::desc("Write .cvc files for each test case (default=false)"), @@ -341,10 +346,30 @@ cl::opt Libcxx( "libcxx", cl::desc("Link the llvm libc++ library into the bitcode (default=false)"), cl::init(false), cl::cat(LinkCat)); + +cl::OptionCategory + TestCompCat("Options specific to Test-Comp", + "These are options specific to the Test-Comp competition."); + +cl::opt WriteXMLTests("write-xml-tests", + cl::desc("Write XML-formated tests"), + cl::init(false), cl::cat(TestCompCat)); + +cl::opt + XMLMetadataProgramFile("xml-metadata-programfile", + cl::desc("Original file name for xml metadata"), + cl::cat(TestCompCat)); + +cl::opt XMLMetadataProgramHash( + "xml-metadata-programhash", + llvm::cl::desc("Test-Comp hash sum of original file for xml metadata"), + llvm::cl::cat(TestCompCat)); + } // namespace namespace klee { extern cl::opt MaxTime; +extern cl::opt FunctionCallReproduce; class ExecutionState; } // namespace klee @@ -384,6 +409,8 @@ class KleeHandler : public InterpreterHandler { void processTestCase(const ExecutionState &state, const char *message, const char *suffix, bool isError = false); + void writeTestCaseXML(bool isError, const KTest &out, unsigned id); + std::string getOutputFilename(const std::string &filename); std::unique_ptr openOutputFile(const std::string &filename); @@ -552,7 +579,9 @@ void KleeHandler::processTestCase(const ExecutionState &state, const char *message, const char *suffix, bool isError) { unsigned id = ++m_numTotalTests; - if (!WriteNone) { + if (!WriteNone && + (FunctionCallReproduce == "" || strcmp(suffix, "assert.err") == 0 || + strcmp(suffix, "reachable.err") == 0)) { KTest ktest; ktest.numArgs = m_argc; ktest.args = m_argv; @@ -566,43 +595,66 @@ void KleeHandler::processTestCase(const ExecutionState &state, const auto start_time = time::getWallTime(); - if (success) { - if (!kTest_toFile( - &ktest, - getOutputFilename(getTestFilename("ktest", id)).c_str())) { - klee_warning("unable to write output test case, losing it"); - } else { - ++m_numGeneratedTests; + if (WriteKTests) { + + if (success) { + if (!kTest_toFile( + &ktest, + getOutputFilename(getTestFilename("ktest", id)).c_str())) { + klee_warning("unable to write output test case, losing it"); + } else { + ++m_numGeneratedTests; + } + + if (WriteStates) { + auto f = openTestFile("state", id); + m_interpreter->logState(state, id, f); + } + } + + if (message) { + auto f = openTestFile(suffix, id); + if (f) + *f << message; } - if (WriteStates) { - auto f = openTestFile("state", id); - m_interpreter->logState(state, id, f); + if (m_pathWriter) { + std::vector concreteBranches; + m_pathWriter->readStream(m_interpreter->getPathStreamID(state), + concreteBranches); + auto f = openTestFile("path", id); + if (f) { + for (const auto &branch : concreteBranches) { + *f << branch << '\n'; + } + } } } - for (unsigned i = 0; i < ktest.numObjects; i++) { - delete[] ktest.objects[i].bytes; - delete[] ktest.objects[i].pointers; + if (message || WriteKQueries) { + std::string constraints; + m_interpreter->getConstraintLog(state, constraints, Interpreter::KQUERY); + auto f = openTestFile("kquery", id); + if (f) + *f << constraints; } - delete[] ktest.objects; - if (message) { - auto f = openTestFile(suffix, id); + if (WriteCVCs) { + // FIXME: If using Z3 as the core solver the emitted file is actually + // SMT-LIBv2 not CVC which is a bit confusing + std::string constraints; + m_interpreter->getConstraintLog(state, constraints, Interpreter::STP); + auto f = openTestFile("cvc", id); if (f) - *f << message; + *f << constraints; } - if (m_pathWriter) { - std::vector concreteBranches; - m_pathWriter->readStream(m_interpreter->getPathStreamID(state), - concreteBranches); - auto f = openTestFile("path", id); - if (f) { - for (const auto &branch : concreteBranches) { - *f << branch << '\n'; - } - } + if (WriteSMT2s) { + std::string constraints; + m_interpreter->getConstraintLog(state, constraints, Interpreter::SMTLIB2); + auto f = openTestFile("smt2", id); + if (f) + *f << constraints; } if (m_symPathWriter) { @@ -617,10 +669,42 @@ void KleeHandler::processTestCase(const ExecutionState &state, } } + if (WriteKPaths) { + std::string blockPath; + m_interpreter->getBlockPath(state, blockPath); + auto f = openTestFile("kpath", id); + if (f) + *f << blockPath; + } + + if (WriteCov) { + std::map> cov; + m_interpreter->getCoveredLines(state, cov); + auto f = openTestFile("cov", id); + if (f) { + for (const auto &entry : cov) { + for (const auto &line : entry.second) { + *f << *entry.first << ':' << line << '\n'; + } + } + } + } + + if (WriteXMLTests) { + writeTestCaseXML(message != nullptr, ktest, id); + ++m_numGeneratedTests; + } + + for (unsigned i = 0; i < ktest.numObjects; i++) { + delete[] ktest.objects[i].bytes; + delete[] ktest.objects[i].pointers; + } + delete[] ktest.objects; + if (m_numGeneratedTests == MaxTests) m_interpreter->setHaltExecution(HaltExecution::MaxTests); - if (WriteTestInfo) { + if (!WriteXMLTests && WriteTestInfo) { time::Span elapsed_time(time::getWallTime() - start_time); auto f = openTestFile("info", id); if (f) @@ -628,57 +712,70 @@ void KleeHandler::processTestCase(const ExecutionState &state, } } // if (!WriteNone) - if (WriteKQueries) { - std::string constraints; - m_interpreter->getConstraintLog(state, constraints, Interpreter::KQUERY); - auto f = openTestFile("kquery", id); - if (f) - *f << constraints; - } - - if (WriteCVCs) { - // FIXME: If using Z3 as the core solver the emitted file is actually - // SMT-LIBv2 not CVC which is a bit confusing - std::string constraints; - m_interpreter->getConstraintLog(state, constraints, Interpreter::STP); - auto f = openTestFile("cvc", id); - if (f) - *f << constraints; + if (isError && OptExitOnError) { + m_interpreter->prepareForEarlyExit(); + klee_error("EXITING ON ERROR:\n%s\n", message); } +} - if (WriteSMT2s) { - std::string constraints; - m_interpreter->getConstraintLog(state, constraints, Interpreter::SMTLIB2); - auto f = openTestFile("smt2", id); - if (f) - *f << constraints; - } +void KleeHandler::writeTestCaseXML(bool isError, const KTest &assignments, + unsigned id) { - if (WriteKPaths) { - std::string blockPath; - m_interpreter->getBlockPath(state, blockPath); - auto f = openTestFile("kpath", id); - if (f) - *f << blockPath; - } + // TODO: This is super specific to test-comp and assumes that the name is the + // type information + auto file = openTestFile("xml", id); + if (!file) + return; - if (WriteCov) { - std::map> cov; - m_interpreter->getCoveredLines(state, cov); - auto f = openTestFile("cov", id); - if (f) { - for (const auto &entry : cov) { - for (const auto &line : entry.second) { - *f << *entry.first << ':' << line << '\n'; - } - } + *file << "\n"; + *file << "\n"; + *file << "\n"; + for (unsigned i = 0; i < assignments.numObjects; i++) { + auto item = assignments.objects[i]; + std::string name(item.name); + + *file << "\t"; + // Ignore the type + auto type_size_bytes = item.numBytes * 8; + llvm::APInt v(type_size_bytes, 0, false); + for (int i = item.numBytes - 1; i >= 0; i--) { + v <<= 8; + v |= item.bytes[i]; } + // print value + + // Check if this is an unsigned type + if (name.find("u") == 0) { + v.print(*file, false); + } else if (name.rfind("*") != std::string::npos) { + // Pointer types + v.print(*file, false); + } else if (name.find("float") == 0) { + llvm::APFloat(APFloatBase::IEEEhalf(), v).print(*file); + } else if (name.find("double") == 0) { + llvm::APFloat(APFloatBase::IEEEdouble(), v).print(*file); + } else if (name.rfind("_t") != std::string::npos) { + // arbitrary type, e.g. sector_t + v.print(*file, false); + } else if (name.find("_") == 0) { + // _Bool + v.print(*file, false); + } else { + // the rest must be signed + v.print(*file, true); + } + *file << "\n"; } - - if (isError && OptExitOnError) { - m_interpreter->prepareForEarlyExit(); - klee_error("EXITING ON ERROR:\n%s\n", message); - } + *file << "\n"; } // load a .path file @@ -1278,6 +1375,47 @@ static int run_klee_on_function(int pArgc, char **pArgv, char **pEnvp, } auto startTime = std::time(nullptr); + + if (WriteXMLTests) { + // Write metadata.xml + auto meta_file = handler->openOutputFile("metadata.xml"); + if (!meta_file) + klee_error("Could not write metadata.xml"); + + *meta_file + << "\n"; + *meta_file + << "\n"; + *meta_file << "\n"; + *meta_file << "\tC\n"; + *meta_file << "\t" << PACKAGE_STRING << "\n"; + + // Assume with early exit a bug finding mode and otherwise coverage + if (OptExitOnError) + *meta_file << "\tCOVER( init(main()), FQL(COVER " + "EDGES(@CALL(__VERIFIER_error))) )\n"; + else + *meta_file << "\tCOVER( init(main()), FQL(COVER " + "EDGES(@DECISIONEDGE)) )\n"; + + // Assume the input file resembles the original source file; just exchange + // extension + *meta_file << "\t" << XMLMetadataProgramFile + << ".c\n"; + *meta_file << "\t" << XMLMetadataProgramHash + << "\n"; + *meta_file << "\t" << EntryPoint << "\n"; + *meta_file << "\t" + << finalModule->getDataLayout().getPointerSizeInBits() + << "bit\n"; + std::stringstream t; + t << std::put_time(std::localtime(&startTime), "%Y-%m-%dT%H:%M:%SZ"); + *meta_file << "\t" << t.str() << "\n"; + *meta_file << "\n"; + } + { // output clock info and start time std::stringstream startInfo; startInfo << time::getClockInfo() << "Started: " @@ -1597,13 +1735,13 @@ int main(int argc, char **argv, char **envp) { module_triple.c_str(), host_triple.c_str()); // Detect architecture - std::string opt_suffix = "64"; // Fall back to 64bit + std::string bit_suffix = "64"; // Fall back to 64bit if (module_triple.find("i686") != std::string::npos || module_triple.find("i586") != std::string::npos || module_triple.find("i486") != std::string::npos || module_triple.find("i386") != std::string::npos || module_triple.find("arm") != std::string::npos) - opt_suffix = "32"; + bit_suffix = "32"; // Add additional user-selected suffix opt_suffix += "_" + RuntimeBuild.getValue(); @@ -1800,6 +1938,10 @@ int main(int argc, char **argv, char **envp) { if (UseGuidedSearch == Interpreter::GuidanceKind::ErrorGuidance) { paths = parseStaticAnalysisInput(); + } else if (FunctionCallReproduce != "") { + klee_warning("Turns on error-guided mode to cover %s function", + FunctionCallReproduce.c_str()); + UseGuidedSearch = Interpreter::GuidanceKind::ErrorGuidance; } Interpreter::InterpreterOptions IOpts(paths); From e9c51dd6526369b923b3bddd470bb41b99921a34 Mon Sep 17 00:00:00 2001 From: Sergey Morozov Date: Thu, 27 Jul 2023 16:15:56 +0300 Subject: [PATCH 2/6] [fix] float and double symbolics --- include/klee-test-comp.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/include/klee-test-comp.c b/include/klee-test-comp.c index 3abfe2df5d..ecda66ba02 100644 --- a/include/klee-test-comp.c +++ b/include/klee-test-comp.c @@ -82,7 +82,7 @@ unsigned long __VERIFIER_nondet_ulong(void) { } double __VERIFIER_nondet_double(void) { - long x; + double x; klee_make_symbolic(&x, sizeof(x), "double"); return x; } @@ -96,7 +96,7 @@ void *__VERIFIER_nondet_pointer(void) { } float __VERIFIER_nondet_float(void) { - int x; + float x; klee_make_symbolic(&x, sizeof(x), "float"); return x; } From bf03cdc3dcd495037009729ba73ce98329f4b072 Mon Sep 17 00:00:00 2001 From: Yurii Kostyukov Date: Thu, 21 Sep 2023 14:45:46 +0300 Subject: [PATCH 3/6] [fix] z3-tree with 0 size pool --- lib/Solver/CoreSolver.cpp | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index e44e8c37a1..ff6f9cf76e 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -28,7 +28,11 @@ DISABLE_WARNING_POP namespace klee { std::unique_ptr createCoreSolver(CoreSolverType cst) { - bool isTreeSolver = false; + bool isTreeSolver = cst == Z3_TREE_SOLVER; + if (!isTreeSolver && MaxSolversApproxTreeInc > 0) + klee_warning("--%s option is ignored because --%s is not z3-tree", + MaxSolversApproxTreeInc.ArgStr.str().c_str(), + CoreSolverToUse.ArgStr.str().c_str()); switch (cst) { case STP_SOLVER: #ifdef ENABLE_STP @@ -56,7 +60,6 @@ std::unique_ptr createCoreSolver(CoreSolverType cst) { case DUMMY_SOLVER: return createDummySolver(); case Z3_TREE_SOLVER: - isTreeSolver = true; case Z3_SOLVER: #ifdef ENABLE_Z3 klee_message("Using Z3 solver backend"); @@ -68,8 +71,12 @@ std::unique_ptr createCoreSolver(CoreSolverType cst) { klee_message("Using Z3 core builder"); type = KLEE_CORE; #endif - if (isTreeSolver) - return std::make_unique(type, MaxSolversApproxTreeInc); + if (isTreeSolver) { + if (MaxSolversApproxTreeInc > 0) + return std::make_unique(type, MaxSolversApproxTreeInc); + klee_warning("--%s is 0, so falling back to non tree-incremental solver", + MaxSolversApproxTreeInc.ArgStr.str().c_str()); + } return std::make_unique(type); #else klee_message("Not compiled with Z3 support"); From b96423d3bf791ea07b685137af686843afc8cffa Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Fri, 22 Sep 2023 01:13:41 +0400 Subject: [PATCH 4/6] [refactor] Use `bit_suffix` explicit --- tools/klee/main.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index a0f0e8fd59..e3e87da330 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -1301,7 +1301,7 @@ createLibCWrapper(std::vector> &userModules, } static void -linkWithUclibc(StringRef libDir, std::string opt_suffix, +linkWithUclibc(StringRef libDir, std::string bit_suffix, std::string opt_suffix, std::vector> &userModules, std::vector> &libsModules) { LLVMContext &ctx = userModules[0]->getContext(); @@ -1320,10 +1320,10 @@ linkWithUclibc(StringRef libDir, std::string opt_suffix, SmallString<128> uclibcBCA(libDir); // Hack to find out bitness of .bc file - if (opt_suffix.substr(0, 2) == "32") { - llvm::sys::path::append(uclibcBCA, KLEE_UCLIBC_BCA_32_NAME); - } else if (opt_suffix.substr(0, 2) == "64") { + if (bit_suffix == "64") { llvm::sys::path::append(uclibcBCA, KLEE_UCLIBC_BCA_64_NAME); + } else if (bit_suffix == "32") { + llvm::sys::path::append(uclibcBCA, KLEE_UCLIBC_BCA_32_NAME); } else { klee_error("Cannot determine bitness of source file from the name %s", uclibcBCA.c_str()); @@ -1744,7 +1744,7 @@ int main(int argc, char **argv, char **envp) { bit_suffix = "32"; // Add additional user-selected suffix - opt_suffix += "_" + RuntimeBuild.getValue(); + std::string opt_suffix = bit_suffix + "_" + RuntimeBuild.getValue(); if (UseGuidedSearch == Interpreter::GuidanceKind::ErrorGuidance) { SimplifyModule = false; @@ -1876,7 +1876,7 @@ int main(int argc, char **argv, char **envp) { break; } case LibcType::UcLibc: - linkWithUclibc(LibraryDir, opt_suffix, loadedUserModules, + linkWithUclibc(LibraryDir, bit_suffix, opt_suffix, loadedUserModules, loadedLibsModules); break; } From f2f66287604de168de75e765101df1c461d02fac Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 21 Sep 2023 02:48:20 +0400 Subject: [PATCH 5/6] [fix] Fix a few bugs --- lib/Core/ExecutionState.cpp | 7 ------- lib/Core/ExecutionState.h | 2 -- lib/Expr/Expr.cpp | 20 -------------------- lib/Solver/IndependentSolver.cpp | 1 - 4 files changed, 30 deletions(-) diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 492e22fb9a..f1152938e7 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -114,15 +114,8 @@ StackFrame::StackFrame(const StackFrame &s) StackFrame::~StackFrame() { delete[] locals; } -CallStackFrame::CallStackFrame(const CallStackFrame &s) - : caller(s.caller), kf(s.kf) {} - InfoStackFrame::InfoStackFrame(KFunction *kf) : kf(kf) {} -InfoStackFrame::InfoStackFrame(const InfoStackFrame &s) - : kf(s.kf), callPathNode(s.callPathNode), - minDistToUncoveredOnReturn(s.minDistToUncoveredOnReturn) {} - /***/ ExecutionState::ExecutionState() : initPC(nullptr), pc(nullptr), prevPC(nullptr), incomingBBIndex(-1), diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 69e597d278..a13b963de7 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -68,7 +68,6 @@ struct CallStackFrame { CallStackFrame(KInstIterator caller_, KFunction *kf_) : caller(caller_), kf(kf_) {} ~CallStackFrame() = default; - CallStackFrame(const CallStackFrame &s); bool equals(const CallStackFrame &other) const; @@ -105,7 +104,6 @@ struct InfoStackFrame { unsigned minDistToUncoveredOnReturn = 0; InfoStackFrame(KFunction *kf); - InfoStackFrame(const InfoStackFrame &s); ~InfoStackFrame() = default; }; diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index e34239682a..ccf6eab730 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -1635,21 +1635,6 @@ ref ConcatExpr::create(const ref &l, const ref &r) { if (ConstantExpr *rCE = dyn_cast(r)) return lCE->Concat(rCE); - if (isa(l) || isa(r)) { - if (SelectExpr *se = dyn_cast(l)) { - if (isa(se->trueExpr)) { - return SelectExpr::create(se->cond, ConcatExpr::create(se->trueExpr, r), - ConcatExpr::create(se->falseExpr, r)); - } - } - if (SelectExpr *se = dyn_cast(r)) { - if (isa(se->trueExpr)) { - return SelectExpr::create(se->cond, ConcatExpr::create(l, se->trueExpr), - ConcatExpr::create(l, se->falseExpr)); - } - } - } - // Merge contiguous Extracts if (ExtractExpr *ee_left = dyn_cast(l)) { if (ExtractExpr *ee_right = dyn_cast(r)) { @@ -1707,11 +1692,6 @@ ref ExtractExpr::create(ref expr, unsigned off, Width w) { } else if (ConstantExpr *CE = dyn_cast(expr)) { return CE->Extract(off, w); } else if (SelectExpr *se = dyn_cast(expr)) { - if (isa(se->trueExpr)) { - return SelectExpr::create(se->cond, - ExtractExpr::create(se->trueExpr, off, w), - ExtractExpr::create(se->falseExpr, off, w)); - } } else { // Extract(Concat) if (ConcatExpr *ce = dyn_cast(expr)) { diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 5d16a15a09..50e518fb59 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -218,7 +218,6 @@ bool IndependentSolver::computeInitialValues( // satisfy the query. ref arrayConstantSize = dyn_cast(retMap.evaluate(arr->size)); - arrayConstantSize->dump(); assert(arrayConstantSize && "Array of symbolic size had not receive value for size!"); SparseStorage ret(arrayConstantSize->getZExtValue()); From dd80c69f79b2f5e3c6eef8d332d7e93a206e868c Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 21 Sep 2023 18:58:00 +0400 Subject: [PATCH 6/6] [fix] Make the tests independent of default search strategies --- test/Solver/CrosscheckCoreStpZ3.c | 6 +++--- test/Solver/CrosscheckZ3AndZ3TreeInc.c | 8 ++++---- test/Solver/DummySolver.c | 2 +- test/Solver/ValidatingSolver.c | 6 +++--- 4 files changed, 11 insertions(+), 11 deletions(-) diff --git a/test/Solver/CrosscheckCoreStpZ3.c b/test/Solver/CrosscheckCoreStpZ3.c index 471f7d40e3..968cc8a795 100644 --- a/test/Solver/CrosscheckCoreStpZ3.c +++ b/test/Solver/CrosscheckCoreStpZ3.c @@ -2,9 +2,9 @@ // REQUIRES: z3 // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=stp --use-forked-solver=false --debug-crosscheck-core-solver=z3 %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --solver-backend=stp --use-forked-solver=false --debug-crosscheck-core-solver=z3 --use-guided-search=none %t1.bc 2>&1 | FileCheck %s #include "ExerciseSolver.c.inc" -// CHECK: KLEE: done: completed paths = 9 -// CHECK: KLEE: done: partially completed paths = 5 +// CHECK: KLEE: done: completed paths = 18 +// CHECK: KLEE: done: partially completed paths = 0 diff --git a/test/Solver/CrosscheckZ3AndZ3TreeInc.c b/test/Solver/CrosscheckZ3AndZ3TreeInc.c index 9c4c499a26..b29050cd4a 100644 --- a/test/Solver/CrosscheckZ3AndZ3TreeInc.c +++ b/test/Solver/CrosscheckZ3AndZ3TreeInc.c @@ -1,11 +1,11 @@ // REQUIRES: z3 // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --search=bfs --solver-backend=z3-tree --max-solvers-approx-tree-inc=4 --debug-crosscheck-core-solver=z3 --debug-z3-validate-models --debug-assignment-validating-solver --use-cex-cache=false %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --search=bfs --solver-backend=z3-tree --max-solvers-approx-tree-inc=4 --debug-crosscheck-core-solver=z3 --debug-z3-validate-models --debug-assignment-validating-solver --use-cex-cache=false --use-guided-search=none %t1.bc 2>&1 | FileCheck %s // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --search=dfs --solver-backend=z3-tree --max-solvers-approx-tree-inc=64 --debug-crosscheck-core-solver=z3 --debug-z3-validate-models --debug-assignment-validating-solver --use-cex-cache=false %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --search=dfs --solver-backend=z3-tree --max-solvers-approx-tree-inc=64 --debug-crosscheck-core-solver=z3 --debug-z3-validate-models --debug-assignment-validating-solver --use-cex-cache=false --use-guided-search=none %t1.bc 2>&1 | FileCheck %s #include "ExerciseSolver.c.inc" -// CHECK: KLEE: done: completed paths = 10 -// CHECK: KLEE: done: partially completed paths = 4 +// CHECK: KLEE: done: completed paths = 18 +// CHECK: KLEE: done: partially completed paths = 0 diff --git a/test/Solver/DummySolver.c b/test/Solver/DummySolver.c index 51c35e936f..9242396854 100644 --- a/test/Solver/DummySolver.c +++ b/test/Solver/DummySolver.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=dummy %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --search=bfs --solver-backend=dummy --use-guided-search=none %t1.bc 2>&1 | FileCheck %s #include "ExerciseSolver.c.inc" diff --git a/test/Solver/ValidatingSolver.c b/test/Solver/ValidatingSolver.c index d492ff9264..6af3496f82 100644 --- a/test/Solver/ValidatingSolver.c +++ b/test/Solver/ValidatingSolver.c @@ -1,8 +1,8 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --debug-validate-solver --debug-assignment-validating-solver %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --search=bfs --debug-validate-solver --debug-assignment-validating-solver --use-guided-search=none %t1.bc 2>&1 | FileCheck %s #include "ExerciseSolver.c.inc" -// CHECK: KLEE: done: completed paths = 9 -// CHECK: KLEE: done: partially completed paths = 5 \ No newline at end of file +// CHECK: KLEE: done: completed paths = 18 +// CHECK: KLEE: done: partially completed paths = 0 \ No newline at end of file