search

llvm / llvm-project

The LLVM Project is a collection of modular and reusable compiler and toolchain technologies.
http://llvm.org
Other
28.04k stars 11.58k forks source link

ConstraintManager.h:102: clang::ento::ConstraintManager::ProgramStatePair clang::ento::ConstraintManager::assumeDual(clang::ento::ProgramStateRef, clang::ento::DefinedSVal): Assertion `assume(State, Cond, false) && "System is over constrained."' failed. #39578

Open vlad902 opened 5 years ago

vlad902 commented 5 years ago
Bugzilla Link 40231
Version trunk
OS All
Attachments Unreduced input
CC @devincoughlin,@haoNoQ

Extended Description

On a Linux build of recent clang with Z3 4.8.4 (built using https://github.com/vlad902/kernel-uninitialized-memory-checker/blob/master/build.sh) I was able to hit the titled exception with the following reduced input:

long a() {
  int b = a();
  b++;
  while (b) {
    b > 0;
    unsigned c = b;
    c > 5;
    b += 5;
  }
}

and the following command: ~/kernel-uninitialized-memory-checker/build/bin/clang-8 -cc1 -triple x86_64-unknown-linux-gnu -analyze -analyzer-store=region -analyzer-opt-analyze-nested-blocks -analyzer-checker=core -nobuiltininc -std=gnu89 -analyzer-output=html -o /tmp/out -x c reduced.c

Note that with an (identically?) built clang on OSX I was not able to hit this exception. I'm not sure why. The full output is:

clang-8: /root/kernel-uninitialized-memory-checker/llvm/tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:102: clang::ento::ConstraintManager::ProgramStatePair clang::ento::ConstraintManager::assumeDual(clang::ento::ProgramStateRef, clang::ento::DefinedSVal): Assertion `assume(State, Cond, false) && "System is over constrained."' failed.
Stack dump:
0.  Program arguments: /root/kernel-uninitialized-memory-checker/build/bin/clang-8 -cc1 -triple x86_64-unknown-linux-gnu -analyze -analyzer-store=region -analyzer-opt-analyze-nested-blocks -analyzer-checker=core -nobuiltininc -std=gnu89 -analyzer-output=html -o /tmp/out -x c reduced.c
1.  <eof> parser at end of file
2.  While analyzing stack:
    #0 Calling a at line 2
    llvm/llvm-project#373 Calling a at line 2
    llvm/llvm-project#374 Calling a at line 2
    llvm/llvm-project#375 Calling a at line 2
    llvm/llvm-project#376 Calling a
3.  reduced.c:7:5: Error evaluating statement
4.  reduced.c:7:5: Error evaluating statement
 #&#8203;0 0x000055c3d07d4ea0 llvm::sys::PrintStackTrace(llvm::raw_ostream&) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x32f4ea0)
 #&#8203;1 0x000055c3d07d4f33 PrintStackTraceSignalHandler(void*) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x32f4f33)
 #&#8203;2 0x000055c3d07d2a13 llvm::sys::RunSignalHandlers() (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x32f2a13)
 #&#8203;3 0x000055c3d07d48b6 SignalHandler(int) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x32f48b6)
 #&#8203;4 0x00007f2ab2966dd0 __restore_rt (/lib/x86_64-linux-gnu/libpthread.so.0+0x12dd0)
 #&#8203;5 0x00007f2ab0f6d077 gsignal (/lib/x86_64-linux-gnu/libc.so.6+0x41077)
 #&#8203;6 0x00007f2ab0f4e535 abort (/lib/x86_64-linux-gnu/libc.so.6+0x22535)
 #&#8203;7 0x00007f2ab0f4e40f __tls_get_addr (/lib/x86_64-linux-gnu/libc.so.6+0x2240f)
 #&#8203;8 0x00007f2ab0f5e142 (/lib/x86_64-linux-gnu/libc.so.6+0x32142)
 #&#8203;9 0x000055c3d294bdbf clang::ento::ConstraintManager::assumeDual(llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>, clang::ento::DefinedSVal) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x546bdbf)
