verifier

Signed-off-by: Pietro Ghiglio <[email protected]>

Author: PietroGhg

include/p4mlir/Dialect/BMv2IR/BMv2IR_OpInterfaces.h

@@ -0,0 +1,9 @@
+#ifndef P4MLIR_DIALECT_BMv2IR_BMv2IR_OPINTERFACES_H
+#define P4MLIR_DIALECT_BMv2IR_BMv2IR_OPINTERFACES_H
+
+#include "mlir/IR/OpDefinition.h"
+
+#include "p4mlir/Dialect/BMv2IR/BMv2IR_OpInterfaces.h.inc"
+
+#endif  // P4MLIR_DIALECT_BMv2IR_BMv2IR_OPINTERFACES_H
+

include/p4mlir/Dialect/BMv2IR/BMv2IR_OpInterfaces.td

@@ -0,0 +1,27 @@
+#ifndef BMv2IR_OP_INTERFACES_TD
+#define BMv2IR_OP_INTERFACES_TD
+
+include "mlir/IR/OpBase.td"
+include "mlir/IR/Interfaces.td"
+
+def AllowedTransitionKey : OpInterface<"AllowedTransitionKey"> {
+  let description = [{
+    Common interfaces for operations that could be used as transition keys
+  }];
+  let methods = [];
+
+
+  let cppNamespace = "::P4::P4MLIR::BMv2IR";
+}
+
+def AllowedParserOp : OpInterface<"AllowedParserOp"> {
+  let description = [{
+    Common interfaces for operations that could be used as parser ops
+  }];
+  let methods = [];
+
+
+  let cppNamespace = "::P4::P4MLIR::BMv2IR";
+}
+
+#endif

include/p4mlir/Dialect/BMv2IR/BMv2IR_Ops.h

@@ -11,8 +11,8 @@
 #include "mlir/IR/OpDefinition.h"
 #include "mlir/IR/SymbolTable.h"
 #include "p4mlir/Dialect/BMv2IR/BMv2IR_Attrs.h"
+#include "p4mlir/Dialect/BMv2IR/BMv2IR_OpInterfaces.h"
 #include "p4mlir/Dialect/BMv2IR/BMv2IR_Types.h"
-
 #define GET_OP_CLASSES
 #include "p4mlir/Dialect/BMv2IR/BMv2IR_Ops.h.inc"
 

include/p4mlir/Dialect/BMv2IR/BMv2IR_Ops.td

@@ -8,6 +8,7 @@ include "mlir/IR/SymbolInterfaces.td"
 include "p4mlir/Dialect/BMv2IR/BMv2IR_Dialect.td"
 include "p4mlir/Dialect/BMv2IR/BMv2IR_Types.td"
 include "p4mlir/Dialect/BMv2IR/BMv2IR_Attrs.td"
+include "p4mlir/Dialect/BMv2IR/BMv2IR_OpInterfaces.td"
 
 //===----------------------------------------------------------------------===//
 // Base BMv2IR operation definition.
@@ -69,6 +70,8 @@ def BMv2IR_ParserStateOp : BMv2IR_Op<"state",
     `\n``transitions` $transitions
     `\n``parser_ops` $parser_ops attr-dict
   }];
+
+  let hasVerifier = 1;
 }
 
 def BMv2IR_TransitionOp : BMv2IR_Op<"transition", [HasParent<"ParserStateOp">]> {
@@ -102,7 +105,7 @@ def BMv2IR_TransitionOp : BMv2IR_Op<"transition", [HasParent<"ParserStateOp">]>
 }
 
 
