[Formal][PropertyAnnotation] Annotating SingleEntryToken invariant

experimental/include/experimental/Support/FormalProperty.h

@@ -33,6 +33,8 @@ class FormalProperty {
     EagerForkNotAllOutputSent,
     CopiedSlotsOfActiveForksAreFull,
     ReconvergentPathFlow,
+    EntryTokenOrder,
+    SingleEntryToken,
   };
 
   TAG getTag() const { return tag; }
@@ -271,6 +273,58 @@ class ReconvergentPathFlow : public FormalProperty {
   inline static const StringLiteral EQUATIONS_LIT = "equations";
 };
 
+class EntryTokenOrder : public FormalProperty {
+public:
+  const std::vector<EffectiveSlotNamer> &getSlots() const { return slots; }
+  int32_t getValue() const { return entryValue; }
+  llvm::json::Value extraInfoToJSON() const override;
+  static std::unique_ptr<EntryTokenOrder>
+  fromJSON(const llvm::json::Value &value, llvm::json::Path path);
+  EntryTokenOrder() = default;
+  EntryTokenOrder(unsigned long id, TAG tag,
+                  std::vector<EffectiveSlotNamer> slots, int32_t value)
+      : FormalProperty(id, tag, TYPE::EntryTokenOrder), slots(std::move(slots)),
+        entryValue(value) {}
+  ~EntryTokenOrder() = default;
+
+  static bool classof(const FormalProperty *fp) {
+    return fp->getType() == TYPE::EntryTokenOrder;
+  }
+
+private:
+  std::vector<EffectiveSlotNamer> slots;
+  int32_t entryValue;
+  inline static const StringLiteral SLOTS_LIT = "slots";
+  inline static const StringLiteral ENTRY_VALUE_LIT = "entry_value";
+};
+
+class SingleEntryToken : public FormalProperty {
+public:
+  const std::vector<EffectiveSlotNamer> &getEcPath() const { return ec; }
+  const std::vector<EffectiveSlotNamer> &getCmPath() const { return cm; }
+
+  llvm::json::Value extraInfoToJSON() const override;
+  static std::unique_ptr<SingleEntryToken>
+  fromJSON(const llvm::json::Value &value, llvm::json::Path path);
+  SingleEntryToken() = default;
+  SingleEntryToken(unsigned long id, TAG tag,
+                   std::vector<EffectiveSlotNamer> ec,
+                   std::vector<EffectiveSlotNamer> cm)
+      : FormalProperty(id, tag, TYPE::SingleEntryToken), ec(std::move(ec)),
+        cm(std::move(cm)) {}
+  ~SingleEntryToken() = default;
+
+  static bool classof(const FormalProperty *fp) {
+    return fp->getType() == TYPE::SingleEntryToken;
+  }
+
+private:
+  std::vector<EffectiveSlotNamer> ec;
+  std::vector<EffectiveSlotNamer> cm;
+  inline static const StringLiteral PATH_EC_LIT = "entry_cmerge_path";
+  inline static const StringLiteral PATH_CM_LIT = "cmerge_mux_path";
+};
+
 class FormalPropertyTable {
 public:
   FormalPropertyTable() = default;

experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp

@@ -84,6 +84,10 @@ struct HandshakeAnnotatePropertiesPass
   LogicalResult annotateCopiedSlots(Operation &op);
   LogicalResult annotateCopiedSlotsOfAllForks(ModuleOp modOp);
   LogicalResult annotateReconvergentPathFlow(ModuleOp modOp);
+  LogicalResult annotateEntryTokenOrderPaths(ControlMergeOp cmerge,
+                                             int32_t entryValue);
+  LogicalResult annotateEntryTokenOrder(ModuleOp modOp);
+  LogicalResult annotateSingleEntryToken(ModuleOp modOp);
 };
 
 bool isChannelToBeChecked(OpResult res) {
@@ -290,6 +294,174 @@ HandshakeAnnotatePropertiesPass::annotateReconvergentPathFlow(ModuleOp modOp) {
   return success();
 }
 
+namespace {
+struct EntryCMergePath {
+  std::vector<EffectiveSlotNamer> slots;
+  ControlMergeOp cmerge;
+  int32_t entryValue;
+};
+std::vector<EntryCMergePath> findEntryCMergePaths(BlockArgument startChannel) {
+  struct PartialPath {
+    std::vector<EffectiveSlotNamer> slots;
+    mlir::Value cur;
+  };
+  std::vector<EntryCMergePath> ret;
+  std::vector<PartialPath> stack;
+  PartialPath start = {
+      .slots = {},
+      .cur = startChannel,
+  };
+  // TODO: Make this an entry slot (which is in a different PR)
+  Operation *op = startChannel.getOwner()->getParentOp();
+  auto nameAttr =
+      op->getAttrOfType<ArrayAttr>("argNames")[startChannel.getArgNumber()];
+  std::string name = dyn_cast<StringAttr>(nameAttr).str();
+  llvm::errs() << name << "\n";
+  start.slots.emplace_back(
+      std::make_unique<BufferSlotFullNamer>(name, "valid", "", 0));
+  stack.push_back(start);
+  while (!stack.empty()) {
+    PartialPath path = std::move(stack.back());
+    stack.pop_back();
+
+    Operation *next = path.cur.getUses().begin()->getOwner();
+    if (auto cmerge = dyn_cast<ControlMergeOp>(next)) {
+      int32_t entry;
+      for (auto [i, input] : llvm::enumerate(cmerge.getDataOperands())) {
+        if (input == path.cur) {
+          entry = i;
+        }
+      }
+      EntryCMergePath retPath = {
+          .slots = path.slots,
+          .cmerge = cmerge,
+          .entryValue = entry,
+      };
+      ret.push_back(retPath);
+    }
+    if (auto buffer = dyn_cast<BufferOp>(next)) {
+      for (auto &slot : buffer.getInternalSlotStateNamers()) {
+        path.slots.emplace_back(std::make_unique<BufferSlotFullNamer>(slot));
+      }
+      path.cur = buffer.getResult();
+      stack.push_back(std::move(path));
+      continue;
+    }
+    if (auto fork = dyn_cast<ForkOp>(next)) {
+      auto sents = fork.getInternalSentStateNamers();
+      for (auto [i, channel] : llvm::enumerate(next->getResults())) {
+        PartialPath nextPath = {
+            .slots = path.slots,
+            .cur = channel,
+        };
+        assert(!nextPath.slots.empty());
+        EffectiveSlotNamer &back = nextPath.slots.back();
+        back.copiedSents.push_back(sents[i]);
+        stack.push_back(nextPath);
+      }
+      continue;
+    }
+  }
+  return ret;
+}
+
+std::vector<std::vector<EffectiveSlotNamer>>
+findCMergeMuxPaths(ControlMergeOp cmerge) {
+  struct PartialPath {
+    std::vector<EffectiveSlotNamer> slots;
+    mlir::Value cur;
+  };
+  std::vector<std::vector<EffectiveSlotNamer>> ret{};
+  std::vector<PartialPath> stack;
+  EffectiveSlotNamer mergeSlot(std::make_unique<BufferSlotFullNamer>(
+      cmerge.getInternalSlotStateNamers()[0]));
+  PartialPath start = {
+      .slots = {},
+      .cur = cmerge.getIndex(),
+  };
+  start.slots.push_back(mergeSlot);
+  stack.push_back(start);
+  while (!stack.empty()) {
+    PartialPath path = stack.back();
+    stack.pop_back();
+
+    Operation *next = path.cur.getUses().begin()->getOwner();
+    if (auto mux = dyn_cast<MuxOp>(next)) {
+      // Path is terminated by MuxOp, so this is the end of the path
+      ret.push_back(std::move(path.slots));
+      continue;
+    }
+    if (auto buffer = dyn_cast<BufferOp>(next)) {
+      for (auto &slot : buffer.getInternalSlotStateNamers()) {
+        path.slots.emplace_back(std::make_unique<BufferSlotFullNamer>(slot));
+      }
+      path.cur = buffer.getResult();
+      stack.push_back(std::move(path));
+      continue;
+    }
+    if (auto fork = dyn_cast<ForkOp>(next)) {
+      auto sents = fork.getInternalSentStateNamers();
+      for (auto [i, channel] : llvm::enumerate(next->getResults())) {
+        PartialPath nextPath = {
+            .slots = path.slots,
+            .cur = channel,
+        };
+        EffectiveSlotNamer &back = nextPath.slots.back();
+        back.copiedSents.push_back(sents[i]);
+        stack.push_back(nextPath);
+      }
+      continue;
+    }
+
+    llvm::report_fatal_error("unexpected op detected");
+  }
+  return ret;
+}
+} // namespace
+
+LogicalResult HandshakeAnnotatePropertiesPass::annotateEntryTokenOrderPaths(
+    ControlMergeOp cmerge, int32_t entryValue) {
+  for (const auto &path : findCMergeMuxPaths(cmerge)) {
+    if (path.size() < 2) {
+      // The regex of this invariant trivially holds for any path of length 1
+      continue;
+    }
+    EntryTokenOrder p(uid++, FormalProperty::TAG::INVAR, path, entryValue);
+    propertyTable.push_back(p.toJSON());
+  }
+  return success();
+}
+
+LogicalResult
+HandshakeAnnotatePropertiesPass::annotateEntryTokenOrder(ModuleOp modOp) {
+  for (auto funcOp : modOp.getOps<handshake::FuncOp>()) {
+    for (BlockArgument arg : funcOp.getRegion().getArguments()) {
+      for (const auto &path : findEntryCMergePaths(arg)) {
+        if (failed(
+                annotateEntryTokenOrderPaths(path.cmerge, path.entryValue))) {
+          return failure();
+        }
+      }
+    }
+  }
+  return success();
+}
+
+LogicalResult
+HandshakeAnnotatePropertiesPass::annotateSingleEntryToken(ModuleOp modOp) {
+  for (auto funcOp : modOp.getOps<handshake::FuncOp>()) {
+    for (BlockArgument arg : funcOp.getRegion().getArguments()) {
+      for (const auto &ec : findEntryCMergePaths(arg)) {
+        for (const auto &cm : findCMergeMuxPaths(ec.cmerge)) {
+          SingleEntryToken p(uid++, FormalProperty::TAG::INVAR, ec.slots, cm);
+          propertyTable.push_back(p.toJSON());
+        }
+      }
+    }
+  }
+  return success();
+}
+
 LogicalResult
 HandshakeAnnotatePropertiesPass::annotateProperty(ModuleOp modOp,
                                                   FormalProperty::TYPE t) {
@@ -304,6 +476,10 @@ HandshakeAnnotatePropertiesPass::annotateProperty(ModuleOp modOp,
     return annotateCopiedSlotsOfAllForks(modOp);
   case FormalProperty::TYPE::ReconvergentPathFlow:
     return annotateReconvergentPathFlow(modOp);
+  case FormalProperty::TYPE::EntryTokenOrder:
+    return annotateEntryTokenOrder(modOp);
+  case FormalProperty::TYPE::SingleEntryToken:
+    return annotateSingleEntryToken(modOp);
   }
   return failure();
 }
@@ -336,6 +512,10 @@ LogicalResult HandshakeAnnotatePropertiesPass::annotateQueriedProperties() {
       return failure();
     if (failed(annotateReconvergentPathFlow(modOp)))
       return failure();
+    if (failed(annotateEntryTokenOrder(modOp)))
+      return failure();
+    if (failed(annotateSingleEntryToken(modOp)))
+      return failure();
   }
   return success();
 }

