Duplicate synthesis errors during evaluation of VariableAccess on the left-hand side of the assignment in LineAwareSynthesis

[TooMuchDakka]

At the time this issue was written I am using the 2.0.0 (commit c90cc2f) of this project.

When trying to synthesis an assignment whos VariableAccess on the left-hand side contains a synthesis error:

module main(inout a(2))
 for $i = 0 to (#a + 1) do
  ++= a.$i
 rof

using the LineAwareSynthesis, two duplicate synthesis errors are reported:

User defined bitrange start value '2' was not within the valid range [0, 2] in bitrange access on variable a 
User defined bitrange start value '2' was not within the valid range [0, 2] in bitrange access on variable a 

while when synthesizing the same SyReC module using the CostAwareSynthesis will only report one synthesis error.

The source of this 'error' is that to determine whether an assignment can be handled by the LineAwareSynthesis the latter will evaluate the left-hand side of the to be processed assignment which in our case generates the first synthesis error. With the LineAwareSynthesis having determined that it cannot handle the assignment it delegates its synthesis to the SyrecSynthesis base class which will reevaluate the VariableAccesses of the assignment and thus leading to the second synthesis error.

[Geremia]

@TooMuchDakka Your code synthesizes fine for me, but trying to line-aware synthesize this:

module test(inout a)
  for $i = 0 to #a do                                                                                              
   ++= a.$i                                                                                                        
  rof

module main(inout a)
  call test(a);
  uncall test(a)

gives:

User defined bitrange start value '32' was not within the valid range [0, 31] in bitrange access on variable o
User defined bitrange start value '32' was not within the valid range [0, 31] in bitrange access on variable o

And cost-aware synthesizing, I get:

User defined bitrange start value '32' was not within the valid range [0, 31] in bitrange access on variable o

Removing the uncall enables synthesizing.

Perhaps it is some off-by-one error when uncalling?

Environment

mqt-core          3.3.3
mqt-syrec         2.0.1.dev78+g38c08ada5.d20260211

[Geremia]

@TooMuchDakka It seems something about these changes since c90cc2f causes the issue:

diff --git a/src/algorithms/synthesis/syrec_synthesis.cpp b/src/algorithms/synthesis/syrec_synthesis.cpp
index 0883895..f7bd357 100644
--- a/src/algorithms/synthesis/syrec_synthesis.cpp
+++ b/src/algorithms/synthesis/syrec_synthesis.cpp
@@ -31,6 +31,7 @@
 #include <cassert>
 #include <chrono>
 #include <cstddef>
+#include <cstdint>
 #include <functional>
 #include <ios>
 #include <iostream>
@@ -680,8 +681,12 @@ namespace syrec {
         const unsigned     step         = statement.step ? statement.step->evaluate(loopMap) : 1U; // default step is +1
         const std::string& loopVariable = statement.loopVariable;
 
-        if (from <= to) {
-            for (unsigned i = from; i <= to; i += step) {
+        if (from == to) {
+            return true;
+        }
+
+        if (from < to) {
+            for (unsigned i = from; i < to; i += step) {
                 // adjust loop variable if necessary
 
                 if (!loopVariable.empty()) {
@@ -694,10 +699,11 @@ namespace syrec {
                     }
                 }
             }
-        }
-
-        else if (from > to) {
-            for (auto i = static_cast<int>(from); std::cmp_greater_equal(i, to); i -= static_cast<int>(step)) {
+        } else {
+            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) {
                 // adjust loop variable if necessary
 
                 if (!loopVariable.empty()) {
@@ -715,7 +721,6 @@ namespace syrec {
         if (!loopVariable.empty()) {
             assert(loopMap.erase(loopVariable) == 1U);
         }
-
         return true;
     }
 
@@ -1706,7 +1711,7 @@ namespace syrec {
         }
 
         if (evaluatedBitrangeStartValue >= accessedVariableBitwidth) {
-            std::cerr << "User defined bitrange start value '" << std::to_string(evaluatedBitrangeStartValue) << "' was not within the valid range [0, " << std::to_string(accessedVariableBitwidth) << "] in bitrange access on variable " << accessedVariableIdentifier << "\n";
+            std::cerr << "User defined bitrange start value '" << std::to_string(evaluatedBitrangeStartValue) << "' was not within the valid range [0, " << std::to_string(accessedVariableBitwidth - 1U) << "] in bitrange access on variable " << accessedVariableIdentifier << "\n";
             return std::nullopt;
         }
 
@@ -1718,7 +1723,7 @@ namespace syrec {
         }
 
         if (evaluatedBitrangeEndValue >= accessedVariableBitwidth) {
-            std::cerr << "User defined bitrange end value '" << std::to_string(evaluatedBitrangeEndValue) << "' was not within the valid range [0, " << std::to_string(accessedVariableBitwidth) << "] in bitrange access on variable " << accessedVariableIdentifier << "\n";
+            std::cerr << "User defined bitrange end value '" << std::to_string(evaluatedBitrangeEndValue) << "' was not within the valid range [0, " << std::to_string(accessedVariableBitwidth - 1U) << "] in bitrange access on variable " << accessedVariableIdentifier << "\n";
             return std::nullopt;
         }
         return EvaluatedBitrangeAccess({.bitrangeStart = evaluatedBitrangeStartValue, .bitrangeEnd = evaluatedBitrangeEndValue});
@@ -1728,7 +1733,7 @@ namespace syrec {
         assert(userDefinedVariableAccess.var != nullptr);
         const std::string_view& accessedVariableIdentifier = userDefinedVariableAccess.var->name;
         if (userDefinedVariableAccess.indexes.size() != userDefinedVariableAccess.var->dimensions.size()) {
-            std::cerr << "The number of indices (" << std::to_string(userDefinedVariableAccess.indexes.size()) << ") defined in a variable access must match the number of dimensions (" << std::to_string(userDefinedVariableAccess.var->dimensions.size()) << ") of the accessed variable " << accessedVariableIdentifier << "\n";
+            std::cerr << "The number of indices (" << std::to_string(userDefinedVariableAccess.indexes.size()) << ") defined in a variable access must match the number of dimensions (" << std::to_string(userDefinedVariableAccess.var->dimensions.size() - 1U) << ") of the accessed variable " << accessedVariableIdentifier << "\n";
             return std::nullopt;
         }
 
@@ -1743,7 +1748,7 @@ namespace syrec {
             if (const auto& dimensionExprAsNumericExpr = std::dynamic_pointer_cast<NumericExpression>(dimensionExpr); dimensionExprAsNumericExpr != nullptr) {
                 if (const std::optional<unsigned> evaluatedDimensionExpr = dimensionExprAsNumericExpr->value != nullptr ? dimensionExprAsNumericExpr->value->tryEvaluate(loopVariableValueLookup) : std::nullopt; evaluatedDimensionExpr.has_value()) {
                     if (*evaluatedDimensionExpr >= userDefinedVariableAccess.var->dimensions.at(dimensionIdx)) {
-                        std::cerr << "Access on value " << std::to_string(*evaluatedDimensionExpr) << " of dimension " << std::to_string(dimensionIdx) << " was not within the valid range [0, " << std::to_string(userDefinedVariableAccess.var->dimensions.at(dimensionIdx)) << " in access on variable " << accessedVariableIdentifier << "\n";
+                        std::cerr << "Access on value " << std::to_string(*evaluatedDimensionExpr) << " of dimension " << std::to_string(dimensionIdx) << " was not within the valid range [0, " << std::to_string(userDefinedVariableAccess.var->dimensions.at(dimensionIdx) - 1U) << "] in access on variable " << accessedVariableIdentifier << "\n";
                         return std::nullopt;
                     }
                     evaluatedDimensionAccess.accessedValuePerDimension[dimensionIdx] = evaluatedDimensionExpr;

[TooMuchDakka]

@Geremia The index-out-of-range error that you are seeing in your given example stems from the inversion semantics of a ForStatement that SyReC inherited from its predecessor Janus (see Figure 5 on page 148) and which can easily be overlooked warranting an additional notice soon being added to the SyReC documentation.

An UncallStatement is synthesized by synthesizing the inverse of the statements in the body of the uncalled module which in your example would require the synthesis of the inverse of a ForStatement defined as for <START> to <END> step <S> do <STMT_LIST> rof. However, the inversion of the ForStatement will not only invert the statements in the loop body but also the value range of the ForStatement thus the inversion result would be equal to for <END> to <START> step <S> do <STMT_LIST>^(-1) which for your example would be equal to:

module test(inout a)
  for $i = 0 to #a do                                                                                              
   ++= a.$i                                                                                                        
  rof

// Module is equal to statement: uncall test(a)
module invTest(inout a)
  for $i = #a to 0 do
    --= a.$i
  rof

module main(inout a)
  call test(a);
  // An index-out-of-range error will be reported due to the loop variable $i being 
  // initialized with the bitwidth of variable 'a' in the uncalled module
  uncall test(a) 

The index-out-of-range error is reported in both the cost- and line-aware synthesis since the semantics of the UncallStatement are shared by both synthesis algorithm variants.

[Geremia]

@TooMuchDakka So is your original issue resolved in master now?

[TooMuchDakka]

@TooMuchDakka So is your original issue resolved in master now?

No, at the moment duplicate synthesis errors (i.e. validation errors of the VariableAccess defined on the left-hand side of an assignment) are still reported by the LineAwareSynthesis.

[Geremia]

@TooMuchDakka

module test(inout a)
  for $i = 0 to #a do                                                                                              
   ++= a.$i                                                                                                        
  rof

// Module is equal to statement: uncall test(a)
module invTest(inout a)
  for $i = #a to 0 do
    --= a.$i
  rof

That's counterintuitive. Why not:

module invTest(inout a)
  for $i = #a to 0 do
    --= a.($i - 1)
  rof

?

---

Update: Oh, I see you've mentioned this in #546.