From 4e7eed47d3d7ef43a96c9e92452f578425e07efc Mon Sep 17 00:00:00 2001 From: Matthias Raschhofer Date: Sun, 19 Jul 2026 11:22:40 +0200 Subject: [PATCH 1/2] Implement operation element of expression - type checking - behavior lowering --- vadl-frontend/main/vadl/ast/AstUtils.java | 3 +- .../main/vadl/ast/BehaviorLowering.java | 7 ++- .../main/vadl/ast/FrontendBuiltIns.java | 49 +++++++++++++++-- vadl-frontend/main/vadl/ast/TypeChecker.java | 39 ++++++++++++++ .../lowering/groupDefinition.vadl | 1 + .../operationElementOfTrivialWarning.vadl | 52 +++++++++++++++++++ .../cppCodeGen/FunctionCodeGenerator.java | 8 ++- .../GenerateInstructionOperandsPass.java | 6 +++ vadl/main/vadl/iss/codegen/IssProcGen.java | 6 +++ .../codegen/IssTbStaticExpressionCodeGen.java | 6 +++ .../iss/codegen/TcgTranslateGenerator.java | 6 +++ .../passes/common/IssNormalizationPass.java | 6 +++ .../common/opDecomposition/Decomposer.java | 6 +++ .../tcg/lowering/TcgOpLoweringPass.java | 6 +++ ...blyInstructionPrinterImmediateHandler.java | 7 +++ ...ilerInstructionExpansionCodeGenerator.java | 16 ++++++ .../relocation/RelocationCodeGenerator.java | 6 +++ .../passes/asm/AsmGrammarRuleGenerator.java | 7 +++ .../viam/graph/dependency/OperationRef.java | 42 +++++++++++++++ 19 files changed, 271 insertions(+), 8 deletions(-) create mode 100644 vadl-frontend/test/resources/frontend-snapshots/typechecker/operationElementOfTrivialWarning.vadl create mode 100644 vadl/main/vadl/viam/graph/dependency/OperationRef.java diff --git a/vadl-frontend/main/vadl/ast/AstUtils.java b/vadl-frontend/main/vadl/ast/AstUtils.java index c6ca9ae89..bab52ab43 100644 --- a/vadl-frontend/main/vadl/ast/AstUtils.java +++ b/vadl-frontend/main/vadl/ast/AstUtils.java @@ -16,6 +16,7 @@ package vadl.ast; +import java.util.ArrayList; import java.util.List; import java.util.Map; import java.util.concurrent.atomic.AtomicBoolean; @@ -90,7 +91,7 @@ static BuiltInTable.BuiltIn getOperatorBuiltIn(Operator operator, List arg } String finalOperatorSymbol = symbol; - var builtIns = operatorLookupTable.getOrDefault(finalOperatorSymbol, List.of()); + var builtIns = operatorLookupTable.getOrDefault(finalOperatorSymbol, new ArrayList<>()); builtIns.removeIf(b -> b.signature().argTypeClasses().size() != argTypes.size()); // Sometimes there are a signed and unsigned version of builtin operation diff --git a/vadl-frontend/main/vadl/ast/BehaviorLowering.java b/vadl-frontend/main/vadl/ast/BehaviorLowering.java index b138894d5..52bf8c9c8 100644 --- a/vadl-frontend/main/vadl/ast/BehaviorLowering.java +++ b/vadl-frontend/main/vadl/ast/BehaviorLowering.java @@ -125,7 +125,6 @@ import vadl.utils.BigIntUtils; import vadl.utils.Either; import vadl.utils.Pair; -import vadl.utils.SourceLocation; import vadl.utils.WithLocation; import vadl.viam.ArtificialResource; import vadl.viam.Constant; @@ -175,6 +174,7 @@ import vadl.viam.graph.dependency.MiaBuiltInCall; import vadl.viam.graph.dependency.OperationExistsNode; import vadl.viam.graph.dependency.OperationForAllNode; +import vadl.viam.graph.dependency.OperationRef; import vadl.viam.graph.dependency.ProcCallNode; import vadl.viam.graph.dependency.ReadArtificialResNode; import vadl.viam.graph.dependency.ReadMemNode; @@ -1064,6 +1064,11 @@ private ExpressionNode visitIdentifiable(Expr expr) { return new GroupRef(expr.type()); } + // Reference to an Operation Definition + if (computedTarget instanceof OperationDefinition) { + return new OperationRef(expr.type()); + } + // Function call without arguments (and no parenthesis) if (computedTarget instanceof FunctionDefinition functionDefinition) { var function = (Function) viamLowering.fetch(functionDefinition).orElseThrow(); diff --git a/vadl-frontend/main/vadl/ast/FrontendBuiltIns.java b/vadl-frontend/main/vadl/ast/FrontendBuiltIns.java index ca76ed3bc..61e00962f 100644 --- a/vadl-frontend/main/vadl/ast/FrontendBuiltIns.java +++ b/vadl-frontend/main/vadl/ast/FrontendBuiltIns.java @@ -34,7 +34,7 @@ final class FrontendBuiltIns { */ static final BuiltInTable.BuiltIn OP_EQU = BuiltInTable.func("VADL::opequ", "=", - Type.relation(PseudoFormatType.class, PseudoFormatType.class, BoolType.class)) + Type.relation(PseudoFormatType.class, PseudoFormatType.class, BoolType.class)) .takesDefault() .returns(Type.bool()) .build(); @@ -46,16 +46,57 @@ final class FrontendBuiltIns { */ static final BuiltInTable.BuiltIn OP_NEQ = BuiltInTable.func("VADL::opneq", "!=", - Type.relation(PseudoFormatType.class, PseudoFormatType.class, BoolType.class)) + Type.relation(PseudoFormatType.class, PseudoFormatType.class, BoolType.class)) .takesDefault() .returns(Type.bool()) .build(); static final List operationEqualityPredicates = List.of(OP_EQU, OP_NEQ); - private FrontendBuiltIns() {} + /** + * Element-of check for operations. Check if the actual instruction, matched by the group + * expression is an element of the given operation. + *
+ * Example: + * 
+   *   instruction A : IType = ...
+   *   instruction B : IType = ...
+   *
+   *   operation O1 = {A}
+   *   operation O1 = {B}
+   *
+   *   [assert : VLIW(0) ∈ O1]
+   *   group VLIW = (O1|O2)
+   *
+ */ + static final BuiltInTable.BuiltIn OP_ELEM_OF = + BuiltInTable.func("VADL::elemof", "∈", + Type.relation(PseudoFormatType.class, PseudoFormatType.class, BoolType.class)) + .takesDefault() + .returns(Type.bool()) + .build(); + + /** + * Negation of the element-of check for operation, see {@link #OP_ELEM_OF}. + * + */ + static final BuiltInTable.BuiltIn OP_NOT_ELEM_OF = + BuiltInTable.func("VADL::nelemof", "∉", + Type.relation(PseudoFormatType.class, PseudoFormatType.class, BoolType.class)) + .takesDefault() + .returns(Type.bool()) + .build(); + + static final List operationElementOfPredicates = + List.of(OP_ELEM_OF, OP_NOT_ELEM_OF); + + private FrontendBuiltIns() { + } static Stream builtIns() { - return Stream.concat(BuiltInTable.builtIns(), operationEqualityPredicates.stream()); + return Stream.concat(BuiltInTable.builtIns(), Stream.concat( + operationEqualityPredicates.stream(), + operationElementOfPredicates.stream() + )); } } diff --git a/vadl-frontend/main/vadl/ast/TypeChecker.java b/vadl-frontend/main/vadl/ast/TypeChecker.java index f744482ce..ce5154612 100644 --- a/vadl-frontend/main/vadl/ast/TypeChecker.java +++ b/vadl-frontend/main/vadl/ast/TypeChecker.java @@ -17,6 +17,7 @@ package vadl.ast; import static java.util.Objects.requireNonNull; +import static vadl.ast.FrontendBuiltIns.OP_NOT_ELEM_OF; import static vadl.ast.GroupDefUtils.GroupExprBitLengthCollector.maxBitLength; import static vadl.ast.GroupDefUtils.GroupExprLengthCollector.maxLength; import static vadl.error.Diagnostic.error; @@ -1042,6 +1043,28 @@ private BuiltInCheckResult unCachedCheckBuiltin(BuiltInTable.BuiltIn builtIn, Li } } + if (args.size() == 2 && FrontendBuiltIns.operationElementOfPredicates.contains(builtIn)) { + // Static checks for operation element predicates + final PseudoFormatType l = (PseudoFormatType) args.getFirst().type(); + final PseudoFormatType r = (PseudoFormatType) args.getLast().type(); + + final Set commonInsns = new LinkedHashSet<>(l.instructions()); + commonInsns.retainAll(r.instructions()); + + if (commonInsns.isEmpty()) { + // If there is no static overlap, we can emit some diagnostics. For ∈, the expr is always + // false, and for ∉ it's always true. + final boolean constVal = builtIn == OP_NOT_ELEM_OF; + final var op = Objects.requireNonNull(r.operations().stream().findFirst().orElse(null)); + DeferredDiagnosticStore.add( + warning("This expression is always %s".formatted(constVal), location) + .description( + "None of the possible concrete instructions matched by the left side " + + "are part of operation `%s`.", op.identifier().name) + .build()); + } + } + if (args.size() == 2 && (BuiltInTable.arithmeticOperators.contains(builtIn) || BuiltInTable.arithmeticComparisons.contains(builtIn))) { var left = args.getFirst(); @@ -3372,6 +3395,22 @@ private void visitIdentifiable(Expr expr) { return; } + if (origin instanceof OperationDefinition op) { + check(op); + + var def = getCurrentlyVisitingDefinition(); + if (!(def instanceof AnnotationDefinition annotation) + || !(annotation.target instanceof GroupDefinition)) { + final var diagnostic = error("Invalid Reference", expr) + .description("Reference to an `operation` definition is only allowed within " + + "`group` annotations."); + addErrorAndContinueChecking(diagnostic.build()); + } + + expr.type = PseudoFormatType.of(List.of(op)); + return; + } + if (origin != null) { // It's not a builtin but we don't handle it yet. // We might be here from a call expr and it might be necessary to handle the call for another diff --git a/vadl-frontend/test/resources/frontend-snapshots/lowering/groupDefinition.vadl b/vadl-frontend/test/resources/frontend-snapshots/lowering/groupDefinition.vadl index 31f30ad45..f4cc5ace3 100644 --- a/vadl-frontend/test/resources/frontend-snapshots/lowering/groupDefinition.vadl +++ b/vadl-frontend/test/resources/frontend-snapshots/lowering/groupDefinition.vadl @@ -19,6 +19,7 @@ instruction set architecture ISA = { operation O2 = {A,B} [stop : exists i in {O1}, j in {O2} then i = j] + [assert : VLIW(0) ∈ O1 && VLIW(2) ∉ O2] [assert : VLIW(0).opcode = 0b0] [assert : VLIW(VLIW.length - 1).opcode != 0b01] [assert : forall i in {O1, O2} then i.opcode(7..4,2) = 0b10101] diff --git a/vadl-frontend/test/resources/frontend-snapshots/typechecker/operationElementOfTrivialWarning.vadl b/vadl-frontend/test/resources/frontend-snapshots/typechecker/operationElementOfTrivialWarning.vadl new file mode 100644 index 000000000..ebc912e50 --- /dev/null +++ b/vadl-frontend/test/resources/frontend-snapshots/typechecker/operationElementOfTrivialWarning.vadl @@ -0,0 +1,52 @@ +instruction set architecture ISA = { + program counter PC : Bits<32> + + format AType : Bits<32> = { + a : Bits<20>, + b : Bits<5>, + c : Bits<7> + } + + format BType : Bits<32> = { + a : Bits<20>, + b : Bits<5>, + d : Bits<7> + } + + instruction A : AType = PC := 0 + encoding A = {a = 0b00} + assembly A = (mnemonic, "") + + instruction B : BType = PC := 0 + encoding B = {a = 0b01} + assembly B = (mnemonic, "") + + operation OpA = {A} + operation OpB = {B} + + [assert : VLIW(0) ∈ OpB] + [assert : VLIW(0) ∉ OpB] + group VLIW = OpA<1..2> +} + + +// Reported Diagnostics: +// +// warning: This expression is always false +// ╭── test/resources/frontend-snapshots/typechecker/operationElementOfTrivialWarning.vadl:27:13 +// │ +// 27 │ [assert : VLIW(0) ∈ OpB] +// │ ^^^^^^^^^^^^^^^ +// │ +// None of the possible concrete instructions matched by the left side are part of operation `OpB`. +// +// warning: This expression is always true +// ╭── test/resources/frontend-snapshots/typechecker/operationElementOfTrivialWarning.vadl:28:13 +// │ +// 28 │ [assert : VLIW(0) ∉ OpB] +// │ ^^^^^^^^^^^^^^^ +// │ +// None of the possible concrete instructions matched by the left side are part of operation `OpB`. +// +// +// Part of the class vadl.ast.FrontendSnapshotTests \ No newline at end of file diff --git a/vadl/main/vadl/cppCodeGen/FunctionCodeGenerator.java b/vadl/main/vadl/cppCodeGen/FunctionCodeGenerator.java index 41e1576c1..30090039c 100644 --- a/vadl/main/vadl/cppCodeGen/FunctionCodeGenerator.java +++ b/vadl/main/vadl/cppCodeGen/FunctionCodeGenerator.java @@ -36,6 +36,7 @@ import vadl.viam.graph.dependency.GroupRef; import vadl.viam.graph.dependency.OperationExistsNode; import vadl.viam.graph.dependency.OperationForAllNode; +import vadl.viam.graph.dependency.OperationRef; import vadl.viam.graph.dependency.ReadArtificialResNode; import vadl.viam.graph.dependency.ReadMemNode; import vadl.viam.graph.dependency.ReadRegTensorNode; @@ -114,6 +115,11 @@ protected void handle(CGenContext ctx, GroupRef toHandle) { throwNotAllowed(toHandle, "group reference expressions"); } + @Handler + protected void handle(CGenContext ctx, OperationRef toHandle) { + throwNotAllowed(toHandle, "operation reference expressions"); + } + public String genReturnExpression() { var returnNode = getSingleNode(function.behavior(), ReturnNode.class); return context.genToString(returnNode.value()); @@ -124,5 +130,3 @@ public CNodeContext context() { return context; } } - - diff --git a/vadl/main/vadl/gcb/passes/operands/GenerateInstructionOperandsPass.java b/vadl/main/vadl/gcb/passes/operands/GenerateInstructionOperandsPass.java index 85ce86abc..d2e6e2057 100644 --- a/vadl/main/vadl/gcb/passes/operands/GenerateInstructionOperandsPass.java +++ b/vadl/main/vadl/gcb/passes/operands/GenerateInstructionOperandsPass.java @@ -74,6 +74,7 @@ import vadl.viam.graph.dependency.MiaBuiltInCall; import vadl.viam.graph.dependency.OperationExistsNode; import vadl.viam.graph.dependency.OperationForAllNode; +import vadl.viam.graph.dependency.OperationRef; import vadl.viam.graph.dependency.ReadArtificialResNode; import vadl.viam.graph.dependency.ReadMemNode; import vadl.viam.graph.dependency.ReadRegTensorNode; @@ -705,6 +706,11 @@ protected void handle(GroupRef node) { throw Diagnostic.error("not supported", node.location()).build(); } + @Handler + protected void handle(OperationRef node) { + throw Diagnostic.error("not supported", node.location()).build(); + } + @Handler protected void handle(LetNode node) { PseudoNodeOperandCollectorDispatcher.dispatch(this, node.expression()); diff --git a/vadl/main/vadl/iss/codegen/IssProcGen.java b/vadl/main/vadl/iss/codegen/IssProcGen.java index 22e3eefc4..41a9b9ef5 100644 --- a/vadl/main/vadl/iss/codegen/IssProcGen.java +++ b/vadl/main/vadl/iss/codegen/IssProcGen.java @@ -45,6 +45,7 @@ import vadl.viam.graph.dependency.LetNode; import vadl.viam.graph.dependency.OperationExistsNode; import vadl.viam.graph.dependency.OperationForAllNode; +import vadl.viam.graph.dependency.OperationRef; import vadl.viam.graph.dependency.ParamNode; import vadl.viam.graph.dependency.ReadRegTensorNode; import vadl.viam.passes.sideEffectScheduling.nodes.InstrExitNode; @@ -229,6 +230,11 @@ void handle(CGenContext ctx, GroupRef toHandle) { throwNotAllowed(toHandle, "group reference expressions"); } + @Handler + void handle(CGenContext ctx, OperationRef toHandle) { + throwNotAllowed(toHandle, "operation reference expressions"); + } + private boolean shouldInlineExprSave(ExprSaveNode save) { return isIdentifierLike(save.value(), new HashSet<>()); } diff --git a/vadl/main/vadl/iss/codegen/IssTbStaticExpressionCodeGen.java b/vadl/main/vadl/iss/codegen/IssTbStaticExpressionCodeGen.java index 38771d7a5..5083f553c 100644 --- a/vadl/main/vadl/iss/codegen/IssTbStaticExpressionCodeGen.java +++ b/vadl/main/vadl/iss/codegen/IssTbStaticExpressionCodeGen.java @@ -37,6 +37,7 @@ import vadl.viam.graph.dependency.GroupRef; import vadl.viam.graph.dependency.OperationExistsNode; import vadl.viam.graph.dependency.OperationForAllNode; +import vadl.viam.graph.dependency.OperationRef; import vadl.viam.graph.dependency.TensorNode; /** @@ -154,4 +155,9 @@ void handle(CGenContext ctx, TensorNode toHandle) { void handle(CGenContext ctx, GroupRef toHandle) { throw new UnsupportedOperationException("Type GroupRef not yet implemented"); } + + @Handler + void handle(CGenContext ctx, OperationRef toHandle) { + throw new UnsupportedOperationException("Type OperationRef not yet implemented"); + } } diff --git a/vadl/main/vadl/iss/codegen/TcgTranslateGenerator.java b/vadl/main/vadl/iss/codegen/TcgTranslateGenerator.java index 7bfa15ed3..f3c2b5f72 100644 --- a/vadl/main/vadl/iss/codegen/TcgTranslateGenerator.java +++ b/vadl/main/vadl/iss/codegen/TcgTranslateGenerator.java @@ -41,6 +41,7 @@ import vadl.viam.graph.dependency.GroupRef; import vadl.viam.graph.dependency.OperationExistsNode; import vadl.viam.graph.dependency.OperationForAllNode; +import vadl.viam.graph.dependency.OperationRef; /** * Emits direct non-helper translation functions. @@ -162,4 +163,9 @@ void handle(CGenContext ctx, OperationExistsNode toHandle) { void handle(CGenContext ctx, GroupRef toHandle) { throwNotAllowed(toHandle, "group reference expressions"); } + + @Handler + void handle(CGenContext ctx, OperationRef toHandle) { + throwNotAllowed(toHandle, "operation reference expressions"); + } } diff --git a/vadl/main/vadl/iss/passes/common/IssNormalizationPass.java b/vadl/main/vadl/iss/passes/common/IssNormalizationPass.java index d06ce406a..4520af6d3 100644 --- a/vadl/main/vadl/iss/passes/common/IssNormalizationPass.java +++ b/vadl/main/vadl/iss/passes/common/IssNormalizationPass.java @@ -80,6 +80,7 @@ import vadl.viam.graph.dependency.LetNode; import vadl.viam.graph.dependency.OperationExistsNode; import vadl.viam.graph.dependency.OperationForAllNode; +import vadl.viam.graph.dependency.OperationRef; import vadl.viam.graph.dependency.ReadArtificialResNode; import vadl.viam.graph.dependency.ReadMemNode; import vadl.viam.graph.dependency.ReadRegTensorNode; @@ -908,4 +909,9 @@ void handle(OperationExistsNode toHandle) { void handle(GroupRef toHandle) { // do nothing } + + @Handler + void handle(OperationRef toHandle) { + // do nothing + } } diff --git a/vadl/main/vadl/iss/passes/common/opDecomposition/Decomposer.java b/vadl/main/vadl/iss/passes/common/opDecomposition/Decomposer.java index ae19ab1a4..6d6b15801 100644 --- a/vadl/main/vadl/iss/passes/common/opDecomposition/Decomposer.java +++ b/vadl/main/vadl/iss/passes/common/opDecomposition/Decomposer.java @@ -59,6 +59,7 @@ import vadl.viam.graph.dependency.MiaBuiltInCall; import vadl.viam.graph.dependency.OperationExistsNode; import vadl.viam.graph.dependency.OperationForAllNode; +import vadl.viam.graph.dependency.OperationRef; import vadl.viam.graph.dependency.ReadArtificialResNode; import vadl.viam.graph.dependency.ReadMemNode; import vadl.viam.graph.dependency.ReadRegTensorNode; @@ -649,6 +650,11 @@ void handle(Request rq, GroupRef toHandle) { throw new UnsupportedOperationException("Type GroupRef not yet implemented"); } + @Handler + void handle(Request rq, OperationRef toHandle) { + throw new UnsupportedOperationException("Type OperationRef not yet implemented"); + } + @Handler void handle(Request rq, BuiltInCall toHandle) { var previousCall = currCall; diff --git a/vadl/main/vadl/iss/passes/tcg/lowering/TcgOpLoweringPass.java b/vadl/main/vadl/iss/passes/tcg/lowering/TcgOpLoweringPass.java index 6715c2da6..ba306efe3 100644 --- a/vadl/main/vadl/iss/passes/tcg/lowering/TcgOpLoweringPass.java +++ b/vadl/main/vadl/iss/passes/tcg/lowering/TcgOpLoweringPass.java @@ -118,6 +118,7 @@ import vadl.viam.graph.dependency.LetNode; import vadl.viam.graph.dependency.OperationExistsNode; import vadl.viam.graph.dependency.OperationForAllNode; +import vadl.viam.graph.dependency.OperationRef; import vadl.viam.graph.dependency.ParamNode; import vadl.viam.graph.dependency.ProcCallNode; import vadl.viam.graph.dependency.ReadArtificialResNode; @@ -750,6 +751,11 @@ void handle(GroupRef node) { throw new UnsupportedOperationException("Type GroupRef not supported"); } + @Handler + void handle(OperationRef node) { + throw new UnsupportedOperationException("Type OperationRef not supported"); + } + /// / Nodes that are already considered lowered //// @Handler diff --git a/vadl/main/vadl/lcb/codegen/assembly/AssemblyInstructionPrinterImmediateHandler.java b/vadl/main/vadl/lcb/codegen/assembly/AssemblyInstructionPrinterImmediateHandler.java index 6af408b0e..539d83a6f 100644 --- a/vadl/main/vadl/lcb/codegen/assembly/AssemblyInstructionPrinterImmediateHandler.java +++ b/vadl/main/vadl/lcb/codegen/assembly/AssemblyInstructionPrinterImmediateHandler.java @@ -79,6 +79,7 @@ import vadl.viam.graph.dependency.GroupRef; import vadl.viam.graph.dependency.OperationExistsNode; import vadl.viam.graph.dependency.OperationForAllNode; +import vadl.viam.graph.dependency.OperationRef; import vadl.viam.graph.dependency.ProcCallNode; import vadl.viam.graph.dependency.ReadArtificialResNode; import vadl.viam.graph.dependency.ReadMemNode; @@ -474,6 +475,12 @@ public void handle(CGenContext ctx, GroupRef node) { throw Diagnostic.error("not supported", node.location()).build(); } + @Handler + @SuppressWarnings("MissingJavadocMethod") + public void handle(CGenContext ctx, OperationRef node) { + throw Diagnostic.error("not supported", node.location()).build(); + } + private void handleConditional(BuiltInCall node, CGenContext ctx, String operation) { node.ensure(node.arguments().size() == 2, "Expected two arguments"); diff --git a/vadl/main/vadl/lcb/codegen/expansion/CompilerInstructionExpansionCodeGenerator.java b/vadl/main/vadl/lcb/codegen/expansion/CompilerInstructionExpansionCodeGenerator.java index ed90f2b90..4b153e1fd 100644 --- a/vadl/main/vadl/lcb/codegen/expansion/CompilerInstructionExpansionCodeGenerator.java +++ b/vadl/main/vadl/lcb/codegen/expansion/CompilerInstructionExpansionCodeGenerator.java @@ -94,6 +94,7 @@ import vadl.viam.graph.dependency.LabelNode; import vadl.viam.graph.dependency.OperationExistsNode; import vadl.viam.graph.dependency.OperationForAllNode; +import vadl.viam.graph.dependency.OperationRef; import vadl.viam.graph.dependency.ReadArtificialResNode; import vadl.viam.graph.dependency.ReadMemNode; import vadl.viam.graph.dependency.ReadRegTensorNode; @@ -1180,6 +1181,11 @@ protected void handle(CGenContext ctx, ReadSignalNode toHandle) { protected void handle(CGenContext ctx, GroupRef toHandle) { throwNotAllowed(toHandle, "group reference node"); } + + @Handler + protected void handle(CGenContext ctx, OperationRef toHandle) { + throwNotAllowed(toHandle, "operation reference node"); + } } /** @@ -1325,6 +1331,11 @@ protected void handle(CGenContext ctx, ReadSignalNode toHandle) { protected void handle(CGenContext ctx, GroupRef toHandle) { throwNotAllowed(toHandle, "group reference node"); } + + @Handler + protected void handle(CGenContext ctx, OperationRef toHandle) { + throwNotAllowed(toHandle, "operation reference node"); + } } /** @@ -1474,6 +1485,11 @@ protected void handle(CGenContext ctx, ReadSignalNode toHandle) { protected void handle(CGenContext ctx, GroupRef toHandle) { throwNotAllowed(toHandle, "group reference node"); } + + @Handler + protected void handle(CGenContext ctx, OperationRef toHandle) { + throwNotAllowed(toHandle, "operation reference node"); + } } class AddingOperands implements CaseHandler { diff --git a/vadl/main/vadl/lcb/codegen/relocation/RelocationCodeGenerator.java b/vadl/main/vadl/lcb/codegen/relocation/RelocationCodeGenerator.java index da492097e..4dc7c83e3 100644 --- a/vadl/main/vadl/lcb/codegen/relocation/RelocationCodeGenerator.java +++ b/vadl/main/vadl/lcb/codegen/relocation/RelocationCodeGenerator.java @@ -38,6 +38,7 @@ import vadl.viam.graph.dependency.GroupRef; import vadl.viam.graph.dependency.OperationExistsNode; import vadl.viam.graph.dependency.OperationForAllNode; +import vadl.viam.graph.dependency.OperationRef; import vadl.viam.graph.dependency.ReadArtificialResNode; import vadl.viam.graph.dependency.ReadMemNode; import vadl.viam.graph.dependency.ReadRegTensorNode; @@ -187,6 +188,11 @@ void handle(CGenContext ctx, GroupRef toHandle) { throwNotAllowed(toHandle, "group reference expressions"); } + @Handler + void handle(CGenContext ctx, OperationRef toHandle) { + throwNotAllowed(toHandle, "operation reference expressions"); + } + @Override public CNodeContext context() { return context; diff --git a/vadl/main/vadl/lcb/passes/asm/AsmGrammarRuleGenerator.java b/vadl/main/vadl/lcb/passes/asm/AsmGrammarRuleGenerator.java index 0b82bdaf7..f09d4a8e0 100644 --- a/vadl/main/vadl/lcb/passes/asm/AsmGrammarRuleGenerator.java +++ b/vadl/main/vadl/lcb/passes/asm/AsmGrammarRuleGenerator.java @@ -79,6 +79,7 @@ import vadl.viam.graph.dependency.LetNode; import vadl.viam.graph.dependency.OperationExistsNode; import vadl.viam.graph.dependency.OperationForAllNode; +import vadl.viam.graph.dependency.OperationRef; import vadl.viam.graph.dependency.ProcCallNode; import vadl.viam.graph.dependency.ReadArtificialResNode; import vadl.viam.graph.dependency.ReadMemNode; @@ -605,4 +606,10 @@ public void handle(AsmRuleContext ctx, SliceNode node) { public void handle(AsmRuleContext ctx, GroupRef node) { throw Diagnostic.error("not supported", node.location()).build(); } + + @Handler + @SuppressWarnings("MissingJavadocMethod") + public void handle(AsmRuleContext ctx, OperationRef node) { + throw Diagnostic.error("not supported", node.location()).build(); + } } diff --git a/vadl/main/vadl/viam/graph/dependency/OperationRef.java b/vadl/main/vadl/viam/graph/dependency/OperationRef.java new file mode 100644 index 000000000..3edf5d3d7 --- /dev/null +++ b/vadl/main/vadl/viam/graph/dependency/OperationRef.java @@ -0,0 +1,42 @@ +// SPDX-FileCopyrightText : © 2026 TU Wien +// 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 . + +package vadl.viam.graph.dependency; + +import vadl.types.Type; +import vadl.viam.Operation; +import vadl.viam.graph.Node; + +/** + * Reference to an {@link Operation} definition. + */ +public class OperationRef extends ExpressionNode { + + public OperationRef(Type type) { + super(type); + } + + @Override + public ExpressionNode copy() { + return new OperationRef(type()); + } + + @Override + public Node shallowCopy() { + return new OperationRef(type()); + } + +} From 3a7f5c2994916621f4a6ba5d0dbd8e324ff829f8 Mon Sep 17 00:00:00 2001 From: Matthias Raschhofer Date: Sun, 19 Jul 2026 12:03:01 +0200 Subject: [PATCH 2/2] Enable hexagon group expression and annotations --- sys/hexagon/hexagon.vadl | 63 +++++++++++++++++----------------------- 1 file changed, 27 insertions(+), 36 deletions(-) diff --git a/sys/hexagon/hexagon.vadl b/sys/hexagon/hexagon.vadl index d94bfc547..c1d3c0116 100644 --- a/sys/hexagon/hexagon.vadl +++ b/sys/hexagon/hexagon.vadl @@ -1290,8 +1290,7 @@ instruction set architecture QDSP6 = // 00 = duplex instruction // An instruction packet can contain one duplex and up to two other (non-duplex) instructions. // The duplex must always appear as the last word in a packet. - // TODO: Reenable this annotation - // [ stop : let parse = VLIW(VLIW.length - 1).parse in ( ( parse = 0b00 ) | (parse = 0b11 ) ) ] + [ stop : let parse = VLIW(VLIW.length - 1).parse in ( ( parse = 0b00 ) || (parse = 0b11 ) ) ] // The constant extender effectively serves as a prefix for an instruction: it is not executed in // a slot, nor does it consume any slot resources. Within a packet, a constant extender must be @@ -1315,17 +1314,13 @@ instruction set architecture QDSP6 = // program flow instructions (J or JR) can be grouped together in a packet (Section 7.8). // Otherwise, at most one program flow instruction is allowed in a packet. = "dual jump" // - May not be first in dual jump: unconditional `jump` - // TODO: Reenable this annotation - // [ assert : !( (VLIW.length >= 2) & ((VLIW(0) ∈ JUMP_IMM) & (VLIW(1) ∈ J)) ) ] + [ assert : !( (VLIW.length >= 2) && ((VLIW(0) ∈ JUMP_IMM) && (VLIW(1) ∈ J)) ) ] // - May not be in dual jump: `if ([!]cmp.xx(Rs.new, Rt)) jump` - // TODO: Reenable this annotation - // [ assert : !( (VLIW.length >= 2) & (((VLIW(0) ∈ JUMP_CMP_NEW) & (VLIW(1) ∈ J)) | ((VLIW(0) ∈ J) & (VLIW(1) ∈ JUMP_CMP_NEW))) ) ] + [ assert : !( (VLIW.length >= 2) && (((VLIW(0) ∈ JUMP_CMP_NEW) && (VLIW(1) ∈ J)) || ((VLIW(0) ∈ J) && (VLIW(1) ∈ JUMP_CMP_NEW))) ) ] // - May not be in dual jump: all `jumpr` (JR is only allowed in slot 1) - // TODO: Reenable this annotation - // [ assert : !( (VLIW.length >= 2) & ((VLIW(0) ∈ J) & (VLIW(1) ∈ JR))) ] + [ assert : !( (VLIW.length >= 2) && ((VLIW(0) ∈ J) && (VLIW(1) ∈ JR))) ] // - May not be in dual jump: all `dealloc_return` - // TODO: Reenable this annotation - // [ assert : !( (VLIW.length >= 2) & (((VLIW(0) ∈ J) & (VLIW(1) ∈ J)) & exists in {DEALLOC_RETURN}) ) ] + [ assert : !( (VLIW.length >= 2) && (((VLIW(0) ∈ J) && (VLIW(1) ∈ J)) && exists in {DEALLOC_RETURN}) ) ] // - May not be in dual jump: `endloopN` // - -> See loop section below // - JR-class instructions can be placed in Slot 2. However, when encoded in a duplex jumpr R31 @@ -1357,12 +1352,10 @@ instruction set architecture QDSP6 = // - -> handled via regex // - memw_locked,memd_locked,l2fetch,and trace must execute on Slot 0. They must be grouped // only with ALU32 or (non-FP) XTYPE instructions. - // TODO: Reenable this annotation - // [ assert : implies(VLIW(VLIW.length-1) ∈ MEMLOCKED_L2FETCH_TRACE, forall j in {ALL} then ((j = VLIW(VLIW.length-1)) | (j ∈ ALU32_XTYPE_NON_FP)) ) ] + [ assert : implies(VLIW(VLIW.length-1) ∈ MEMLOCKED_L2FETCH_TRACE, forall j in {ALL} then ((j = VLIW(VLIW.length-1)) || (j ∈ ALU32_XTYPE_NON_FP)) ) ] // - dccleana,dcinva,dccleaninva,and dczeroa must execute on Slot 0. Slot 1 must be empty or an // ALU32 instruction. Note that Slot 1 being empty means that Slot 2 or 3 follow immediately. - // TODO: Reenable this annotation - // [ assert : implies(VLIW(VLIW.length-1) ∈ CACHE_MAINTENANCE_SPECIAL, (VLIW.length = 1) | !(VLIW(VLIW.length-2) ∈ LD_ST)) ] + [ assert : implies(VLIW(VLIW.length-1) ∈ CACHE_MAINTENANCE_SPECIAL, (VLIW.length = 1) || !(VLIW(VLIW.length-2) ∈ LD_ST)) ] // "Dependency constraints" // - Instructions in a packet cannot write to the same destination register. The assembler @@ -1384,8 +1377,8 @@ instruction set architecture QDSP6 = // - (floating point because it reads trap/rounding flags from USR) // - l2fetch sets "L2 prefetch active". But it can only be together with ALU and non-FP XTYPE anyway // - all instructions that set the OVF Sticky Saturation Overflow - // TODO: Reenable this annotation - // [ assert : !( (exists i in {TRANSFER_C_R,TRANSFER_CC_RR} then i.d5 = 8) & exists in {FLOATING_POINT, SATURATING} ) ] + + [ assert : !( (exists i in {TRANSFER_C_R,TRANSFER_CC_RR} then i.d5 = 8) && exists in {FLOATING_POINT, SATURATING} ) ] // - Multiple compare instructions are allowed to target the same predicate register in order // to perform a logical AND of the results (Section 6.2.3). // - If a packet contains endloopN, it cannot perform an auto-AND with predicate register P3. @@ -1394,18 +1387,17 @@ instruction set architecture QDSP6 = // register, then no other instruction in the packet can write to the same predicate // register. (As a result, a register transfer to P3:0 or C5:4 cannot be grouped with any // other predicate-writing instruction.) - // TODO: Reenable this annotation - // [ assert : !( ((exists i in {TRANSFER_C_R,TRANSFER_CC_RR} then i.d5 = 4) | (exists in {TRANSFER_P_R})) & - // exists in {PRED_WRITING} ) ] + + [ assert : !( ((exists i in {TRANSFER_C_R,TRANSFER_CC_RR} then i.d5 = 4) || (exists in {TRANSFER_P_R})) && + exists in {PRED_WRITING} ) ] // - The instructions spNloop0, decbin, tlbmatch, memw_locked, memd_locked, add:carry, // sub:carry, sfcmp, and dfcmp cannot be grouped with another instruction that sets the // same predicate register. - // TODO: Reenable this annotation - // [ assert : forall i in {ARITH_CARRY /*, CMP_FP, TODO */} then !( - // ((exists j in {PRED_WRITING} then (i != j) & (j.d2 = i.u2)) | - // (exists j in {TRANSFER_C_R,TRANSFER_CC_RR} then j.d5 = 4)) | - // (exists j in {TRANSFER_P_R} then j.d2 = i.u2 ) - // ) ] + [ assert : forall i in {ARITH_CARRY /*, CMP_FP, TODO */} then !( + ((exists j in {PRED_WRITING} then (i != j) && (j.d2 = i.u2)) || + (exists j in {TRANSFER_C_R,TRANSFER_CC_RR} then j.d5 = 4)) || + (exists j in {TRANSFER_P_R} then j.d2 = i.u2 ) + ) ] // Hexagon V60/V61 Programmer's Reference Manual p. 26 @@ -1420,17 +1412,16 @@ instruction set architecture QDSP6 = // 0. In memory, instructions in a packet must appear in strictly decreasing slot order. // Additionally, if an instruction can go in a higher-numbered slot, and that slot is empty, // then it must be moved into the higher-numbered slot. - // TODO: Reenable this annotation and group definition - // [ assert : VLIW.length <= 4 ] - // group VLIW = ( - // ( - // ( XTYPE<0..1> | ALU32<0..1> | J<0..1> | CR<0..1> ). - // ( XTYPE<0..1> | ALU32<0..1> | J<0..1> | JR<0..1> | CR23<0..1> ). - // ( LD<0..1> | ST<0..1> | ALU32<0..1> ). - // ( LD<0..1> | ST<0..1> | ALU32<0..1> /* | MEMOP<0..1> | NV<0..1> | SYSTEM<0..1> */) - // ) - // | SYSTEMSolo - // ) + [ assert : VLIW.length <= 4 ] + group VLIW = ( + ( + ( XTYPE<0..1> | ALU32<0..1> | J<0..1> | CR<0..1> ). + ( XTYPE<0..1> | ALU32<0..1> | J<0..1> | JR<0..1> | CR23<0..1> ). + ( LD<0..1> | ST<0..1> | ALU32<0..1> ). + ( LD<0..1> | ST<0..1> | ALU32<0..1> /* | MEMOP<0..1> | NV<0..1> | SYSTEM<0..1> */) + ) + | SYSTEMSolo + ) }