experimental/lib/Support/FormalProperty.cpp

@@ -33,6 +33,10 @@ FormalProperty::typeFromStr(const std::string &s) {
     return FormalProperty::TYPE::CopiedSlotsOfActiveForksAreFull;
   if (s == "ReconvergentPathFlow")
     return FormalProperty::TYPE::ReconvergentPathFlow;
+  if (s == "EntryTokenOrder")
+    return FormalProperty::TYPE::EntryTokenOrder;
+  if (s == "SingleEntryToken")
+    return FormalProperty::TYPE::SingleEntryToken;
 
   return std::nullopt;
 }
@@ -49,6 +53,10 @@ std::string FormalProperty::typeToStr(TYPE t) {
     return "CopiedSlotsOfActiveForksAreFull";
   case TYPE::ReconvergentPathFlow:
     return "ReconvergentPathFlow";
+  case TYPE::EntryTokenOrder:
+    return "EntryTokenOrder";
+  case TYPE::SingleEntryToken:
+    return "SingleEntryToken";
   }
 }
 
@@ -108,6 +116,10 @@ FormalProperty::fromJSON(const llvm::json::Value &value,
                                                     path.field(INFO_LIT));
   case TYPE::ReconvergentPathFlow:
     return ReconvergentPathFlow::fromJSON(value, path.field(INFO_LIT));
