Prisma's discrepancy analyzer against Dialyzer

How often the discrepancy analyzer (mode => discrepancy, success typing) is right, how it compares with Dialyzer inside the same category of warning, and what that costs in time, CPU and memory. Corpus: RabbitMQ. Harness: bench/.

The gradual (-spec contract) and oxbow checks are a different analyzer with different tools to compare against; they appear here only where they change the cost of the discrepancy analysis (section 6) or explain a number.

1. Summary

Three things to keep in mind when reading it:

• RabbitMQ runs Dialyzer in its own CI, so zero warnings from Dialyzer is the expected answer. Every warning Prisma gives there is a false positive or something Dialyzer cannot see. The first run gave 51 and 44 of them were false positives; the work below is what took them to zero.
• The correctness work cost speed. Over the same code the analysis is 55% slower than at the start (0.71 s to 1.08 s, user CPU +60%, memory +1% to +11%), and no feature was added that Dialyzer lacks to explain it: it is the price of looking inside more constructs and of trusting declared -specs (section 6).
• Everything is one corpus on one machine. A second corpus (Elixir, a different style of Erlang) has not been measured.

2. Method and environment

Tools are only compared inside a category. prisma check mixes four kinds of warning (discrepancy, gradual contract, dead code, oxbow) and Dialyzer reports the first plus some dead code, so the full counts of the two are not comparable. bench/adapters.py normalizes each tool's output.

3. Correctness

3.1 What each tool says

At the start (same corpus, same mode) the numbers were 51 and 101. Dead code is a warning in Prisma's levels (certain, but it does not fail when the code runs), so in discrepancy mode these are 0 errors and 5 and 45 warnings; the errors are the discrepancies and the missing functions.

3.2 The false positives, how each was found, and the fix

Every false positive has a minimal reproduction in bench/repro/ and a test.

One false positive remains known: rabbit_ff_controller:run_callback/5, whose -spec is overloaded by the value of Command. Its code is right, but the return fits neither overload alone; telling it needs the correlation between the parameter and the spec's clause, which Prisma does not follow.

3.3 The true warnings: wrong specs

Each was read against the source, its callers and its docs. None is a bug in the code; they are -specs that contradict a clause that does run.

Dialyzer confirms five of these only with -Woverspecs / -Wunderspecs, buried in 942 spec-difference warnings for rabbit and 2,229 for the 440 modules; its default warnings give none. Prisma reports exactly the cases where a spec contradicts a clause. The lists are not subsets of each other.

3.4 Property-based tests (PropEr)

The oracle is semantic, so no human triage is needed. rebar3 proper, 10 properties, all passing.

• Type algebra (test/prop_prisma_type.erl): member(Term, Type) decides whether a concrete term belongs to a ground type, generators build terms of a type. Subtyping is reflexive and sound, widening is accepted, join is an upper bound, meet is sound and keeps common values, union normalization keeps members and is idempotent. One limit by design: the type language has no non-empty improper list, so the meet of improper_list(E, T) with a nonempty_list is a safe superset.
• Inference and warnings against execution (test/prop_prisma_infer.erl): PropEr generates small well-typed modules (bindings, case, integers, floats, booleans, atoms, pairs, lists, [H | T] cells, overloaded specs, calls from a plain body, a fun, a comprehension, a record field and a try), compiles and runs them on 25 samples. The arguments and result must be inside the inferred types, and no discrepancy or dead_code warning may point at a line that ran without crashing: a line that ran refutes a warning that says "this fails". It passes 1,500 programs x 25 runs. Against the sources before each fix it fails (7 to 388 cases), so it does not pass because it went blind.
• A property is as good as what it generates. Every real finding the generator missed became a production in it: floats and ==, comparisons with 0, guards joined by orelse, record patterns in heads, callers and callees with specs.
• Self-analysis: a test analyzes Prisma's own beams and requires 0 warnings. It caught three false positives that the generators did not.

3.5 False negatives: mutation testing

bench/mutate.escript injects one fault in the abstract code of a compiled module (keeping every line number); bench/run_mutants.py puts the mutant in a copy of the application's ebin, runs the tools, and counts a fault as detected when the tool gives, inside the mutated function, a warning it did not give for the unmodified directory (keyed by module, line, kind and, for Prisma, the type found). erlc is counted only for warnings that say the code fails.

Sample: seed 1, up to 25 mutants per operator over ra, khepri, cuttlefish, cowlib and ranch (144 modules): 125 mutants.

Prisma alone sees two that Dialyzer does not (a call in the generated conf_parse, a byte_size in cow_qpack); Dialyzer alone sees none.

Four of the 125 are warnings, not errors. Four r4 mutants (a call to a function that does not exist, in ra_log, ra_server, ra_file and ra_server_proc) are inside the log macros of ra, which expand to a try ... catch _:_: the code does not crash, but the line of log is never written. Prisma lists them as handled_undef with the level warning (it would hide a misspelled function for good); --no-warnings leaves them out, and then 121 of the 125 are reported.

At the start Prisma missed most of what Dialyzer found, and the misses followed one thing: where the fault is. Four gaps, closed one at a time (reproductions in bench/repro/false_negatives/); the same 125 mutants after each:

The last miss was not Prisma's. cuttlefish_unit:generate_config/3 already had a true warning on the line of its return in the unmodified code ({error, atom(), any()} is not [any()]); the mutation changed the type to mutant_atom and Prisma said so, on the same line and of the same kind, so a comparison on (module, line, kind) took it for the old one.

