Summary:
This diff lifts the Prop.Attribute module out of Prop. This required
moving several Prop functions that depend on Attribute
(find_arithmetic_problem, deallocate_stack_vars, find_equal_formal_path)
and adding numerous calls to Prop.normalize to fix normal/exposed
mismatches. Also note that the type of Prop.normalize is generalized to
allow calling it on normalized props.
Reviewed By: cristianoc
Differential Revision: D3684523
fbshipit-source-id: f37af8b
Summary:
Enable warning 23 (Useless record with clause), make fatal, and fix the
existing instance.
Reviewed By: sblackshear
Differential Revision: D3685950
fbshipit-source-id: 8ee415d
Summary:
Move the Sil.attribute type and associated types and operations to a new
PredSymb module.
Reviewed By: cristianoc
Differential Revision: D3683834
fbshipit-source-id: d3606a8
Summary:
Change the Aobjc_null attribute from a family of unary predicates, one
for each Pvar.t * Ident.fieldname list, to a single binary predicate.
This diff should not change behavior except for printing of Aobjc_null
attributes. Also, operations such as free variables, etc. should now
behave correctly with respect to variables occurring in the arguments of
Aobjc_null.
Reviewed By: cristianoc
Differential Revision: D3669392
fbshipit-source-id: fe4434a
Summary:
Add support for nary predicates, not just unary ones. Many operations
don't make much sense for nullary predicates, and are generally treated
as no-ops. The first argument is treated specially, as the "anchor" of
the predicate application. For example, adding or removing an attribute
uses the anchor to identify the atom to operate on. Also, abstraction
and normalization operations treat the anchor specially.
Reviewed By: cristianoc
Differential Revision: D3669391
fbshipit-source-id: 3d142ea
Summary:
There is no need to call exp_normalize on the sub-expressions of
arguments to atom_normalize, as it calls exp_normalize on its
sub-expressions.
Reviewed By: cristianoc
Differential Revision: D3669390
fbshipit-source-id: 468b6b1
Summary:
Simplify the (implementation and) interface of Prop by using the atom
type directly instead of a tuple type that duplicates the fields.
This change does not weaken the type guarantees, while reducing
redundancy between types thereby making future changes easier.
Reviewed By: cristianoc
Differential Revision: D3669388
fbshipit-source-id: 65f7493
Summary:
Change representation of pure predicate applications to distinguish
between positive and negative literals using the Apred and Anpred
constructors instead of a boolean field.
This representation is more compact, and is uniform with the treatment
of equalities and disequalities. Some code is simpler, but there isn't
much in it.
Reviewed By: cristianoc
Differential Revision: D3669387
fbshipit-source-id: 07cdea6
Summary:
Treat attributes as unary predicates in classical first-order logic.
This diff extends predicates with a polarity and uses classical 2-valued
semantics. This potentially changes the behavior of negating
attributes, which was not previously relied on.
Reviewed By: sblackshear
Differential Revision: D3669365
fbshipit-source-id: 2f26776
Summary:
Replace disequalities to Attribute expressions with predicate symbol
application pure atomic formulas.
This diff should preserve existing behavior, up to the comparison order
of attribute disequalities versus predicate applications.
Reviewed By: sblackshear
Differential Revision: D3647049
fbshipit-source-id: c39a901
Summary:
Cosmetic changes to comments to improve the results of the Reason
comment attachment logic.
These were found using `git grep -nH -e 'in[ ]*(\*'` although the
attachment logic seems ok if the associated `let` is on the same line.
Some others were found with `git grep -nH -e ')[ ]*(\*'` although the
attachment logic seems ok if the associated `(` is on the same line.
Reviewed By: jvillard
Differential Revision: D3654027
fbshipit-source-id: 122aa3b
Summary:
Make checks context-aware, to increase flexibility.
As an example application of this change, whenever an atomic property is accessed from within a synchronized block, skip reporting a `DIRECT_ATOMIC_PROPERTY_ACCESS` warning.
Reviewed By: jvillard
Differential Revision: D3648831
fbshipit-source-id: c033f45
Summary: Follow up D3579581. We forget about memory acquired in resources with assumption that developers use raii and free memory in destructors.
Reviewed By: jvillard
Differential Revision: D3614056
fbshipit-source-id: 08fa112
Summary:
This is needed on osx, where one of {`Sys.executable_name`, `Unix.readlink`}
does not behave the same as Linux.
Reviewed By: jberdine
Differential Revision: D3614254
fbshipit-source-id: a376636
Summary:
Previously, we would translate `throw` with `return`. However, `throw` in
ObjC/C++ is often used to mean "abort". We now translate `throw` the same as
`exit` to prune these paths.
Reviewed By: akotulski
Differential Revision: D3594156
fbshipit-source-id: 81083bb
Summary:
Minor stuff:
- GCCAst -> GCCAsm
- separate constants and mutable global state in cFrontend_config
- alphabetical ordering in cFrontend_config
Reviewed By: akotulski
Differential Revision: D3593858
fbshipit-source-id: 6f4d9c3
Summary:
No longer allow pointer types to be passed inside var_exp_typ. We used to accept both forms,
but it won't be possible any longer once shared_ptr becomes pointer type.
Reviewed By: dulmarod
Differential Revision: D3593003
fbshipit-source-id: a830914
Summary:
1. Attempt to simplify callExpr_trans by merging multiple if-else branches into one in `CTrans_utils.builtin_trans`. Not every special case works that way, so some of them are still there.
2. On top of that, make type of parameters in `CTrans_models` functions `Procname.t` instead `Procname.t option`. This triggered some more changes to `callExpr_trans`.
3. Semi-randomly reorder instructions in `callExpr_trans`
This is mainly an attempt to clean up the code so any suggestions how to make it better are welcome.
Reviewed By: jvillard
Differential Revision: D3586419
fbshipit-source-id: aef8580
Summary:
Python needs to know about these because it does different things depending on
whether these flags are passed or not.
Reviewed By: cristianoc
Differential Revision: D3593381
fbshipit-source-id: fe3194d
Summary:
Since clang -### can silently return nothing when passed bogus arguments (eg,
trying to compile a non-existent file), run the original command in that case
in case it's a genuine error. This prevents puzzling behaviours such as
`infer -- clang -c bogus_file.c` succeeding with 0 files analyzed.
Reviewed By: martinoluca
Differential Revision: D3592924
fbshipit-source-id: 5d8bc81
Summary:
Store more information inside Procname.objc_cpp type: replace mangling info
with "kind" info, which also contains mangling info when appropriate.
Reviewed By: akotulski
Differential Revision: D3580283
fbshipit-source-id: b1197ed
Summary: ClassTemplateSpecializationDecl now contains structures information about the specialization
Reviewed By: jvillard
Differential Revision: D3586446
fbshipit-source-id: d567a0b
Summary:
Use Itanium mangling for C++ functions/methods instead of raw type name. This is a step towards removing expensive `ti_raw` field from `type_info`.
For virtual methods, use mangled name of the method from base class in order for dynamic dispatch to work.
Reviewed By: dulmarod
Differential Revision: D3556118
fbshipit-source-id: e45edb5
Summary:
Class names fragile, easy to break and they introduce another level of indirection.
Since C++ translation doesn't need names, pass decl pointers everywhere.
Doing otherwise will most likely result in assert false.
Handling of class names in objc translation is more involving and it's left
for now. Later, objc can use same mechanism as C++.
Reviewed By: dulmarod
Differential Revision: D3570176
fbshipit-source-id: b957aba
Summary:
When analyzing C model in C++, we were seeing some SKIP function triggered by generated constructors/operators= for C structs.
In C they weren't present, but in C++ compiler generates them for us. To avoid this (and future) problems
with models, translate all functions that are needed when computing the model
Reviewed By: dulmarod
Differential Revision: D3561873
fbshipit-source-id: f8ad2a0
Summary:
Generation of the module dependency graph was broken (all IR modules
were omitted) by the reason conversion.
Reviewed By: cristianoc
Differential Revision: D3541395
fbshipit-source-id: e5af125
Summary: Move Sil.dexp type and operations into separate DecompExp module.
Reviewed By: dulmarod
Differential Revision: D3548095
fbshipit-source-id: 5ab4360
Summary:
Move Sil.call_flags type and operations into separate CallFlags
module.
Reviewed By: dulmarod
Differential Revision: D3548086
fbshipit-source-id: 6d264e9
Josh Berdine
Martino Luca
Lázaro Clapp Jiménez Labora
Sam Blackshear
Vaibhav Tulsyan
Ryan Rhee
Jules Villard
Zac Sweers
Dulma Churchill
Daiva Naudziuniene
Andrzej Kotulski