1//===-- LLZKTransformationPasses.td ------------------------*- tablegen -*-===//
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
8//===----------------------------------------------------------------------===//
10#ifndef LLZK_TRANSFORMATION_PASSES_TD
11#define LLZK_TRANSFORMATION_PASSES_TD
13include "llzk/Pass/PassBase.td"
15def RedundantReadAndWriteEliminationPass
16 : LLZKPass<"llzk-duplicate-read-write-elim"> {
17 let summary = "Remove redundant reads and writes";
19 Remove redundant or unnecessary reads and writes to struct members, arrays,
20 globals, and RAM. Global writes are removed when they are overwritten or
21 write an already-known value. RAM stores require the same translated address
24 Struct-member accesses match only when the base, member, table offset,
25 affine map metadata, and translated affine operands match. Omitted
26 member-read offsets and member writes denote the current row.
28 Stateful reads are reused when the current analysis state proves the read
29 observes the same value. Writes and stores update that known state, while
30 unknown or non-read state effects invalidate it.
34def RedundantOperationEliminationPass : LLZKPass<"llzk-duplicate-op-elim"> {
35 let summary = "Remove redundant operations";
37 Remove equivalent memory-effect-free operations and duplicate LLZK constraints.
39 Pass should be run after `llzk-duplicate-read-write-elim` for maximum effect.
43def UnusedDeclarationEliminationPass
44 : LLZKPass<"llzk-unused-declaration-elim"> {
45 let summary = "Remove unused member and struct declarations";
47 Remove member and struct declarations that are unused within the current compilation
48 unit. Note that this pass may cause linking issues with external modules that
49 depend on any unused member and struct declarations from this compilation unit.
51 Pass should be run after `llzk-duplicate-read-write-elim`
52 and `llzk-duplicate-op-elim` for maximum effect.
54 let options = [Option<"removeStructs", "remove-structs", "bool",
55 /* default */ "false",
56 "Whether to remove unused struct definitions as well. "
57 "Requires module to declare a Main component, "
58 "otherwise all components will appear unused.">,
62def RemoveUnusedDiscardableAllocationsPass
63 : LLZKPass<"llzk-remove-unused-discardable-allocations"> {
64 let summary = "Remove unread discardable allocations and their dead stores";
66 Remove ops with the selected allocator operation name when they are marked with
67 `MemAlloc<DiscardableAllocationResource>`, the allocation has no reads, and every direct user is
68 a discardable allocation accessor that can be erased as a dead store.
70 let options = [Option<
71 "allocatorOpName", "allocator-op", "std::string",
73 "Operation name of the discardable allocator to remove">];
76def PolyLoweringPass : LLZKPass<"llzk-poly-lowering-pass"> {
78 "Lower the degree of all polynomial equations to a specified maximum";
80 Rewrites constraint expressions into an (observationally) equivalent system where the degree of
81 every polynomial is less than or equal to the specified maximum.
83 High-degree subexpressions are factored into auxiliary struct members. The pass also recurses
84 through degree-neutral roots such as `felt.add`, `felt.sub`, and `felt.neg`, so composite
85 equality operands and struct constrain call arguments satisfy their degree bounds.
87 The pass expects already-flattened, straight-line `compute` and `constrain` bodies. Run
88 `llzk-flatten` or another control-flow lowering pass before this pass; nested-region,
89 successor-bearing, or multi-block functions are rejected instead of being rewritten with
90 component-lifetime auxiliary members.
92 This pass is best used on already-flattened input as part of the `-llzk-full-poly-lowering`
93 pipeline, which includes additional cleanup passes to ensure correctness and optimal
96 let options = [Option<"maxDegree", "max-degree", "unsigned",
98 "Maximum degree of constraint polynomials "
99 "(default 2, minimum 2)">,
103def ComputeConstrainToProductPass
104 : LLZKPass<"llzk-compute-constrain-to-product"> {
105 let summary = "Replace separate @compute and @constrain functions in a "
106 "struct with a single @product function";
107 let description = summary;
108 let options = [Option<"rootStruct", "root-struct", "std::string",
109 /* default */ "\"Main\"",
110 "Root struct at which to start alignment "
111 "(default to `@Main`)">];
114def FuseProductLoopsPass : LLZKPass<"llzk-fuse-product-loops"> {
115 let summary = "Fuse matching witness/constraint loops in a @product function";
116 let description = summary;
119def EnforceNoMemberOverwritePass : LLZKPass<"llzk-enforce-no-overwrite"> {
120 let summary = "Checks that every struct member is written exactly once";
122 This pass currently reports an error if any struct member may not be written
123 exactly once (i.e. overwritten or left uninitialized), and does not
124 attempt to perform any repairs (e.g. SSA-ifying overwritten struct
125 members, or default-initializing unwritten members). This pass
126 overapproximates conditionals, and can result in false positives.
130def InlineFreeFunctionsPass : LLZKPass<"llzk-inline-free-functions"> {
131 let summary = "Inline calls to free functions";
133 Inlines `function.call` operations inside `function.def` bodies when the
134 target is a free `function.def` directly inside the pass's root
135 `builtin.module`. Calls to functions in nested or included modules, and
136 calls outside `function.def` bodies, are left unchanged. After inlining,
137 root free functions that have no remaining symbol uses anywhere in the
138 module are erased. This cleanup applies to every non-external root free
139 function, regardless of its symbol visibility or whether any call to it
142 Inlining is best effort: free functions that participate in a call
143 cycle are skipped (inlining one would re-materialize its calls
144 forever). If inlining a callee fails, its remaining calls are left in
145 place with a warning while processing continues with other callees.
149def WhileToForPass : LLZKPass<"llzk-while-to-for"> {
151 "Converts scf.while loops to equivalent scf.for loops when possible";
153 "This pass identifies scf.while loops that have an "
154 "induction variable and a uniform step, and converts them "
155 "to equivalent scf.for loops, which are preferred by some "
156 "analyses. This pass may introduce some spurious felt/index casts which "
157 "should be cleaned up by --canonicalize.";
160#endif // LLZK_TRANSFORMATION_PASSES_TD