diff options
Diffstat (limited to 'include/clang/StaticAnalyzer/Core/PathSensitive')
43 files changed, 327 insertions, 881 deletions
diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h b/include/clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h index 243795e720..4b7d6054cd 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h @@ -1,9 +1,8 @@ //== APSIntType.h - Simple record of the type of APSInts --------*- C++ -*--==// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h index 50b9b566ed..b0dda78a00 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h @@ -1,9 +1,8 @@ //== AnalysisManager.h - Path sensitive analysis data manager ------*- C++ -*-// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h b/include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h index 1c5d4eb2de..ac218bc070 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h @@ -1,9 +1,8 @@ //==- BasicValueFactory.h - Basic values for Path Sens analysis --*- C++ -*-==// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/BlockCounter.h b/include/clang/StaticAnalyzer/Core/PathSensitive/BlockCounter.h index 5e831095ab..46ff69e0c3 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/BlockCounter.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/BlockCounter.h @@ -1,9 +1,8 @@ //==- BlockCounter.h - ADT for counting block visits ---------------*- C++ -*-// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h b/include/clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h index 81dd83fc10..19996cf9a1 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h @@ -1,9 +1,8 @@ //===- CallEvent.h - Wrapper for all function and method calls --*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h b/include/clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h index 6ee75b7384..6a49aebc14 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h @@ -1,9 +1,8 @@ //== CheckerContext.h - Context info for path-sensitive checkers--*- C++ -*--=// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // @@ -220,6 +219,24 @@ public: Eng.getBugReporter().emitReport(std::move(R)); } + + /// Produce a program point tag that displays an additional path note + /// to the user. This is a lightweight alternative to the + /// BugReporterVisitor mechanism: instead of visiting the bug report + /// node-by-node to restore the sequence of events that led to discovering + /// a bug, you can add notes as you add your transitions. + const NoteTag *getNoteTag(NoteTag::Callback &&Cb) { + return Eng.getNoteTags().makeNoteTag(std::move(Cb)); + } + + /// A shorthand version of getNoteTag that doesn't require you to accept + /// the BugReporterContext arguments when you don't need it. + const NoteTag *getNoteTag(std::function<std::string(BugReport &)> &&Cb) { + return getNoteTag( + [Cb](BugReporterContext &, BugReport &BR) { return Cb(BR); }); + } + + /// Returns the word that should be used to refer to the declaration /// in the report. StringRef getDeclDescription(const Decl *D); diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/CheckerHelpers.h b/include/clang/StaticAnalyzer/Core/PathSensitive/CheckerHelpers.h index 7f34a7a5b1..b53c042a1c 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/CheckerHelpers.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/CheckerHelpers.h @@ -1,9 +1,8 @@ //== CheckerHelpers.h - Helper functions for checkers ------------*- C++ -*--=// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h index d4f8fbaa43..5b69299f78 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h @@ -1,9 +1,8 @@ //===- ConstraintManager.h - Constraints on symbolic values. ----*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // @@ -80,6 +79,9 @@ public: ConstraintManager() = default; virtual ~ConstraintManager(); + virtual bool haveEqualConstraints(ProgramStateRef S1, + ProgramStateRef S2) const = 0; + virtual ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond, bool Assumption) = 0; diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h b/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h index 17369a85bf..310c2a43aa 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h @@ -1,9 +1,8 @@ //===- CoreEngine.h - Path-Sensitive Dataflow Engine ------------*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // @@ -195,7 +194,7 @@ public: void enqueueStmtNode(ExplodedNode *N, const CFGBlock *Block, unsigned Idx); }; -// TODO: Turn into a calss. +// TODO: Turn into a class. struct NodeBuilderContext { const CoreEngine &Eng; const CFGBlock *Block; diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/DynamicTypeInfo.h b/include/clang/StaticAnalyzer/Core/PathSensitive/DynamicTypeInfo.h index 092e23ce73..9bb1e21375 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/DynamicTypeInfo.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/DynamicTypeInfo.h @@ -1,9 +1,8 @@ //== DynamicTypeInfo.h - Runtime type information ----------------*- C++ -*--=// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_DYNAMICTYPEINFO_H diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/DynamicTypeMap.h b/include/clang/StaticAnalyzer/Core/PathSensitive/DynamicTypeMap.h index b0d514dc28..6608f26b3b 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/DynamicTypeMap.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/DynamicTypeMap.h @@ -1,9 +1,8 @@ //===- DynamicTypeMap.h - Dynamic type map ----------------------*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/Environment.h b/include/clang/StaticAnalyzer/Core/PathSensitive/Environment.h index 6d498031be..6fc589b838 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/Environment.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/Environment.h @@ -1,9 +1,8 @@ //===- Environment.h - Map from Stmt* to Locations/Values -------*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/ExplodedGraph.h b/include/clang/StaticAnalyzer/Core/PathSensitive/ExplodedGraph.h index bf460df278..727d04cba2 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/ExplodedGraph.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/ExplodedGraph.h @@ -1,9 +1,8 @@ //===- ExplodedGraph.h - Local, Path-Sens. "Exploded Graph" -----*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h b/include/clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h index 86b776afb8..f0b01f182b 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h @@ -1,9 +1,8 @@ //===- ExprEngine.h - Path-Sensitive Expression-Level Dataflow --*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // @@ -23,6 +22,7 @@ #include "clang/Analysis/ProgramPoint.h" #include "clang/Basic/LLVM.h" #include "clang/StaticAnalyzer/Core/BugReporter/BugReporter.h" +#include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h" #include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h" #include "clang/StaticAnalyzer/Core/PathSensitive/FunctionSummary.h" @@ -131,6 +131,9 @@ private: /// SymMgr - Object that manages the symbol information. SymbolManager &SymMgr; + /// MRMgr - MemRegionManager object that creates memory regions. + MemRegionManager &MRMgr; + /// svalBuilder - SValBuilder object that creates SVals from expressions. SValBuilder &svalBuilder; @@ -153,6 +156,8 @@ private: /// The flag, which specifies the mode of inlining for the engine. InliningModes HowToInline; + NoteTag::Factory NoteTags; + public: ExprEngine(cross_tu::CrossTranslationUnitContext &CTU, AnalysisManager &mgr, SetOfConstDecls *VisitedCalleesIn, @@ -180,6 +185,10 @@ public: AnalysisManager &getAnalysisManager() override { return AMgr; } + AnalysisDeclContextManager &getAnalysisDeclContextManager() { + return AMgr.getAnalysisDeclContextManager(); + } + CheckerManager &getCheckerManager() const { return *AMgr.getCheckerManager(); } @@ -387,9 +396,11 @@ public: return StateMgr.getBasicVals(); } - // FIXME: Remove when we migrate over to just using ValueManager. SymbolManager &getSymbolManager() { return SymMgr; } - const SymbolManager &getSymbolManager() const { return SymMgr; } + MemRegionManager &getRegionManager() { return MRMgr; } + + NoteTag::Factory &getNoteTags() { return NoteTags; } + // Functions for external checking of whether we have unfinished work bool wasBlocksExhausted() const { return Engine.wasBlocksExhausted(); } @@ -707,6 +718,25 @@ private: AnalyzerOptions &Opts, const EvalCallOptions &CallOpts); + /// See if the given AnalysisDeclContext is built for a function that we + /// should always inline simply because it's small enough. + /// Apart from "small" functions, we also have "large" functions + /// (cf. isLarge()), some of which are huge (cf. isHuge()), and we classify + /// the remaining functions as "medium". + bool isSmall(AnalysisDeclContext *ADC) const; + + /// See if the given AnalysisDeclContext is built for a function that we + /// should inline carefully because it looks pretty large. + bool isLarge(AnalysisDeclContext *ADC) const; + + /// See if the given AnalysisDeclContext is built for a function that we + /// should never inline because it's legit gigantic. + bool isHuge(AnalysisDeclContext *ADC) const; + + /// See if the given AnalysisDeclContext is built for a function that we + /// should inline, just by looking at the declaration of the function. + bool mayInlineDecl(AnalysisDeclContext *ADC) const; + /// Checks our policies and decides weither the given call should be inlined. bool shouldInlineCall(const CallEvent &Call, const Decl *D, const ExplodedNode *Pred, diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/FunctionSummary.h b/include/clang/StaticAnalyzer/Core/PathSensitive/FunctionSummary.h index b70faa10f0..53b4bf6058 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/FunctionSummary.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/FunctionSummary.h @@ -1,9 +1,8 @@ //===- FunctionSummary.h - Stores summaries of functions. -------*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/LoopUnrolling.h b/include/clang/StaticAnalyzer/Core/PathSensitive/LoopUnrolling.h index a4c505ce5f..d25d264354 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/LoopUnrolling.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/LoopUnrolling.h @@ -1,9 +1,8 @@ //===--- LoopUnrolling.h - Unroll loops -------------------------*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// /// diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/LoopWidening.h b/include/clang/StaticAnalyzer/Core/PathSensitive/LoopWidening.h index f494c5d6da..7484a51b1e 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/LoopWidening.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/LoopWidening.h @@ -1,9 +1,8 @@ //===--- LoopWidening.h - Widen loops ---------------------------*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// /// diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h b/include/clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h index 3d0ff4efa1..071e35085a 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h @@ -1,9 +1,8 @@ //==- MemRegion.h - Abstract memory regions for static analysis -*- C++ -*--==// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // @@ -774,9 +773,6 @@ class SymbolicRegion : public SubRegion { assert(s->getType()->isAnyPointerType() || s->getType()->isReferenceType() || s->getType()->isBlockPointerType()); - - // populateWorklistFromSymbol() relies on this assertion, and needs to be - // updated if more cases are introduced. assert(isa<UnknownSpaceRegion>(sreg) || isa<HeapSpaceRegion>(sreg)); } @@ -912,7 +908,7 @@ protected: DeclRegion(const ValueDecl *d, const MemRegion *sReg, Kind k) : TypedValueRegion(sReg, k), D(d) { assert(classof(this)); - assert(d); + assert(d && d->isCanonicalDecl()); } static void ProfileRegion(llvm::FoldingSetNodeID& ID, const Decl *D, diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h b/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h index c3a7028d87..2c6465d5fb 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h @@ -1,9 +1,8 @@ //== ProgramState.h - Path-sensitive "State" for tracking values -*- C++ -*--=// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // @@ -21,7 +20,6 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h" #include "clang/StaticAnalyzer/Core/PathSensitive/Store.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/TaintTag.h" #include "llvm/ADT/FoldingSet.h" #include "llvm/ADT/ImmutableMap.h" #include "llvm/Support/Allocator.h" @@ -44,7 +42,6 @@ typedef std::unique_ptr<ConstraintManager>(*ConstraintManagerCreator)( ProgramStateManager &, SubEngine *); typedef std::unique_ptr<StoreManager>(*StoreManagerCreator)( ProgramStateManager &); -typedef llvm::ImmutableMap<const SubRegion*, TaintTagType> TaintedSubRegions; //===----------------------------------------------------------------------===// // ProgramStateTrait - Traits used by the Generic Data Map of a ProgramState. @@ -368,38 +365,6 @@ public: template <typename CB> CB scanReachableSymbols(llvm::iterator_range<region_iterator> Reachable) const; - /// Create a new state in which the statement is marked as tainted. - LLVM_NODISCARD ProgramStateRef - addTaint(const Stmt *S, const LocationContext *LCtx, - TaintTagType Kind = TaintTagGeneric) const; - - /// Create a new state in which the value is marked as tainted. - LLVM_NODISCARD ProgramStateRef - addTaint(SVal V, TaintTagType Kind = TaintTagGeneric) const; - - /// Create a new state in which the symbol is marked as tainted. - LLVM_NODISCARD ProgramStateRef addTaint(SymbolRef S, - TaintTagType Kind = TaintTagGeneric) const; - - /// Create a new state in which the region symbol is marked as tainted. - LLVM_NODISCARD ProgramStateRef - addTaint(const MemRegion *R, TaintTagType Kind = TaintTagGeneric) const; - - /// Create a new state in a which a sub-region of a given symbol is tainted. - /// This might be necessary when referring to regions that can not have an - /// individual symbol, e.g. if they are represented by the default binding of - /// a LazyCompoundVal. - LLVM_NODISCARD ProgramStateRef - addPartialTaint(SymbolRef ParentSym, const SubRegion *SubRegion, - TaintTagType Kind = TaintTagGeneric) const; - - /// Check if the statement is tainted in the current state. - bool isTainted(const Stmt *S, const LocationContext *LCtx, - TaintTagType Kind = TaintTagGeneric) const; - bool isTainted(SVal V, TaintTagType Kind = TaintTagGeneric) const; - bool isTainted(SymbolRef Sym, TaintTagType Kind = TaintTagGeneric) const; - bool isTainted(const MemRegion *Reg, TaintTagType Kind=TaintTagGeneric) const; - //==---------------------------------------------------------------------==// // Accessing the Generic Data Map (GDM). //==---------------------------------------------------------------------==// @@ -463,10 +428,8 @@ public: const LocationContext *CurrentLC = nullptr) const; void printDOT(raw_ostream &Out, const LocationContext *CurrentLC = nullptr) const; - void printTaint(raw_ostream &Out, const char *nl = "\n") const; void dump() const; - void dumpTaint() const; private: friend void ProgramStateRetain(const ProgramState *state); @@ -500,7 +463,6 @@ private: std::unique_ptr<ConstraintManager> ConstraintMgr; ProgramState::GenericDataMap::Factory GDMFactory; - TaintedSubRegions::Factory TSRFactory; typedef llvm::DenseMap<void*,std::pair<void*,void (*)(void*)> > GDMContextsTy; GDMContextsTy GDMContexts; @@ -589,11 +551,15 @@ public: ProgramStateRef getPersistentStateWithGDM(ProgramStateRef FromState, ProgramStateRef GDMState); - bool haveEqualEnvironments(ProgramStateRef S1, ProgramStateRef S2) { + bool haveEqualConstraints(ProgramStateRef S1, ProgramStateRef S2) const { + return ConstraintMgr->haveEqualConstraints(S1, S2); + } + + bool haveEqualEnvironments(ProgramStateRef S1, ProgramStateRef S2) const { return S1->Env == S2->Env; } - bool haveEqualStores(ProgramStateRef S1, ProgramStateRef S2) { + bool haveEqualStores(ProgramStateRef S1, ProgramStateRef S2) const { return S1->store == S2->store; } diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h b/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h index 64de736c7e..da82a55e36 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h @@ -1,9 +1,8 @@ //ProgramStateTrait.h - Partial implementations of ProgramStateTrait -*- C++ -*- // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h b/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h index 415bb7713d..0ea26bf2e5 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h @@ -1,9 +1,8 @@ //== ProgramState_Fwd.h - Incomplete declarations of ProgramState -*- C++ -*--=/ // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h index 1b12a4edc2..a9ca3451d8 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h @@ -1,9 +1,8 @@ //== RangedConstraintManager.h ----------------------------------*- C++ -*--==// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // @@ -114,7 +113,8 @@ private: public: RangeSet Intersect(BasicValueFactory &BV, Factory &F, llvm::APSInt Lower, llvm::APSInt Upper) const; - + RangeSet Intersect(BasicValueFactory &BV, Factory &F, + const RangeSet &Other) const; RangeSet Negate(BasicValueFactory &BV, Factory &F) const; void print(raw_ostream &os) const; diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/Regions.def b/include/clang/StaticAnalyzer/Core/PathSensitive/Regions.def index 10f89ecc55..3c52c2bc71 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/Regions.def +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/Regions.def @@ -1,9 +1,8 @@ //===-- Regions.def - Metadata about MemRegion kinds ------------*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h index 8eaa9365be..fe097b92b3 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -1,9 +1,8 @@ //== SMTConstraintManager.h -------------------------------------*- C++ -*--==// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // @@ -18,17 +17,20 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h" +typedef llvm::ImmutableSet< + std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>> + ConstraintSMTType; +REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTType) + namespace clang { namespace ento { -template <typename ConstraintSMT, typename SMTExprTy> class SMTConstraintManager : public clang::ento::SimpleConstraintManager { - SMTSolverRef &Solver; + mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver(); public: - SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB, - SMTSolverRef &S) - : SimpleConstraintManager(SE, SB), Solver(S) {} + SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB) + : SimpleConstraintManager(SE, SB) {} virtual ~SMTConstraintManager() = default; //===------------------------------------------------------------------===// @@ -42,7 +44,8 @@ public: QualType RetTy; bool hasComparison; - SMTExprRef Exp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison); + llvm::SMTExprRef Exp = + SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison); // Create zero comparison for implicit boolean cast, with reversed // assumption @@ -78,12 +81,12 @@ public: QualType RetTy; // The expression may be casted, so we cannot call getZ3DataExpr() directly - SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); - SMTExprRef Exp = + llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); + llvm::SMTExprRef Exp = SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true); // Negate the constraint - SMTExprRef NotExp = + llvm::SMTExprRef NotExp = SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false); ConditionTruthVal isSat = checkModel(State, Sym, Exp); @@ -116,7 +119,7 @@ public: // this method tries to get the interpretation (the actual value) from // the solver, which is currently not cached. - SMTExprRef Exp = + llvm::SMTExprRef Exp = SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty)); Solver->reset(); @@ -132,7 +135,7 @@ public: return nullptr; // A value has been obtained, check if it is the only value - SMTExprRef NotExp = SMTConv::fromBinOp( + llvm::SMTExprRef NotExp = SMTConv::fromBinOp( Solver, Exp, BO_NE, Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue()) : Solver->mkBitvector(Value, Value.getBitWidth()), @@ -213,11 +216,16 @@ public: OS << nl << sep << "Constraints:"; for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) { OS << nl << ' ' << I->first << " : "; - I->second.print(OS); + I->second->print(OS); } OS << nl; } + bool haveEqualConstraints(ProgramStateRef S1, + ProgramStateRef S2) const override { + return S1->get<ConstraintSMT>() == S2->get<ConstraintSMT>(); + } + bool canReasonAbout(SVal X) const override { const TargetInfo &TI = getBasicVals().getContext().getTargetInfo(); @@ -270,11 +278,10 @@ public: protected: // Check whether a new model is satisfiable, and update the program state. virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym, - const SMTExprRef &Exp) { + const llvm::SMTExprRef &Exp) { // Check the model, avoid simplifying AST to save time if (checkModel(State, Sym, Exp).isConstrainedTrue()) - return State->add<ConstraintSMT>( - std::make_pair(Sym, static_cast<const SMTExprTy &>(*Exp))); + return State->add<ConstraintSMT>(std::make_pair(Sym, Exp)); return nullptr; } @@ -288,11 +295,11 @@ protected: // Construct the logical AND of all the constraints if (I != IE) { - std::vector<SMTExprRef> ASTs; + std::vector<llvm::SMTExprRef> ASTs; - SMTExprRef Constraint = Solver->newExprRef(I++->second); + llvm::SMTExprRef Constraint = I++->second; while (I != IE) { - Constraint = Solver->mkAnd(Constraint, Solver->newExprRef(I++->second)); + Constraint = Solver->mkAnd(Constraint, I++->second); } Solver->addConstraint(Constraint); @@ -301,9 +308,9 @@ protected: // Generate and check a Z3 model, using the given constraint. ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym, - const SMTExprRef &Exp) const { - ProgramStateRef NewState = State->add<ConstraintSMT>( - std::make_pair(Sym, static_cast<const SMTExprTy &>(*Exp))); + const llvm::SMTExprRef &Exp) const { + ProgramStateRef NewState = + State->add<ConstraintSMT>(std::make_pair(Sym, Exp)); llvm::FoldingSetNodeID ID; NewState->get<ConstraintSMT>().Profile(ID); diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h index cdca2a0970..bdebe23882 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h @@ -1,9 +1,8 @@ //== SMTConv.h --------------------------------------------------*- C++ -*--==// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // @@ -16,8 +15,8 @@ #include "clang/AST/Expr.h" #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h" +#include "llvm/Support/SMTAPI.h" namespace clang { namespace ento { @@ -25,8 +24,8 @@ namespace ento { class SMTConv { public: // Returns an appropriate sort, given a QualType and it's bit width. - static inline SMTSortRef mkSort(SMTSolverRef &Solver, const QualType &Ty, - unsigned BitWidth) { + static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver, + const QualType &Ty, unsigned BitWidth) { if (Ty->isBooleanType()) return Solver->getBoolSort(); @@ -36,10 +35,10 @@ public: return Solver->getBitvectorSort(BitWidth); } - /// Constructs an SMTExprRef from an unary operator. - static inline SMTExprRef fromUnOp(SMTSolverRef &Solver, - const UnaryOperator::Opcode Op, - const SMTExprRef &Exp) { + /// Constructs an SMTSolverRef from an unary operator. + static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver, + const UnaryOperator::Opcode Op, + const llvm::SMTExprRef &Exp) { switch (Op) { case UO_Minus: return Solver->mkBVNeg(Exp); @@ -55,10 +54,10 @@ public: llvm_unreachable("Unimplemented opcode"); } - /// Constructs an SMTExprRef from a floating-point unary operator. - static inline SMTExprRef fromFloatUnOp(SMTSolverRef &Solver, - const UnaryOperator::Opcode Op, - const SMTExprRef &Exp) { + /// Constructs an SMTSolverRef from a floating-point unary operator. + static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver, + const UnaryOperator::Opcode Op, + const llvm::SMTExprRef &Exp) { switch (Op) { case UO_Minus: return Solver->mkFPNeg(Exp); @@ -71,27 +70,28 @@ public: llvm_unreachable("Unimplemented opcode"); } - /// Construct an SMTExprRef from a n-ary binary operator. - static inline SMTExprRef fromNBinOp(SMTSolverRef &Solver, - const BinaryOperator::Opcode Op, - const std::vector<SMTExprRef> &ASTs) { + /// Construct an SMTSolverRef from a n-ary binary operator. + static inline llvm::SMTExprRef + fromNBinOp(llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op, + const std::vector<llvm::SMTExprRef> &ASTs) { assert(!ASTs.empty()); if (Op != BO_LAnd && Op != BO_LOr) llvm_unreachable("Unimplemented opcode"); - SMTExprRef res = ASTs.front(); + llvm::SMTExprRef res = ASTs.front(); for (std::size_t i = 1; i < ASTs.size(); ++i) res = (Op == BO_LAnd) ? Solver->mkAnd(res, ASTs[i]) : Solver->mkOr(res, ASTs[i]); return res; } - /// Construct an SMTExprRef from a binary operator. - static inline SMTExprRef fromBinOp(SMTSolverRef &Solver, - const SMTExprRef &LHS, - const BinaryOperator::Opcode Op, - const SMTExprRef &RHS, bool isSigned) { + /// Construct an SMTSolverRef from a binary operator. + static inline llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver, + const llvm::SMTExprRef &LHS, + const BinaryOperator::Opcode Op, + const llvm::SMTExprRef &RHS, + bool isSigned) { assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) && "AST's must have the same sort!"); @@ -163,9 +163,10 @@ public: llvm_unreachable("Unimplemented opcode"); } - /// Construct an SMTExprRef from a special floating-point binary operator. - static inline SMTExprRef - fromFloatSpecialBinOp(SMTSolverRef &Solver, const SMTExprRef &LHS, + /// Construct an SMTSolverRef from a special floating-point binary + /// operator. + static inline llvm::SMTExprRef + fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::APFloat::fltCategory &RHS) { switch (Op) { @@ -196,11 +197,11 @@ public: llvm_unreachable("Unimplemented opcode"); } - /// Construct an SMTExprRef from a floating-point binary operator. - static inline SMTExprRef fromFloatBinOp(SMTSolverRef &Solver, - const SMTExprRef &LHS, - const BinaryOperator::Opcode Op, - const SMTExprRef &RHS) { + /// Construct an SMTSolverRef from a floating-point binary operator. + static inline llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef &Solver, + const llvm::SMTExprRef &LHS, + const BinaryOperator::Opcode Op, + const llvm::SMTExprRef &RHS) { assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) && "AST's must have the same sort!"); @@ -254,11 +255,13 @@ public: llvm_unreachable("Unimplemented opcode"); } - /// Construct an SMTExprRef from a QualType FromTy to a QualType ToTy, and - /// their bit widths. - static inline SMTExprRef fromCast(SMTSolverRef &Solver, const SMTExprRef &Exp, - QualType ToTy, uint64_t ToBitWidth, - QualType FromTy, uint64_t FromBitWidth) { + /// Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy, + /// and their bit widths. + static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver, + const llvm::SMTExprRef &Exp, + QualType ToTy, uint64_t ToBitWidth, + QualType FromTy, + uint64_t FromBitWidth) { if ((FromTy->isIntegralOrEnumerationType() && ToTy->isIntegralOrEnumerationType()) || (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) || @@ -292,7 +295,7 @@ public: } if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) { - SMTSortRef Sort = Solver->getFloatSort(ToBitWidth); + llvm::SMTSortRef Sort = Solver->getFloatSort(ToBitWidth); return FromTy->isSignedIntegerOrEnumerationType() ? Solver->mkSBVtoFP(Exp, Sort) : Solver->mkUBVtoFP(Exp, Sort); @@ -307,7 +310,7 @@ public: } // Callback function for doCast parameter on APSInt type. - static inline llvm::APSInt castAPSInt(SMTSolverRef &Solver, + static inline llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver, const llvm::APSInt &V, QualType ToTy, uint64_t ToWidth, QualType FromTy, uint64_t FromWidth) { @@ -315,30 +318,32 @@ public: return TargetType.convert(V); } - /// Construct an SMTExprRef from a SymbolData. - static inline SMTExprRef fromData(SMTSolverRef &Solver, const SymbolID ID, - const QualType &Ty, uint64_t BitWidth) { + /// Construct an SMTSolverRef from a SymbolData. + static inline llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver, + const SymbolID ID, const QualType &Ty, + uint64_t BitWidth) { llvm::Twine Name = "$" + llvm::Twine(ID); return Solver->mkSymbol(Name.str().c_str(), mkSort(Solver, Ty, BitWidth)); } - // Wrapper to generate SMTExprRef from SymbolCast data. - static inline SMTExprRef getCastExpr(SMTSolverRef &Solver, ASTContext &Ctx, - const SMTExprRef &Exp, QualType FromTy, - QualType ToTy) { + // Wrapper to generate SMTSolverRef from SymbolCast data. + static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver, + ASTContext &Ctx, + const llvm::SMTExprRef &Exp, + QualType FromTy, QualType ToTy) { return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy, Ctx.getTypeSize(FromTy)); } - // Wrapper to generate SMTExprRef from unpacked binary symbolic expression. - // Sets the RetTy parameter. See getSMTExprRef(). - static inline SMTExprRef getBinExpr(SMTSolverRef &Solver, ASTContext &Ctx, - const SMTExprRef &LHS, QualType LTy, - BinaryOperator::Opcode Op, - const SMTExprRef &RHS, QualType RTy, - QualType *RetTy) { - SMTExprRef NewLHS = LHS; - SMTExprRef NewRHS = RHS; + // Wrapper to generate SMTSolverRef from unpacked binary symbolic + // expression. Sets the RetTy parameter. See getSMTSolverRef(). + static inline llvm::SMTExprRef + getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, + const llvm::SMTExprRef &LHS, QualType LTy, + BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, + QualType RTy, QualType *RetTy) { + llvm::SMTExprRef NewLHS = LHS; + llvm::SMTExprRef NewRHS = RHS; doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy); // Update the return type parameter if the output type has changed. @@ -366,36 +371,40 @@ public: LTy->isSignedIntegerOrEnumerationType()); } - // Wrapper to generate SMTExprRef from BinarySymExpr. - // Sets the hasComparison and RetTy parameters. See getSMTExprRef(). - static inline SMTExprRef getSymBinExpr(SMTSolverRef &Solver, ASTContext &Ctx, - const BinarySymExpr *BSE, - bool *hasComparison, QualType *RetTy) { + // Wrapper to generate SMTSolverRef from BinarySymExpr. + // Sets the hasComparison and RetTy parameters. See getSMTSolverRef(). + static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver, + ASTContext &Ctx, + const BinarySymExpr *BSE, + bool *hasComparison, + QualType *RetTy) { QualType LTy, RTy; BinaryOperator::Opcode Op = BSE->getOpcode(); if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) { - SMTExprRef LHS = + llvm::SMTExprRef LHS = getSymExpr(Solver, Ctx, SIE->getLHS(), <y, hasComparison); llvm::APSInt NewRInt; std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS()); - SMTExprRef RHS = Solver->mkBitvector(NewRInt, NewRInt.getBitWidth()); + llvm::SMTExprRef RHS = + Solver->mkBitvector(NewRInt, NewRInt.getBitWidth()); return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); } if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) { llvm::APSInt NewLInt; std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS()); - SMTExprRef LHS = Solver->mkBitvector(NewLInt, NewLInt.getBitWidth()); - SMTExprRef RHS = + llvm::SMTExprRef LHS = + Solver->mkBitvector(NewLInt, NewLInt.getBitWidth()); + llvm::SMTExprRef RHS = getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison); return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); } if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) { - SMTExprRef LHS = + llvm::SMTExprRef LHS = getSymExpr(Solver, Ctx, SSM->getLHS(), <y, hasComparison); - SMTExprRef RHS = + llvm::SMTExprRef RHS = getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison); return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); } @@ -405,9 +414,10 @@ public: // Recursive implementation to unpack and generate symbolic expression. // Sets the hasComparison and RetTy parameters. See getExpr(). - static inline SMTExprRef getSymExpr(SMTSolverRef &Solver, ASTContext &Ctx, - SymbolRef Sym, QualType *RetTy, - bool *hasComparison) { + static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver, + ASTContext &Ctx, SymbolRef Sym, + QualType *RetTy, + bool *hasComparison) { if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) { if (RetTy) *RetTy = Sym->getType(); @@ -421,7 +431,7 @@ public: *RetTy = Sym->getType(); QualType FromTy; - SMTExprRef Exp = + llvm::SMTExprRef Exp = getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison); // Casting an expression with a comparison invalidates it. Note that this @@ -433,7 +443,8 @@ public: } if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) { - SMTExprRef Exp = getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy); + llvm::SMTExprRef Exp = + getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy); // Set the hasComparison parameter, in post-order traversal order. if (hasComparison) *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode()); @@ -443,13 +454,14 @@ public: llvm_unreachable("Unsupported SymbolRef type!"); } - // Generate an SMTExprRef that represents the given symbolic expression. + // Generate an SMTSolverRef that represents the given symbolic expression. // Sets the hasComparison parameter if the expression has a comparison // operator. Sets the RetTy parameter to the final return type after // promotions and casts. - static inline SMTExprRef getExpr(SMTSolverRef &Solver, ASTContext &Ctx, - SymbolRef Sym, QualType *RetTy = nullptr, - bool *hasComparison = nullptr) { + static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver, + ASTContext &Ctx, SymbolRef Sym, + QualType *RetTy = nullptr, + bool *hasComparison = nullptr) { if (hasComparison) { *hasComparison = false; } @@ -457,11 +469,11 @@ public: return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison); } - // Generate an SMTExprRef that compares the expression to zero. - static inline SMTExprRef getZeroExpr(SMTSolverRef &Solver, ASTContext &Ctx, - const SMTExprRef &Exp, QualType Ty, - bool Assumption) { - + // Generate an SMTSolverRef that compares the expression to zero. + static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver, + ASTContext &Ctx, + const llvm::SMTExprRef &Exp, + QualType Ty, bool Assumption) { if (Ty->isRealFloatingType()) { llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty)); @@ -486,21 +498,21 @@ public: llvm_unreachable("Unsupported type for zero value!"); } - // Wrapper to generate SMTExprRef from a range. If From == To, an equality - // will be created instead. - static inline SMTExprRef getRangeExpr(SMTSolverRef &Solver, ASTContext &Ctx, - SymbolRef Sym, const llvm::APSInt &From, - const llvm::APSInt &To, bool InRange) { + // Wrapper to generate SMTSolverRef from a range. If From == To, an + // equality will be created instead. + static inline llvm::SMTExprRef + getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, + const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) { // Convert lower bound QualType FromTy; llvm::APSInt NewFromInt; std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From); - SMTExprRef FromExp = + llvm::SMTExprRef FromExp = Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth()); // Convert symbol QualType SymTy; - SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy); + llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy); // Construct single (in)equality if (From == To) @@ -510,16 +522,17 @@ public: QualType ToTy; llvm::APSInt NewToInt; std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To); - SMTExprRef ToExp = Solver->mkBitvector(NewToInt, NewToInt.getBitWidth()); + llvm::SMTExprRef ToExp = + Solver->mkBitvector(NewToInt, NewToInt.getBitWidth()); assert(FromTy == ToTy && "Range values have different types!"); // Construct two (in)equalities, and a logical and/or - SMTExprRef LHS = + llvm::SMTExprRef LHS = getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp, FromTy, /*RetTy=*/nullptr); - SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy, - InRange ? BO_LE : BO_GT, ToExp, ToTy, - /*RetTy=*/nullptr); + llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy, + InRange ? BO_LE : BO_GT, ToExp, ToTy, + /*RetTy=*/nullptr); return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS, SymTy->isSignedIntegerOrEnumerationType()); @@ -551,23 +564,24 @@ public: // Perform implicit type conversion on binary symbolic expressions. // May modify all input parameters. // TODO: Refactor to use built-in conversion functions - static inline void doTypeConversion(SMTSolverRef &Solver, ASTContext &Ctx, - SMTExprRef &LHS, SMTExprRef &RHS, - QualType <y, QualType &RTy) { + static inline void doTypeConversion(llvm::SMTSolverRef &Solver, + ASTContext &Ctx, llvm::SMTExprRef &LHS, + llvm::SMTExprRef &RHS, QualType <y, + QualType &RTy) { assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!"); // Perform type conversion if ((LTy->isIntegralOrEnumerationType() && RTy->isIntegralOrEnumerationType()) && (LTy->isArithmeticType() && RTy->isArithmeticType())) { - SMTConv::doIntTypeConversion<SMTExprRef, &fromCast>(Solver, Ctx, LHS, LTy, - RHS, RTy); + SMTConv::doIntTypeConversion<llvm::SMTExprRef, &fromCast>( + Solver, Ctx, LHS, LTy, RHS, RTy); return; } if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) { - SMTConv::doFloatTypeConversion<SMTExprRef, &fromCast>(Solver, Ctx, LHS, - LTy, RHS, RTy); + SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>( + Solver, Ctx, LHS, LTy, RHS, RTy); return; } @@ -625,12 +639,11 @@ public: // Perform implicit integer type conversion. // May modify all input parameters. // TODO: Refactor to use Sema::handleIntegerConversion() - template <typename T, T (*doCast)(SMTSolverRef &Solver, const T &, QualType, - uint64_t, QualType, uint64_t)> - static inline void doIntTypeConversion(SMTSolverRef &Solver, ASTContext &Ctx, - T &LHS, QualType <y, T &RHS, - QualType &RTy) { - + template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &, + QualType, uint64_t, QualType, uint64_t)> + static inline void doIntTypeConversion(llvm::SMTSolverRef &Solver, + ASTContext &Ctx, T &LHS, QualType <y, + T &RHS, QualType &RTy) { uint64_t LBitWidth = Ctx.getTypeSize(LTy); uint64_t RBitWidth = Ctx.getTypeSize(RTy); @@ -708,12 +721,11 @@ public: // Perform implicit floating-point type conversion. // May modify all input parameters. // TODO: Refactor to use Sema::handleFloatConversion() - template <typename T, T (*doCast)(SMTSolverRef &Solver, const T &, QualType, - uint64_t, QualType, uint64_t)> + template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &, + QualType, uint64_t, QualType, uint64_t)> static inline void - doFloatTypeConversion(SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, + doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType <y, T &RHS, QualType &RTy) { - uint64_t LBitWidth = Ctx.getTypeSize(LTy); uint64_t RBitWidth = Ctx.getTypeSize(RTy); @@ -750,4 +762,4 @@ public: } // namespace ento } // namespace clang -#endif
\ No newline at end of file +#endif diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h deleted file mode 100644 index 9dedf96cfa..0000000000 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h +++ /dev/null @@ -1,62 +0,0 @@ -//== SMTExpr.h --------------------------------------------------*- C++ -*--==// -// -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// -// -// This file defines a SMT generic Expr API, which will be the base class -// for every SMT solver expr specific class. -// -//===----------------------------------------------------------------------===// - -#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H -#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H - -#include "clang/Basic/TargetInfo.h" -#include "llvm/ADT/FoldingSet.h" - -namespace clang { -namespace ento { - -/// Generic base class for SMT exprs -class SMTExpr { -public: - SMTExpr() = default; - virtual ~SMTExpr() = default; - - bool operator<(const SMTExpr &Other) const { - llvm::FoldingSetNodeID ID1, ID2; - Profile(ID1); - Other.Profile(ID2); - return ID1 < ID2; - } - - virtual void Profile(llvm::FoldingSetNodeID &ID) const { - static int Tag = 0; - ID.AddPointer(&Tag); - } - - friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) { - return LHS.equal_to(RHS); - } - - virtual void print(raw_ostream &OS) const = 0; - - LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } - -protected: - /// Query the SMT solver and returns true if two sorts are equal (same kind - /// and bit width). This does not check if the two sorts are the same objects. - virtual bool equal_to(SMTExpr const &other) const = 0; -}; - -/// Shared pointer for SMTExprs, used by SMTSolver API. -using SMTExprRef = std::shared_ptr<SMTExpr>; - -} // namespace ento -} // namespace clang - -#endif diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h deleted file mode 100644 index 2abe5fc987..0000000000 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h +++ /dev/null @@ -1,303 +0,0 @@ -//== SMTSolver.h ------------------------------------------------*- C++ -*--==// -// -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// -// -// This file defines a SMT generic Solver API, which will be the base class -// for every SMT solver specific class. -// -//===----------------------------------------------------------------------===// - -#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H -#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H - -#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h" -#include "llvm/ADT/APSInt.h" - -namespace clang { -namespace ento { - -/// Generic base class for SMT Solvers -/// -/// This class is responsible for wrapping all sorts and expression generation, -/// through the mk* methods. It also provides methods to create SMT expressions -/// straight from clang's AST, through the from* methods. -class SMTSolver { -public: - SMTSolver() = default; - virtual ~SMTSolver() = default; - - LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } - - // Returns an appropriate floating-point sort for the given bitwidth. - SMTSortRef getFloatSort(unsigned BitWidth) { - switch (BitWidth) { - case 16: - return getFloat16Sort(); - case 32: - return getFloat32Sort(); - case 64: - return getFloat64Sort(); - case 128: - return getFloat128Sort(); - default:; - } - llvm_unreachable("Unsupported floating-point bitwidth!"); - } - - // Returns a boolean sort. - virtual SMTSortRef getBoolSort() = 0; - - // Returns an appropriate bitvector sort for the given bitwidth. - virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0; - - // Returns a floating-point sort of width 16 - virtual SMTSortRef getFloat16Sort() = 0; - - // Returns a floating-point sort of width 32 - virtual SMTSortRef getFloat32Sort() = 0; - - // Returns a floating-point sort of width 64 - virtual SMTSortRef getFloat64Sort() = 0; - - // Returns a floating-point sort of width 128 - virtual SMTSortRef getFloat128Sort() = 0; - - // Returns an appropriate sort for the given AST. - virtual SMTSortRef getSort(const SMTExprRef &AST) = 0; - - // Returns a new SMTExprRef from an SMTExpr - virtual SMTExprRef newExprRef(const SMTExpr &E) const = 0; - - /// Given a constraint, adds it to the solver - virtual void addConstraint(const SMTExprRef &Exp) const = 0; - - /// Creates a bitvector addition operation - virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector subtraction operation - virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector multiplication operation - virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector signed modulus operation - virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector unsigned modulus operation - virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector signed division operation - virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector unsigned division operation - virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector logical shift left operation - virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector arithmetic shift right operation - virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector logical shift right operation - virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector negation operation - virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0; - - /// Creates a bitvector not operation - virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0; - - /// Creates a bitvector xor operation - virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector or operation - virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector and operation - virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector unsigned less-than operation - virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector signed less-than operation - virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector unsigned greater-than operation - virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector signed greater-than operation - virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector unsigned less-equal-than operation - virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector signed less-equal-than operation - virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector unsigned greater-equal-than operation - virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a bitvector signed greater-equal-than operation - virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a boolean not operation - virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0; - - /// Creates a boolean equality operation - virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a boolean and operation - virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a boolean or operation - virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a boolean ite operation - virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T, - const SMTExprRef &F) = 0; - - /// Creates a bitvector sign extension operation - virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0; - - /// Creates a bitvector zero extension operation - virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0; - - /// Creates a bitvector extract operation - virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low, - const SMTExprRef &Exp) = 0; - - /// Creates a bitvector concat operation - virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS, - const SMTExprRef &RHS) = 0; - - /// Creates a floating-point negation operation - virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0; - - /// Creates a floating-point isInfinite operation - virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0; - - /// Creates a floating-point isNaN operation - virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0; - - /// Creates a floating-point isNormal operation - virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0; - - /// Creates a floating-point isZero operation - virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0; - - /// Creates a floating-point multiplication operation - virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a floating-point division operation - virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a floating-point remainder operation - virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a floating-point addition operation - virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a floating-point subtraction operation - virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a floating-point less-than operation - virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a floating-point greater-than operation - virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a floating-point less-than-or-equal operation - virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a floating-point greater-than-or-equal operation - virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; - - /// Creates a floating-point equality operation - virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS, - const SMTExprRef &RHS) = 0; - - /// Creates a floating-point conversion from floatint-point to floating-point - /// operation - virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0; - - /// Creates a floating-point conversion from signed bitvector to - /// floatint-point operation - virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, - const SMTSortRef &To) = 0; - - /// Creates a floating-point conversion from unsigned bitvector to - /// floatint-point operation - virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, - const SMTSortRef &To) = 0; - - /// Creates a floating-point conversion from floatint-point to signed - /// bitvector operation - virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) = 0; - - /// Creates a floating-point conversion from floatint-point to unsigned - /// bitvector operation - virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) = 0; - - /// Creates a new symbol, given a name and a sort - virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0; - - // Returns an appropriate floating-point rounding mode. - virtual SMTExprRef getFloatRoundingMode() = 0; - - // If the a model is available, returns the value of a given bitvector symbol - virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth, - bool isUnsigned) = 0; - - // If the a model is available, returns the value of a given boolean symbol - virtual bool getBoolean(const SMTExprRef &Exp) = 0; - - /// Constructs an SMTExprRef from a boolean. - virtual SMTExprRef mkBoolean(const bool b) = 0; - - /// Constructs an SMTExprRef from a finite APFloat. - virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0; - - /// Constructs an SMTExprRef from an APSInt and its bit width - virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0; - - /// Given an expression, extract the value of this operand in the model. - virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0; - - /// Given an expression extract the value of this operand in the model. - virtual bool getInterpretation(const SMTExprRef &Exp, - llvm::APFloat &Float) = 0; - - /// Check if the constraints are satisfiable - virtual Optional<bool> check() const = 0; - - /// Push the current solver state - virtual void push() = 0; - - /// Pop the previous solver state - virtual void pop(unsigned NumStates = 1) = 0; - - /// Reset the solver and remove all constraints. - virtual void reset() = 0; - - /// Checks if the solver supports floating-points. - virtual bool isFPSupported() = 0; - - virtual void print(raw_ostream &OS) const = 0; -}; - -/// Shared pointer for SMTSolvers. -using SMTSolverRef = std::shared_ptr<SMTSolver>; - -/// Convenience method to create and Z3Solver object -SMTSolverRef CreateZ3Solver(); - -} // namespace ento -} // namespace clang - -#endif diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h deleted file mode 100644 index 41ef573f0c..0000000000 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h +++ /dev/null @@ -1,91 +0,0 @@ -//== SMTSort.h --------------------------------------------------*- C++ -*--==// -// -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// -// -// This file defines a SMT generic Sort API, which will be the base class -// for every SMT solver sort specific class. -// -//===----------------------------------------------------------------------===// - -#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H -#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H - -#include "clang/Basic/TargetInfo.h" - -namespace clang { -namespace ento { - -/// Generic base class for SMT sorts -class SMTSort { -public: - SMTSort() = default; - virtual ~SMTSort() = default; - - /// Returns true if the sort is a bitvector, calls isBitvectorSortImpl(). - virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); } - - /// Returns true if the sort is a floating-point, calls isFloatSortImpl(). - virtual bool isFloatSort() const { return isFloatSortImpl(); } - - /// Returns true if the sort is a boolean, calls isBooleanSortImpl(). - virtual bool isBooleanSort() const { return isBooleanSortImpl(); } - - /// Returns the bitvector size, fails if the sort is not a bitvector - /// Calls getBitvectorSortSizeImpl(). - virtual unsigned getBitvectorSortSize() const { - assert(isBitvectorSort() && "Not a bitvector sort!"); - unsigned Size = getBitvectorSortSizeImpl(); - assert(Size && "Size is zero!"); - return Size; - }; - - /// Returns the floating-point size, fails if the sort is not a floating-point - /// Calls getFloatSortSizeImpl(). - virtual unsigned getFloatSortSize() const { - assert(isFloatSort() && "Not a floating-point sort!"); - unsigned Size = getFloatSortSizeImpl(); - assert(Size && "Size is zero!"); - return Size; - }; - - friend bool operator==(SMTSort const &LHS, SMTSort const &RHS) { - return LHS.equal_to(RHS); - } - - virtual void print(raw_ostream &OS) const = 0; - - LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } - -protected: - /// Query the SMT solver and returns true if two sorts are equal (same kind - /// and bit width). This does not check if the two sorts are the same objects. - virtual bool equal_to(SMTSort const &other) const = 0; - - /// Query the SMT solver and checks if a sort is bitvector. - virtual bool isBitvectorSortImpl() const = 0; - - /// Query the SMT solver and checks if a sort is floating-point. - virtual bool isFloatSortImpl() const = 0; - - /// Query the SMT solver and checks if a sort is boolean. - virtual bool isBooleanSortImpl() const = 0; - - /// Query the SMT solver and returns the sort bit width. - virtual unsigned getBitvectorSortSizeImpl() const = 0; - - /// Query the SMT solver and returns the sort bit width. - virtual unsigned getFloatSortSizeImpl() const = 0; -}; - -/// Shared pointer for SMTSorts, used by SMTSolver API. -using SMTSortRef = std::shared_ptr<SMTSort>; - -} // namespace ento -} // namespace clang - -#endif diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h index c9e284a1a3..35ebefdc00 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h @@ -1,9 +1,8 @@ // SValBuilder.h - Construction of SVals from evaluating expressions -*- C++ -*- // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h index f87fdce156..fc83e26183 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h @@ -1,9 +1,8 @@ //===--- SValVisitor.h - Visitor for SVal subclasses ------------*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.def b/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.def index a0e3099378..eb05de6d99 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.def +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.def @@ -1,9 +1,8 @@ //===-- SVals.def - Metadata about SVal kinds -------------------*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h index 0efe96f67f..e859936621 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h @@ -1,9 +1,8 @@ //===- SVals.h - Abstract Values for Static Analysis ------------*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // @@ -668,13 +667,4 @@ private: } // namespace clang -namespace llvm { - -template <typename T> struct isPodLike; -template <> struct isPodLike<clang::ento::SVal> { - static const bool value = true; -}; - -} // namespace llvm - #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SVALS_H diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h index d64b90e2d3..6bf5e94afd 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h @@ -1,9 +1,8 @@ //== SimpleConstraintManager.h ----------------------------------*- C++ -*--==// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/Store.h b/include/clang/StaticAnalyzer/Core/PathSensitive/Store.h index f49f761c77..1773683329 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/Store.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/Store.h @@ -1,9 +1,8 @@ //===- Store.h - Interface for maps from Locations to Values ----*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/StoreRef.h b/include/clang/StaticAnalyzer/Core/PathSensitive/StoreRef.h index 22259a239c..a2dd05cfdf 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/StoreRef.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/StoreRef.h @@ -1,9 +1,8 @@ //===- StoreRef.h - Smart pointer for store objects -------------*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h index d745b0f51a..9296e17ca0 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h @@ -1,9 +1,8 @@ //== SubEngine.h - Interface of the subengine of CoreEngine --------*- C++ -*-// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SummaryManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SummaryManager.h index 0a75eeb3ea..1a56153da1 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SummaryManager.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SummaryManager.h @@ -1,9 +1,8 @@ //== SummaryManager.h - Generic handling of function summaries --*- C++ -*--==// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h index 69b9858d3f..abfcd1d80f 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h @@ -1,9 +1,8 @@ //===- SymExpr.h - Management of Symbolic Values ----------------*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h index d02a8abd11..d212e23da6 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h @@ -1,9 +1,8 @@ //===- SymbolManager.h - Management of Symbolic Values ----------*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/Symbols.def b/include/clang/StaticAnalyzer/Core/PathSensitive/Symbols.def index 7d4d8fe0a5..7163a16263 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/Symbols.def +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/Symbols.def @@ -1,9 +1,8 @@ //===-- Symbols.def - Metadata about SymExpr kinds --------------*- C++ -*-===// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/TaintManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/TaintManager.h deleted file mode 100644 index 8218fb1eea..0000000000 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/TaintManager.h +++ /dev/null @@ -1,59 +0,0 @@ -//===- TaintManager.h - Managing taint --------------------------*- C++ -*-===// -// -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// -// -// This file provides APIs for adding, removing, querying symbol taint. -// -//===----------------------------------------------------------------------===// - -#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_TAINTMANAGER_H -#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_TAINTMANAGER_H - -#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/TaintTag.h" -#include "llvm/ADT/ImmutableMap.h" - -namespace clang { -namespace ento { - -/// The GDM component containing the tainted root symbols. We lazily infer the -/// taint of the dependent symbols. Currently, this is a map from a symbol to -/// tag kind. TODO: Should support multiple tag kinds. -// FIXME: This does not use the nice trait macros because it must be accessible -// from multiple translation units. -struct TaintMap {}; - -using TaintMapImpl = llvm::ImmutableMap<SymbolRef, TaintTagType>; - -template<> struct ProgramStateTrait<TaintMap> - : public ProgramStatePartialTrait<TaintMapImpl> { - static void *GDMIndex(); -}; - -/// The GDM component mapping derived symbols' parent symbols to their -/// underlying regions. This is used to efficiently check whether a symbol is -/// tainted when it represents a sub-region of a tainted symbol. -struct DerivedSymTaint {}; - -using DerivedSymTaintImpl = llvm::ImmutableMap<SymbolRef, TaintedSubRegions>; - -template<> struct ProgramStateTrait<DerivedSymTaint> - : public ProgramStatePartialTrait<DerivedSymTaintImpl> { - static void *GDMIndex(); -}; - -class TaintManager { - TaintManager() = default; -}; - -} // namespace ento -} // namespace clang - -#endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_TAINTMANAGER_H diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/TaintTag.h b/include/clang/StaticAnalyzer/Core/PathSensitive/TaintTag.h deleted file mode 100644 index 50c4b8194c..0000000000 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/TaintTag.h +++ /dev/null @@ -1,30 +0,0 @@ -//===- TaintTag.h - Path-sensitive "State" for tracking values --*- C++ -*-===// -// -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// -// -// Defines a set of taint tags. Several tags are used to differentiate kinds -// of taint. -// -//===----------------------------------------------------------------------===// - -#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_TAINTTAG_H -#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_TAINTTAG_H - -namespace clang { -namespace ento { - -/// The type of taint, which helps to differentiate between different types of -/// taint. -using TaintTagType = unsigned; - -static const TaintTagType TaintTagGeneric = 0; - -} // namespace ento -} // namespace clang - -#endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_TAINTTAG_H diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/WorkList.h b/include/clang/StaticAnalyzer/Core/PathSensitive/WorkList.h index ef3c2694b2..7beb7ddf5b 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/WorkList.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/WorkList.h @@ -1,9 +1,8 @@ //==- WorkList.h - Worklist class used by CoreEngine ---------------*- C++ -*-// // -// The LLVM Compiler Infrastructure -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception // //===----------------------------------------------------------------------===// // |