Summary:
I hear that this scheduler is better. I want the best scheduler
possible. Also pulse's join is a bit complex so it might matter one day.
whydididothis
Reviewed By: mbouaziz
Differential Revision: D12958131
fbshipit-source-id: 3bd77ccba
Summary:
This may help running the id map bookkeeping on its own in the future
and makes the code slightly more readable in my opinion.
Reviewed By: mbouaziz
Differential Revision: D12858066
fbshipit-source-id: fea4aea63
Summary:
HIL wanted to do its own HTML printing, causing code duplication and hacks to
avoid double opening/closing files. Instead, pass a hook to print SIL
instructions or not.
This also makes the debug HTML be printed even in case of raised exceptions,
which is invaluable to debug crashes or even just reports in the case of
checkers that can raise `Stop_analysis` (pulse only for now).
This also print intermediate abstract states between instructions instead of
only at the start and end of nodes, for moar debugging.
Reviewed By: mbouaziz
Differential Revision: D12857425
fbshipit-source-id: 4ee6c88d6
Summary: Make the whole type private, introduce constructors for each variant, and deal with the consequences.
Reviewed By: da319
Differential Revision: D12825810
fbshipit-source-id: a01922812
Summary:
Seems useful to know when we're printing one instruction only, but not when we
print lots of them for readability.
Reviewed By: mbouaziz
Differential Revision: D12823481
fbshipit-source-id: 2beb339f2
Summary:
It terminates narrowing when new and old states are not comparable.
Since current narrowing does not use meet operations guaranteeing
termination of narrowing, it tries to terminate narrowing more
conservatively.
Reviewed By: mbouaziz
Differential Revision: D12815419
fbshipit-source-id: e8b45199e
Summary:
Instead of propagating a partial state give up the analysis of the
function entirely on error. The state after an error is mostly
non-sensical so until we know better just giving up makes sure the
analysis remains sensible and produce fewer spurious warnings.
Reviewed By: mbouaziz
Differential Revision: D10483979
fbshipit-source-id: 171ec8469
Summary:
New analysis in foetal form to detect invalid use of C++ objects after their
lifetime has ended. For now it has:
- A domain consisting of a graph of abstract locations representing the heap, a map from program variables to abstract locations representing the stack, and a set of locations known to be invalid (their lifetime has ended)
- The heap graph is unfolded lazily when we resolve accesses to the heap down to an abstract location. When we traverse a memory location we check that it's not known to be invalid.
- A simple transfer function reads and updates the stack and heap in a rudimentary way for now
- C++ `delete` is modeled as adding the location that its argument resolves to to the set of invalid locations
- Also, the domain has a really crappy join and widening for now (see comments in the code)
With this we already pass most of the "use after delete" tests from the
Ownership checker. The ones we don't pass are only because we are missing
models.
Reviewed By: mbouaziz
Differential Revision: D10383249
fbshipit-source-id: f414664cb
Summary:
In some error paths we may end up querying the state for the instruction
being executed, but that is only populated by biabduction. Now it's
populated by AI checkers too.
Reviewed By: jberdine
Differential Revision: D10381068
fbshipit-source-id: dca1325d7
Summary:
When the backend crashes we print which instruction/file/... we were analysing,
but because of recursion we can end up repeating that information all
the way to the toplevel call.
This makes sure we only print the innermost one, we don't care about the
calling context because the analysis is compositional.
Reviewed By: mbouaziz
Differential Revision: D10381141
fbshipit-source-id: 1c92bb861
Summary: Before this diff, the analysis would only lookup the attributes with the classname appearing in the instruction. However, it would fail to find those attributes for inherited and not overridden methods. With this diff, the attributes are now searched recursively in the super classes.
Reviewed By: mbouaziz
Differential Revision: D10007469
fbshipit-source-id: 77d721cba
Summary: This fixes some cases of false positives where the analysis will compare with the wrong overridden methods. This could later be improved with the possibility to do sub-typing comparison on the parameters.
Reviewed By: ngorogiannis
Differential Revision: D9985249
fbshipit-source-id: 7998d8619
Summary:
Now we see which file/procedure/instruction is responsible for a crash in the
backend. Biabduction and eradicate not supported yet for the instruction-level
debug.
Reviewed By: mbouaziz, da319
Differential Revision: D9915666
fbshipit-source-id: 279472305
Summary:
The internal concept of "kind" should in fact be named "severity" to match the convention used by many other tools, whereas the internal concept of "severity", i.e "HIGH", "MEDIUM" and "LOW" was never used and in any case redundant with the concept of "info", "warning", "error".
This diff maps both the "kind" and "severity" fields to value of the form "advice", "info", "warning", and "error" to be able to progressively migrate the code using the "kind" field.
Reviewed By: mbouaziz, jvillard
Differential Revision: D9187978
fbshipit-source-id: 447d89f51
Summary:
It adds relational domains to Inferbo: octagon of Apron and polyhedra of Elina.
- Each Mem domain value includes one relational value containing relations among symbols. The relational values are modified by the `Prune` and `Store` commands.
- Each abstract value includes three symbols, which represent integer value, array offset, and array size of an abstract value.
The relational domain is deactivated by default. Use the `--bo-relational-domain {oct, poly}` option for the activation, though Inferbo with the relational domains does not work at this point because some modifications of Apron and Elina we made has not been applied to their opam repositories yet.
Reviewed By: jvillard
Differential Revision: D8874102
fbshipit-source-id: 08e5883cb
Summary:
It adds relational domains to Inferbo: octagon of Apron and polyhedra of Elina.
- Each `Mem` domain value includes one relational value containing relations among *symbols*. The relational values are modified by the `Prune` and `Store` commands.
- Each abstract value includes three *symbols*, which represent integer value, array offset, and array size of an abstract value.
The relational domain is deactivated by default, so this diff should not make any differences in CI.
Use `--bo-relational-domain {oct, poly}` for the activation, though Inferbo with the relational domains does not work at this point because some modifications of Apron and Elina we made has not been applied to their opam repositories yet.
Reviewed By: mbouaziz, jvillard
Differential Revision: D8478542
fbshipit-source-id: 510ff53
Summary:
`make doc` will use `jbuilder` (which in turn uses `odoc`) to generate the
documentation for infer's modules. This is useful to browse the APIs of infer
and gives a more discoverable place to host more general documentation about
infer's internals.
Besides the actual plumbing necessary to generate the docs, this diff also
- Moves the various infer/src/*/README.md to index.mld files that make it to the generated docs
- Fixes some doc comments that would anger `ocamldoc`
Closes#435
Reviewed By: mbouaziz
Differential Revision: D8314572
fbshipit-source-id: 4a5c70e
Summary: Create mechanism for suppressing starvation reports. To do that, refactor and expose a Checkers function.
Reviewed By: mbouaziz
Differential Revision: D8259583
fbshipit-source-id: f5b5a63
Summary:
Having the `Node` module including in the `CFG` one is confusing.
Let's keep it separate.
Reviewed By: ngorogiannis
Differential Revision: D8185754
fbshipit-source-id: 62077e6
Jules Villard
Mehdi Bouaziz
Sungkeun Cho
Jeremy Dubreil
Ezgi Çiçek
Nikos Gorogiannis
Josh Berdine