diff --git a/include/revng/ABI/FunctionType/Layout.h b/include/revng/ABI/FunctionType/Layout.h
index 830cc9699..ea304e44f 100644
--- a/include/revng/ABI/FunctionType/Layout.h
+++ b/include/revng/ABI/FunctionType/Layout.h
@@ -11,6 +11,7 @@
 #include "revng/ABI/Definition.h"
 #include "revng/ADT/STLExtras.h"
 #include "revng/Model/Binary.h"
+#include "revng/Support/YAMLTraits.h"
 
 namespace abi::FunctionType {
 
@@ -88,12 +89,11 @@ public:
 
   public:
     struct StackSpan {
-      uint64_t Offset;
-      uint64_t Size;
-
-      StackSpan operator+(uint64_t Offset) const {
-        return { this->Offset + Offset, Size };
-      }
+      /// The offset should be interpreted as an offset within the struct
+      /// containing the stack arguments. It's not an offset from some reference
+      /// stack pointer value.
+      uint64_t Offset = 0;
+      uint64_t Size = 0;
     };
 
   public:
@@ -196,9 +196,25 @@ public:
   }
 
 public:
-  void dump() const debug_function;
+  void dump() const debug_function { dump(dbg); }
+
+  template<typename T>
+  void dump(T &Stream) const {
+    // TODO: accept an arbitrary stream
+    serialize(Stream, *this);
+  }
 };
 
+inline Layout::Argument::StackSpan
+operator+(const Layout::Argument::StackSpan &This, uint64_t Offset) {
+  return { This.Offset + Offset, This.Size };
+}
+
+inline Layout::Argument::StackSpan
+operator+(uint64_t Offset, const Layout::Argument::StackSpan &This) {
+  return { This.Offset + Offset, This.Size };
+}
+
 inline std::span<const model::Register::Values>
 calleeSavedRegisters(const model::CABIFunctionDefinition &Prototype) {
   return abi::Definition::get(Prototype.ABI()).CalleeSavedRegisters();
@@ -276,3 +292,49 @@ inline UsedRegisters usedRegisters(const model::UpcastableType &FunctionType) {
 }
 
 } // namespace abi::FunctionType
+
+using FTL = abi::FunctionType::Layout;
+namespace FTAK = abi::FunctionType::ArgumentKind;
+
+template<>
+struct llvm::yaml::ScalarEnumerationTraits<FTAK::Values>
+  : public NamedEnumScalarTraits<FTAK::Values> {};
+
+template<>
+struct llvm::yaml::MappingTraits<FTL::Argument::StackSpan> {
+  static void mapping(IO &IO, FTL::Argument::StackSpan &SS) {
+    IO.mapRequired("Offset", SS.Offset);
+    IO.mapRequired("Size", SS.Size);
+  }
+};
+LLVM_YAML_IS_SEQUENCE_VECTOR(FTL::Argument::StackSpan)
+
+template<>
+struct llvm::yaml::MappingTraits<FTL::ReturnValue> {
+  static void mapping(IO &IO, FTL::ReturnValue &RV) {
+    IO.mapRequired("Type", RV.Type);
+    IO.mapRequired("Registers", RV.Registers);
+  }
+};
+LLVM_YAML_IS_SEQUENCE_VECTOR(FTL::ReturnValue)
+
+template<>
+struct llvm::yaml::MappingTraits<FTL::Argument> {
+  static void mapping(IO &IO, FTL::Argument &A) {
+    IO.mapRequired("Type", A.Type);
+    IO.mapRequired("Kind", A.Kind);
+    IO.mapRequired("Registers", A.Registers);
+    IO.mapOptional("Stack", A.Stack);
+  }
+};
+LLVM_YAML_IS_SEQUENCE_VECTOR(FTL::Argument)
+
+template<>
+struct llvm::yaml::MappingTraits<FTL> {
+  static void mapping(IO &IO, FTL &L) {
+    IO.mapRequired("Arguments", L.Arguments);
+    IO.mapRequired("ReturnValues", L.ReturnValues);
+    IO.mapRequired("CalleeSavedRegisters", L.CalleeSavedRegisters);
+    IO.mapRequired("FinalStackOffset", L.FinalStackOffset);
+  }
+};
diff --git a/include/revng/ABI/ModelHelpers.h b/include/revng/ABI/ModelHelpers.h
index 3e1bb3b77..307b41b84 100644
--- a/include/revng/ABI/ModelHelpers.h
+++ b/include/revng/ABI/ModelHelpers.h
@@ -120,14 +120,10 @@ layoutToLLVMFunctionType(llvm::LLVMContext &Context,
     if constexpr (LegacyLocalVariables) {
       ReturnType = TargetPointerSizedInteger;
     } else {
-      if (Layout.hasSPTAR()) {
-        ReturnType = TargetPointerSizedInteger;
-      } else {
-        const model::Type &ReturnAggregate = Layout.returnValueAggregateType();
-        size_t ReturnSize = *ReturnAggregate.size();
-        auto *Int8 = llvm::IntegerType::getInt8Ty(Context);
-        ReturnType = llvm::ArrayType::get(Int8, ReturnSize);
-      }
+      const model::Type &ReturnAggregate = Layout.returnValueAggregateType();
+      size_t ReturnSize = *ReturnAggregate.size();
+      auto *Int8 = llvm::IntegerType::getInt8Ty(Context);
+      ReturnType = llvm::ArrayType::get(Int8, ReturnSize);
     }
   } break;
 
diff --git a/include/revng/ADT/GenericGraph.h b/include/revng/ADT/GenericGraph.h
index c7bb06f48..a5832af2a 100644
--- a/include/revng/ADT/GenericGraph.h
+++ b/include/revng/ADT/GenericGraph.h
@@ -1615,8 +1615,9 @@ struct GraphTraits<llvm::Inverse<T *>>
                                             typename T::nodes_iterator>;
 
   static NodeRef getEntryNode(llvm::Inverse<T *> Inv) {
-    // TODO: we might want to consider an option of having optional
-    // `ExitNode`s as well, for consistency.
+    // NOTE: this is clearly misguided, however it's coherent with what happens
+    //       for Inverse<llvm::Function *>.
+    //       Don't use this.
     return Inv.Graph->getEntryNode();
   }
 
