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