Composition

Region decompositions can be composed and combined using operators within the [@@decomp ...] attribute. This lets you build complex analyses from simple building blocks.

Composition operators

|>> — Apply refiner (pipe forward)

Chain a refiner onto a decomposition result:

let d = f
[@@decomp top () |>> prune]

This runs top to produce the decomposition, then pipes the result through prune to remove infeasible regions.

<< — Merge

Substitute a function's decomposition into another. This is used when you've decomposed a function g with f in its basis (kept symbolic), and now want to merge f's own decomposition in:

let d_g_merged_f = g
[@@decomp top ~basis:[ [%id f] ] () << top () [%id f]]

This takes the decomposition of g (where f is symbolic) and substitutes in the decomposition of f, producing a fully expanded decomposition.

<|< — Compound merge

Combines merging and combining while preserving distinctions between the merged function's regions:

let d_g_compound_f = g
[@@decomp top ~basis:[ [%id f] ] () <|< top () [%id f]]

~| — Combine

Merge regions with identical invariants by creating disjunctive constraints. Wraps the entire decomposition expression:

let d_combined = g
[@@decomp ~| (top ~basis:[ [%id f] ] ())]

Building complex analyses

Composition is particularly powerful for analyzing pipelines — sequences of functions where the output of one feeds into the next.

Example: Two-stage decomposition

let validate x =
  if x < 0 then Error "negative"
  else if x > 100 then Error "too large"
  else Ok x
 
let process x =
  match validate x with
  | Error _ -> -1
  | Ok v -> v * 2

You can decompose process with validate in the basis, then merge:

let d = process
[@@decomp top ~basis:[ [%id validate] ] () << top () [%id validate]]

This reveals how each validation region maps through to the final output — without needing to analyze process as a monolithic function.

Example: Basis with pruning

let d = g
[@@decomp top ~basis:[ [%id f] ] () << top () [%id f] |>> prune]

This decomposes g symbolically over f, merges in f's decomposition, and then prunes any infeasible regions.