Summary:
Rather than printing the footprint using its actual representation (an access trie with bool nodes), print it as a set of access paths.
This makes it easier to read sources in Quandary specs/debug Quandary.
Reviewed By: jeremydubreil
Differential Revision: D5682630
fbshipit-source-id: ac55b7f
Summary:
Add `is_empty` to `AbstractDomain.WithBottom` sig and use the empty checks for nicer printing of access trees: don't print empty nodes/traces.
This should make it easier to debug Quandary; it's pretty hard to stare at an access tree and see what's going on right now.
Reviewed By: jberdine
Differential Revision: D5682248
fbshipit-source-id: 56d2a9d
Summary:
We now represent the footprint with an access trie, so this code is no longer required.
This lets us simplify things a bit
Reviewed By: jberdine
Differential Revision: D5664484
fbshipit-source-id: c35edf2
Summary:
In looking at summaries that Quandary took a long time to compute, one thing I notice frequently is redundancy in the footprint sources (e.g., I might see `Footprint(x), Footprint(x.f), Footprint(x*)`).
`sudo perf top` indicates that joining big sets of sources is a major performance bottleneck, and a large number of footprint sources is surely a big part of this (since we expect the number of non-footprint sources to be small).
This diff addresses the redundancy issue by using a more complex representation for a set of sources. The "known" sources are still in a set, but the footprint sources are now represented as a set of access paths (via an access trie).
The access path trie is a minimal representation of a set of access paths, so it would represent the example above as a simple `x*`.
This should make join/widen/<= faster and improve performance
Reviewed By: jberdine
Differential Revision: D5663980
fbshipit-source-id: 9fb66f8
Summary:
It's nice to have "raw" as the default kind of access path, since it's used much more often than the abstraction.
This is also a prereq for supporting index expressions in access paths, since we'll need mutual recursion between accesses and access paths.
Reviewed By: jeremydubreil
Differential Revision: D5529807
fbshipit-source-id: cb3f521
Summary:
Conversion and reformat of infer source using ocamlformat
auto-formatting tool.
Current status:
- Because Reason does not handle docstrings, the output of the
conversion is not 'Warning 50'-clean, meaning that there are
docstrings with ambiguous placement. I'll need to manually fix
them just before landing.
Reviewed By: jvillard
Differential Revision: D5225546
fbshipit-source-id: 3bd2786
Summary: Gflags is a popular library used to create command line arguments. Flags shouldn't flow directly to `exec` etc.
Reviewed By: jvillard, mbouaziz
Differential Revision: D5058393
fbshipit-source-id: ab062f8
Summary:
Remove the remaining uses of polymorphic equality `=`.
In case of basic types, this is replaced by String.equal or Int.equal.
In case of `= []`, this is replaced by `List.is_empty`.
In case of `= None`, this is replaced by `is_none`.
In case of a datatype definition such as `type a = A | B`,
a `compare_a` function is defined by adding `type a = A | B [@deriving compare]`
and a `equal_a` function is defined as `let equal_a = [%compare.equal : a]`.
In case of comparison with a polymorphic variant `= `Yes`, the equality
defined in `PVariant.(=)` is used. Typically, `open! Pvariant` is added
at the beginning of the file to cover all the uses.
Reviewed By: jberdine
Differential Revision: D4456129
fbshipit-source-id: f31c433
Summary:
A domain should not definite its initial state, since distinct users of the domain may want to choose different initial values.
For example, one user might want to bind all of the formals to some special values, and one user might want the initial domain to be an empty map
This diff makes this distinction clear in the types by (a) requiring the initial state to be passed to the abstract interpreter and (b) lifting the requirement that abstract domains define `initial`.
Reviewed By: jberdine
Differential Revision: D4359629
fbshipit-source-id: cbcee28
Summary:
Previously, summaries worked by flattening the access tree representing the post of the procedure into (in essence) a list of functions from caller input traces to callee output traces.
This is inefficient in many ways, and is also much more complex than just using the original access tree as the summary.
One big inefficiency of the old way is this: calling `Trace.append` is slow, and we want to do it as few times as possible.
Under the old summary system, we would do it at most once for each "function" in the summary list.
Now, we'll do it at most once for each node in the access tree summary.
This will be a smaller number of calls, since each node can summarize many input/output relationships.
Reviewed By: jeremydubreil
Differential Revision: D4271579
fbshipit-source-id: 34e407a
Summary:
Change the domain of SIOF to be based on sets of pvar * location instead of
single pvars. This allows us to group several accesses together. However, we
still get different trace elems for different instructions in a proc. We do two
things to get around this limitation and get a trace where all accesses within
the same proc are grouped together, instead of one trace for each access:
1. A post-processing phase at the end of the analysis of one proc collects all
the globals directly accessed in the proc into a single trace elem.
2. When creating the error trace, unpack this set into several trace elements
to see each access (at its correct location) separately in the trace.
This is a bit hacky and another way would be to extend the API of traces to
handle in-procedure accesses natively instead of shoe-horning them. However
since SIOF is the only one to use this, it introduces less boilerplate to do it
that way for now.
Also, a few .mlis for good measure.
Reviewed By: sblackshear
Differential Revision: D4299070
fbshipit-source-id: 3bbb5c2
Summary:
Use In_channel and Out_channel operations instead of those in Pervasives. Don't
use physical equality on values that aren't heap-allocated since it doesn't help
the compiler generate faster code and the semantics is unspecified. Also use
phys_equal for physical equality.
Reviewed By: sblackshear
Differential Revision: D4232459
fbshipit-source-id: 36fcfa8
Summary:
Utils contains definitions intended to be in the global namespace for
all of the infer code-base, as well as pretty-printing functions, and
assorted utility functions mostly for dealing with files and processes.
This diff changes the module opened into the global namespace to
IStd (Std conflict with extlib), and moves the pretty-printing
definitions from Utils to Pp.
Reviewed By: jvillard
Differential Revision: D4232457
fbshipit-source-id: 1e070e0
Summary:
Trying to stop other users of the trace domain from making the mistake that Quandary made before D4234766.
This should also improve the performance of Quandary, since the filtering of FP's is now done before building up the full interprocedural trace (which requires disk reads).
Reviewed By: jeremydubreil
Differential Revision: D4234770
fbshipit-source-id: e7e9291
Summary:
We only ought to report a source-sink flow at the call site where the sink is introduced.
Otherwise, we will report silly false positives.
Reviewed By: jeremydubreil
Differential Revision: D4234766
fbshipit-source-id: 118051f
Summary: Generalizing jvillard's awesome work to include passthroughs in traces, then calling it from Quandary.
Reviewed By: jvillard
Differential Revision: D4172108
fbshipit-source-id: 0296c59
Summary:
This adds generic support for reporting error traces as usual infer issues
traces (instead of putting them in the textual description of the error) to
Trace.ml and SinkTrace.ml.
The siof checker is made to use these new traces, and gets an improved error
message mentioning the name of the problematic global as well, which requires a
slight API change in Pvar.re.
The support in Trace.ml is incomplete: passthroughs are ignored. This missing
feature will be needed by Quandary to migrate its error messages.
Reviewed By: sblackshear
Differential Revision: D4159542
fbshipit-source-id: 8c1101d
Summary:
There's not really a concept of callee here, so s/callee/callsite/, and "to"
suggests we get the callee whereas we update it, so s/to/with/.
Feel free to bikeshed further.
Reviewed By: sblackshear
Differential Revision: D4153426
fbshipit-source-id: 6ea762c
Summary: Other checkers are going to start using these, so they shouldn't live in the Quandary directory anymore
Reviewed By: jvillard
Differential Revision: D4124654
fbshipit-source-id: b1d5bdd
Summary: Other checkers are going to start using these, so they shouldn't live in the Quandary directory anymore
Reviewed By: jvillard
Differential Revision: D4117359
fbshipit-source-id: e3f151e
Sam Blackshear
Josh Berdine
Andrzej Kotulski
Cristiano Calcagno
Jules Villard