10b57cec5SDimitry Andric //== SimpleConstraintManager.cpp --------------------------------*- C++ -*--==//
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 defines SimpleConstraintManager, a class that provides a
100b57cec5SDimitry Andric // simplified constraint manager interface, compared to ConstraintManager.
110b57cec5SDimitry Andric //
120b57cec5SDimitry Andric //===----------------------------------------------------------------------===//
130b57cec5SDimitry Andric
140b57cec5SDimitry Andric #include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
150b57cec5SDimitry Andric #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
160b57cec5SDimitry Andric #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
170b57cec5SDimitry Andric #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
180b57cec5SDimitry Andric
190b57cec5SDimitry Andric namespace clang {
200b57cec5SDimitry Andric
210b57cec5SDimitry Andric namespace ento {
220b57cec5SDimitry Andric
~SimpleConstraintManager()230b57cec5SDimitry Andric SimpleConstraintManager::~SimpleConstraintManager() {}
240b57cec5SDimitry Andric
assume(ProgramStateRef State,DefinedSVal Cond,bool Assumption)250b57cec5SDimitry Andric ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef State,
260b57cec5SDimitry Andric DefinedSVal Cond,
270b57cec5SDimitry Andric bool Assumption) {
280b57cec5SDimitry Andric // If we have a Loc value, cast it to a bool NonLoc first.
290b57cec5SDimitry Andric if (Optional<Loc> LV = Cond.getAs<Loc>()) {
300b57cec5SDimitry Andric SValBuilder &SVB = State->getStateManager().getSValBuilder();
310b57cec5SDimitry Andric QualType T;
320b57cec5SDimitry Andric const MemRegion *MR = LV->getAsRegion();
330b57cec5SDimitry Andric if (const TypedRegion *TR = dyn_cast_or_null<TypedRegion>(MR))
340b57cec5SDimitry Andric T = TR->getLocationType();
350b57cec5SDimitry Andric else
360b57cec5SDimitry Andric T = SVB.getContext().VoidPtrTy;
370b57cec5SDimitry Andric
380b57cec5SDimitry Andric Cond = SVB.evalCast(*LV, SVB.getContext().BoolTy, T).castAs<DefinedSVal>();
390b57cec5SDimitry Andric }
400b57cec5SDimitry Andric
410b57cec5SDimitry Andric return assume(State, Cond.castAs<NonLoc>(), Assumption);
420b57cec5SDimitry Andric }
430b57cec5SDimitry Andric
assume(ProgramStateRef State,NonLoc Cond,bool Assumption)440b57cec5SDimitry Andric ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef State,
450b57cec5SDimitry Andric NonLoc Cond, bool Assumption) {
460b57cec5SDimitry Andric State = assumeAux(State, Cond, Assumption);
475ffd83dbSDimitry Andric if (NotifyAssumeClients && EE)
485ffd83dbSDimitry Andric return EE->processAssume(State, Cond, Assumption);
490b57cec5SDimitry Andric return State;
500b57cec5SDimitry Andric }
510b57cec5SDimitry Andric
assumeAux(ProgramStateRef State,NonLoc Cond,bool Assumption)520b57cec5SDimitry Andric ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State,
530b57cec5SDimitry Andric NonLoc Cond,
540b57cec5SDimitry Andric bool Assumption) {
550b57cec5SDimitry Andric
560b57cec5SDimitry Andric // We cannot reason about SymSymExprs, and can only reason about some
570b57cec5SDimitry Andric // SymIntExprs.
580b57cec5SDimitry Andric if (!canReasonAbout(Cond)) {
590b57cec5SDimitry Andric // Just add the constraint to the expression without trying to simplify.
60*af732203SDimitry Andric SymbolRef Sym = Cond.getAsSymbol();
610b57cec5SDimitry Andric assert(Sym);
620b57cec5SDimitry Andric return assumeSymUnsupported(State, Sym, Assumption);
630b57cec5SDimitry Andric }
640b57cec5SDimitry Andric
650b57cec5SDimitry Andric switch (Cond.getSubKind()) {
660b57cec5SDimitry Andric default:
670b57cec5SDimitry Andric llvm_unreachable("'Assume' not implemented for this NonLoc");
680b57cec5SDimitry Andric
690b57cec5SDimitry Andric case nonloc::SymbolValKind: {
700b57cec5SDimitry Andric nonloc::SymbolVal SV = Cond.castAs<nonloc::SymbolVal>();
710b57cec5SDimitry Andric SymbolRef Sym = SV.getSymbol();
720b57cec5SDimitry Andric assert(Sym);
730b57cec5SDimitry Andric return assumeSym(State, Sym, Assumption);
740b57cec5SDimitry Andric }
750b57cec5SDimitry Andric
760b57cec5SDimitry Andric case nonloc::ConcreteIntKind: {
770b57cec5SDimitry Andric bool b = Cond.castAs<nonloc::ConcreteInt>().getValue() != 0;
780b57cec5SDimitry Andric bool isFeasible = b ? Assumption : !Assumption;
790b57cec5SDimitry Andric return isFeasible ? State : nullptr;
800b57cec5SDimitry Andric }
810b57cec5SDimitry Andric
820b57cec5SDimitry Andric case nonloc::PointerToMemberKind: {
830b57cec5SDimitry Andric bool IsNull = !Cond.castAs<nonloc::PointerToMember>().isNullMemberPointer();
840b57cec5SDimitry Andric bool IsFeasible = IsNull ? Assumption : !Assumption;
850b57cec5SDimitry Andric return IsFeasible ? State : nullptr;
860b57cec5SDimitry Andric }
870b57cec5SDimitry Andric
880b57cec5SDimitry Andric case nonloc::LocAsIntegerKind:
890b57cec5SDimitry Andric return assume(State, Cond.castAs<nonloc::LocAsInteger>().getLoc(),
900b57cec5SDimitry Andric Assumption);
910b57cec5SDimitry Andric } // end switch
920b57cec5SDimitry Andric }
930b57cec5SDimitry Andric
assumeInclusiveRange(ProgramStateRef State,NonLoc Value,const llvm::APSInt & From,const llvm::APSInt & To,bool InRange)940b57cec5SDimitry Andric ProgramStateRef SimpleConstraintManager::assumeInclusiveRange(
950b57cec5SDimitry Andric ProgramStateRef State, NonLoc Value, const llvm::APSInt &From,
960b57cec5SDimitry Andric const llvm::APSInt &To, bool InRange) {
970b57cec5SDimitry Andric
980b57cec5SDimitry Andric assert(From.isUnsigned() == To.isUnsigned() &&
990b57cec5SDimitry Andric From.getBitWidth() == To.getBitWidth() &&
1000b57cec5SDimitry Andric "Values should have same types!");
1010b57cec5SDimitry Andric
1020b57cec5SDimitry Andric if (!canReasonAbout(Value)) {
1030b57cec5SDimitry Andric // Just add the constraint to the expression without trying to simplify.
104*af732203SDimitry Andric SymbolRef Sym = Value.getAsSymbol();
1050b57cec5SDimitry Andric assert(Sym);
1060b57cec5SDimitry Andric return assumeSymInclusiveRange(State, Sym, From, To, InRange);
1070b57cec5SDimitry Andric }
1080b57cec5SDimitry Andric
1090b57cec5SDimitry Andric switch (Value.getSubKind()) {
1100b57cec5SDimitry Andric default:
1110b57cec5SDimitry Andric llvm_unreachable("'assumeInclusiveRange' is not implemented"
1120b57cec5SDimitry Andric "for this NonLoc");
1130b57cec5SDimitry Andric
1140b57cec5SDimitry Andric case nonloc::LocAsIntegerKind:
1150b57cec5SDimitry Andric case nonloc::SymbolValKind: {
1160b57cec5SDimitry Andric if (SymbolRef Sym = Value.getAsSymbol())
1170b57cec5SDimitry Andric return assumeSymInclusiveRange(State, Sym, From, To, InRange);
1180b57cec5SDimitry Andric return State;
1190b57cec5SDimitry Andric } // end switch
1200b57cec5SDimitry Andric
1210b57cec5SDimitry Andric case nonloc::ConcreteIntKind: {
1220b57cec5SDimitry Andric const llvm::APSInt &IntVal = Value.castAs<nonloc::ConcreteInt>().getValue();
1230b57cec5SDimitry Andric bool IsInRange = IntVal >= From && IntVal <= To;
1240b57cec5SDimitry Andric bool isFeasible = (IsInRange == InRange);
1250b57cec5SDimitry Andric return isFeasible ? State : nullptr;
1260b57cec5SDimitry Andric }
1270b57cec5SDimitry Andric } // end switch
1280b57cec5SDimitry Andric }
1290b57cec5SDimitry Andric
1300b57cec5SDimitry Andric } // end of namespace ento
1310b57cec5SDimitry Andric
1320b57cec5SDimitry Andric } // end of namespace clang
133