iss: Implement PC annotations [current], [next] and [next next]

vadl/main/vadl/ast/AnnotationTable.java

@@ -52,6 +52,7 @@
 import vadl.viam.ArtificialResource;
 import vadl.viam.AssemblyDescription;
 import vadl.viam.Constant;
+import vadl.viam.Counter;
 import vadl.viam.Encoding;
 import vadl.viam.Endianness;
 import vadl.viam.Format;
@@ -68,6 +69,7 @@
 import vadl.viam.annotations.DefineOperandAnnotation;
 import vadl.viam.annotations.EnableHtifAnno;
 import vadl.viam.annotations.InstructionUndefinedAnno;
+import vadl.viam.annotations.PcOffsetAnnotation;
 import vadl.viam.annotations.TbStateRegisterAnnotation;
 
 /**
@@ -107,7 +109,11 @@ public class AnnotationTable {
         .add("next", EnableAnnotation::new)
         .add("next next", EnableAnnotation::new)
         .check(GroupedAnnotationBuilder.GroupCheckContext::verifyOnlyOneOfGroup)
-        // FIXME: Apply to AST, see Issue #938
+        .applyViam(ctx -> {
+          var reg = ((Counter) ctx.targetDefinition).registerTensor();
+          ctx.get("next").ifPresent(ann -> reg.addAnnotation(new PcOffsetAnnotation(1)));
+          ctx.get("next next").ifPresent(ann -> reg.addAnnotation(new PcOffsetAnnotation(2)));
+        })
         .build();
 
     groupOn(AliasDefinition.class)
@@ -123,7 +129,11 @@ public class AnnotationTable {
                           + "and program counter aliases"));
           ctx.verifyOnlyOneOfGroup();
         })
-        // FIXME: Apply to AST, see Issue #938
+        .applyViam(ctx -> {
+          var reg = ((Counter) ctx.targetDefinition).registerTensor();
+          ctx.get("next").ifPresent(ann -> reg.addAnnotation(new PcOffsetAnnotation(1)));
+          ctx.get("next next").ifPresent(ann -> reg.addAnnotation(new PcOffsetAnnotation(2)));
+        })
         .build();
 
     annotationOn(RegisterDefinition.class, "zero", ZeroConstraintAnnotation::new)

vadl/main/vadl/ast/BehaviorLowering.java

@@ -1324,34 +1324,18 @@ private ExpressionNode visitSubCall(CallIndexExpr expr, ExpressionNode exprBefor
           case null, default -> false;
         };
         if (targetIsCounter) {
-          // FIXME: @ffreitag this is currently hardcoded as was wrong before.
-          //  It must add the instruction width in bytes.
-          // This width is obtained by the format type of the current instruction
-          var instrWidth = 32;
-          // The byte is defined by the "word" that is returned by the main memory definition.
-          // So essentially the return type in the relation type of the memory definition.
-          var byteWidth = 8;
-          var instrWidthInByte = instrWidth / byteWidth;
-
-          // FIXME: Handle slicing and format subcall propperly
+          // FIXME: Handle slicing and format subcall properly
           int offset = 0;
           for (var subcall : expr.subCalls) {
             var subcallName = subcall.identifier().name;
-            if (subcallName.equals("current")) {
-              offset = 0;
-            } else if (subcallName.equals("next")) {
-              offset += instrWidthInByte;
-            } else if (subcallName.equals("nextnext")) {
-              offset += instrWidthInByte * 2;
-            } else {
-              throw new IllegalStateException("unknown subcall: " + subcallName);
+            switch (subcallName) {
+              case "current" -> offset = 0;
+              case "next" -> offset += 1;
+              case "nextnext" -> offset += 2;
+              default -> throw new IllegalStateException("unknown subcall: " + subcallName);
             }
           }
-
-          resultExpr = BuiltInCall.of(BuiltInTable.ADD,
-              resRead,
-              intU(offset, resRead.type().bitWidth()).toNode()
-          );
+          resRead.setPcOffset(offset);
         }
       } else {
         throw new IllegalStateException();

vadl/main/vadl/ast/SymbolTable.java

@@ -28,6 +28,7 @@
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
+import java.util.function.Predicate;
 import java.util.function.Supplier;
 import javax.annotation.Nullable;
 import vadl.error.Diagnostic;
@@ -388,8 +389,8 @@ Set<String> allSymbolNames() {
   @SafeVarargs
   final Set<String> allSymbolNamesOf(Class<? extends Node>... classes) {
     var matchingNames = symbols.entrySet().stream()
-        .filter(entry -> entry.getValue() instanceof AstSymbol astSymbol
-            && Arrays.stream(classes).anyMatch(klass -> klass.isInstance(astSymbol.origin)))
+        .filter(entry -> entry.getValue() instanceof AstSymbol(Node origin)
+            && Arrays.stream(classes).anyMatch(klass -> klass.isInstance(origin)))
         .map(Map.Entry::getKey)
         .toList();
 
@@ -400,6 +401,26 @@ final Set<String> allSymbolNamesOf(Class<? extends Node>... classes) {
     return names;
   }
 
+  /**
+   * Returns all symbol names in scope that point to nodes satisfying the given predicate.
+   *
+   * @param predicate that must be satisfied.
+   * @return the set of all available names.
+   */
+  final Set<String> allSymbolNamesWhere(Predicate<Node> predicate) {
+    var matchingNames = symbols.entrySet().stream()
+        .filter(entry -> entry.getValue() instanceof AstSymbol(Node origin)
+            && predicate.test(origin))
+        .map(Map.Entry::getKey)
+        .toList();
+
+    var names = new HashSet<>(matchingNames);
+    if (parent != null) {
+      names.addAll(parent.allSymbolNamesWhere(predicate));
+    }
+    return names;
+  }
+
   /**
    * Returns all symbol names in scope that point to the defined node classes.
    *

vadl/main/vadl/ast/TypeChecker.java

@@ -1603,13 +1603,26 @@ public Void visit(AliasDefinition definition) {
       // if this does not directly reference a register,
       // it might reference another alias definition
       var alias = definition.symbolTable().findAs(targetIdent, AliasDefinition.class);
-      if (alias == null || alias.kind != AliasDefinition.AliasKind.REGISTER) {
+      if (alias == null) {
+        var candidates = new ArrayList<>(definition.symbolTable().allSymbolNamesWhere(
+            node -> node instanceof RegisterDefinition
+                || (node instanceof AliasDefinition aliasDef
+                && aliasDef.kind == AliasDefinition.AliasKind.REGISTER)
+        ));
+        var suggestions = Levenshtein.suggestions(targetIdent.pathToString(), candidates);
         throw addErrorAndStopChecking(
             error("Unknown alias source register", targetIdent.location())
                 .locationDescription(targetIdent.location(), "Unknown register `%s`.",
                     targetIdent)
+                .suggestions(suggestions)
                 .build());
       }
+      if (alias.kind == AliasDefinition.AliasKind.PROGRAM_COUNTER) {
+        throw addErrorAndStopChecking(
+            error("Register alias cannot refer to program counter alias", targetIdent.location())
+                .build()
+        );
+      }
       check(alias);
       reg = (RegisterDefinition) requireNonNull(alias.computedTarget);
     }
@@ -1622,7 +1635,7 @@ public Void visit(AliasDefinition definition) {
       addErrorAndStopChecking(
           error("Unsupported Alias Type", definition)
               .locationDescription(definition,
-                  "The typechecker doesn't know how such aliases yet.")
+                  "The typechecker doesn't know such aliases yet.")
               .locationHelp(definition,
                   "If you desire this feature, please let us know at: "
                       + "https://github.com/OpenVADL/openvadl/issues/new")

vadl/main/vadl/pass/order/ViamPassOrder.java

@@ -35,6 +35,7 @@
 import vadl.viam.passes.functionInliner.ArtificialResInlinerPass;
 import vadl.viam.passes.functionInliner.FieldAccessInlinerPass;
 import vadl.viam.passes.functionInliner.FunctionInlinerPass;
+import vadl.viam.passes.pcOffset.PcOffsetPass;
 import vadl.viam.passes.sideeffect_condition.SideEffectConditionResolvingPass;
 import vadl.viam.passes.staticCounterAccess.CounterAccessResolvingPass;
 import vadl.viam.passes.statusBuiltInInlinePass.RemoveUnusedStatusFlagsFromBuiltinsPass;
@@ -61,6 +62,7 @@ public static PassOrder create(GeneralConfiguration configuration) throws IOExce
     order.add(new NormalizeFieldsToFieldAccessFunctionsPass(configuration));
     order.add(new RenamingConflictingRegistersPass(configuration));
     order.add(new SnapshotInstructionBehaviorPass(configuration));
+    order.add(new PcOffsetPass(configuration));
 
     order.add(new RemoveUnusedStatusFlagsFromBuiltinsPass(configuration));
     order.add(new StatusBuiltInInlinePass(configuration));

vadl/main/vadl/viam/annotations/PcOffsetAnnotation.java

@@ -0,0 +1,47 @@
+// SPDX-FileCopyrightText : © 2026 TU Wien <vadl@tuwien.ac.at>
+// SPDX-License-Identifier: GPL-3.0-or-later
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU General Public License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+package vadl.viam.annotations;
+
+import vadl.viam.Annotation;
+import vadl.viam.RegisterTensor;
+
+/**
+ * Annotation for offsetting read pc values by one or two instruction
+ * lengths. Can be overwritten by {@link vadl.viam.passes.pcOffset.nodes.PcOffsetNode}.
+ *
+ * <p>The offset is applied by {@link vadl.viam.passes.pcOffset.PcOffsetPass}.
+ */
+public class PcOffsetAnnotation extends Annotation<RegisterTensor> {
+
+  public PcOffsetAnnotation(int offset) {
+    this.offset = offset;
+  }
+
+  private final int offset;
+
+  @Override
+  public Class<RegisterTensor> parentDefinitionClass() {
+    return RegisterTensor.class;
+  }
+
+  /**
+   * The offset in instructions lengths that is added.
+   */
+  public int offset() {
+    return offset;
+  }
+}

