PodToScalarPass.cpp File Reference

This file implements the -llzk-pod-to-scalar pass. More...

#include "llzk/Dialect/Array/IR/Dialect.h"
#include "llzk/Dialect/Array/IR/Ops.h"
#include "llzk/Dialect/Array/IR/Types.h"
#include "llzk/Dialect/Bool/IR/Dialect.h"
#include "llzk/Dialect/Bool/IR/Ops.h"
#include "llzk/Dialect/Bool/Transforms/TransformationPasses.h"
#include "llzk/Dialect/Cast/IR/Dialect.h"
#include "llzk/Dialect/Constrain/IR/Dialect.h"
#include "llzk/Dialect/Constrain/IR/Ops.h"
#include "llzk/Dialect/Felt/IR/Dialect.h"
#include "llzk/Dialect/Function/IR/Dialect.h"
#include "llzk/Dialect/Function/IR/Ops.h"
#include "llzk/Dialect/Include/IR/Dialect.h"
#include "llzk/Dialect/LLZK/IR/Dialect.h"
#include "llzk/Dialect/LLZK/IR/Ops.h"
#include "llzk/Dialect/POD/IR/Dialect.h"
#include "llzk/Dialect/POD/IR/Ops.h"
#include "llzk/Dialect/POD/IR/Types.h"
#include "llzk/Dialect/POD/Transforms/TransformationPasses.h"
#include "llzk/Dialect/Polymorphic/IR/Dialect.h"
#include "llzk/Dialect/Polymorphic/IR/Ops.h"
#include "llzk/Dialect/Polymorphic/Transforms/TransformationPasses.h"
#include "llzk/Dialect/RAM/IR/Dialect.h"
#include "llzk/Dialect/String/IR/Dialect.h"
#include "llzk/Dialect/Struct/IR/Ops.h"
#include "llzk/Transforms/LLZKConversionUtils.h"
#include "llzk/Transforms/LLZKTransformationPasses.h"
#include "llzk/Transforms/SpecializedMemoryPasses.h"
#include "llzk/Util/Concepts.h"
#include "llzk/Util/TypeHelper.h"
#include "llzk/Util/Walk.h"
#include <mlir/Dialect/SCF/IR/SCF.h>
#include <mlir/Dialect/SCF/Transforms/Patterns.h>
#include <mlir/Pass/PassManager.h>
#include <mlir/Transforms/DialectConversion.h>
#include <mlir/Transforms/GreedyPatternRewriteDriver.h>
#include <mlir/Transforms/Passes.h>
#include <llvm/ADT/DenseMapInfo.h>
#include <llvm/ADT/STLExtras.h>
#include <llvm/ADT/TypeSwitch.h>
#include <llvm/Support/Debug.h>
#include <llvm/Support/raw_ostream.h>
#include <functional>
#include <limits>
#include <optional>
#include "llzk/Dialect/POD/Transforms/TransformationPasses.h.inc"

Include dependency graph for PodToScalarPass.cpp:

Go to the source code of this file.

Classes
class	llzk::pod::impl::PodToScalarPassBase< DerivedT >
struct	llvm::DenseMapInfo< RecordChain >
struct	llvm::DenseMapInfo< CompatiblePodLeafMaterializationKey >

Namespaces
namespace	llzk
namespace	llzk::pod
namespace	llzk::pod::impl
namespace	llvm

Macros
#define	GEN_PASS_DEF_PODTOSCALARPASS
#define	DEBUG_TYPE   "llzk-pod-to-scalar"

Functions
std::unique_ptr<::mlir::Pass >	llzk::pod::impl::createPodToScalarPass ()
std::unique_ptr<::mlir::Pass >	llzk::pod::createPodToScalarPass ()

Detailed Description

This file implements the -llzk-pod-to-scalar pass.

The steps of this transformation are as follows:

1. Run preparatory lowering passes, then rewrite pod-typed llzk.nondet ops into pod.new so later stages only need to reason about POD storage through POD dialect operations.
2. Run a dialect conversion that replaces pod-typed struct members with one scalar member per POD record, replaces array-typed struct members whose element type is a POD with one parallel array member per POD record, and remembers how each original member was split for the later rewriting steps.
3. Run a dialect conversion that splits arrays whose element type is a POD into parallel arrays in llzk.nondet, array.*, constrain.eq, constrain.in, struct.readm, struct.writem, function.def, function.call, and function.return.
4. Run a dialect conversion that does the following:
   • Replace MemberReadOp and MemberWriteOp targeting the pod-typed struct members split in step 1 so they instead perform reads and writes on the new scalar members. Reads and writes are tracked through virtual POD placeholders so the conversion can keep propagating scalar leaves instead of re-introducing aggregate POD storage.
   • Remove optional initialization from NewPodOp and instead insert a list of WritePodOp immediately following.
   • Split remaining direct POD values to scalars in FuncDefOp, CallOp, and ReturnOp. When a rewritten op still needs POD contents locally, keep them in the same virtual placeholder form for as long as possible and only materialize concrete pod.write operations as a fallback for unresolved uses.
5. Promote pod reads and writes out of scf.if, scf.for, and scf.while regions when the access can be modeled as an SSA value flowing through the region boundary. This puts the pod accesses that mem2reg must eliminate into a parent block or loop-carried value.
6. Run MLIR "sroa" pass to split remaining POD allocations into single-record POD allocations (to prepare for the "mem2reg" pass because its API cannot split memory by itself).
7. Run MLIR "mem2reg" pass to convert all single-record POD allocations and accesses into SSA values.
8. Remove POD allocations that become unread after memory promotion, then remove SSA values made dead by that cleanup.

Steps 5-7 are rerun while nested POD types are still being exposed, until a fixpoint.

Note: This transformation imposes a "last write wins" semantics on pod records. If different/configurable semantics are added in the future, some additional transformation would be necessary before/during this pass so that multiple writes to the same record can be handled properly while they still exist.

Note: This transformation will introduce a nondet op when there exists a read from a pod record that was not earlier written to.

Terminology: A "virtual POD" is a POD-typed placeholder whose contents are represented by SSA values for each flattened leaf record rather than by explicit pod.write operations on an aggregate POD object. The pass uses virtual PODs to keep propagating scalar leaves through rewrites for as long as possible because that avoids re-introducing aggregate POD storage that later stages would need to split or promote again. Concrete POD storage is materialized only when some remaining use cannot be resolved from those leaf values directly.

Definition in file PodToScalarPass.cpp.

Macro Definition Documentation

DEBUG_TYPE

#define DEBUG_TYPE   "llzk-pod-to-scalar"

Definition at line 137 of file PodToScalarPass.cpp.

GEN_PASS_DEF_PODTOSCALARPASS

#define GEN_PASS_DEF_PODTOSCALARPASS

Definition at line 125 of file PodToScalarPass.cpp.