Summary: Some more tests to make sure we consider the size of tuples when pattern matching.
Reviewed By: mmarescotti
Differential Revision: D30132889
fbshipit-source-id: 74ae4d1a1
Summary: Report `badrecord` errors with Pulse when trying to access or update a record with a wrong name.
Reviewed By: rgrig
Differential Revision: D30068424
fbshipit-source-id: b88abb7ca
Summary:
Add support for Erlang records, including:
- Parsing record definitions, storing info in environment
- Record index expressions and patterns
- Record creation expression, including initializers
- Record update expressions and patterns
- Record field access expressions
- Pulse models
The key idea is to translate records to tagged tuples (just as Erlang does under the hood), but this requires some bookkeeping to figure out which field maps to which tuple element.
Reviewed By: rgrig
Differential Revision: D29991819
fbshipit-source-id: a1c713b41
Summary: Add support for tuples, including expressions, pattern matching and pulse models. Tuples are modeled similarly to `Cons` (lists): they have a dynamic type (including the size of the tuple) and elements as fields.
Reviewed By: mmarescotti
Differential Revision: D29875650
fbshipit-source-id: f0262a42c
Summary: Add some tests for lists: nil, cons, and some basic pattern matching. We can extend this suite later with more features on lists (e.g. concatenation).
Reviewed By: skcho
Differential Revision: D29844279
fbshipit-source-id: 62c8b92c3
Summary: Add support for the xor operator by reducing `(X xor Y)` to `(X and not Y) or (not X and Y)`. Alternatively, `(X != Y)` could have been used but that might not be safe since SIL models Booleans with integers.
Reviewed By: skcho
Differential Revision: D29816793
fbshipit-source-id: 2496b718b
Summary: Add support for short circuit counterparts (andalso, orelse) of the logic operators (and, or).
Reviewed By: skcho
Differential Revision: D29815177
fbshipit-source-id: 98d28deed
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: Add support for *unary minus* and *logical not* in the Erlang translation, both as expression (e.g., `X = -Y`) and pattern (e.g., `case X of -3 -> ...`).
Reviewed By: rgrig
Differential Revision: D29582176
fbshipit-source-id: 17ef89496
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 tests for binary expressions. The idea is that tests come in pairs: in both cases we do the same calculations, one is asserting the good result and one is not, where only the latter should trigger a warning.
Reviewed By: rgrig
Differential Revision: D29556364
fbshipit-source-id: 5b601d141
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:
Topl matches procedure names against whatever Procname.hashable_name
returns. For Java, it returns something like "java.util.ArrayList.add(...)",
but for Erlang it used to return something like "add/1": no module and
no parenthesis after. Now, Erlang returns "lists:add/1"; that is, it
includes module name. Also, Topl doesn't insist anymore on having a
paranthesis after the name.
Differential Revision: D29520365
fbshipit-source-id: d23be1cc8
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