1e5dd7070Spatrick //===- ConstraintManager.cpp - Constraints on symbolic values. ------------===//
2e5dd7070Spatrick //
3e5dd7070Spatrick // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4e5dd7070Spatrick // See https://llvm.org/LICENSE.txt for license information.
5e5dd7070Spatrick // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6e5dd7070Spatrick //
7e5dd7070Spatrick //===----------------------------------------------------------------------===//
8e5dd7070Spatrick //
9e5dd7070Spatrick // This file defined the interface to manage constraints on symbolic values.
10e5dd7070Spatrick //
11e5dd7070Spatrick //===----------------------------------------------------------------------===//
12e5dd7070Spatrick
13e5dd7070Spatrick #include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
14e5dd7070Spatrick #include "clang/AST/Type.h"
15e5dd7070Spatrick #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h"
16e5dd7070Spatrick #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
17e5dd7070Spatrick #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
18e5dd7070Spatrick #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
19*12c85518Srobert #include "llvm/ADT/ScopeExit.h"
20e5dd7070Spatrick
21e5dd7070Spatrick using namespace clang;
22e5dd7070Spatrick using namespace ento;
23e5dd7070Spatrick
24e5dd7070Spatrick ConstraintManager::~ConstraintManager() = default;
25e5dd7070Spatrick
getLocFromSymbol(const ProgramStateRef & State,SymbolRef Sym)26e5dd7070Spatrick static DefinedSVal getLocFromSymbol(const ProgramStateRef &State,
27e5dd7070Spatrick SymbolRef Sym) {
28e5dd7070Spatrick const MemRegion *R =
29e5dd7070Spatrick State->getStateManager().getRegionManager().getSymbolicRegion(Sym);
30e5dd7070Spatrick return loc::MemRegionVal(R);
31e5dd7070Spatrick }
32e5dd7070Spatrick
checkNull(ProgramStateRef State,SymbolRef Sym)33e5dd7070Spatrick ConditionTruthVal ConstraintManager::checkNull(ProgramStateRef State,
34e5dd7070Spatrick SymbolRef Sym) {
35e5dd7070Spatrick QualType Ty = Sym->getType();
36e5dd7070Spatrick DefinedSVal V = Loc::isLocType(Ty) ? getLocFromSymbol(State, Sym)
37e5dd7070Spatrick : nonloc::SymbolVal(Sym);
38e5dd7070Spatrick const ProgramStatePair &P = assumeDual(State, V);
39e5dd7070Spatrick if (P.first && !P.second)
40e5dd7070Spatrick return ConditionTruthVal(false);
41e5dd7070Spatrick if (!P.first && P.second)
42e5dd7070Spatrick return ConditionTruthVal(true);
43e5dd7070Spatrick return {};
44e5dd7070Spatrick }
45*12c85518Srobert
46*12c85518Srobert template <typename AssumeFunction>
47*12c85518Srobert ConstraintManager::ProgramStatePair
assumeDualImpl(ProgramStateRef & State,AssumeFunction & Assume)48*12c85518Srobert ConstraintManager::assumeDualImpl(ProgramStateRef &State,
49*12c85518Srobert AssumeFunction &Assume) {
50*12c85518Srobert if (LLVM_UNLIKELY(State->isPosteriorlyOverconstrained()))
51*12c85518Srobert return {State, State};
52*12c85518Srobert
53*12c85518Srobert // Assume functions might recurse (see `reAssume` or `tryRearrange`). During
54*12c85518Srobert // the recursion the State might not change anymore, that means we reached a
55*12c85518Srobert // fixpoint.
56*12c85518Srobert // We avoid infinite recursion of assume calls by checking already visited
57*12c85518Srobert // States on the stack of assume function calls.
58*12c85518Srobert const ProgramState *RawSt = State.get();
59*12c85518Srobert if (LLVM_UNLIKELY(AssumeStack.contains(RawSt)))
60*12c85518Srobert return {State, State};
61*12c85518Srobert AssumeStack.push(RawSt);
62*12c85518Srobert auto AssumeStackBuilder =
63*12c85518Srobert llvm::make_scope_exit([this]() { AssumeStack.pop(); });
64*12c85518Srobert
65*12c85518Srobert ProgramStateRef StTrue = Assume(true);
66*12c85518Srobert
67*12c85518Srobert if (!StTrue) {
68*12c85518Srobert ProgramStateRef StFalse = Assume(false);
69*12c85518Srobert if (LLVM_UNLIKELY(!StFalse)) { // both infeasible
70*12c85518Srobert ProgramStateRef StInfeasible = State->cloneAsPosteriorlyOverconstrained();
71*12c85518Srobert assert(StInfeasible->isPosteriorlyOverconstrained());
72*12c85518Srobert // Checkers might rely on the API contract that both returned states
73*12c85518Srobert // cannot be null. Thus, we return StInfeasible for both branches because
74*12c85518Srobert // it might happen that a Checker uncoditionally uses one of them if the
75*12c85518Srobert // other is a nullptr. This may also happen with the non-dual and
76*12c85518Srobert // adjacent `assume(true)` and `assume(false)` calls. By implementing
77*12c85518Srobert // assume in therms of assumeDual, we can keep our API contract there as
78*12c85518Srobert // well.
79*12c85518Srobert return ProgramStatePair(StInfeasible, StInfeasible);
80*12c85518Srobert }
81*12c85518Srobert return ProgramStatePair(nullptr, StFalse);
82*12c85518Srobert }
83*12c85518Srobert
84*12c85518Srobert ProgramStateRef StFalse = Assume(false);
85*12c85518Srobert if (!StFalse) {
86*12c85518Srobert return ProgramStatePair(StTrue, nullptr);
87*12c85518Srobert }
88*12c85518Srobert
89*12c85518Srobert return ProgramStatePair(StTrue, StFalse);
90*12c85518Srobert }
91*12c85518Srobert
92*12c85518Srobert ConstraintManager::ProgramStatePair
assumeDual(ProgramStateRef State,DefinedSVal Cond)93*12c85518Srobert ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) {
94*12c85518Srobert auto AssumeFun = [&](bool Assumption) {
95*12c85518Srobert return assumeInternal(State, Cond, Assumption);
96*12c85518Srobert };
97*12c85518Srobert return assumeDualImpl(State, AssumeFun);
98*12c85518Srobert }
99*12c85518Srobert
100*12c85518Srobert ConstraintManager::ProgramStatePair
assumeInclusiveRangeDual(ProgramStateRef State,NonLoc Value,const llvm::APSInt & From,const llvm::APSInt & To)101*12c85518Srobert ConstraintManager::assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value,
102*12c85518Srobert const llvm::APSInt &From,
103*12c85518Srobert const llvm::APSInt &To) {
104*12c85518Srobert auto AssumeFun = [&](bool Assumption) {
105*12c85518Srobert return assumeInclusiveRangeInternal(State, Value, From, To, Assumption);
106*12c85518Srobert };
107*12c85518Srobert return assumeDualImpl(State, AssumeFun);
108*12c85518Srobert }
109*12c85518Srobert
assume(ProgramStateRef State,DefinedSVal Cond,bool Assumption)110*12c85518Srobert ProgramStateRef ConstraintManager::assume(ProgramStateRef State,
111*12c85518Srobert DefinedSVal Cond, bool Assumption) {
112*12c85518Srobert ConstraintManager::ProgramStatePair R = assumeDual(State, Cond);
113*12c85518Srobert return Assumption ? R.first : R.second;
114*12c85518Srobert }
115*12c85518Srobert
116*12c85518Srobert ProgramStateRef
assumeInclusiveRange(ProgramStateRef State,NonLoc Value,const llvm::APSInt & From,const llvm::APSInt & To,bool InBound)117*12c85518Srobert ConstraintManager::assumeInclusiveRange(ProgramStateRef State, NonLoc Value,
118*12c85518Srobert const llvm::APSInt &From,
119*12c85518Srobert const llvm::APSInt &To, bool InBound) {
120*12c85518Srobert ConstraintManager::ProgramStatePair R =
121*12c85518Srobert assumeInclusiveRangeDual(State, Value, From, To);
122*12c85518Srobert return InBound ? R.first : R.second;
123*12c85518Srobert }
124