1657ac148SPeter Szecsi //===--- LoopUnrolling.cpp - Unroll loops -----------------------*- C++ -*-===//
2657ac148SPeter Szecsi //
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
6657ac148SPeter Szecsi //
7657ac148SPeter Szecsi //===----------------------------------------------------------------------===//
8657ac148SPeter Szecsi ///
9657ac148SPeter Szecsi /// This file contains functions which are used to decide if a loop worth to be
103c3e1b0bSPeter Szecsi /// unrolled. Moreover, these functions manages the stack of loop which is
113c3e1b0bSPeter Szecsi /// tracked by the ProgramState.
12657ac148SPeter Szecsi ///
13657ac148SPeter Szecsi //===----------------------------------------------------------------------===//
14657ac148SPeter Szecsi 
15657ac148SPeter Szecsi #include "clang/ASTMatchers/ASTMatchers.h"
16657ac148SPeter Szecsi #include "clang/ASTMatchers/ASTMatchFinder.h"
17657ac148SPeter Szecsi #include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h"
18657ac148SPeter Szecsi #include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"
19657ac148SPeter Szecsi #include "clang/StaticAnalyzer/Core/PathSensitive/LoopUnrolling.h"
20657ac148SPeter Szecsi 
21657ac148SPeter Szecsi using namespace clang;
22657ac148SPeter Szecsi using namespace ento;
23657ac148SPeter Szecsi using namespace clang::ast_matchers;
24657ac148SPeter Szecsi 
250db84863SPeter Szecsi static const int MAXIMUM_STEP_UNROLLED = 128;
260db84863SPeter Szecsi 
273c3e1b0bSPeter Szecsi struct LoopState {
283c3e1b0bSPeter Szecsi private:
293c3e1b0bSPeter Szecsi   enum Kind { Normal, Unrolled } K;
303c3e1b0bSPeter Szecsi   const Stmt *LoopStmt;
313c3e1b0bSPeter Szecsi   const LocationContext *LCtx;
320db84863SPeter Szecsi   unsigned maxStep;
LoopStateLoopState330db84863SPeter Szecsi   LoopState(Kind InK, const Stmt *S, const LocationContext *L, unsigned N)
340db84863SPeter Szecsi       : K(InK), LoopStmt(S), LCtx(L), maxStep(N) {}
35657ac148SPeter Szecsi 
363c3e1b0bSPeter Szecsi public:
getNormalLoopState370db84863SPeter Szecsi   static LoopState getNormal(const Stmt *S, const LocationContext *L,
380db84863SPeter Szecsi                              unsigned N) {
390db84863SPeter Szecsi     return LoopState(Normal, S, L, N);
403c3e1b0bSPeter Szecsi   }
getUnrolledLoopState410db84863SPeter Szecsi   static LoopState getUnrolled(const Stmt *S, const LocationContext *L,
420db84863SPeter Szecsi                                unsigned N) {
430db84863SPeter Szecsi     return LoopState(Unrolled, S, L, N);
443c3e1b0bSPeter Szecsi   }
isUnrolledLoopState453c3e1b0bSPeter Szecsi   bool isUnrolled() const { return K == Unrolled; }
getMaxStepLoopState460db84863SPeter Szecsi   unsigned getMaxStep() const { return maxStep; }
getLoopStmtLoopState473c3e1b0bSPeter Szecsi   const Stmt *getLoopStmt() const { return LoopStmt; }
getLocationContextLoopState483c3e1b0bSPeter Szecsi   const LocationContext *getLocationContext() const { return LCtx; }
operator ==LoopState493c3e1b0bSPeter Szecsi   bool operator==(const LoopState &X) const {
503c3e1b0bSPeter Szecsi     return K == X.K && LoopStmt == X.LoopStmt;
513c3e1b0bSPeter Szecsi   }
ProfileLoopState523c3e1b0bSPeter Szecsi   void Profile(llvm::FoldingSetNodeID &ID) const {
533c3e1b0bSPeter Szecsi     ID.AddInteger(K);
543c3e1b0bSPeter Szecsi     ID.AddPointer(LoopStmt);
553c3e1b0bSPeter Szecsi     ID.AddPointer(LCtx);
560db84863SPeter Szecsi     ID.AddInteger(maxStep);
573c3e1b0bSPeter Szecsi   }
583c3e1b0bSPeter Szecsi };
59657ac148SPeter Szecsi 
603c3e1b0bSPeter Szecsi // The tracked stack of loops. The stack indicates that which loops the
613c3e1b0bSPeter Szecsi // simulated element contained by. The loops are marked depending if we decided
623c3e1b0bSPeter Szecsi // to unroll them.
633c3e1b0bSPeter Szecsi // TODO: The loop stack should not need to be in the program state since it is
643c3e1b0bSPeter Szecsi // lexical in nature. Instead, the stack of loops should be tracked in the
653c3e1b0bSPeter Szecsi // LocationContext.
663c3e1b0bSPeter Szecsi REGISTER_LIST_WITH_PROGRAMSTATE(LoopStack, LoopState)
67657ac148SPeter Szecsi 
68657ac148SPeter Szecsi namespace clang {
69657ac148SPeter Szecsi namespace ento {
70657ac148SPeter Szecsi 
isLoopStmt(const Stmt * S)71657ac148SPeter Szecsi static bool isLoopStmt(const Stmt *S) {
7216be17adSBalazs Benics   return isa_and_nonnull<ForStmt, WhileStmt, DoStmt>(S);
73657ac148SPeter Szecsi }
74657ac148SPeter Szecsi 
processLoopEnd(const Stmt * LoopStmt,ProgramStateRef State)753c3e1b0bSPeter Szecsi ProgramStateRef processLoopEnd(const Stmt *LoopStmt, ProgramStateRef State) {
763c3e1b0bSPeter Szecsi   auto LS = State->get<LoopStack>();
77d91554bcSPeter Szecsi   if (!LS.isEmpty() && LS.getHead().getLoopStmt() == LoopStmt)
783c3e1b0bSPeter Szecsi     State = State->set<LoopStack>(LS.getTail());
793c3e1b0bSPeter Szecsi   return State;
803c3e1b0bSPeter Szecsi }
813c3e1b0bSPeter Szecsi 
simpleCondition(StringRef BindName,StringRef RefName)821af97c9dSAbbas Sabra static internal::Matcher<Stmt> simpleCondition(StringRef BindName,
831af97c9dSAbbas Sabra                                                StringRef RefName) {
841af97c9dSAbbas Sabra   return binaryOperator(
851af97c9dSAbbas Sabra              anyOf(hasOperatorName("<"), hasOperatorName(">"),
860db84863SPeter Szecsi                    hasOperatorName("<="), hasOperatorName(">="),
870db84863SPeter Szecsi                    hasOperatorName("!=")),
88657ac148SPeter Szecsi              hasEitherOperand(ignoringParenImpCasts(
891af97c9dSAbbas Sabra                  declRefExpr(to(varDecl(hasType(isInteger())).bind(BindName)))
901af97c9dSAbbas Sabra                      .bind(RefName))),
911af97c9dSAbbas Sabra              hasEitherOperand(
921af97c9dSAbbas Sabra                  ignoringParenImpCasts(integerLiteral().bind("boundNum"))))
930db84863SPeter Szecsi       .bind("conditionOperator");
94657ac148SPeter Szecsi }
95657ac148SPeter Szecsi 
968de103f2SPeter Szecsi static internal::Matcher<Stmt>
changeIntBoundNode(internal::Matcher<Decl> VarNodeMatcher)978de103f2SPeter Szecsi changeIntBoundNode(internal::Matcher<Decl> VarNodeMatcher) {
988de103f2SPeter Szecsi   return anyOf(
998de103f2SPeter Szecsi       unaryOperator(anyOf(hasOperatorName("--"), hasOperatorName("++")),
100657ac148SPeter Szecsi                     hasUnaryOperand(ignoringParenImpCasts(
1018de103f2SPeter Szecsi                         declRefExpr(to(varDecl(VarNodeMatcher)))))),
1024c87d233SPeter Szecsi       binaryOperator(isAssignmentOperator(),
103657ac148SPeter Szecsi                      hasLHS(ignoringParenImpCasts(
1048de103f2SPeter Szecsi                          declRefExpr(to(varDecl(VarNodeMatcher)))))));
105657ac148SPeter Szecsi }
106657ac148SPeter Szecsi 
1078de103f2SPeter Szecsi static internal::Matcher<Stmt>
callByRef(internal::Matcher<Decl> VarNodeMatcher)1088de103f2SPeter Szecsi callByRef(internal::Matcher<Decl> VarNodeMatcher) {
1098de103f2SPeter Szecsi   return callExpr(forEachArgumentWithParam(
1108de103f2SPeter Szecsi       declRefExpr(to(varDecl(VarNodeMatcher))),
1118de103f2SPeter Szecsi       parmVarDecl(hasType(references(qualType(unless(isConstQualified())))))));
112657ac148SPeter Szecsi }
113657ac148SPeter Szecsi 
1148de103f2SPeter Szecsi static internal::Matcher<Stmt>
assignedToRef(internal::Matcher<Decl> VarNodeMatcher)1158de103f2SPeter Szecsi assignedToRef(internal::Matcher<Decl> VarNodeMatcher) {
1168de103f2SPeter Szecsi   return declStmt(hasDescendant(varDecl(
117657ac148SPeter Szecsi       allOf(hasType(referenceType()),
1188de103f2SPeter Szecsi             hasInitializer(anyOf(
1198de103f2SPeter Szecsi                 initListExpr(has(declRefExpr(to(varDecl(VarNodeMatcher))))),
1208de103f2SPeter Szecsi                 declRefExpr(to(varDecl(VarNodeMatcher)))))))));
121657ac148SPeter Szecsi }
122657ac148SPeter Szecsi 
1238de103f2SPeter Szecsi static internal::Matcher<Stmt>
getAddrTo(internal::Matcher<Decl> VarNodeMatcher)1248de103f2SPeter Szecsi getAddrTo(internal::Matcher<Decl> VarNodeMatcher) {
1258de103f2SPeter Szecsi   return unaryOperator(
126657ac148SPeter Szecsi       hasOperatorName("&"),
1278de103f2SPeter Szecsi       hasUnaryOperand(declRefExpr(hasDeclaration(VarNodeMatcher))));
128657ac148SPeter Szecsi }
129657ac148SPeter Szecsi 
hasSuspiciousStmt(StringRef NodeName)130657ac148SPeter Szecsi static internal::Matcher<Stmt> hasSuspiciousStmt(StringRef NodeName) {
1318de103f2SPeter Szecsi   return hasDescendant(stmt(
1323c3e1b0bSPeter Szecsi       anyOf(gotoStmt(), switchStmt(), returnStmt(),
133657ac148SPeter Szecsi             // Escaping and not known mutation of the loop counter is handled
134657ac148SPeter Szecsi             // by exclusion of assigning and address-of operators and
135657ac148SPeter Szecsi             // pass-by-ref function calls on the loop counter from the body.
136adcd0268SBenjamin Kramer             changeIntBoundNode(equalsBoundNode(std::string(NodeName))),
137adcd0268SBenjamin Kramer             callByRef(equalsBoundNode(std::string(NodeName))),
138adcd0268SBenjamin Kramer             getAddrTo(equalsBoundNode(std::string(NodeName))),
139adcd0268SBenjamin Kramer             assignedToRef(equalsBoundNode(std::string(NodeName))))));
140657ac148SPeter Szecsi }
141657ac148SPeter Szecsi 
forLoopMatcher()142657ac148SPeter Szecsi static internal::Matcher<Stmt> forLoopMatcher() {
143657ac148SPeter Szecsi   return forStmt(
1441af97c9dSAbbas Sabra              hasCondition(simpleCondition("initVarName", "initVarRef")),
145657ac148SPeter Szecsi              // Initialization should match the form: 'int i = 6' or 'i = 42'.
146f717d479SHenry Wong              hasLoopInit(
147f717d479SHenry Wong                  anyOf(declStmt(hasSingleDecl(
148f717d479SHenry Wong                            varDecl(allOf(hasInitializer(ignoringParenImpCasts(
149f717d479SHenry Wong                                              integerLiteral().bind("initNum"))),
150657ac148SPeter Szecsi                                          equalsBoundNode("initVarName"))))),
151f717d479SHenry Wong                        binaryOperator(hasLHS(declRefExpr(to(varDecl(
152f717d479SHenry Wong                                           equalsBoundNode("initVarName"))))),
153f717d479SHenry Wong                                       hasRHS(ignoringParenImpCasts(
154f717d479SHenry Wong                                           integerLiteral().bind("initNum")))))),
155657ac148SPeter Szecsi              // Incrementation should be a simple increment or decrement
156657ac148SPeter Szecsi              // operator call.
157657ac148SPeter Szecsi              hasIncrement(unaryOperator(
158657ac148SPeter Szecsi                  anyOf(hasOperatorName("++"), hasOperatorName("--")),
159657ac148SPeter Szecsi                  hasUnaryOperand(declRefExpr(
160657ac148SPeter Szecsi                      to(varDecl(allOf(equalsBoundNode("initVarName"),
161657ac148SPeter Szecsi                                       hasType(isInteger())))))))),
1621af97c9dSAbbas Sabra              unless(hasBody(hasSuspiciousStmt("initVarName"))))
1631af97c9dSAbbas Sabra       .bind("forLoop");
164657ac148SPeter Szecsi }
165657ac148SPeter Szecsi 
isCapturedByReference(ExplodedNode * N,const DeclRefExpr * DR)1661af97c9dSAbbas Sabra static bool isCapturedByReference(ExplodedNode *N, const DeclRefExpr *DR) {
1671af97c9dSAbbas Sabra 
1681af97c9dSAbbas Sabra   // Get the lambda CXXRecordDecl
1691af97c9dSAbbas Sabra   assert(DR->refersToEnclosingVariableOrCapture());
1701af97c9dSAbbas Sabra   const LocationContext *LocCtxt = N->getLocationContext();
1711af97c9dSAbbas Sabra   const Decl *D = LocCtxt->getDecl();
1721af97c9dSAbbas Sabra   const auto *MD = cast<CXXMethodDecl>(D);
1731af97c9dSAbbas Sabra   assert(MD && MD->getParent()->isLambda() &&
1741af97c9dSAbbas Sabra          "Captured variable should only be seen while evaluating a lambda");
1751af97c9dSAbbas Sabra   const CXXRecordDecl *LambdaCXXRec = MD->getParent();
1761af97c9dSAbbas Sabra 
1771af97c9dSAbbas Sabra   // Lookup the fields of the lambda
1781af97c9dSAbbas Sabra   llvm::DenseMap<const VarDecl *, FieldDecl *> LambdaCaptureFields;
1791af97c9dSAbbas Sabra   FieldDecl *LambdaThisCaptureField;
1801af97c9dSAbbas Sabra   LambdaCXXRec->getCaptureFields(LambdaCaptureFields, LambdaThisCaptureField);
1811af97c9dSAbbas Sabra 
1821af97c9dSAbbas Sabra   // Check if the counter is captured by reference
1831af97c9dSAbbas Sabra   const VarDecl *VD = cast<VarDecl>(DR->getDecl()->getCanonicalDecl());
1841af97c9dSAbbas Sabra   assert(VD);
1851af97c9dSAbbas Sabra   const FieldDecl *FD = LambdaCaptureFields[VD];
1861af97c9dSAbbas Sabra   assert(FD && "Captured variable without a corresponding field");
1871af97c9dSAbbas Sabra   return FD->getType()->isReferenceType();
1881af97c9dSAbbas Sabra }
1891af97c9dSAbbas Sabra 
1901af97c9dSAbbas Sabra // A loop counter is considered escaped if:
1911af97c9dSAbbas Sabra // case 1: It is a global variable.
1921af97c9dSAbbas Sabra // case 2: It is a reference parameter or a reference capture.
1931af97c9dSAbbas Sabra // case 3: It is assigned to a non-const reference variable or parameter.
1941af97c9dSAbbas Sabra // case 4: Has its address taken.
isPossiblyEscaped(ExplodedNode * N,const DeclRefExpr * DR)1951af97c9dSAbbas Sabra static bool isPossiblyEscaped(ExplodedNode *N, const DeclRefExpr *DR) {
1961af97c9dSAbbas Sabra   const VarDecl *VD = cast<VarDecl>(DR->getDecl()->getCanonicalDecl());
1971af97c9dSAbbas Sabra   assert(VD);
1981af97c9dSAbbas Sabra   // Case 1:
1998de103f2SPeter Szecsi   if (VD->hasGlobalStorage())
2008de103f2SPeter Szecsi     return true;
2018de103f2SPeter Szecsi 
2021af97c9dSAbbas Sabra   const bool IsRefParamOrCapture =
2031af97c9dSAbbas Sabra       isa<ParmVarDecl>(VD) || DR->refersToEnclosingVariableOrCapture();
2041af97c9dSAbbas Sabra   // Case 2:
2051af97c9dSAbbas Sabra   if ((DR->refersToEnclosingVariableOrCapture() &&
2061af97c9dSAbbas Sabra        isCapturedByReference(N, DR)) ||
2071af97c9dSAbbas Sabra       (IsRefParamOrCapture && VD->getType()->isReferenceType()))
20899b94f29SArtem Dergachev     return true;
20999b94f29SArtem Dergachev 
2108de103f2SPeter Szecsi   while (!N->pred_empty()) {
2116b85f8e9SArtem Dergachev     // FIXME: getStmtForDiagnostics() does nasty things in order to provide
2126b85f8e9SArtem Dergachev     // a valid statement for body farms, do we need this behavior here?
2136b85f8e9SArtem Dergachev     const Stmt *S = N->getStmtForDiagnostics();
2148de103f2SPeter Szecsi     if (!S) {
2158de103f2SPeter Szecsi       N = N->getFirstPred();
2168de103f2SPeter Szecsi       continue;
2178de103f2SPeter Szecsi     }
2188de103f2SPeter Szecsi 
2198de103f2SPeter Szecsi     if (const DeclStmt *DS = dyn_cast<DeclStmt>(S)) {
2208de103f2SPeter Szecsi       for (const Decl *D : DS->decls()) {
2218de103f2SPeter Szecsi         // Once we reach the declaration of the VD we can return.
2228de103f2SPeter Szecsi         if (D->getCanonicalDecl() == VD)
2238de103f2SPeter Szecsi           return false;
2248de103f2SPeter Szecsi       }
2258de103f2SPeter Szecsi     }
2268de103f2SPeter Szecsi     // Check the usage of the pass-by-ref function calls and adress-of operator
2278de103f2SPeter Szecsi     // on VD and reference initialized by VD.
2288de103f2SPeter Szecsi     ASTContext &ASTCtx =
2298de103f2SPeter Szecsi         N->getLocationContext()->getAnalysisDeclContext()->getASTContext();
2301af97c9dSAbbas Sabra     // Case 3 and 4:
2318de103f2SPeter Szecsi     auto Match =
2328de103f2SPeter Szecsi         match(stmt(anyOf(callByRef(equalsNode(VD)), getAddrTo(equalsNode(VD)),
2338de103f2SPeter Szecsi                          assignedToRef(equalsNode(VD)))),
2348de103f2SPeter Szecsi               *S, ASTCtx);
2358de103f2SPeter Szecsi     if (!Match.empty())
2368de103f2SPeter Szecsi       return true;
2378de103f2SPeter Szecsi 
2388de103f2SPeter Szecsi     N = N->getFirstPred();
2398de103f2SPeter Szecsi   }
24099b94f29SArtem Dergachev 
2411af97c9dSAbbas Sabra   // Reference parameter and reference capture will not be found.
2421af97c9dSAbbas Sabra   if (IsRefParamOrCapture)
24399b94f29SArtem Dergachev     return false;
24499b94f29SArtem Dergachev 
2458de103f2SPeter Szecsi   llvm_unreachable("Reached root without finding the declaration of VD");
2468de103f2SPeter Szecsi }
2478de103f2SPeter Szecsi 
shouldCompletelyUnroll(const Stmt * LoopStmt,ASTContext & ASTCtx,ExplodedNode * Pred,unsigned & maxStep)2488de103f2SPeter Szecsi bool shouldCompletelyUnroll(const Stmt *LoopStmt, ASTContext &ASTCtx,
2490db84863SPeter Szecsi                             ExplodedNode *Pred, unsigned &maxStep) {
250657ac148SPeter Szecsi 
251657ac148SPeter Szecsi   if (!isLoopStmt(LoopStmt))
252657ac148SPeter Szecsi     return false;
253657ac148SPeter Szecsi 
254657ac148SPeter Szecsi   // TODO: Match the cases where the bound is not a concrete literal but an
255657ac148SPeter Szecsi   // integer with known value
256657ac148SPeter Szecsi   auto Matches = match(forLoopMatcher(), *LoopStmt, ASTCtx);
2578de103f2SPeter Szecsi   if (Matches.empty())
2588de103f2SPeter Szecsi     return false;
2598de103f2SPeter Szecsi 
2601af97c9dSAbbas Sabra   const auto *CounterVarRef = Matches[0].getNodeAs<DeclRefExpr>("initVarRef");
2611496d188SPeter Szecsi   llvm::APInt BoundNum =
2621496d188SPeter Szecsi       Matches[0].getNodeAs<IntegerLiteral>("boundNum")->getValue();
2631496d188SPeter Szecsi   llvm::APInt InitNum =
2641496d188SPeter Szecsi       Matches[0].getNodeAs<IntegerLiteral>("initNum")->getValue();
2650db84863SPeter Szecsi   auto CondOp = Matches[0].getNodeAs<BinaryOperator>("conditionOperator");
2661496d188SPeter Szecsi   if (InitNum.getBitWidth() != BoundNum.getBitWidth()) {
267*6bec3e93SJay Foad     InitNum = InitNum.zext(BoundNum.getBitWidth());
268*6bec3e93SJay Foad     BoundNum = BoundNum.zext(InitNum.getBitWidth());
2691496d188SPeter Szecsi   }
2701496d188SPeter Szecsi 
2710db84863SPeter Szecsi   if (CondOp->getOpcode() == BO_GE || CondOp->getOpcode() == BO_LE)
2720db84863SPeter Szecsi     maxStep = (BoundNum - InitNum + 1).abs().getZExtValue();
2730db84863SPeter Szecsi   else
2740db84863SPeter Szecsi     maxStep = (BoundNum - InitNum).abs().getZExtValue();
2758de103f2SPeter Szecsi 
2768de103f2SPeter Szecsi   // Check if the counter of the loop is not escaped before.
2771af97c9dSAbbas Sabra   return !isPossiblyEscaped(Pred, CounterVarRef);
278657ac148SPeter Szecsi }
279657ac148SPeter Szecsi 
madeNewBranch(ExplodedNode * N,const Stmt * LoopStmt)280d0604acdSPeter Szecsi bool madeNewBranch(ExplodedNode *N, const Stmt *LoopStmt) {
281d0604acdSPeter Szecsi   const Stmt *S = nullptr;
2820db84863SPeter Szecsi   while (!N->pred_empty()) {
283d0604acdSPeter Szecsi     if (N->succ_size() > 1)
284d0604acdSPeter Szecsi       return true;
285d0604acdSPeter Szecsi 
286d0604acdSPeter Szecsi     ProgramPoint P = N->getLocation();
287d0604acdSPeter Szecsi     if (Optional<BlockEntrance> BE = P.getAs<BlockEntrance>())
2884e53032dSArtem Dergachev       S = BE->getBlock()->getTerminatorStmt();
289d0604acdSPeter Szecsi 
290d0604acdSPeter Szecsi     if (S == LoopStmt)
291d0604acdSPeter Szecsi       return false;
292d0604acdSPeter Szecsi 
293d0604acdSPeter Szecsi     N = N->getFirstPred();
294d0604acdSPeter Szecsi   }
295d0604acdSPeter Szecsi 
296d0604acdSPeter Szecsi   llvm_unreachable("Reached root without encountering the previous step");
297d0604acdSPeter Szecsi }
298d0604acdSPeter Szecsi 
2993c3e1b0bSPeter Szecsi // updateLoopStack is called on every basic block, therefore it needs to be fast
updateLoopStack(const Stmt * LoopStmt,ASTContext & ASTCtx,ExplodedNode * Pred,unsigned maxVisitOnPath)3003c3e1b0bSPeter Szecsi ProgramStateRef updateLoopStack(const Stmt *LoopStmt, ASTContext &ASTCtx,
3010db84863SPeter Szecsi                                 ExplodedNode *Pred, unsigned maxVisitOnPath) {
302657ac148SPeter Szecsi   auto State = Pred->getState();
3033c3e1b0bSPeter Szecsi   auto LCtx = Pred->getLocationContext();
304657ac148SPeter Szecsi 
3053c3e1b0bSPeter Szecsi   if (!isLoopStmt(LoopStmt))
3063c3e1b0bSPeter Szecsi     return State;
3073c3e1b0bSPeter Szecsi 
3083c3e1b0bSPeter Szecsi   auto LS = State->get<LoopStack>();
3093c3e1b0bSPeter Szecsi   if (!LS.isEmpty() && LoopStmt == LS.getHead().getLoopStmt() &&
310d0604acdSPeter Szecsi       LCtx == LS.getHead().getLocationContext()) {
311d0604acdSPeter Szecsi     if (LS.getHead().isUnrolled() && madeNewBranch(Pred, LoopStmt)) {
312d0604acdSPeter Szecsi       State = State->set<LoopStack>(LS.getTail());
3130db84863SPeter Szecsi       State = State->add<LoopStack>(
3140db84863SPeter Szecsi           LoopState::getNormal(LoopStmt, LCtx, maxVisitOnPath));
315d0604acdSPeter Szecsi     }
3163c3e1b0bSPeter Szecsi     return State;
317d0604acdSPeter Szecsi   }
3180db84863SPeter Szecsi   unsigned maxStep;
3190db84863SPeter Szecsi   if (!shouldCompletelyUnroll(LoopStmt, ASTCtx, Pred, maxStep)) {
3200db84863SPeter Szecsi     State = State->add<LoopStack>(
3210db84863SPeter Szecsi         LoopState::getNormal(LoopStmt, LCtx, maxVisitOnPath));
3223c3e1b0bSPeter Szecsi     return State;
323657ac148SPeter Szecsi   }
3243c3e1b0bSPeter Szecsi 
3250db84863SPeter Szecsi   unsigned outerStep = (LS.isEmpty() ? 1 : LS.getHead().getMaxStep());
3260db84863SPeter Szecsi 
3270db84863SPeter Szecsi   unsigned innerMaxStep = maxStep * outerStep;
3280db84863SPeter Szecsi   if (innerMaxStep > MAXIMUM_STEP_UNROLLED)
3290db84863SPeter Szecsi     State = State->add<LoopStack>(
3300db84863SPeter Szecsi         LoopState::getNormal(LoopStmt, LCtx, maxVisitOnPath));
3310db84863SPeter Szecsi   else
3320db84863SPeter Szecsi     State = State->add<LoopStack>(
3330db84863SPeter Szecsi         LoopState::getUnrolled(LoopStmt, LCtx, innerMaxStep));
3343c3e1b0bSPeter Szecsi   return State;
3353c3e1b0bSPeter Szecsi }
3363c3e1b0bSPeter Szecsi 
isUnrolledState(ProgramStateRef State)3373c3e1b0bSPeter Szecsi bool isUnrolledState(ProgramStateRef State) {
3383c3e1b0bSPeter Szecsi   auto LS = State->get<LoopStack>();
3393c3e1b0bSPeter Szecsi   if (LS.isEmpty() || !LS.getHead().isUnrolled())
3403c3e1b0bSPeter Szecsi     return false;
341657ac148SPeter Szecsi   return true;
342657ac148SPeter Szecsi }
343657ac148SPeter Szecsi }
344657ac148SPeter Szecsi }
345