Summary: Could be made better for cycles but not used and not unit tested, let's remove it.
Reviewed By: ngorogiannis
Differential Revision: D16017744
fbshipit-source-id: 6f7ae95c1
Summary: Do not fail on cycles, normalize values issuing from cycles, but do not try to recognize equal cycles like `let rec x = 1 :: x` and `let rec y = 1 :: 1 :: y`. This is unlikely to happen in our code.
Reviewed By: ngorogiannis
Differential Revision: D16017365
fbshipit-source-id: 691bb756c
Summary:
The previous version had a potentially exponential behavior on values with already lots of sharing.
This is fixed here at the price of a multiplicative constant factor (cost of `Hashtbl.hash`).
It also prepares for the handling of cycles.
Reviewed By: ngorogiannis
Differential Revision: D16016906
fbshipit-source-id: 611287917
Summary:
Reduces the size of the `tenv` by sharing values as most as possible, in an untyped - but supposedly safe - way, by using black magic on objects.
Can be reused for other things later.
Reviewed By: ngorogiannis
Differential Revision: D15855870
fbshipit-source-id: 169a4b86b
Summary:
Instrument SIL according to TOPL properties. Roughly, the
instrumentation is a set of calls into procedures that simulate a
nondeterministic automaton. For now, those procedures are NOP dummies.
Reviewed By: jvillard
Differential Revision: D15063942
fbshipit-source-id: d22c2f6fa
Summary:
Improve the error messages, change is more or less documented in the
code.
Reviewed By: mbouaziz
Differential Revision: D15374334
fbshipit-source-id: f1dd54180
Summary:
TOPL properties are essentially automata, which will be modeled as a set
of procedures. The code-to-analyze makes calls into these procedures,
thereby driving the automaton. In this commit, these calls do not do
anything. The point is to prepare the hook-up mechanism.
Reviewed By: jvillard
Differential Revision: D14819650
fbshipit-source-id: d95ecdb3d
Summary:
This ensures that each attribute type can only be present once per
address. Makes ~80x time improvement on pathological cases such as
Duff's device.
This introduces a new kind of Set in `PrettyPrintable`.
Reviewed By: mbouaziz
Differential Revision: D14645091
fbshipit-source-id: c7f9b760c
Summary: Spent some time staring at empty HTML output instead of seeing `<Some ...>` because I'm dumb. Now it's dumb proof.
Reviewed By: mbouaziz
Differential Revision: D14258492
fbshipit-source-id: d1368d212
Summary:
The `oenv` is an option.
This diff ensures that it is `Some` during the analysis and `None` when it is stored in a summary.
It could have been resolved with another type, e.g. `unit`, but an option was needed to avoid duplicating code that is generic up to some point.
The price to pay is a parametric type.
Reviewed By: skcho
Differential Revision: D13825418
fbshipit-source-id: 71824609d
Summary:
Record per-location traces. Actually, that doesn't quite make sense as a
location can be accessed in many ways, so associate a trace to each
*edge* in the memory graph. For instance, when doing `x->f = *y`, we
want to take the history of the `<val of y> --*--> ..` edge, add "assigned
at location blah" to it and store this extended history to the edge
`<val of x> --f--> ..`.
Use this machinery to print nicer traces in `infer explore` and better
error messages too (include the last assignment, like biabduction
messages).
Reviewed By: da319
Differential Revision: D13518668
fbshipit-source-id: 0a62fb55f
Summary:
When assign to the special `return` variable, check that the result is
not the address of a local variable, otherwise report.
Reviewed By: ngorogiannis
Differential Revision: D13466896
fbshipit-source-id: 465da7f13
Summary:
When a lambda gets created, record the abstract addresses it captures, then
complain if we see some of them be invalidated before it is called.
Add a notion of "allocator" for reporting better messages. The messages are
still a bit sucky, will need to improve them more generally at some point.
```
jul lambda ~ infer 1 infer -g --pulse-only -- clang -std=c++11 -c infer/tests/codetoanalyze/cpp/pulse/closures.cpp
Logs in /home/jul/infer.fb/infer-out/logs
Capturing in make/cc mode...
Found 1 source file to analyze in /home/jul/infer.fb/infer-out
Found 2 issues
infer/tests/codetoanalyze/cpp/pulse/closures.cpp:21: error: USE_AFTER_DESTRUCTOR
`&(f)` accesses address `s` captured by `&(f)` as `s` invalidated by destructor call `S_~S(s)` at line 20, column 3 past its lifetime (debug: 5).
19. f = [&s] { return s.f; };
20. } // destructor for s called here
21. > return f(); // s used here
22. }
23.
infer/tests/codetoanalyze/cpp/pulse/closures.cpp:30: error: USE_AFTER_DESTRUCTOR
`&(f)` accesses address `s` captured by `&(f)` as `s` invalidated by destructor call `S_~S(s)` at line 29, column 3 past its lifetime (debug: 8).
28. f = [&] { return s.f; };
29. }
30. > return f();
31. }
32.
Summary of the reports
USE_AFTER_DESTRUCTOR: 2
```
Reviewed By: da319
Differential Revision: D13400074
fbshipit-source-id: 3c68ff4ea
Summary:
Sometimes in debug mode, the condition set is too big to print in the
log file. This diff limits the maximum number of conditions to print
as 30.
Reviewed By: mbouaziz
Differential Revision: D12836661
fbshipit-source-id: 8ddfe64a7
Summary:
This adds an option `--trace-events` that generates a Chrome trace event[1] to
quickly visualise the performance of infer.
Reviewed By: mbouaziz
Differential Revision: D9831599
fbshipit-source-id: 96a33c627
Summary:
`ANSITerminal` flushes after almost every operation. As a result, there is a
lot of flicker in the task bar. Going through `Format` instead reduces the
flicker.
Also erase end-of-lines when outputting logging stuff to the console. This makes sure the output is not garbled with stuff from the task bar.
Reviewed By: ngorogiannis
Differential Revision: D8931294
fbshipit-source-id: e89c87f84
Summary:
Replace the previous outputting of "." and "F" with an actual progress bar and
a multiline display of what procedure each process is currently busy analysing.
Observe:
```lang=text
Found 19 source files to analyze in /home/jul/code/openssl-1.1.0d/infer-out
7/19 [######################......................................] 36%
⊢ [ 1.14s] crypto/mem.c: CRYPTO_malloc
⊢ [ 1.68s] crypto/o_time.c: julian_adj
⊢ [ 0.50s] crypto/mem.c: CRYPTO_zalloc
⊢ [ 1.80s] crypto/o_str.c: OPENSSL_strlcpy
```
This works by setting up a worker pool (as before) that waits to receive jobs
(not as before: we used to fork for each new job). Unix pipes are used for
communication.
The new worker pool can be used to experiment with other concurrency models,
such as reviving per-procedure-parallelism, or making sure each procedure is
analysed only once.
Perf tests indicate that this version is no slower than the previous one,
either on laptops or devserver: about 3% worse user time but ~40% better system time.
This new version forks <jobs> processes whereas the previous version would
fork `O(number of source files)` times.
`infer -j 1` shows a progress bar that doesn't update timing info (because it
would need a second process to do that).
Reviewed By: mbouaziz
Differential Revision: D8517507
fbshipit-source-id: c8ca104
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:
Now the result won't depend on the visit order of instructions
Depends on D8235834
Reviewed By: jeremydubreil
Differential Revision: D8235907
fbshipit-source-id: a6eb469
Summary:
Forcing integration with `--force-integration` would only work for some
integrations that stayed in OCaml-land. This propagetes the forcing to
infer.py.
Also remove some unused options on the Python side, and add more debug
information.
Fixes#927
Reviewed By: mbouaziz
Differential Revision: D8235504
fbshipit-source-id: 1d98543
Summary:
Change the license of the source code from BSD + PATENTS to MIT.
Change `checkCopyright` to reflect the new license and learn some new file
types.
Generated with:
```
git grep BSD | xargs -n 1 ./scripts/checkCopyright -i
```
Reviewed By: jeremydubreil, mbouaziz, jberdine
Differential Revision: D8071249
fbshipit-source-id: 97ca23a
Summary:
For now: just moving this list behind an abstract type.
Next: changing the internal representation.
Reviewed By: ngorogiannis
Differential Revision: D8140926
fbshipit-source-id: 5b959b0
Summary:
`IList.map_changed` relies on `take_append`.
The existing code was a `take_rev_append` instead.
Fixed it.
Tests are still passing, we might want to look at callsites and consider a `map_changed_unordered`.
Reviewed By: jvillard
Differential Revision: D8201187
fbshipit-source-id: 151b95c
Summary:
We never really need the list of nodes/succs/preds, we only need to fold over them.
This will reduce garbage for computed lists like in the Exceptional CFG or the OneInstrPerNode CFG.
Reviewed By: ngorogiannis
Differential Revision: D8185665
fbshipit-source-id: d042beb
Summary:
Append can be costly, let's do it once only.
Depends on D8185619
Reviewed By: jeremydubreil
Differential Revision: D8185634
fbshipit-source-id: 67f84a9
Summary: It seems that we don't need to rely on `make` anymore as the internal process manager is working fine on Buck Java projects.
Reviewed By: jvillard
Differential Revision: D7903639
fbshipit-source-id: 9b32f05
Summary:
This is an attempt to make things more consistent, and maybe save some work
from the `Format` module in case flambda doesn't have our backs.
Reviewed By: jberdine
Differential Revision: D7775496
fbshipit-source-id: 59a6314
Summary:
Upgrade ocamlformat, and base which needs to be done in sync in order to build
ocamlformat, and the other deps can come for the ride.
Reviewed By: jvillard
Differential Revision: D7663537
fbshipit-source-id: 3e90970
Summary:
Add a `--procedures` option to `infer explore` to print information about the
procedures captured by infer. More precisely, `infer explore --procedures` will
print each row of the "procedures" table in the results database. A new
`--procedures-filter` controls which procedures to print information about, and
there is one flag per column in the db too to print more or less options about
each procedure (in particular, we can now print attributes), with some defaults.
Reviewed By: sblackshear
Differential Revision: D7639062
fbshipit-source-id: 034a2b8
Summary:
There's actually a nice separation between IR/, base/, istd/, and the rest of
infer, so they can be made into separate jbuilder libraries so that the
separation remains. This helps make sense of the infer codebase.
Also:
- move everything biabduction-related out of backend/ and into a new
biabduction/ directory. This clarifies the current situation where backend/
contains a mix of analysis-independent code (still there now), and
biabduction-specific code (moved to biabduction/).
- move everything from base/ that is not infer-specific into istd/, e.g. IList.ml
- kill unused `FbTraceCalls`
- A couple of files needed to move around to complete the separation of base/ and IR/
Reviewed By: mbouaziz
Differential Revision: D7381842
fbshipit-source-id: cd86dea
Summary:
Limit the scope of what gets included into IStd.ml to only values that we want
to shadow. New values go into other files.
Also, build istd/ with `Core` open.
Reviewed By: mbouaziz
Differential Revision: D7382111
fbshipit-source-id: 969f0e8
Summary:
There's no real reason not to use `Core` lists in this module. Changed the
interface to be more `Core`-like. Changed the `*_changed` functions to use a
ref to track changes instead of passing the changed state around.
Reviewed By: mbouaziz
Differential Revision: D7123211
fbshipit-source-id: b27791a
Summary:
Just a bunch of minor changes.
- The mutable field doesn't need to be mutable: it's only mutated once in the code somewhere that doesn't even need to mutate
- Hence the type can be public
- All the `ms_get_*` functions are replaced by field accesses
- `CMethod_signature` -> `CMethodSignature` while I'm at it, although maybe that's bad since other files in clang/ follow the former convention
- `type method_signature` -> `type t`
- `pp` function instead of `to_string`, since it's used with `fprintf`. This gets rid of the only caller of `IList.to_string`.
Reviewed By: dulmarod
Differential Revision: D7123795
fbshipit-source-id: fdfae42
Summary:
`Sequence` API to walk over free variables in expressions, instead of computing lists with uniqueness constraints that make them have linear complexity for insertion.
Switch to a Set representation when we don't care about the order of elements,
otherwise to a `Hash_queue`:
https://ocaml.janestreet.com/ocaml-core/113.33/doc/core/Std/Hash_queue.mod/S.modt/
Often, we don't even need to compute the sequence of free variables, as we are
just testing membership/emptiness/...
Reviewed By: mbouaziz
Differential Revision: D7099294
fbshipit-source-id: e96f84b
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:
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:
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:
:
Make both buck capture and compilation database handle buck command line arguments and invoke buck query the same way.
Plus allow:
- target patterns `//some/dir:` and `//some/dir/...`. However since `//some/dir:#flavor` and `//some/dir/...#flavor` are not supported, they need to be expanded before adding the infer flavor.
- target aliases (defined in `.buckconfig`)
- shortcuts `//some/dir` rewritten to `//some/dir:dir`
- relative path `some/dir:name` rewritten to `//some/dir:name`
Reviewed By: jvillard
Differential Revision: D5321087
fbshipit-source-id: 48876d4
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:
Wrap ANSITerminal so that it doesn't apply control codes unless they can be
interpreted, and so that clients are unable to call ANSITerminal directly.
Reviewed By: mbouaziz
Differential Revision: D5953733
fbshipit-source-id: 6b3602a
Summary: Remove functions that are redundant with Base.List functions on sorted lists.
Reviewed By: mbouaziz
Differential Revision: D5931792
fbshipit-source-id: caec210
Summary:
`reraise` was error-prone when one forgot to save the backtrace between where the exception is caught and where it is reraised.
If any exception was raised (even caught) in between, the printed backtrace would be the one of the last exception thrown and it would be very confusing.
This diff kills `reraise` and introduces `reraise_after exn ~f` and `reraise_if exn ~f` to be used right after catching the exception.
Also turned some of them to the common pattern `try_finally ~f ~finally`.
Reviewed By: jvillard
Differential Revision: D5911244
fbshipit-source-id: 9883d1e
Summary:
With flambda (`-O3`), compilation time is ~5x slower, but the backend is ~25% faster!
To mitigate the atrocious compilation times, introduce a new `opt` build mode in the jbuilder files.
- build in "opt" mode by default from the toplevel (so that install scripts and external users get the fastest infer by default), in "default" mode by default from infer/src (since the latter is only called directly by infer devs, for faster builds)
- `make byte` is as fast as before in any mode
- `make test` will build "opt" by default, which is very slow. Solution for testing (or building the models) locally: `make BUILD_MODE=default test`.
- You can even change the default locally with `export BUILD_MODE=default`.
The benchmarks are to be taken with a sizable pinch of salt because I ran them only once and other stuff could be running in the background. That said, the perf win is consistent across all projects, with 15-20% win in wallclock time and around 25% win in total CPU time, ~9% win in sys time, and ~25% fewer minor allocations, and ~5-10% fewer overall allocations. This is only for the backend; the capture is by and large unaffected (either the same or a tad faster within noise range).
Here are the results running on OpenSSL 1.0.2d on osx (12 cores, 32G RAM)
=== base
infer binary: 26193088 bytes
compile time: 40s
capture:
```lang=text
real 1m7.513s
user 3m11.437s
sys 0m55.236s
```
analysis:
```lang=text
real 5m41.580s
user 61m37.855s
sys 1m12.870s
```
Memory profile:
```lang=json
{
...
"minor_gb": 0.1534719169139862,
"promoted_gb": 0.0038930922746658325,
"major_gb": 0.4546157643198967,
"allocated_gb": 0.6041945889592171,
"minor_collections": 78,
"major_collections": 23,
"compactions": 7,
"top_heap_gb": 0.07388687133789062,
"stack_kb": 0.3984375,
"minor_heap_kb": 8192.0,
...
}
```
=== flambda with stock options (no `-Oclassic`, just the same flags as base)
Exactly the same as base.
=== flambda `-O3`
infer binary: 56870376 bytes (2.17x bigger)
compile time: 191s (4.78x slower)
capture is the same as base:
```lang=text
real 1m9.203s
user 3m12.242s
sys 0m58.905s
```
analysis is ~20% wallclock time faster, ~25% CPU time faster:
```lang=text
real 4m32.656s
user 46m43.987s
sys 1m2.424s
```
memory usage is a bit lower too:
```lang=json
{
...
"minor_gb": 0.11583046615123749, // 75% of previous
"promoted_gb": 0.00363825261592865, // 93% of previous
"major_gb": 0.45415670424699783, // about same
"allocated_gb": 0.5663489177823067, // 94% of previous
"minor_collections": 73,
"major_collections": 22,
"compactions": 7,
"top_heap_gb": 0.07165145874023438,
"stack_kb": 0.3359375,
"minor_heap_kb": 8192.0,
...
}
```
=== flambda `-O2`
Not nearly as exciting as `-O3`, but the compilation cost is still quite high:
infer: 37826856 bytes
compilation of infer: 100s
Capture and analysis timings are mostly the same as base.
Reviewed By: jberdine
Differential Revision: D4867979
fbshipit-source-id: 99230b7
Summary: Try to preserve the original backtrace. Introduce `reraise` in the global namespace.
Reviewed By: jberdine
Differential Revision: D5804121
fbshipit-source-id: 0947a47
Summary: With Logging.exit you have more control of the code that invokes exit, for example when forking and running certain functions that may in turn invoke exit, and you want to handle the execution flow differently - like invoking certain callbacks before exiting, or not exiting at all.
Reviewed By: jvillard
Differential Revision: D5746914
fbshipit-source-id: 596fba1
Summary:
- failwith police: no more `failwith`. Instead, use `Logging.die`.
- Introduce the `SimpleLogging` module for dying from modules where `Logging`
cannot be used (usually because that would create a cyclic dependency).
- always log backtraces, and show backtraces on the console except for usage errors
- Also point out in the log file where the toplevel executions of infer happen
Reviewed By: jeremydubreil
Differential Revision: D5726362
fbshipit-source-id: d7a01fc
Summary:
This simplifies the jbuild files: no need to list these files explicitly
anymore, nor to exclude them explicitly from the main `InferModules` library
(due to their different compilation flags).
Isolate common parts into jbuild.common do `cat`-based code inclusion into
jbuild files to factorize code.
Reviewed By: jberdine
Differential Revision: D5678328
fbshipit-source-id: 6d7d925
Mehdi Bouaziz
Josh Berdine
Radu Grigore
Jules Villard
Jeremy Dubreil
Daniel Mercier
Nikos Gorogiannis
Nikos Gorogiannis
Sungkeun Cho
Ezgi Çiçek
Dino Distefano
Daiva Naudziuniene
Dulma Churchill
Martino Luca