commit klee for openSUSE:Factory
Script 'mail_helper' called by obssrc Hello community, here is the log from the commit of package klee for openSUSE:Factory checked in at 2021-06-01 10:34:54 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/klee (Old) and /work/SRC/openSUSE:Factory/.klee.new.1898 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Package is "klee" Tue Jun 1 10:34:54 2021 rev:27 rq:895887 version:2.2+20210510 Changes: -------- --- /work/SRC/openSUSE:Factory/klee/klee.changes 2021-03-02 14:15:54.729280512 +0100 +++ /work/SRC/openSUSE:Factory/.klee.new.1898/klee.changes 2021-06-01 10:35:14.156585675 +0200 @@ -1,0 +2,24 @@ +Fri May 28 05:52:48 UTC 2021 - Jiri Slaby <jslaby@suse.cz> + +- Update to version 2.2+20210510: + * allocate memory objects for functions + * differentiate between partial and completed paths in summary and fix paths + stats when not dumping states + * posix runtime: add malloc checks + * Fix erroneous klee-stats legend for --print-all + * Replaced the time-based delay + * Refactored maxStaticPctChecks into a sequence of conditions. + * Added a warning when forking is skipped due to MaxStatic*Pct limits being + reached + * Added -max-static-pct-check-delay to replace the hardcoded delay after + which the MaxStatic*Pct checks are performed. + * klee-replay: Fix -Wformat-truncation warning +- Switch to LLVM 12. (patches from pr#1389 + 1) + * 0001-llvm12-VectorType-getNumElements-has-been-deprecated.patch + * 0002-llvm12-Add-LLVM-12-to-lit.cfg.patch + * 0005-llvm12-Implement-llvm.-s-u-max-min-intrinsics.patch + * 0006-llvm11-Handle-llvm.roundeven-instrinsic.patch + * 0007-llvm12-Implement-llvm.abs-intrinsic.patch + * 0001-test-disable-until-it-is-fixed.patch + +------------------------------------------------------------------- Old: ---- klee-2.2+20210222.obscpio New: ---- 0001-llvm12-VectorType-getNumElements-has-been-deprecated.patch 0001-test-disable-until-it-is-fixed.patch 0002-llvm12-Add-LLVM-12-to-lit.cfg.patch 0005-llvm12-Implement-llvm.-s-u-max-min-intrinsics.patch 0006-llvm11-Handle-llvm.roundeven-instrinsic.patch 0007-llvm12-Implement-llvm.abs-intrinsic.patch klee-2.2+20210510.obscpio ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ klee.spec ++++++ --- /var/tmp/diff_new_pack.Y51KdL/_old 2021-06-01 10:35:14.752586690 +0200 +++ /var/tmp/diff_new_pack.Y51KdL/_new 2021-06-01 10:35:14.756586698 +0200 @@ -16,7 +16,7 @@ # -%define llvm_version_major 11 +%define llvm_version_major 12 %define llvm_version %{llvm_version_major} %ifarch x86_64 @@ -31,13 +31,19 @@ Summary: LLVM Execution Engine License: NCSA Group: Development/Languages/Other -Version: 2.2+20210222 +Version: 2.2+20210510 Release: 0 URL: http://klee.github.io/ Source0: %{name}-%{version}.tar.xz Source1: %{name}-rpmlintrc Source2: https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-%{llvm_version_major}.0.0/llvm/utils/not/not.cpp Source3: https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-%{llvm_version_major}.0.0/llvm/utils/FileCheck/FileCheck.cpp +Patch0: 0001-llvm12-VectorType-getNumElements-has-been-deprecated.patch +Patch1: 0002-llvm12-Add-LLVM-12-to-lit.cfg.patch +Patch2: 0005-llvm12-Implement-llvm.-s-u-max-min-intrinsics.patch +Patch3: 0006-llvm11-Handle-llvm.roundeven-instrinsic.patch +Patch4: 0007-llvm12-Implement-llvm.abs-intrinsic.patch +Patch5: 0001-test-disable-until-it-is-fixed.patch BuildRequires: clang%{llvm_version} BuildRequires: cmake BuildRequires: gperftools-devel ++++++ 0001-llvm12-VectorType-getNumElements-has-been-deprecated.patch ++++++ From: Lukas Zaoral <lzaoral@redhat.com> Date: Thu, 4 Mar 2021 15:02:57 +0100 Subject: llvm12: VectorType::getNumElements() has been deprecated Git-repo: https://github.com/lzaoral/klee.git Git-commit: 74ea9e5e63c5933ca2d5d7f846858c4de6e86b81 Patch-mainline: pr#1389 References: LLVM 12 ... and has already been removed from the LLVM 13 source tree. See: https://reviews.llvm.org/D78127 https://reviews.llvm.org/D95570 Signed-off-by: Jiri Slaby <jslaby@suse.cz> --- lib/Core/Executor.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index a81c4882..aaa56a55 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3137,7 +3137,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { return; } uint64_t iIdx = cIdx->getZExtValue(); +#if LLVM_VERSION_MAJOR >= 11 + const auto *vt = cast<llvm::FixedVectorType>(iei->getType()); +#else const llvm::VectorType *vt = iei->getType(); +#endif unsigned EltBits = getWidthForLLVMType(vt->getElementType()); if (iIdx >= vt->getNumElements()) { @@ -3175,7 +3179,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { return; } uint64_t iIdx = cIdx->getZExtValue(); +#if LLVM_VERSION_MAJOR >= 11 + const auto *vt = cast<llvm::FixedVectorType>(eei->getVectorOperandType()); +#else const llvm::VectorType *vt = eei->getVectorOperandType(); +#endif unsigned EltBits = getWidthForLLVMType(vt->getElementType()); if (iIdx >= vt->getNumElements()) { -- 2.26.2 ++++++ 0001-test-disable-until-it-is-fixed.patch ++++++ From: Jiri Slaby <jslaby@suse.cz> Date: Thu, 20 May 2021 12:16:09 +0200 Subject: test: disable until it is fixed Patch-mainline: no References: LLVM 12 Signed-off-by: Jiri Slaby <jslaby@suse.cz> --- .../Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c | 1 + 1 file changed, 1 insertion(+) diff --git a/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c b/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c index 95b94e41..c274b214 100644 --- a/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c +++ b/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c @@ -1,3 +1,4 @@ +// REQUIRES: lt-llvm-12.0 // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --exit-on-error --optimize --libc=uclibc %t1.bc -- 2.26.2 ++++++ 0002-llvm12-Add-LLVM-12-to-lit.cfg.patch ++++++ From: Lukas Zaoral <lzaoral@redhat.com> Date: Thu, 4 Mar 2021 15:12:03 +0100 Subject: llvm12: Add LLVM 12 to lit.cfg Git-repo: https://github.com/lzaoral/klee.git Git-commit: af84c2c765dd748083dada51f9182d7648eb974b Patch-mainline: pr#1389 References: LLVM 12 Signed-off-by: Jiri Slaby <jslaby@suse.cz> --- test/lit.cfg | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/test/lit.cfg b/test/lit.cfg index a195a1dc..c79c44a5 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -157,7 +157,8 @@ config.substitutions.append( # Add feature for the LLVM version in use, so it can be tested in REQUIRES and # XFAIL checks. We also add "not-XXX" variants, for the same reason. -known_llvm_versions = set(["3.8", "3.9", "4.0", "5.0", "6.0", "7.0", "7.1", "8.0", "9.0", "10.0", "11.0", "11.1"]) +known_llvm_versions = { "3.8", "3.9", "4.0", "5.0", "6.0", "7.0", "7.1", "8.0", + "9.0", "10.0", "11.0", "11.1", "12.0" } current_llvm_version_tuple = (int(config.llvm_version_major), int(config.llvm_version_minor)) current_llvm_version = "%s.%s" % current_llvm_version_tuple -- 2.26.2 ++++++ 0005-llvm12-Implement-llvm.-s-u-max-min-intrinsics.patch ++++++ From: Lukas Zaoral <lzaoral@redhat.com> Date: Thu, 27 May 2021 21:20:58 +0200 Subject: llvm12: Implement llvm.{s,u}{max,min} intrinsics Git-repo: https://github.com/lzaoral/klee.git Git-commit: a34fb8961649bf3a065ec8f0eb4bc58715fd1d57 Patch-mainline: pr#1389 References: LLVM 12 The vector variants are not implemented at the moment. See: https://reviews.llvm.org/D84125 Signed-off-by: Jiri Slaby <jslaby@suse.cz> --- lib/Module/IntrinsicCleaner.cpp | 35 ++++++++++++++++++++ test/Intrinsics/MinMax.ll | 57 +++++++++++++++++++++++++++++++++ 2 files changed, 92 insertions(+) create mode 100644 test/Intrinsics/MinMax.ll diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp index eaec7722..a4bb4ee8 100644 --- a/lib/Module/IntrinsicCleaner.cpp +++ b/lib/Module/IntrinsicCleaner.cpp @@ -345,6 +345,41 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { } #endif +#if LLVM_VERSION_CODE >= LLVM_VERSION(12, 0) + case Intrinsic::smax: + case Intrinsic::smin: + case Intrinsic::umax: + case Intrinsic::umin: { + IRBuilder<> builder(ii); + assert(ii->getNumArgOperands() == 2 && "wrong number of arguments"); + + Value *op1 = ii->getArgOperand(0); + Value *op2 = ii->getArgOperand(1); + + assert(op1->getType() == op2->getType() && "operand type mismatch"); + + // TODO: vectors + assert(!isa<VectorType>(op1->getType()) && + "llvm.{s,u}{max,min} with vectors is not supported"); + + Value *condition = nullptr; + if (ii->getIntrinsicID() == Intrinsic::smax) + condition = builder.CreateICmpSGT(op1, op2); + else if (ii->getIntrinsicID() == Intrinsic::smin) + condition = builder.CreateICmpSLT(op1, op2); + else if (ii->getIntrinsicID() == Intrinsic::umax) + condition = builder.CreateICmpUGT(op1, op2); + else // (ii->getIntrinsicID() == Intrinsic::umin) + condition = builder.CreateICmpULT(op1, op2); + + Value *result = builder.CreateSelect(condition, op1, op2); + ii->replaceAllUsesWith(result); + ii->eraseFromParent(); + dirty = true; + break; + } +#endif + // The following intrinsics are currently handled by LowerIntrinsicCall // (Invoking LowerIntrinsicCall with any intrinsics not on this // list throws an exception.) diff --git a/test/Intrinsics/MinMax.ll b/test/Intrinsics/MinMax.ll new file mode 100644 index 00000000..429fb1f2 --- /dev/null +++ b/test/Intrinsics/MinMax.ll @@ -0,0 +1,57 @@ +; REQUIRES: geq-llvm-12.0 +; RUN: %llvmas %s -o=%t.bc +; RUN: rm -rf %t.klee-out +; RUN: %klee -exit-on-error --output-dir=%t.klee-out --optimize=false %t.bc | \ +; RUN: FileCheck %s +; ModuleID = 'MinMax.ll' +source_filename = "MinMax.c" +target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128" +target triple = "x86_64-unknown-linux-gnu" + +@0 = private unnamed_addr constant [4 x i8] c"%d\0A\00", align 1 +@1 = private unnamed_addr constant [4 x i8] c"%u\0A\00", align 1 + +; Function Attrs: nofree nounwind uwtable +define dso_local i32 @main() local_unnamed_addr #0 { + ; smax + %1 = call i32 @llvm.smax.i32(i32 -10, i32 10) + %2 = call i32 (i8*, ...) @printf(i8* nonnull dereferenceable(1) getelementptr inbounds ([4 x i8], [4 x i8]* @0, i64 0, i64 0), i32 %1) + ; CHECK: 10 + ; smin + %3 = call i32 @llvm.smin.i32(i32 -10, i32 %2) + %4 = call i32 (i8*, ...) @printf(i8* nonnull dereferenceable(1) getelementptr inbounds ([4 x i8], [4 x i8]* @0, i64 0, i64 0), i32 %3) + ; CHECK: -10 + ; smin + %5 = call i32 @llvm.umax.i32(i32 %2, i32 20) + %6 = call i32 (i8*, ...) @printf(i8* nonnull dereferenceable(1) getelementptr inbounds ([4 x i8], [4 x i8]* @1, i64 0, i64 0), i32 %5) + ; CHECK: 20 + ; smin + %7 = call i32 @llvm.umin.i32(i32 10, i32 %5) + %8 = call i32 (i8*, ...) @printf(i8* nonnull dereferenceable(1) getelementptr inbounds ([4 x i8], [4 x i8]* @1, i64 0, i64 0), i32 %7) + ; CHECK: 10 + ret i32 0 +} + +; Function Attrs: nofree nounwind +declare dso_local noundef i32 @printf(i8* nocapture noundef readonly, ...) local_unnamed_addr #1 + +; Function Attrs: nofree nosync nounwind readnone speculatable willreturn +declare i32 @llvm.smax.i32(i32, i32) #2 + +; Function Attrs: nofree nosync nounwind readnone speculatable willreturn +declare i32 @llvm.smin.i32(i32, i32) #2 + +; Function Attrs: nofree nosync nounwind readnone speculatable willreturn +declare i32 @llvm.umax.i32(i32, i32) #2 + +; Function Attrs: nofree nosync nounwind readnone speculatable willreturn +declare i32 @llvm.umin.i32(i32, i32) #2 + +attributes #0 = { nofree nounwind uwtable "disable-tail-calls"="false" "frame-pointer"="none" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" "unsafe-fp-math"="false" "use-soft-float"="false" } +attributes #1 = { nofree nounwind "disable-tail-calls"="false" "frame-pointer"="none" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" "unsafe-fp-math"="false" "use-soft-float"="false" } +attributes #2 = { nofree nosync nounwind readnone speculatable willreturn } + +!0 = !{!1, !1, i64 0} +!1 = !{!"int", !2, i64 0} +!2 = !{!"omnipotent char", !3, i64 0} +!3 = !{!"Simple C/C++ TBAA"} -- 2.26.2 ++++++ 0006-llvm11-Handle-llvm.roundeven-instrinsic.patch ++++++ From: Lukas Zaoral <lzaoral@redhat.com> Date: Thu, 27 May 2021 21:25:00 +0200 Subject: llvm11: Handle llvm.roundeven instrinsic Git-repo: https://github.com/lzaoral/klee.git Git-commit: 2b29d86a39421ac76421b888b96613173bc18851 Patch-mainline: pr#1389 References: LLVM 12 See: https://reviews.llvm.org/D75670 Signed-off-by: Jiri Slaby <jslaby@suse.cz> --- lib/Module/IntrinsicCleaner.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp index a4bb4ee8..0851d8b5 100644 --- a/lib/Module/IntrinsicCleaner.cpp +++ b/lib/Module/IntrinsicCleaner.cpp @@ -427,6 +427,9 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { case Intrinsic::readcyclecounter: case Intrinsic::returnaddress: case Intrinsic::round: +#if LLVM_VERSION_CODE >= LLVM_VERSION(11, 0) + case Intrinsic::roundeven: +#endif case Intrinsic::sin: case Intrinsic::sqrt: case Intrinsic::stackrestore: -- 2.26.2 ++++++ 0007-llvm12-Implement-llvm.abs-intrinsic.patch ++++++ From: Lukas Zaoral <lzaoral@redhat.com> Date: Thu, 27 May 2021 21:48:02 +0200 Subject: llvm12: Implement llvm.abs intrinsic Git-repo: https://github.com/lzaoral/klee.git Git-commit: c0b10c6f7a00d81cfce24115168dd06888685f87 Patch-mainline: pr#1389 References: LLVM 12 The vector and poisonous variants are not implemented at the moment. See: https://reviews.llvm.org/D84125 Signed-off-by: Jiri Slaby <jslaby@suse.cz> --- lib/Module/IntrinsicCleaner.cpp | 41 ++++++++++++ test/Intrinsics/abs-no-overflow.ll | 102 +++++++++++++++++++++++++++++ 2 files changed, 143 insertions(+) create mode 100644 test/Intrinsics/abs-no-overflow.ll diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp index 0851d8b5..d8fab623 100644 --- a/lib/Module/IntrinsicCleaner.cpp +++ b/lib/Module/IntrinsicCleaner.cpp @@ -346,6 +346,47 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { #endif #if LLVM_VERSION_CODE >= LLVM_VERSION(12, 0) + case Intrinsic::abs: { + assert(ii->getNumArgOperands() == 2 && "wrong number of arguments"); + + Value *op = ii->getArgOperand(0); + ConstantInt *isIntMinPoison = + dyn_cast_or_null<ConstantInt>(ii->getArgOperand(1)); + + assert(isIntMinPoison && + "Failed to get second argument or it is not ConstantInt"); + assert(isIntMinPoison->getBitWidth() == 1 && + "Second argument is not an i1"); + + // TODO: vectors + unsigned bw = op->getType()->getPrimitiveSizeInBits(); + assert(!isa<VectorType>(op->getType()) && + "llvm.abs with vectors is not supported"); + + // TODO: support isIntMinPoison + // if (isIntMinPoison->isOne()) + + ConstantInt *zero = ConstantInt::get(ctx, APInt(bw, 0)); + ConstantInt *mone = ConstantInt::get(ctx, APInt(bw, -1)); + ConstantInt *smin = ConstantInt::get(ctx, APInt::getSignedMinValue(bw)); + + IRBuilder<> builder(ii); + + // conditions to flip the sign -- INT_MIN < op < 0 + Value *negative = builder.CreateICmpSLT(op, zero); + Value *notsmin = builder.CreateICmpNE(op, smin); + Value *condition = builder.CreateAnd(negative, notsmin); + + // flip and select the result + Value *flipped = builder.CreateMul(op, mone); + Value *result = builder.CreateSelect(condition, flipped, op); + + ii->replaceAllUsesWith(result); + ii->eraseFromParent(); + dirty = true; + break; + } + case Intrinsic::smax: case Intrinsic::smin: case Intrinsic::umax: diff --git a/test/Intrinsics/abs-no-overflow.ll b/test/Intrinsics/abs-no-overflow.ll new file mode 100644 index 00000000..fad95412 --- /dev/null +++ b/test/Intrinsics/abs-no-overflow.ll @@ -0,0 +1,102 @@ +; LLVM has an intrinsic for abs. +; This file is based on the following code with the modification to +; poisoning of llvm.abs. +; ``` +; #include "klee/klee.h" +; +; #include <assert.h> +; #include <limits.h> +; +; volatile int abs_a; +; +; int main(void) +; { +; int a; +; klee_make_symbolic(&a, sizeof(a), "a"); +; +; abs_a = a < 0 ? -a : a; +; if (abs_a == INT_MIN) +; assert(abs_a == a); +; else +; assert(abs_a >= 0); +; return abs_a; +; } +; ``` +; REQUIRES: geq-llvm-12.0 +; RUN: %llvmas %s -o=%t.bc +; RUN: rm -rf %t.klee-out +; RUN: %klee -exit-on-error --output-dir=%t.klee-out --optimize=false %t.bc +; ModuleID = 'abs-no-overflow.ll' +source_filename = "abs-no-overflow.c" +target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128" +target triple = "x86_64-unknown-linux-gnu" + +@0 = private unnamed_addr constant [2 x i8] c"a\00", align 1 +@abs_a = dso_local global i32 0, align 4 +@1 = private unnamed_addr constant [11 x i8] c"abs_a == a\00", align 1 +@2 = private unnamed_addr constant [7 x i8] c"test.c\00", align 1 +@3 = private unnamed_addr constant [15 x i8] c"int main(void)\00", align 1 +@4 = private unnamed_addr constant [11 x i8] c"abs_a >= 0\00", align 1 + +; Function Attrs: nounwind uwtable +define dso_local i32 @main() local_unnamed_addr #0 { + %1 = alloca i32, align 4 + %2 = bitcast i32* %1 to i8* + call void @llvm.lifetime.start.p0i8(i64 4, i8* nonnull %2) #5 + call void @klee_make_symbolic(i8* nonnull %2, i64 4, i8* getelementptr inbounds ([2 x i8], [2 x i8]* @0, i64 0, i64 0)) #5 + %3 = load i32, i32* %1, align 4, !tbaa !0 + %4 = call i32 @llvm.abs.i32(i32 %3, i1 false) + store volatile i32 %4, i32* @abs_a, align 4, !tbaa !0 + %5 = load volatile i32, i32* @abs_a, align 4, !tbaa !0 + %6 = icmp eq i32 %5, -2147483648 + %7 = load volatile i32, i32* @abs_a, align 4, !tbaa !0 + br i1 %6, label %8, label %11 + +8: ; preds = %0 + %9 = icmp eq i32 %7, %3 + br i1 %9, label %14, label %10 + +10: ; preds = %8 + call void @__assert_fail(i8* getelementptr inbounds ([11 x i8], [11 x i8]* @1, i64 0, i64 0), i8* getelementptr inbounds ([7 x i8], [7 x i8]* @2, i64 0, i64 0), i32 15, i8* getelementptr inbounds ([15 x i8], [15 x i8]* @3, i64 0, i64 0)) #6 + unreachable + +11: ; preds = %0 + %12 = icmp sgt i32 %7, -1 + br i1 %12, label %14, label %13 + +13: ; preds = %11 + call void @__assert_fail(i8* getelementptr inbounds ([11 x i8], [11 x i8]* @4, i64 0, i64 0), i8* getelementptr inbounds ([7 x i8], [7 x i8]* @2, i64 0, i64 0), i32 17, i8* getelementptr inbounds ([15 x i8], [15 x i8]* @3, i64 0, i64 0)) #6 + unreachable + +14: ; preds = %11, %8 + %15 = load volatile i32, i32* @abs_a, align 4, !tbaa !0 + call void @llvm.lifetime.end.p0i8(i64 4, i8* nonnull %2) #5 + ret i32 %15 +} + +; Function Attrs: argmemonly nofree nosync nounwind willreturn +declare void @llvm.lifetime.start.p0i8(i64 immarg, i8* nocapture) #1 + +declare dso_local void @klee_make_symbolic(i8*, i64, i8*) local_unnamed_addr #2 + +; Function Attrs: noreturn nounwind +declare dso_local void @__assert_fail(i8*, i8*, i32, i8*) local_unnamed_addr #3 + +; Function Attrs: argmemonly nofree nosync nounwind willreturn +declare void @llvm.lifetime.end.p0i8(i64 immarg, i8* nocapture) #1 + +; Function Attrs: nofree nosync nounwind readnone speculatable willreturn +declare i32 @llvm.abs.i32(i32, i1 immarg) #4 + +attributes #0 = { nounwind uwtable "disable-tail-calls"="false" "frame-pointer"="none" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" "unsafe-fp-math"="false" "use-soft-float"="false" } +attributes #1 = { argmemonly nofree nosync nounwind willreturn } +attributes #2 = { "disable-tail-calls"="false" "frame-pointer"="none" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" "unsafe-fp-math"="false" "use-soft-float"="false" } +attributes #3 = { noreturn nounwind "disable-tail-calls"="false" "frame-pointer"="none" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" "unsafe-fp-math"="false" "use-soft-float"="false" } +attributes #4 = { nofree nosync nounwind readnone speculatable willreturn } +attributes #5 = { nounwind } +attributes #6 = { noreturn nounwind } + +!0 = !{!1, !1, i64 0} +!1 = !{!"int", !2, i64 0} +!2 = !{!"omnipotent char", !3, i64 0} +!3 = !{!"Simple C/C++ TBAA"} -- 2.26.2 ++++++ FileCheck.cpp ++++++ --- /var/tmp/diff_new_pack.Y51KdL/_old 2021-06-01 10:35:14.832586827 +0200 +++ /var/tmp/diff_new_pack.Y51KdL/_new 2021-06-01 10:35:14.832586827 +0200 @@ -15,12 +15,12 @@ // //===----------------------------------------------------------------------===// +#include "llvm/FileCheck/FileCheck.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/InitLLVM.h" #include "llvm/Support/Process.h" #include "llvm/Support/WithColor.h" #include "llvm/Support/raw_ostream.h" -#include "llvm/Support/FileCheck.h" #include <cmath> using namespace llvm; @@ -77,6 +77,10 @@ cl::desc("Allow the input file to be empty. This is useful when making\n" "checks that some error message does not occur, for example.")); +static cl::opt<bool> AllowUnusedPrefixes( + "allow-unused-prefixes", cl::init(true), + cl::desc("Allow prefixes to be specified but not appear in the test.")); + static cl::opt<bool> MatchFullLines( "match-full-lines", cl::init(false), cl::desc("Require all positive matches to cover an entire input line.\n" @@ -324,7 +328,7 @@ }; /// Get an abbreviation for the check type. -std::string GetCheckTypeAbbreviation(Check::FileCheckType Ty) { +static std::string GetCheckTypeAbbreviation(Check::FileCheckType Ty) { switch (Ty) { case Check::CheckPlain: if (Ty.getCount() > 1) @@ -402,6 +406,18 @@ LabelWidth = std::max((std::string::size_type)LabelWidth, A.Label.size()); A.Marker = GetMarker(DiagItr->MatchTy); + if (!DiagItr->Note.empty()) { + A.Marker.Note = DiagItr->Note; + // It's less confusing if notes that don't actually have ranges don't have + // markers. For example, a marker for 'with "VAR" equal to "5"' would + // seem to indicate where "VAR" matches, but the location we actually have + // for the marker simply points to the start of the match/search range for + // the full pattern of which the substitution is potentially just one + // component. + if (DiagItr->InputStartLine == DiagItr->InputEndLine && + DiagItr->InputStartCol == DiagItr->InputEndCol) + A.Marker.Lead = ' '; + } A.FoundAndExpectedMatch = DiagItr->MatchTy == FileCheckDiag::MatchFoundAndExpected; @@ -503,54 +519,54 @@ OS << "Input was:\n<<<<<<\n"; // Sort annotations. - std::sort(Annotations.begin(), Annotations.end(), - [](const InputAnnotation &A, const InputAnnotation &B) { - // 1. Sort annotations in the order of the input lines. - // - // This makes it easier to find relevant annotations while - // iterating input lines in the implementation below. FileCheck - // does not always produce diagnostics in the order of input - // lines due to, for example, CHECK-DAG and CHECK-NOT. - if (A.InputLine != B.InputLine) - return A.InputLine < B.InputLine; - // 2. Sort annotations in the temporal order FileCheck produced - // their associated diagnostics. - // - // This sort offers several benefits: - // - // A. On a single input line, the order of annotations reflects - // the FileCheck logic for processing directives/patterns. - // This can be helpful in understanding cases in which the - // order of the associated directives/patterns in the check - // file or on the command line either (i) does not match the - // temporal order in which FileCheck looks for matches for the - // directives/patterns (due to, for example, CHECK-LABEL, - // CHECK-NOT, or `--implicit-check-not`) or (ii) does match - // that order but does not match the order of those - // diagnostics along an input line (due to, for example, - // CHECK-DAG). - // - // On the other hand, because our presentation format presents - // input lines in order, there's no clear way to offer the - // same benefit across input lines. For consistency, it might - // then seem worthwhile to have annotations on a single line - // also sorted in input order (that is, by input column). - // However, in practice, this appears to be more confusing - // than helpful. Perhaps it's intuitive to expect annotations - // to be listed in the temporal order in which they were - // produced except in cases the presentation format obviously - // and inherently cannot support it (that is, across input - // lines). - // - // B. When diagnostics' annotations are split among multiple - // input lines, the user must track them from one input line - // to the next. One property of the sort chosen here is that - // it facilitates the user in this regard by ensuring the - // following: when comparing any two input lines, a - // diagnostic's annotations are sorted in the same position - // relative to all other diagnostics' annotations. - return A.DiagIndex < B.DiagIndex; - }); + llvm::sort(Annotations, + [](const InputAnnotation &A, const InputAnnotation &B) { + // 1. Sort annotations in the order of the input lines. + // + // This makes it easier to find relevant annotations while + // iterating input lines in the implementation below. FileCheck + // does not always produce diagnostics in the order of input + // lines due to, for example, CHECK-DAG and CHECK-NOT. + if (A.InputLine != B.InputLine) + return A.InputLine < B.InputLine; + // 2. Sort annotations in the temporal order FileCheck produced + // their associated diagnostics. + // + // This sort offers several benefits: + // + // A. On a single input line, the order of annotations reflects + // the FileCheck logic for processing directives/patterns. + // This can be helpful in understanding cases in which the + // order of the associated directives/patterns in the check + // file or on the command line either (i) does not match the + // temporal order in which FileCheck looks for matches for the + // directives/patterns (due to, for example, CHECK-LABEL, + // CHECK-NOT, or `--implicit-check-not`) or (ii) does match + // that order but does not match the order of those + // diagnostics along an input line (due to, for example, + // CHECK-DAG). + // + // On the other hand, because our presentation format presents + // input lines in order, there's no clear way to offer the + // same benefit across input lines. For consistency, it might + // then seem worthwhile to have annotations on a single line + // also sorted in input order (that is, by input column). + // However, in practice, this appears to be more confusing + // than helpful. Perhaps it's intuitive to expect annotations + // to be listed in the temporal order in which they were + // produced except in cases the presentation format obviously + // and inherently cannot support it (that is, across input + // lines). + // + // B. When diagnostics' annotations are split among multiple + // input lines, the user must track them from one input line + // to the next. One property of the sort chosen here is that + // it facilitates the user in this regard by ensuring the + // following: when comparing any two input lines, a + // diagnostic's annotations are sorted in the same position + // relative to all other diagnostics' annotations. + return A.DiagIndex < B.DiagIndex; + }); // Compute the width of the label column. const unsigned char *InputFilePtr = InputFileText.bytes_begin(), @@ -759,6 +775,7 @@ return 2; Req.AllowEmptyInput = AllowEmptyInput; + Req.AllowUnusedPrefixes = AllowUnusedPrefixes; Req.EnableVarScope = EnableVarScope; Req.AllowDeprecatedDagOverlap = AllowDeprecatedDagOverlap; Req.Verbose = Verbose; ++++++ _servicedata ++++++ --- /var/tmp/diff_new_pack.Y51KdL/_old 2021-06-01 10:35:14.868586887 +0200 +++ /var/tmp/diff_new_pack.Y51KdL/_new 2021-06-01 10:35:14.868586887 +0200 @@ -1,4 +1,4 @@ <servicedata> <service name="tar_scm"> <param name="url">git://github.com/klee/klee.git</param> - <param name="changesrevision">148a68df793fca84a36fefd8824ea54fdf6583f4</param></service></servicedata> \ No newline at end of file + <param name="changesrevision">24badb5bf17ff586dc3f1856901f27210713b2ac</param></service></servicedata> \ No newline at end of file ++++++ klee-2.2+20210222.obscpio -> klee-2.2+20210510.obscpio ++++++ /work/SRC/openSUSE:Factory/klee/klee-2.2+20210222.obscpio /work/SRC/openSUSE:Factory/.klee.new.1898/klee-2.2+20210510.obscpio differ: char 49, line 1 ++++++ klee.obsinfo ++++++ --- /var/tmp/diff_new_pack.Y51KdL/_old 2021-06-01 10:35:14.928586990 +0200 +++ /var/tmp/diff_new_pack.Y51KdL/_new 2021-06-01 10:35:14.928586990 +0200 @@ -1,5 +1,5 @@ name: klee -version: 2.2+20210222 -mtime: 1614010572 -commit: 148a68df793fca84a36fefd8824ea54fdf6583f4 +version: 2.2+20210510 +mtime: 1620665314 +commit: 24badb5bf17ff586dc3f1856901f27210713b2ac ++++++ not.cpp ++++++ --- /var/tmp/diff_new_pack.Y51KdL/_old 2021-06-01 10:35:14.944587017 +0200 +++ /var/tmp/diff_new_pack.Y51KdL/_new 2021-06-01 10:35:14.948587024 +0200 @@ -15,6 +15,10 @@ #include "llvm/Support/WithColor.h" #include "llvm/Support/raw_ostream.h" +#ifdef _WIN32 +#include <windows.h> +#endif + using namespace llvm; int main(int argc, const char **argv) { @@ -27,6 +31,16 @@ ++argv; --argc; ExpectCrash = true; + + // Crash is expected, so disable crash report and symbolization to reduce + // output and avoid potentially slow symbolization. +#ifdef _WIN32 + SetEnvironmentVariableA("LLVM_DISABLE_CRASH_REPORT", "1"); + SetEnvironmentVariableA("LLVM_DISABLE_SYMBOLIZATION", "1"); +#else + setenv("LLVM_DISABLE_CRASH_REPORT", "1", 0); + setenv("LLVM_DISABLE_SYMBOLIZATION", "1", 0); +#endif } if (argc == 0)
participants (1)
-
Source-Sync