new feature: --staticBoundChecks:on to enforce static array index checking (#10965)

compiler/sempass2.nim

@@ -75,6 +75,7 @@ type
     gcUnsafe, isRecursive, isTopLevel, hasSideEffect, inEnforcedGcSafe: bool
     inEnforcedNoSideEffects: bool
     maxLockLevel, currLockLevel: TLockLevel
+    currOptions: TOptions
     config: ConfigRef
     graph: ModuleGraph
     c: PContext
@@ -668,6 +669,32 @@ proc cstringCheck(tracked: PEffects; n: PNode) =
       a.typ.kind == tyString and a.kind notin {nkStrLit..nkTripleStrLit}):
     message(tracked.config, n.info, warnUnsafeCode, renderTree(n))
 
+proc checkLe(c: PEffects; a, b: PNode) =
+  case proveLe(c.guards, a, b)
+  of impUnknown:
+    #for g in c.guards.s:
+    #  if g != nil: echo "I Know ", g
+    message(c.config, a.info, warnStaticIndexCheck,
+      "cannot prove: " & $a & " <= " & $b)
+  of impYes:
+    discard
+  of impNo:
+    message(c.config, a.info, warnStaticIndexCheck,
+      "can prove: " & $a & " > " & $b)
+
+proc checkBounds(c: PEffects; arr, idx: PNode) =
+  checkLe(c, lowBound(c.config, arr), idx)
+  checkLe(c, idx, highBound(c.config, arr, c.guards.o))
+
+proc checkRange(c: PEffects; value: PNode; typ: PType) =
+  if typ.skipTypes(abstractInst - {tyRange}).kind == tyRange:
+    let lowBound = nkIntLit.newIntNode(firstOrd(c.config, typ))
+    lowBound.info = value.info
+    let highBound = nkIntLit.newIntNode(lastOrd(c.config, typ))
+    highBound.info = value.info
+    checkLe(c, lowBound, value)
+    checkLe(c, value, highBound)
+
 proc createTypeBoundOps(tracked: PEffects, typ: PType; info: TLineInfo) =
   createTypeBoundOps(tracked.graph, tracked.c, typ, info)
   if (typ != nil and tfHasAsgn in typ.flags) or
@@ -755,12 +782,17 @@ proc track(tracked: PEffects, n: PNode) =
           discard
         else:
           message(tracked.config, arg.info, warnProveInit, $arg)
+
       # check required for 'nim check':
       if n[1].typ.len > 0:
         createTypeBoundOps(tracked, n[1].typ.lastSon, n.info)
         createTypeBoundOps(tracked, n[1].typ, n.info)
         # new(x, finalizer): Problem: how to move finalizer into 'createTypeBoundOps'?
 
+    elif a.kind == nkSym and a.sym.magic in {mArrGet, mArrPut} and
+        optStaticBoundsCheck in tracked.currOptions:
+      checkBounds(tracked, n[1], n[2])
+
     if a.kind == nkSym and a.sym.name.s.len > 0 and a.sym.name.s[0] == '=' and
           tracked.owner.kind != skMacro:
       let opKind = find(AttachedOpToStr, a.sym.name.s.normalize)
@@ -849,6 +881,28 @@ proc track(tracked: PEffects, n: PNode) =
   of nkForStmt, nkParForStmt:
     # we are very conservative here and assume the loop is never executed:
     let oldState = tracked.init.len
+
+    let oldFacts = tracked.guards.s.len
+    let iterCall = n[n.len-2]
+    if optStaticBoundsCheck in tracked.currOptions and iterCall.kind in nkCallKinds:
+      let op = iterCall[0]
+      if op.kind == nkSym and fromSystem(op.sym):
+        let iterVar = n[0]
+        case op.sym.name.s
+        of "..", "countup", "countdown":
+          let lower = iterCall[1]
+          let upper = iterCall[2]
+          # for i in 0..n   means  0 <= i and i <= n. Countdown is
+          # the same since only the iteration direction changes.
+          addFactLe(tracked.guards, lower, iterVar)
+          addFactLe(tracked.guards, iterVar, upper)
+        of "..<":
+          let lower = iterCall[1]
+          let upper = iterCall[2]
+          addFactLe(tracked.guards, lower, iterVar)
+          addFactLt(tracked.guards, iterVar, upper)
+        else: discard
+
     for i in 0..<n.len-2:
       let it = n[i]
       track(tracked, it)
@@ -858,7 +912,6 @@ proc track(tracked: PEffects, n: PNode) =
             createTypeBoundOps(tracked, x.typ, x.info)
         else:
           createTypeBoundOps(tracked, it.typ, it.info)
-    let iterCall = n[^2]
     let loopBody = n[^1]
     if tracked.owner.kind != skMacro and iterCall.safeLen > 1:
       # XXX this is a bit hacky:
@@ -867,6 +920,7 @@ proc track(tracked: PEffects, n: PNode) =
     track(tracked, iterCall)
     track(tracked, loopBody)
     setLen(tracked.init, oldState)
+    setLen(tracked.guards.s, oldFacts)
   of nkObjConstr:
     when false: track(tracked, n[0])
     let oldFacts = tracked.guards.s.len
@@ -932,18 +986,27 @@ proc track(tracked: PEffects, n: PNode) =
         # a better solution will come up eventually.
         if n[1].typ.kind != tyString:
           createTypeBoundOps(tracked, n[1].typ, n[1].info)
+      if optStaticBoundsCheck in tracked.currOptions:
+        checkRange(tracked, n[1], n.typ)
   of nkObjUpConv, nkObjDownConv, nkChckRange, nkChckRangeF, nkChckRange64:
     if n.len == 1:
       track(tracked, n[0])
       if tracked.owner.kind != skMacro:
         createTypeBoundOps(tracked, n.typ, n.info)
         createTypeBoundOps(tracked, n[0].typ, n[0].info)
+      if optStaticBoundsCheck in tracked.currOptions:
+        checkRange(tracked, n[0], n.typ)
   of nkBracket:
     for i in 0..<n.safeLen:
       track(tracked, n[i])
       checkForSink(tracked.config, tracked.owner, n[i])
     if tracked.owner.kind != skMacro:
       createTypeBoundOps(tracked, n.typ, n.info)
+  of nkBracketExpr:
+    if optStaticBoundsCheck in tracked.currOptions and n.len == 2:
+      if n[0].typ != nil and skipTypes(n[0].typ, abstractVar).kind != tyTuple:
+        checkBounds(tracked, n[0], n[1])
+    for i in 0 ..< n.len: track(tracked, n[i])
   else:
     for i in 0..<n.safeLen: track(tracked, n[i])
 
@@ -1028,6 +1091,8 @@ proc initEffects(g: ModuleGraph; effects: PNode; s: PSym; t: var TEffects; c: PC
   t.init = @[]
   t.guards.s = @[]
   t.guards.o = initOperators(g)
+  t.currOptions = g.config.options + s.options
+  t.guards.beSmart = optStaticBoundsCheck in t.currOptions
   t.locked = @[]
   t.graph = g
   t.config = g.config