-def BMv2_ExtractOp : BMv2IR_Op<"extract", [HasParent<"ParserStateOp">]> {
+def BMv2_ExtractOp : BMv2IR_Op<"extract", [HasParent<"ParserStateOp">, AllowedParserOp]> {
   let summary = "Extract header operation";
   let description = [{
     Extracts the field of a header instance, header stack, or union stack element.
@@ -129,7 +132,7 @@ def BMv2_ExtractOp : BMv2IR_Op<"extract", [HasParent<"ParserStateOp">]> {
 // see https://github.com/p4lang/behavioral-model/blob/main/docs/JSON_format.md#the-type-value-object
 //===-------------------------------------------------------------------------------------------===//
 
-def BMv2IR_FieldOp : BMv2IR_Op<"field"> {
+def BMv2IR_FieldOp : BMv2IR_Op<"field", [AllowedTransitionKey]> {
   let summary = "BMv2 header field access";
   let description = [{
     Represents access to a field within a header instance.
@@ -144,7 +147,7 @@ def BMv2IR_FieldOp : BMv2IR_Op<"field"> {
   let assemblyFormat = "`<` $headerInstance `,` $fieldMember `>` attr-dict";
 }
 
-def BMv2_StackFieldOp : BMv2IR_Op<"stack_field"> {
+def BMv2_StackFieldOp : BMv2IR_Op<"stack_field", [AllowedTransitionKey]> {
   let summary = "BMv2 header stack field access";
   let description = [{
     Represents access to a field in the last valid header instance in a stack.
@@ -160,7 +163,7 @@ def BMv2_StackFieldOp : BMv2IR_Op<"stack_field"> {
 }
 
 
-def BMv2IR_LookaheadOp : BMv2IR_Op<"lookahead"> {
+def BMv2IR_LookaheadOp : BMv2IR_Op<"lookahead", [AllowedTransitionKey]> {
   let summary = "BMv2 parser lookahead";
   let description = [{
     Represents a lookahead operation in a parser.
@@ -175,7 +178,7 @@ def BMv2IR_LookaheadOp : BMv2IR_Op<"lookahead"> {
   let assemblyFormat = "`<` $bitOffset `,` $bitwidth `>` attr-dict";
 }
 
-def BMv2_UnionStackFieldOp : BMv2IR_Op<"union_stack_field"> {
+def BMv2_UnionStackFieldOp : BMv2IR_Op<"union_stack_field", [AllowedTransitionKey]> {
   let summary = "BMv2 header union stack field access";
   let description = [{
     Represents access to a field in the last valid union instance in a stack.

include/p4mlir/Dialect/BMv2IR/CMakeLists.txt

@@ -14,3 +14,9 @@ mlir_tablegen(BMv2IR_EnumAttrs.h.inc -gen-enum-decls)
 mlir_tablegen(BMv2IR_EnumAttrs.cpp.inc -gen-enum-defs)
 add_public_tablegen_target(P4MLIR_BMv2IR_AttrIncGen)
 add_dependencies(mlir-headers P4MLIR_BMv2IR_AttrIncGen)
+
+set(LLVM_TARGET_DEFINITIONS BMv2IR_OpInterfaces.td)
+mlir_tablegen(BMv2IR_OpInterfaces.h.inc -gen-op-interface-decls)
+mlir_tablegen(BMv2IR_OpInterfaces.cpp.inc -gen-op-interface-defs)
+add_public_tablegen_target(P4MLIR_BMv2IR_OpsInterfacesIncGen)
+add_dependencies(mlir-headers P4MLIR_BMv2IR_OpsInterfacesIncGen)

lib/Conversion/P4HIRToBMv2IR/P4HIRToBMv2IR.cpp

@@ -97,7 +97,7 @@ struct ParserStateOpConversionPattern : public OpConversionPattern<P4HIR::Parser
         op.walk([&](P4HIR::ParserTransitionSelectOp transitionSelectOp) {
             for (auto operand : transitionSelectOp.getArgs()) {
                 auto transitionKey =
-                    insertTransitionKey(operand.getDefiningOp(), rewriter, &keysBlock);
+                    insertTransitionKey(operand.getDefiningOp(), rewriter, &keysBlock, eraseList);
                 transitionInserted &= transitionKey != nullptr;
             }
 
@@ -145,7 +145,7 @@ struct ParserStateOpConversionPattern : public OpConversionPattern<P4HIR::Parser
 
  private:
     static Operation *insertTransitionKey(Operation *op, ConversionPatternRewriter &rewriter,
-                                          Block *block) {
+                                          Block *block, SmallVector<Operation*>& eraseList) {
         auto loc = op->getLoc();
         if (auto lookAheadOp = dyn_cast<P4CoreLib::PacketLookAheadOp>(op)) {
             // TODO: not sure how to handle offsets
@@ -155,6 +155,7 @@ struct ParserStateOpConversionPattern : public OpConversionPattern<P4HIR::Parser
             auto width = rewriter.getI32IntegerAttr(bitTy.getWidth());
             ConversionPatternRewriter::InsertionGuard guard(rewriter);
             rewriter.setInsertionPointToEnd(block);
+            eraseList.push_back(lookAheadOp);
             return rewriter.create<BMv2IR::LookaheadOp>(loc, offset, width);
         }
         llvm_unreachable("Unsupported operand");

lib/Dialect/BMv2IR/BMv2IR_Ops.cpp

@@ -2,10 +2,37 @@
 
 #include "mlir/IR/Builders.h"
 #include "p4mlir/Dialect/BMv2IR/BMv2IR_Dialect.h"
+#include "p4mlir/Dialect/BMv2IR/BMv2IR_OpInterfaces.h"
 
-using namespace P4::P4MLIR;
+using namespace mlir;
+using namespace P4::P4MLIR::BMv2IR;
 
-void BMv2IR::BMv2IRDialect::initialize() {
+LogicalResult ParserStateOp::verify() {
+    // Check that only allowed ops are used as transition keys, transitions and parser ops
+
+    for (auto &block : getTransitionKeys()) {
+        for (auto &op : block) {
+            if (!isa<AllowedTransitionKey>(op)) {
+                return emitError("Op not allowed as transition key");
+            }
+        }
+    }
+
+    for (auto &block : getTransitions()) {
+        for (auto &op : block) {
+            if (!isa<TransitionOp>(op)) return emitError("Op not allowed as transition");
+        }
+    }
+
+    for (auto &block : getParserOps()) {
+        for (auto &op : block) {
+            if (!isa<AllowedParserOp>(op)) return emitError("Op not allowed as parser op");
+        }
+    }
+    return success();
+}
+
+void BMv2IRDialect::initialize() {
     registerTypes();
     registerAttributes();
     addOperations<

test/Conversion/BMv2IR/parser.mlir

@@ -58,7 +58,6 @@ module {
 // CHECK:      bmv2ir.transition type  default, @prs::@parse_bottom
 // CHECK:    }
 // CHECK:     parser_ops {
-// CHECK:      %lookahead = p4corelib.packet_lookahead %arg0 : !p4corelib.packet_in -> !b8i
 // CHECK:    }
     p4hir.state @parse_one {
       %one_field_ref = p4hir.struct_field_ref %arg1["one"] : <!Headers_t>