Implement operation element-of expression

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
+  )
 }
 
 

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<Type> 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

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();

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<BuiltInTable.BuiltIn> 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.
+   * <br>
+   * Example:
+   * <pre>
+   *   instruction A : IType = ...
+   *   instruction B : IType = ...
+   *
+   *   operation O1 = {A}
+   *   operation O1 = {B}
+   *
+   *   [assert : VLIW(0) ∈ O1]
+   *   group VLIW = (O1|O2)
+   * </pre>
+   */
+  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<BuiltInTable.BuiltIn> operationElementOfPredicates =
+      List.of(OP_ELEM_OF, OP_NOT_ELEM_OF);
+
+  private FrontendBuiltIns() {
+  }
 
   static Stream<BuiltInTable.BuiltIn> builtIns() {
-    return Stream.concat(BuiltInTable.builtIns(), operationEqualityPredicates.stream());
+    return Stream.concat(BuiltInTable.builtIns(), Stream.concat(
+        operationEqualityPredicates.stream(),
+        operationElementOfPredicates.stream()
+    ));
   }
 }

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<InstructionDefinition> 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

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]

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

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<Node> ctx, GroupRef toHandle) {
     throwNotAllowed(toHandle, "group reference expressions");
   }
 
+  @Handler
+  protected void handle(CGenContext<Node> 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;
   }
 }
-
-

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());