Expected semantics when inverting a `ForStatement`

[TooMuchDakka]

At the moment a ForStatement can perform iterations as defined below:

// $i gets the values 0, 1, 2 assigned
for $i = 0 to 3 step 1 do
  ...
rof

// $i gets the values 3, 2, 1 assigned
for $i = 3 to 0 step 1 do
  ...
rof

In both cases the iteration range is equal to the interval [start, end). Additionally, we assume that SyReC inherits the statement inversion semantics from its predecessor Janus which defines the inversion of a ForStatement by not only inverting the statements in the loop body but also by switching the start and end value of the ForStatement.

However, if we do perform said switch which includes the simple swap of start end end then the resulting "inverted" ForStatement does not match the actual inverse one and could also lead to subtle index-out-of-range errors as shown in #545. The two ForStatements from above would at the moment be inverted as:

// $i gets the values 3, 2, 1 assigned, in the non-inverted loop $i would have the values 0, 1, 2
for $i = 3 to 0 step 1 do
   ...
rof

// $i gets the values 0, 1, 2 assigned, in the non-inverted loop $i would have the values 3, 2, 1
for $i = 0 to 3 step 1 do
  ...
rof

We can see that in both inverted loops the iteration range ([end, start)) now starts at the value excluded in the non-inverted loop and excludes the start value that is included in the iteration range of the non-inverted loop. The actual inverse of both loops would defined the iteration range as (end, start] with a loop in which the start value is smaller than the end being inverted as:

// To be inverted loop
for $i = 0 to 3 step 1 do
   ...
rof

for $i = 3 to 0 step 1 do
  // All occurrences of $i would have to be replaced with ($i - 1). This should be fine since
  // $i is a compile time constant which in turn would also allow one to evaluate ($i - 1) at compile time.
  ...
rof

A loop in which start is larger than end could be inverted similarily with two equivalent definitions being shown in the example below:

// To be inverted loop
for $i = 3 to 0 step 1 do
   ...
rof

// Variant one
for $i = 0 to 3 step 1 do
  // Replace all occurrences of $i with ($i + 1)
  ...
rof

// Variant two
for $i = (0 + 1) to (3 + 1) step 1 do
  ...
rof

@burgholzer Should we update the inversion semantics of a ForStatement as defined above or is the current behaviour in which a simple swap of the start and end value occurs the expected one?

[burgholzer]

as pointed out in the review, I think this is actually a bug and should be fixed.

[Geremia]

@TooMuchDakka
Would

diff --git a/src/algorithms/synthesis/syrec_synthesis.cpp b/src/algorithms/synthesis/syrec_synthesis.cpp
index f7bd357..a255666 100644
--- a/src/algorithms/synthesis/syrec_synthesis.cpp
+++ b/src/algorithms/synthesis/syrec_synthesis.cpp
@@ -703,7 +703,7 @@ namespace syrec {
             const auto fromSigned = static_cast<std::int64_t>(from);
             const auto toSigned   = static_cast<std::int64_t>(to);
             const auto stepSigned = static_cast<std::int64_t>(step);
-            for (auto i = fromSigned; i > toSigned; i -= stepSigned) {
+            for (auto i = fromSigned - stepSigned; i > toSigned; i -= stepSigned) {
                 // adjust loop variable if necessary
 
                 if (!loopVariable.empty()) {

fix this?

[TooMuchDakka]

It could be a solution if the function (in our case the syrec::onStatement(const ForStatement&) would only handle reversed ForStatements but since we are also handling non-reversed ones then the code you posted will skip the additional iteration performed in the current solution in the reversed ForStatement case (but does not include the to value, so one iteration is skipped again) while also omitting two iterations in the non-reversed case.

[Geremia]

@TooMuchDakka Is there a way to tell from within onStatement if it's reversed or non-reversed?

[TooMuchDakka]

No, at the moment neither the syrec::Statement base struct nor any of its derivations encode this information which should only be needed for the synthesis of a ForStatement so one could either extend the ForStatement definition or encode this information somehow in the synthesis algorithms. In the latter the SyrecSynthesis::statementExecutionOrderStack member variable (see) might be helpful.

However, if such a reversed/non-reversed flag in the synthesis algorithm is used to fix the synthesis of the ForStatement then one would have to think about whether the returned value of the ForStatement::reverse function is actually usable/valid without a SyrecSynthesis instance.