#&#8203;10 0x000055c3d294c0a9 clang::ento::ProgramState::assume(clang::ento::DefinedOrUnknownSVal) const (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x546c0a9)
#&#8203;11 0x000055c3d2ec57f8 clang::ento::ExprEngine::evalEagerlyAssumeBinOpBifurcation(clang::ento::ExplodedNodeSet&, clang::ento::ExplodedNodeSet&, clang::Expr const*) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x59e57f8)
#&#8203;12 0x000055c3d2ebd8d2 clang::ento::ExprEngine::Visit(clang::Stmt const*, clang::ento::ExplodedNode*, clang::ento::ExplodedNodeSet&) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x59dd8d2)
#&#8203;13 0x000055c3d2eb9852 clang::ento::ExprEngine::ProcessStmt(clang::Stmt const*, clang::ento::ExplodedNode*) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x59d9852)
#&#8203;14 0x000055c3d2eb8a18 clang::ento::ExprEngine::processCFGElement(clang::CFGElement, clang::ento::ExplodedNode*, unsigned int, clang::ento::NodeBuilderContext*) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x59d8a18)
#&#8203;15 0x000055c3d2ea3da5 clang::ento::CoreEngine::HandlePostStmt(clang::CFGBlock const*, unsigned int, clang::ento::ExplodedNode*) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x59c3da5)
#&#8203;16 0x000055c3d2ea2ab4 clang::ento::CoreEngine::dispatchWorkItem(clang::ento::ExplodedNode*, clang::ProgramPoint, clang::ento::WorkListUnit const&) (.localalias.0) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x59c2ab4)
#&#8203;17 0x000055c3d2ea2600 clang::ento::CoreEngine::ExecuteWorkList(clang::LocationContext const*, unsigned int, llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x59c2600)
#&#8203;18 0x000055c3d28baa96 clang::ento::ExprEngine::ExecuteWorkList(clang::LocationContext const*, unsigned int) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x53daa96)
#&#8203;19 0x000055c3d28bdc35 (anonymous namespace)::AnalysisConsumer::RunPathSensitiveChecks(clang::Decl*, clang::ento::ExprEngine::InliningModes, llvm::DenseSet<clang::Decl const*, llvm::DenseMapInfo<clang::Decl const*> >*) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x53ddc35)
#&#8203;20 0x000055c3d28bda70 (anonymous namespace)::AnalysisConsumer::HandleCode(clang::Decl*, unsigned int, clang::ento::ExprEngine::InliningModes, llvm::DenseSet<clang::Decl const*, llvm::DenseMapInfo<clang::Decl const*> >*) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x53dda70)
#&#8203;21 0x000055c3d28bc732 (anonymous namespace)::AnalysisConsumer::HandleDeclsCallGraph(unsigned int) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x53dc732)
#&#8203;22 0x000055c3d28bcba3 (anonymous namespace)::AnalysisConsumer::runAnalysisOnTranslationUnit(clang::ASTContext&) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x53dcba3)
#&#8203;23 0x000055c3d28bcdf6 (anonymous namespace)::AnalysisConsumer::HandleTranslationUnit(clang::ASTContext&) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x53dcdf6)
#&#8203;24 0x000055c3d301ca94 clang::ParseAST(clang::Sema&, bool, bool) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x5b3ca94)
#&#8203;25 0x000055c3d127c9d1 clang::ASTFrontendAction::ExecuteAction() (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x3d9c9d1)
#&#8203;26 0x000055c3d127c3c2 clang::FrontendAction::Execute() (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x3d9c3c2)
#&#8203;27 0x000055c3d1209676 clang::CompilerInstance::ExecuteAction(clang::FrontendAction&) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x3d29676)
#&#8203;28 0x000055c3d13d546b clang::ExecuteCompilerInvocation(clang::CompilerInstance*) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x3ef546b)
#&#8203;29 0x000055c3cf279314 cc1_main(llvm::ArrayRef<char const*>, char const*, void*) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x1d99314)
#&#8203;30 0x000055c3cf26f033 ExecuteCC1Tool(llvm::ArrayRef<char const*>, llvm::StringRef) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x1d8f033)
#&#8203;31 0x000055c3cf27009f main (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x1d9009f)
#&#8203;32 0x00007f2ab0f5009b __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2409b)
#&#8203;33 0x000055c3cf26b39a _start (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x1d8b39a)

I've attached the unreduced input for verification.

llvmbot commented 2 years ago

changed the description

haoNoQ commented 5 years ago

Hmm, i didn't notice this bug. Ugh. Sorry.

The assertion is fundamental but non-blocking (just means that we're doing redundant work when hit), and it was recently pointed out that we're not paying enough attention to it: https://reviews.llvm.org/D57062

We'll get to this eventually, hopefully.

vlad902 commented 5 years ago

assigned to @haoNoQ