Recently I tried to understand the exact semantics of the scf.for (and affine.for) operation:
scf.for %iv = %A to %B step %S { <body> }
When I first tried to understand it, two “obvious” but non-equivalent interpretations came to my mind:
- Loop over all
iv in {i | A <= i < B, i = A+j*S for some int j}. Trip countceil((B-A)/S)(in exact math over infinite precision integers). - It operates like this:
iv := A; while (iv < B) { <body>; iv := iv + S }.
These interpretations deviate if iv+S is in danger to overflow (see below for an example). I always believed (1) to be the intended interpretation, mostly based on the rather suggestive syntax (IMO). But yesterday I reconsidered the description of scf.for and tried to extract the answer from this:
The lower and upper bounds specify a half-open range: the iteration is executed iff the comparison of induction variable value is less than the upper bound and bigger or equal to the lower bound.
Unfortunately this is too vague for me and I cannot definitively conclude or exclude any of my interpretations. So I did some experiments. I found two interesting cases. The first one has a loop with an effect:
// overflow_acc.mlir
func.func @main() {
%lb = arith.constant 126 : i8
%ub = arith.constant 127 : i8
%step = arith.constant 2 : i8
%init = arith.constant 0 : i32
%one = arith.constant 1 : i32
%sum = scf.for %iv = %lb to %ub step %step iter_args(%acc = %init) -> (i32) : i8 {
%next = arith.addi %acc, %one : i32
scf.yield %next : i32
}
vector.print str "sum = "
vector.print %sum : i32
return
}
Under interpretation (1) this should print `sum = 1`, under interpretation (2) it should never terminate. (%step = 3 is also interesting because it always terminates but still wraps around and prints sum = 171 under (2)). The other example is a loop without any effect:
// overflow_empty.mlir
func.func @main() {
%lb = arith.constant 126 : i8
%ub = arith.constant 127 : i8
%step = arith.constant 2 : i8
%init = arith.constant 0 : i32
scf.for %iv = %lb to %ub step %step : i8 {}
vector.print str "terminated\n"
return
}
Under interpretation (1) it should terminate, under (2) it should run forever. I tested it with the following command:
FILE=$1
CANON=""
if [ "$2" = "1" ]; then
CANON="-canonicalize"
fi
mlir-opt $FILE \
$CANON -lower-affine \
-convert-vector-to-llvm -convert-scf-to-cf -convert-cf-to-llvm \
-convert-func-to-llvm -convert-arith-to-llvm -reconcile-unrealized-casts \
| mlir-runner -e main --entry-point-result=void \
--shared-libs=build/dev/lib/libmlir_c_runner_utils.so
The gist of the experiment is that it depends on various factors which interpretation “wins”. Some code actively works in favor of (1) (trip count computation) other code actively works in favor of (2) (lowering to cf).
First of all, with -canonicalize interpretation (1) wins for both example files. The principle reason seems to be that it detects that the trip count is 1 (using infinite precision math) and inlines the loop body. There is a function std::optional<APInt> constantTripCount(...) in StaticValueUtils.cpp which seems to do the mentioned computation. There are users of this function which ask “is the trip count exactly 1, if yes e.g. inline the body into the parent”. I confirmed that this function is crucial by modifying it and seeing that the outcome is different.
Without canonicalize and for overflow_empty.mlir interpretation (1) wins - but by accident. If I remember correctly the loop was identified as trivially dead by the greedy pattern driver (but not sure). In any case, the loop is already eliminated by the seemingly unrelated -convert-vector-to-llvm .
Again without canonicalize and for overflow_acc.mlir interpretation (2) wins. This can be best seen by just applying -convert-scf-to-cf to the file and inspecting the resulting IR.
I have several questions:
- Is there an intended exact specification of (overflow) behavior of loops?
- Or do we have to live with semantic ambiguities in corner cases (for reasons)?
- Should behave “seemingly identical”
affine.forandscf.forloops lead to the same observable behavior? - Would some of the behavior I documented be considered a bug?
Background info: I got interested in this topic while working on this PR: [mlir][SCFToAffine] Raise scf.for to affine.for by rainij · Pull Request #200851 · llvm/llvm-project · GitHub . It raises scf.for to affine.for and can deal with non-index typed scf.for ops (as long as index is wider than the base type). Under interpretation (1) (the one I believed strongly in until today) there is no issue. But under interpretation (2) there would be corner cases were observable behavior changes similar to the example above. I still think it is OK as is but I would like to have a deeper insight to gain confidence for future contributions. Also: The same examples behave almost the same way for affine.for (but it seems to not have the single-iteration trick built in). I am no expert but I believe that polyhedral optimization probably has to rely on something like (1) to theoretically work. I suppose that some affine optimizations would also not be semantic preserving if something like (2) holds.