Skip to content

Using lazy BDD structure for functions #14799

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 8 commits into from
Closed

Using lazy BDD structure for functions #14799

Changes from 2 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
760552c
Unify fun BDD ops with the rest
gldubc Sep 29, 2025
a883888
Add lazy bdd for funs. Solves spitfire perf issue.
gldubc Sep 29, 2025
580fb13
Do not require ordering when matching statics and dynamics
josevalim Sep 30, 2025
8cd653e
Fix fun_top?
josevalim Sep 30, 2025
d57266b
Eliminate fun unions
josevalim Sep 30, 2025
4a29c67
Remove fun_eliminate_intersections
josevalim Sep 30, 2025
a58f713
Refactor bdd creation
gldubc Sep 29, 2025
3ab4ee1
Prepare for lazy BDD switch
gldubc Sep 30, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
219 changes: 122 additions & 97 deletions lib/elixir/lib/module/types/descr.ex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ defmodule Module.Types.Descr do
@bit_top (1 <<< 7) - 1
@bit_number @bit_integer ||| @bit_float

# Remark: those use AST for BDDs
defmacrop map_literal(tag, fields), do: {:{}, [], [{tag, fields}, :bdd_top, :bdd_bot]}
defmacrop tuple_literal(tag, elements), do: {:{}, [], [{tag, elements}, :bdd_top, :bdd_bot]}
defmacrop list_literal(list, last), do: {:{}, [], [{list, last}, :bdd_top, :bdd_bot]}
Expand All @@ -48,6 +49,7 @@ defmodule Module.Types.Descr do
{:domain_key, :list}
]

# Remark: those are explicit BDD constructors. The functional constructors are `bdd_new/1` and `bdd_new/3`.
@fun_top :bdd_top
@atom_top {:negation, :sets.new(version: 2)}
@map_top {{:open, %{}}, :bdd_top, :bdd_bot}
Expand Down Expand Up @@ -1090,7 +1092,7 @@ defmodule Module.Types.Descr do
# rather than unary functions with tuple domains to handle special cases like representing
# functions of a specific arity (e.g., (none,none->term) for arity 2).
# NOTE: this is a ternary (lazy) BDD where the middle node encodes unions.
defp fun_new(inputs, output), do: {{inputs, output}, :bdd_top, :bdd_bot, :bdd_bot}
defp fun_new(inputs, output), do: lazy_bdd_new({inputs, output})

# Creates a function type from a list of inputs and an output
# where the inputs and/or output may be dynamic.
Expand Down Expand Up @@ -1847,34 +1849,34 @@ defmodule Module.Types.Descr do
end
end

defp list_new(list_type, last_type) do
{{list_type, last_type}, :bdd_top, :bdd_bot}
defp list_new(list_type, last_type), do: bdd_new({list_type, last_type})

defp non_empty_list_literals_intersection(list_literals) do
try do
Enum.reduce(list_literals, {:term, :term}, fn {next_list, next_last}, {list, last} ->
{non_empty_intersection!(list, next_list), non_empty_intersection!(last, next_last)}
end)
catch
:empty -> :empty
end
end

# Takes all the lines from the root to the leaves finishing with a 1,
# and compile into tuples of positive and negative nodes. Positive nodes are
# those followed by a left path, negative nodes are those followed by a right path.
defp list_bdd_to_dnf(bdd), do: list_bdd_to_dnf([], {:term, :term}, [], bdd)

defp list_bdd_to_dnf(acc, {list_acc, tail_acc} = pos, negs, bdd) do
case bdd do
:bdd_bot ->
acc

:bdd_top ->
if list_line_empty?(list_acc, tail_acc, negs), do: acc, else: [{pos, negs} | acc]

{{list, tail} = next_list, left, right} ->
try do
li = non_empty_intersection!(list_acc, list)
la = non_empty_intersection!(tail_acc, tail)
defp list_bdd_to_dnf(bdd) do
bdd_to_dnf(bdd)
|> Enum.reduce([], fn {pos_list, neg_list}, acc ->
case non_empty_list_literals_intersection(pos_list) do
:empty ->
acc

list_bdd_to_dnf(acc, {li, la}, negs, left)
|> list_bdd_to_dnf(pos, [next_list | negs], right)
catch
:empty -> list_bdd_to_dnf(acc, pos, [next_list | negs], right)
end
end
{list, last} ->
if list_line_empty?(list, last, neg_list),
do: acc,
else: [{{list, last}, neg_list} | acc]
end
end)
end

