xref: /freebsd-src/contrib/llvm-project/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp (revision 5f757f3ff9144b609b3c433dfd370cc6bdc191ad)
10b57cec5SDimitry Andric //===- ConstraintManager.cpp - Constraints on symbolic values. ------------===//
20b57cec5SDimitry Andric //
30b57cec5SDimitry Andric // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
40b57cec5SDimitry Andric // See https://llvm.org/LICENSE.txt for license information.
50b57cec5SDimitry Andric // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
60b57cec5SDimitry Andric //
70b57cec5SDimitry Andric //===----------------------------------------------------------------------===//
80b57cec5SDimitry Andric //
90b57cec5SDimitry Andric //  This file defined the interface to manage constraints on symbolic values.
100b57cec5SDimitry Andric //
110b57cec5SDimitry Andric //===----------------------------------------------------------------------===//
120b57cec5SDimitry Andric 
130b57cec5SDimitry Andric #include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
140b57cec5SDimitry Andric #include "clang/AST/Type.h"
150b57cec5SDimitry Andric #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h"
160b57cec5SDimitry Andric #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
170b57cec5SDimitry Andric #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
180b57cec5SDimitry Andric #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
1981ad6265SDimitry Andric #include "llvm/ADT/ScopeExit.h"
200b57cec5SDimitry Andric 
210b57cec5SDimitry Andric using namespace clang;
220b57cec5SDimitry Andric using namespace ento;
230b57cec5SDimitry Andric 
240b57cec5SDimitry Andric ConstraintManager::~ConstraintManager() = default;
250b57cec5SDimitry Andric 
getLocFromSymbol(const ProgramStateRef & State,SymbolRef Sym)260b57cec5SDimitry Andric static DefinedSVal getLocFromSymbol(const ProgramStateRef &State,
270b57cec5SDimitry Andric                                     SymbolRef Sym) {
280b57cec5SDimitry Andric   const MemRegion *R =
290b57cec5SDimitry Andric       State->getStateManager().getRegionManager().getSymbolicRegion(Sym);
300b57cec5SDimitry Andric   return loc::MemRegionVal(R);
310b57cec5SDimitry Andric }
320b57cec5SDimitry Andric 
checkNull(ProgramStateRef State,SymbolRef Sym)330b57cec5SDimitry Andric ConditionTruthVal ConstraintManager::checkNull(ProgramStateRef State,
340b57cec5SDimitry Andric                                                SymbolRef Sym) {
350b57cec5SDimitry Andric   QualType Ty = Sym->getType();
360b57cec5SDimitry Andric   DefinedSVal V = Loc::isLocType(Ty) ? getLocFromSymbol(State, Sym)
370b57cec5SDimitry Andric                                      : nonloc::SymbolVal(Sym);
380b57cec5SDimitry Andric   const ProgramStatePair &P = assumeDual(State, V);
390b57cec5SDimitry Andric   if (P.first && !P.second)
400b57cec5SDimitry Andric     return ConditionTruthVal(false);
410b57cec5SDimitry Andric   if (!P.first && P.second)
420b57cec5SDimitry Andric     return ConditionTruthVal(true);
430b57cec5SDimitry Andric   return {};
440b57cec5SDimitry Andric }
4581ad6265SDimitry Andric 
4681ad6265SDimitry Andric template <typename AssumeFunction>
4781ad6265SDimitry Andric ConstraintManager::ProgramStatePair
assumeDualImpl(ProgramStateRef & State,AssumeFunction & Assume)4881ad6265SDimitry Andric ConstraintManager::assumeDualImpl(ProgramStateRef &State,
4981ad6265SDimitry Andric                                   AssumeFunction &Assume) {
5081ad6265SDimitry Andric   if (LLVM_UNLIKELY(State->isPosteriorlyOverconstrained()))
5181ad6265SDimitry Andric     return {State, State};
5281ad6265SDimitry Andric 
5381ad6265SDimitry Andric   // Assume functions might recurse (see `reAssume` or `tryRearrange`). During
5481ad6265SDimitry Andric   // the recursion the State might not change anymore, that means we reached a
5581ad6265SDimitry Andric   // fixpoint.
5681ad6265SDimitry Andric   // We avoid infinite recursion of assume calls by checking already visited
5781ad6265SDimitry Andric   // States on the stack of assume function calls.
5881ad6265SDimitry Andric   const ProgramState *RawSt = State.get();
5981ad6265SDimitry Andric   if (LLVM_UNLIKELY(AssumeStack.contains(RawSt)))
6081ad6265SDimitry Andric     return {State, State};
6181ad6265SDimitry Andric   AssumeStack.push(RawSt);
6281ad6265SDimitry Andric   auto AssumeStackBuilder =
6381ad6265SDimitry Andric       llvm::make_scope_exit([this]() { AssumeStack.pop(); });
6481ad6265SDimitry Andric 
6581ad6265SDimitry Andric   ProgramStateRef StTrue = Assume(true);
6681ad6265SDimitry Andric 
6781ad6265SDimitry Andric   if (!StTrue) {
6881ad6265SDimitry Andric     ProgramStateRef StFalse = Assume(false);
6981ad6265SDimitry Andric     if (LLVM_UNLIKELY(!StFalse)) { // both infeasible
7081ad6265SDimitry Andric       ProgramStateRef StInfeasible = State->cloneAsPosteriorlyOverconstrained();
7181ad6265SDimitry Andric       assert(StInfeasible->isPosteriorlyOverconstrained());
7281ad6265SDimitry Andric       // Checkers might rely on the API contract that both returned states
7381ad6265SDimitry Andric       // cannot be null. Thus, we return StInfeasible for both branches because
7481ad6265SDimitry Andric       // it might happen that a Checker uncoditionally uses one of them if the
7581ad6265SDimitry Andric       // other is a nullptr. This may also happen with the non-dual and
7681ad6265SDimitry Andric       // adjacent `assume(true)` and `assume(false)` calls. By implementing
7781ad6265SDimitry Andric       // assume in therms of assumeDual, we can keep our API contract there as
7881ad6265SDimitry Andric       // well.
7981ad6265SDimitry Andric       return ProgramStatePair(StInfeasible, StInfeasible);
8081ad6265SDimitry Andric     }
8181ad6265SDimitry Andric     return ProgramStatePair(nullptr, StFalse);
8281ad6265SDimitry Andric   }
8381ad6265SDimitry Andric 
8481ad6265SDimitry Andric   ProgramStateRef StFalse = Assume(false);
8581ad6265SDimitry Andric   if (!StFalse) {
8681ad6265SDimitry Andric     return ProgramStatePair(StTrue, nullptr);
8781ad6265SDimitry Andric   }
8881ad6265SDimitry Andric 
8981ad6265SDimitry Andric   return ProgramStatePair(StTrue, StFalse);
9081ad6265SDimitry Andric }
9181ad6265SDimitry Andric 
9281ad6265SDimitry Andric ConstraintManager::ProgramStatePair
assumeDual(ProgramStateRef State,DefinedSVal Cond)9381ad6265SDimitry Andric ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) {
94*5f757f3fSDimitry Andric   auto AssumeFun = [&, Cond](bool Assumption) {
9581ad6265SDimitry Andric     return assumeInternal(State, Cond, Assumption);
9681ad6265SDimitry Andric   };
9781ad6265SDimitry Andric   return assumeDualImpl(State, AssumeFun);
9881ad6265SDimitry Andric }
9981ad6265SDimitry Andric 
10081ad6265SDimitry Andric ConstraintManager::ProgramStatePair
assumeInclusiveRangeDual(ProgramStateRef State,NonLoc Value,const llvm::APSInt & From,const llvm::APSInt & To)10181ad6265SDimitry Andric ConstraintManager::assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value,
10281ad6265SDimitry Andric                                             const llvm::APSInt &From,
10381ad6265SDimitry Andric                                             const llvm::APSInt &To) {
10481ad6265SDimitry Andric   auto AssumeFun = [&](bool Assumption) {
10581ad6265SDimitry Andric     return assumeInclusiveRangeInternal(State, Value, From, To, Assumption);
10681ad6265SDimitry Andric   };
10781ad6265SDimitry Andric   return assumeDualImpl(State, AssumeFun);
10881ad6265SDimitry Andric }
10981ad6265SDimitry Andric 
assume(ProgramStateRef State,DefinedSVal Cond,bool Assumption)11081ad6265SDimitry Andric ProgramStateRef ConstraintManager::assume(ProgramStateRef State,
11181ad6265SDimitry Andric                                           DefinedSVal Cond, bool Assumption) {
11281ad6265SDimitry Andric   ConstraintManager::ProgramStatePair R = assumeDual(State, Cond);
11381ad6265SDimitry Andric   return Assumption ? R.first : R.second;
11481ad6265SDimitry Andric }
11581ad6265SDimitry Andric 
11681ad6265SDimitry Andric ProgramStateRef
assumeInclusiveRange(ProgramStateRef State,NonLoc Value,const llvm::APSInt & From,const llvm::APSInt & To,bool InBound)11781ad6265SDimitry Andric ConstraintManager::assumeInclusiveRange(ProgramStateRef State, NonLoc Value,
11881ad6265SDimitry Andric                                         const llvm::APSInt &From,
11981ad6265SDimitry Andric                                         const llvm::APSInt &To, bool InBound) {
12081ad6265SDimitry Andric   ConstraintManager::ProgramStatePair R =
12181ad6265SDimitry Andric       assumeInclusiveRangeDual(State, Value, From, To);
12281ad6265SDimitry Andric   return InBound ? R.first : R.second;
12381ad6265SDimitry Andric }
124