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
Summary:
Remove `-error-style short` from the compilation flags since it causes
merlin to complain, see https://github.com/ocaml/merlin/issues/1176.
After this diff, developers will need to set `OCAML_ERROR_STYLE=short`
in their environment.
Reviewed By: jvillard
Differential Revision: D24306066
fbshipit-source-id: 9c4f26393
Summary:
The usage of equal_or_opposite boils down to evaluating formulas on
propositional constants, which seems clearer.
Reviewed By: jvillard
Differential Revision: D24306104
fbshipit-source-id: df5d07628
Summary:
Represent And and Or formulas as pairs of sets of formulas. One set is
interpreted as positive and the other as negative. This results in
normalization with respect to associativity, commutativity, and unit
laws. This does not normalize distributivity laws, e.g. formulas are
not expanded to disjunctive-normal form or conjunctive-normal
form. Additionally, "zero" laws P ∧ ¬P iff ⊥ and P ∨ ¬P iff ⊤ are
cheaply detected and normalized. Note that formulas are already in
negation-normal form.
Reviewed By: jvillard
Differential Revision: D24306072
fbshipit-source-id: e52265a44
Summary:
Some Iter and Containers functions take optional arguments that
default to polymorphic comparison. This diff wraps all of these making
the argument non-optional to avoid silently using polymorphic compare.
Reviewed By: ngorogiannis
Differential Revision: D24306074
fbshipit-source-id: 34772ee86
Summary:
Expressing the sort of short-circuit evaluation in the changed code is
conceptually more direct using iterators.
Also, when using With_return, getting usable backtraces relies on the
compiler recognizing that the `raise` in the implementation of
`Base.Exn.raise_without_backtrace` should be a `reraise`. Using
iterators avoids this potential fragility.
Reviewed By: jvillard
Differential Revision: D24306094
fbshipit-source-id: b1abe04fb
Summary:
Change implementation of IArray from a wrapper of
Core_kernel.Array.Permissioned to NS.Array, and remove magic. Also
add operations to Array and Iter in order to ensure that IArray is an
extremely thin wrapper of Array: only defining conversions to/from
arrays as well as adding hashing support.
Reviewed By: jvillard
Differential Revision: D24306095
fbshipit-source-id: 97b9187be
Summary: Can be useful, especially to dump all the summaries as json.
Reviewed By: skcho
Differential Revision: D24504253
fbshipit-source-id: 845e7d657
Summary:
Emit the crucial parts of Pulse summaries as json to enable
post-processing by external tools. Stop somewhat arbitrarily at some
datatypes that are just emitted as "opaque" values.
For example:
```
$ infer debug --procedures --procedures-summary-json --select 0
[[["pulse",[["ContinueProgram",{"post":{"heap":[["v3",[[["Dereference"],["v4","_"]]]],["v7",[[["Dereference"],["v3","_"]]]]],"stack":[[["ProgramVar",{"plain":"return","mangled":null}],["v7","_"]]],"attrs":"_"},"pre":{"heap":[],"stack":[],"attrs":"_"},"skipped_calls":"_","path_condition":"_"}],["ContinueProgram",{"post":{"heap":[["v3",[[["Dereference"],["v4","_"]]]],["v8",[[["Dereference"],["v3","_"]]]]],"stack":[[["ProgramVar",{"plain":"return","mangled":null}],["v8","_"]]],"attrs":"_"},"pre":{"heap":[],"stack":[],"attrs":"_"},"skipped_calls":"_","path_condition":"_"}]]]]]
```
Reviewed By: ezgicicek
Differential Revision: D24503387
fbshipit-source-id: 9bd08e93b
Summary:
Output summaries in json format, so that other tools can exploit the
results of infer without having to be written inside infer itself.
For now the json for a summary is just one line saying "opaque" :)
Set up the infra to generate (yo)json automatically using
ppx_yojson_conv. See it in action in the next diff.
Reviewed By: ezgicicek
Differential Revision: D24503343
fbshipit-source-id: e24a2fff3
Summary:
- output the "menu" of the interactive mode on stderr instead of stdout
so that we can pipe the results, eg
`infer debug --procedures --procedures-summary | cat`
This will be more useful when we add an option to output json, as
otherwise the menu pollutes the json.
- Allow "--select" to work for infer-debug too:
`infer debug --procedures --procedures-summary --select 0`
Reviewed By: da319
Differential Revision: D24503301
fbshipit-source-id: d7fb4b713
Summary:
This diff revises `nextObject` model to handle multiple symbolic enumerators. Instead joining the
symbolic offsets of them, which sometimes introduces top, it sums the offsets. This is a sound &
conservative semantics since they are all non-negative integers.
Reviewed By: ezgicicek
Differential Revision: D24474513
fbshipit-source-id: 6707aa907
Summary:
This diff revises memory model of enumerator in ObjC to enable passing it as a parameter.
The cost checker was not able to analyze a function precisely when it gets an enumerator as a
parameter because the offset of an enumerator was available only when the analyzer knew the correct
relation between the enumerator and an array.
This diff simplifies the enumerator to have a similar value with `array->elements`, so its offset can
be taken without the relation between enumerator and array to get them.
Reviewed By: ezgicicek
Differential Revision: D24446574
fbshipit-source-id: 27cdc051e
Summary:
This diff adds an option hiding function pointers in costs to users: `cost-suppress-func-ptr` is
true by default.
Reviewed By: ezgicicek
Differential Revision: D24448212
fbshipit-source-id: 88f6b5ea1
Josh Berdine
Sungkeun Cho
Jules Villard
Ezgi Çiçek
Daiva Naudziuniene
Nikos Gorogiannis