# Takes all the lines from the root to the leaves finishing with a 1,
Expand All @@ -1884,40 +1886,51 @@ defmodule Module.Types.Descr do
# if the negative list type is a supertype of the positive list type. In that case,
# we can remove the negative last type from the positive one.
# (If this subtracted type was empty, the whole type would be empty)
defp list_bdd_to_pos_dnf(bdd), do: list_bdd_to_pos_dnf(:term, :term, bdd, [])
defp list_bdd_to_pos_dnf(bdd) do
bdd_to_dnf(bdd)
|> Enum.reduce([], fn {pos_list, neg_list}, acc ->
case non_empty_list_literals_intersection(pos_list) do
:empty ->
acc

defp list_bdd_to_pos_dnf(list_acc, last_acc, bdd, lines_acc) do
case bdd do
:bdd_bot ->
lines_acc
{list, last} ->
if list_line_empty?(list, last, neg_list), do: acc, else: [{list, last} | acc]
end
end)
end

:bdd_top ->
[{list_acc, last_acc} | lines_acc]
# defp list_bdd_to_pos_dnf(list_acc, last_acc, bdd, lines_acc) do
# case bdd do
# :bdd_bot ->
# lines_acc

{{list, last}, left, right} ->
# Case 1: count the list_type negatively. Check condition when it affects the positive one.
lines_acc =
if subtype?(list_acc, list) do
last = difference(last_acc, last)
# :bdd_top ->
# [{list_acc, last_acc} | lines_acc]

if empty?(last),
do: lines_acc,
else: list_bdd_to_pos_dnf(list_acc, last, right, lines_acc)
else
list_bdd_to_pos_dnf(list_acc, last_acc, right, lines_acc)
end
# {{list, last}, left, right} ->
# # Case 1: count the list_type negatively. Check condition when it affects the positive one.
# lines_acc =
# if subtype?(list_acc, list) do
# last = difference(last_acc, last)

# Case 2: count the list_type positively.
list_acc = intersection(list_acc, list)
last_acc = intersection(last_acc, last)
# if empty?(last),
# do: lines_acc,
# else: list_bdd_to_pos_dnf(list_acc, last, right, lines_acc)
# else
# list_bdd_to_pos_dnf(list_acc, last_acc, right, lines_acc)
# end

if empty?(list_acc) or empty?(last_acc) do
lines_acc
else
list_bdd_to_pos_dnf(list_acc, last_acc, left, lines_acc)
end
end
end
# # Case 2: count the list_type positively.
# list_acc = intersection(list_acc, list)
# last_acc = intersection(last_acc, last)

# if empty?(list_acc) or empty?(last_acc) do
# lines_acc
# else
# list_bdd_to_pos_dnf(list_acc, last_acc, left, lines_acc)
# end
# end
# end

defp list_pop_dynamic(:term), do: {false, :term}

Expand All @@ -1934,10 +1947,7 @@ defmodule Module.Types.Descr do
@compile {:inline, list_union: 2}
defp list_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2)

defp is_list_top?({{list, tail}, :bdd_top, :bdd_bot}) do
list == :term and tail == :term
end

defp is_list_top?(list_literal(list, tail)), do: list == :term and tail == :term
defp is_list_top?(_), do: false

defp list_intersection(list_literal(list1, last1), list_literal(list2, last2)) do
Expand Down Expand Up @@ -1988,16 +1998,6 @@ defmodule Module.Types.Descr do
end
end

defp non_empty_list_literals_intersection(list_literals) do
try do
Enum.reduce(list_literals, {:term, :term}, fn {next_list, next_last}, {list, last} ->
{non_empty_intersection!(list, next_list), non_empty_intersection!(last, next_last)}
end)
catch
:empty -> :empty
end
end

defp list_empty?(@non_empty_list_top), do: false