vadl/main/vadl/viam/graph/dependency/ReadResourceNode.java

@@ -37,6 +37,11 @@ public abstract class ReadResourceNode extends ExpressionNode {
   @Input
   protected NodeList<ExpressionNode> indices;
 
+  // FIXME: not sure what is the best way to implement this...
+  //        maybe add a special node for adding this offset?
+  @Nullable
+  private Integer pcOffset;
+
   public ReadResourceNode(@Nullable ExpressionNode address, DataType type) {
     super(type);
     this.indices = address == null ? new NodeList<>() : new NodeList<>(address);
@@ -104,6 +109,12 @@ protected void collectInputs(List<Node> collection) {
     collection.addAll(indices);
   }
 
+  @Override
+  protected void collectData(List<Object> collection) {
+    super.collectData(collection);
+    collection.add(pcOffset);
+  }
+
   @Override
   public void applyOnInputsUnsafe(
       vadl.viam.graph.GraphVisitor.Applier<vadl.viam.graph.Node> visitor) {
@@ -122,4 +133,21 @@ public boolean hasConstantAddress() {
 
     return false;
   }
+
+  /**
+   * Sets the read offset produced by calling e.g. {@code .next} on a program
+   * counter.
+   */
+  public void setPcOffset(int pcOffset) {
+    this.pcOffset = pcOffset;
+  }
+
+  /**
+   * Returns the read offset produced by calling e.g. {@code .next} on a program
+   * counter. Is used by {@link vadl.viam.passes.pcOffset.PcOffsetPass}.
+   */
+  @Nullable
+  public Integer pcOffset() {
+    return pcOffset;
+  }
 }

vadl/main/vadl/viam/passes/pcOffset/PcOffsetPass.java

@@ -0,0 +1,91 @@
+// SPDX-FileCopyrightText : © 2026 TU Wien <vadl@tuwien.ac.at>
+// SPDX-License-Identifier: GPL-3.0-or-later
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU General Public License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+package vadl.viam.passes.pcOffset;
+
+import java.io.IOException;
+import javax.annotation.Nullable;
+import vadl.configuration.GeneralConfiguration;
+import vadl.pass.Pass;
+import vadl.pass.PassName;
+import vadl.pass.PassResults;
+import vadl.types.BuiltInTable;
+import vadl.utils.GraphUtils;
+import vadl.utils.ViamUtils;
+import vadl.viam.Instruction;
+import vadl.viam.Specification;
+import vadl.viam.annotations.PcOffsetAnnotation;
+import vadl.viam.graph.Graph;
+import vadl.viam.graph.dependency.BuiltInCall;
+import vadl.viam.graph.dependency.ReadResourceNode;
+
+/**
+ * Applies program counter offsets to program counter reads.
+ *
+ * <p>When reading a program counter that has been annotated with
+ * {@code [current]}, {@code [next]} or {@code [next next]} or when using
+ * one of the subcalls {@code .current}, {@code .next} or {@code .nextnext},
+ * the read value is offset by multiples of the instruction length. The subcalls
+ * overwrite the annotations.
+ *
+ * <p>This pass looks for {@link PcOffsetAnnotation}s and checks
+ * {@link ReadResourceNode#pcOffset()} and applies them by inserting addition nodes.
+ */
+public class PcOffsetPass extends Pass {
+
+  public PcOffsetPass(GeneralConfiguration configuration) {
+    super(configuration);
+  }
+
+  @Override
+  public PassName getName() {
+    return new PassName("PC Offset Pass");
+  }
+
+  @Override
+  public @Nullable Object execute(PassResults passResults, Specification viam)
+      throws IOException {
+    ViamUtils.findAllBehaviors(viam).forEach(this::handleBehaviour);
+    return null;
+  }
+
+  private void handleBehaviour(Graph behaviour) {
+    // FIXME: are instruction lengths always multiples of 8?
+    //        What if the pc does not counter per byte?
+    // FIXME: What instruction length should be used in behaviours outside
+    //        instructions (eg in functions)?
+    int instrBytes = behaviour.parentDefinition() instanceof Instruction instruction
+        ? instruction.format().type().bitWidth() / 8
+        : 32;
+
+    behaviour.getNodes(ReadResourceNode.class)
+        .forEach(n -> handleRead(n, instrBytes));
+  }
+
+  private void handleRead(ReadResourceNode read, int instrBytes) {
+    var offsetAnn = read.resourceDefinition().annotation(PcOffsetAnnotation.class);
+    var regOffset = offsetAnn == null ? 0 : offsetAnn.offset();
+    var readOffset = read.pcOffset();
+    int offset = readOffset != null ? readOffset : regOffset;
+
+    if (offset != 0) {
+      read.replace(BuiltInCall.of(
+          BuiltInTable.ADD, read,
+          GraphUtils.intUNode((long) offset * instrBytes, read.type().bitWidth())
+      ));
+    }
+  }
+}

vadl/test/resources/testSource/passes/pcOffset/valid_pc_alias_ann_current.vadl

@@ -0,0 +1,19 @@
+
+instruction set architecture PcTest = {
+  using Regs = Bits<32>
+
+  register A: Regs
+  [ current ]
+  alias program counter PC: Regs = A
+
+  instruction READ_PC: F = A := PC
+
+  encoding READ_PC = { I = 2 }
+  assembly READ_PC = "Test"
+
+  format F: Regs = {
+    I: Regs
+  }
+}
+
+processor TEST implements PcTest = {}