+  case TYPE::EntryTokenOrder:
+    return EntryTokenOrder::fromJSON(value, path.field(INFO_LIT));
+  case TYPE::SingleEntryToken:
+    return SingleEntryToken::fromJSON(value, path.field(INFO_LIT));
   }
 }
 
@@ -362,6 +374,43 @@ ReconvergentPathFlow::fromJSON(const llvm::json::Value &value,
   return prop;
 }
 
+llvm::json::Value EntryTokenOrder::extraInfoToJSON() const {
+  return llvm::json::Object(
+      {{SLOTS_LIT, slots}, {ENTRY_VALUE_LIT, entryValue}});
+}
+
+std::unique_ptr<EntryTokenOrder>
+EntryTokenOrder::fromJSON(const llvm::json::Value &value,
+                          llvm::json::Path path) {
+  auto prop = std::make_unique<EntryTokenOrder>();
+
+  llvm::json::Value info = prop->parseBaseAndExtractInfo(value, path);
+  llvm::json::ObjectMapper mapper(info, path);
+
+  if (!mapper || !mapper.map(SLOTS_LIT, prop->slots) ||
+      !mapper.map(ENTRY_VALUE_LIT, prop->entryValue))
+    return nullptr;
+  return prop;
+}
+
+llvm::json::Value SingleEntryToken::extraInfoToJSON() const {
+  return llvm::json::Object({{PATH_CM_LIT, cm}, {PATH_EC_LIT, ec}});
+}
+
+std::unique_ptr<SingleEntryToken>
+SingleEntryToken::fromJSON(const llvm::json::Value &value,
+                           llvm::json::Path path) {
+  auto prop = std::make_unique<SingleEntryToken>();
+
+  llvm::json::Value info = prop->parseBaseAndExtractInfo(value, path);
+  llvm::json::ObjectMapper mapper(info, path);
+
+  if (!mapper || !mapper.map(PATH_CM_LIT, prop->cm) ||
+      !mapper.map(PATH_EC_LIT, prop->ec))
+    return nullptr;
+  return prop;
+}
+
 LogicalResult FormalPropertyTable::addPropertiesFromJSON(StringRef filepath) {
   // Open the properties' database
   std::ifstream inputFile(filepath.str());