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