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
Summary:
Before this diff we would just propagate the callee abstract state,
which doesn't make sense in the caller. We could just remove the state
from AbortProgram altogether as Pulse itself doesn't use it, but for now
let's at least make sure it's accurate.
Also needed for upcoming hackathon that will start from Pulse error
specs to try to produce tests :)
Reviewed By: ezgicicek
Differential Revision: D24448073
fbshipit-source-id: 9100b3f79
Summary:
Detect when changed files paths are trying to escape the project root
and try to guess their relative project root (which has to be a parent
of the current one).
This is perhaps a bit too hacky but it works for the case we need it to.
Reviewed By: martintrojer
Differential Revision: D24425427
fbshipit-source-id: 018651740
Summary:
Sometimes you need several project roots (eww), this makes paths make
sense even in that case.
Reviewed By: martintrojer
Differential Revision: D24336244
fbshipit-source-id: f087d533a
Summary:
Term.const_of is misleading as it is easy to expect it checks if a
term is a constant, or to expect that it returns the constant part of
a term. Instead, Term.split_const is clearer:
```
val split_const : t -> t * Q.t
(** Splits a term into the sum of its constant and non-constant parts.
That is, [split_const a] is [(b, c)] such that [a = b + c] and the
absolute value of [c] is maximal. *)
```
Reviewed By: ngorogiannis
Differential Revision: D24306065
fbshipit-source-id: ba15958ad
Summary:
The treatment of comparison and exceptions in Core/Core_kernel/Base
makes them questionable as the default. This diff changes nonstdlib so
that Core is no longer opened in the global namespace, and makes a few
changes to handle the resulting minor API changes. This leads to a
lighter-touch nonstdlib, which makes a few definitions of its own, and
selects and extends modules from several libraries, including base,
core_kernel, containers, iter.
Reviewed By: jvillard
Differential Revision: D24306090
fbshipit-source-id: 42c91bd1b
Summary: Now elapsed time and the info in Unix.process_times is treated uniformly.
Reviewed By: jvillard
Differential Revision: D24306049
fbshipit-source-id: 09ab734ea
Summary:
The unary comparison to zero predicates are confusing to read since
whether the 0 is the left or right argument of the naturally infix
comparison is ambiguous. So replace Gt0 with Pos, meaning the argument
is positive, and remove the rest.
Reviewed By: jvillard
Differential Revision: D24306067
fbshipit-source-id: 2bd30dbe4
Summary:
Checking whether a formula is negative now only needs to inspect the
principle connective.
Reviewed By: ngorogiannis
Differential Revision: D24306061
fbshipit-source-id: 1f110e7f1
Josh Berdine
Jules Villard
Daiva Naudziuniene
Nikos Gorogiannis
Sungkeun Cho
Mitya Lyubarskiy