Summary: Previously we just reported NONEXHAUSTIVE_PATTERN_MATCH, which was (1) not correct because not only patterns can cause nonexhaustive behavior, but also guards, and (2) the Erlang runtime reports errors more precisely, indicating whether the nonexhaustive behavior occurs with `if`, `case`, functions or match expressions.
Reviewed By: rgrig
Differential Revision: D29681637
fbshipit-source-id: 74a25b371
Summary:
This fixes a bug that caused imprecise tracking of dynamic types.
Suppose we knew
term_eqs:
(x instanceof T)=v1
(y instanceof T)=v2
0=v2
attrs:
x has DynamicType T
y has DynamicType T
The simplification used to produce
term_eqs:
1=v1
0=v2
That's because term_eqs is a map and 1 can appear at most once as a key.
Note that the missing fact (1=v2) contradicts (0=v2). The imprecision
came from not noticing such contradictions. Most of these imprecisions
were observed in Erlang tests.
The fix is to go from using Term.VarMap to the smarter functions in
PulseFormula.Normalizer.
Reviewed By: jvillard
Differential Revision: D29541209
fbshipit-source-id: e4e077c87
Summary: Add support for guards, both in function clauses and case clauses.
Reviewed By: rgrig
Differential Revision: D29634937
fbshipit-source-id: 5a9f8ec2d
Summary: Group tests based on the different constructs: functions, case expressions and match expressions.
Reviewed By: rgrig
Differential Revision: D29559982
fbshipit-source-id: eb645ed8d
Summary: Add some test cases to potentially non-exhaustive case clauses.
Reviewed By: rgrig
Differential Revision: D29555525
fbshipit-source-id: f710e93e6
Summary: If a test function `F` has multiple calls to a possibly problematic function `G`, our current expected output does not tell exactly which call to `G` causes the problem. This diff splits up such functions `F` into smaller parts `F1`, `F2`, ..., so that each part only calls `G` once. This way our expected output can match more precisely.
Reviewed By: rgrig
Differential Revision: D29554848
fbshipit-source-id: bdc62731c
Summary:
The gist of this diff is a set of Pulse models for the built-ins
that have been put in Sil by the Erlang frontend:
- __erlang_make_nil, for creating an empty list like []
- __erlang_make_cons, for creating a nonempty list like [1|[]]
- __erlang_pattern_fail, which marks that no pattern matched
The models for the first two update the abstract state. The model for
the third generates a reportable error.
The diff also includes a test.
And also a few bugfixes:
- a type ErlangAny was used sometimes instead of ErlangAny*
- a load that was meant to be n=13 was instead n=*13;
changed to (*tmp=13; n=*tmp)
- the Makefile's guard for the rebar build-system test was inside the large
guard for java analyzers; of course, we don't need java to run rebar
Reviewed By: jvillard
Differential Revision: D29230161
fbshipit-source-id: c8fd6d88a
Akos Hajdu
Radu Grigore