/**

* @name Unbounded loop

* @description All loops should have a fixed upper bound; the counter should also be incremented along all paths within the loop.

* This check excludes loops that are meant to be nonterminating (like schedulers).

* @kind problem

* @id cpp/jpl-c/loop-bounds

* @problem.severity warning

* @tags correctness

* external/jpl

*/

import cpp

predicate validVarForBound(Loop loop, Variable var) {

// The variable is read in the loop controlling expression

var.getAnAccess().getParent*() = loop.getControllingExpr() and

// The variable is not assigned in the loop body

not inScope(loop, var.getAnAssignment().getEnclosingStmt()) and

// The variable is not incremented/decremented in the loop body

not inScope(loop, var.getAnAccess().getParent().(CrementOperation).getEnclosingStmt())

}

predicate upperBoundCheck(Loop loop, VariableAccess checked) {

exists(RelationalOperation rop | loop.getControllingExpr().getAChild*() = rop |

checked = rop.getLesserOperand() and

// The RHS is something "valid", i.e. a constant or

// a variable that isn't assigned in the loop body

(

exists(rop.getGreaterOperand().getValue()) or

rop.getGreaterOperand().(VariableAccess).getTarget().isConst() or

validVarForBound(loop, rop.getGreaterOperand().(VariableAccess).getTarget())

) and

not rop.getGreaterOperand() instanceof CharLiteral

)

}

predicate lowerBoundCheck(Loop loop, VariableAccess checked) {

exists(RelationalOperation rop | loop.getControllingExpr().getAChild*() = rop |

checked = rop.getGreaterOperand() and

// The RHS is something "valid", i.e. a constant or

// a variable that isn't assigned in the loop body

(

exists(rop.getLesserOperand().getValue()) or

rop.getLesserOperand().(VariableAccess).getTarget().isConst() or

validVarForBound(loop, rop.getLesserOperand().(VariableAccess).getTarget())

) and

not rop.getLesserOperand() instanceof CharLiteral

)

}

VariableAccess getAnIncrement(Variable var) {

result.getTarget() = var and

(

result.getParent() instanceof IncrementOperation

or

exists(AssignAddExpr a | a.getLValue() = result and a.getRValue().getValue().toInt() > 0)

or

exists(AssignExpr a | a.getLValue() = result |

a.getRValue() =

any(AddExpr ae |

ae.getAnOperand() = var.getAnAccess() and

ae.getAnOperand().getValue().toInt() > 0

)

)

)

}

VariableAccess getADecrement(Variable var) {

result.getTarget() = var and

(

result.getParent() instanceof DecrementOperation

or

exists(AssignSubExpr a | a.getLValue() = result and a.getRValue().getValue().toInt() > 0)

or

exists(AssignExpr a | a.getLValue() = result |

a.getRValue() =

any(SubExpr ae |

ae.getLeftOperand() = var.getAnAccess() and

ae.getRightOperand().getValue().toInt() > 0

)

)

)

}

predicate inScope(Loop l, Stmt s) { l.getAChild*() = s }

predicate reachesNoInc(VariableAccess source, ControlFlowNode target) {

upperBoundCheck(_, source) and source.getASuccessor() = target

or

exists(ControlFlowNode mid |

reachesNoInc(source, mid) and not mid = getAnIncrement(source.getTarget())

|

target = mid.getASuccessor() and

inScope(source.getEnclosingStmt(), target.getEnclosingStmt())

)

}

predicate reachesNoDec(VariableAccess source, ControlFlowNode target) {

lowerBoundCheck(_, source) and source.getASuccessor() = target

or

exists(ControlFlowNode mid |

reachesNoDec(source, mid) and not mid = getADecrement(source.getTarget())

|

target = mid.getASuccessor() and

inScope(source.getEnclosingStmt(), target.getEnclosingStmt())

)

}

predicate hasSafeBound(Loop l) {

exists(VariableAccess bound | upperBoundCheck(l, bound) | not reachesNoInc(bound, bound))

or

exists(VariableAccess bound | lowerBoundCheck(l, bound) | not reachesNoDec(bound, bound))

or

exists(l.getControllingExpr().getValue())

}

predicate markedAsNonterminating(Loop l) {

exists(Comment c | c.getContents().matches("%@non-terminating@%") | c.getCommentedElement() = l)

}

from Loop loop, string msg

where

not hasSafeBound(loop) and

not markedAsNonterminating(loop) and

(

not upperBoundCheck(loop, _) and

not lowerBoundCheck(loop, _) and

msg = "This loop does not have a fixed bound."

or

exists(VariableAccess bound |

upperBoundCheck(loop, bound) and

reachesNoInc(bound, bound) and

msg =

"The loop counter " + bound.getTarget().getName() +

" is not always incremented in the loop body."

)

or

exists(VariableAccess bound |

lowerBoundCheck(loop, bound) and

reachesNoDec(bound, bound) and

msg =

"The loop counter " + bound.getTarget().getName() +

" is not always decremented in the loop body."

)

)

select loop, msg