1fa0734ecSArgyrios Kyrtzidis //== SimpleConstraintManager.cpp --------------------------------*- C++ -*--==//
2fa0734ecSArgyrios Kyrtzidis //
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
6fa0734ecSArgyrios Kyrtzidis //
7fa0734ecSArgyrios Kyrtzidis //===----------------------------------------------------------------------===//
8fa0734ecSArgyrios Kyrtzidis //
99bc02ceeSDominic Chen // This file defines SimpleConstraintManager, a class that provides a
109bc02ceeSDominic Chen // simplified constraint manager interface, compared to ConstraintManager.
11fa0734ecSArgyrios Kyrtzidis //
12fa0734ecSArgyrios Kyrtzidis //===----------------------------------------------------------------------===//
13fa0734ecSArgyrios Kyrtzidis
149bc02ceeSDominic Chen #include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
15728be7f6SJordy Rose #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
16f8cbac4bSTed Kremenek #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
17001fd5b4STed Kremenek #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
18fa0734ecSArgyrios Kyrtzidis
19fa0734ecSArgyrios Kyrtzidis namespace clang {
20fa0734ecSArgyrios Kyrtzidis
21fa0734ecSArgyrios Kyrtzidis namespace ento {
22fa0734ecSArgyrios Kyrtzidis
~SimpleConstraintManager()23637d1e66SAngel Garcia Gomez SimpleConstraintManager::~SimpleConstraintManager() {}
24fa0734ecSArgyrios Kyrtzidis
assumeInternal(ProgramStateRef State,DefinedSVal Cond,bool Assumption)251c1c1e25SGabor Marton ProgramStateRef SimpleConstraintManager::assumeInternal(ProgramStateRef State,
26fa0734ecSArgyrios Kyrtzidis DefinedSVal Cond,
27fa0734ecSArgyrios Kyrtzidis bool Assumption) {
28acd080b9SJordan Rose // If we have a Loc value, cast it to a bool NonLoc first.
29acd080b9SJordan Rose if (Optional<Loc> LV = Cond.getAs<Loc>()) {
30c7772addSDominic Chen SValBuilder &SVB = State->getStateManager().getSValBuilder();
31acd080b9SJordan Rose QualType T;
32acd080b9SJordan Rose const MemRegion *MR = LV->getAsRegion();
33acd080b9SJordan Rose if (const TypedRegion *TR = dyn_cast_or_null<TypedRegion>(MR))
34acd080b9SJordan Rose T = TR->getLocationType();
35326702f1STed Kremenek else
36acd080b9SJordan Rose T = SVB.getContext().VoidPtrTy;
37acd080b9SJordan Rose
38acd080b9SJordan Rose Cond = SVB.evalCast(*LV, SVB.getContext().BoolTy, T).castAs<DefinedSVal>();
39326702f1STed Kremenek }
40fa0734ecSArgyrios Kyrtzidis
41c7772addSDominic Chen return assume(State, Cond.castAs<NonLoc>(), Assumption);
42fa0734ecSArgyrios Kyrtzidis }
43fa0734ecSArgyrios Kyrtzidis
assume(ProgramStateRef State,NonLoc Cond,bool Assumption)44c7772addSDominic Chen ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef State,
45c7772addSDominic Chen NonLoc Cond, bool Assumption) {
46c7772addSDominic Chen State = assumeAux(State, Cond, Assumption);
47*8131ee4cSGabor Marton if (EE)
48d70ec366SAdam Balogh return EE->processAssume(State, Cond, Assumption);
49c7772addSDominic Chen return State;
50fa0734ecSArgyrios Kyrtzidis }
51fa0734ecSArgyrios Kyrtzidis
assumeAux(ProgramStateRef State,NonLoc Cond,bool Assumption)52c7772addSDominic Chen ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State,
53fa0734ecSArgyrios Kyrtzidis NonLoc Cond,
54fa0734ecSArgyrios Kyrtzidis bool Assumption) {
55fa0734ecSArgyrios Kyrtzidis
5651090d5fSAnna Zaks // We cannot reason about SymSymExprs, and can only reason about some
5751090d5fSAnna Zaks // SymIntExprs.
58fa0734ecSArgyrios Kyrtzidis if (!canReasonAbout(Cond)) {
5951090d5fSAnna Zaks // Just add the constraint to the expression without trying to simplify.
6086e1b735SDenys Petrov SymbolRef Sym = Cond.getAsSymbol();
619bc02ceeSDominic Chen assert(Sym);
629bc02ceeSDominic Chen return assumeSymUnsupported(State, Sym, Assumption);
63fa0734ecSArgyrios Kyrtzidis }
64fa0734ecSArgyrios Kyrtzidis
65fa0734ecSArgyrios Kyrtzidis switch (Cond.getSubKind()) {
66fa0734ecSArgyrios Kyrtzidis default:
6783d382b1SDavid Blaikie llvm_unreachable("'Assume' not implemented for this NonLoc");
68fa0734ecSArgyrios Kyrtzidis
69fa0734ecSArgyrios Kyrtzidis case nonloc::SymbolValKind: {
702fdacbc5SDavid Blaikie nonloc::SymbolVal SV = Cond.castAs<nonloc::SymbolVal>();
71c7772addSDominic Chen SymbolRef Sym = SV.getSymbol();
72c7772addSDominic Chen assert(Sym);
739bc02ceeSDominic Chen return assumeSym(State, Sym, Assumption);
74d066f79cSAnna Zaks }
75fa0734ecSArgyrios Kyrtzidis
76fa0734ecSArgyrios Kyrtzidis case nonloc::ConcreteIntKind: {
772fdacbc5SDavid Blaikie bool b = Cond.castAs<nonloc::ConcreteInt>().getValue() != 0;
78fa0734ecSArgyrios Kyrtzidis bool isFeasible = b ? Assumption : !Assumption;
79c7772addSDominic Chen return isFeasible ? State : nullptr;
80fa0734ecSArgyrios Kyrtzidis }
81fa0734ecSArgyrios Kyrtzidis
8264c01f7bSDevin Coughlin case nonloc::PointerToMemberKind: {
8364c01f7bSDevin Coughlin bool IsNull = !Cond.castAs<nonloc::PointerToMember>().isNullMemberPointer();
8464c01f7bSDevin Coughlin bool IsFeasible = IsNull ? Assumption : !Assumption;
8564c01f7bSDevin Coughlin return IsFeasible ? State : nullptr;
8664c01f7bSDevin Coughlin }
8764c01f7bSDevin Coughlin
88fa0734ecSArgyrios Kyrtzidis case nonloc::LocAsIntegerKind:
891c1c1e25SGabor Marton return assumeInternal(State, Cond.castAs<nonloc::LocAsInteger>().getLoc(),
90fa0734ecSArgyrios Kyrtzidis Assumption);
91fa0734ecSArgyrios Kyrtzidis } // end switch
92fa0734ecSArgyrios Kyrtzidis }
93fa0734ecSArgyrios Kyrtzidis
assumeInclusiveRangeInternal(ProgramStateRef State,NonLoc Value,const llvm::APSInt & From,const llvm::APSInt & To,bool InRange)9432f189b0SGabor Marton ProgramStateRef SimpleConstraintManager::assumeInclusiveRangeInternal(
95eb538abfSDevin Coughlin ProgramStateRef State, NonLoc Value, const llvm::APSInt &From,
96eb538abfSDevin Coughlin const llvm::APSInt &To, bool InRange) {
97eb538abfSDevin Coughlin
98eb538abfSDevin Coughlin assert(From.isUnsigned() == To.isUnsigned() &&
99eb538abfSDevin Coughlin From.getBitWidth() == To.getBitWidth() &&
100eb538abfSDevin Coughlin "Values should have same types!");
101eb538abfSDevin Coughlin
102eb538abfSDevin Coughlin if (!canReasonAbout(Value)) {
103eb538abfSDevin Coughlin // Just add the constraint to the expression without trying to simplify.
10486e1b735SDenys Petrov SymbolRef Sym = Value.getAsSymbol();
105eb538abfSDevin Coughlin assert(Sym);
1069bc02ceeSDominic Chen return assumeSymInclusiveRange(State, Sym, From, To, InRange);
107eb538abfSDevin Coughlin }
108eb538abfSDevin Coughlin
109eb538abfSDevin Coughlin switch (Value.getSubKind()) {
110eb538abfSDevin Coughlin default:
1113f8c3fa7SDominic Chen llvm_unreachable("'assumeInclusiveRange' is not implemented"
112eb538abfSDevin Coughlin "for this NonLoc");
113eb538abfSDevin Coughlin
114eb538abfSDevin Coughlin case nonloc::LocAsIntegerKind:
115eb538abfSDevin Coughlin case nonloc::SymbolValKind: {
116eb538abfSDevin Coughlin if (SymbolRef Sym = Value.getAsSymbol())
1179bc02ceeSDominic Chen return assumeSymInclusiveRange(State, Sym, From, To, InRange);
118eb538abfSDevin Coughlin return State;
119eb538abfSDevin Coughlin } // end switch
120eb538abfSDevin Coughlin
121eb538abfSDevin Coughlin case nonloc::ConcreteIntKind: {
122eb538abfSDevin Coughlin const llvm::APSInt &IntVal = Value.castAs<nonloc::ConcreteInt>().getValue();
123eb538abfSDevin Coughlin bool IsInRange = IntVal >= From && IntVal <= To;
124eb538abfSDevin Coughlin bool isFeasible = (IsInRange == InRange);
125eb538abfSDevin Coughlin return isFeasible ? State : nullptr;
126eb538abfSDevin Coughlin }
127eb538abfSDevin Coughlin } // end switch
128eb538abfSDevin Coughlin }
129eb538abfSDevin Coughlin
130fa0734ecSArgyrios Kyrtzidis } // end of namespace ento
131fa0734ecSArgyrios Kyrtzidis
132fa0734ecSArgyrios Kyrtzidis } // end of namespace clang
133