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