diff --git a/include/revng/ADT/ReversePostOrderTraversal.h b/include/revng/ADT/ReversePostOrderTraversal.h
index a60980b0e..72fe7147a 100644
--- a/include/revng/ADT/ReversePostOrderTraversal.h
+++ b/include/revng/ADT/ReversePostOrderTraversal.h
@@ -16,8 +16,9 @@ class ReversePostOrderTraversalExt {
   NodeVec Blocks; // Block list in normal RPO order
 
   void initialize(GraphT G, SetType &WhiteList) {
-    std::copy(po_ext_begin(G, WhiteList),
-              po_ext_end(G, WhiteList),
+    using ExtIter = llvm::po_ext_iterator<GraphT, SetType, GT>;
+    std::copy(ExtIter::begin(G, WhiteList),
+              ExtIter::end(G, WhiteList),
               std::back_inserter(Blocks));
   }
 
diff --git a/include/revng/FunctionIsolation/StructInitializers.h b/include/revng/FunctionIsolation/StructInitializers.h
index bd5b88fbc..2e787b9f3 100644
--- a/include/revng/FunctionIsolation/StructInitializers.h
+++ b/include/revng/FunctionIsolation/StructInitializers.h
@@ -14,11 +14,16 @@ class StructInitializers {
 private:
   OpaqueFunctionsPool<llvm::StructType *> Pool;
   llvm::LLVMContext &Context;
+  bool EmitBody = true;
 
 public:
-  StructInitializers(llvm::Module *M);
+  StructInitializers(llvm::Module *M, bool EmitBody = true);
 
 public:
+  llvm::CallInst *createCall(revng::IRBuilder &Builder,
+                             llvm::StructType *ReturnType,
+                             llvm::ArrayRef<llvm::Value *> Values);
+
   llvm::Instruction *createReturn(revng::IRBuilder &Builder,
                                   llvm::ArrayRef<llvm::Value *> Values);
 };
diff --git a/include/revng/MFP/DOTGraphTraits.h b/include/revng/MFP/DOTGraphTraits.h
index ab8d18509..76803bb2f 100644
--- a/include/revng/MFP/DOTGraphTraits.h
+++ b/include/revng/MFP/DOTGraphTraits.h
@@ -13,9 +13,9 @@ namespace llvm {
 class Instruction;
 }
 
-template<MFP::MonotoneFrameworkInstance MFI>
-struct llvm::DOTGraphTraits<const MFP::Graph<MFI> *> {
-  using GraphType = const MFP::Graph<MFI> *;
+template<mfp::MonotoneFrameworkInstance MFI>
+struct llvm::DOTGraphTraits<const mfp::Graph<MFI> *> {
+  using GraphType = const mfp::Graph<MFI> *;
   using UnderlyingGraphType = MFI::GraphType;
   using UnderlyingDOTGraphTraits = llvm::DOTGraphTraits<UnderlyingGraphType>;
   using NodeRef = llvm::GraphTraits<GraphType>::NodeRef;
@@ -63,7 +63,7 @@ struct llvm::DOTGraphTraits<const MFP::Graph<MFI> *> {
           llvm::raw_string_ostream Stream(Result);
           Stream << Name.str() << " value:"
                  << "\n";
-          MFP::dump(Stream, 1, ToDump);
+          mfp::dump(Stream, 1, ToDump);
         }
 
         replaceAll(Result, "\n", Newline);
@@ -141,6 +141,6 @@ struct llvm::DOTGraphTraits<const MFP::Graph<MFI> *> {
   }
 };
 
-template<MFP::MonotoneFrameworkInstance MFI>
-struct llvm::DOTGraphTraits<MFP::Graph<MFI> *>
-  : llvm::DOTGraphTraits<const MFP::Graph<MFI> *> {};
+template<mfp::MonotoneFrameworkInstance MFI>
+struct llvm::DOTGraphTraits<mfp::Graph<MFI> *>
+  : llvm::DOTGraphTraits<const mfp::Graph<MFI> *> {};
diff --git a/include/revng/MFP/Graph.h b/include/revng/MFP/Graph.h
index d9064964b..db9d4310c 100644
--- a/include/revng/MFP/Graph.h
+++ b/include/revng/MFP/Graph.h
@@ -6,7 +6,7 @@
 
 #include "revng/MFP/MFP.h"
 
-namespace MFP {
+namespace mfp {
 
 template<MonotoneFrameworkInstance MFI>
 class Graph {
@@ -28,12 +28,12 @@ public:
   const auto &results() const { return Results; }
 };
 
-} // namespace MFP
+} // namespace mfp
 
 /// \note This implementation of GraphTraits forwards everything 1-to-1
-template<MFP::MonotoneFrameworkInstance MFI>
-struct llvm::GraphTraits<MFP::Graph<MFI> *> {
-  using GraphType = MFP::Graph<MFI> *;
+template<mfp::MonotoneFrameworkInstance MFI>
+struct llvm::GraphTraits<mfp::Graph<MFI> *> {
+  using GraphType = mfp::Graph<MFI> *;
   using UnderlyingGraphTraits = llvm::GraphTraits<typename MFI::GraphType>;
   using NodeRef = typename UnderlyingGraphTraits::NodeRef;
   using EdgeRef = typename UnderlyingGraphTraits::EdgeRef;
@@ -76,9 +76,9 @@ struct llvm::GraphTraits<MFP::Graph<MFI> *> {
 };
 
 /// \note This implementation of GraphTraits forwards everything 1-to-1
-template<MFP::MonotoneFrameworkInstance MFI>
-struct llvm::GraphTraits<const MFP::Graph<MFI> *> {
-  using GraphType = const MFP::Graph<MFI> *;
+template<mfp::MonotoneFrameworkInstance MFI>
+struct llvm::GraphTraits<const mfp::Graph<MFI> *> {
+  using GraphType = const mfp::Graph<MFI> *;
   using UnderlyingGraphTraits = llvm::GraphTraits<typename MFI::GraphType>;
   using NodeRef = const typename UnderlyingGraphTraits::NodeRef;
   using EdgeRef = typename UnderlyingGraphTraits::EdgeRef;
diff --git a/include/revng/MFP/MFP.h b/include/revng/MFP/MFP.h
index fdaf5e2be..678e543ec 100644
--- a/include/revng/MFP/MFP.h
+++ b/include/revng/MFP/MFP.h
@@ -1,5 +1,8 @@
 #pragma once
 
+#include "revng/ADT/STLExtras.h"
+#include "revng/Support/Debug.h"
+
 //
 // This file is distributed under the MIT License. See LICENSE.md for details.
 //
@@ -9,8 +12,13 @@
 #include <map>
 #include <queue>
 #include <type_traits>
+#include <unordered_map>
+#include <utility>
+#include <variant>
 
+#include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/GraphTraits.h"
+#include "llvm/ADT/Hashing.h"
 #include "llvm/ADT/PostOrderIterator.h"
 #include "llvm/ADT/SmallSet.h"
 #include "llvm/ADT/iterator_range.h"
@@ -20,22 +28,133 @@
 #include "revng/ADT/GenericGraph.h"
 #include "revng/ADT/ReversePostOrderTraversal.h"
 
-namespace MFP {
+namespace mfp {
 
 inline Logger NullLogger("");
 
-template<typename T>
-void dump(llvm::raw_ostream &Stream, unsigned Indent, const T &Element) {
+/// @{
+/// Tag types selecting how `MFPConfiguration::EntryLabels` is computed when
+/// the caller does not provide an explicit `std::vector<Label>`.
+
+/// Use `GT::getEntryNode(Flow)` as the only entry label. Default. Appropriate
+/// for forward analyses where the graph has a single entry node.
+///
+/// WARNING: Do not use with `llvm::Inverse<...>` graphs. By LLVM convention
+/// `GraphTraits<Inverse<llvm::Function*>>::getEntryNode` still returns the
+/// forward entry node (and `GenericGraph` follows the same convention), so
+/// RPOT seeded from that node in the inverse direction reaches nothing
+/// useful. This is unfortunate, but it is what it is. Use `All` instead.
+struct Entry {};
+
+/// Enumerate every node via `GT::nodes_begin..nodes_end` and use them all as
+/// entry labels. Appropriate for backward analyses on `llvm::Inverse<...>`,
+/// where `getEntryNode` is unreliable.
+struct All {};
+/// @}
+
+template<typename Label>
+using EntryLabelsOptions = std::variant<Entry,
+                                        All,
+                                        /* non-nullptr */
+                                        const std::vector<Label> *>;
+
+template<typename T, typename StreamT>
+void dump(StreamT &Stream, unsigned Indent, const T &Element) {
   for (unsigned I = 0; I < Indent; ++I)
     Stream << "  ";
   Stream << "(not implemented)\n";
 }
 
-template<typename T>
-void dumpLabel(llvm::raw_ostream &Stream, const T &Element) {
+template<typename T, typename StreamT>
+void dumpLabel(StreamT &Stream, const T &Element) {
   Stream << "(not implemented)";
 }
 
+/// Position relative to a `Key` recorded into an `ExtraState`
+enum class Position : unsigned char {
+  Before,
+  After
+};
+
+/// An hashmap that enables transfer functions to attach a LatticeElement to
+/// sub-Label entities (e.g., instructions in a basic block), depending to what
+/// the user is interested in
+template<typename KeyT, typename LatticeElement>
+class ExtraState {
+public:
+  using Key = KeyT;
+  using KeyAndPosition = std::pair<Key, Position>;
+
+private:
+  struct Hash {
+    size_t operator()(const KeyAndPosition &P) const noexcept {
+      return llvm::hash_combine(P.first, static_cast<int>(P.second));
+    }
+  };
+
+private:
+  /// The presence of a `(Key, Position)` entry marks it as interesting; the
+  /// stored value is the most recently recorded one.
+  std::unordered_map<KeyAndPosition, LatticeElement, Hash> Map;
+
+public:
+  /// @{
+  /// Mark a `(Key, Position)` pair as interesting. Caller-side.
+
+  void registerAsInterestingBefore(const Key &K) {
+    Map.try_emplace({ K, Position::Before });
+  }
+
+  void registerAsInterestingAfter(const Key &K) {
+    Map.try_emplace({ K, Position::After });
+  }
+  /// @}
+
+  /// @{
+  /// Record `Value` for `(K, Position)`. No-op if not interesting. Called
+  /// from inside `applyTransferFunction`.
+  void registerBefore(const Key &K, const LatticeElement &Value) {
+    auto It = Map.find({ K, Position::Before });
+    if (It != Map.end())
+      It->second = Value;
+  }
+
+  void registerAfter(const Key &K, const LatticeElement &Value) {
+    auto It = Map.find({ K, Position::After });
+    if (It != Map.end())
+      It->second = Value;
+  }
+  /// @}
+
+  /// @{
+  /// Retrieve the recorded value. Caller-side, after `getMaximalFixedPoint`.
+  const LatticeElement &getBefore(const Key &K) const {
+    auto It = Map.find({ K, Position::Before });
+    revng_assert(It != Map.end());
+    return It->second;
+  }
+
+  const LatticeElement &getAfter(const Key &K) const {
+    auto It = Map.find({ K, Position::After });
+    revng_assert(It != Map.end());
+    return It->second;
+  }
+  /// @}
+
+public:
+  template<typename T>
+  void dump(T &Stream) const {
+    Stream << Map.size() << " elements:\n";
+    for (const auto &[Key, Element] : Map) {
+      Stream << "  " << (Key.second == Position::Before ? "Before " : "After ");
+      mfp::dumpLabel(Stream, Key.first);
+      Stream << "\n";
+
+      mfp::dump<LatticeElement>(Stream, 2, Element);
+    }
+  }
+};
+
 template<typename LatticeElement>
 struct MFPResult {
   LatticeElement InValue;
@@ -48,11 +167,40 @@ auto successors(typename GT::NodeRef From) {
   return llvm::make_range(GT::child_begin(From), GT::child_end(From));
 }
 
+/// Placeholder struct to be employed when an MFI does not need to track extra
+/// state
+struct NoExtraState {};
+
+template<typename MFI>
+concept HasExtraStateKey = requires { typename MFI::ExtraStateKey; };
+
+template<typename MFI>
+struct GetExtraStateKey {
+  using type = typename MFI::ExtraStateKey;
+};
+
+template<typename T>
+struct Identity {
+  using type = T;
+};
+
+template<typename MFI>
+using ExtraStateKey = std::conditional_t<HasExtraStateKey<MFI>,
+                                         GetExtraStateKey<MFI>,
+                                         Identity<void *>>::type;
+
+template<typename MFI>
+using ExtraStateType = std::conditional_t<
+  HasExtraStateKey<MFI>,
+  ExtraState<ExtraStateKey<MFI>, typename MFI::LatticeElement>,
+  NoExtraState>;
+
 template<typename MFI, typename LatticeElement = typename MFI::LatticeElement>
 concept MonotoneFrameworkInstance = requires(const MFI &I,
                                              LatticeElement E1,
                                              LatticeElement E2,
-                                             typename MFI::Label L) {
+                                             typename MFI::Label L,
+                                             ExtraStateType<MFI> &ES) {
   /// To compute the reverse post order traversal of the graph starting from
   /// the extremal nodes, we need that the nodes also represent a subgraph
   typename llvm::GraphTraits<typename MFI::Label>::NodeRef;
@@ -61,7 +209,13 @@ concept MonotoneFrameworkInstance = requires(const MFI &I,
                typename llvm::GraphTraits<typename MFI::GraphType>::NodeRef>;
   { I.combineValues(E1, E2) } -> std::same_as<LatticeElement>;
   { I.isLessOrEqual(E1, E2) } -> std::same_as<bool>;
-  { I.applyTransferFunction(L, E2) } -> std::same_as<LatticeElement>;
+  { I.applyTransferFunction(L, E2, ES) } -> std::same_as<LatticeElement>;
+};
+
+template<typename GT>
+concept HasNodeRange = requires() {
+  { GT::nodes_begin };
+  { GT::nodes_end };
 };
 
 template<typename Label, typename LatticeElement>
@@ -71,6 +225,44 @@ template<MonotoneFrameworkInstance MFI>
 using MFIResultMap = ResultMap<typename MFI::Label,
                                typename MFI::LatticeElement>;
 
+template<MonotoneFrameworkInstance MFIType>
+struct MFPConfiguration {
+  /// The monotone framework instance
+  const MFIType *Instance = nullptr;
+
+  /// The graph on which the monotone framework will run
+  typename MFIType::GraphType Flow;
+
+  /// The value that will be used to initialize all the non-extremal nodes.
+  /// Defaults to default constructor.
+  const typename MFIType::LatticeElement *Bottom = nullptr;
+
+  /// The value that will be used to initialize all the extremal nodes
+  /// Defaults to default constructor.
+  const typename MFIType::LatticeElement *ExtremalValue = nullptr;
+
+  /// The list of extremal labels
+  /// Defaults to empty.
+  const std::vector<typename MFIType::Label> *ExtremalLabels = nullptr;
+
+  /// How to seed the worklist (priority RPOT). Defaults to `Entry{}`. Pass
+  /// `All{}` to enumerate every node (required for backward analyses on
+  /// `llvm::Inverse<...>` graphs, where `getEntryNode` returns the forward
+  /// entry and is therefore unreliable). Pass `&vec` (non-null) for full
+  /// control.
+  EntryLabelsOptions<typename MFIType::Label> EntryLabels = Entry{};
+
+  /// The extra state to populate during the analysis
+  /// Defaults to empty.
+  ExtraStateType<MFIType> *ExtraState = nullptr;
+
+  /// A logger where the advancement of the MFP algorithm should be reported
+  /// Defaults to NullLogger.
+  Logger *Logger = nullptr;
+};
+
+/// Compute the solution to the given instance of a monotone framework.
+///
 /// Compute the maximum fixed points of an instance of monotone framework GT an
 /// instance of llvm::GraphTraits that tells us how to visit the graph LGT a
 /// graph type that tells us how to visit the subgraph induced by a node in the
@@ -78,22 +270,80 @@ using MFIResultMap = ResultMap<typename MFI::Label,
 /// Inverse<...>) the nodes don't necessary carry all the information that
 /// GraphType has.
 template<MonotoneFrameworkInstance MFIType,
-         typename GT = llvm::GraphTraits<typename MFIType::GraphType>,
-         typename LGT = typename MFIType::Label>
+         typename GT = llvm::GraphTraits<typename MFIType::GraphType>>
 MFIResultMap<MFIType>
-getMaximalFixedPoint(const MFIType &MFI,
-                     typename MFIType::GraphType Flow,
-                     typename MFIType::LatticeElement InitialValue,
-                     typename MFIType::LatticeElement ExtremalValue,
-                     const std::vector<typename MFIType::Label> &ExtremalLabels,
-                     const std::vector<typename MFIType::Label> &InitialNodes,
-                     Logger &Logger = NullLogger) {
+getMaximalFixedPointImpl(MFPConfiguration<MFIType> &Configuration) {
   using Label = typename MFIType::Label;
   using LatticeElement = typename MFIType::LatticeElement;
 
-  std::map<Label, LatticeElement> PartialAnalysis;
+  auto &Instance = notNull(Configuration.Instance);
+  auto &Bottom = notNull(Configuration.Bottom);
+  auto &ExtremalValue = notNull(Configuration.ExtremalValue);
+  auto &ExtremalLabels = notNull(Configuration.ExtremalLabels);
+  auto &ExtraState = notNull(Configuration.ExtraState);
+  auto &Logger = notNull(Configuration.Logger);
+
+  // Resolve the EntryLabels variant into a concrete list of seeds.
+  std::vector<Label> EntryLabels;
+  auto ResolveEntryLabels = [&](const auto &Option) {
+    using T = std::decay_t<decltype(Option)>;
+    if constexpr (std::is_same_v<T, Entry>) {
+      auto Seed = GT::getEntryNode(Configuration.Flow);
+      if (Seed != typename GT::NodeRef{}) {
+        EntryLabels.push_back(Seed);
+      }
+    } else if constexpr (std::is_same_v<T, All>) {
+      if constexpr (HasNodeRange<GT>) {
+        auto &Flow = Configuration.Flow;
+        for (auto Node :
+             llvm::make_range(GT::nodes_begin(Flow), GT::nodes_end(Flow))) {
+          EntryLabels.push_back(Node);
+        }
+      } else {
+        revng_abort();
+      }
+    } else {
+      static_assert(std::is_same_v<T, const std::vector<Label> *>);
+      EntryLabels = notNull(Option);
+    }
+  };
+  std::visit(ResolveEntryLabels, Configuration.EntryLabels);
+
+  if (Logger.isEnabled()) {
+    revng_log(Logger, "Initializing extremal labels");
+    LoggerIndent Indent(Logger);
+    Logger << "Extremal value:\n";
+    mfp::dump(*Logger.getAsLLVMStream(), 1, Configuration.ExtremalValue);
+    Logger << DoLog;
+
+    Logger << "Extremal labels:" << DoLog;
+    LoggerIndent Indent2(Logger);
+    for (Label ExtremalLabel : ExtremalLabels) {
+      mfp::dumpLabel(*Logger.getAsLLVMStream(), ExtremalLabel);
+      Logger << DoLog;
+    }
+
+    revng_log(Logger, "Initializing initial nodes");
+    LoggerIndent Indent3(Logger);
+    Logger << "Initial value:\n";
+    mfp::dump(*Logger.getAsLLVMStream(), 1, Bottom);
+    Logger << DoLog;
+
+    Logger << "Initial labels:" << DoLog;
+    LoggerIndent Indent4(Logger);
+    for (Label InitialNode : EntryLabels) {
+      mfp::dumpLabel(*Logger.getAsLLVMStream(), InitialNode);
+      Logger << DoLog;
+    }
+  }
+
   std::map<Label, MFPResult<LatticeElement>> AnalysisResult;
 
+  // Initialize the state of the analysis: associate extremal labels to extremal
+  // values
+  for (Label ExtremalLabel : ExtremalLabels)
+    AnalysisResult[ExtremalLabel].InValue = ExtremalValue;
+
   struct WorklistItem {
     size_t Priority;
     Label Item;
@@ -101,63 +351,32 @@ getMaximalFixedPoint(const MFIType &MFI,
     std::weak_ordering operator<=>(const WorklistItem &) const = default;
   };
   std::set<WorklistItem> Worklist;
-
-  llvm::SmallSet<Label, 8> Visited{};
   std::map<Label, size_t> LabelPriority;
 
   //
-  // Initialize the worklist and extremal labels
+  // Initialize the worklist with the nodes in reverse post order.
+  // Also, record the visit order as priority.
   //
+  // If the graph has multiple initial nodes, we perform a reverse post order
+  // visit from each initial node, sharing the list of visited nodes with
+  // previous visits.
+  {
+    using NodeSet = llvm::SmallSet<Label, 8>;
+    NodeSet Visited;
+    for (Label Start : EntryLabels) {
 
-  if (Logger.isEnabled()) {
-    revng_log(Logger, "Initializing extremal labels");
-    LoggerIndent Indent(Logger);
-    Logger << "Extremal value:\n";
-    MFP::dump(*Logger.getAsLLVMStream(), 1, ExtremalValue);
-    Logger << DoLog;
+      if (Visited.contains(Start))
+        continue;
 
-    Logger << "Extremal labels:" << DoLog;
-    LoggerIndent Indent2(Logger);
-    for (Label ExtremalLabel : ExtremalLabels) {
-      MFP::dumpLabel(*Logger.getAsLLVMStream(), ExtremalLabel);
-      Logger << DoLog;
-    }
-  }
+      ReversePostOrderTraversalExt<Label, GT, NodeSet> RPOT(Start, Visited);
+      for (Label Node : RPOT) {
+        LabelPriority[Node] = LabelPriority.size();
+        Worklist.insert({ LabelPriority.at(Node), Node });
 
-  for (Label ExtremalLabel : ExtremalLabels)
-    AnalysisResult[ExtremalLabel].InValue = ExtremalValue;
-
-  if (Logger.isEnabled()) {
-    revng_log(Logger, "Initializing initial nodes");
-    LoggerIndent Indent(Logger);
-    Logger << "Initial value:\n";
-    MFP::dump(*Logger.getAsLLVMStream(), 1, InitialValue);
-    Logger << DoLog;
-
-    Logger << "Initial labels:" << DoLog;
-    LoggerIndent Indent2(Logger);
-    for (Label InitialNode : InitialNodes) {
-      MFP::dumpLabel(*Logger.getAsLLVMStream(), InitialNode);
-      Logger << DoLog;
-    }
-  }
-
-  for (Label Start : InitialNodes) {
-
-    if (Visited.contains(Start))
-      continue;
-
-    // Fill the worklist with nodes in reverse post order launching a visit
-    // from each remaining node
-    ReversePostOrderTraversalExt<LGT, GT, llvm::SmallSet<Label, 8>>
-      RPOTE(Start, Visited);
-    for (Label Node : RPOTE) {
-      LabelPriority[Node] = LabelPriority.size();
-      Worklist.insert({ LabelPriority.at(Node), Node });
-
-      // Initialize the analysis value for non extremal nodes
-      if (!AnalysisResult.contains(Node))
-        AnalysisResult[Node].InValue = InitialValue;
+        // Initialize the analysis value for non extremal nodes
+        if (not AnalysisResult.contains(Node))
+          AnalysisResult[Node].InValue = Bottom;
+      }
     }
   }
 
@@ -176,7 +395,7 @@ getMaximalFixedPoint(const MFIType &MFI,
 
     if (Logger.isEnabled()) {
       Logger << "Iteration #" << IterationIndex << " on ";
-      MFP::dumpLabel(*Logger.getAsLLVMStream(), Start);
+      mfp::dumpLabel(*Logger.getAsLLVMStream(), Start);
       Logger << DoLog;
     }
 
@@ -184,24 +403,26 @@ getMaximalFixedPoint(const MFIType &MFI,
 
     if (Logger.isEnabled()) {
       Logger << "Initial value:\n";
-      MFP::dump(*Logger.getAsLLVMStream(), 1, LabelAnalysis.InValue);
+      mfp::dump(*Logger.getAsLLVMStream(), 1, LabelAnalysis.InValue);
       Logger << DoLog;
 
       Logger << "Final value:\n";
-      MFP::dump(*Logger.getAsLLVMStream(), 1, LabelAnalysis.OutValue);
+      mfp::dump(*Logger.getAsLLVMStream(), 1, LabelAnalysis.OutValue);
       Logger << DoLog;
     }
 
-    // Run the transfer function
+    // Run the transfer function.
     revng_log(Logger, "Running the transfer function");
     Logger.indent();
-    const auto &New = MFI.applyTransferFunction(Start, LabelAnalysis.InValue);
+    const auto New = Instance.applyTransferFunction(Start,
+                                                    LabelAnalysis.InValue,
+                                                    ExtraState);
     Logger.unindent();
 
     if (Logger.isEnabled()) {
       LoggerIndent Indent(Logger);
       Logger << "New final value:\n";
-      MFP::dump(*Logger.getAsLLVMStream(), 1, New);
+      mfp::dump(*Logger.getAsLLVMStream(), 1, New);
       Logger << DoLog;
     }
 
@@ -218,28 +439,29 @@ getMaximalFixedPoint(const MFIType &MFI,
 
       if (Logger.isEnabled()) {
         Logger << "Considering successor ";
-        MFP::dumpLabel(*Logger.getAsLLVMStream(), Successor);
+        mfp::dumpLabel(*Logger.getAsLLVMStream(), Successor);
         Logger << DoLog;
 
         Logger << "Initial value:\n";
         LoggerIndent Indent(Logger);
         Logger << DoLog;
-        MFP::dump(*Logger.getAsLLVMStream(), 1, SuccessorResults.InValue);
+        mfp::dump(*Logger.getAsLLVMStream(), 1, SuccessorResults.InValue);
         Logger << DoLog;
       }
       LoggerIndent Indent(Logger);
 
-      if (not MFI.isLessOrEqual(LabelAnalysis.OutValue,
-                                SuccessorResults.InValue)) {
+      if (not Instance.isLessOrEqual(LabelAnalysis.OutValue,
+                                     SuccessorResults.InValue)) {
         // We need to re-enqueue
 
         // Combine the old value with the new incoming value and update it
-        SuccessorResults.InValue = MFI.combineValues(SuccessorResults.InValue,
-                                                     LabelAnalysis.OutValue);
+        SuccessorResults.InValue = Instance
+                                     .combineValues(SuccessorResults.InValue,
+                                                    LabelAnalysis.OutValue);
 
         if (Logger.isEnabled()) {
           Logger << "Enqueuing. New initial value:\n";
-          MFP::dump(*Logger.getAsLLVMStream(), 1, SuccessorResults.InValue);
+          mfp::dump(*Logger.getAsLLVMStream(), 1, SuccessorResults.InValue);
           Logger << DoLog;
         }
 
@@ -256,36 +478,46 @@ getMaximalFixedPoint(const MFIType &MFI,
   return AnalysisResult;
 }
 
-template<MonotoneFrameworkInstance MFI,
-         typename GT = llvm::GraphTraits<typename MFI::GraphType>,
-         typename LGT = typename MFI::Label>
-MFIResultMap<MFI>
-getMaximalFixedPoint(const MFI &Instance,
-                     typename MFI::GraphType Flow,
-                     typename MFI::LatticeElement InitialValue,
-                     typename MFI::LatticeElement ExtremalValue,
-                     const std::vector<typename MFI::Label> &ExtremalLabels,
-                     Logger &Logger = NullLogger) {
-  using Label = typename MFI::Label;
-  std::vector<Label> InitialNodes(ExtremalLabels);
+template<MonotoneFrameworkInstance MFIType,
+         typename GT = llvm::GraphTraits<typename MFIType::GraphType>>
+MFIResultMap<MFIType>
+getMaximalFixedPoint(MFPConfiguration<MFIType> Configuration) {
+  std::optional<MFIType> DefaultInstance;
+  if constexpr (std::is_default_constructible_v<MFIType>) {
+    if (Configuration.Instance == nullptr)
+      Configuration.Instance = &DefaultInstance.emplace();
+  } else {
+    revng_assert(Configuration.Instance != nullptr);
+  }
 
-  // Handle the special case that the graph has a single entry node
-  if (GT::getEntryNode(Flow) != typename GT::NodeRef{}) {
-    InitialNodes.push_back(GT::getEntryNode(Flow));
+  using LatticElement = typename MFIType::LatticeElement;
+  std::optional<LatticElement> DefaultBottom;
+  std::optional<typename MFIType::LatticeElement> DefaultExtremalValue;
+  if constexpr (std::is_default_constructible_v<LatticElement>) {
+
+    if (Configuration.Bottom == nullptr)
+      Configuration.Bottom = &DefaultBottom.emplace();
+
+    if (Configuration.ExtremalValue == nullptr)
+      Configuration.ExtremalValue = &DefaultExtremalValue.emplace();
+
+  } else {
+    revng_assert(Configuration.Bottom != nullptr);
+    revng_assert(Configuration.ExtremalValue != nullptr);
   }
-  // Start visits for nodes that we still haven't visited
-  // prioritizing extremal nodes
-  for (Label Node :
-       llvm::make_range(GT::nodes_begin(Flow), GT::nodes_end(Flow))) {
-    InitialNodes.push_back(Node);
-  }
-  return getMaximalFixedPoint<MFI, GT, LGT>(Instance,
-                                            Flow,
-                                            InitialValue,
-                                            ExtremalValue,
-                                            ExtremalLabels,
-                                            InitialNodes,
-                                            Logger);
+
+  std::vector<typename MFIType::Label> DefaultExtremalLabels;
+  if (Configuration.ExtremalLabels == nullptr)
+    Configuration.ExtremalLabels = &DefaultExtremalLabels;
+
+  if (Configuration.Logger == nullptr)
+    Configuration.Logger = &NullLogger;
+
+  ExtraStateType<MFIType> DefaultExtraState;
+  if (Configuration.ExtraState == nullptr)
+    Configuration.ExtraState = &DefaultExtraState;
+
+  return getMaximalFixedPointImpl<MFIType, GT>(Configuration);
 }
 
-} // namespace MFP
+} // namespace mfp
diff --git a/include/revng/RegisterUsageAnalyses/Liveness.h b/include/revng/RegisterUsageAnalyses/Liveness.h
index dbf599afa..0a94a8abe 100644
--- a/include/revng/RegisterUsageAnalyses/Liveness.h
+++ b/include/revng/RegisterUsageAnalyses/Liveness.h
@@ -18,7 +18,12 @@ private:
 
 public:
   using LatticeElement = Set;
-  using GraphType = llvm::Inverse<const Function *>;
+  // Backward analysis. We store the forward graph here (by value, so no
+  // dangling-reference traps); callers must override the `GT` template
+  // parameter of `getMaximalFixedPoint` to
+  // `llvm::GraphTraits<llvm::Inverse<const Function *>>` to actually walk
+  // backwards.
+  using GraphType = const Function *;
   using Label = const BlockNode *;
 
 private:
@@ -54,7 +59,8 @@ public:
   }
 
   RegisterSet applyTransferFunction(const BlockNode *Block,
-                                    const RegisterSet &InitialState) const {
+                                    const RegisterSet &InitialState,
+                                    mfp::NoExtraState &) const {
     RegisterSet Result = InitialState;
 
     for (const Operation &Operation :
@@ -80,6 +86,6 @@ public:
   }
 };
 
-static_assert(MFP::MonotoneFrameworkInstance<Liveness>);
+static_assert(mfp::MonotoneFrameworkInstance<Liveness>);
 
 } // namespace rua
diff --git a/include/revng/RegisterUsageAnalyses/ReachingDefinitions.h b/include/revng/RegisterUsageAnalyses/ReachingDefinitions.h
index d641e057f..460064138 100644
--- a/include/revng/RegisterUsageAnalyses/ReachingDefinitions.h
+++ b/include/revng/RegisterUsageAnalyses/ReachingDefinitions.h
@@ -64,6 +64,7 @@ public:
   using LatticeElement = WritersSet;
   using GraphType = Function *;
   using Label = BlockNode *;
+  using ExtraStateType = mfp::NoExtraState;
 
 private:
   llvm::DenseMap<const Operation *, uint8_t> WriteToIndex;
@@ -131,7 +132,8 @@ public:
   }
 
   WritersSet applyTransferFunction(const Block *Block,
-                                   const WritersSet &InitialState) const {
+                                   const WritersSet &InitialState,
+                                   mfp::NoExtraState &) const {
     WritersSet Result = InitialState;
 
     for (const Operation &Operation : *Block) {
@@ -158,6 +160,6 @@ public:
   }
 };
 
-static_assert(MFP::MonotoneFrameworkInstance<ReachingDefinitions>);
+static_assert(mfp::MonotoneFrameworkInstance<ReachingDefinitions>);
 
 } // namespace rua
diff --git a/include/revng/RestructureCFG/RegionCFGTreeImpl.h b/include/revng/RestructureCFG/RegionCFGTreeImpl.h
index a06a24799..8b0149b15 100644
--- a/include/revng/RestructureCFG/RegionCFGTreeImpl.h
+++ b/include/revng/RestructureCFG/RegionCFGTreeImpl.h
@@ -715,8 +715,11 @@ struct ReachableExitsAnalysis
   using LatticeElement = typename SetUnionLattice<
     std::set<BasicBlockNode<NodeT> *>>::LatticeElement;
 
+  using ExtraStateType = mfp::NoExtraState;
+
   static LatticeElement applyTransferFunction(const Label &L,
-                                              const LatticeElement E) {
+                                              const LatticeElement E,
+                                              mfp::NoExtraState &) {
 
     const auto IsInlined = [](const auto &NodeLabelPair) {
       return NodeLabelPair.second.Inlined;
@@ -761,10 +764,10 @@ inline bool RegionCFG<NodeT>::inflate() {
 
   using REA = ReachableExitsAnalysis<NodeT>;
   using Inverse = llvm::Inverse<typename REA::GraphType>;
-  auto ReachableExits = MFP::getMaximalFixedPoint<
-    REA,
-    llvm::GraphTraits<Inverse>,
-    llvm::Inverse<BasicBlockNode<NodeT> *>>({}, &Graph, {}, {}, {}, Exits);
+  using GraphTraits = llvm::GraphTraits<Inverse>;
+  auto GetMaximalFixedPoint = mfp::getMaximalFixedPoint<REA, GraphTraits>;
+  auto ReachableExits = GetMaximalFixedPoint({ .Flow = &Graph,
+                                               .EntryLabels = &Exits });
 
   // Refresh information of dominator and postdominator trees.
   DT.recalculate(Graph);
diff --git a/include/revng/Support/IRHelpers.h b/include/revng/Support/IRHelpers.h
index 1bc39dbdb..c00bb0732 100644
--- a/include/revng/Support/IRHelpers.h
+++ b/include/revng/Support/IRHelpers.h
@@ -1573,7 +1573,10 @@ std::optional<T> getConstantArg(llvm::CallInst *Call, unsigned Index) {
   using namespace llvm;
 
   if (auto *CI = dyn_cast<ConstantInt>(Call->getArgOperand(Index))) {
-    return CI->getLimitedValue();
+    if constexpr (std::is_signed_v<T>)
+      return CI->getSExtValue();
+    else
+      return CI->getZExtValue();
   } else {
     return {};
   }
diff --git a/include/revng/ValueMaterializer/AdvancedValueInfo.h b/include/revng/ValueMaterializer/AdvancedValueInfo.h
index 25d917311..613353a4c 100644
--- a/include/revng/ValueMaterializer/AdvancedValueInfo.h
+++ b/include/revng/ValueMaterializer/AdvancedValueInfo.h
@@ -25,8 +25,9 @@ public:
   using LatticeElement = std::map<llvm::Instruction *, ConstantRangeSet>;
   using GraphType = const ControlFlowEdgesGraph *;
   using Label = const ControlFlowEdgesGraph::Node *;
-  using ResultsMap = std::map<Label, MFP::MFPResult<LatticeElement>>;
+  using ResultsMap = std::map<Label, mfp::MFPResult<LatticeElement>>;
   using InstructionsSet = llvm::SmallPtrSetImpl<llvm::Instruction *>;
+  using ExtraStateType = mfp::NoExtraState;
 
 private:
   llvm::LazyValueInfo &LVI;
@@ -57,13 +58,15 @@ public:
   bool isLessOrEqual(const LatticeElement &LHS,
                      const LatticeElement &RHS) const;
 
-  LatticeElement applyTransferFunction(Label L, const LatticeElement &E) const;
+  LatticeElement applyTransferFunction(Label L,
+                                       const LatticeElement &E,
+                                       mfp::NoExtraState &) const;
 
 public:
   static void dump(GraphType CFEG, const ResultsMap &AllResults);
 };
 
-static_assert(MFP::MonotoneFrameworkInstance<AdvancedValueInfoMFI>);
+static_assert(mfp::MonotoneFrameworkInstance<AdvancedValueInfoMFI>);
 
 /// \p DFG the data flow graph containing the instructions we're interested in.
 /// \p Context the position in the function for the current query.
@@ -71,7 +74,7 @@ std::tuple<
   std::map<llvm::Instruction *, ConstantRangeSet>,
   ControlFlowEdgesGraph,
   std::map<const ForwardNode<ControlFlowEdgesNode> *,
-           MFP::MFPResult<std::map<llvm::Instruction *, ConstantRangeSet>>>>
+           mfp::MFPResult<std::map<llvm::Instruction *, ConstantRangeSet>>>>
 runAVI(const DataFlowGraph &DFG,
        llvm::Instruction *Context,
        const llvm::DominatorTree &DT,
@@ -80,10 +83,10 @@ runAVI(const DataFlowGraph &DFG,
        bool ZeroExtendConstraints);
 
 template<>
-void MFP::dump(llvm::raw_ostream &Stream,
+void mfp::dump(llvm::raw_ostream &Stream,
                unsigned Indent,
                const std::map<llvm::Instruction *, ConstantRangeSet> &Element);
 
 template<>
-void MFP::dumpLabel(llvm::raw_ostream &Stream,
+void mfp::dumpLabel(llvm::raw_ostream &Stream,
                     const ControlFlowEdgesGraph::Node *const &Label);
diff --git a/include/revng/ValueMaterializer/ValueMaterializer.h b/include/revng/ValueMaterializer/ValueMaterializer.h
index a713344bb..a571933be 100644
--- a/include/revng/ValueMaterializer/ValueMaterializer.h
+++ b/include/revng/ValueMaterializer/ValueMaterializer.h
@@ -58,7 +58,7 @@ private:
   DataFlowGraph DataFlowGraph;
   ConstraintsMap OracleConstraints;
   std::map<const ForwardNode<ControlFlowEdgesNode> *,
-           MFP::MFPResult<std::map<llvm::Instruction *, ConstantRangeSet>>>
+           mfp::MFPResult<std::map<llvm::Instruction *, ConstantRangeSet>>>
     MFIResults;
   std::optional<MaterializedValues> Values;
   ControlFlowEdgesGraph CFEG;
diff --git a/lib/ABI/FunctionType/Layout.cpp b/lib/ABI/FunctionType/Layout.cpp
index 1fcc8e6d9..663e3b0bd 100644
--- a/lib/ABI/FunctionType/Layout.cpp
+++ b/lib/ABI/FunctionType/Layout.cpp
@@ -12,7 +12,6 @@
 #include "revng/Model/Binary.h"
 #include "revng/Model/Helpers.h"
 #include "revng/Support/Debug.h"
-#include "revng/Support/YAMLTraits.h"
 #include "revng/TupleTree/NamedEnumScalarTraits.h"
 
 #include "ValueDistributor.h"
@@ -707,54 +706,3 @@ UsedRegisters usedRegisters(const model::CABIFunctionDefinition &Function) {
 }
 
 } // namespace abi::FunctionType
-
-using FTL = abi::FunctionType::Layout;
-namespace FTAK = abi::FunctionType::ArgumentKind;
-
-template<>
-struct llvm::yaml::ScalarEnumerationTraits<FTAK::Values>
-  : public NamedEnumScalarTraits<FTAK::Values> {};
-
-template<>
-struct llvm::yaml::MappingTraits<FTL::Argument::StackSpan> {
-  static void mapping(IO &IO, FTL::Argument::StackSpan &SS) {
-    IO.mapRequired("Offset", SS.Offset);
-    IO.mapRequired("Size", SS.Size);
-  }
-};
-LLVM_YAML_IS_SEQUENCE_VECTOR(FTL::Argument::StackSpan)
-
-template<>
-struct llvm::yaml::MappingTraits<FTL::ReturnValue> {
-  static void mapping(IO &IO, FTL::ReturnValue &RV) {
-    IO.mapRequired("Type", RV.Type);
-    IO.mapRequired("Registers", RV.Registers);
-  }
-};
-LLVM_YAML_IS_SEQUENCE_VECTOR(FTL::ReturnValue)
-
-template<>
-struct llvm::yaml::MappingTraits<FTL::Argument> {
-  static void mapping(IO &IO, FTL::Argument &A) {
-    IO.mapRequired("Type", A.Type);
-    IO.mapRequired("Kind", A.Kind);
-    IO.mapRequired("Registers", A.Registers);
-    IO.mapOptional("Stack", A.Stack);
-  }
-};
-LLVM_YAML_IS_SEQUENCE_VECTOR(FTL::Argument)
-
-template<>
-struct llvm::yaml::MappingTraits<FTL> {
-  static void mapping(IO &IO, FTL &L) {
-    IO.mapRequired("Arguments", L.Arguments);
-    IO.mapRequired("ReturnValues", L.ReturnValues);
-    IO.mapRequired("CalleeSavedRegisters", L.CalleeSavedRegisters);
-    IO.mapRequired("FinalStackOffset", L.FinalStackOffset);
-  }
-};
-
-void FTL::dump() const {
-  // TODO: accept an arbitrary stream
-  serialize(dbg, *this);
-}
diff --git a/lib/Canonicalize/ArithmeticToGEP.cpp b/lib/Canonicalize/ArithmeticToGEP.cpp
index 82141119b..386f6a63a 100644
--- a/lib/Canonicalize/ArithmeticToGEP.cpp
+++ b/lib/Canonicalize/ArithmeticToGEP.cpp
@@ -866,11 +866,12 @@ private:
       LocalValue<> &Pointer = Pointers[K];
       // Skip globals because they have no local operands.
       llvm::Value *V = Pointer.value();
+
       if (isGlobal(V))
         continue;
       revng_assert(isLocal(V));
-      auto *I = dyn_cast<llvm::Instruction>(V);
-      if (I) {
+
+      if (auto *I = dyn_cast<llvm::Instruction>(V)) {
         for (llvm::Use &U : I->operands()) {
           propagatePointersBackwards(U);
         }
@@ -893,8 +894,7 @@ private:
 };
 
 static bool foldPointerCasts(llvm::Function &F) {
-  using WTVH = llvm::WeakTrackingVH;
-  llvm::SmallVector<WTVH, 8> Dead;
+  llvm::SmallVector<llvm::WeakTrackingVH, 8> Dead;
 
   for (llvm::Instruction &I : llvm::instructions(F)) {
 
diff --git a/lib/Canonicalize/CMakeLists.txt b/lib/Canonicalize/CMakeLists.txt
index 6d41e1088..c2a0f28f9 100644
--- a/lib/Canonicalize/CMakeLists.txt
+++ b/lib/Canonicalize/CMakeLists.txt
@@ -11,7 +11,7 @@ revng_add_analyses_library_internal(
   ExitSSAPass.cpp
   ExtractValueToGEP.cpp
   FoldModelGEP.cpp
-  HoistStructPhis.cpp
+  SplitStructPhis.cpp
   ImplicitModelCastPass.cpp
   LoopRewriteWithCanonicalIV.cpp
   MakeLocalVariables.cpp
@@ -33,6 +33,7 @@ revng_add_analyses_library_internal(
 
 target_link_libraries(
   revngCanonicalize
+  revngFunctionIsolation
   revngInitModelTypes
   revngTypeNames
   revngSupport
diff --git a/lib/Canonicalize/HoistStructPhis.cpp b/lib/Canonicalize/HoistStructPhis.cpp
deleted file mode 100644
index 4ecabe99d..000000000
--- a/lib/Canonicalize/HoistStructPhis.cpp
+++ /dev/null
@@ -1,155 +0,0 @@
-//
-// This file is distributed under the MIT License. See LICENSE.md for details.
-//
-
-#include "llvm/Passes/PassBuilder.h"
-
-#include "revng/Model/FunctionTags.h"
-#include "revng/Support/Debug.h"
-#include "revng/Support/IRHelpers.h"
-
-using namespace llvm;
-
-static bool isLastBeforeTerminator(Instruction *I) {
-  auto It = I->getIterator();
-  ++It;
-  auto End = I->getParent()->end();
-  return It != End && ++It == End;
-}
-
-/// This pass hoists calls turns phis of calls returning a `StructType` into
-/// a single call (in place of the original phi) whose arguments are phis of the
-/// arguments of the original call.
-/// This is currently necessary since the backend does not handle well
-// `StructType`.
-///
-/// It turns:
-///
-/// a:
-///   %x1 = call x(1, 2)
-///   br c
-/// b:
-///   %x2 = call x(3, 4)
-///   br c
-/// c:
-///   %x3 = phi [(a, %x1), (b, %x2)]
-///
-/// Into:
-/// c:
-///   %arg1 = phi [(a, 1), (b, 3)]
-///   %arg2 = phi [(a, 2), (b, 4)]
-///   %x3 = call x(%arg1, %arg2)
-///
-/// \note This can be done only when x does not have side-effects.
-class HoistStructPhis : public llvm::FunctionPass {
-public:
-  static char ID;
-  HoistStructPhis() : llvm::FunctionPass(ID) {}
-
-  bool runOnFunction(llvm::Function &F) override {
-    llvm::SmallVector<PHINode *, 16> ToFix;
-
-    // Collect phis that need fixing
-    for (BasicBlock &BB : F)
-      for (Instruction &I : BB)
-        if (auto *Phi = dyn_cast<PHINode>(&I))
-          if (isa<StructType>(I.getType()))
-            ToFix.push_back(Phi);
-
-    if (ToFix.size() == 0)
-      return false;
-
-    for (PHINode *Phi : ToFix)
-      handlePhi(Phi);
-
-    return true;
-  }
-
-  void handlePhi(PHINode *Phi) {
-    auto PhiSize = Phi->getNumIncomingValues();
-
-    if (PhiSize == 1) {
-      Phi->replaceAllUsesWith(Phi->getIncomingValue(0));
-      return;
-    }
-
-    // Create all the phis
-    CallInst *FirstCall = nullptr;
-    Value *CalledValue = nullptr;
-    llvm::SmallVector<Value *, 2> Phis;
-    llvm::SmallVector<CallInst *, 2> Calls;
-
-    for (auto &V : Phi->incoming_values()) {
-      if (auto *Call = dyn_cast<CallInst>(V.get())) {
-        if (CalledValue == nullptr) {
-          // This is the first call we see, make some extra checks
-          CalledValue = Call->getCalledOperand();
-          FirstCall = Call;
-
-          Function *Callee = getCalledFunction(Call);
-
-          // Ignore isolated functions, they are not side-effect free
-          if (Callee == nullptr or FunctionTags::Isolated.isTagOf(Callee))
-            return;
-
-          revng_assert(isLastBeforeTerminator(Call)
-                       or Callee->onlyReadsMemory());
-
-          // First iteration, create phis
-          for (Type *ArgumentType : Call->getFunctionType()->params()) {
-            llvm::Instruction *NewPhi = PHINode::Create(ArgumentType,
-                                                        PhiSize,
-                                                        "",
-                                                        Phi);
-            NewPhi->setDebugLoc(Phi->getDebugLoc());
-            Phis.push_back(NewPhi);
-          }
-
-          Calls.push_back(Call);
-
-        } else {
-          // Ensure all the incomings are calls to the same function
-          revng_assert(CalledValue == Call->getCalledOperand());
-        }
-      }
-    }
-
-    for (auto &&[V, Predecessor] : zip(Phi->incoming_values(), Phi->blocks())) {
-      if (isa<UndefValue>(V)) {
-        for (auto *NewPhi : Phis)
-          cast<PHINode>(NewPhi)->addIncoming(UndefValue::get(NewPhi->getType()),
-                                             Predecessor);
-      } else if (isa<PoisonValue>(V)) {
-        for (auto *NewPhi : Phis) {
-          auto *Poison = PoisonValue::get(NewPhi->getType());
-          cast<PHINode>(NewPhi)->addIncoming(Poison, Predecessor);
-        }
-      } else if (auto *Call = dyn_cast<CallInst>(V)) {
-        revng_assert(Call->arg_size() == Phis.size());
-        for (auto &&[Argument, NewPhi] : zip(Call->args(), Phis))
-          cast<PHINode>(NewPhi)->addIncoming(Argument, Predecessor);
-      }
-    }
-
-    // Create a new function call
-    Instruction *InsertionPoint = Phi->getParent()->getFirstNonPHI();
-    auto *NewCall = CallInst::Create({ FirstCall->getFunctionType(),
-                                       CalledValue },
-                                     ArrayRef<Value *>(Phis),
-                                     ArrayRef<OperandBundleDef>{},
-                                     "",
-                                     InsertionPoint);
-
-    // Steal metadata and replace original phi
-    NewCall->copyMetadata(*FirstCall);
-    revng_assert(NewCall->getType() == Phi->getType());
-    Phi->replaceAllUsesWith(NewCall);
-    Phi->eraseFromParent();
-
-    for (CallInst *Call : Calls)
-      eraseFromParent(Call);
-  }
-};
-
-char HoistStructPhis::ID;
-static RegisterPass<HoistStructPhis> R("hoist-struct-phis", "", false, false);
diff --git a/lib/Canonicalize/SplitStructPhis.cpp b/lib/Canonicalize/SplitStructPhis.cpp
new file mode 100644
index 000000000..017907a15
--- /dev/null
+++ b/lib/Canonicalize/SplitStructPhis.cpp
@@ -0,0 +1,244 @@
+//
+// This file is distributed under the MIT License. See LICENSE.md for details.
+//
+
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/SmallVector.h"
+#include "llvm/IR/IRBuilder.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/Passes/PassBuilder.h"
+
+#include "revng/FunctionIsolation/StructInitializers.h"
+#include "revng/Model/FunctionTags.h"
+#include "revng/Support/Debug.h"
+#include "revng/Support/IRBuilder.h"
+#include "revng/Support/IRHelpers.h"
+#include "revng/Support/OpaqueFunctionsPool.h"
+
+using namespace llvm;
+
+/// This pass eliminates phi nodes of `StructType` by splitting them into one
+/// phi per struct field.
+///
+/// For each phi `%p : {T0, ..., Tn}`, it inserts an `OpaqueExtractvalue` for
+/// each field at the end of every predecessor block, then creates `n+1`
+/// scalar phis, one per field. Uses of the original phi that are themselves
+/// `OpaqueExtractvalue` calls get rewired to the matching scalar phi; chained
+/// struct phis are handled by reusing the per-field phis of the producer
+/// directly (so no extraction is needed across the chain). Any other kind of
+/// use causes the pass to abort.
+///
+/// It turns:
+///
+/// a:
+///   %x1 = call <{i64, i64}> @f(...)
+///   br c
+/// b:
+///   %x2 = call <{i64, i64}> @f(...)
+///   br c
+/// c:
+///   %x3 = phi <{i64, i64}> [(a, %x1), (b, %x2)]
+///   %y0 = call i64 @OpaqueExtractvalue(%x3, i64 0)
+///   %y1 = call i64 @OpaqueExtractvalue(%x3, i64 1)
+///
+/// Into:
+///
+/// a:
+///   %x1   = call <{i64, i64}> @f(...)
+///   %x1.0 = call i64 @OpaqueExtractvalue(%x1, i64 0)
+///   %x1.1 = call i64 @OpaqueExtractvalue(%x1, i64 1)
+///   br c
+/// b:
+///   %x2   = call <{i64, i64}> @f(...)
+///   %x2.0 = call i64 @OpaqueExtractvalue(%x2, i64 0)
+///   %x2.1 = call i64 @OpaqueExtractvalue(%x2, i64 1)
+///   br c
+/// c:
+///   %y0 = phi i64 [(a, %x1.0), (b, %x2.0)]
+///   %y1 = phi i64 [(a, %x1.1), (b, %x2.1)]
+class SplitStructPhis : public llvm::FunctionPass {
+public:
+  static char ID;
+  SplitStructPhis() : llvm::FunctionPass(ID) {}
+
+  bool runOnFunction(llvm::Function &F) override {
+    SmallVector<PHINode *, 16> SingleIncoming;
+    SmallVector<PHINode *, 16> MultiIncoming;
+
+    for (BasicBlock &BB : F) {
+      for (Instruction &I : BB) {
+        auto *Phi = dyn_cast<PHINode>(&I);
+        if (Phi == nullptr or not isa<StructType>(Phi->getType()))
+          continue;
+        if (Phi->getNumIncomingValues() == 1)
+          SingleIncoming.push_back(Phi);
+        else
+          MultiIncoming.push_back(Phi);
+      }
+    }
+
+    bool Changed = not SingleIncoming.empty() or not MultiIncoming.empty();
+
+    // Trivially eliminate single-incoming struct phis.
+    for (PHINode *Phi : SingleIncoming) {
+      Phi->replaceAllUsesWith(Phi->getIncomingValue(0));
+      Phi->eraseFromParent();
+    }
+
+    if (MultiIncoming.empty())
+      return Changed;
+
+    auto OpaqueEVPool = FunctionTags::OpaqueExtractValue
+                          .getPool(*F.getParent());
+    LLVMContext &Ctx = F.getContext();
+    Type *Int64Ty = IntegerType::getInt64Ty(Ctx);
+
+    // Step 1: pre-create empty per-field phis for every struct phi, so we can
+    // resolve cross-references (including cycles) between chained struct phis.
+    DenseMap<PHINode *, SmallVector<PHINode *, 2>> PerFieldPhis;
+    for (PHINode *Phi : MultiIncoming) {
+      auto *ST = cast<StructType>(Phi->getType());
+      unsigned NumIncoming = Phi->getNumIncomingValues();
+      SmallVector<PHINode *, 2> Fields;
+      for (Type *FieldType : ST->elements()) {
+        auto *NewPhi = PHINode::Create(FieldType, NumIncoming, "", Phi);
+        NewPhi->setDebugLoc(Phi->getDebugLoc());
+        Fields.push_back(NewPhi);
+      }
+      PerFieldPhis[Phi] = std::move(Fields);
+    }
+
+    // Step 2: fill in the incoming values for each per-field phi.
+    for (PHINode *Phi : MultiIncoming) {
+      auto *ST = cast<StructType>(Phi->getType());
+      auto &Fields = PerFieldPhis[Phi];
+
+      for (unsigned I = 0, N = Phi->getNumIncomingValues(); I < N; ++I) {
+        Value *Incoming = Phi->getIncomingValue(I);
+        BasicBlock *Pred = Phi->getIncomingBlock(I);
+
+        // Undef / poison: propagate the same to every per-field phi.
+        if (isa<UndefValue>(Incoming) or isa<PoisonValue>(Incoming)) {
+          for (auto &&[FieldType, NewPhi] : zip(ST->elements(), Fields)) {
+            Value *V = isa<PoisonValue>(Incoming) ?
+                         cast<Value>(PoisonValue::get(FieldType)) :
+                         UndefValue::get(FieldType);
+            NewPhi->addIncoming(V, Pred);
+          }
+          continue;
+        }
+
+        // Chained struct phi: reuse the producer's per-field phis directly.
+        if (auto *IncomingPhi = dyn_cast<PHINode>(Incoming)) {
+          auto It = PerFieldPhis.find(IncomingPhi);
+          if (It != PerFieldPhis.end()) {
+            for (auto &&[Src, Dst] : zip(It->second, Fields))
+              Dst->addIncoming(Src, Pred);
+            continue;
+          }
+        }
+
+        // If the incoming is a `struct_initializer` call, use its arguments
+        // directly instead of materializing `OpaqueExtractvalue` calls that
+        // would just undo the packing. The `struct_initializer` call becomes
+        // dead afterwards and DCE will clean it up.
+        if (auto *Call = dyn_cast<CallInst>(Incoming);
+            Call != nullptr
+            and isCallToTagged(Call, FunctionTags::StructInitializer)) {
+          revng_assert(Call->arg_size() == Fields.size());
+          for (auto &&[Arg, FieldNewPhi] : zip(Call->args(), Fields))
+            FieldNewPhi->addIncoming(Arg.get(), Pred);
+          continue;
+        }
+
+        // General case: materialize one OpaqueExtractvalue per field at the
+        // end of the predecessor block.
+        Instruction *InsertBefore = Pred->getTerminator();
+        IRBuilder<> Builder(InsertBefore);
+        for (auto &&[Idx, FieldNewPhi] : llvm::enumerate(Fields)) {
+          Type *FieldType = ST->getElementType(Idx);
+          auto *FT = FunctionType::get(FieldType,
+                                       { Incoming->getType(), Int64Ty },
+                                       false);
+          FunctionTags::TypePair Key = { FieldType, Incoming->getType() };
+          auto *EVFn = OpaqueEVPool.get(Key, FT, "OpaqueExtractvalue");
+          auto *Index = ConstantInt::get(Int64Ty, Idx);
+          CallInst *Extract = Builder.CreateCall(EVFn, { Incoming, Index });
+          Extract->setDebugLoc(InsertBefore->getDebugLoc());
+          FieldNewPhi->addIncoming(Extract, Pred);
+        }
+      }
+    }
+
+    // Step 3: rewrite uses of the original struct phis.
+    //   - `OpaqueExtractvalue` users get rewired to the matching per-field phi.
+    //   - Chained struct phis already point at our per-field phis (Step 2), so
+    //     we leave their use of the original phi alone (it'll be dropped in
+    //     Step 4 when the chained phi itself is erased).
+    //   - Anything else: reconstruct the struct via `struct_initializer` at the
+    //     join block and redirect the use to the reconstruction.
+    // remove-lifting-artifacts has already purged the bodies of all
+    // non-isolated functions before this point, so don't put one back.
+    StructInitializers Initializers(F.getParent(), /* EmitBody */ false);
+
+    for (PHINode *Phi : MultiIncoming) {
+      auto &Fields = PerFieldPhis[Phi];
+
+      for (User *U : llvm::make_early_inc_range(Phi->users())) {
+        auto *Call = dyn_cast<CallInst>(U);
+        if (Call != nullptr
+            and isCallToTagged(Call, FunctionTags::OpaqueExtractValue)) {
+          auto *IndexConst = cast<ConstantInt>(Call->getArgOperand(1));
+          uint64_t Index = IndexConst->getZExtValue();
+          revng_assert(Index < Fields.size());
+          Call->replaceAllUsesWith(Fields[Index]);
+          Call->eraseFromParent();
+        }
+      }
+
+      // After OpaqueExtractvalue rewriting, any remaining non-chained use
+      // needs the original struct value. Reconstruct it via struct_initializer.
+      bool NeedsReconstruction = false;
+      for (User *U : Phi->users()) {
+        if (auto *OtherPhi = dyn_cast<PHINode>(U))
+          if (PerFieldPhis.find(OtherPhi) != PerFieldPhis.end())
+            continue;
+        NeedsReconstruction = true;
+        break;
+      }
+
+      if (NeedsReconstruction) {
+        Instruction *InsertionPoint = Phi->getParent()->getFirstNonPHI();
+        revng::IRBuilder ReconstructBuilder(Ctx);
+        ReconstructBuilder.SetInsertPoint(InsertionPoint, Phi->getDebugLoc());
+
+        SmallVector<Value *, 4> FieldValues(Fields.begin(), Fields.end());
+        auto *ST = cast<StructType>(Phi->getType());
+        CallInst *Reconstructed = Initializers.createCall(ReconstructBuilder,
+                                                          ST,
+                                                          FieldValues);
+
+        for (User *U : llvm::make_early_inc_range(Phi->users())) {
+          if (auto *OtherPhi = dyn_cast<PHINode>(U))
+            if (PerFieldPhis.find(OtherPhi) != PerFieldPhis.end())
+              continue;
+          U->replaceUsesOfWith(Phi, Reconstructed);
+        }
+      }
+    }
+
+    // Step 4: erase the original struct phis. Any remaining cross-references
+    // between them (in chained-phi operand lists) are dropped via undef so
+    // that the erases can happen in any order.
+    for (PHINode *Phi : MultiIncoming)
+      Phi->replaceAllUsesWith(UndefValue::get(Phi->getType()));
+    for (PHINode *Phi : MultiIncoming)
+      Phi->eraseFromParent();
+
+    return Changed;
+  }
+};
+
+char SplitStructPhis::ID;
+static RegisterPass<SplitStructPhis> R("split-struct-phis", "", false, false);
diff --git a/lib/Canonicalize/SwitchToStatements.cpp b/lib/Canonicalize/SwitchToStatements.cpp
index b3e95d83a..e49d58ba4 100644
--- a/lib/Canonicalize/SwitchToStatements.cpp
+++ b/lib/Canonicalize/SwitchToStatements.cpp
@@ -494,7 +494,8 @@ public:
   }
 
   LatticeElement applyTransferFunction(ProgramPointNode *L,
-                                       const LatticeElement &E) const;
+                                       const LatticeElement &E,
+                                       mfp::NoExtraState &ExtraState) const;
 
 private:
   void applyTransferFunctionImpl(Instruction *I, LatticeElement &E) const;
@@ -509,7 +510,7 @@ template<bool IsLegacy>
 using LatticeElement = AEMFP<IsLegacy>::LatticeElement;
 
 template<bool IsLegacy>
-using AvailableExpressionsMap = MFP::MFIResultMap<AEMFP<IsLegacy>>;
+using AvailableExpressionsMap = mfp::MFIResultMap<AEMFP<IsLegacy>>;
 
 static bool legacyLocalVariablesNoAlias(const Instruction *I,
                                         const Instruction *J) {
@@ -644,8 +645,8 @@ void AEMFP<IsLegacy>::applyTransferFunctionImpl(Instruction *I,
 template<bool IsLegacy>
 AEMFP<IsLegacy>::LatticeElement
 AEMFP<IsLegacy>::applyTransferFunction(ProgramPointNode *ProgramPoint,
-                                       const AEMFP<IsLegacy>::LatticeElement &E)
-  const {
+                                       const AEMFP<IsLegacy>::LatticeElement &E,
+                                       mfp::NoExtraState &ExtraState) const {
 
   Instruction *I = ProgramPoint->TheInstruction;
 
@@ -955,18 +956,23 @@ static AEResult<IsLegacy> getAvailableExpressions(Function &F,
     }
   }
 
-  AvailableSet Empty{};
   ProgramPointsCFG *Graph = &Result.ProgramPointsGraph;
   ProgramPointNode *Entry = Graph->getEntryNode();
 
-  AEMFP<IsLegacy> AvailableExpressionsMF{ AA, MST };
+  using AEMFP = AEMFP<IsLegacy>;
+  AEMFP AvailableExpressionsMF{ AA, MST };
+  std::vector Entries = { Entry };
+  mfp::MFPConfiguration<AEMFP> Configuration{
+    .Instance = &AvailableExpressionsMF,
+    .Flow = Graph,
+    .Bottom = &Bottom,
+    .ExtremalLabels = &Entries,
+    .EntryLabels = &Entries
+  };
+
   // std::exchange here is only needed to make revng check-conventions happy.
   std::exchange(Result.AvailableExpressions,
-                MFP::getMaximalFixedPoint<>(AvailableExpressionsMF,
-                                            Graph,
-                                            Bottom,
-                                            Empty,
-                                            { Entry }));
+                mfp::getMaximalFixedPoint<AEMFP>(Configuration));
   return Result;
 }
 
diff --git a/lib/CliftEmitC/CBackend.cpp b/lib/CliftEmitC/CBackend.cpp
index 477e06cb8..7671d009f 100644
--- a/lib/CliftEmitC/CBackend.cpp
+++ b/lib/CliftEmitC/CBackend.cpp
@@ -98,8 +98,6 @@ public:
   //===---------------------------- Expressions ---------------------------===//
 
   RecursiveCoroutine<void> emitUndefExpression(mlir::Value V) {
-    revng_assert(isScalarType(V.getType()));
-
     Tokens.emitLiteralIdentifier("undef");
     Tokens.emitOperator(CTE::Operator::LeftParenthesis);
     emitType(V.getType());
diff --git a/lib/CliftTransforms/ImplicitCastElision.cpp b/lib/CliftTransforms/ImplicitCastElision.cpp
index 8a88fba74..fe7f88317 100644
--- a/lib/CliftTransforms/ImplicitCastElision.cpp
+++ b/lib/CliftTransforms/ImplicitCastElision.cpp
@@ -44,14 +44,13 @@ public:
                   BitwiseOrOp,
                   BitwiseXorOp,
                   ShiftLeftOp,
-                  ShiftRightOp,
-                  CmpEqOp,
-                  CmpNeOp,
-                  CmpLtOp,
-                  CmpGtOp,
-                  CmpLeOp,
-                  CmpGeOp>(Op))
+                  ShiftRightOp>(Op))
       return elideArithmeticCasts(Op);
+
+    if (mlir::isa<CmpEqOp, CmpNeOp, CmpLtOp, CmpGtOp, CmpLeOp, CmpGeOp>(Op)) {
+      if (clift::unwrapped_isa<IntegralType>(Op->getOperand(0).getType()))
+        elideArithmeticCasts(Op);
+    }
   }
 
 private:
diff --git a/lib/Clifter/Clifter.cpp b/lib/Clifter/Clifter.cpp
index 199fa30f9..7c2ed5bfa 100644
--- a/lib/Clifter/Clifter.cpp
+++ b/lib/Clifter/Clifter.cpp
@@ -1621,7 +1621,7 @@ private:
     Builder.create<GotoOp>(Loc, Iterator->second.Label);
   }
 
-  bool isCallToSPTAR(const llvm::CallInst *Call) {
+  bool returnsAggregate(const llvm::CallInst *Call) {
     if (not Call->hasMetadata(PrototypeMDName))
       return false;
 
@@ -1629,7 +1629,7 @@ private:
     auto Layout = abi::FunctionType::Layout::make(*ModelCallType);
     namespace ReturnMethod = abi::FunctionType::ReturnMethod;
 
-    return Layout.hasSPTAR();
+    return Layout.returnMethod() == ReturnMethod::ModelAggregate;
   }
 
   // This function emits a single basic block as part of a larger C scope.
@@ -1751,7 +1751,7 @@ private:
           continue;
 
         // Some function calls are emitted in local variable initializers.
-        if (isCallToSPTAR(Call)) {
+        if (returnsAggregate(Call)) {
           mlir::Location Loc = C.getLocation(Call);
 
           auto Op = Builder.create<ExpressionStatementOp>(Loc);
@@ -1801,10 +1801,6 @@ private:
         mlir::Type FuncReturnType = FunctionType.getReturnType();
         mlir::Type LLVMReturnType = FuncReturnType;
 
-        // In SPTAR functions, values are returned by address. In this case
-        if (FunctionLayout.hasSPTAR())
-          LLVMReturnType = C.getPointerType(LLVMReturnType);
-
         // Emit the expression tree rooted at the return instruction directly
         // into the expression region of the newly created return operation:
         emitExpressionTreeImpl(Op.getResult(), [&]() {
@@ -1830,47 +1826,11 @@ private:
                                                         ReturnValue);
           }
 
-          if (FunctionLayout.hasSPTAR()) {
-            // TODO: This may happen when the pointer size of the Model doesn't
-            // match the pointer size on LLVM IR, due to mismatching DataLayout.
-            // SPTAR functions return model-pointer-sized integers, with the
-            // semantic is to actually return the pointee by copy.
-            // Given that the return value is model-pointer-sized, it's size
-            // doesn't necessarily match the pointer size in LLVM's DataLayout.
-            // Until we don't solve the broader issue of LLVM's DataLayout
-            // mismatching the pointer size of the input binary and the Model,
-            // we'll have to deal with this corner case.
-            // Another option would be to change SPTAR function to return
-            // llvm-pointer-sized integers or even LLVM's pointers, instead of
-            // model-pointer-sized integers.
-            uint64_t
-              LLVMPointerSize = unwrapped_cast<PointerType>(LLVMReturnType)
-                                  .getObjectSize();
-            uint64_t ModelPointerSize = C.getModelPointerSize();
-            uint64_t OperandSize = unwrapped_cast<IntegerType>(ReturnValue
-                                                                 .getType())
-                                     .getObjectSize();
-            revng_assert(ModelPointerSize == OperandSize);
-            if (ModelPointerSize != LLVMPointerSize)
-              ReturnValue = emitIntegerCast(TerminalLoc,
-                                            ReturnValue,
-                                            LLVMPointerSize);
-          }
-
           // Emit an implicit cast to the required return type if necessary:
           ReturnValue = emitImplicitBitcast(TerminalLoc,
                                             ReturnValue,
                                             LLVMReturnType);
 
-          // In the case of SPTAR, because in the LLVM IR the return is by
-          // address, but in Clift the return is by value as usual, a final
-          // indirection is needed to convert the LLVM IR pointer to a value:
-          if (FunctionLayout.hasSPTAR()) {
-            ReturnValue = Builder.create<IndirectionOp>(TerminalLoc,
-                                                        FuncReturnType,
-                                                        ReturnValue);
-          }
-
           return ReturnValue;
         });
       }
diff --git a/lib/EarlyFunctionAnalysis/AnalyzeRegisterUsage.cpp b/lib/EarlyFunctionAnalysis/AnalyzeRegisterUsage.cpp
index 38c2cd3a1..f990acff3 100644
--- a/lib/EarlyFunctionAnalysis/AnalyzeRegisterUsage.cpp
+++ b/lib/EarlyFunctionAnalysis/AnalyzeRegisterUsage.cpp
@@ -261,11 +261,26 @@ RUAResults analyzeRegisterUsage(Function *F,
     // Run the liveness analysis
     revng_log(Log, "Running Liveness");
     rua::Liveness Liveness(Function.Function);
-    auto AnalysisResult = MFP::getMaximalFixedPoint(Liveness,
-                                                    &Function.Function,
-                                                    Liveness.defaultValue(),
-                                                    Liveness.defaultValue(),
-                                                    { Function.ReturnNode });
+
+    auto DefaultValue = Liveness.defaultValue();
+    std::vector<const rua::BlockNode *> ExtremalLabels{ Function.ReturnNode };
+    // Backward analysis: `getEntryNode(Inverse<...>)` is unreliable (returns
+    // the forward entry), and seeding only from the return node would skip
+    // no-return blocks (e.g., calls to non-returning functions). Use `All` to
+    // seed RPOT from every node.
+    mfp::MFPConfiguration<rua::Liveness> Configuration{
+      .Instance = &Liveness,
+      .Flow = &Function.Function,
+      .Bottom = &DefaultValue,
+      .ExtremalValue = &DefaultValue,
+      .ExtremalLabels = &ExtremalLabels,
+      .EntryLabels = mfp::All{}
+    };
+
+    using namespace mfp;
+    using InverseGT = llvm::GraphTraits<llvm::Inverse<const rua::Function *>>;
+    auto GetMaximalFixedPoint = getMaximalFixedPoint<rua::Liveness, InverseGT>;
+    auto AnalysisResult = GetMaximalFixedPoint(Configuration);
 
     // Collect registers alive at the entry
     revng_log(Log, "Registers alive at the entry of the function:");
@@ -303,11 +318,24 @@ RUAResults analyzeRegisterUsage(Function *F,
     rua::ReachingDefinitions ReachingDefinitions(Function.Function);
     auto DefaultValue = ReachingDefinitions.defaultValue();
     auto *EntryNode = Function.Function.getEntryNode();
-    auto AnalysisResult = MFP::getMaximalFixedPoint(ReachingDefinitions,
-                                                    &Function.Function,
-                                                    DefaultValue,
-                                                    DefaultValue,
-                                                    { EntryNode });
+    std::vector ExtremalLabels{ EntryNode };
+
+    // Seed RPOT from every node: callers read `AnalysisResult.at(...)` for
+    // nodes (e.g. `ReturnNode`) that may not be forward-reachable from the
+    // entry (functions with no return paths). With `Entry{}` those nodes
+    // would be absent from the result map.
+    mfp::MFPConfiguration<rua::ReachingDefinitions> Configuration{
+      .Instance = &ReachingDefinitions,
+      .Flow = &Function.Function,
+      .Bottom = &DefaultValue,
+      .ExtremalValue = &DefaultValue,
+      .ExtremalLabels = &ExtremalLabels,
+      .EntryLabels = mfp::All{}
+    };
+
+    using namespace mfp;
+    auto GetMaximalFixedPoint = getMaximalFixedPoint<rua::ReachingDefinitions>;
+    auto AnalysisResult = GetMaximalFixedPoint(Configuration);
 
     auto Compute = [&AnalysisResult, &Function](rua::Function::Node *Node,
                                                 bool Before) {
diff --git a/lib/FunctionIsolation/EnforceABI.cpp b/lib/FunctionIsolation/EnforceABI.cpp
index ddeb52034..063bcbb54 100644
--- a/lib/FunctionIsolation/EnforceABI.cpp
+++ b/lib/FunctionIsolation/EnforceABI.cpp
@@ -381,6 +381,7 @@ void EnforceABI::handleRegularFunctionCall(const MetaAddress &CallerAddress,
     const auto *Prototype = Binary.prototypeOrDefault(ModelFunc.prototype());
     revng_assert(Prototype != nullptr);
     auto UsedRegisters = abi::FunctionType::usedRegisters(*Prototype);
+
     Callee = getOrCreateNewFunction(*Callee, UsedRegisters);
   }
 
diff --git a/lib/FunctionIsolation/PromoteCSVs.cpp b/lib/FunctionIsolation/PromoteCSVs.cpp
index a27fd136c..20979eead 100644
--- a/lib/FunctionIsolation/PromoteCSVs.cpp
+++ b/lib/FunctionIsolation/PromoteCSVs.cpp
@@ -20,7 +20,7 @@
 #include "revng/Support/IRHelpers.h"
 
 using namespace llvm;
-using namespace MFP;
+using namespace mfp;
 
 // TODO: switch from CallInst to CallBase
 
@@ -450,9 +450,11 @@ static bool needsWrapper(Function *F) {
 struct UsedRegistersMFI : public SetUnionLattice<FunctionNodeData::UsedCSVSet> {
   using Label = FunctionNode *;
   using GraphType = GenericCallGraph *;
+  using ExtraStateType = mfp::NoExtraState;
 
   static LatticeElement applyTransferFunction(Label L,
-                                              const LatticeElement &Value) {
+                                              const LatticeElement &Value,
+                                              mfp::NoExtraState &) {
     return combineValues(L->UsedCSVs, Value);
   }
 };
@@ -542,12 +544,8 @@ CSVsUsageMap PromoteCSVs::getUsedCSVs(ArrayRef<CallInst *> CallsRange) {
     }
   }
 
-  auto AnalysisResult = getMaximalFixedPoint<UsedRegistersMFI>({},
-                                                               &CallGraph,
-                                                               {},
-                                                               {},
-                                                               {},
-                                                               {});
+  auto GetMaximalFixedPoint = getMaximalFixedPoint<UsedRegistersMFI>;
+  auto AnalysisResult = GetMaximalFixedPoint({ .Flow = &CallGraph });
 
   // Populate results set
   for (auto &[Label, Value] : AnalysisResult) {
diff --git a/lib/FunctionIsolation/StructInitializers.cpp b/lib/FunctionIsolation/StructInitializers.cpp
index 008ed4b84..c6d05cf0a 100644
--- a/lib/FunctionIsolation/StructInitializers.cpp
+++ b/lib/FunctionIsolation/StructInitializers.cpp
@@ -9,8 +9,8 @@ using namespace llvm;
 
 const char *StructInitializerPrefix = "struct_initializer";
 
-StructInitializers::StructInitializers(llvm::Module *M) :
-  Pool(M, false), Context(M->getContext()) {
+StructInitializers::StructInitializers(llvm::Module *M, bool EmitBody) :
+  Pool(M, false), Context(M->getContext()), EmitBody(EmitBody) {
   Pool.setMemoryEffects(MemoryEffects::none());
   Pool.addFnAttribute(Attribute::NoUnwind);
   Pool.addFnAttribute(Attribute::WillReturn);
@@ -21,12 +21,9 @@ StructInitializers::StructInitializers(llvm::Module *M) :
   Pool.initializeFromReturnType(FunctionTags::StructInitializer);
 }
 
-Instruction *StructInitializers::createReturn(revng::IRBuilder &Builder,
-                                              ArrayRef<Value *> Values) {
-  // Obtain return StructType
-  auto *FT = Builder.GetInsertBlock()->getParent()->getFunctionType();
-  auto *ReturnType = cast<StructType>(FT->getReturnType());
-
+CallInst *StructInitializers::createCall(revng::IRBuilder &Builder,
+                                         StructType *ReturnType,
+                                         ArrayRef<Value *> Values) {
   SmallVector<Type *, 8> Types;
   llvm::copy(ReturnType->elements(), std::back_inserter(Types));
 
@@ -36,8 +33,10 @@ Instruction *StructInitializers::createReturn(revng::IRBuilder &Builder,
                                    Types,
                                    StructInitializerPrefix);
 
-  // Lazily populate its body
-  if (Initializer->isDeclaration()) {
+  // Lazily populate its body, unless the caller opted out (e.g., the body
+  // would otherwise persist past `remove-lifting-artifacts` and confuse later
+  // canonicalize passes that expect non-isolated functions to be declarations).
+  if (EmitBody and Initializer->isDeclaration()) {
     auto *Entry = BasicBlock::Create(Context, "", Initializer);
 
     // TODO: the checks should be enabled conditionally based on the user.
@@ -51,5 +50,14 @@ Instruction *StructInitializers::createReturn(revng::IRBuilder &Builder,
   }
 
   // Emit a call in the caller
-  return Builder.CreateRet(Builder.CreateCall(Initializer, Values));
+  return cast<CallInst>(Builder.CreateCall(Initializer, Values));
+}
+
+Instruction *StructInitializers::createReturn(revng::IRBuilder &Builder,
+                                              ArrayRef<Value *> Values) {
+  // Obtain return StructType
+  auto *FT = Builder.GetInsertBlock()->getParent()->getFunctionType();
+  auto *ReturnType = cast<StructType>(FT->getReturnType());
+
+  return Builder.CreateRet(createCall(Builder, ReturnType, Values));
 }
diff --git a/lib/Lift/CodeGenerator.cpp b/lib/Lift/CodeGenerator.cpp
index 4d3f53a99..0790ce7f9 100644
--- a/lib/Lift/CodeGenerator.cpp
+++ b/lib/Lift/CodeGenerator.cpp
@@ -536,7 +536,6 @@ void CodeGenerator::translate(LibTcg &LibTcg,
 
     } // End loop over instructions
 
-    TranslateTask.complete();
     TranslateTask.advance("Finalization", true);
 
     Variables.closeTranslationBlock();
diff --git a/lib/Model/FunctionTags.cpp b/lib/Model/FunctionTags.cpp
index ccb62eeb2..127c49889 100644
--- a/lib/Model/FunctionTags.cpp
+++ b/lib/Model/FunctionTags.cpp
@@ -104,9 +104,7 @@ FunctionPoolTag<TypePair>
                        llvm::Attribute::NoMerge,
                        llvm::Attribute::NoUnwind,
                        llvm::Attribute::WillReturn },
-                     // The following is necessary to prevent the optimizer to
-                     // move these around.
-                     llvm::MemoryEffects::inaccessibleMemOnly(),
+                     llvm::MemoryEffects::none(),
                      { &FunctionTags::UniquedByPrototype },
                      [](OpaqueFunctionsPool<TypePair> &Pool,
                         llvm::Module &M,
diff --git a/lib/Model/Importer/DebugInfo/DwarfToModelConverter.cpp b/lib/Model/Importer/DebugInfo/DwarfToModelConverter.cpp
index efc754a8c..54c53c4b2 100644
--- a/lib/Model/Importer/DebugInfo/DwarfToModelConverter.cpp
+++ b/lib/Model/Importer/DebugInfo/DwarfToModelConverter.cpp
@@ -3,6 +3,7 @@
 //
 
 #include "llvm/ADT/STLExtras.h"
+#include "llvm/Support/MathExtras.h"
 #include "llvm/Support/Progress.h"
 
 #include "revng/Model/Importer/DebugInfo/DwarfImporter.h"
@@ -297,6 +298,12 @@ void DwarfToModelConverter::createType(const DWARFDie &Die) {
       return;
     }
 
+    if (Kind == model::PrimitiveKind::Float and Size > 8) {
+      reportIgnoredDie(Die, "Ignoring floating-point primitives larger than 8");
+      createInvalidPrimitivePlaceholder(Die);
+      return;
+    }
+
     record(Die, model::PrimitiveType::make(Kind, Size));
   } break;
 
diff --git a/lib/PromoteStackPointer/DetectStackSizePass.cpp b/lib/PromoteStackPointer/DetectStackSizePass.cpp
index 9fac3e8fa..6c0b52ee2 100644
--- a/lib/PromoteStackPointer/DetectStackSizePass.cpp
+++ b/lib/PromoteStackPointer/DetectStackSizePass.cpp
@@ -301,7 +301,7 @@ void DetectStackSize::electFunctionStackFrameSize(FunctionStackInfo &FSI) {
   // If we have call site, the stack size is the highest value of the
   // following expression:
   //
-  //    StackSizeAtCallSite - CallSiteStackArgumentsSize
+  //     StackSizeAtCallSite - CallSiteStackArgumentsSize
   //
   for (const CallSite &CallSite : FSI.CallSites) {
     auto MaybeNewCandidate = handleCallSite(CallSite);
@@ -322,6 +322,15 @@ void DetectStackSize::electFunctionStackFrameSize(FunctionStackInfo &FSI) {
 
     auto EmptyStruct = Binary->makeStructDefinition(*StackSize).second;
     ModelFunction.StackFrame().Type() = std::move(EmptyStruct);
+  } else {
+    if (Log.isEnabled()) {
+      Log << "No valid stack size: ";
+      if (StackSize.has_value())
+        Log << "(none)";
+      else
+        Log << *StackSize;
+      Log << DoLog;
+    }
   }
 }
 
diff --git a/lib/PromoteStackPointer/SegregateStackAccessesPass.cpp b/lib/PromoteStackPointer/SegregateStackAccessesPass.cpp
index 0636e367f..20b96876d 100644
--- a/lib/PromoteStackPointer/SegregateStackAccessesPass.cpp
+++ b/lib/PromoteStackPointer/SegregateStackAccessesPass.cpp
@@ -5,9 +5,11 @@
 #include <optional>
 #include <set>
 
+#include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/STLExtras.h"
 #include "llvm/IR/DerivedTypes.h"
 #include "llvm/IR/Instructions.h"
+#include "llvm/IR/PatternMatch.h"
 #include "llvm/IR/Verifier.h"
 
 #include "revng/ABI/FunctionType/Layout.h"
@@ -35,9 +37,24 @@
 
 using namespace llvm;
 using std::tie;
+using StackSpan = abi::FunctionType::Layout::Argument::StackSpan;
 
 static Logger Log("segregate-stack-accesses");
 
+struct OffsetRange {
+  int64_t Start = 0;
+  int64_t End = 0;
+};
+using OffsetRanges = SmallVector<OffsetRange>;
+
+static uint64_t getRangeSize(const OffsetRanges &Ranges) {
+  uint64_t Result = 0;
+  for (const auto &Range : Ranges) {
+    Result += Range.End - Range.Start;
+  }
+  return Result;
+}
+
 inline Value *createAdd(revng::IRBuilder &B, Value *V, uint64_t Addend) {
   return B.CreateAdd(V, ConstantInt::get(V->getType(), Addend));
 }
@@ -89,13 +106,8 @@ static std::optional<int64_t> getStackOffset(Instruction *I) {
         auto MaybeStart = getSignedConstantArg(Call, 1);
         auto MaybeEnd = getSignedConstantArg(Call, 2);
 
-        revng_log(Log, "AccessSize: " << AccessSize);
-        revng_log(Log, "MaybeStart: " << (MaybeStart ? *MaybeStart : -1));
-        revng_log(Log, "MaybeEnd: " << (MaybeEnd ? *MaybeEnd : -1));
-
         if (MaybeStart and MaybeEnd
             and *MaybeEnd == *MaybeStart + AccessSize + 1) {
-          revng_log(Log, "StackOffset found: " << *MaybeStart);
           return MaybeStart;
         }
       }
@@ -105,45 +117,94 @@ static std::optional<int64_t> getStackOffset(Instruction *I) {
   return {};
 }
 
-struct StoredByte {
-  int64_t StackOffset = 0;
-  llvm::StoreInst *Store = nullptr;
-  unsigned StoreOffset = 0;
+/// Per-function memoizer for `getStackOffset`. `getStackOffset` walks the
+/// def-use chain on every call; this class amortizes that cost by storing
+/// the result the first time each instruction is queried.
+class StackOffsetCache {
+private:
+  llvm::DenseMap<llvm::Instruction *, std::optional<int64_t>> Cache;
 
-  bool operator<(const StoredByte &Other) const {
-    auto ThisTuple = std::tie(StackOffset, Store, StoreOffset);
-    auto OtherTuple = std::tie(Other.StackOffset,
-                               Other.Store,
-                               Other.StoreOffset);
-    return ThisTuple < OtherTuple;
+public:
+  std::optional<int64_t> get(llvm::Instruction *I) {
+    auto [It, Inserted] = Cache.try_emplace(I);
+    if (Inserted)
+      It->second = getStackOffset(I);
+    return It->second;
   }
 };
 
+struct StoredByte {
+  int64_t StackOffset = 0;
+  llvm::Instruction *Writer = nullptr;
+
+  bool operator<(const StoredByte &Other) const {
+    auto ThisTuple = std::tie(StackOffset, Writer);
+    auto OtherTuple = std::tie(Other.StackOffset, Other.Writer);
+    return ThisTuple < OtherTuple;
+  }
+
+  void dump() const debug_function { dump(dbg, 0); }
+
+  template<typename T>
+  void dump(T &Stream, unsigned Indent) const {
+    for (unsigned I = 0; I < Indent; ++I)
+      Stream << "  ";
+    Stream << StackOffset << ": " << getName(Writer) << "\n";
+  }
+};
+
+/// This class tracks the range of stack that's "owned" by a certain alloca.
+///
+/// You can have multiple instance of this, for instance one for the caller
+/// function and then one for each call site.
+///
+/// In any case, the data in this data structure is always relative to the value
+/// of the stack pointer at the entry of the function.
+///
+/// This means that you will have positive values for stack arguments of the
+/// caller, while for all the rest you should expect negative values.
+/// Users of this class are expected to follow this rule.
 class StackAccessRedirector {
 private:
-  using Span = abi::FunctionType::Layout::Argument::StackSpan;
-
-private:
-  int64_t BaseOffset;
-  std::map<int64_t, std::pair<uint64_t, Value *>> Map;
+  /// This is for debugging purposes only
+  Value *Reference = nullptr;
+  std::map<int64_t, std::pair<int64_t, Value *>> Map;
 
 public:
-  StackAccessRedirector(int64_t BaseOffset) : BaseOffset(BaseOffset) {}
+  StackAccessRedirector() = default;
+  StackAccessRedirector(Value *Reference) : Reference(Reference) {}
 
-  void recordSpan(const Span &Span, Value *BaseAddress) {
+public:
+  Value *reference() const { return Reference; }
+
+public:
+  void recordSpan(const OffsetRange &Span, Value *BaseAddress) {
+    revng_log(Log,
+              "Redirecting from " << Span.Start << " to " << Span.End << " to "
+                                  << getName(BaseAddress));
     revng_assert(BaseAddress->getType()->isIntegerTy());
-    auto Offset = BaseOffset + Span.Offset;
-    revng_assert(!Map.contains(Offset));
-    Map[Offset] = { Span.Size, BaseAddress };
+    revng_assert(!Map.contains(Span.Start));
+    Map[Span.Start] = { Span.End, BaseAddress };
 
+    if (not verify()) {
+      dump();
+      revng_abort();
+    }
     revng_assert(verify());
   }
 
+  void recordSpan(const StackSpan &Span, Value *BaseAddress) {
+    OffsetRange NewRange{ static_cast<int64_t>(Span.Offset),
+                          static_cast<int64_t>(Span.Offset + Span.Size) };
+    return recordSpan(NewRange, BaseAddress);
+  }
+
 public:
   std::optional<std::pair<uint64_t, Value *>>
   computeNewBase(int64_t Offset, uint64_t Size) const {
 
     revng_log(Log, "Searching for " << Offset << " of size " << Size);
+    LoggerIndent Indent(Log);
 
     auto It = Map.upper_bound(Offset);
     if (It == Map.begin()) {
@@ -154,14 +215,12 @@ public:
     --It;
 
     int64_t SpanStart = It->first;
-    uint64_t SpanSize = It->second.first;
+    int64_t SpanEnd = It->second.first;
     Value *BaseAddress = It->second.second;
 
     using OSI = OverflowSafeInt<int64_t>;
-    auto MaybeSpanEnd = (OSI(SpanStart) + SpanSize).value();
     auto MaybeEnd = (OSI(Offset) + Size).value();
-    if (not MaybeSpanEnd or not MaybeEnd or Offset >= *MaybeSpanEnd
-        or *MaybeEnd > *MaybeSpanEnd) {
+    if (not MaybeEnd or Offset >= SpanEnd or *MaybeEnd > SpanEnd) {
       revng_log(Log, "Not found");
       return std::nullopt;
     }
@@ -176,77 +235,591 @@ public:
       auto FirstToSemiLast = llvm::make_range(Map.begin(), --Map.end());
       auto SecondToLast = llvm::make_range(++Map.begin(), Map.end());
       for (auto &&[Current, Next] : llvm::zip(FirstToSemiLast, SecondToLast)) {
-        auto CurrentEnd = Current.first
-                          + static_cast<int64_t>(Current.second.first);
+        auto CurrentEnd = Current.second.first;
         auto NextStart = Next.first;
         if (CurrentEnd > NextStart)
           return false;
       }
     }
+
     return true;
   }
 
   template<typename T>
   void dump(T &Stream) const {
     for (auto &&[K, V] : Map) {
-      Stream << K << ": [" << V.first << ", " << getName(V.second) << "]\n";
+      Stream << K << " -> " << V.first << ": " << getName(V.second) << "\n";
     }
   }
 
   void dump() const debug_function { dump(dbg); }
 };
 
-using Lattice = std::set<StoredByte>;
+class FunctionStackAccessRedirectors {
+private:
+  const StackAccessRedirector *FunctionRedirector = nullptr;
+  std::vector<std::unique_ptr<StackAccessRedirector>> CallSiteRedirectors;
+  std::map<Instruction *, const StackAccessRedirector *>
+    RedirectorForInstruction;
 
-struct SegregateStackAccessesMFI : public SetUnionLattice<Lattice> {
+public:
+  FunctionStackAccessRedirectors() = default;
+  explicit FunctionStackAccessRedirectors(const StackAccessRedirector
+                                            *FunctionRedirector) :
+    FunctionRedirector(FunctionRedirector) {}
+
+public:
+  void setFunctionRedirector(const StackAccessRedirector *Redirector) {
+    FunctionRedirector = Redirector;
+  }
+
+  bool empty() const {
+    return FunctionRedirector == nullptr and CallSiteRedirectors.empty();
+  }
+
+  const StackAccessRedirector *get(Instruction *I) const {
+    auto It = RedirectorForInstruction.find(I);
+    if (It == RedirectorForInstruction.end())
+      return FunctionRedirector;
+    else
+      return It->second;
+  }
+
+  const StackAccessRedirector *
+  getCommon(const SmallVector<Instruction *> &Instructions) {
+    const StackAccessRedirector *Result = FunctionRedirector;
+    bool First = true;
+    for (auto *Writer : Instructions) {
+      const StackAccessRedirector *WriterRedirector = get(Writer);
+      if (First) {
+        First = false;
+        Result = WriterRedirector;
+      } else if (WriterRedirector == Result) {
+        // All good so far
+      } else {
+        revng_log(Log,
+                  "Different writers of this load are associated to "
+                  "different redirectors. Falling back to the "
+                  "default one.");
+        return FunctionRedirector;
+      }
+    }
+
+    return Result;
+  }
+
+public:
+  const StackAccessRedirector *record(StackAccessRedirector &&Redirector) {
+    using SAR = StackAccessRedirector;
+    CallSiteRedirectors.push_back(std::make_unique<SAR>(std::move(Redirector)));
+    return CallSiteRedirectors.back().get();
+  }
+
+  void registerOwner(const StackAccessRedirector *Redirector, Instruction *I) {
+    revng_log(Log,
+              "Registering redirector " << Redirector << " for " << getName(I));
+    auto IsRedirector = [&Redirector](const auto &ExistingRedirector) {
+      return ExistingRedirector.get() == Redirector;
+    };
+    revng_assert(llvm::any_of(CallSiteRedirectors, IsRedirector));
+
+    RedirectorForInstruction[I] = Redirector;
+  }
+};
+
+class MemoryAreaState : public std::set<StoredByte> {
+public:
+  void eraseRange(int64_t Start, int64_t End) {
+    erase(lower_bound(StoredByte{ Start }), upper_bound(StoredByte{ End }));
+  }
+
+  void record(int64_t Start, int64_t End, llvm::Instruction *Writer) {
+    revng_assert(Start <= End);
+    for (auto Offset = Start; Offset < End; ++Offset)
+      insert({ Offset, Writer });
+  }
+
+public:
+  template<typename T>
+  void dump(T &Stream, unsigned Indent) const {
+    for (const StoredByte &Stored : *this)
+      Stored.dump(Stream, Indent);
+  }
+
+  void dump() const debug_function { dump(dbg, 0); }
+};
+
+class InstructionStackUsage;
+
+class CallSite {
+public:
+  size_t CallInstructionPushSize = 0;
+  std::optional<int64_t> MaybeStackOffset;
+  abi::FunctionType::Layout Layout;
+  CallInst *OldCall = nullptr;
+
+  OffsetRanges StackArgumentRanges;
+  std::optional<OffsetRange> StackReturnValueRange;
+
+  StackAccessRedirector Redirector;
+
+public:
+  static CallSite make(CallInst *SSACSCall,
+                       const model::TypeDefinition &Prototype,
+                       size_t CallInstructionPushSize);
+
+public:
+  void processSPTAR(CallInst *InitLocalSPCall,
+                    uint64_t StackFrameSize,
+                    const MemoryAreaState &State,
+                    InstructionStackUsage &StackUsage);
+
+private:
+  std::optional<OffsetRange>
+  stackArgumentRange(const abi::FunctionType::Layout::Argument &Argument)
+    const {
+
+    if (not Argument.Stack.has_value())
+      return std::nullopt;
+
+    OverflowSafeInt<int64_t> StackSizeAtCallSite(MaybeStackOffset.value());
+
+    auto StartOffset = StackSizeAtCallSite + Argument.Stack->Offset
+                       + CallInstructionPushSize;
+    auto EndOffset = StartOffset + Argument.Stack->Size;
+
+    if (not StartOffset or not EndOffset) {
+      revng_log(Log,
+                "Overflow in computing stack argument offset, "
+                "ignoring");
+      return std::nullopt;
+    }
+
+    return OffsetRange(*StartOffset, *EndOffset);
+  }
+
+public:
+  template<typename T>
+  void dump(T &Stream) const {
+    if (MaybeStackOffset.has_value()) {
+      Stream << "MaybeStackSize: " << *MaybeStackOffset;
+    } else {
+      Stream << "MaybeStackSize: no";
+    }
+    Stream << "\n";
+
+    Stream << "Layout:\n";
+    Layout.dump(Stream);
+    Stream << "\n";
+
+    Stream << "OldCall: " << getName(OldCall) << "\n";
+
+    Stream << "StackArgumentRanges:\n";
+    for (auto [Start, End] : StackArgumentRanges) {
+      Stream << "  " << Start << " -> " << End << "\n";
+    }
+
+    if (StackReturnValueRange.has_value()) {
+      Stream << "StackReturnValueRange: " << StackReturnValueRange->Start
+             << ", " << StackReturnValueRange->End;
+    } else {
+      Stream << "StackReturnValueRange: no";
+    }
+    Stream << "\n";
+
+    Stream << "Redirector:\n";
+    Redirector.dump(Stream);
+    Stream << "\n";
+  }
+
+  void dump() const debug_function { dump(dbg); }
+};
+
+CallSite CallSite::make(CallInst *SSACSCall,
+                        const model::TypeDefinition &Prototype,
+                        size_t CallInstructionPushSize) {
+  CallSite Result;
+  Result.Redirector = StackAccessRedirector(SSACSCall);
+  Result.CallInstructionPushSize = CallInstructionPushSize;
+
+  // Get stack size at call site
+  auto MaybeArgument = getSignedConstantArg(SSACSCall, 0);
+  if (MaybeArgument.has_value())
+    Result.MaybeStackOffset = -*MaybeArgument;
+
+  // Obtain the prototype layout
+  using namespace abi::FunctionType;
+  Result.Layout = Layout::make(Prototype);
+
+  // Find old call instruction
+  Result.OldCall = findAssociatedCall(SSACSCall);
+  revng_assert(Result.OldCall != nullptr);
+
+  if (not Result.MaybeStackOffset.has_value()) {
+    revng_log(Log, "Stack size unknown, ignoring stack arguments");
+  } else {
+
+    auto &Layout = Result.Layout;
+
+    // Clobber stack arguments
+    for (const auto &Argument : Layout.Arguments) {
+      if (auto MaybeStackRange = Result.stackArgumentRange(Argument)) {
+        Result.StackArgumentRanges.push_back(MaybeStackRange.value());
+      }
+    }
+  }
+
+  return Result;
+}
+
+using CallSiteMap = std::map<CallInst *, CallSite>;
+
+/// Given an instruction, returns what parts of the stack clobbers/writes
+///
+/// For store, we check the pointer operand and store size.
+/// For calls, we clobber all the stack arguments and mark as written the stack
+/// portion pointed to by the SPTAR, if present.
+class InstructionStackUsage {
+public:
+  struct StackUsage {
+    OffsetRanges Clobbers;
+    OffsetRanges Writes;
+  };
+
+private:
+  CallSiteMap &CallSites;
+  CallInst *const &InitLocalSPCall;
+  const uint64_t &StackFrameSize;
+  StackOffsetCache Offsets;
+
+public:
+  InstructionStackUsage(CallSiteMap &CallSites,
+                        CallInst *const &InitLocalSPCall,
+                        const uint64_t &StackFrameSize) :
+    CallSites(CallSites),
+    InitLocalSPCall(InitLocalSPCall),
+    StackFrameSize(StackFrameSize) {}
+
+public:
+  /// Returns the (memoized) stack offset of `I`, or `nullopt` if it's not a
+  /// stack access. All callers in this pass should query offsets through this
+  /// instead of `getStackOffset` directly, so each instruction is analyzed at
+  /// most once per function. Non-const because it populates the internal
+  /// cache; getReads/getWrites that call it are therefore non-const too.
+  std::optional<int64_t> stackOffsetOf(Instruction *I) {
+    return Offsets.get(I);
+  }
+
+  void detectStackReturnValueRange(Instruction *I,
+                                   const MemoryAreaState &State) {
+    auto *Call = dyn_cast<CallInst>(I);
+    if (Call == nullptr)
+      return;
+
+    auto It = CallSites.find(Call);
+    if (It == CallSites.end())
+      return;
+
+    It->second.processSPTAR(InitLocalSPCall, StackFrameSize, State, *this);
+  }
+
+  StackUsage getWrites(Instruction *I) {
+    StackUsage Result;
+
+    if (auto *Call = dyn_cast<CallInst>(I)) {
+      auto It = CallSites.find(Call);
+      if (It == CallSites.end())
+        return Result;
+
+      auto &CallSite = It->second;
+
+      for (auto [Start, End] : CallSite.StackArgumentRanges)
+        Result.Clobbers.push_back({ Start, End });
+
+      if (CallSite.StackReturnValueRange.has_value()) {
+        Result.Writes = { CallSite.StackReturnValueRange.value() };
+      }
+
+    } else if (auto *Store = dyn_cast<StoreInst>(I)) {
+      // Get stack offset, if available
+      auto MaybeStartStackOffset = stackOffsetOf(I);
+      if (not MaybeStartStackOffset)
+        return Result;
+
+      int64_t StartStackOffset = *MaybeStartStackOffset;
+      unsigned AccessSize = getMemoryAccessSize(I);
+      int64_t EndStackOffset = StartStackOffset + AccessSize;
+
+      Result.Writes = { { StartStackOffset, EndStackOffset } };
+    }
+
+    return Result;
+  }
+
+  OffsetRanges getReads(Instruction *I) {
+    OffsetRanges Result;
+
+    if (auto *Call = dyn_cast<CallInst>(I)) {
+      auto It = CallSites.find(Call);
+      if (It == CallSites.end())
+        return Result;
+
+      for (auto [Start, End] : It->second.StackArgumentRanges)
+        Result.push_back({ Start, End });
+
+    } else if (auto *Store = dyn_cast<LoadInst>(I)) {
+      // Get stack offset, if available
+      auto MaybeStartStackOffset = stackOffsetOf(I);
+      if (not MaybeStartStackOffset)
+        return Result;
+
+      int64_t StartStackOffset = *MaybeStartStackOffset;
+      unsigned AccessSize = getMemoryAccessSize(I);
+      auto EndStackOffset = OverflowSafeInt<int64_t>(StartStackOffset)
+                            + AccessSize;
+
+      if (EndStackOffset) {
+        return { { StartStackOffset, *EndStackOffset } };
+      } else {
+        revng_log(Log, "Overflow in StartStackOffset + AccessSize, ignoring");
+        return {};
+      }
+    }
+
+    return Result;
+  }
+};
+
+[[nodiscard]] static SmallVector<Instruction *>
+findAllWriters(const MemoryAreaState &State,
+               InstructionStackUsage &StackUsage,
+               const OffsetRanges &Ranges) {
+  SmallVector<Instruction *> Result;
+  DenseMap<Instruction *, unsigned> StoreBytesSeen;
+
+  // `State` is a `std::set<StoredByte>` ordered by `(StackOffset, Writer)`,
+  // so iteration yields bytes in ascending offset order. Sort `Ranges` by
+  // `Start` and walk both sequences together: for each byte, advance past
+  // ranges that already ended; the current range then covers the byte iff
+  // its `Start <= Offset`. This turns the previous O(|State| * |Ranges|)
+  // double loop into O(|State| + |Ranges| log |Ranges|).
+  SmallVector<OffsetRange> SortedRanges(Ranges.begin(), Ranges.end());
+  llvm::sort(SortedRanges, [](const OffsetRange &A, const OffsetRange &B) {
+    return std::tie(A.Start, A.End) < std::tie(B.Start, B.End);
+  });
+
+  size_t RangeIndex = 0;
+  for (const StoredByte &Byte : State) {
+    int64_t Offset = Byte.StackOffset;
+
+    while (RangeIndex < SortedRanges.size()
+           and SortedRanges[RangeIndex].End <= Offset) {
+      ++RangeIndex;
+    }
+
+    if (RangeIndex == SortedRanges.size())
+      break;
+
+    if (SortedRanges[RangeIndex].Start > Offset)
+      continue;
+
+    auto It = StoreBytesSeen.find(Byte.Writer);
+    if (It == StoreBytesSeen.end()) {
+      Result.push_back(Byte.Writer);
+      StoreBytesSeen[Byte.Writer] = 1;
+    } else {
+      ++It->second;
+    }
+  }
+
+  // Purge entries where the read-write pairs where the read does not fully
+  // contain the read or vice-versa, i.e., skip partial overlaps.
+  auto RangesSize = getRangeSize(Ranges);
+  auto PartiallyOverlaps = [&](Instruction *I) {
+    auto OtherRangeSize = getRangeSize(StackUsage.getWrites(I).Writes);
+    auto SmallerSize = std::min(RangesSize, OtherRangeSize);
+    bool Partial = StoreBytesSeen[I] != SmallerSize;
+    if (Partial) {
+      revng_log(Log,
+                "Dropping "
+                  << getName(I) << " due to partial overlap (RangeSize: "
+                  << RangesSize << ", OtherRangeSize: " << OtherRangeSize
+                  << ", Overlapping: " << StoreBytesSeen[I] << ")");
+    }
+    return Partial;
+  };
+  llvm::erase_if(Result, PartiallyOverlaps);
+
+  return Result;
+}
+
+void CallSite::processSPTAR(CallInst *InitLocalSPCall,
+                            uint64_t StackFrameSize,
+                            const MemoryAreaState &State,
+                            InstructionStackUsage &StackUsage) {
+
+  if (not Layout.hasSPTAR())
+    return;
+
+  revng_log(Log, "Processing SPTAR");
+  LoggerIndent Indent(Log);
+
+  if (StackFrameSize == 0) {
+    revng_log(Log, "The stack frame has size 0, bailing out");
+    return;
+  }
+
+  // We expect the first argument to be (revng_undefined_local_sp + constant)
+
+  if (InitLocalSPCall == nullptr) {
+    revng_log(Log, "Couldn't find call to revng_undefined_local_sp");
+    return;
+  }
+
+  revng_assert(Layout.Arguments.size() > 0);
+  auto &SPTARArgument = Layout.Arguments[0];
+  Value *SPTAR = nullptr;
+  if (SPTARArgument.Stack.has_value()) {
+    revng_log(Log, "SPTAR is on the stack");
+
+    // The SPTAR is on the stack, we need to try to fetch the only write for
+    // that stack slot writing a constant offset from the initial value of the
+    // stack pointer.
+    revng_assert(SPTARArgument.Registers.size() == 0);
+    if (auto MaybeRange = stackArgumentRange(SPTARArgument)) {
+      auto Writers = findAllWriters(State, StackUsage, { *MaybeRange });
+
+      // Hopefully there's a single reaching store targeting this slot
+      if (Writers.size() == 1 and isa<StoreInst>(Writers[0])) {
+        SPTAR = cast<StoreInst>(Writers[0])->getValueOperand();
+      } else {
+        revng_log(Log,
+                  "We were looking for a single store writing the SPTAR "
+                  "argument, but failed");
+      }
+    } else {
+      revng_log(Log,
+                "Can't obtain the offset range of the SPTAR stack argument");
+    }
+  } else {
+    revng_log(Log, "SPTAR is in a register");
+    revng_assert(SPTARArgument.Registers.size() > 0);
+    revng_assert(OldCall->arg_size() > 0);
+    SPTAR = OldCall->getArgOperand(0);
+  }
+
+  using namespace PatternMatch;
+  llvm::ConstantInt *Offset = nullptr;
+  if (SPTAR == nullptr
+      or not match(SPTAR,
+                   m_Add(m_Specific(InitLocalSPCall), m_ConstantInt(Offset)))) {
+    revng_log(Log,
+              "Couldn't identify offset in the stack of the stack-allocated "
+              "return value passed via SPTAR");
+    return;
+  }
+
+  revng_assert(Offset != nullptr);
+
+  OverflowSafeInt<int64_t> EndOffset(Offset->getSExtValue());
+  auto ReturnValueSize = Layout.returnValueAggregateType().size();
+  revng_assert(ReturnValueSize.has_value());
+
+  EndOffset += ReturnValueSize.value();
+  if (EndOffset) {
+    // Record the call itself as the writer of the SPTAR range
+    StackReturnValueRange = { Offset->getSExtValue(), *EndOffset };
+  } else {
+    revng_log(Log,
+              "Overflow while computing the final offset of "
+              "StackReturnValueRange");
+  }
+}
+
+struct SegregateStackAccessesMFI : public SetUnionLattice<MemoryAreaState> {
+public:
   using Label = llvm::BasicBlock *;
   using GraphType = llvm::Function *;
+  using ExtraStateKey = llvm::Instruction *;
+  using ExtraStateType = mfp::ExtraState<llvm::Instruction *, MemoryAreaState>;
 
-  static LatticeElement applyTransferFunction(llvm::BasicBlock *BB,
-                                              const LatticeElement &Value) {
+private:
+  InstructionStackUsage &StackUsage;
+
+public:
+  SegregateStackAccessesMFI(InstructionStackUsage &StackUsage) :
+    StackUsage(StackUsage) {}
+
+private:
+  void processInstruction(llvm::Instruction &I,
+                          MemoryAreaState &StackBytes) const {
+    revng_log(Log, "Processing " << getName(&I));
+    LoggerIndent Indent(Log);
+
+    StackUsage.detectStackReturnValueRange(&I, StackBytes);
+
+    auto Usage = StackUsage.getWrites(&I);
+
+    for (auto [Start, End] : Usage.Clobbers) {
+      revng_log(Log, "Clobbering from " << Start << " to " << End);
+      StackBytes.eraseRange(Start, End);
+    }
+
+    for (auto [Start, End] : Usage.Writes) {
+      revng_log(Log,
+                "Recording from " << Start << " to " << End << " as written by "
+                                  << getName(&I));
+      StackBytes.record(Start, End, &I);
+    }
+  }
+
+public:
+  MemoryAreaState applyTransferFunction(llvm::BasicBlock *BB,
+                                        const MemoryAreaState &Value,
+                                        ExtraStateType &State) const {
     using namespace llvm;
     revng_log(Log, "Analyzing block " << getName(BB));
     LoggerIndent Indent(Log);
 
-    LatticeElement StackBytes = Value;
+    MemoryAreaState StackBytes = Value;
 
+    // Expose the lattice value at the boundaries of every instruction so
+    // the caller can observe the value at specific program points (e.g.
+    // the stack_size_at_call_site marker placed right before an isolated
+    // call).
     for (Instruction &I : *BB) {
-      if (isCallToIsolatedFunction(&I)) {
-        StackBytes.clear();
-        continue;
-      }
-
-      // If it's not a load/store, pointer is nullptr
-      if (not isa<LoadInst>(&I) and not isa<StoreInst>(&I))
-        continue;
-
-      revng_log(Log, "Analyzing instruction " << getName(&I));
-      LoggerIndent Indent(Log);
-
-      // Get stack offset, if available
-      auto MaybeStartStackOffset = getStackOffset(&I);
-      if (not MaybeStartStackOffset)
-        continue;
-
-      int64_t StartStackOffset = *MaybeStartStackOffset;
-      unsigned AccessSize = getMemoryAccessSize(&I);
-      int64_t EndStackOffset = StartStackOffset + AccessSize;
-
-      // Erase all the existing entries
-      // TODO: use lower_bound instead of scanning everything
-      StackBytes.erase(StackBytes.lower_bound(StoredByte{ StartStackOffset }),
-                       StackBytes.upper_bound(StoredByte{ EndStackOffset }));
-
-      // If it's a store, record all of its bytes
-      if (auto *Store = dyn_cast<StoreInst>(&I))
-        for (unsigned I = 0; I < AccessSize; ++I)
-          StackBytes.insert({ StartStackOffset + I, Store, I });
+      State.registerBefore(&I, StackBytes);
+      processInstruction(I, StackBytes);
+      State.registerAfter(&I, StackBytes);
     }
 
     return StackBytes;
   }
 };
 
+static_assert(mfp::MonotoneFrameworkInstance<SegregateStackAccessesMFI>);
+
+namespace mfp {
+
+template<>
+void dump<MemoryAreaState>(Logger &Stream,
+                           unsigned Indent,
+                           const MemoryAreaState &Element) {
+  Element.dump(Stream, Indent);
+}
+
+template<>
+void dumpLabel<BasicBlock *>(Logger &Stream, BasicBlock *const &Label) {
+  Stream << getName(Label);
+}
+
+template<>
+void dumpLabel<Instruction *>(Logger &Stream, Instruction *const &Label) {
+  Stream << getName(Label);
+}
+
+} // namespace mfp
+
 struct SortByFunction {
   bool operator()(const Instruction *LHS, const Instruction *RHS) const {
     using std::make_pair;
@@ -254,7 +827,7 @@ struct SortByFunction {
   }
 };
 
-inline CallInst *getAsModelGEP(revng::IRBuilder &B,
+static CallInst *getAsModelGEP(revng::IRBuilder &B,
                                Value *Pointer,
                                const model::Type &ModelType) {
   Module &M = *B.GetInsertBlock()->getModule();
@@ -290,13 +863,9 @@ struct PointersMetadata {
 static PointersMetadata getPointerMetadata(const abi::FunctionType::Layout &L) {
   PointersMetadata Result;
 
-  if (L.hasSPTAR()) {
-    // SPTAR always returns a pointer on LLVM IR.
-    Result.ReturnValues.push_back(true);
-  } else {
-    for (const auto &R : L.ReturnValues)
+  for (const auto &R : L.ReturnValues)
+    if (L.returnMethod() != abi::FunctionType::ReturnMethod::ModelAggregate)
       Result.ReturnValues.push_back(R.Type->isPointer());
-  }
 
   for (const auto &R : L.Arguments)
     Result.Arguments.push_back(R.Type->isPointer());
@@ -304,6 +873,9 @@ static PointersMetadata getPointerMetadata(const abi::FunctionType::Layout &L) {
   return Result;
 }
 
+template<bool Legacy>
+class SegregateFunctionStack;
+
 /// Rewrite all stack memory accesses
 ///
 /// This pass changes the base address of stack memory access to either:
@@ -320,19 +892,17 @@ static PointersMetadata getPointerMetadata(const abi::FunctionType::Layout &L) {
 /// `revng_undefined_local_sp` is dropped entirely.
 ///
 /// This pass has two modes of operation:
-/// - when LegacyLocalVariables is true it uses old FunctionTags and dedicated
+/// - when Legacy is true it uses old FunctionTags and dedicated
 /// functions to represent local variables, and accesses to them;
-/// - when LegacyLocalVariables is false it represents local variables as
+/// - when Legacy is false it represents local variables as
 ///   regular LLVM allocas, while accesses are modeled as regular load/store
 ///   instructions
 //
 // TODO: At some point the legacy mode will be discontinued and we can remove
 // the template parameter.
-template<bool LegacyLocalVariables>
+template<bool Legacy>
 class SegregateStackAccesses : public pipeline::FunctionPassImpl {
-private:
-  using MFIResult = std::map<BasicBlock *,
-                             MFP::MFPResult<std::set<StoredByte>>>;
+  friend class SegregateFunctionStack<Legacy>;
 
 private:
   const model::Binary &Binary;
@@ -343,13 +913,11 @@ private:
   model::VerifyHelper VH;
   const size_t CallInstructionPushSize = 0;
   std::map<Function *, Function *> OldToNew;
-  std::set<Function *> FunctionsWithStackArguments;
-  std::map<Function *, StackAccessRedirector> StackArgumentsRedirectors;
-  std::vector<Instruction *> ToPushALAP;
+  SmallVector<Instruction *> ToPushALAP;
 
   llvm::Type *TargetPointerSizedInteger = nullptr;
   llvm::Type *OpaquePointerType = nullptr;
-  LocalVariableBuilder<LegacyLocalVariables> VariableBuilder;
+  LocalVariableBuilder<Legacy> VariableBuilder;
   OpaqueFunctionsPool<FunctionTags::TypePair> *AddressOfPool = nullptr;
 
 public:
@@ -365,7 +933,7 @@ public:
     TargetPointerSizedInteger(getPointerSizedInteger(M.getContext(),
                                                      Binary.Architecture())),
     OpaquePointerType(PointerType::get(M.getContext(), 0)),
-    VariableBuilder(makeVariableBuilder<LegacyLocalVariables>(Binary, M)),
+    VariableBuilder(makeVariableBuilder<Legacy>(Binary, M)),
     AddressOfPool(VariableBuilder.getAddressOfPool()) {}
 
   SegregateStackAccesses(const model::Binary &Binary, llvm::Module &M) :
@@ -378,7 +946,7 @@ public:
     TargetPointerSizedInteger(getPointerSizedInteger(M.getContext(),
                                                      Binary.Architecture())),
     OpaquePointerType(PointerType::get(M.getContext(), 0)),
-    VariableBuilder(makeVariableBuilder<LegacyLocalVariables>(Binary, M)),
+    VariableBuilder(makeVariableBuilder<Legacy>(Binary, M)),
     AddressOfPool(VariableBuilder.getAddressOfPool()) {}
 
 public:
@@ -391,13 +959,7 @@ public:
   }
 
   bool runOnFunction(const model::Function &ModelFunction,
-                     llvm::Function &Function) final {
-
-    llvm::Function &NewFunction = upgradeLocalFunction(&Function);
-    segregateStackAccesses(NewFunction);
-
-    return true;
-  }
+                     llvm::Function &Function) final;
 
   bool epilogue() final {
     pushALAP();
@@ -414,27 +976,6 @@ public:
   }
 
 private:
-  Value *pointer(revng::IRBuilder &B, Value *V) const {
-    return B.CreateIntToPtr(V, OpaquePointerType);
-  }
-
-  CallInst *createAddressOf(revng::IRBuilder &B,
-                            Value *V,
-                            const model::UpcastableType &AllocatedType) {
-    revng_assert(LegacyLocalVariables);
-
-    auto *ArgType = V->getType();
-    // Inject a call to AddressOf
-    Constant *ModelTypeString = toLLVMString(AllocatedType, M);
-    auto *AddressOfFunctionType = getAddressOfType(TargetPointerSizedInteger,
-                                                   ArgType);
-    auto *AddressOfFunction = AddressOfPool->get({ TargetPointerSizedInteger,
-                                                   ArgType },
-                                                 AddressOfFunctionType,
-                                                 "AddressOf");
-    return B.CreateCall(AddressOfFunction, { ModelTypeString, V });
-  }
-
   void upgradeDynamicFunctions() {
     SmallVector<Function *, 8> Functions;
     for (Function &F : FunctionTags::DynamicFunction.functions(&M))
@@ -476,416 +1017,6 @@ private:
     }
   }
 
-  /// Upgrade function to reflect their model prototype
-  Function &upgradeLocalFunction(Function *OldFunction) {
-    using namespace abi::FunctionType;
-
-    auto &&[NewFunction, Layout] = getOrCreateNewLocalFunction(OldFunction);
-
-    // Let the new function steal the body from the old function
-    moveBlocksInto(*OldFunction, *NewFunction);
-
-    FunctionTags::StackAccessesSegregated.addTo(NewFunction);
-
-    Type *NewReturnType = NewFunction->getReturnType();
-
-    //
-    // Map llvm::Argument * to model::Register
-    //
-    std::map<model::Register::Values, llvm::Argument *> ArgumentToRegister;
-    auto ArgumentRegisters = Layout.argumentRegisters();
-    for (const auto &[Register, OldArgument] :
-         zip(ArgumentRegisters, OldFunction->args()))
-      ArgumentToRegister[Register] = &OldArgument;
-
-    //
-    // Update references to old arguments
-    //
-
-    // Create StackAccessRedirector, if required
-    StackAccessRedirector *Redirector = nullptr;
-    auto IsStackArgument = [](const auto &Argument) -> bool {
-      return Argument.Stack.has_value();
-    };
-    if (llvm::any_of(Layout.Arguments, IsStackArgument)) {
-      auto It = StackArgumentsRedirectors.emplace(NewFunction, 0).first;
-      Redirector = &It->second;
-    }
-
-    auto ModelArguments = llvm::make_range(Layout.Arguments.begin(),
-                                           Layout.Arguments.end());
-
-    // Perform sanity checks on the return value and extract the type of the
-    // result variable, if we're returning through a variable
-    auto ReturnMethod = Layout.returnMethod();
-    switch (ReturnMethod) {
-    case ReturnMethod::Void:
-      revng_assert(NewReturnType->isVoidTy());
-      break;
-
-    case ReturnMethod::ModelAggregate:
-      if constexpr (LegacyLocalVariables) {
-        // Nothing to check here.
-      } else {
-        if (Layout.hasSPTAR()) {
-          // Nothing to check here
-        } else {
-          revng_assert(NewReturnType->isArrayTy());
-          auto *ArrayTy = cast<llvm::ArrayType>(NewReturnType);
-          auto *ElemTy = ArrayTy->getElementType();
-          revng_assert(cast<llvm::IntegerType>(ElemTy)->getBitWidth() == 8);
-          unsigned NumElems = ArrayTy->getNumElements();
-          size_t ModelAggregateSize = *Layout.returnValueAggregateType().size();
-          revng_assert(ModelAggregateSize == NumElems);
-        }
-      }
-      break;
-
-    case ReturnMethod::RegisterSet:
-      // Assert each return instruction is using a StructInitializer
-      for (BasicBlock &BB : *NewFunction) {
-        if (auto *Ret = dyn_cast<ReturnInst>(BB.getTerminator())) {
-          auto *Call = cast<CallInst>(Ret->getReturnValue());
-          auto *Callee = getCalledFunction(Call);
-          revng_assert(Call != nullptr);
-          revng_assert(FunctionTags::StructInitializer.isTagOf(Callee));
-        }
-      }
-      break;
-    case ReturnMethod::Scalar:
-      break;
-    }
-
-    Value *ReturnValueAllocation = nullptr;
-    Value *ReturnValueIntAddress = nullptr;
-    if (ReturnMethod == ReturnMethod::ModelAggregate) {
-      const model::Type &A = Layout.returnValueAggregateType();
-      VariableBuilder.setTargetFunction(NewFunction);
-      tie(ReturnValueAllocation,
-          ReturnValueIntAddress) = VariableBuilder
-                                     .createLocalVariableAndTakeIntAddress(A);
-      revng_assert(ReturnValueAllocation);
-      revng_assert(ReturnValueIntAddress);
-
-      if (Layout.hasSPTAR()) {
-        // Identify the SPTAR
-        auto &ModelArgument = Layout.Arguments[0];
-        // Handle the argument pointing to the return value
-        if (ModelArgument.Stack) {
-          revng_assert(ModelArgument.Registers.size() == 0);
-          Redirector->recordSpan(*ModelArgument.Stack + CallInstructionPushSize,
-                                 ReturnValueIntAddress);
-        } else {
-          // It's in a register
-          revng_assert(ModelArgument.Registers.size() == 1);
-          Argument *OldArgument = nullptr;
-          OldArgument = ArgumentToRegister.at(ModelArgument.Registers[0]);
-          OldArgument->replaceAllUsesWith(ReturnValueIntAddress);
-        }
-
-        // Exclude the SPTAR from the list to process
-        ModelArguments = llvm::drop_begin(ModelArguments);
-      }
-    }
-
-    // TODO: the checks should be enabled conditionally based on the user.
-    revng::NonDebugInfoCheckingIRBuilder B(NewFunction->getContext());
-    setInsertPointToFirstNonAlloca(B, *NewFunction);
-
-    // Handle arguments
-    for (auto &&[ModelArgument, NewArgument] :
-         zip(ModelArguments, NewFunction->args())) {
-
-      // Extract from the new argument the old arguments
-      unsigned OffsetInNewArgument = 0;
-      Type *NewArgumentType = NewArgument.getType();
-      unsigned NewArgumentSize = NewArgumentType->getIntegerBitWidth() / 8;
-
-      llvm::Value *ToRecordSpan = nullptr;
-      bool UsesStack = ModelArgument.Stack.has_value();
-
-      using namespace abi::FunctionType::ArgumentKind;
-      if (ModelArgument.Kind == PointerToCopy) {
-        auto Architecture = Binary.Architecture();
-        auto PointerSize = model::Architecture::getPointerSize(Architecture);
-        revng_assert(ModelArgument.Type->size() > PointerSize);
-        Value *AddressOfNewArgument = &NewArgument;
-        if constexpr (LegacyLocalVariables)
-          AddressOfNewArgument = createAddressOf(B,
-                                                 &NewArgument,
-                                                 ModelArgument.Type);
-
-        if (UsesStack) {
-          // When loading from this stack slot, return the address of the
-          // address of the new argument
-          revng_assert(ModelArgument.Registers.size() == 0);
-          ToRecordSpan = AddressOfNewArgument;
-        } else {
-          // Replace the old argument with an address of the new argument
-          revng_assert(ModelArgument.Registers.size() == 1);
-          auto Register = ModelArgument.Registers[0];
-          Argument *OldArgument = ArgumentToRegister.at(Register);
-          OldArgument->replaceAllUsesWith(AddressOfNewArgument);
-        }
-
-      } else if (ModelArgument.Kind == Scalar) {
-        revng_assert(ModelArgument.Type->isScalar());
-        // Handle scalar argument
-        for (model::Register::Values Register : ModelArgument.Registers) {
-          Argument *OldArgument = ArgumentToRegister.at(Register);
-          Type *OldArgumentType = OldArgument->getType();
-          auto OldArgumentSize = OldArgumentType->getIntegerBitWidth() / 8;
-          revng_assert(model::Register::getSize(Register) == OldArgumentSize);
-
-          // Compute the shift amount
-          unsigned ShiftAmount = shiftAmount(OffsetInNewArgument,
-                                             NewArgumentSize,
-                                             OldArgumentSize);
-
-          // Shift and trunc
-          Value *Shifted = &NewArgument;
-          if (ShiftAmount != 0)
-            Shifted = B.CreateLShr(&NewArgument, ShiftAmount);
-          Value *Trunced = B.CreateZExtOrTrunc(Shifted, OldArgumentType);
-
-          // Replace old argument with the extracted valued
-          OldArgument->replaceAllUsesWith(Trunced);
-
-          // Consume size
-          OffsetInNewArgument += OldArgumentSize;
-        }
-
-        if (ModelArgument.Stack) {
-          Type *ArgumentType = NewArgument.getType();
-          auto Pair = VariableBuilder.createAllocaWithPtrToInt(NewFunction,
-                                                               ArgumentType);
-          auto [Alloca, PtrToInt] = Pair;
-          B.CreateStore(&NewArgument, Alloca);
-          ToRecordSpan = PtrToInt;
-        }
-
-      } else if (ModelArgument.Kind == ReferenceToAggregate) {
-
-        // Handle non-scalar argument (passed by pointer)
-        Value *AddressOfNewArgument = &NewArgument;
-        if constexpr (LegacyLocalVariables)
-          AddressOfNewArgument = createAddressOf(B,
-                                                 &NewArgument,
-                                                 ModelArgument.Type);
-
-        for (model::Register::Values Register : ModelArgument.Registers) {
-          Argument *OldArgument = ArgumentToRegister.at(Register);
-
-          // Load value
-          Value *ArgumentPointer = computeAddress(B,
-                                                  AddressOfNewArgument,
-                                                  OffsetInNewArgument);
-          Value *ArgumentValue = B.CreateLoad(OldArgument->getType(),
-                                              ArgumentPointer);
-
-          // Replace
-          OldArgument->replaceAllUsesWith(ArgumentValue);
-
-          // Consume size
-          OffsetInNewArgument += model::Register::getSize(Register);
-        }
-
-        if (ModelArgument.Stack)
-          ToRecordSpan = AddressOfNewArgument;
-      }
-
-      if (ToRecordSpan) {
-        Redirector->recordSpan(*ModelArgument.Stack + CallInstructionPushSize,
-                               ToRecordSpan);
-      }
-    }
-
-    SmallVector<ReturnInst *, 4> Returns;
-    for (BasicBlock &BB : *NewFunction)
-      if (auto *Ret = dyn_cast<ReturnInst>(BB.getTerminator()))
-        Returns.push_back(Ret);
-
-    for (BasicBlock &BB : *NewFunction)
-      revng_assert(BB.getTerminator() != nullptr);
-
-    // Handle return values
-    switch (ReturnMethod) {
-    case ReturnMethod::ModelAggregate: {
-      // Replace return instructions with returning a copy of the local variable
-      // representing the return value
-      for (ReturnInst *Ret : Returns) {
-        B.SetInsertPoint(Ret);
-
-        if (not Layout.hasSPTAR()) {
-          // We have an aggregate returned through registers, fill in the
-          // struct using stores
-          revng_assert(Layout.returnValueRegisterCount() > 0);
-
-          // Collect returned values
-          SmallVector<llvm::Value *, 4> ReturnValues;
-          Value *RetValue = Ret->getReturnValue();
-          if (Layout.returnValueRegisterCount() == 1) {
-            ReturnValues.push_back(RetValue);
-          } else {
-            auto *Call = cast<CallInst>(Ret->getReturnValue());
-            auto *Callee = getCalledFunction(Call);
-            revng_assert(Call != nullptr);
-            revng_assert(FunctionTags::StructInitializer.isTagOf(Callee));
-            llvm::copy(Call->args(), std::back_inserter(ReturnValues));
-          }
-
-          // Populate the local variable we're returning with the returned
-          // values
-          uint64_t Offset = 0;
-          for (Value *ReturnValue : ReturnValues) {
-            Value *Pointer = createAdd(B, ReturnValueIntAddress, Offset);
-            B.CreateStore(ReturnValue, pointer(B, Pointer));
-            Offset += ReturnValue->getType()->getIntegerBitWidth() / 8;
-          }
-        }
-
-        // Return the pointer to the result variable
-        revng_assert(ReturnValueAllocation);
-        revng_assert(ReturnValueIntAddress);
-        Value *ToReturn = nullptr;
-        if constexpr (LegacyLocalVariables) {
-          ToReturn = ReturnValueAllocation;
-        } else {
-          if (Layout.hasSPTAR()) {
-            ToReturn = ReturnValueIntAddress;
-          } else {
-            ToReturn = B.CreateLoad(NewReturnType, ReturnValueAllocation);
-          }
-        }
-        B.CreateRet(ToReturn);
-        Ret->eraseFromParent();
-      }
-    } break;
-
-    case ReturnMethod::Scalar: {
-      Type *OldReturnType = OldFunction->getReturnType();
-
-      if (OldReturnType != NewReturnType) {
-        if (OldReturnType->isIntegerTy() and NewReturnType->isIntegerTy()) {
-          // Handle return values smaller than the original function
-          for (ReturnInst *Ret : Returns) {
-            B.SetInsertPoint(Ret);
-            B.CreateRet(B.CreateTrunc(Ret->getReturnValue(), NewReturnType));
-            Ret->eraseFromParent();
-          }
-        } else if (OldReturnType->isStructTy()
-                   and NewReturnType->isIntegerTy()) {
-          // Turn struct_initializer into a an integer
-          for (ReturnInst *Ret : Returns) {
-            auto *Call = cast<CallInst>(Ret->getReturnValue());
-            auto *Callee = getCalledFunction(Call);
-            revng_assert(Call != nullptr);
-            revng_assert(FunctionTags::StructInitializer.isTagOf(Callee));
-
-            B.SetInsertPoint(Ret);
-            Value *Accumulator = ConstantInt::get(NewReturnType, 0);
-            uint64_t ShiftAmount = 0;
-            for (Value *Argument : Call->args()) {
-              auto *Extended = B.CreateZExtOrTrunc(Argument, NewReturnType);
-              Accumulator = B.CreateOr(Accumulator,
-                                       B.CreateShl(Extended, ShiftAmount));
-              ShiftAmount += Argument->getType()->getIntegerBitWidth();
-            }
-            B.CreateRet(Accumulator);
-            Ret->eraseFromParent();
-            Call->eraseFromParent();
-          }
-        }
-      }
-    } break;
-
-    case ReturnMethod::Void:
-    case ReturnMethod::RegisterSet:
-      // Nothing to do here
-      break;
-
-    default:
-      revng_abort();
-    }
-
-    for (BasicBlock &BB : *NewFunction)
-      revng_assert(BB.getTerminator() != nullptr);
-
-    return *NewFunction;
-  }
-
-  void segregateStackAccesses(Function &F) {
-    // Get model::Function
-    MetaAddress Entry = getMetaAddressMetadata(&F, "revng.function.entry");
-    const model::Function &ModelFunction = Binary.Functions().at(Entry);
-
-    revng_log(Log,
-              "Segregating "
-                << model::CNameBuilder(Binary).name(ModelFunction));
-
-    LoggerIndent Indent(Log);
-
-    // Lookup the redirector, if any
-    auto It = StackArgumentsRedirectors.find(&F);
-    StackAccessRedirector *Redirector = nullptr;
-    if (It != StackArgumentsRedirectors.end())
-      Redirector = &It->second;
-
-    //
-    // Analyze stack usage
-    //
-
-    // Analysis preparation: split basic blocks at call sites.
-    // This enables us to use the *final* value of the monotone framework
-    // associated to the basic block of stack_size_at_call_site.
-    {
-      std::set<Instruction *> SplitPoints;
-      for (BasicBlock &BB : F)
-        for (Instruction &I : BB)
-          if (isCallToIsolatedFunction(&I))
-            SplitPoints.insert(&I);
-      for (Instruction *I : SplitPoints)
-        I->getParent()->splitBasicBlock(I);
-    }
-
-    // Run the analysis
-    MFIResult AnalysisResult;
-    {
-      revng_log(Log, "Running SegregateStackAccessesMFI");
-      LoggerIndent Indent(Log);
-      using SSAMFI = SegregateStackAccessesMFI;
-      BasicBlock *Entry = &F.getEntryBlock();
-      AnalysisResult = MFP::getMaximalFixedPoint<SSAMFI>({},
-                                                         &F,
-                                                         {},
-                                                         {},
-                                                         { Entry });
-    }
-
-    //
-    // Handle a call to an isolated function
-    //
-    if (SSACS != nullptr)
-      for (BasicBlock &BB : F)
-        for (Instruction &I : BB)
-          if (CallInst *SSACSCall = getCallTo(&I, SSACS))
-            handleCallSite(AnalysisResult, SSACSCall);
-
-    //
-    // Handle memory access, possibly targeting formal stack arguments
-    //
-    if (Redirector != nullptr)
-      for (BasicBlock &BB : F)
-        for (Instruction &I : BB)
-          if (isa<LoadInst>(&I) or isa<StoreInst>(&I))
-            handleMemoryAccess(*Redirector, &I);
-
-    //
-    // Fix stack frame
-    //
-    adjustStackFrame(ModelFunction, F);
-  }
-
   void pushALAP() {
     // Push ALAP all stack arguments allocations
     Function *LastFunction = nullptr;
@@ -903,580 +1034,20 @@ private:
     }
   }
 
-  void handleCallSite(MFIResult &AnalysisResult, CallInst *SSACSCall) {
-    LoggerIndent Indent(Log);
-
-    //
-    // Find call to revng_undefined_local_sp
-    //
-    Function *Caller = SSACSCall->getParent()->getParent();
-
-    // Get stack size at call site
-    auto MaybeStackSize = getSignedConstantArg(SSACSCall, 0);
-
-    // Obtain the prototype
-    const auto &Prototype = *getCallSitePrototype(Binary, SSACSCall);
-    using namespace abi::FunctionType;
-    abi::FunctionType::Layout Layout = Layout::make(Prototype);
-
-    // Find old call instruction
-    CallInst *OldCall = findAssociatedCall(SSACSCall);
-    revng_assert(OldCall != nullptr);
-
-    revng::IRBuilder B(OldCall);
-
-    //
-    // Map llvm::Argument * to model::Register
-    //
-    std::map<model::Register::Values, llvm::Value *> ArgumentToRegister;
-    auto ArgumentRegisters = Layout.argumentRegisters();
-    for (auto &&[Register, OldArg] : zip(ArgumentRegisters, OldCall->args()))
-      ArgumentToRegister[Register] = OldArg.get();
-
-    // Check if it's a direct call
-    auto *Callee = dyn_cast<Function>(OldCall->getCalledOperand());
-    bool IsDirect = (Callee != nullptr);
-
-    // Obtain or compute the function type for the call
-    FunctionType *CalleeType = nullptr;
-    Value *CalledValue = nullptr;
-    if (IsDirect) {
-      Function *NewCallee = getOrCreateNewFunction(Callee);
-      CalledValue = NewCallee;
-      CalleeType = NewCallee->getFunctionType();
-    } else {
-      LLVMContext &Context = OldCall->getContext();
-      auto Architecture = Binary.Architecture();
-      CalleeType = &layoutToLLVMFunctionType<LegacyLocalVariables>(Context,
-                                                                   Architecture,
-                                                                   Layout);
-      CalledValue = B.CreateBitCast(OldCall->getCalledOperand(),
-                                    CalleeType->getPointerTo());
-    }
-
-    SmallVector<llvm::Value *, 4> Arguments;
-
-    StackAccessRedirector Redirector(-MaybeStackSize.value_or(0)
-                                     + CallInstructionPushSize);
-
-    SmallVector<llvm::Type *, 8> LLVMArgumentTypes;
-    bool HasSPTAR = Layout.hasSPTAR();
-
-    auto ReturnMethod = Layout.returnMethod();
-    if (ReturnMethod == ReturnMethod::ModelAggregate and HasSPTAR) {
-      // Inject the SPTAR in LLVMArgumentTypes
-      revng_assert(Layout.Arguments.size() > 0);
-      uint64_t SPTARSize = *Layout.Arguments[0].Type->size();
-      LLVMArgumentTypes.push_back(B.getIntNTy(SPTARSize * 8));
-    }
-
-    copy(CalleeType->params(), std::back_inserter(LLVMArgumentTypes));
-
-    bool MessageEmitted = false;
-    for (auto &&[LLVMType, ModelArgument] :
-         llvm::zip(LLVMArgumentTypes, Layout.Arguments)) {
-      uint64_t NewSize = *ModelArgument.Type->size();
-
-      switch (ModelArgument.Kind) {
-
-      case ArgumentKind::PointerToCopy: {
-        Value *Pointer = nullptr;
-
-        if (ModelArgument.Stack) {
-          model::Architecture::Values Architecture = Binary.Architecture();
-          auto PointerSize = model::Architecture::getPointerSize(Architecture);
-          revng_assert(ModelArgument.Type->size() > PointerSize);
-          revng_assert(ModelArgument.Registers.size() == 0);
-          revng_assert(ModelArgument.Stack->Size == PointerSize);
-          revng_assert(MaybeStackSize);
-
-          // Create an alloca
-          auto *StackSpanType = B.getIntNTy(ModelArgument.Stack->Size * 8);
-          auto Pair = VariableBuilder.createAllocaWithPtrToInt(Caller,
-                                                               StackSpanType);
-          auto [Alloca, PtrToInt] = Pair;
-
-          // Record its portion of the stack for redirection
-          Redirector.recordSpan(*ModelArgument.Stack, PtrToInt);
-
-          // Load the alloca and record it as a pointer
-          Pointer = B.CreateLoad(Alloca->getAllocatedType(), Alloca);
-        } else {
-          revng_assert(ModelArgument.Registers.size() == 1);
-          auto Register = ModelArgument.Registers[0];
-          Pointer = ArgumentToRegister.at(Register);
-        }
-
-        // Pass as argument the pointer compute above.
-        // In legacy mode, wrap it into a ModelGEP at offset 0.
-        if constexpr (LegacyLocalVariables) {
-          Pointer = getAsModelGEP(B, Pointer, *ModelArgument.Type);
-        }
-        Arguments.push_back(Pointer);
-      } break;
-
-      case ArgumentKind::Scalar:
-      case ArgumentKind::ShadowPointerToAggregateReturnValue: {
-        revng_assert(ModelArgument.Type->isScalar());
-        Value *Accumulator = ConstantInt::get(LLVMType, 0);
-        unsigned OffsetInNewArgument = 0;
-        for (auto &Register : ModelArgument.Registers) {
-          Value *OldArgument = ArgumentToRegister.at(Register);
-          unsigned OldSize = model::Register::getSize(Register);
-
-          Value *Extended = B.CreateZExtOrTrunc(OldArgument, LLVMType);
-
-          unsigned ShiftAmount = shiftAmount(OffsetInNewArgument,
-                                             NewSize,
-                                             OldSize);
-          Value *Shifted = Extended;
-          if (ShiftAmount != 0)
-            Shifted = B.CreateLShr(Extended, ShiftAmount);
-
-          Accumulator = B.CreateOr(Accumulator, Shifted);
-
-          // Consume size
-          OffsetInNewArgument += OldSize;
-        }
-
-        if (ModelArgument.Stack and not MaybeStackSize) {
-          if (not MessageEmitted) {
-            MessageEmitted = true;
-            emitMessage(OldCall,
-                        "Ignoring stack arguments for this call site: "
-                        "stack size at call site unknown",
-                        OldCall->getDebugLoc());
-          }
-        } else if (ModelArgument.Stack) {
-          unsigned OldSize = ModelArgument.Stack->Size;
-          revng_assert(OldSize <= 128 / 8);
-          revng_assert(MaybeStackSize);
-
-          // Create an alloca
-          IntegerType *StackSpanType = B.getIntNTy(OldSize * 8);
-          auto Pair = VariableBuilder.createAllocaWithPtrToInt(Caller,
-                                                               StackSpanType);
-          auto [Alloca, PtrToInt] = Pair;
-
-          // Record its portion of the stack for redirection
-          Redirector.recordSpan(*ModelArgument.Stack, PtrToInt);
-
-          Value *Loaded = B.CreateLoad(Alloca->getAllocatedType(), Alloca);
-
-          // Extend, shift and or in Accumulator
-          // Note: here we might truncate too, since certain architectures
-          //       report a stack span of 8 bytes but the associated type is
-          //       actually 32 bits
-          Value *Extended = B.CreateZExtOrTrunc(Loaded, LLVMType);
-
-          unsigned ShiftAmount = shiftAmount(OffsetInNewArgument,
-                                             NewSize,
-                                             OldSize);
-          Value *Shifted = Extended;
-          if (ShiftAmount != 0)
-            Shifted = B.CreateShl(Extended, ShiftAmount);
-
-          Accumulator = B.CreateOr(Accumulator, Shifted);
-        }
-
-        Arguments.push_back(Accumulator);
-      } break;
-
-      case ArgumentKind::ReferenceToAggregate: {
-
-        VariableBuilder.setTargetFunction(SSACSCall->getFunction());
-        Instruction
-          *StackArgsAddress = VariableBuilder
-                                .createCallStackArgumentVariable(*ModelArgument
-                                                                    .Type);
-        revng_assert(StackArgsAddress);
-        Instruction *StackArgsAllocation = nullptr;
-        if constexpr (LegacyLocalVariables) {
-          // When in legacy mode, the actual instruction performing the stack
-          // allocation is the first operand of StackArgsAddress, which is
-          // guaranteed to be a call to AddressOf.
-          auto *CallToAddressOf = getCallToTagged(StackArgsAddress,
-                                                  FunctionTags::AddressOf);
-          auto *AllocationInst = CallToAddressOf->getArgOperand(1);
-          StackArgsAllocation = cast<Instruction>(AllocationInst);
-          // Then we have to push the address computation and the allocation
-          // ALAP. The address should be pushed ALAP first to leave slack for
-          // the allocation instruction to also be pushed ALAP afterwards.
-          ToPushALAP.push_back(StackArgsAddress);
-          ToPushALAP.push_back(StackArgsAllocation);
-        } else {
-          // When not in legacy mode, the instruction returning the address of
-          // the stack arguments is also the instruction performing the actual
-          // allocation, so we can just say they're equal.
-          //
-          // Also, there's no need to push it ALAP, since it's an alloca.
-          // We do have to push ALAP its cast to an integer though.
-          revng_assert(isa<PtrToIntInst>(StackArgsAddress));
-          revng_assert(isa<AllocaInst>(StackArgsAddress->getOperand(0)));
-          StackArgsAllocation = StackArgsAddress;
-          ToPushALAP.push_back(StackArgsAddress);
-        }
-
-        // We also have to copy over metadata, from the annotation about the
-        // size of the stack arguments.
-        StackArgsAllocation->copyMetadata(*SSACSCall);
-
-        unsigned OffsetInNewArgument = 0;
-        for (auto &Register : ModelArgument.Registers) {
-          Value *OldArgument = ArgumentToRegister.at(Register);
-          unsigned OldSize = model::Register::getSize(Register);
-
-          Value *Address = createAdd(B, StackArgsAddress, OffsetInNewArgument);
-
-          // Store value
-          Value *Pointer = pointer(B, Address);
-          B.CreateStore(OldArgument, Pointer);
-
-          // Consume size
-          OffsetInNewArgument += OldSize;
-        }
-
-        if (ModelArgument.Stack)
-          Redirector.recordSpan(*ModelArgument.Stack, StackArgsAddress);
-
-        Arguments.push_back(StackArgsAllocation);
-      } break;
-
-      default:
-        revng_abort();
-      }
-    }
-
-    if (Log.isEnabled()) {
-      Log << "Redirector data:\n";
-      LoggerIndent X(Log);
-      Redirector.dump(Log);
-      Log << DoLog;
-    }
-
-    revng_assert(Redirector.verify());
-
-    Value *ReturnValuePointer = nullptr;
-    // Handle SPTAR by dropping the actual argument and saving it for later
-    if (HasSPTAR) {
-      revng_assert(Arguments.size() > 0);
-
-      // The return value is pointed by the SPTAR
-      ReturnValuePointer = Arguments[0];
-
-      Arguments.erase(Arguments.begin());
-    }
-
-    // If the old return type and the new one are identical, switch to the old
-    // one in the new call
-    auto *OldCallType = OldCall->getFunctionType();
-    auto *OldReturnType = OldCallType->getReturnType();
-    auto *NewReturnType = CalleeType->getReturnType();
-    if (auto *OldStructType = dyn_cast<StructType>(OldReturnType)) {
-      if (auto *NewStructType = dyn_cast<StructType>(NewReturnType)) {
-        if (NewStructType->isLayoutIdentical(OldStructType)) {
-          CalleeType = FunctionType::get(OldReturnType,
-                                         CalleeType->params(),
-                                         CalleeType->isVarArg());
-        }
-      }
-    }
-
-    // Actually create the new call and replace the old one
-    CallInst *NewCall = B.CreateCall(CalleeType, CalledValue, Arguments);
-    NewCall->copyMetadata(*OldCall);
-    NewCall->setAttributes(OldCall->getAttributes());
-    const auto &[PointerReturns, PointerArguments] = getPointerMetadata(Layout);
-    setPointersMetadata(NewCall, PointerReturns, PointerArguments);
-
-    switch (Layout.returnMethod()) {
-    case ReturnMethod::ModelAggregate: {
-      if (HasSPTAR) {
-        // In legacy mode, make a reference out of ReturnValuePointer, using a
-        // ModelGEP at offset 0.
-        if constexpr (LegacyLocalVariables) {
-          getAsModelGEP(B,
-                        ReturnValuePointer,
-                        Layout.returnValueAggregateType());
-        }
-      } else {
-        revng_assert(not ReturnValuePointer);
-        const auto &ReturnType = Layout.returnValueAggregateType();
-        if constexpr (LegacyLocalVariables) {
-          ReturnValuePointer = createAddressOf(B, NewCall, ReturnType);
-        } else {
-          auto &VB = VariableBuilder;
-          VB.setTargetFunction(Caller);
-          Value *Allocation = nullptr;
-          Value *IntAddress = nullptr;
-          tie(Allocation,
-              IntAddress) = VB.createLocalVariableAndTakeIntAddress(ReturnType);
-          B.CreateStore(NewCall, Allocation);
-          ReturnValuePointer = IntAddress;
-        }
-      }
-
-      if (HasSPTAR) {
-        revng_assert(not OldReturnType->isStructTy());
-        OldCall->replaceAllUsesWith(ReturnValuePointer);
-      } else {
-        // We're returning an aggregate, but not via SPTAR, we're using one or
-        // more registers
-        if (OldReturnType->isStructTy()) {
-          SmallVector<SmallPtrSet<CallInst *, 2>, 2>
-            ExtractedValues = getExtractedValuesFromInstruction(OldCall);
-          for (auto &Group : llvm::enumerate(ExtractedValues)) {
-
-            unsigned FieldIndex = Group.index();
-            SmallPtrSet<CallInst *, 2> &ExtractedAtIndex = Group.value();
-            if (ExtractedAtIndex.empty())
-              continue;
-
-            unsigned BitOffset = getBitOffsetAt(cast<StructType>(OldReturnType),
-                                                FieldIndex);
-            revng_assert(0 == (BitOffset % 8));
-            unsigned ByteOffset = BitOffset / 8;
-
-            Value *Pointer = createAdd(B, ReturnValuePointer, ByteOffset);
-            Type *ExtractedType = (*ExtractedAtIndex.begin())->getType();
-            auto *Load = B.CreateLoad(ExtractedType, pointer(B, Pointer));
-
-            for (CallInst *Extractor : Group.value()) {
-              Extractor->replaceAllUsesWith(Load);
-              eraseFromParent(Extractor);
-            }
-          }
-        } else {
-          auto *Load = B.CreateLoad(ReturnValuePointer->getType(),
-                                    pointer(B, ReturnValuePointer));
-          OldCall->replaceAllUsesWith(Load);
-        }
-      }
-
-    } break;
-
-    case ReturnMethod::Scalar:
-
-      if (OldReturnType != NewReturnType and OldReturnType->isIntegerTy()
-          and NewReturnType->isIntegerTy()) {
-        // We're using a large register to return a smaller integer value (e.g.,
-        // returning a 32-bit integer through rax, which is 64-bit)
-        auto OldSize = OldReturnType->getIntegerBitWidth();
-        auto NewSize = NewReturnType->getIntegerBitWidth();
-        revng_assert(NewSize <= OldSize);
-        auto *Extended = cast<Instruction>(B.CreateZExt(NewCall,
-                                                        OldReturnType));
-        OldCall->replaceAllUsesWith(Extended);
-      } else if (OldReturnType->isStructTy() and NewReturnType->isIntegerTy()) {
-        // We're returning a large integer value through multiple values (e.g.,
-        // returning a 64-bit integer through two registers in i386)
-        SmallVector<SmallPtrSet<CallInst *, 2>, 2>
-          ExtractedValues = getExtractedValuesFromInstruction(OldCall);
-        for (auto &Group : llvm::enumerate(ExtractedValues)) {
-
-          unsigned FieldIndex = Group.index();
-          SmallPtrSet<CallInst *, 2> &ExtractedAtIndex = Group.value();
-          if (ExtractedAtIndex.empty())
-            continue;
-
-          unsigned ShiftAmount = getBitOffsetAt(cast<StructType>(OldReturnType),
-                                                FieldIndex);
-          Type *TruncatedType = (*ExtractedAtIndex.begin())->getType();
-          Value *Replacement = B.CreateTrunc(B.CreateLShr(NewCall, ShiftAmount),
-                                             TruncatedType);
-          for (CallInst *Extractor : Group.value()) {
-            revng_assert(TruncatedType == Extractor->getType());
-            Extractor->replaceAllUsesWith(Replacement);
-            eraseFromParent(Extractor);
-          }
-        }
-      } else {
-        revng_assert(not OldReturnType->isStructTy());
-        OldCall->replaceAllUsesWith(NewCall);
-      }
-      break;
-
-    case ReturnMethod::Void:
-      // Nothing to do here
-      break;
-    case ReturnMethod::RegisterSet:
-      OldCall->replaceAllUsesWith(NewCall);
-      break;
-
-    default:
-      revng_abort();
-    }
-
-    eraseFromParent(OldCall);
-    revng_assert(CalleeType->getPointerTo() == CalledValue->getType());
-
-    if (not MaybeStackSize)
-      return;
-
-    int64_t StackSizeAtCallSite = *MaybeStackSize;
-
-    // Identify all the StoredBytes targeting this call sites' stack
-    // arguments
-    struct StoreInfo {
-      unsigned Count = 0;
-      int64_t Offset = 0;
-    };
-    std::map<StoreInst *, StoreInfo> Stores;
-    BasicBlock *BB = SSACSCall->getParent();
-
-    // We use the *final* value. In fact, we split the basic block before the
-    // call to the isolated function as appropriate.
-    const std::set<StoredByte> &BlockFinalResult = AnalysisResult.at(BB)
-                                                     .OutValue;
-    for (const StoredByte &Byte : BlockFinalResult) {
-      StoreInfo &Info = Stores[Byte.Store];
-      Info.Count += 1;
-      Info.Offset = Byte.StackOffset - Byte.StoreOffset;
-    }
-
-    // Process MarkedStores
-    for (const auto &[Store, Info] : Stores) {
-      auto Size = getMemoryAccessSize(Store);
-      int64_t StackArgumentsOffset = (Info.Offset + StackSizeAtCallSite
-                                      - CallInstructionPushSize);
-
-      revng_log(Log, "Considering " << getName(Store));
-      LoggerIndent Indent(Log);
-      revng_log(Log, "Size: " << Size);
-      revng_log(Log, "Info.Count: " << Info.Count);
-      revng_log(Log, "Info.Offset: " << Info.Count);
-      revng_log(Log, "StackSizeAtCallSite: " << StackSizeAtCallSite);
-      revng_log(Log, "StackArgumentsOffset: " << StackArgumentsOffset);
-
-      if (Size != Info.Count) {
-        revng_log(Log,
-                  "Warning: " << getName(Store) << " has size " << Size
-                              << " but only " << Info.Count << " bytes target "
-                              << getName(SSACSCall)
-                              << " stack arguments. Ignoring.");
-        continue;
-      }
-
-      // OK, this call site owns this store entirely
-
-      // Check if we're writing to the return address
-      int64_t NegativePushSize = -CallInstructionPushSize;
-      bool TargetsReturnAddress = (StackArgumentsOffset == NegativePushSize
-                                   and Size == CallInstructionPushSize);
-
-      if (TargetsReturnAddress) {
-        // This store targets the saved return address slot, drop it
-        revng_log(Log,
-                  "This store is saving the return address: we'll drop it");
-        ToPurge.insert(Store);
-      } else if (auto NewBase = Redirector.computeNewBase(Info.Offset, Size)) {
-        // This ends up in a stack argument
-        replace(Store, NewBase->second, NewBase->first);
-      }
-    }
-  }
-
-  void handleMemoryAccess(const StackAccessRedirector &Redirector,
-                          Instruction *I) {
-    revng_log(Log, "Handling memory access " << getName(I));
-    LoggerIndent Indent(Log);
-
-    auto MaybeStackOffset = getStackOffset(I);
-    if (not MaybeStackOffset)
-      return;
-    int64_t StackOffset = *MaybeStackOffset;
-    revng_log(Log, "StackOffset: " << StackOffset);
-
-    unsigned AccessSize = getMemoryAccessSize(I);
-    auto NewBase = Redirector.computeNewBase(StackOffset, AccessSize);
-    if (NewBase)
-      replace(I, NewBase->second, NewBase->first);
-  }
-
-  void adjustStackFrame(const model::Function &ModelFunction, Function &F) {
-    //
-    // Find call to revng_undefined_local_sp
-    //
-    if (InitLocalSP == nullptr)
-      return;
-
-    CallInst *InitLocalSPCall = findCallTo(&F, InitLocalSP);
-
-    if (InitLocalSPCall == nullptr
-        or ModelFunction.StackFrame().Type().isEmpty())
-      return;
-
-    //
-    // Get stack frame size
-    //
-    uint64_t StackFrameSize = 0;
-    if (const model::TypeDefinition *T = ModelFunction.stackFrameType())
-      StackFrameSize = *rc_eval(T->size(VH));
-
-    //
-    // Create call and rebase SP0, if StackFrameSize is not zero
-    //
-    if (StackFrameSize != 0) {
-
-      model::UpcastableType FrameType = ModelFunction.StackFrame().Type();
-      VariableBuilder.setTargetFunction(&F);
-      Instruction *StackFrameAddress = VariableBuilder
-                                         .createStackFrameVariable(FrameType);
-
-      revng::IRBuilder Builder(InitLocalSPCall);
-      auto *SP0 = Builder.CreateAdd(StackFrameAddress,
-                                    getSPConstant(StackFrameSize));
-      InitLocalSPCall->replaceAllUsesWith(SP0);
-
-      // Cleanup revng_undefined_local_sp
-      eraseFromParent(InitLocalSPCall);
-    }
-  }
-
-private:
-  /// \name Support functions
-  /// \{
-
-  Constant *getSPConstant(uint64_t Value) const {
-    return ConstantInt::get(TargetPointerSizedInteger, Value);
-  }
-
-  Value *
-  computeAddress(revng::IRBuilder &B, Value *Base, int64_t Offset) const {
-    return pointer(B, createAdd(B, Base, Offset));
-  }
-
-  void replace(Instruction *I, Value *Base, int64_t Offset) {
-    ToPurge.insert(I);
-
-    revng::IRBuilder B(I);
-    auto *NewAddress = computeAddress(B, Base, Offset);
-
-    Instruction *NewInstruction = nullptr;
-    if (auto *Store = dyn_cast<StoreInst>(I)) {
-      NewInstruction = B.CreateStore(Store->getValueOperand(), NewAddress);
-    } else if (auto *Load = dyn_cast<LoadInst>(I)) {
-      NewInstruction = B.CreateLoad(I->getType(), NewAddress);
-    }
-
-    I->replaceAllUsesWith(NewInstruction);
-    NewInstruction->copyMetadata(*I);
-  }
-
 private:
   std::pair<llvm::Function *, abi::FunctionType::Layout>
   recreateApplyingModelPrototype(Function *OldFunction,
                                  const model::TypeDefinition &Prototype) {
     using namespace abi::FunctionType;
     auto Layout = Layout::make(Prototype);
+
     LLVMContext &Context = OldFunction->getContext();
     auto Architecture = Binary.Architecture();
 
     Type *OldReturnType = OldFunction->getReturnType();
-    FunctionType
-      &NewType = layoutToLLVMFunctionType<LegacyLocalVariables>(Context,
-                                                                Architecture,
-                                                                Layout);
+    FunctionType &NewType = layoutToLLVMFunctionType<Legacy>(Context,
+                                                             Architecture,
+                                                             Layout);
 
     // NOTE: all the model *must* be read above this line!
     //       If we don't do this, we will break invalidation tracking
@@ -1495,21 +1066,1155 @@ private:
 
     return { &NewFunction, Layout };
   }
+};
+
+/// Per-function state and logic for SegregateStackAccesses. One instance is
+/// constructed per call to runOnFunction. `upgrade()` rewrites the function
+/// signature and lowers arguments/return values; `segregate()` then runs the
+/// data-flow analysis and redirects every stack access to its proper base.
+template<bool Legacy>
+class SegregateFunctionStack {
+private:
+  SegregateStackAccesses<Legacy> &SSA;
+  const model::Function &ModelFunction;
+  llvm::Function &OldFunction;
+
+  // Populated by upgrade()
+  llvm::Function *NewFunction = nullptr;
+  abi::FunctionType::Layout Layout;
+  std::map<model::Register::Values, llvm::Argument *> ArgumentToRegister;
+  StackAccessRedirector StackArgumentRedirector;
+  bool HasStackArgumentRedirector = false;
+  llvm::Value *ReturnValueAllocation = nullptr;
+  llvm::Value *ReturnValueIntAddress = nullptr;
+
+  // Populated by segregate()
+  llvm::CallInst *InitLocalSPCall = nullptr;
+  uint64_t StackFrameSize = 0;
+  CallSiteMap CallSites;
+  SegregateStackAccessesMFI::ExtraStateType MFPExtraState;
+  InstructionStackUsage StackUsage;
+  FunctionStackAccessRedirectors Redirectors;
+
+public:
+  SegregateFunctionStack(SegregateStackAccesses<Legacy> &P,
+                         const model::Function &ModelFunction,
+                         llvm::Function &OldFunction) :
+    SSA(P),
+    ModelFunction(ModelFunction),
+    OldFunction(OldFunction),
+    StackUsage(CallSites, InitLocalSPCall, StackFrameSize) {}
+
+public:
+  void upgrade();
+  void segregate();
+
+private:
+  void setupNewFunction();
+  void checkReturnMethod();
+  void prepareReturnValueStorage();
+  void lowerArguments(revng::IRBuilder &B);
+  void lowerReturnValues(revng::IRBuilder &B);
+
+  /// Record a stack argument's storage in the function-level redirector.
+  ///
+  /// Layout sketch:
+  ///
+  ///   0x0000
+  ///                 -16
+  ///     _________   -8
+  ///    |_________|  +0  Saved return address
+  ///    |_________|  +8  struct StackArguments { uint64_t Offset0;
+  ///    |_________|  +16   uint64_t Offset8; };
+  ///    |_________|  +24
+  ///   _|_________|_
+  ///
+  ///   0xffff
+  void recordFunctionStackArgument(const StackSpan &Span, llvm::Value *V) {
+    StackArgumentRedirector.recordSpan(SSA.CallInstructionPushSize + Span, V);
+  }
+
+  void initialize();
+  void collectCallSites();
+  void runDataFlowAnalysis();
+  void lowerCallSites();
+  void redirectMemoryAccesses();
+  void adjustStackFrame();
+  StackAccessRedirector handleCallSite(llvm::CallInst *SSACSCall,
+                                       const CallSite &CallSite);
+
+  void handleMemoryAccess(const StackAccessRedirector &Redirector,
+                          llvm::Instruction *I,
+                          std::optional<int64_t> MaybeStackOffset) {
+    if (not MaybeStackOffset)
+      return;
+    int64_t StackOffset = *MaybeStackOffset;
+    revng_log(Log, "StackOffset: " << StackOffset);
+
+    unsigned AccessSize = getMemoryAccessSize(I);
+    auto NewBase = Redirector.computeNewBase(StackOffset, AccessSize);
+    if (NewBase)
+      replace(I, NewBase->second, NewBase->first);
+  }
+
+  llvm::Value *pointer(revng::IRBuilder &B, llvm::Value *V) const {
+    return B.CreateIntToPtr(V, SSA.OpaquePointerType);
+  }
+
+  llvm::Value *
+  computeAddress(revng::IRBuilder &B, llvm::Value *Base, int64_t Offset) const {
+    return pointer(B, createAdd(B, Base, Offset));
+  }
+
+  void replace(llvm::Instruction *I, llvm::Value *Base, int64_t Offset) {
+    SSA.ToPurge.insert(I);
+
+    revng::IRBuilder B(I);
+    auto *NewAddress = computeAddress(B, Base, Offset);
+
+    llvm::Instruction *NewInstruction = nullptr;
+    if (auto *Store = dyn_cast<llvm::StoreInst>(I)) {
+      NewInstruction = B.CreateStore(Store->getValueOperand(), NewAddress);
+    } else if (auto *Load = dyn_cast<llvm::LoadInst>(I)) {
+      NewInstruction = B.CreateLoad(I->getType(), NewAddress);
+    }
+
+    I->replaceAllUsesWith(NewInstruction);
+    NewInstruction->copyMetadata(*I);
+  }
+
+  llvm::CallInst *createAddressOf(revng::IRBuilder &B,
+                                  llvm::Value *V,
+                                  const model::UpcastableType &AllocatedType) {
+    revng_assert(Legacy);
+
+    auto *ArgType = V->getType();
+    llvm::Constant *ModelTypeString = toLLVMString(AllocatedType, SSA.M);
+    auto *AddressOfFunctionType = getAddressOfType(SSA
+                                                     .TargetPointerSizedInteger,
+                                                   ArgType);
+    auto *AddressOfFunction = SSA.AddressOfPool
+                                ->get({ SSA.TargetPointerSizedInteger,
+                                        ArgType },
+                                      AddressOfFunctionType,
+                                      "AddressOf");
+    return B.CreateCall(AddressOfFunction, { ModelTypeString, V });
+  }
+
+  llvm::Constant *getSPConstant(uint64_t Value) const {
+    return llvm::ConstantInt::get(SSA.TargetPointerSizedInteger, Value);
+  }
 
   unsigned
   shiftAmount(unsigned Offset, unsigned NewSize, unsigned OldSize) const {
     if (NewSize >= OldSize)
       return 0;
-    if (model::Architecture::isLittleEndian(Binary.Architecture())) {
+    if (model::Architecture::isLittleEndian(SSA.Binary.Architecture())) {
       return Offset * 8;
     } else {
       return (NewSize - Offset - OldSize) * 8;
     }
   }
-
-  /// \}
 };
 
+template<bool Legacy>
+void SegregateFunctionStack<Legacy>::upgrade() {
+  revng_log(Log, "Upgrading " << getName(&OldFunction));
+  LoggerIndent Indent(Log);
+
+  setupNewFunction();
+
+  checkReturnMethod();
+
+  prepareReturnValueStorage();
+
+  // TODO: the checks should be enabled conditionally based on the user.
+  revng::NonDebugInfoCheckingIRBuilder B(NewFunction->getContext());
+  setInsertPointToFirstNonAlloca(B, *NewFunction);
+
+  lowerArguments(B);
+
+  lowerReturnValues(B);
+
+  for (BasicBlock &BB : *NewFunction) {
+    revng_assert(BB.getTerminator() != nullptr);
+  }
+}
+
+template<bool Legacy>
+void SegregateFunctionStack<Legacy>::segregate() {
+  revng_log(Log,
+            "Segregating "
+              << model::CNameBuilder(SSA.Binary).name(ModelFunction));
+  LoggerIndent Indent(Log);
+
+  initialize();
+
+  collectCallSites();
+
+  runDataFlowAnalysis();
+
+  lowerCallSites();
+
+  redirectMemoryAccesses();
+
+  adjustStackFrame();
+}
+
+template<bool Legacy>
+void SegregateFunctionStack<Legacy>::setupNewFunction() {
+  auto &&[NewFn, NewLayout] = SSA.getOrCreateNewLocalFunction(&OldFunction);
+  NewFunction = NewFn;
+  Layout = std::move(NewLayout);
+
+  // Let the new function steal the body from the old function
+  moveBlocksInto(OldFunction, *NewFunction);
+
+  FunctionTags::StackAccessesSegregated.addTo(NewFunction);
+
+  // Map llvm::Argument * to model::Register
+  auto ArgumentRegisters = Layout.argumentRegisters();
+  for (const auto &[Register, OldArgument] :
+       zip(ArgumentRegisters, OldFunction.args())) {
+    ArgumentToRegister[Register] = &OldArgument;
+  }
+
+  // Decide whether we need a redirector for the function's stack arguments
+  auto IsStackArgument = [](const auto &Argument) -> bool {
+    return Argument.Stack.has_value();
+  };
+  if (llvm::any_of(Layout.Arguments, IsStackArgument)) {
+    revng_log(Log, "Creating redirector for stack arguments");
+    HasStackArgumentRedirector = true;
+  }
+}
+
+template<bool Legacy>
+void SegregateFunctionStack<Legacy>::checkReturnMethod() {
+  using namespace abi::FunctionType;
+
+  Type *NewReturnType = NewFunction->getReturnType();
+  switch (Layout.returnMethod()) {
+  case ReturnMethod::Void:
+    revng_assert(NewReturnType->isVoidTy());
+    break;
+
+  case ReturnMethod::ModelAggregate:
+    if constexpr (Legacy) {
+      // Nothing to check here.
+    } else {
+      if (Layout.hasSPTAR()) {
+        // Nothing to check here
+      } else {
+        revng_assert(NewReturnType->isArrayTy());
+        auto *ArrayTy = cast<llvm::ArrayType>(NewReturnType);
+        auto *ElemTy = ArrayTy->getElementType();
+        revng_assert(cast<llvm::IntegerType>(ElemTy)->getBitWidth() == 8);
+        unsigned NumElems = ArrayTy->getNumElements();
+        size_t ModelAggregateSize = *Layout.returnValueAggregateType().size();
+        revng_assert(ModelAggregateSize == NumElems);
+      }
+    }
+    break;
+
+  case ReturnMethod::RegisterSet:
+    // Assert each return instruction is using a StructInitializer
+    for (BasicBlock &BB : *NewFunction) {
+      if (auto *Ret = dyn_cast<ReturnInst>(BB.getTerminator())) {
+        auto *Call = cast<CallInst>(Ret->getReturnValue());
+        auto *Callee = getCalledFunction(Call);
+        revng_assert(Call != nullptr);
+        revng_assert(FunctionTags::StructInitializer.isTagOf(Callee));
+      }
+    }
+    break;
+
+  case ReturnMethod::Scalar:
+    break;
+  }
+}
+
+template<bool Legacy>
+void SegregateFunctionStack<Legacy>::prepareReturnValueStorage() {
+  using namespace abi::FunctionType;
+
+  if (Layout.returnMethod() != ReturnMethod::ModelAggregate)
+    return;
+
+  const model::Type &A = Layout.returnValueAggregateType();
+  SSA.VariableBuilder.setTargetFunction(NewFunction);
+  tie(ReturnValueAllocation,
+      ReturnValueIntAddress) = SSA.VariableBuilder
+                                 .createLocalVariableAndTakeIntAddress(A);
+  revng_assert(ReturnValueAllocation);
+  revng_assert(ReturnValueIntAddress);
+
+  if (not Layout.hasSPTAR())
+    return;
+
+  // Identify the SPTAR and redirect the argument pointing at the storage of
+  // the return value to our freshly created local variable.
+  auto &ModelArgument = Layout.Arguments[0];
+  if (ModelArgument.Stack) {
+    revng_assert(ModelArgument.Registers.size() == 0);
+    recordFunctionStackArgument(*ModelArgument.Stack, ReturnValueIntAddress);
+  } else {
+    revng_assert(ModelArgument.Registers.size() == 1);
+    Argument *OldArgument = ArgumentToRegister.at(ModelArgument.Registers[0]);
+    OldArgument->replaceAllUsesWith(ReturnValueIntAddress);
+  }
+}
+
+template<bool Legacy>
+void SegregateFunctionStack<Legacy>::lowerArguments(revng::IRBuilder &B) {
+  using namespace abi::FunctionType;
+  using namespace abi::FunctionType::ArgumentKind;
+
+  // The SPTAR argument was handled in prepareReturnValueStorage; drop it
+  // from the list of arguments we still need to lower.
+  auto ModelArguments = llvm::make_range(Layout.Arguments.begin(),
+                                         Layout.Arguments.end());
+  if (Layout.returnMethod() == ReturnMethod::ModelAggregate
+      and Layout.hasSPTAR()) {
+    ModelArguments = llvm::drop_begin(ModelArguments);
+  }
+
+  for (auto &&[ModelArgument, NewArgument] :
+       zip(ModelArguments, NewFunction->args())) {
+
+    unsigned OffsetInNewArgument = 0;
+    Type *NewArgumentType = NewArgument.getType();
+    unsigned NewArgumentSize = NewArgumentType->getIntegerBitWidth() / 8;
+
+    llvm::Value *ToRecordSpan = nullptr;
+    bool UsesStack = ModelArgument.Stack.has_value();
+
+    if (ModelArgument.Kind == PointerToCopy) {
+      auto Architecture = SSA.Binary.Architecture();
+      auto PointerSize = model::Architecture::getPointerSize(Architecture);
+      revng_assert(ModelArgument.Type->size() > PointerSize);
+      Value *AddressOfNewArgument = &NewArgument;
+      if constexpr (Legacy)
+        AddressOfNewArgument = createAddressOf(B,
+                                               &NewArgument,
+                                               ModelArgument.Type);
+
+      if (UsesStack) {
+        // When loading from this stack slot, return the address of the
+        // address of the new argument
+        revng_assert(ModelArgument.Registers.size() == 0);
+        ToRecordSpan = AddressOfNewArgument;
+      } else {
+        // Replace the old argument with an address of the new argument
+        revng_assert(ModelArgument.Registers.size() == 1);
+        auto Register = ModelArgument.Registers[0];
+        Argument *OldArgument = ArgumentToRegister.at(Register);
+        OldArgument->replaceAllUsesWith(AddressOfNewArgument);
+      }
+
+    } else if (ModelArgument.Kind == Scalar) {
+      revng_assert(ModelArgument.Type->isScalar());
+      for (model::Register::Values Register : ModelArgument.Registers) {
+        Argument *OldArgument = ArgumentToRegister.at(Register);
+        Type *OldArgumentType = OldArgument->getType();
+        auto OldArgumentSize = OldArgumentType->getIntegerBitWidth() / 8;
+        revng_assert(model::Register::getSize(Register) == OldArgumentSize);
+
+        unsigned ShiftAmount = shiftAmount(OffsetInNewArgument,
+                                           NewArgumentSize,
+                                           OldArgumentSize);
+
+        Value *Shifted = &NewArgument;
+        if (ShiftAmount != 0)
+          Shifted = B.CreateLShr(&NewArgument, ShiftAmount);
+        Value *Trunced = B.CreateZExtOrTrunc(Shifted, OldArgumentType);
+
+        OldArgument->replaceAllUsesWith(Trunced);
+
+        OffsetInNewArgument += OldArgumentSize;
+      }
+
+      if (ModelArgument.Stack) {
+        Type *ArgumentType = NewArgument.getType();
+        auto Pair = SSA.VariableBuilder.createAllocaWithPtrToInt(NewFunction,
+                                                                 ArgumentType);
+        auto [Alloca, PtrToInt] = Pair;
+        B.CreateStore(&NewArgument, Alloca);
+        ToRecordSpan = PtrToInt;
+      }
+
+    } else if (ModelArgument.Kind == ReferenceToAggregate) {
+      Value *AddressOfNewArgument = &NewArgument;
+      if constexpr (Legacy)
+        AddressOfNewArgument = createAddressOf(B,
+                                               &NewArgument,
+                                               ModelArgument.Type);
+
+      for (model::Register::Values Register : ModelArgument.Registers) {
+        Argument *OldArgument = ArgumentToRegister.at(Register);
+
+        Value *ArgumentPointer = computeAddress(B,
+                                                AddressOfNewArgument,
+                                                OffsetInNewArgument);
+        Value *ArgumentValue = B.CreateLoad(OldArgument->getType(),
+                                            ArgumentPointer);
+
+        OldArgument->replaceAllUsesWith(ArgumentValue);
+
+        OffsetInNewArgument += model::Register::getSize(Register);
+      }
+
+      if (ModelArgument.Stack)
+        ToRecordSpan = AddressOfNewArgument;
+    }
+
+    if (ToRecordSpan) {
+      recordFunctionStackArgument(*ModelArgument.Stack, ToRecordSpan);
+    }
+  }
+}
+
+template<bool Legacy>
+void SegregateFunctionStack<Legacy>::lowerReturnValues(revng::IRBuilder &B) {
+  using namespace abi::FunctionType;
+
+  Type *NewReturnType = NewFunction->getReturnType();
+
+  llvm::SmallVector<ReturnInst *, 4> Returns;
+  for (BasicBlock &BB : *NewFunction) {
+    if (auto *Ret = dyn_cast<ReturnInst>(BB.getTerminator()))
+      Returns.push_back(Ret);
+  }
+
+  for (BasicBlock &BB : *NewFunction) {
+    revng_assert(BB.getTerminator() != nullptr);
+  }
+
+  switch (Layout.returnMethod()) {
+  case ReturnMethod::ModelAggregate: {
+    // Replace return instructions with returning a copy of the local variable
+    // representing the return value
+    for (ReturnInst *Ret : Returns) {
+      B.SetInsertPoint(Ret);
+
+      if (not Layout.hasSPTAR()) {
+        // We have an aggregate returned through registers, fill in the
+        // struct using stores
+        revng_assert(Layout.returnValueRegisterCount() > 0);
+
+        llvm::SmallVector<llvm::Value *, 4> ReturnValues;
+        Value *RetValue = Ret->getReturnValue();
+        if (Layout.returnValueRegisterCount() == 1) {
+          ReturnValues.push_back(RetValue);
+        } else {
+          auto *Call = cast<CallInst>(Ret->getReturnValue());
+          auto *Callee = getCalledFunction(Call);
+          revng_assert(Call != nullptr);
+          revng_assert(FunctionTags::StructInitializer.isTagOf(Callee));
+          llvm::copy(Call->args(), std::back_inserter(ReturnValues));
+        }
+
+        uint64_t Offset = 0;
+        for (Value *ReturnValue : ReturnValues) {
+          Value *Pointer = createAdd(B, ReturnValueIntAddress, Offset);
+          B.CreateStore(ReturnValue, pointer(B, Pointer));
+          Offset += ReturnValue->getType()->getIntegerBitWidth() / 8;
+        }
+      }
+
+      revng_assert(ReturnValueAllocation);
+      revng_assert(ReturnValueIntAddress);
+      Value *ToReturn = nullptr;
+      if constexpr (Legacy) {
+        ToReturn = ReturnValueAllocation;
+      } else {
+        // TODO: we should review all the CreateLoad alignments
+        ToReturn = B.CreateLoad(NewReturnType, ReturnValueAllocation);
+      }
+      B.CreateRet(ToReturn);
+      Ret->eraseFromParent();
+    }
+  } break;
+
+  case ReturnMethod::Scalar: {
+    Type *OldReturnType = OldFunction.getReturnType();
+
+    if (OldReturnType != NewReturnType) {
+      if (OldReturnType->isIntegerTy() and NewReturnType->isIntegerTy()) {
+        // Handle return values smaller than the original function
+        for (ReturnInst *Ret : Returns) {
+          B.SetInsertPoint(Ret);
+          B.CreateRet(B.CreateTrunc(Ret->getReturnValue(), NewReturnType));
+          Ret->eraseFromParent();
+        }
+      } else if (OldReturnType->isStructTy() and NewReturnType->isIntegerTy()) {
+        // Turn struct_initializer into an integer
+        for (ReturnInst *Ret : Returns) {
+          auto *Call = cast<CallInst>(Ret->getReturnValue());
+          auto *Callee = getCalledFunction(Call);
+          revng_assert(Call != nullptr);
+          revng_assert(FunctionTags::StructInitializer.isTagOf(Callee));
+
+          B.SetInsertPoint(Ret);
+          Value *Accumulator = ConstantInt::get(NewReturnType, 0);
+          uint64_t ShiftAmount = 0;
+          for (Value *Argument : Call->args()) {
+            auto *Extended = B.CreateZExtOrTrunc(Argument, NewReturnType);
+            Accumulator = B.CreateOr(Accumulator,
+                                     B.CreateShl(Extended, ShiftAmount));
+            ShiftAmount += Argument->getType()->getIntegerBitWidth();
+          }
+          B.CreateRet(Accumulator);
+          Ret->eraseFromParent();
+          Call->eraseFromParent();
+        }
+      }
+    }
+  } break;
+
+  case ReturnMethod::Void:
+  case ReturnMethod::RegisterSet:
+    break;
+
+  default:
+    revng_abort();
+  }
+}
+
+template<bool Legacy>
+void SegregateFunctionStack<Legacy>::initialize() {
+  if (SSA.InitLocalSP != nullptr)
+    InitLocalSPCall = findCallTo(NewFunction, SSA.InitLocalSP);
+
+  if (const model::TypeDefinition *T = ModelFunction.stackFrameType())
+    StackFrameSize = *rc_eval(T->size(SSA.VH));
+
+  revng_log(Log, "StackFrameSize: " << StackFrameSize);
+
+  StackAccessRedirector *Default = HasStackArgumentRedirector ?
+                                     &StackArgumentRedirector :
+                                     nullptr;
+  revng_log(Log, "Default redirector: " << (Default ? "yes" : "no"));
+  Redirectors.setFunctionRedirector(Default);
+}
+
+template<bool Legacy>
+void SegregateFunctionStack<Legacy>::collectCallSites() {
+  for (BasicBlock &BB : *NewFunction) {
+    for (Instruction &I : BB) {
+      CallInst *SSACSCall = nullptr;
+      if (SSA.SSACS != nullptr and (SSACSCall = getCallTo(&I, SSA.SSACS))) {
+        revng_log(Log, "Processing " << getName(SSACSCall));
+        LoggerIndent Indent(Log);
+
+        MFPExtraState.registerAsInterestingBefore(SSACSCall);
+
+        const auto &Prototype = *getCallSitePrototype(SSA.Binary, SSACSCall);
+        CallSites[SSACSCall] = CallSite::make(SSACSCall,
+                                              Prototype,
+                                              SSA.CallInstructionPushSize);
+
+        if (Log.isEnabled()) {
+          CallSites[SSACSCall].dump(Log);
+          Log << DoLog;
+        }
+
+      } else if (isa<LoadInst>(&I)
+                 and StackUsage.stackOffsetOf(&I).has_value()) {
+        // Handle load from the stack
+        revng_log(Log, "Registering " << getName(&I) << " as interesting");
+        MFPExtraState.registerAsInterestingBefore(&I);
+      }
+    }
+  }
+}
+
+template<bool Legacy>
+void SegregateFunctionStack<Legacy>::runDataFlowAnalysis() {
+  revng_log(Log, "Running SegregateStackAccessesMFI");
+  LoggerIndent Indent(Log);
+  BasicBlock *Entry = &NewFunction->getEntryBlock();
+  std::vector ExtremalLabels = { Entry };
+  using SSAMFI = SegregateStackAccessesMFI;
+  SSAMFI MFI(StackUsage);
+  mfp::getMaximalFixedPoint<SSAMFI>({ .Instance = &MFI,
+                                      .Flow = NewFunction,
+                                      .ExtremalLabels = &ExtremalLabels,
+                                      .ExtraState = &MFPExtraState,
+                                      .Logger = &Log });
+
+  if (Log.isEnabled()) {
+    Log << "Extra state:\n";
+    MFPExtraState.dump(Log);
+    Log << DoLog;
+  }
+}
+
+template<bool Legacy>
+void SegregateFunctionStack<Legacy>::lowerCallSites() {
+  revng_log(Log, "Handling call sites");
+  LoggerIndent Indent(Log);
+  for (auto &[SSACSCall, CallSite] : CallSites) {
+    revng_log(Log, "Handling " << getName(SSACSCall));
+    LoggerIndent Indent(Log);
+
+    const auto &AnalysisResult = MFPExtraState.getBefore(SSACSCall);
+
+    auto *CallSiteRedirector = Redirectors.record(handleCallSite(SSACSCall,
+                                                                 CallSite));
+    Redirectors.registerOwner(CallSiteRedirector, SSACSCall);
+
+    if (Log.isEnabled()) {
+      Log << "Status of the analysis at call site:\n";
+      AnalysisResult.dump(Log, 1);
+      Log << DoLog;
+    }
+
+    for (Instruction *I : findAllWriters(AnalysisResult,
+                                         StackUsage,
+                                         CallSite.StackArgumentRanges)) {
+      Redirectors.registerOwner(CallSiteRedirector, I);
+    }
+  }
+}
+
+template<bool Legacy>
+void SegregateFunctionStack<Legacy>::redirectMemoryAccesses() {
+  if (Redirectors.empty())
+    return;
+
+  revng_log(Log, "Handling memory accesses");
+  LoggerIndent Indent(Log);
+  for (BasicBlock &BB : *NewFunction) {
+    for (Instruction &I : BB) {
+      if (not(isa<LoadInst>(&I) or isa<StoreInst>(&I)))
+        continue;
+
+      if (isa<LoadInst>(&I))
+        revng_log(Log, "Handling load " << getName(&I));
+      else
+        revng_log(Log, "Handling store " << getName(&I));
+      LoggerIndent Indent(Log);
+
+      auto MaybeStackOffset = StackUsage.stackOffsetOf(&I);
+      if (Log.isEnabled()) {
+        Log << "StackOffset: ";
+        if (MaybeStackOffset.has_value())
+          Log << *MaybeStackOffset;
+        else
+          Log << "(none)";
+        Log << DoLog;
+      }
+
+      // Find the correct redirector
+      const StackAccessRedirector *Redirector = nullptr;
+      if (isa<LoadInst>(&I) and MaybeStackOffset.has_value()) {
+        // For loads, choose the redirector of its writers
+        const auto &AnalysisResult = MFPExtraState.getBefore(&I);
+
+        auto ReadRanges = StackUsage.getReads(&I);
+        auto Writers = findAllWriters(AnalysisResult, StackUsage, ReadRanges);
+
+        if (Log.isEnabled()) {
+          Log << "Found " << Writers.size() << " writers:\n";
+          for (auto *Writer : Writers) {
+            Log << "  " << getName(Writer) << "\n";
+          }
+          Log << DoLog;
+        }
+
+        Redirector = Redirectors.getCommon(Writers);
+      } else {
+        Redirector = Redirectors.get(&I);
+      }
+
+      if (Redirector == nullptr) {
+        revng_log(Log, "No redirector");
+      } else {
+        revng_log(Log,
+                  "Redirecting using " << getName(Redirector->reference()));
+        handleMemoryAccess(*Redirector, &I, MaybeStackOffset);
+      }
+    }
+  }
+}
+
+template<bool Legacy>
+void SegregateFunctionStack<Legacy>::adjustStackFrame() {
+  if (InitLocalSPCall == nullptr or ModelFunction.StackFrame().Type().isEmpty())
+    return;
+
+  // Create call and rebase SP0, if StackFrameSize is not zero
+  if (StackFrameSize == 0)
+    return;
+
+  model::UpcastableType FrameType = ModelFunction.StackFrame().Type();
+  SSA.VariableBuilder.setTargetFunction(NewFunction);
+  Instruction *StackFrameAddress = SSA.VariableBuilder
+                                     .createStackFrameVariable(FrameType);
+
+  revng::IRBuilder Builder(InitLocalSPCall);
+  auto *SP0 = Builder.CreateAdd(StackFrameAddress,
+                                getSPConstant(StackFrameSize));
+  InitLocalSPCall->replaceAllUsesWith(SP0);
+
+  // Cleanup revng_undefined_local_sp
+  eraseFromParent(InitLocalSPCall);
+}
+
+template<bool Legacy>
+StackAccessRedirector
+SegregateFunctionStack<Legacy>::handleCallSite(llvm::CallInst *SSACSCall,
+                                               const CallSite &CallSite) {
+  using namespace abi::FunctionType;
+
+  revng_log(Log, "Analyzing call to SSACS " << getName(SSACSCall));
+  LoggerIndent Indent(Log);
+
+  Function *Caller = SSACSCall->getParent()->getParent();
+
+  // Unpack CallSite
+  const auto
+    &[_1, MaybeStackOffsetAtCallSite, Layout, OldCall, _2, _3, _4] = CallSite;
+
+  revng::IRBuilder B(OldCall);
+
+  // Map llvm::Argument * to model::Register
+  std::map<model::Register::Values, llvm::Value *> ArgumentToRegister;
+  auto ArgumentRegisters = Layout.argumentRegisters();
+  for (auto &&[Register, OldArg] : zip(ArgumentRegisters, OldCall->args()))
+    ArgumentToRegister[Register] = OldArg.get();
+
+  // Check if it's a direct call
+  auto *Callee = dyn_cast<Function>(OldCall->getCalledOperand());
+  bool IsDirect = (Callee != nullptr);
+
+  // Obtain or compute the function type for the call
+  FunctionType *CalleeType = nullptr;
+  Value *CalledValue = nullptr;
+  if (IsDirect) {
+    Function *NewCallee = SSA.getOrCreateNewFunction(Callee);
+    CalledValue = NewCallee;
+    CalleeType = NewCallee->getFunctionType();
+  } else {
+    LLVMContext &Context = OldCall->getContext();
+    auto Architecture = SSA.Binary.Architecture();
+    CalleeType = &layoutToLLVMFunctionType<Legacy>(Context,
+                                                   Architecture,
+                                                   Layout);
+    CalledValue = B.CreateBitCast(OldCall->getCalledOperand(),
+                                  CalleeType->getPointerTo());
+  }
+
+  SmallVector<llvm::Value *, 4> Arguments;
+
+  StackAccessRedirector Redirector;
+  auto RecordStackArgument =
+    [this, &Redirector, &MaybeStackOffsetAtCallSite](const StackSpan &StackSpan,
+                                                     Value *V) {
+      revng_assert(MaybeStackOffsetAtCallSite);
+      // Record its portion of the stack for redirection
+
+      // 0x0000
+      // _____________ -40
+      //  |_________|  -32 Saved return address, MaybeStackSize
+      //  |_________|  -24 struct StackArguments { uint64_t Offset0;
+      //  |_________|  -16  uint64_t Offset8; };
+      // _|_________|_ -8  Local variable
+      //  |_________|  +0  Saved return address
+      // _|_________|_
+      //
+      // 0xffff
+
+      Redirector.recordSpan(*MaybeStackOffsetAtCallSite
+                              + SSA.CallInstructionPushSize + StackSpan,
+                            V);
+    };
+
+  SmallVector<llvm::Type *, 8> LLVMArgumentTypes;
+  bool HasSPTAR = Layout.hasSPTAR();
+
+  auto ReturnMethod = Layout.returnMethod();
+  if (HasSPTAR) {
+    revng_log(Log, "This call site has a SPTAR");
+    revng_assert(ReturnMethod == ReturnMethod::ModelAggregate);
+
+    // The original function produced by enforce-abi had the SPTAR but the
+    // re-created one doesn't, re-inject it temporarily
+    revng_assert(Layout.Arguments.size() > 0);
+    uint64_t SPTARSize = *Layout.Arguments[0].Type->size();
+    LLVMArgumentTypes.push_back(B.getIntNTy(SPTARSize * 8));
+  }
+
+  copy(CalleeType->params(), std::back_inserter(LLVMArgumentTypes));
+
+  bool MessageEmitted = false;
+  for (auto &&[LLVMType, ModelArgument] :
+       llvm::zip(LLVMArgumentTypes, Layout.Arguments)) {
+    uint64_t NewSize = *ModelArgument.Type->size();
+
+    switch (ModelArgument.Kind) {
+
+    case ArgumentKind::PointerToCopy: {
+      Value *Pointer = nullptr;
+
+      if (ModelArgument.Stack) {
+        model::Architecture::Values Architecture = SSA.Binary.Architecture();
+        auto PointerSize = model::Architecture::getPointerSize(Architecture);
+        revng_assert(ModelArgument.Type->size() > PointerSize);
+        revng_assert(ModelArgument.Registers.size() == 0);
+        revng_assert(ModelArgument.Stack->Size == PointerSize);
+        revng_assert(MaybeStackOffsetAtCallSite);
+
+        // Create an alloca
+        auto *StackSpanType = B.getIntNTy(ModelArgument.Stack->Size * 8);
+        auto Pair = SSA.VariableBuilder.createAllocaWithPtrToInt(Caller,
+                                                                 StackSpanType);
+        auto [Alloca, PtrToInt] = Pair;
+
+        RecordStackArgument(*ModelArgument.Stack, PtrToInt);
+
+        // Load the alloca and record it as a pointer
+        Pointer = B.CreateLoad(Alloca->getAllocatedType(), Alloca);
+      } else {
+        revng_assert(ModelArgument.Registers.size() == 1);
+        auto Register = ModelArgument.Registers[0];
+        Pointer = ArgumentToRegister.at(Register);
+      }
+
+      // Pass as argument the pointer computed above.
+      // In legacy mode, wrap it into a ModelGEP at offset 0.
+      if constexpr (Legacy) {
+        Pointer = getAsModelGEP(B, Pointer, *ModelArgument.Type);
+      }
+      Arguments.push_back(Pointer);
+    } break;
+
+    case ArgumentKind::Scalar:
+    case ArgumentKind::ShadowPointerToAggregateReturnValue: {
+      revng_assert(ModelArgument.Type->isScalar());
+      Value *Accumulator = ConstantInt::get(LLVMType, 0);
+      unsigned OffsetInNewArgument = 0;
+      for (auto &Register : ModelArgument.Registers) {
+        Value *OldArgument = ArgumentToRegister.at(Register);
+        unsigned OldSize = model::Register::getSize(Register);
+
+        Value *Extended = B.CreateZExtOrTrunc(OldArgument, LLVMType);
+
+        unsigned ShiftAmount = shiftAmount(OffsetInNewArgument,
+                                           NewSize,
+                                           OldSize);
+        Value *Shifted = Extended;
+        if (ShiftAmount != 0)
+          Shifted = B.CreateLShr(Extended, ShiftAmount);
+
+        Accumulator = B.CreateOr(Accumulator, Shifted);
+
+        OffsetInNewArgument += OldSize;
+      }
+
+      if (ModelArgument.Stack and not MaybeStackOffsetAtCallSite) {
+        if (not MessageEmitted) {
+          MessageEmitted = true;
+          emitMessage(OldCall,
+                      "Ignoring stack arguments for this call site: "
+                      "stack size at call site unknown",
+                      OldCall->getDebugLoc());
+        }
+      } else if (ModelArgument.Stack) {
+        unsigned OldSize = ModelArgument.Stack->Size;
+        revng_assert(OldSize <= 128 / 8);
+        revng_assert(MaybeStackOffsetAtCallSite);
+
+        // Create an alloca
+        IntegerType *StackSpanType = B.getIntNTy(OldSize * 8);
+        auto Pair = SSA.VariableBuilder.createAllocaWithPtrToInt(Caller,
+                                                                 StackSpanType);
+        auto [Alloca, PtrToInt] = Pair;
+
+        // Record its portion of the stack for redirection
+        RecordStackArgument(*ModelArgument.Stack, PtrToInt);
+
+        Value *Loaded = B.CreateLoad(Alloca->getAllocatedType(), Alloca);
+
+        // Extend, shift and or in Accumulator
+        // Note: here we might truncate too, since certain architectures
+        //       report a stack span of 8 bytes but the associated type is
+        //       actually 32 bits
+        Value *Extended = B.CreateZExtOrTrunc(Loaded, LLVMType);
+
+        unsigned ShiftAmount = shiftAmount(OffsetInNewArgument,
+                                           NewSize,
+                                           OldSize);
+        Value *Shifted = Extended;
+        if (ShiftAmount != 0)
+          Shifted = B.CreateShl(Extended, ShiftAmount);
+
+        Accumulator = B.CreateOr(Accumulator, Shifted);
+      }
+
+      Arguments.push_back(Accumulator);
+    } break;
+
+    case ArgumentKind::ReferenceToAggregate: {
+
+      SSA.VariableBuilder.setTargetFunction(SSACSCall->getFunction());
+      Instruction
+        *StackArgsAddress = SSA.VariableBuilder
+                              .createCallStackArgumentVariable(*ModelArgument
+                                                                  .Type);
+      revng_assert(StackArgsAddress);
+      Instruction *StackArgsAllocation = nullptr;
+      if constexpr (Legacy) {
+        // When in legacy mode, the actual instruction performing the stack
+        // allocation is the first operand of StackArgsAddress, which is
+        // guaranteed to be a call to AddressOf.
+        auto *CallToAddressOf = getCallToTagged(StackArgsAddress,
+                                                FunctionTags::AddressOf);
+        auto *AllocationInst = CallToAddressOf->getArgOperand(1);
+        StackArgsAllocation = cast<Instruction>(AllocationInst);
+        // Then we have to push the address computation and the allocation
+        // ALAP. The address should be pushed ALAP first to leave slack for
+        // the allocation instruction to also be pushed ALAP afterwards.
+        SSA.ToPushALAP.push_back(StackArgsAddress);
+        SSA.ToPushALAP.push_back(StackArgsAllocation);
+      } else {
+        // When not in legacy mode, the instruction returning the address of
+        // the stack arguments is also the instruction performing the actual
+        // allocation, so we can just say they're equal.
+        //
+        // Also, there's no need to push it ALAP, since it's an alloca.
+        // We do have to push ALAP its cast to an integer though.
+        revng_assert(isa<PtrToIntInst>(StackArgsAddress));
+        revng_assert(isa<AllocaInst>(StackArgsAddress->getOperand(0)));
+        StackArgsAllocation = StackArgsAddress;
+        SSA.ToPushALAP.push_back(StackArgsAddress);
+      }
+
+      // We also have to copy over metadata, from the annotation about the
+      // size of the stack arguments.
+      StackArgsAllocation->copyMetadata(*SSACSCall);
+
+      unsigned OffsetInNewArgument = 0;
+      for (auto &Register : ModelArgument.Registers) {
+        Value *OldArgument = ArgumentToRegister.at(Register);
+        unsigned OldSize = model::Register::getSize(Register);
+
+        Value *Address = createAdd(B, StackArgsAddress, OffsetInNewArgument);
+
+        // Store value
+        Value *Pointer = pointer(B, Address);
+        B.CreateStore(OldArgument, Pointer);
+
+        OffsetInNewArgument += OldSize;
+      }
+
+      if (ModelArgument.Stack) {
+        if (MaybeStackOffsetAtCallSite) {
+          RecordStackArgument(*ModelArgument.Stack, StackArgsAddress);
+        } else {
+          if (not MessageEmitted) {
+            MessageEmitted = true;
+            emitMessage(OldCall,
+                        "Ignoring stack arguments for this call site: "
+                        "stack size at call site unknown",
+                        OldCall->getDebugLoc());
+          }
+        }
+      }
+
+      Arguments.push_back(StackArgsAllocation);
+    } break;
+
+    default:
+      revng_abort();
+    }
+  }
+
+  if (Log.isEnabled()) {
+    Log << "Redirector data:\n";
+    LoggerIndent X(Log);
+    Redirector.dump(Log);
+    Log << DoLog;
+  }
+
+  revng_assert(Redirector.verify());
+
+  // Remove the SPTAR from the argument list, it's not there in the new
+  // prototype
+  if (HasSPTAR) {
+    revng_assert(Arguments.size() > 0);
+    Arguments.erase(Arguments.begin());
+  }
+
+  // If the old return type and the new one are identical, switch to the old
+  // one in the new call
+  auto *OldCallType = OldCall->getFunctionType();
+  auto *OldReturnType = OldCallType->getReturnType();
+  auto *NewReturnType = CalleeType->getReturnType();
+  if (auto *OldStructType = dyn_cast<StructType>(OldReturnType)) {
+    if (auto *NewStructType = dyn_cast<StructType>(NewReturnType)) {
+      if (NewStructType->isLayoutIdentical(OldStructType)) {
+        CalleeType = FunctionType::get(OldReturnType,
+                                       CalleeType->params(),
+                                       CalleeType->isVarArg());
+      }
+    }
+  }
+
+  // Actually create the new call and replace the old one
+  CallInst *NewCall = B.CreateCall(CalleeType, CalledValue, Arguments);
+  NewCall->copyMetadata(*OldCall);
+  NewCall->setAttributes(OldCall->getAttributes());
+  const auto &[PointerReturns, PointerArguments] = getPointerMetadata(Layout);
+  setPointersMetadata(NewCall, PointerReturns, PointerArguments);
+
+  Value *ReturnValuePointer = nullptr;
+  switch (Layout.returnMethod()) {
+  case ReturnMethod::ModelAggregate: {
+    revng_log(Log, "This call site returns a model aggregate");
+    if (HasSPTAR and Legacy) {
+      // In legacy mode, make a reference out of ReturnValuePointer, using a
+      // ModelGEP at offset 0.
+      ReturnValuePointer = Arguments[0];
+      getAsModelGEP(B, ReturnValuePointer, Layout.returnValueAggregateType());
+
+      revng_assert(not OldReturnType->isStructTy());
+      OldCall->replaceAllUsesWith(ReturnValuePointer);
+    } else {
+      revng_assert(not ReturnValuePointer);
+      const auto &ReturnType = Layout.returnValueAggregateType();
+
+      if constexpr (Legacy) {
+        ReturnValuePointer = createAddressOf(B, NewCall, ReturnType);
+      } else {
+        revng_log(Log, "Creating local variable to store the return value");
+        auto &VB = SSA.VariableBuilder;
+        VB.setTargetFunction(Caller);
+        Value *Allocation = nullptr;
+        Value *IntAddress = nullptr;
+        tie(Allocation,
+            IntAddress) = VB.createLocalVariableAndTakeIntAddress(ReturnType);
+        B.CreateStore(NewCall, Allocation);
+        ReturnValuePointer = IntAddress;
+
+        if (HasSPTAR) {
+          if (CallSite.StackReturnValueRange.has_value()) {
+            // StackReturnValueRange is already relative to the initial value
+            // of the stack pointer
+            Redirector.recordSpan(*CallSite.StackReturnValueRange, IntAddress);
+          } else {
+            revng_log(Log,
+                      "Warning: couldn't resolve the location of the pointer "
+                      "to the storage for the return value in the SPTAR");
+          }
+        }
+      }
+
+      // We're returning an aggregate, but not via SPTAR, we're using one or
+      // more registers
+      if (OldReturnType->isStructTy()) {
+        SmallVector<SmallPtrSet<CallInst *, 2>, 2>
+          ExtractedValues = getExtractedValuesFromInstruction(OldCall);
+        for (auto &Group : llvm::enumerate(ExtractedValues)) {
+
+          unsigned FieldIndex = Group.index();
+          SmallPtrSet<CallInst *, 2> &ExtractedAtIndex = Group.value();
+          if (ExtractedAtIndex.empty())
+            continue;
+
+          unsigned BitOffset = getBitOffsetAt(cast<StructType>(OldReturnType),
+                                              FieldIndex);
+          revng_assert(0 == (BitOffset % 8));
+          unsigned ByteOffset = BitOffset / 8;
+
+          Value *Pointer = createAdd(B, ReturnValuePointer, ByteOffset);
+          Type *ExtractedType = (*ExtractedAtIndex.begin())->getType();
+          auto *Load = B.CreateLoad(ExtractedType, pointer(B, Pointer));
+
+          for (CallInst *Extractor : Group.value()) {
+            Extractor->replaceAllUsesWith(Load);
+            eraseFromParent(Extractor);
+          }
+        }
+
+        revng_assert(OldCall->use_empty());
+      } else {
+        OldCall->replaceAllUsesWith(ReturnValuePointer);
+      }
+    }
+
+  } break;
+
+  case ReturnMethod::Scalar:
+
+    if (OldReturnType != NewReturnType and OldReturnType->isIntegerTy()
+        and NewReturnType->isIntegerTy()) {
+      // We're using a large register to return a smaller integer value (e.g.,
+      // returning a 32-bit integer through rax, which is 64-bit)
+      auto OldSize = OldReturnType->getIntegerBitWidth();
+      auto NewSize = NewReturnType->getIntegerBitWidth();
+      revng_assert(NewSize <= OldSize);
+      auto *Extended = cast<Instruction>(B.CreateZExt(NewCall, OldReturnType));
+      OldCall->replaceAllUsesWith(Extended);
+    } else if (OldReturnType->isStructTy() and NewReturnType->isIntegerTy()) {
+      // We're returning a large integer value through multiple values (e.g.,
+      // returning a 64-bit integer through two registers in i386)
+      SmallVector<SmallPtrSet<CallInst *, 2>, 2>
+        ExtractedValues = getExtractedValuesFromInstruction(OldCall);
+      for (auto &Group : llvm::enumerate(ExtractedValues)) {
+
+        unsigned FieldIndex = Group.index();
+        SmallPtrSet<CallInst *, 2> &ExtractedAtIndex = Group.value();
+        if (ExtractedAtIndex.empty())
+          continue;
+
+        unsigned ShiftAmount = getBitOffsetAt(cast<StructType>(OldReturnType),
+                                              FieldIndex);
+        Type *TruncatedType = (*ExtractedAtIndex.begin())->getType();
+        Value *Replacement = B.CreateTrunc(B.CreateLShr(NewCall, ShiftAmount),
+                                           TruncatedType);
+        for (CallInst *Extractor : Group.value()) {
+          revng_assert(TruncatedType == Extractor->getType());
+          Extractor->replaceAllUsesWith(Replacement);
+          eraseFromParent(Extractor);
+        }
+      }
+
+      revng_assert(OldCall->use_empty());
+    } else {
+      revng_assert(not OldReturnType->isStructTy());
+      OldCall->replaceAllUsesWith(NewCall);
+    }
+    break;
+
+  case ReturnMethod::Void:
+    // Nothing to do here
+    break;
+  case ReturnMethod::RegisterSet:
+    OldCall->replaceAllUsesWith(NewCall);
+    break;
+
+  default:
+    revng_abort();
+  }
+
+  eraseFromParent(OldCall);
+  revng_assert(CalleeType->getPointerTo() == CalledValue->getType());
+
+  return Redirector;
+}
+
+template<bool Legacy>
+bool SegregateStackAccesses<Legacy>::runOnFunction(const model::Function
+                                                     &ModelFunction,
+                                                   llvm::Function &Function) {
+  SegregateFunctionStack<Legacy> Worker(*this, ModelFunction, Function);
+  Worker.upgrade();
+  Worker.segregate();
+  return true;
+}
+
 static void getAnalysisUsage(llvm::AnalysisUsage &AU) {
   AU.setPreservesCFG();
   AU.addRequired<LoadModelWrapperPass>();
@@ -1546,7 +2251,7 @@ struct LegacySegregateStackAccessesPipe {
   }
 
   void registerPasses(legacy::PassManager &Manager) {
-    using Pass = SegregateStackAccesses</* LegacyLocalVariables = */ true>;
+    using Pass = SegregateStackAccesses</* Legacy = */ true>;
     Manager.add(new pipeline::FunctionPass<Pass>);
   }
 };
@@ -1567,7 +2272,7 @@ struct SegregateStackAccessesPipe {
   }
 
   void registerPasses(legacy::PassManager &Manager) {
-    using Pass = SegregateStackAccesses</* LegacyLocalVariables = */ false>;
+    using Pass = SegregateStackAccesses</* Legacy = */ false>;
     Manager.add(new pipeline::FunctionPass<Pass>);
   }
 };
diff --git a/lib/TypeShrinking/BitLiveness.cpp b/lib/TypeShrinking/BitLiveness.cpp
index 71ebcf913..23679d8e9 100644
--- a/lib/TypeShrinking/BitLiveness.cpp
+++ b/lib/TypeShrinking/BitLiveness.cpp
@@ -14,6 +14,7 @@
 
 #include "llvm/ADT/APInt.h"
 #include "llvm/ADT/BitVector.h"
+#include "llvm/ADT/GraphTraits.h"
 #include "llvm/IR/AssemblyAnnotationWriter.h"
 #include "llvm/IR/Constants.h"
 #include "llvm/IR/Instruction.h"
@@ -30,12 +31,12 @@
 
 namespace TypeShrinking {
 
-class BitLivenwssAnnotatedWriter : public llvm::AssemblyAnnotationWriter {
+class BitLivenessAnnotatedWriter : public llvm::AssemblyAnnotationWriter {
 private:
   const BitLivenessAnalysisResults &Results;
 
 public:
-  BitLivenwssAnnotatedWriter(const BitLivenessAnalysisResults &Results) :
+  BitLivenessAnnotatedWriter(const BitLivenessAnalysisResults &Results) :
     Results(Results) {}
 
   void emitInstructionAnnot(const llvm::Instruction *I,
@@ -49,7 +50,7 @@ public:
 };
 
 void BitLivenessWrapperPass::dump(llvm::Function &F) const {
-  BitLivenwssAnnotatedWriter Annotator(Result);
+  BitLivenessAnnotatedWriter Annotator(Result);
   llvm::raw_os_ostream Stream(dbg);
   F.print(Stream, &Annotator);
 }
@@ -61,7 +62,8 @@ struct BitLivenessAnalysis {
   using GraphType = GenericGraph<DataFlowNode> *;
   using LatticeElement = uint32_t;
   using Label = DataFlowNode *;
-  using MFPResult = MFP::MFPResult<BitLivenessAnalysis::LatticeElement>;
+  using MFPResult = mfp::MFPResult<BitLivenessAnalysis::LatticeElement>;
+  using ExtraStateType = mfp::NoExtraState;
 
   uint32_t combineValues(const uint32_t &LHS, const uint32_t &RHS) const {
     return std::max(LHS, RHS);
@@ -71,7 +73,9 @@ struct BitLivenessAnalysis {
     return LHS <= RHS;
   }
 
-  uint32_t applyTransferFunction(DataFlowNode *L, const uint32_t E) const;
+  uint32_t applyTransferFunction(DataFlowNode *L,
+                                 const uint32_t E,
+                                 mfp::NoExtraState &) const;
 };
 
 using BitVector = llvm::BitVector;
@@ -239,7 +243,8 @@ static uint32_t transferZExt(Instruction *Ins, const uint32_t &Element) {
 }
 
 uint32_t BitLivenessAnalysis::applyTransferFunction(DataFlowNode *L,
-                                                    const uint32_t E) const {
+                                                    const uint32_t E,
+                                                    mfp::NoExtraState &) const {
   auto *Ins = L->Instruction;
   switch (Ins->getOpcode()) {
   case Instruction::And:
@@ -277,13 +282,23 @@ BitLivenessPass::Result BitLivenessPass::run(llvm::Function &F,
     }
   }
 
-  auto MFPRes = MFP::getMaximalFixedPoint<BitLivenessAnalysis>({},
-                                                               &DataFlowGraph,
-                                                               0,
-                                                               Top,
-                                                               ExtremalLabels);
+  // The data-flow graph has no designated entry node and the analysis is
+  // backward-shaped (extremals are sinks). Seed RPOT from every node.
+  mfp::MFPConfiguration<BitLivenessAnalysis> Configuration{
+    .Flow = &DataFlowGraph,
+    .ExtremalValue = &Top,
+    .ExtremalLabels = &ExtremalLabels,
+    .EntryLabels = mfp::All{}
+  };
+
+  auto Results = mfp::getMaximalFixedPoint<BitLivenessAnalysis>(Configuration);
+
+  using GraphType = typename BitLivenessAnalysis::GraphType;
+  using GraphTraits = llvm::GraphTraits<GraphType>;
+  static_assert(mfp::HasNodeRange<GraphTraits>);
+
   BitLivenessPass::Result Result;
-  for (auto &[Label, MFPResult] : MFPRes) {
+  for (auto &[Label, MFPResult] : Results) {
     auto &Entry = Result[Label->Instruction];
     Entry.Result = MFPResult.InValue;
     Entry.Operands = MFPResult.OutValue;
@@ -292,7 +307,7 @@ BitLivenessPass::Result BitLivenessPass::run(llvm::Function &F,
   if (llvm::Error Error = DataFlowGraph.verify())
     revng_abort(revng::unwrapError(std::move(Error)).c_str());
 
-  MFP::Graph<BitLivenessAnalysis> MFPGraph(&DataFlowGraph, MFPRes);
+  mfp::Graph<BitLivenessAnalysis> MFPGraph(&DataFlowGraph, Results);
 
   return Result;
 }
@@ -306,7 +321,7 @@ bool BitLivenessWrapperPass::runOnFunction(llvm::Function &F) {
 } // namespace TypeShrinking
 
 template<>
-void MFP::dump(llvm::raw_ostream &Stream,
+void mfp::dump(llvm::raw_ostream &Stream,
                unsigned Indent,
                const unsigned &Value) {
   Stream << Value;
diff --git a/lib/ValueMaterializer/AdvancedValueInfo.cpp b/lib/ValueMaterializer/AdvancedValueInfo.cpp
index 0dc65b6d8..66fb68394 100644
--- a/lib/ValueMaterializer/AdvancedValueInfo.cpp
+++ b/lib/ValueMaterializer/AdvancedValueInfo.cpp
@@ -78,7 +78,8 @@ bool AdvancedValueInfoMFI::isLessOrEqual(const LatticeElement &LHS,
 
 AdvancedValueInfoMFI::LatticeElement
 AdvancedValueInfoMFI::applyTransferFunction(Label L,
-                                            const LatticeElement &E) const {
+                                            const LatticeElement &E,
+                                            mfp::NoExtraState &) const {
 
   revng_log(AVILogger, "   " << L->toString());
   LoggerIndent Indent(AVILogger);
@@ -190,7 +191,7 @@ AdvancedValueInfoMFI::applyTransferFunction(Label L,
 }
 
 void AdvancedValueInfoMFI::dump(GraphType CFEG, const ResultsMap &AllResults) {
-  MFP::Graph<AdvancedValueInfoMFI> MFPGraph(CFEG, AllResults);
+  mfp::Graph<AdvancedValueInfoMFI> MFPGraph(CFEG, AllResults);
   llvm::WriteGraph(&MFPGraph, "cfeg");
 }
 
@@ -199,7 +200,7 @@ void AdvancedValueInfoMFI::dump(GraphType CFEG, const ResultsMap &AllResults) {
 std::tuple<std::map<llvm::Instruction *, ConstantRangeSet>,
            ControlFlowEdgesGraph,
            map<const ForwardNode<ControlFlowEdgesNode> *,
-               MFP::MFPResult<map<llvm::Instruction *, ConstantRangeSet>>>>
+               mfp::MFPResult<map<llvm::Instruction *, ConstantRangeSet>>>>
 runAVI(const DataFlowGraph &DFG,
        llvm::Instruction *Context,
        const llvm::DominatorTree &DT,
@@ -237,7 +238,7 @@ runAVI(const DataFlowGraph &DFG,
       std::map<llvm::Instruction *, ConstantRangeSet>{},
       ControlFlowEdgesGraph(),
       map<const ForwardNode<ControlFlowEdgesNode> *,
-          MFP::MFPResult<map<llvm::Instruction *, ConstantRangeSet>>>{}
+          mfp::MFPResult<map<llvm::Instruction *, ConstantRangeSet>>>{}
     };
   }
 
@@ -315,13 +316,17 @@ runAVI(const DataFlowGraph &DFG,
     ExtremalValue[I] = ConstantRangeSet(I->getType()->getIntegerBitWidth(),
                                         true);
 
-  auto AllResults = MFP::getMaximalFixedPoint(AVIMFI,
-                                              &CFEG,
-                                              {},
-                                              ExtremalValue,
-                                              InitialNodes,
-                                              InitialNodes,
-                                              AVILogger);
+  mfp::MFPConfiguration<AdvancedValueInfoMFI> Configuration{
+    .Instance = &AVIMFI,
+    .Flow = &CFEG,
+    .ExtremalValue = &ExtremalValue,
+    .ExtremalLabels = &InitialNodes,
+    .EntryLabels = &InitialNodes,
+    .Logger = &AVILogger
+  };
+
+  auto GetMaximalFixedPoint = mfp::getMaximalFixedPoint<AdvancedValueInfoMFI>;
+  auto AllResults = GetMaximalFixedPoint(Configuration);
 
   if (AVILogger.isEnabled()) {
     AVILogger << "Dumping MFP results:" << DoLog;
@@ -329,9 +334,9 @@ runAVI(const DataFlowGraph &DFG,
     for (const auto &[Node, AnalysisResults] : AllResults) {
       AVILogger << Node->toString() << ":\n";
       AVILogger << "  Initial value:\n";
-      MFP::dump(*AVILogger.getAsLLVMStream().get(), 2, AnalysisResults.InValue);
+      mfp::dump(*AVILogger.getAsLLVMStream().get(), 2, AnalysisResults.InValue);
       AVILogger << "  Final value:\n";
-      MFP::dump(*AVILogger.getAsLLVMStream().get(),
+      mfp::dump(*AVILogger.getAsLLVMStream().get(),
                 2,
                 AnalysisResults.OutValue);
     }
@@ -344,7 +349,7 @@ runAVI(const DataFlowGraph &DFG,
 }
 
 template<>
-void MFP::dump(llvm::raw_ostream &Stream,
+void mfp::dump(llvm::raw_ostream &Stream,
                unsigned Indent,
                const std::map<llvm::Instruction *, ConstantRangeSet> &Element) {
   for (const auto &[I, Range] : Element) {
@@ -357,7 +362,7 @@ void MFP::dump(llvm::raw_ostream &Stream,
 }
 
 template<>
-void MFP::dumpLabel(llvm::raw_ostream &Stream,
+void mfp::dumpLabel(llvm::raw_ostream &Stream,
                     const ControlFlowEdgesGraph::Node *const &Label) {
   Stream << Label->toString();
 }
diff --git a/python/revng/internal/cli/_commands/override_by_name.py b/python/revng/internal/cli/_commands/override_by_name.py
index 082d847d4..77a356cf2 100644
--- a/python/revng/internal/cli/_commands/override_by_name.py
+++ b/python/revng/internal/cli/_commands/override_by_name.py
@@ -87,6 +87,8 @@ class ModelOverrideByName(Command):
                     return 1
 
                 for base_function in base_model["Functions"]:
+                    if "Name" not in base_function:
+                        continue
                     if base_function["Name"] == function_name:
                         function_to_override["Entry"] = base_function["Entry"]
                         function_to_override["Name"] = base_function["Name"]
diff --git a/python/revng/internal/pipeline.yml b/python/revng/internal/pipeline.yml
index 0de255072..016abbde8 100644
--- a/python/revng/internal/pipeline.yml
+++ b/python/revng/internal/pipeline.yml
@@ -261,7 +261,7 @@ branches:
       - pipe: pure-llvm-passes-pipe
         arguments: [llvm-functions]
         configuration:
-          passes: [hoist-struct-phis]
+          passes: [split-struct-phis]
       - pipe: legacy-segregate-stack-accesses
         arguments: [llvm-functions]
       - pipe: pure-llvm-passes-pipe
@@ -312,7 +312,7 @@ branches:
         arguments: [llvm-functions]
         configuration:
           passes:
-            - hoist-struct-phis
+            - split-struct-phis
       - pipe: segregate-stack-accesses
         arguments: [llvm-functions]
       - pipe: pure-llvm-passes-pipe
diff --git a/share/doc/revng/references/mime-types.md b/share/doc/revng/references/mime-types.md
index 12ed16d38..475f2fa66 100644
--- a/share/doc/revng/references/mime-types.md
+++ b/share/doc/revng/references/mime-types.md
@@ -26,6 +26,7 @@ USAGE: revng-artifact [options] <artifact> <binary>
   emit-model-header           - text/x.c+ptml
   emit-type-definitions       - text/x.c+tar+gz
   cleanup-ir                  - application/x.llvm.bc+zstd
+  segregate-stack-accesses    - application/x.llvm.bc+zstd
   emit-c                      - text/x.c+ptml+tar+gz
   emit-c-as-single-file       - text/x.c+ptml
 ```
diff --git a/share/revng/include/primitive-types.h b/share/revng/include/primitive-types.h
index a9388d737..0884dfa5b 100644
--- a/share/revng/include/primitive-types.h
+++ b/share/revng/include/primitive-types.h
@@ -216,9 +216,9 @@ static_assert(sizeof(float128_t) == 16, "");
 // Undefined values
 //
 
-extern uintmax_t undef_value(void);
+extern void const *undef_value(size_t size);
 
-#define undef(T) ((T) undef_value())
+#define undef(T) (*(__typeof__(T) *) undef_value(sizeof(T)))
 
 //
 // Break and continue
diff --git a/share/revng/pipelines/revng-pipelines.yml b/share/revng/pipelines/revng-pipelines.yml
index a28bc946f..be5655056 100644
--- a/share/revng/pipelines/revng-pipelines.yml
+++ b/share/revng/pipelines/revng-pipelines.yml
@@ -420,7 +420,7 @@ Branches:
           - Type: llvm-pipe
             UsedContainers: [functions.bc.zstd]
             Passes:
-              - hoist-struct-phis
+              - split-struct-phis
               - legacy-segregate-stack-accesses
               - cleanup-stack-size-markers
               - dce
@@ -483,7 +483,7 @@ Branches:
           - Type: llvm-pipe
             UsedContainers: [functions.bc.zstd]
             Passes:
-              - hoist-struct-phis
+              - split-struct-phis
               - remove-llvmassume-calls
               - dce
               - remove-pointer-casts
@@ -648,7 +648,7 @@ Branches:
           - Type: llvm-pipe
             UsedContainers: [functions.bc.zstd]
             Passes:
-              - hoist-struct-phis
+              - split-struct-phis
               - segregate-stack-accesses
               - cleanup-stack-size-markers
               - dce
@@ -673,6 +673,11 @@ Branches:
               - strip-dead-prototypes
               - split-overflow-intrinsics
               - dce
+        Artifacts:
+          Container: functions.bc.zstd
+          Kind: stack-accesses-segregated
+          SingleTargetFilename: clean-ir.ll
+          Docs: ""
       - Name: emit-c
         Pipes:
           - Type: llvm-pipe
diff --git a/share/revng/test/configuration/revng/segregate-stack-accesses.yml b/share/revng/test/configuration/revng/segregate-stack-accesses.yml
index 99396ca7a..315ed91b5 100644
--- a/share/revng/test/configuration/revng/segregate-stack-accesses.yml
+++ b/share/revng/test/configuration/revng/segregate-stack-accesses.yml
@@ -24,7 +24,7 @@ commands:
 
       revng analyze --resume "$OUTPUT" detect-stack-size "$INPUT" -o /dev/null;
 
-      revng artifact --resume "$OUTPUT" make-segment-ref "$INPUT" |
+      revng artifact --resume "$OUTPUT" segregate-stack-accesses "$INPUT" |
         revng opt -S | FileCheck ${SOURCE}.filecheck.ll;
 
       revng artifact --resume "$OUTPUT" emit-c "$INPUT" -o /dev/null;
diff --git a/share/revng/test/tests/analysis/SegregateStackAccesses/dynamic_native/segregate.c.filecheck.ll b/share/revng/test/tests/analysis/SegregateStackAccesses/dynamic_native/segregate.c.filecheck.ll
index 581bc375f..f4ce7db30 100644
--- a/share/revng/test/tests/analysis/SegregateStackAccesses/dynamic_native/segregate.c.filecheck.ll
+++ b/share/revng/test/tests/analysis/SegregateStackAccesses/dynamic_native/segregate.c.filecheck.ll
@@ -7,6 +7,10 @@ CHECK-DAG: add i64 [[IGN:.*]]%[[ARG1]]
 CHECK-DAG: add i64 [[IGN:.*]]%[[ARG2]]
 CHECK: }
 
+CHECK: define i64 @local_call_raw_primitives_on_registers() [[IGN:.*]] {
+CHECK-DAG:   = call i64 @local_raw_primitives_on_registers(i64 2, i64 1)
+CHECK: }
+
 CHECK: define i64 @local_raw_pointers_on_registers(i64 %[[ARG1:.*]], i64 %[[ARG2:.*]]) [[IGN:.*]] {
 CHECK-DAG: %[[ARG1_PTR:.*]] = inttoptr i64 %[[ARG1]] to ptr
 CHECK-DAG: load i64, ptr %[[ARG1_PTR:.*]]
@@ -14,64 +18,147 @@ CHECK-DAG: %[[ARG2_PTR:.*]] = inttoptr i64 %[[ARG2]] to ptr
 CHECK-DAG: load i64, ptr %[[ARG2_PTR]]
 CHECK: }
 
+CHECK: define i64 @local_call_raw_pointers_on_registers() [[IGN:.*]] {
+CHECK-DAG:   = call i64 @local_raw_pointers_on_registers(i64 [[ARG:.*]], i64 [[ARG]])
+CHECK: }
+
 CHECK: define i64 @local_raw_primitives_on_stack(i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[STACK_ARG:.*]]) [[IGN:.*]] {
-CHECK-DAG:   %[[STACK_ARG_AO:.*]] = call i64 @AddressOf([[IGN:.*]]i64 %[[STACK_ARG]])
-CHECK-DAG:   %[[STACK_ARG8:.*]] = add i64 %[[STACK_ARG_AO]], 8
+CHECK-DAG:   %[[STACK_ARG8:.*]] = add i64 %[[STACK_ARG]], 8
 CHECK-DAG:   %[[STACK_ARG8_PTR:.*]] = inttoptr i64 %[[STACK_ARG8]] to ptr
 CHECK-DAG:   load i64, ptr %[[STACK_ARG8_PTR:.*]]
-CHECK-DAG:   %[[STACK_ARG_PTR:.*]] = inttoptr i64 %[[STACK_ARG_AO]] to ptr
+CHECK-DAG:   %[[STACK_ARG_PTR:.*]] = inttoptr i64 %[[STACK_ARG]] to ptr
 CHECK-DAG:   load i64, ptr %[[STACK_ARG_PTR]]
 CHECK: }
 
+CHECK: define i64 @local_call_raw_primitives_on_stack() [[IGN:.*]] {
+CHECK-DAG:   %[[STACK:.*]] = alloca [16 x i8]
+CHECK-DAG:   %[[STACK_INT:.*]] = ptrtoint ptr %[[STACK]] to i64
+CHECK-DAG:   %[[STACK_INT_8:.*]] = add i64 %[[STACK_INT]], 8
+CHECK-DAG:   %[[STACK_8:.*]] = inttoptr i64 %[[STACK_INT_8]] to ptr
+CHECK-DAG:   store i64 8, ptr %[[STACK_8]]
+CHECK-DAG:   store i64 7, ptr %[[STACK]]
+CHECK-DAG:   = call i64 @local_raw_primitives_on_stack(i64 4, i64 3, i64 2, i64 1, i64 5, i64 6, i64 %[[STACK_INT]])
+CHECK: }
+
 CHECK: define i64 @local_cabi_primitives_on_registers(i64 %[[ARG1:.*]], i64 %[[ARG2:.*]]) [[IGN:.*]] {
 CHECK-DAG: add i64 [[IGN:.*]]%[[ARG1]]
 CHECK-DAG: add i64 [[IGN:.*]]%[[ARG2]]
 CHECK: }
 
+CHECK: define i64 @local_call_cabi_primitives_on_registers() [[IGN:.*]] {
+CHECK-DAG:   = call i64 @local_cabi_primitives_on_registers(i64 1, i64 2)
+CHECK: }
+
 CHECK: define i64 @local_cabi_primitives_on_stack(i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[STACK_ARG1:.*]], i64 %[[STACK_ARG2:.*]]) [[IGN:.*]] {
 CHECK-DAG:   %[[IGN:.*]] = add i64 %[[IGN:.*]]%[[STACK_ARG1]]
 CHECK-DAG:   %[[IGN:.*]] = add i64 %[[IGN:.*]]%[[STACK_ARG2]]
 CHECK: }
 
+CHECK: define i64 @local_call_cabi_primitives_on_stack() [[IGN:.*]] {
+CHECK-DAG:   = call i64 @local_cabi_primitives_on_stack(i64 1, i64 2, i64 3, i64 4, i64 5, i64 6, i64 [[SCALAR1:.*]], i64 [[SCALAR2:.*]])
+CHECK: }
+
 CHECK: define i64 @local_cabi_aggregate_on_registers(i64 %[[ARG1:.*]]) [[IGN:.*]] {
-CHECK-DAG:   %[[ARG1_AO:.*]] = call i64 @AddressOf([[IGN:.*]]i64 %[[ARG1]])
-CHECK-DAG:   %[[FIELD1_PTR:.*]] = inttoptr i64 %[[ARG1_AO]] to ptr
+CHECK-DAG:   %[[FIELD1_PTR:.*]] = inttoptr i64 %[[ARG1]] to ptr
 CHECK-DAG:   load i64, ptr %[[FIELD1_PTR]]
-CHECK-DAG:   %[[FIELD2_ADDR:.*]] = add i64 %[[ARG1_AO]], 8
+CHECK-DAG:   %[[FIELD2_ADDR:.*]] = add i64 %[[ARG1]], 8
 CHECK-DAG:   %[[FIELD2_PTR:.*]] = inttoptr i64 %[[FIELD2_ADDR]] to ptr
 CHECK-DAG:   load i64, ptr %[[FIELD2_PTR]], align 8
 CHECK: }
 
+CHECK: define i64 @local_call_cabi_aggregate_on_registers() [[IGN:.*]] {
+CHECK-DAG:   %[[STACK:.*]] = alloca [16 x i8]
+CHECK-DAG:   %[[STACK_INT:.*]] = ptrtoint ptr %[[STACK]] to i64
+CHECK-DAG:   store i64 1, ptr %[[STACK]]
+CHECK-DAG:   %[[STACK_INT_8:.*]] = add i64 %[[STACK_INT]], 8
+CHECK-DAG:   %[[STACK_8:.*]] = inttoptr i64 %[[STACK_INT_8]] to ptr
+CHECK-DAG:   store i64 2, ptr %[[STACK_8]]
+CHECK-DAG:   = call i64 @local_cabi_aggregate_on_registers(i64 %[[STACK_INT]])
+CHECK: }
+
 CHECK: define i64 @local_cabi_aggregate_on_stack(i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[STACK_ARG:.*]]) [[IGN:.*]] {
-CHECK-DAG:   %[[STACK_ARG_AO:.*]] = call i64 @AddressOf([[IGN:.*]]i64 %[[STACK_ARG]])
-CHECK-DAG:   %[[FIELD1_PTR:.*]] = inttoptr i64 %[[STACK_ARG_AO]] to ptr
+CHECK-DAG:   %[[FIELD1_PTR:.*]] = inttoptr i64 %[[STACK_ARG]] to ptr
 CHECK-DAG:   load i64, ptr %[[FIELD1_PTR]]
-CHECK-DAG:   %[[FIELD2_ADDR:.*]] = add i64 %[[STACK_ARG_AO]], 8
+CHECK-DAG:   %[[FIELD2_ADDR:.*]] = add i64 %[[STACK_ARG]], 8
 CHECK-DAG:   %[[FIELD2_PTR:.*]] = inttoptr i64 %[[FIELD2_ADDR]] to ptr
 CHECK-DAG:   load i64, ptr %[[FIELD2_PTR]]
 CHECK: }
 
+CHECK: define i64 @local_call_cabi_aggregate_on_stack() [[IGN:.*]] {
+CHECK-DAG:   %[[STACK:.*]] = alloca [16 x i8]
+CHECK-DAG:   %[[STACK_INT:.*]] = ptrtoint ptr %[[STACK]] to i64
+CHECK-DAG:   store i64 1, ptr %[[STACK]]
+CHECK-DAG:   %[[STACK_INT_8:.*]] = add i64 %[[STACK_INT]], 8
+CHECK-DAG:   %[[STACK_8:.*]] = inttoptr i64 %[[STACK_INT_8]] to ptr
+CHECK-DAG:   store i64 2, ptr %[[STACK_8]]
+CHECK-DAG:   = call i64 @local_cabi_aggregate_on_stack(i64 1, i64 2, i64 3, i64 4, i64 5, i64 6, i64 %[[STACK_INT]])
+CHECK: }
+
 CHECK: define i64 @local_cabi_aggregate_on_stack_and_registers(i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[IGN:.*]], i64 %[[STACK_ARG:.*]]) [[IGN:.*]] {
-CHECK-DAG:   %[[STACK_ARG_AO:.*]] = call i64 @AddressOf([[IGN:.*]]i64 %[[STACK_ARG]])
-CHECK-DAG:   %[[FIELD1_PTR:.*]] = inttoptr i64 %[[STACK_ARG_AO]] to ptr
+CHECK-DAG:   %[[FIELD1_PTR:.*]] = inttoptr i64 %[[STACK_ARG]] to ptr
 CHECK-DAG:   load i64, ptr %[[FIELD1_PTR]]
-CHECK-DAG:   %[[FIELD2_ADDR:.*]] = add i64 %[[STACK_ARG_AO]], 8
+CHECK-DAG:   %[[FIELD2_ADDR:.*]] = add i64 %[[STACK_ARG]], 8
 CHECK-DAG:   %[[FIELD2_PTR:.*]] = inttoptr i64 %[[FIELD2_ADDR]] to ptr
 CHECK-DAG:   load i64, ptr %[[FIELD2_PTR]]
 CHECK: }
 
-CHECK: define i64 @local_caller() [[IGN:.*]] {
-CHECK-DAG:   = call i64 @local_raw_primitives_on_registers(i64 2, i64 1)
-CHECK-DAG:   = call i64 @local_raw_pointers_on_registers(i64 %[[ARG:.*]], i64 %[[ARG]])
-CHECK-DAG:   %[[STACK:.*]] = call i64 @revng_call_stack_arguments([[IGN:.*]], i64 16)
-CHECK-DAG:   = call i64 @local_raw_primitives_on_stack(i64 4, i64 3, i64 2, i64 1, i64 5, i64 6, i64 %[[STACK]])
-CHECK-DAG:   = call i64 @local_cabi_primitives_on_registers(i64 1, i64 2)
-TODO: devise a pipeline that highlights both arguments as immediates
-CHECK-DAG:   = call i64 @local_cabi_primitives_on_stack(i64 1, i64 2, i64 3, i64 4, i64 5, i64 6, i64 [[SCALAR1:.*]], i64 [[SCALAR2:.*]])
-CHECK-DAG:   %[[AGGREGATE:.*]] = call i64 @revng_call_stack_arguments([[IGN:.*]], i64 16)
-CHECK-DAG:   = call i64 @local_cabi_aggregate_on_registers(i64 %[[AGGREGATE]])
-CHECK-DAG:   %[[AGGREGATE:.*]] = call i64 @revng_call_stack_arguments([[IGN:.*]], i64 16)
-CHECK-DAG:   = call i64 @local_cabi_aggregate_on_stack(i64 1, i64 2, i64 3, i64 4, i64 5, i64 6, i64 %[[AGGREGATE]])
-CHECK-DAG:   %[[AGGREGATE:.*]] = call i64 @revng_call_stack_arguments([[IGN:.*]], i64 16)
-CHECK-DAG:   = call i64 @local_cabi_aggregate_on_stack_and_registers(i64 1, i64 2, i64 3, i64 4, i64 5, i64 %[[AGGREGATE]])
+CHECK: define i64 @local_call_cabi_aggregate_on_stack_and_registers() [[IGN:.*]] {
+CHECK-DAG:   %[[STACK:.*]] = alloca [16 x i8]
+CHECK-DAG:   %[[STACK_INT:.*]] = ptrtoint ptr %[[STACK]] to i64
+CHECK-DAG:   store i64 1, ptr %[[STACK]]
+CHECK-DAG:   %[[STACK_INT_8:.*]] = add i64 %[[STACK_INT]], 8
+CHECK-DAG:   %[[STACK_8:.*]] = inttoptr i64 %[[STACK_INT_8]] to ptr
+CHECK-DAG:   store i64 2, ptr %[[STACK_8]]
+CHECK-DAG:   = call i64 @local_cabi_aggregate_on_stack_and_registers(i64 1, i64 2, i64 3, i64 4, i64 5, i64 %[[STACK_INT]])
+CHECK: }
+
+CHECK: define <{ i64, i64 }> @local_raw_return_small_aggregate() [[IGN:.*]] {
+CHECK-DAG:   %[[RESULT:.*]] = call <{ i64, i64 }> @struct_initializer(i64 124, i64 123)
+CHECK-DAG:   ret <{ i64, i64 }> %[[RESULT]]
+CHECK: }
+
+CHECK: define i64 @local_call_raw_return_small_aggregate() [[IGN:.*]] {
+CHECK:   %[[RESULT:.*]] = call <{ i64, i64 }> @local_raw_return_small_aggregate()
+CHECK-DAG:   call i64 @OpaqueExtractvalue(<{ i64, i64 }> %[[RESULT]], i64 1)
+CHECK: }
+
+CHECK: define [16 x i8] @local_cabi_return_small_aggregate() [[IGN:.*]] {
+CHECK-DAG:   %[[RETURN_ALLOCA:.*]] = alloca [16 x i8]
+CHECK-DAG:   %[[RETURN_ALLOCA_INT:.*]] = ptrtoint ptr %[[RETURN_ALLOCA]] to i64
+CHECK-DAG:   %[[RETURN_ALLOCA_INT_8:.*]] = add i64 %[[RETURN_ALLOCA_INT]], 8
+CHECK-DAG:   %[[RETURN_ALLOCA_8:.*]] = inttoptr i64 %[[RETURN_ALLOCA_INT_8]] to ptr
+CHECK-DAG:   store i64 124, ptr %[[RETURN_ALLOCA]]
+CHECK-DAG:   store i64 123, ptr %[[RETURN_ALLOCA_8]]
+CHECK-DAG:   %[[TO_RETURN:.*]] = load [16 x i8], ptr %[[RETURN_ALLOCA]]
+CHECK-DAG:   ret [16 x i8] %[[TO_RETURN]]
+CHECK: }
+
+CHECK: define i64 @local_call_cabi_return_small_aggregate() [[IGN:.*]] {
+CHECK-DAG:   %[[RETURN_ALLOCA:.*]] = alloca [16 x i8]
+CHECK-DAG:   %[[RETURN_ALLOCA_INT:.*]] = ptrtoint ptr %[[RETURN_ALLOCA]] to i64
+CHECK-DAG:   %[[RETURN_VALUE:.*]] = call [16 x i8] @local_cabi_return_small_aggregate()
+CHECK-DAG:   store [16 x i8] %[[RETURN_VALUE]], ptr %[[RETURN_ALLOCA]]
+CHECK-DAG:   %[[RETURN_ALLOCA_INT_8:.*]] = add i64 %[[RETURN_ALLOCA_INT]], 8
+CHECK-DAG:   %[[RETURN_ALLOCA_8:.*]] = inttoptr i64 %[[RETURN_ALLOCA_INT_8]] to ptr
+CHECK-DAG:   %[[TO_RETURN:.*]] = load i64, ptr %[[RETURN_ALLOCA_8]]
+CHECK: }
+
+CHECK: define [64 x i8] @local_cabi_return_big_aggregate() [[IGN:.*]] {
+CHECK-DAG:   %[[RETURN_ALLOCA:.*]] = alloca [64 x i8]
+CHECK-DAG:   %[[RETURN_ALLOCA_INT:.*]] = ptrtoint ptr %[[RETURN_ALLOCA]] to i64
+CHECK-DAG:   %[[RETURN_ALLOCA_INT_16:.*]] = add i64 %[[RETURN_ALLOCA_INT]], 16
+CHECK-DAG:   %[[RETURN_ALLOCA_16:.*]] = inttoptr i64 %[[RETURN_ALLOCA_INT_16]] to ptr
+CHECK-DAG:   store i64 123, ptr %[[RETURN_ALLOCA_16]]
+CHECK-DAG:   %[[TO_RETURN:.*]] = load [64 x i8], ptr %[[RETURN_ALLOCA]]
+CHECK-DAG:   ret [64 x i8] %[[TO_RETURN]]
+CHECK: }
+
+CHECK: define i64 @local_call_cabi_return_big_aggregate() [[IGN:.*]] {
+CHECK-DAG:   %[[RETURN_ALLOCA:.*]] = alloca [64 x i8]
+CHECK-DAG:   %[[RETURN_ALLOCA_INT:.*]] = ptrtoint ptr %[[RETURN_ALLOCA]] to i64
+CHECK-DAG:   %[[RETURN_VALUE:.*]] = call [64 x i8] @local_cabi_return_big_aggregate()
+CHECK-DAG:   store [64 x i8] %[[RETURN_VALUE]], ptr %[[RETURN_ALLOCA]]
+CHECK-DAG:   %[[RETURN_ALLOCA_INT_16:.*]] = add i64 %[[RETURN_ALLOCA_INT]], 16
+CHECK-DAG:   %[[RETURN_ALLOCA_16:.*]] = inttoptr i64 %[[RETURN_ALLOCA_INT_16]] to ptr
+CHECK-DAG:   %[[TO_RETURN:.*]] = load i64, ptr %[[RETURN_ALLOCA_16]]
 CHECK: }
diff --git a/share/revng/test/tests/analysis/SegregateStackAccesses/dynamic_native/segregate.c.override.yml b/share/revng/test/tests/analysis/SegregateStackAccesses/dynamic_native/segregate.c.override.yml
index 7f041e3e0..e3e9955cc 100644
--- a/share/revng/test/tests/analysis/SegregateStackAccesses/dynamic_native/segregate.c.override.yml
+++ b/share/revng/test/tests/analysis/SegregateStackAccesses/dynamic_native/segregate.c.override.yml
@@ -37,10 +37,18 @@ Functions:
     Prototype:
       Kind: DefinedType
       Definition: "/TypeDefinitions/100008-CABIFunctionDefinition"
-  - Name: cabi_return_big_aggregate
+  - Name: cabi_return_small_aggregate
     Prototype:
       Kind: DefinedType
       Definition: "/TypeDefinitions/100010-CABIFunctionDefinition"
+  - Name: cabi_return_big_aggregate
+    Prototype:
+      Kind: DefinedType
+      Definition: "/TypeDefinitions/100012-CABIFunctionDefinition"
+  - Name: raw_return_small_aggregate
+    Prototype:
+      Kind: DefinedType
+      Definition: "/TypeDefinitions/100013-RawFunctionDefinition"
 TypeDefinitions:
   - Kind: StructDefinition
     ID: 100003
@@ -310,6 +318,28 @@ TypeDefinitions:
           Definition: "/TypeDefinitions/100003-StructDefinition"
   - Kind: StructDefinition
     ID: 100009
+    Size: 16
+    Fields:
+      - Offset: 0
+        Type:
+          Kind: PrimitiveType
+          PrimitiveKind: Generic
+          Size: 8
+      - Offset: 8
+        Type:
+          Kind: PrimitiveType
+          PrimitiveKind: Generic
+          Size: 8
+  - Kind: CABIFunctionDefinition
+    ID: 100010
+    ABI: SystemV_x86_64
+    ReturnType:
+      Kind: DefinedType
+      Definition: "/TypeDefinitions/100009-StructDefinition"
+    Arguments: []
+  - Kind: StructDefinition
+    ID: 100011
+    Size: 64
     Fields:
       - Offset: 0
         Type:
@@ -351,11 +381,24 @@ TypeDefinitions:
           Kind: PrimitiveType
           PrimitiveKind: Generic
           Size: 8
-    Size: 64
   - Kind: CABIFunctionDefinition
-    ID: 100010
+    ID: 100012
     ABI: SystemV_x86_64
     ReturnType:
       Kind: DefinedType
-      Definition: "/TypeDefinitions/100009-StructDefinition"
+      Definition: "/TypeDefinitions/100011-StructDefinition"
     Arguments: []
+  - Kind: RawFunctionDefinition
+    ID: 100013
+    Architecture: x86_64
+    ReturnValues:
+      - Location: rax_x86_64
+        Type:
+          Kind: PrimitiveType
+          PrimitiveKind: Generic
+          Size: 8
+      - Location: rdx_x86_64
+        Type:
+          Kind: PrimitiveType
+          PrimitiveKind: Generic
+          Size: 8
diff --git a/tests/unit/CMakeLists.txt b/tests/unit/CMakeLists.txt
index f6317d6c5..2874e2f9a 100644
--- a/tests/unit/CMakeLists.txt
+++ b/tests/unit/CMakeLists.txt
@@ -484,6 +484,18 @@ revng_add_test(
   "${CMAKE_BINARY_DIR}/bin/revng opt -S -early-type-shrinking -type-shrinking -instcombine ${SRC}/TypeShrinking.ll | FileCheck ${SRC}/TypeShrinking.ll"
 )
 
+#
+# test_mfp
+#
+
+revng_add_test_executable(test_mfp "${SRC}/MFP.cpp")
+target_compile_definitions(test_mfp PRIVATE "BOOST_TEST_DYN_LINK=1")
+target_include_directories(test_mfp PRIVATE "${CMAKE_SOURCE_DIR}")
+target_link_libraries(test_mfp revngSupport revngUnitTestHelpers
+                      Boost::unit_test_framework ${LLVM_LIBRARIES})
+revng_add_test(NAME test_mfp COMMAND test_mfp)
+set_tests_properties(test_mfp PROPERTIES LABELS "unit;mfp")
+
 #
 # test_combingpass
 #
diff --git a/tests/unit/MFP.cpp b/tests/unit/MFP.cpp
new file mode 100644
index 000000000..8ab6d8109
--- /dev/null
+++ b/tests/unit/MFP.cpp
@@ -0,0 +1,207 @@
+//
+// This file is distributed under the MIT License. See LICENSE.md for details.
+//
+
+#define BOOST_TEST_MODULE MFPExtraState
+bool init_unit_test();
+#include <set>
+#include <string>
+#include <vector>
+
+#include "boost/test/unit_test.hpp"
+
+#include "llvm/ADT/GraphTraits.h"
+
+#include "revng/ADT/GenericGraph.h"
+#include "revng/MFP/MFP.h"
+#include "revng/MFP/SetLattices.h"
+
+// Each node has a name and an ordered list of integer "operations" that the
+// transfer function adds to a `std::set<int>` lattice. The `ExtraState`
+// recording surface uses `(NodeName, OperationIndex)` as its key, so each
+// individual operation can be observed before/after.
+struct OperationNodeData {
+  std::string Name;
+  std::vector<int> Operations;
+};
+
+using OperationNode = ForwardNode<OperationNodeData>;
+using OperationGraph = GenericGraph<OperationNode>;
+
+using OperationKey = std::pair<std::string, size_t>;
+using IntSet = std::set<int>;
+
+struct OperationsMFI : public SetUnionLattice<IntSet> {
+  using Label = OperationNode *;
+  using GraphType = OperationGraph *;
+  using LatticeElement = IntSet;
+  using ExtraStateKey = OperationKey;
+  using ExtraStateType = mfp::ExtraState<OperationKey, LatticeElement>;
+
+  LatticeElement applyTransferFunction(Label Node,
+                                       const LatticeElement &In,
+                                       ExtraStateType &State) const {
+    LatticeElement Current = In;
+    for (size_t I = 0; I < Node->Operations.size(); ++I) {
+      OperationKey K{ Node->Name, I };
+      State.registerBefore(K, Current);
+      Current.insert(Node->Operations[I]);
+      State.registerAfter(K, Current);
+    }
+    return Current;
+  }
+};
+
+static_assert(mfp::MonotoneFrameworkInstance<OperationsMFI>);
+
+namespace {
+
+struct DiamondGraph {
+  // A diamond:
+  //
+  //         Entry:[1]
+  //         /        \
+  //   Left:[2]      Right:[3]
+  //         \        /
+  //           Tail:[4]
+  //
+  OperationGraph Graph;
+  OperationNode *Entry = nullptr;
+  OperationNode *Left = nullptr;
+  OperationNode *Right = nullptr;
+  OperationNode *Tail = nullptr;
+
+  DiamondGraph() {
+    Entry = Graph.addNode(OperationNodeData{ "Entry", { 1 } });
+    Left = Graph.addNode(OperationNodeData{ "Left", { 2 } });
+    Right = Graph.addNode(OperationNodeData{ "Right", { 3 } });
+    Tail = Graph.addNode(OperationNodeData{ "Tail", { 4 } });
+    Graph.setEntryNode(Entry);
+    Entry->addSuccessor(Left);
+    Entry->addSuccessor(Right);
+    Left->addSuccessor(Tail);
+    Right->addSuccessor(Tail);
+  }
+};
+
+} // namespace
+
+// The fixed point of a simple set-union analysis on a diamond graph is the
+// union of every reachable predecessor's contributions. After convergence
+// every node downstream of `Entry` must observe `1` on entry; `Tail` must see
+// the contributions of both `Left` and `Right`.
+BOOST_AUTO_TEST_CASE(DiamondMFP) {
+  DiamondGraph G;
+
+  OperationsMFI MFI;
+  IntSet Bottom;
+  IntSet ExtremalValue;
+  std::vector<OperationNode *> ExtremalLabels{ G.Entry };
+
+  mfp::MFPConfiguration<OperationsMFI> Configuration{
+    .Instance = &MFI,
+    .Flow = &G.Graph,
+    .Bottom = &Bottom,
+    .ExtremalValue = &ExtremalValue,
+    .ExtremalLabels = &ExtremalLabels,
+  };
+
+  auto Result = mfp::getMaximalFixedPoint<OperationsMFI>(Configuration);
+
+  BOOST_TEST(Result.at(G.Entry).InValue == IntSet{});
+  BOOST_TEST(Result.at(G.Entry).OutValue == IntSet({ 1 }));
+
+  BOOST_TEST(Result.at(G.Left).InValue == IntSet({ 1 }));
+  BOOST_TEST(Result.at(G.Left).OutValue == IntSet({ 1, 2 }));
+
+  BOOST_TEST(Result.at(G.Right).InValue == IntSet({ 1 }));
+  BOOST_TEST(Result.at(G.Right).OutValue == IntSet({ 1, 3 }));
+
+  // `Tail` joins both branches, so its incoming value must be `{1, 2, 3}` and
+  // its outgoing value must additionally contain its own contribution `4`.
+  BOOST_TEST(Result.at(G.Tail).InValue == IntSet({ 1, 2, 3 }));
+  BOOST_TEST(Result.at(G.Tail).OutValue == IntSet({ 1, 2, 3, 4 }));
+}
+
+// Verify the analysis reaches the same fixed point on a graph with a back
+// edge (and a multi-step node), exercising the worklist.
+BOOST_AUTO_TEST_CASE(LoopMFP) {
+  // A:[1] --> B:[2,3] --> C:[4]
+  //              ^         /
+  //              \________/
+  OperationGraph Graph;
+  auto *A = Graph.addNode(OperationNodeData{ "A", { 1 } });
+  auto *B = Graph.addNode(OperationNodeData{ "B", { 2, 3 } });
+  auto *C = Graph.addNode(OperationNodeData{ "C", { 4 } });
+  Graph.setEntryNode(A);
+  A->addSuccessor(B);
+  B->addSuccessor(C);
+  C->addSuccessor(B);
+
+  OperationsMFI MFI;
+  IntSet Bottom;
+  IntSet ExtremalValue;
+  std::vector<OperationNode *> ExtremalLabels{ A };
+
+  mfp::MFPConfiguration<OperationsMFI> Configuration{
+    .Instance = &MFI,
+    .Flow = &Graph,
+    .Bottom = &Bottom,
+    .ExtremalValue = &ExtremalValue,
+    .ExtremalLabels = &ExtremalLabels,
+  };
+
+  auto Result = mfp::getMaximalFixedPoint<OperationsMFI>(Configuration);
+
+  // The loop forces B and C's incoming values to include {1, 2, 3, 4} once
+  // the analysis converges.
+  BOOST_TEST(Result.at(A).OutValue == IntSet({ 1 }));
+  BOOST_TEST(Result.at(B).InValue == IntSet({ 1, 2, 3, 4 }));
+  BOOST_TEST(Result.at(B).OutValue == IntSet({ 1, 2, 3, 4 }));
+  BOOST_TEST(Result.at(C).InValue == IntSet({ 1, 2, 3, 4 }));
+  BOOST_TEST(Result.at(C).OutValue == IntSet({ 1, 2, 3, 4 }));
+}
+
+// Same diamond as the first case, but the caller hands in an `ExtraState`
+// pre-populated with a few interesting `(operation, position)` pairs and
+// confirms the recorded values match the per-operation lattice values at the
+// fixed point. The ExtraState observation is a check on top of the regular
+// MFP result, not the focus of the test.
+BOOST_AUTO_TEST_CASE(ExtraStateRecordingOnDiamond) {
+  DiamondGraph G;
+
+  using State = mfp::ExtraState<OperationKey, IntSet>;
+  State S;
+
+  // Mark a single point per node.
+  OperationKey EntryOp0{ "Entry", 0 };
+  OperationKey LeftOp0{ "Left", 0 };
+  OperationKey TailOp0{ "Tail", 0 };
+  S.registerAsInterestingBefore(EntryOp0);
+  S.registerAsInterestingAfter(LeftOp0);
+  S.registerAsInterestingBefore(TailOp0);
+
+  OperationsMFI MFI;
+  IntSet Bottom;
+  IntSet ExtremalValue;
+  std::vector<OperationNode *> ExtremalLabels{ G.Entry };
+
+  mfp::MFPConfiguration<OperationsMFI> Configuration{
+    .Instance = &MFI,
+    .Flow = &G.Graph,
+    .Bottom = &Bottom,
+    .ExtremalValue = &ExtremalValue,
+    .ExtremalLabels = &ExtremalLabels,
+    .ExtraState = &S
+  };
+
+  auto Result = mfp::getMaximalFixedPoint<OperationsMFI>(Configuration);
+
+  // Sanity: the fixed-point lattice values must match the diamond test above.
+  BOOST_TEST(Result.at(G.Tail).OutValue == IntSet({ 1, 2, 3, 4 }));
+
+  // The recorded values agree with the labels' InValue / partial OutValue.
+  BOOST_TEST(S.getBefore(EntryOp0) == IntSet{});
+  BOOST_TEST(S.getAfter(LeftOp0) == IntSet({ 1, 2 }));
+  BOOST_TEST(S.getBefore(TailOp0) == IntSet({ 1, 2, 3 }));
+}
diff --git a/tests/unit/RegisterUsageAnalyses.cpp b/tests/unit/RegisterUsageAnalyses.cpp
index 4c77aad5a..1447d8f54 100644
--- a/tests/unit/RegisterUsageAnalyses.cpp
+++ b/tests/unit/RegisterUsageAnalyses.cpp
@@ -128,11 +128,20 @@ createNoReturn(rua::Block::OperationsVector &&Header,
 BOOST_AUTO_TEST_CASE(LivenessTest) {
   auto RunAnalysis = [](rua::Function &Function, BlockNode *Entry) {
     Liveness LA(Function);
-    return MFP::getMaximalFixedPoint(LA,
-                                     &Function,
-                                     LA.defaultValue(),
-                                     LA.defaultValue(),
-                                     { Entry });
+    auto DefaultValue = LA.defaultValue();
+    std::vector<const BidirectionalNode<Block> *> ExtremalLabels{ Entry };
+    // Backward analysis: `getEntryNode(Inverse<...>)` is unreliable (returns
+    // the forward entry), and a single exit doesn't reach no-return blocks.
+    // Use `All` to seed RPOT from every node.
+    using InverseGT = llvm::GraphTraits<llvm::Inverse<const rua::Function *>>;
+    auto GetMaximalFixedPoint = mfp::getMaximalFixedPoint<Liveness, InverseGT>;
+    return GetMaximalFixedPoint(mfp::MFPConfiguration<Liveness>{
+      .Instance = &LA,
+      .Flow = &Function,
+      .Bottom = &DefaultValue,
+      .ExtremalValue = &DefaultValue,
+      .ExtremalLabels = &ExtremalLabels,
+      .EntryLabels = mfp::All{} });
   };
 
   auto RunOnSingleNode =
@@ -274,11 +283,19 @@ BOOST_AUTO_TEST_CASE(LivenessTest) {
 BOOST_AUTO_TEST_CASE(ReachingDefinitionsTest) {
   auto RunAnalysis = [](TestAnalysisResult &&F) {
     ReachingDefinitions RD(F.Function);
-    auto Results = MFP::getMaximalFixedPoint(RD,
-                                             &F.Function,
-                                             RD.defaultValue(),
-                                             RD.defaultValue(),
-                                             { F.Entry });
+    auto DefaultValue = RD.defaultValue();
+    std::vector ExtremalLabels{ F.Entry };
+
+    mfp::MFPConfiguration<ReachingDefinitions> Configuration{
+      .Instance = &RD,
+      .Flow = &F.Function,
+      .Bottom = &DefaultValue,
+      .ExtremalValue = &DefaultValue,
+      .ExtremalLabels = &ExtremalLabels
+    };
+
+    using namespace mfp;
+    auto Results = getMaximalFixedPoint<ReachingDefinitions>(Configuration);
     return ReachingDefinitions::compute(Results[F.Exit].OutValue,
                                         Results[F.Sink].OutValue);
   };