Summary:
This is the basic building blocks for the future annotation graph. This
diff introduces the first abstraction to be iterated on.
Reviewed By: artempyanykh
Differential Revision: D24621414
fbshipit-source-id: 19acdf216
Summary:
Before we were creating a fresh internal value when we were constructing `folly::Optional`. This diff models `folly::Optional` constructor more precisely by copying the given value.
There was also a missing dereference in the model of `value_or`
Reviewed By: jvillard
Differential Revision: D24621016
fbshipit-source-id: c86d3c157
Summary:
The global type environment is loaded in all analysis workers, so it is best to minimise its memory footprint. `MaxSharing` does a great job at this but
- it is very slow
- it may be involved in observed segfaults, since it uses potentially unsafe operations
This diff replaces `MaxSharing` with a post-facto poor-man's hashcons pass through the parts involved in a java type environment. It is not as efficient as `MaxSharing` at reducing footprint, but it's much faster.
Reviewed By: jberdine
Differential Revision: D24590400
fbshipit-source-id: c37100325
Summary:
Namely `enumerateObjectsUsingBlock` which takes a collection and a block as an arg and the iterates over the collection and applies the block to each element of the collection.
This is a common way to iterate over Objc collections, so let's add a model for it.
Reviewed By: skcho
Differential Revision: D24604590
fbshipit-source-id: 1ceeb4b40
Summary:
The autorelease pool size checker increases the size when an non-arc-compiled function calls
arc-compiled function. However, if the callee is declared in arc-compiled code and its body is not
actually captured or compiled, we should not increase the autorelease pool size.
Reviewed By: ezgicicek
Differential Revision: D24569661
fbshipit-source-id: 2fd707096
Summary:
This diff revises the translation of message expression's arguments in ObjC frontend. In the
frontend, it massages the arguments when calling a static method, so the class or object value is
not given to the static method as the first parameter.
The problem is that it used a raise-exception-and-catch way to detect where we remove the first
parameter. This way of using an exception is not only hard to understand, but also incorrectly
removed the first parameter, with breaking abstract semantics sometimes. (See the added test.) This diff
avoids using the exception.
Reviewed By: jvillard
Differential Revision: D24565513
fbshipit-source-id: 0a84ca394
Summary:
Apply normalization to conditional terms similar to conditional
formulas: evaluate terms with literal conditions, equal branches, and
ensure the condition is not negative.
Reviewed By: jvillard
Differential Revision: D24532344
fbshipit-source-id: 7818dc496
Summary:
Operations over the core representation are more useful in the core
representation modules.
Reviewed By: ngorogiannis
Differential Revision: D24532340
fbshipit-source-id: f1eab822d
Summary:
The Fol.Term and Fol.Formula provide an interface which supports
if-then-else terms and formulas, while the underlying representation
in Trm does not and Fml only supports if-then-else over formulas, not
terms. The implementation of the rest of the first-order solver needs
to use the underlying, normalized, representation. This diff exports
Trm and Fml to separate modules for this purpose. Later, they will be
packed into a library for the first-order solver, and only used from
within.
Reviewed By: ngorogiannis
Differential Revision: D24532351
fbshipit-source-id: 7310827da
Summary:
And add Monad.Make to implement the full interface from return and
bind.
Reviewed By: ngorogiannis
Differential Revision: D24532341
fbshipit-source-id: 5740ba1c2
Summary:
The `make clean` did not remove objects and dot files, so
```
infer/tests/codetoanalyze/objc/frontend$ make test
infer/tests/codetoanalyze/objc/frontend$ make clean
infer/tests/codetoanalyze/objc/frontend$ make test
```
the second `make test` did nothing. This diff adds additional regular
expressions to clean all objects and dot files generated.
Reviewed By: ngorogiannis
Differential Revision: D24566169
fbshipit-source-id: b8c50c922
Summary: This diff fixes on-demand symbolic value generation of a class that inherits NSEnumerator.
Reviewed By: ngorogiannis
Differential Revision: D24504955
fbshipit-source-id: bcb20e8aa
Summary:
This diff replaces overridden method calls in ObjC when possible, ie the first parameter of the
method has a sub-class type of the method's class. For example,
when `MyEnumerator` is a sub-class of `NSEnumerator` and there is overridden `nextObject`,
```
[my_enumerator nextObject]
```
in Sil, it was translated to like
```
NSEnumerator.nextObject(my_enumerator : MyEnumerator*)
```
and the analyzer missed the overridden method. This diff replaces the function call to
```
MyEnumerator.nextObject(my_enumerator : MyEnumerator*)
```
Reviewed By: ezgicicek
Differential Revision: D24477290
fbshipit-source-id: 6842a76f8
Summary: Model `folly::Optional::value_or(default)` to return value if not-empty and `default` if empty.
Reviewed By: jvillard
Differential Revision: D24539456
fbshipit-source-id: cc9e176cc
Summary:
The iterator is simpler to define and all the traversals are then
available through Iter.
Reviewed By: jvillard
Differential Revision: D24401743
fbshipit-source-id: 81f0653d9
Summary:
It is redundant to include the unit of conjunction in conjunction
formulas (resp., disjunction).
Reviewed By: jvillard
Differential Revision: D24371084
fbshipit-source-id: 6edc151e5
Summary: Simplify output of arithmetic terms, and omit trivial pure part of Sh.
Reviewed By: jvillard
Differential Revision: D24371082
fbshipit-source-id: 91f2117d3
Summary:
Normalization of literal formulas is determined by their term
arguments. Logically, this is part of the theories, so move this code
out of the Propositional module which is theory-independent and into
Fol, which is theory-sensitive.
Reviewed By: jvillard
Differential Revision: D24371081
fbshipit-source-id: f80a19ab8
Summary:
Change the type of `fold` functions to enable them to compose
better. The guiding reasoning behind using types such as:
```
val fold : 'a t -> 's -> f:('a -> 's -> 's) -> 's
```
is:
1. The function argument should be labeled. This is so that it can be
reordered relative to the others, since it is often a multi-line
`fun` expression.
2. The function argument should come last. This enables its
arguments (which are often polymorphic) to benefit from type-based
disambiguation information determined by the types of the other
arguments at the call sites.
3. The function argument's type should produce an
accumulator-transformer when partially-applied. That is,
`f x : 's -> 's`. This composes well with other functions designed
to produce transformers/endofunctions when partially applied, and
in particular improves the common case of composing folds into
"state-passing style" code.
4. The fold function itself should produce an accumulator-transformer
when partially applied. So `'a t -> 's -> f:_ -> 's` rather than
`'s -> 'a t -> f:_ -> 's` or `'a t -> init:'s -> f:_ -> 's` etc.
Reviewed By: jvillard
Differential Revision: D24306063
fbshipit-source-id: 13bd8bbee
Summary:
The changes in set_intf.ml dictate the rest. The previous API
minimized changes when changing the backing implementation. But that
API is hostile toward composition, partial application, and
state-passing style code.
Reviewed By: jvillard
Differential Revision: D24306089
fbshipit-source-id: 00a09f486
Summary:
Preceding commit reversed Map.to_iter to match the previous behavior
of to_list.
Reviewed By: jvillard
Differential Revision: D24306051
fbshipit-source-id: aad12e434
Summary:
The changes in map_intf.ml dictate the rest. The previous API
minimized changes when changing the backing implementation. But that
API is hostile toward composition, partial application, and
state-passing style code.
Reviewed By: jvillard
Differential Revision: D24306050
fbshipit-source-id: 71e286d4e
Mitya Lyubarskiy
Daiva Naudziuniene
Nikos Gorogiannis
Josh Berdine
Ezgi Çiçek
Sungkeun Cho
Jules Villard