A failure is reported where it is and only there. Dialyzer names every function above the faulty one ("no local return"), without saying why. Prisma must not copy that: callers trust the declared -spec of a callee over what was inferred from its body. Measured on the 125 mutants, the new warnings outside the mutated function are 0 for Prisma and 201 for Dialyzer (they were 6 for Prisma before gap 4). A unit test covers a fault three calls deep, with specs on the callers and calls from a fun, a try and a comprehension.

What the sample does not say: 125 mutants of five kinds injected on purpose are not the distribution of real bugs; "must fail" is by contract or by BIF, so a mutant on code that is never reached still counts; and Dialyzer ran with its default warnings and the erts/kernel/stdlib PLT. The first version of the runner looked for warnings between the first and last line of the function and missed Dialyzer's invalid-spec warnings, which sit on the -spec line; it was caught by looking at the mutants one by one before the big batch.

3.6 Precision lost, and limits

• hd([]) is no longer reported: the type has no "non-empty improper list" to tell it from hd([1 | 2]) (the compiler already warns about it). In exchange tl(X) + 1 is no longer a false badarith.

• Two rabbit_vhost_limit clauses ({ok, Limit} when Limit < 0, dead on purpose) are no longer reported: seeing them needs "a float that is not negative", which the type language lacks. The sound answer is "cannot tell".
• What a fun, try, receive or comprehension binds does not reach the code after it (patterns inside bind to any, the result is any): faults that depend on those values are missed.
• The exact meet of two improper lists with list-able tails is cut at depth 2 and then a safe superset (without the cut the PPLT of OTP's compiler took minutes).
• In the gradual check, a value known only by a wide type (integer(), number(), [T]) against a narrower contract (non_neg_integer(), pos_integer(), [T, ...]) is a gap in what is proven, not a contradiction, and is not reported (prisma_checker:accepts/2). Literals, floats, atoms, [] for a non-empty list and N - 1 with N :: pos_integer() for pos_integer() still are.

4. Where Prisma and Dialyzer differ

5. Benchmark

All figures: hyperfine 2.0.0 --metrics all --ignore-failure, mean of the runs, other applications running on the machine (variance in the tables).

hyperfine --metrics all --runs 5 --warmup 1 --ignore-failure \
  -n "Prisma (discrepancy)" "prisma check --mode discrepancy --no-oxbow /path/to/deps/rabbit/ebin" \
  -n "Dialyzer"             "dialyzer --no_check_plt /path/to/deps/rabbit/ebin"

rabbit (234 modules)

440 modules (7 applications)

Cold start

Dialyzer needs a PLT of the OTP base applications before it can check anything (dialyzer --build_plt --apps erts kernel stdlib): 13.2 s, 44.7 s of CPU, 768 MiB on this machine. Prisma builds the .pplt of a package once per version and loads it on demand.

The cache is not free (it adds about 0.4 s) and it changes the result: the extra 44 warnings are calls into the dependencies, checked against their real specs. The "no cold start" of Prisma is only true when dependencies are not analyzed. Dialyzer was run without the PLT of the dependencies, as above; a run with a full PLT is pending.

The PPLT of OTP's kernel and stdlib (202 modules, 1.1 MB): 2.4 s, 419 MiB. It did not end in 5 minutes before the fix below: calendar, uri_string, file_sorter and dist_util made the inference ask for meets of unions of nested improper lists that grew without end (the 100 modules of stdlib had taken 3 min 34 s once).

6. What the correctness work cost

Same corpus, same machine and harness (rabbit, discrepancy mode, 5 runs), start of the correctness work (14226fd) against now:

The analysis is slower because it does more (it looks inside fun, try, receive and comprehensions, trusts declared specs, subtracts patterns in every case, bounds types with widen/1); the PPLT is smaller because it no longer keeps the abstract code of each function.

A performance mistake, how it was found, and what changed. The fix for improper cells made the inferred type of some recursive functions grow with every pass of the inference. It was missed because the measurement was check on deps/rabbit and the PPLT of OTP's compiler, not the PPLT of RabbitMQ's dependencies: building that one went from 3.9 s to 235 s and the operating system killed the process for its memory. A bisection found one module (rabbit_binary_parser) at 48,900 million words once written out from 9,000 in memory, a factor of 113,000: Erlang shares equal sub-terms in memory, and term_to_binary and any recursion over the type expand them as if it were a tree. Fixes: the members of a union of proper lists make one nonempty_list (a cons distributed over K clauses gave K, K², K³ members); inferred types are bounded by prisma_type:widen/1 (nesting beyond four levels, and unions of more than 16 members, become any; flat literals up to 1,024); the .pplt no longer stores func_contract.clauses; normalize_union/1 has shortcuts for the lists of one or two types it nearly always gets. Written out and in memory now match on the 440 modules (10 / 10 million words, factor 1.0).

Optimizations tried since, with measurements:

The profile (fprof on rabbit_common, own time): prisma_infer 26%, erl_parse 19% before the change above, lists 17%, prisma_type 13%, maps 9.5%.

7. Not yet measured, and what is left

• Gradual contract mismatches (92 on rabbit, 221 on the 440 modules) against Gradualizer and Eqwalizer (tasks #12 and #17). Of the 55 that the return-type-from-spec change added to the hybrid mode, all were read: 40 are true by contract (the spec says less than the code), 14 are no longer reported, 1 is the known false positive above.
• Oxbow (80 on rabbit) against xref's unused locals: xref reports 0 because the compiler already warns on them, so most of the 80 are "ignored parameter" findings with no counterpart.
• Dialyzer with a full PLT of the dependencies: this run lacks it, so Dialyzer sees fewer calls.
• A second corpus, to know whether the 5 / 45 warnings and 125 / 125 mutants generalize.
• Speed: the correctness work made the analysis 55% slower; the dependency tracking of the passes took back part of it (rabbit 1.10 s to 0.95 s; the start was 0.71 s).