defp list_empty?(bdd) do
Expand Down Expand Up @@ -2425,7 +2425,7 @@ defmodule Module.Types.Descr do
defguardp is_optional_static(map)
when is_map(map) and is_map_key(map, :optional)

defp map_new(tag, fields = %{}), do: {{tag, fields}, :bdd_top, :bdd_bot}
defp map_new(tag, fields = %{}), do: bdd_new({tag, fields})

defp map_only?(descr), do: empty?(Map.delete(descr, :map))

Expand All @@ -2443,12 +2443,13 @@ defmodule Module.Types.Descr do

nil ->
case {{tag1, fields1}, {tag2, fields2}} do
{r, l} when l < r -> {l, :bdd_top, {r, :bdd_top, :bdd_bot}}
{l, r} -> {l, :bdd_top, {r, :bdd_top, :bdd_bot}}
{r, l} when l < r -> bdd_new(l, :bdd_top, bdd_new(r))
{l, r} -> bdd_new(l, :bdd_top, bdd_new(r))
end
end
end

@compile {:inline, map_union: 2}
def map_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
def map_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2)
defp map_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2)


defp maybe_optimize_map_union({tag1, pos1, []} = map1, {tag2, pos2, []} = map2) do
Expand Down Expand Up @@ -2549,8 +2550,8 @@ defmodule Module.Types.Descr do

defp map_intersection(map_literal(tag1, fields1), map_literal(tag2, fields2)) do
try do
map = map_literal_intersection(tag1, fields1, tag2, fields2)
{map, :bdd_top, :bdd_bot}
map_literal = map_literal_intersection(tag1, fields1, tag2, fields2)
bdd_new(map_literal)
catch
:empty -> :bdd_bot
end
Expand Down Expand Up @@ -2762,7 +2763,7 @@ defmodule Module.Types.Descr do

# Optimization: if the key does not exist in the map, avoid building
# if_set/not_set pairs and return the popped value directly.
defp map_fetch_static(%{map: {{tag_or_domains, fields}, :bdd_top, :bdd_bot}}, key)
defp map_fetch_static(%{map: map_literal(tag_or_domains, fields)}, key)
when not is_map_key(fields, key) do
map_key_tag_to_type(tag_or_domains) |> pop_optional_static()
end
Expand Down Expand Up @@ -2936,8 +2937,8 @@ defmodule Module.Types.Descr do
end
end

def map_refresh_domain(%{map: {{tag, fields}, :bdd_top, :bdd_bot}}, domain, type) do
%{map: {{map_refresh_tag(tag, domain, type), fields}, :bdd_top, :bdd_bot}}
def map_refresh_domain(%{map: map_literal(tag, fields)}, domain, type) do
%{map: bdd_new({map_refresh_tag(tag, domain, type), fields})}
end

def map_refresh_domain(%{map: bdd}, domain, type) do
Expand Down Expand Up @@ -3305,7 +3306,7 @@ defmodule Module.Types.Descr do

# Takes a static map type and removes a key from it.
# This allows the key to be put or deleted later on.
defp map_take_static(%{map: {{tag, fields}, :bdd_top, :bdd_bot}} = descr, key, initial)
defp map_take_static(%{map: map_literal(tag, fields)} = descr, key, initial)
when not is_map_key(fields, key) do
case tag do
:open -> {true, maybe_union(initial, fn -> term() end), descr}
Expand Down Expand Up @@ -4026,6 +4027,7 @@ defmodule Module.Types.Descr do
end
end

@compile {:inline, tuple_union: 2}
defp tuple_union(bdd1, bdd2), do: bdd_union(bdd1, bdd2)

defp maybe_optimize_tuple_union({tag1, pos1} = tuple1, {tag2, pos2} = tuple2) do
Expand Down Expand Up @@ -4122,30 +4124,21 @@ defmodule Module.Types.Descr do

# Transforms a bdd into a union of tuples with no negations.
# Note: it is important to compose the results with tuple_dnf_union/2 to avoid duplicates
defp tuple_normalize(bdd), do: tuple_normalize([], {:open, []}, [], bdd)

