The system: [1] The Nelson-Oppen decision procedure: [2]
There's a subset of of arithmetic and logic that's completely decidable.
It includes addition, subtraction, multiplication by constants, "if", the theory of arrays, a similar theory of structures, and the Boolean operators (on bools, not integers.) This is enough for most subscript and overflow checks. Complete solvers exist for this subset. If you try to prove all constraints that need run-time checks with this approach, you can eliminate maybe 80-90% of run time checks as unnecessary.
Some checks cannot be eliminated, but can be hoisted out of loops. This means making one check before entering the loop, rather than one on each iteration. FOR statements usually can be optimized in this way. That's almost a no-brainer in modern compilers. The "Go" compiler does this. Heavier machinery is needed for more complex loops.
Really? I was under the impression the Go compiler did only simplistic optimisations, to get their wonderfully fast compile times. Do you have a source (e.g. the source)?
That was from the developers mailing list. I think the only optimization they're doing is for FOR statements, where you know the bounds on a loop variable at loop start. This is a big win for loops that iterate over an array and do something trivial, like setting the array elements to 0. Subscript check performance is mostly an inner-loop problem.
Oh, I'm curious why you pointed out Go specifically, since that sounds like fairly standard bounds check eliminations that pretty much all optimising compilers can do (compilers built on both LLVM and GCC's infrastructure), and most compilers aren't tied to specific looping constructs for it: it can work with while loops, or for loops, or whatever.
And, my impression is that bounds checks are only avoided in Go with range-based for loops (which are very similar to C++ or Rust iterators, which avoid bounds checks in probably exactly the same way), not a loop over integers with indexing.
There's a subset of of arithmetic and logic that's completely decidable. It includes addition, subtraction, multiplication by constants, "if", the theory of arrays, a similar theory of structures, and the Boolean operators (on bools, not integers.) This is enough for most subscript and overflow checks. Complete solvers exist for this subset. If you try to prove all constraints that need run-time checks with this approach, you can eliminate maybe 80-90% of run time checks as unnecessary.
Some checks cannot be eliminated, but can be hoisted out of loops. This means making one check before entering the loop, rather than one on each iteration. FOR statements usually can be optimized in this way. That's almost a no-brainer in modern compilers. The "Go" compiler does this. Heavier machinery is needed for more complex loops.
[1] http://www.animats.com/papers/verifier/verifiermanual.pdf
[2] http://www.cs.cmu.edu/~joshuad/NelsonOppen.pdf