Summary:
It supports flexible array member using the following heuristic:
- a memory for a class is allocated by `malloc(sizeof(C) + n * sizeof(T))` format
- the last field of the class is an array
- the static size of the last field is one, i.e., `T field_name[1]`
When allocating and initializing members of classes, it sets the size of flexible array to `n+1` if the above conditions are met.
Reviewed By: mbouaziz
Differential Revision: D7056291
fbshipit-source-id: 31c5868
Summary:
The semantics of "placement new" is defined simply as an assignment.
For example, `C* x = new (y) C();` is analyzed as if `C* x = y;`.
Reviewed By: mbouaziz
Differential Revision: D7054007
fbshipit-source-id: 1c6754f
Summary:
It abstracts the environments required in modeling functions and type
declarations as a record type.
Reviewed By: mbouaziz
Differential Revision: D7065996
fbshipit-source-id: b60cd3c
Summary:
This commit improves precision of symbol instantiations.
When a return value of a callee is `[s1 + s2, _]` and if we want to
instantiate `s1` to `c3 + max(c4, s5)`, the lower bound was
substituted to `-oo` because our domain cannot express `c3 + max(c4,
s5) + s2`.
However, we can have instantiations that are preciser than `-oo`:
(1) `c3 + c4 + s2`
(2) or `c3 + s5 + s2`
because they are smaller than the ideal instantiation, `c3 + max(c4,
s5) + s2` and it is on the lower bound position.
For now, the implementation instantiates to (1) between the two ones,
because constant values introduced by `assert` or `assume`(`if`)
command are often used as safety conditions, e.g., `assert(index >=
0);` can place before array accesses. (We can change the stratege
later if we find that it doesn't work on some other cases.)
Reviewed By: mbouaziz
Differential Revision: D7020063
fbshipit-source-id: 62fb390
Summary:
It prunes abstract memories on `assert` commands.
Problem: Since the assert command is sometimes translated to two
sequential `if` statments, it was not able to prune the memory
precisely at `assert` commands in Inferbo---the pruned memory at the
first branch was joined before the second branch.
Solution: To avoid losing the pruning information at the first branch,
now, it records which locations are pruned at the first branch and
applies the same pruning at the next branch if they have
semantically the same condition.
Reviewed By: mbouaziz
Differential Revision: D6895919
fbshipit-source-id: 15ac1cb
Summary: The heuristics to determine the end of a block/procedure was too brittle, the new one ignores non significant instructions.
Reviewed By: jvillard
Differential Revision: D6845380
fbshipit-source-id: feab557
Summary:
- `NonZeroInt` for added guarantees on the invariants of `SymLinear` coefficients
- some simplifications
- some optimizations
Reviewed By: jvillard
Differential Revision: D6833968
fbshipit-source-id: 39e28a0
Summary:
`&::.*-->` allows to match any path end.
Used for models of `std::array` to force unmodelled functions (and types) to have a Skip summary
Depends on D6408415
Reviewed By: jvillard
Differential Revision: D6611203
fbshipit-source-id: 6663b2c
Summary:
Found the dead code with the script in the next commit, iteratively until no
warnings remained.
Methodology:
1. I kept pretty-printers for values, which can be useful to use from infer's REPL (or
when printf-debugging infer in general)
2. I kept functions that formed some consistent API (but not often, so YMMV), for instance if it looked like `Set.S`, or if it provides utility functions for stuff in development (mostly the procname dispatcher functions)
3. I tried not to lose comments associated with values no longer exported: if the value is commented in the .mli and not the .ml, I moved the comment
4. Some comments needed updating (not claiming I caught all of those)
5. Sometimes I rewrote the comments a bit when I noticed mis-attached comments
Reviewed By: mbouaziz
Differential Revision: D6723482
fbshipit-source-id: eabaafd
Summary:
Upgrade ocamlformat to 0.3, and (necessarily) base to v0.10.0.
- Fix accumulated mis-formatting
- Update opam.lock to unbreak clean build
- Update to base v0.10.0
- Update opam.lock for base
- Update offline opam repo
- Everyone should already have removed their ocamlformat pin
- ocamlformat 0.3 supports output to stdout natively
- bump version of ocamlformat
Reviewed By: jeremydubreil
Differential Revision: D6636741
fbshipit-source-id: 41a56a8
Summary:
Model for `folly::split` that handles the representation in the cpp model.
Depends on D6544992
Reviewed By: jvillard
Differential Revision: D6545006
fbshipit-source-id: 2b7a139
Summary:
Allows:
- matching function arguments with or without capturing,
- capturing part of an argument, e.g. expression only,
- optional arguments, wrapped into an OCaml option if captured.
Reviewed By: jvillard
Differential Revision: D6544992
fbshipit-source-id: a64ba45
Summary: There was a back and forth conversion between `string` and `IssueType.t` which was not necessary.
Reviewed By: sblackshear
Differential Revision: D6562747
fbshipit-source-id: 70b57a2
Summary:
It seems that the abstraction instructions were not previously added the the CFG.
This is a functional changes to make sure that the abstraction state is always added. We can simplify the code later and just run this step before storing the CFG instead of after loading them.
Reviewed By: sblackshear, jvillard
Differential Revision: D6383672
fbshipit-source-id: cedcb8a
Summary:
justmovingthingsaround
Models need these functions, they have to be somewhere else.
The split might seem weird for now but will (hopefully) look more obvious in the following diff.
Reviewed By: skcho
Differential Revision: D6408322
fbshipit-source-id: c7e430f
Summary:
Extends `ProcnameDispatcher` to allow matching typenames only.
There isn't much new here, mainly moving stuff so that we only have to open one module to use the operators.
Reviewed By: skcho
Differential Revision: D6408245
fbshipit-source-id: afc6533
Summary:
- Plug model checkers
- Add alloc size safety condition on alloc of negative, zero or big size
Reviewed By: sblackshear
Differential Revision: D6375144
fbshipit-source-id: bbea6f3
Summary:
A modeled function is not only an evaluator but also a checker, at least in Inferbo where both things happen in two passes.
This diff just prepares for it without generating new alarms.
Reviewed By: jvillard
Differential Revision: D6373051
fbshipit-source-id: 264696f
Summary: There is a lot of code to create LaTeX output of the Infer datastructures, but this does not seem to be used anymore.
Reviewed By: jvillard
Differential Revision: D6355686
fbshipit-source-id: 55de8e9
Summary:
Allow capturing function arguments.
Model functions don't have to match on a list any more.
Depends on D6347829
Reviewed By: jvillard
Differential Revision: D6350628
fbshipit-source-id: e88b758
Summary: When not matching overloads, when the wrong number of arguments is given, instead of just no matching the function, we may want to fail, e.g. for internal-use functions.
Reviewed By: jvillard
Differential Revision: D6347829
fbshipit-source-id: 48f41be
Summary:
First steps of a dispatcher for C++ functions/methods overloads.
For now only used on Inferbo C modeled functions so most of the features are still unused.
Reviewed By: jvillard
Differential Revision: D6336088
fbshipit-source-id: ebd5b6f
Summary:
...so I just removed it
+ renamed `loc` of type `Location.t` to `location` to differentiate from `Loc.t` values
Reviewed By: jvillard
Differential Revision: D6358413
fbshipit-source-id: 2d3eba9
Summary:
Change ocamlformat installation procedure to use opam instead of
pinning.
Reformat all code with v0.2, which has a few improvements.
Reviewed By: jvillard
Differential Revision: D6292057
fbshipit-source-id: 759967f
Summary:
:
As we want to model many C++ methods, using a lot of matchers with `if / else if` will be tiring.
This diff introduces a dispatcher which is a nicer way to write the same thing.
No new model for now, just a refactoring.
Ideally we'd need a parser generator for C++ names...
Reviewed By: jvillard
Differential Revision: D6209234
fbshipit-source-id: 49fae5e
Summary:
vector::data returns a pointer to the first value of the vector.
- The size of the (array) pointer should be the same with the vector.
- The pointer should point to the same abstract value with the vector.
Reviewed By: mbouaziz
Differential Revision: D6196592
fbshipit-source-id: cc17096
Summary:
Install ocamlformat from github as part of `make devsetup`, and use it
for formatting OCaml (and jbuild) code.
Reviewed By: jvillard
Differential Revision: D6092464
fbshipit-source-id: 4ba0845
Summary: This commit adds unsigned symbol for preciser analysis results with less number of uses of min/max operators.
Reviewed By: mbouaziz
Differential Revision: D6040437
fbshipit-source-id: 999ca4c
Summary:
Next step to issue deduplication: do not keep safety conditions that are subsumed by others.
Only do it if they do not have infinite bound: replacing `0 < size` by `1 < size` is ok, but replacing it by `+oo < size` is not because it looks much more like a lack of precision.
Reviewed By: skcho
Differential Revision: D5978455
fbshipit-source-id: acc2384
Summary:
A specific type of alias is added for the vector::empty() result and it is used at pruning.
Now, there are two types of aliases:
- "simple" alias: x=y
- "empty" alias: x=v.empty() and y=v.size
So, if x!=0, y is pruned by (y=0). Otherwise, i.e., x==0, y is pruned by (y>=1).
Reviewed By: mbouaziz
Differential Revision: D6004968
fbshipit-source-id: bb8d50d
Summary:
Move Inferbo safety conditions to their own file.
Split the old `Condition.t` to a condition together with a trace.
This will ease having: different kind of condition and several traces for the same condition (see following diff)
Reviewed By: jvillard
Differential Revision: D5942030
fbshipit-source-id: d74a612
Summary:
Bottom bounds do not make sense (what is the meaning of `[_|_; 1]`?), let's get rid of them.
`Bot` was useful for substitution though, with a special meaning, use `bottom_lifted` for that case.
Reviewed By: skcho
Differential Revision: D5941796
fbshipit-source-id: 5778255
Summary: A bottom interval in a safety condition doesn't make sense. Let's not allow it at all.
Reviewed By: skcho
Differential Revision: D5941552
fbshipit-source-id: 6bd2a65
Summary: Use `pp` functions until it needs to be turned into a string.
Reviewed By: jvillard
Differential Revision: D5941473
fbshipit-source-id: 87ca9df
Summary:
The interval bound of the abstract domain is extended.
`[min|max](int, symbol)` => `int [+|-] [min|max](int, symbol)`
As a result, `vector::empty` can be modelled to return a more precise value: `1 - min(1, size)`.
Reviewed By: mbouaziz
Differential Revision: D5899404
fbshipit-source-id: c8c3f49
Sungkeun Cho
Mehdi Bouaziz
Jeremy Dubreil
Jules Villard
Josh Berdine
Sam Blackshear