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