LLZK 0.1.0
Veridise's ZK Language IR
Loading...
Searching...
No Matches
LLZKValidationPasses.cpp
Go to the documentation of this file.
1//===-- LLZKValidationPasses.cpp - LLZK validation passes -------*- C++ -*-===//
2//
3// Part of the LLZK Project, under the Apache License v2.0.
4// See LICENSE.txt for license information.
5// Copyright 2025 Veridise Inc.
6// SPDX-License-Identifier: Apache-2.0
7//
8//===----------------------------------------------------------------------===//
14//===----------------------------------------------------------------------===//
15
18
19#include <mlir/IR/BuiltinOps.h>
21// Include the generated base pass class definitions.
22namespace llzk {
23#define GEN_PASS_DEF_FIELDWRITEVALIDATORPASS
25} // namespace llzk
27using namespace mlir;
28using namespace llzk;
29using namespace llzk::component;
30using namespace llzk::function;
31
32namespace {
33class FieldWriteValidatorPass
34 : public llzk::impl::FieldWriteValidatorPassBase<FieldWriteValidatorPass> {
35 void runOnOperation() override {
36 StructDefOp structDef = getOperation();
37 FuncDefOp computeFunc = structDef.getComputeFuncOp();
38
39 // Initialize map with all field names mapped to nullptr (i.e., no write found).
40 llvm::StringMap<FieldWriteOp> fieldNameToWriteOp;
41 for (FieldDefOp x : structDef.getFieldDefs()) {
42 fieldNameToWriteOp[x.getSymName()] = nullptr;
43 }
44 // Search the function body for writes, store them in the map and emit warning if multiple
45 // writes to the same field are found.
46 for (Block &block : computeFunc.getBody()) {
47 for (Operation &op : block) {
48 if (FieldWriteOp write = dyn_cast<FieldWriteOp>(op)) {
49 // FieldWriteOp::verifySymbolUses() ensures FieldWriteOp only target the containing "self"
50 // struct. That means the target of the FieldWriteOp must be in `fieldNameToWriteOp` so
51 // using 'at()' will not abort.
52 assert(structDef.getType() == write.getComponent().getType());
53 StringRef writeToFieldName = write.getFieldName();
54 if (FieldWriteOp earlierWrite = fieldNameToWriteOp.at(writeToFieldName)) {
55 auto diag = write.emitWarning().append(
56 "found multiple writes to '", FieldDefOp::getOperationName(), "' named \"@",
57 writeToFieldName, '"'
58 );
59 diag.attachNote(earlierWrite.getLoc()).append("earlier write here");
60 diag.report();
61 }
62 fieldNameToWriteOp[writeToFieldName] = write;
63 }
64 }
65 }
66 // Finally, report a warning if any field was not written at all.
67 for (auto &[a, b] : fieldNameToWriteOp) {
68 if (!b) {
69 computeFunc.emitWarning()
70 .append(
72 "\" missing write to '", FieldDefOp::getOperationName(), "' named \"@", a, '"'
73 )
74 .report();
75 }
76 }
77
78 markAllAnalysesPreserved();
79 }
80};
81} // namespace
82
83std::unique_ptr<mlir::Pass> llzk::createFieldWriteValidatorPass() {
84 return std::make_unique<FieldWriteValidatorPass>();
85};
static constexpr ::llvm::StringLiteral getOperationName()
Definition Ops.h.inc:332
StructType getType(::std::optional<::mlir::ArrayAttr > constParams={})
Gets the StructType representing this struct.
::std::vector< FieldDefOp > getFieldDefs()
Get all FieldDefOp in this structure.
Definition Ops.cpp:413
::llzk::function::FuncDefOp getComputeFuncOp()
Gets the FuncDefOp that defines the compute function in this structure, if present,...
Definition Ops.cpp:423
static constexpr ::llvm::StringLiteral getOperationName()
Definition Ops.h.inc:571
::mlir::Region & getBody()
Definition Ops.h.inc:595
constexpr char FUNC_NAME_COMPUTE[]
Symbol name for the witness generation (and resp.
Definition Constants.h:27
std::unique_ptr< mlir::Pass > createFieldWriteValidatorPass()