map_put/map_update unsound rewrite of negated BDD

[lukaszsamson]

Existing issue

• I have searched existing issues and could not find a duplicate.

Elixir and Erlang/OTP versions

Erlang/OTP 28 [erts-16.4.0.1] [source] [64-bit] [smp:12:12] [ds:12:12:10] [async-threads:1] [jit]

Interactive Elixir (1.21.0-dev)

Operating system

any

Current behavior

The following 5 repros are manifestations of the same underlying bug:

1. negated closed leaf

d = opt_difference(open_map(), empty_map())
{:ok, res} = map_put(d, atom(), atom([:x]))
to_quoted_string(res)
"map() and not %{atom() => :x}" # wrong
subtype?(closed_map(a: atom([:x])), res)
false # wrong

2. negated domains

d2 = opt_difference(open_map([{[:integer], atom()}]),
                            closed_map([{[:integer], atom([:y])}]))
{:ok, res2} = map_put(d2, integer(), atom([:y]))
x = opt_difference(closed_map([{[:integer], atom([:y])}]), empty_map())
empty?(opt_intersection(x, res2))
true # wrong

3. negated empty map

w = opt_difference(closed_map([{[:integer], atom([:z])}]), empty_map())
{:ok, pw} = map_put(w, integer(), atom([:y]))
to_quoted_string(pw)
"%{integer() => :y or :z} and not %{integer() => :y}" # wrong
empty?(pw)
false
x = opt_difference(closed_map([{[:integer], atom([:y])}]), empty_map())
empty?(opt_intersection(pw, x))
true # wrong

4. map_update path

d = opt_difference(open_map(), empty_map())
{_v, resu, _e} = map_update(d, atom(), atom([:x]), false, true)
to_quoted_string(resu)
"map() and not %{atom() => :x}" # wrong
subtype?(closed_map(a: atom([:x])), resu)
false # wrong

5. dynamic path

{:ok, resd} = map_put(dynamic(d), atom(), atom([:x]))
to_quoted_string(resd)
"dynamic(map() and not %{atom() => :x})" # wrong
subtype?(dynamic(closed_map(a: atom([:x]))), resd)
false # wrong
{_v2, resud, _e2} = map_update(dynamic(d), atom(), atom([:x]), false, true)
subtype?(dynamic(closed_map(a: atom([:x]))), resud)
false # wrong

Likely reason:

elixir/lib/elixir/lib/module/types/descr.ex

Line 3786 in 4215bbe

defp map_update_put_domains(bdd, domain_keys, type_fun, force?) do

bdd_map rewrites every leaf label, including negated ones. The comment on map_update_put_domains is not true as proven by the repros above.

For negations, we count on the idea that a negation will not remove any
type from a domain unless it completely cancels out the type.

Rewriting not(N) to not(put(N)) changes what is excluded. put(N) >= N, so not(put(N)) <= not(N). The result type can exclude reachable values even when nothing is cancelled.

Note: this is a different bug than #15507

Expected behavior

No unsound rewrite of negated BDD