15bc81eb9SEugene Zelenko //===- ConstraintManager.cpp - Constraints on symbolic values. ------------===//
2244e1d7dSTed Kremenek //
32946cd70SChandler Carruth // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
42946cd70SChandler Carruth // See https://llvm.org/LICENSE.txt for license information.
52946cd70SChandler Carruth // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6244e1d7dSTed Kremenek //
7244e1d7dSTed Kremenek //===----------------------------------------------------------------------===//
8244e1d7dSTed Kremenek //
9244e1d7dSTed Kremenek //  This file defined the interface to manage constraints on symbolic values.
10244e1d7dSTed Kremenek //
11244e1d7dSTed Kremenek //===----------------------------------------------------------------------===//
12244e1d7dSTed Kremenek 
135bc81eb9SEugene Zelenko #include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
145bc81eb9SEugene Zelenko #include "clang/AST/Type.h"
155bc81eb9SEugene Zelenko #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h"
16244e1d7dSTed Kremenek #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
175bc81eb9SEugene Zelenko #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
185bc81eb9SEugene Zelenko #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
19f66f4d3bSGabor Marton #include "llvm/ADT/ScopeExit.h"
20244e1d7dSTed Kremenek 
21244e1d7dSTed Kremenek using namespace clang;
22244e1d7dSTed Kremenek using namespace ento;
23244e1d7dSTed Kremenek 
245bc81eb9SEugene Zelenko ConstraintManager::~ConstraintManager() = default;
25244e1d7dSTed Kremenek 
getLocFromSymbol(const ProgramStateRef & State,SymbolRef Sym)26244e1d7dSTed Kremenek static DefinedSVal getLocFromSymbol(const ProgramStateRef &State,
27244e1d7dSTed Kremenek                                     SymbolRef Sym) {
289bc02ceeSDominic Chen   const MemRegion *R =
299bc02ceeSDominic Chen       State->getStateManager().getRegionManager().getSymbolicRegion(Sym);
30244e1d7dSTed Kremenek   return loc::MemRegionVal(R);
31244e1d7dSTed Kremenek }
32244e1d7dSTed Kremenek 
checkNull(ProgramStateRef State,SymbolRef Sym)33417591fbSJordan Rose ConditionTruthVal ConstraintManager::checkNull(ProgramStateRef State,
34244e1d7dSTed Kremenek                                                SymbolRef Sym) {
35a808e165STed Kremenek   QualType Ty = Sym->getType();
36244e1d7dSTed Kremenek   DefinedSVal V = Loc::isLocType(Ty) ? getLocFromSymbol(State, Sym)
37244e1d7dSTed Kremenek                                      : nonloc::SymbolVal(Sym);
38244e1d7dSTed Kremenek   const ProgramStatePair &P = assumeDual(State, V);
39244e1d7dSTed Kremenek   if (P.first && !P.second)
40244e1d7dSTed Kremenek     return ConditionTruthVal(false);
41244e1d7dSTed Kremenek   if (!P.first && P.second)
42244e1d7dSTed Kremenek     return ConditionTruthVal(true);
435bc81eb9SEugene Zelenko   return {};
44244e1d7dSTed Kremenek }
45c4fa05f5SGabor Marton 
4696fba640SGabor Marton template <typename AssumeFunction>
47c4fa05f5SGabor Marton ConstraintManager::ProgramStatePair
assumeDualImpl(ProgramStateRef & State,AssumeFunction & Assume)4896fba640SGabor Marton ConstraintManager::assumeDualImpl(ProgramStateRef &State,
4996fba640SGabor Marton                                   AssumeFunction &Assume) {
50*17e9ea61SGabor Marton   if (LLVM_UNLIKELY(State->isPosteriorlyOverconstrained()))
5181e44414SGabor Marton     return {State, State};
5281e44414SGabor Marton 
53f66f4d3bSGabor Marton   // Assume functions might recurse (see `reAssume` or `tryRearrange`). During
54f66f4d3bSGabor Marton   // the recursion the State might not change anymore, that means we reached a
55f66f4d3bSGabor Marton   // fixpoint.
56f66f4d3bSGabor Marton   // We avoid infinite recursion of assume calls by checking already visited
57f66f4d3bSGabor Marton   // States on the stack of assume function calls.
58f66f4d3bSGabor Marton   const ProgramState *RawSt = State.get();
59f66f4d3bSGabor Marton   if (LLVM_UNLIKELY(AssumeStack.contains(RawSt)))
60f66f4d3bSGabor Marton     return {State, State};
61f66f4d3bSGabor Marton   AssumeStack.push(RawSt);
62f66f4d3bSGabor Marton   auto AssumeStackBuilder =
63f66f4d3bSGabor Marton       llvm::make_scope_exit([this]() { AssumeStack.pop(); });
64f66f4d3bSGabor Marton 
6596fba640SGabor Marton   ProgramStateRef StTrue = Assume(true);
66c4fa05f5SGabor Marton 
67c4fa05f5SGabor Marton   if (!StTrue) {
6896fba640SGabor Marton     ProgramStateRef StFalse = Assume(false);
69c4fa05f5SGabor Marton     if (LLVM_UNLIKELY(!StFalse)) { // both infeasible
70c4fa05f5SGabor Marton       ProgramStateRef StInfeasible = State->cloneAsPosteriorlyOverconstrained();
71c4fa05f5SGabor Marton       assert(StInfeasible->isPosteriorlyOverconstrained());
72c4fa05f5SGabor Marton       // Checkers might rely on the API contract that both returned states
73c4fa05f5SGabor Marton       // cannot be null. Thus, we return StInfeasible for both branches because
74c4fa05f5SGabor Marton       // it might happen that a Checker uncoditionally uses one of them if the
75c4fa05f5SGabor Marton       // other is a nullptr. This may also happen with the non-dual and
76c4fa05f5SGabor Marton       // adjacent `assume(true)` and `assume(false)` calls. By implementing
77c4fa05f5SGabor Marton       // assume in therms of assumeDual, we can keep our API contract there as
78c4fa05f5SGabor Marton       // well.
79c4fa05f5SGabor Marton       return ProgramStatePair(StInfeasible, StInfeasible);
80c4fa05f5SGabor Marton     }
81c4fa05f5SGabor Marton     return ProgramStatePair(nullptr, StFalse);
82c4fa05f5SGabor Marton   }
83c4fa05f5SGabor Marton 
8496fba640SGabor Marton   ProgramStateRef StFalse = Assume(false);
85c4fa05f5SGabor Marton   if (!StFalse) {
86c4fa05f5SGabor Marton     return ProgramStatePair(StTrue, nullptr);
87c4fa05f5SGabor Marton   }
88c4fa05f5SGabor Marton 
89c4fa05f5SGabor Marton   return ProgramStatePair(StTrue, StFalse);
90c4fa05f5SGabor Marton }
911c1c1e25SGabor Marton 
9232f189b0SGabor Marton ConstraintManager::ProgramStatePair
assumeDual(ProgramStateRef State,DefinedSVal Cond)9396fba640SGabor Marton ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) {
9496fba640SGabor Marton   auto AssumeFun = [&](bool Assumption) {
9596fba640SGabor Marton     return assumeInternal(State, Cond, Assumption);
9696fba640SGabor Marton   };
9796fba640SGabor Marton   return assumeDualImpl(State, AssumeFun);
9896fba640SGabor Marton }
9996fba640SGabor Marton 
10096fba640SGabor Marton ConstraintManager::ProgramStatePair
assumeInclusiveRangeDual(ProgramStateRef State,NonLoc Value,const llvm::APSInt & From,const llvm::APSInt & To)10132f189b0SGabor Marton ConstraintManager::assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value,
10232f189b0SGabor Marton                                             const llvm::APSInt &From,
10332f189b0SGabor Marton                                             const llvm::APSInt &To) {
10496fba640SGabor Marton   auto AssumeFun = [&](bool Assumption) {
10596fba640SGabor Marton     return assumeInclusiveRangeInternal(State, Value, From, To, Assumption);
10696fba640SGabor Marton   };
10796fba640SGabor Marton   return assumeDualImpl(State, AssumeFun);
10832f189b0SGabor Marton }
10932f189b0SGabor Marton 
assume(ProgramStateRef State,DefinedSVal Cond,bool Assumption)1101c1c1e25SGabor Marton ProgramStateRef ConstraintManager::assume(ProgramStateRef State,
1111c1c1e25SGabor Marton                                           DefinedSVal Cond, bool Assumption) {
1121c1c1e25SGabor Marton   ConstraintManager::ProgramStatePair R = assumeDual(State, Cond);
1131c1c1e25SGabor Marton   return Assumption ? R.first : R.second;
1141c1c1e25SGabor Marton }
11532f189b0SGabor Marton 
11632f189b0SGabor Marton ProgramStateRef
assumeInclusiveRange(ProgramStateRef State,NonLoc Value,const llvm::APSInt & From,const llvm::APSInt & To,bool InBound)11732f189b0SGabor Marton ConstraintManager::assumeInclusiveRange(ProgramStateRef State, NonLoc Value,
11832f189b0SGabor Marton                                         const llvm::APSInt &From,
11932f189b0SGabor Marton                                         const llvm::APSInt &To, bool InBound) {
12032f189b0SGabor Marton   ConstraintManager::ProgramStatePair R =
12132f189b0SGabor Marton       assumeInclusiveRangeDual(State, Value, From, To);
12232f189b0SGabor Marton   return InBound ? R.first : R.second;
12332f189b0SGabor Marton }
124