defp tuple_normalize(acc, {tag, elements} = tuple, negs, bdd) do
case bdd do
:bdd_bot ->
acc

:bdd_top ->
if tuple_line_empty?(tag, elements, negs) do
defp tuple_normalize(bdd) do
bdd_to_dnf(bdd)
|> Enum.reduce([], fn {positive_tuples, negative_tuples}, acc ->
case non_empty_tuple_literals_intersection(positive_tuples) do
:empty ->
acc
else
tuple_eliminate_negations(tag, elements, negs) |> tuple_dnf_union(acc)
end

{{next_tag, next_elements} = next_tuple, left, right} ->
# If an intersection of tuples is empty, the line is empty and we skip it.
acc =
case tuple_literal_intersection(tag, elements, next_tag, next_elements) do
:empty -> acc
new_tuple -> tuple_normalize(acc, new_tuple, negs, left)
{tag, elements} ->
if tuple_line_empty?(tag, elements, negative_tuples) do
acc
else
tuple_eliminate_negations(tag, elements, negative_tuples) |> tuple_dnf_union(acc)
end

tuple_normalize(acc, tuple, [next_tuple | negs], right)
end
end
end)
end

# Given a union of tuples, fuses the tuple unions when possible,
Expand Down Expand Up @@ -4470,6 +4463,19 @@ defmodule Module.Types.Descr do

## BDD helpers

# defp bdd_new(literal), do: lazy_bdd_new(literal)
# defp bdd_new(literal, left, right), do: lazy_bdd_new(literal, left, right)

# defp bdd_intersection(bdd1, bdd2), do: lazy_bdd_intersection(bdd1, bdd2)
# defp bdd_difference(bdd1, bdd2), do: lazy_bdd_difference(bdd1, bdd2)
# defp bdd_union(bdd1, bdd2), do: lazy_bdd_union(bdd1, bdd2)
# defp bdd_negation(bdd), do: lazy_bdd_negation(bdd)
# defp bdd_map(bdd, fun), do: lazy_bdd_map(bdd, fun)
# defp bdd_to_dnf(bdd), do: lazy_bdd_to_dnf(bdd)

defp bdd_new(literal), do: {literal, :bdd_top, :bdd_bot}
defp bdd_new(literal, left, right), do: {literal, left, right}

# Leaf cases
defp bdd_intersection(_, :bdd_bot), do: :bdd_bot
defp bdd_intersection(:bdd_bot, _), do: :bdd_bot
Expand Down Expand Up @@ -4544,6 +4550,10 @@ defmodule Module.Types.Descr do
end
end

## Lazy BDD helpers
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
## Lazy BDD helpers
## Lazy BDD helpers
@compile {:inline, lazy_bdd_new: 1, lazy_bdd_new: 3}

defp lazy_bdd_new(literal), do: {literal, :bdd_top, :bdd_bot, :bdd_bot}
defp lazy_bdd_new(literal, left, right), do: {literal, left, :bdd_bot, right}

def lazy_bdd_union(bdd1, bdd2) do
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Remember to make all of them private :)

case {bdd1, bdd2} do
{:bdd_top, _bdd} ->
Expand Down Expand Up @@ -4650,8 +4660,23 @@ defmodule Module.Types.Descr do
end

# Optional guard: blow up if someone passes a binary node by mistake
defp lazy_bdd_to_dnf(_acc, _pos, _neg, {_lit, _t, _e}) do
raise ArgumentError, "lazy_bdd_to_dnf expects lazy nodes {lit, c, u, d}"
defp lazy_bdd_to_dnf(_acc, _pos, _neg, {_lit, _t, _e} = node) do
raise ArgumentError,
"lazy_bdd_to_dnf expects lazy nodes {lit, c, u, d} #{inspect(node)}\n
#{inspect(Process.info(self(), :current_stacktrace))}"
end

defp lazy_bdd_map(bdd, fun) do
case bdd do
:bdd_bot ->
:bdd_bot

:bdd_top ->
:bdd_top

{literal, left, union, right} ->
{fun.(literal), bdd_map(left, fun), bdd_map(union, fun), bdd_map(right, fun)}
end
end

## Pairs
Expand Down