Summary:
After some testing, it looks like getting the pdesc via
`Ondemand.get_proc_desc` will also load models' proc descs from their
summaries, so this code should not be needed.
Reviewed By: jeremydubreil, mbouaziz, martintrojer
Differential Revision: D9197176
fbshipit-source-id: 1b8603bfa
Summary:
`Errlog` will merge similar issues (same severity, name, description) reported at the same location, so let's make sure the locaiton is mandatory.
Issues:
- errors happening in `Ondemand` still use the `State` which makes sense only for biabduction and eradicate
- a case of `NullabilitySuggest` didn't have a location, I did my best to patch it but I'm sure the location could be more precise
Reviewed By: jvillard
Differential Revision: D9332840
fbshipit-source-id: ee7898146
Summary: Keeping pushing arguments higher in the stack, `node_id_key` is not used in calls to `log_warning/error`
Reviewed By: jvillard
Differential Revision: D9332826
fbshipit-source-id: e5c48c686
Summary:
Before we would convert it to string in `Reporting` and pass it to `Errlog` which would use it only to 'log events'.
I guess the reason is that there was a cyclic dependency between `Errlog` and `clang_method_kind` defined in `ProcAttributes`.
This diff:
- moves it to its own module
- defers the conversion to string
Reviewed By: jvillard
Differential Revision: D9332819
fbshipit-source-id: 43a028b61
Summary:
- abstracted the type for a node key
- moved it to its own module with an ugly `compute` to avoid cyclic dependencies...
- renamed `node_id` to `node_id_key` where needed
- moved key computation from `State` to `Procdesc.Node`
Reviewed By: jvillard
Differential Revision: D9332803
fbshipit-source-id: fe1ae8c1c
Summary:
- made arguments of `Errlog.log_issue` mandatory
- pushed some arguments of `log_issue_from_errlog` higher in the stack, the goal is to make sure `State` is only used in analyses that update it (biabduction and eradicate, if I'm correct)
Reviewed By: jvillard
Differential Revision: D9332773
fbshipit-source-id: ce79df21c
Summary: The procedure id is likely to be trucated with random CRC values so we should probably not use it to match Java names
Reviewed By: mbouaziz
Differential Revision: D9183518
fbshipit-source-id: b450c7869
Summary: The `procedure` field in the final report should use the non-ambiguous fully qualified name containing the Java package declaration and the list of parameter types.
Reviewed By: mbouaziz
Differential Revision: D9237522
fbshipit-source-id: e9b0ff664
Summary: C++17 introduce guaranteed copy elision which omits constructor calls. In ownership analysis, we depended on these constructor calls to acquire ownership. In particular, when a method returns struct, previously, a constructor was used to acquire ownership. In this diff, we acquire ownership of the returned structs directly.
Reviewed By: mbouaziz
Differential Revision: D9244302
fbshipit-source-id: ae8261b99
Summary:
Useful tips and tricks to debug infer's OCaml code. Also emit a developer
warning when the database is not initialised (since it's only expected to
happen when running infer from the toplevel).
Reviewed By: mbouaziz
Differential Revision: D9295782
fbshipit-source-id: 09b7b9a02
Summary:
To keep up with the times. Changes consist of new features and moving modules
around so shouldn't change anything on our side.
Depends on D9239803
The controller you requested could not be found.: facebook-clang-plugins
Reviewed By: da319
Differential Revision: D9239817
fbshipit-source-id: d02a2076a
Summary: This test was not re-run when the Java dependencies were changing
Reviewed By: mbouaziz
Differential Revision: D9238288
fbshipit-source-id: 65cc9c03c
Summary:
Use `ignore` instead, as this will warn if the argument is an arrow type,
unlike `let _ = ...`. This makes the code more future-proof: if an argument is
added to a function called in `let _ = f x` then the compiler will complain
instead of silently turning a value into a partial evaluation.
Also got rid of particularly irksome `let _ = <stuff returning unit> in` where I could.
Reviewed By: mbouaziz
Differential Revision: D9217176
fbshipit-source-id: 3be463405
Summary: It moves the functions that constructs array values from BufferOverrunSemantics to ArrayBlk and Val modules.
Reviewed By: mbouaziz
Differential Revision: D9194130
fbshipit-source-id: bf040a01a
Summary:
It removes the sizeof function because most of the cases on static types are addressed in the clang frontend.
Depends on D9193802
Reviewed By: mbouaziz
Differential Revision: D9213876
fbshipit-source-id: 0ce2f3749
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:
- changes the `Ondemand` callbacks to take the execution environment instead of a `get_proc_desc` function.
- removes all the cases passing `get_proc_desc` as parameter to use `Ondemand.get_proc_desc` instead.
Reviewed By: jvillard
Differential Revision: D9200583
fbshipit-source-id: d16c218b5
Summary:
Some paths are hardcoded in infer as being relative to the current executable,
for instance the directory where to find the models. By copying infertop.bc to
infer/bin like we do for `infer` these relative paths lead to the expected
place, which means models can be loaded in the toplevel like they would be in a
normal infer execution. This is more useful for debugging than previously.
Reviewed By: jeremydubreil, mbouaziz
Differential Revision: D9197142
fbshipit-source-id: 48c4f82fb
Summary:
Using the proc name directly should be equivalent and does not rely on
`Summary` caching summaries for us.
Reviewed By: mbouaziz
Differential Revision: D9196503
fbshipit-source-id: dea67999a
Summary:
We want to kill the cache in `Summary`, and calling `Summary.get` relies on
that cache existing for efficiency. However in this case it's not needed
because we can pass the summary from above instead.
Reviewed By: mbouaziz
Differential Revision: D9195234
fbshipit-source-id: 5b7023242
Summary:
Exposing the in-memory cache seems dangerous. There were only 2 uses anyway:
eradicate and biabduction. I think the biabduction one is safe to remove. The
eradicate one I do not really understand as we return a different summary than
the one we cache... the tests pass though.
Reviewed By: jeremydubreil
Differential Revision: D9150167
fbshipit-source-id: cf30af232
Summary:
This makes sure that the javac_jar is disabled when setting the external compiler option to point at the Infer wrapper
Closes#976
Reviewed By: jvillard
Differential Revision: D9193336
fbshipit-source-id: abafb51fc
Summary:
When we see `pthread_create(..., ..., foo, ...)`, we want to call the function
`foo` to check that its precondition is met. The initial goal was to get rid
of the uncouth call to `Summary.get` when what we really want is to analyse
`foo` instead of just betting on the fact that it has been analysed already.
Besides switching to `Ondemand.analyze_proc_name`, this also changes the
matching of the function pointer in the arguments of `pthread_create()` to
detect the common case of a constant function name. I also added tests.
Reviewed By: jeremydubreil
Differential Revision: D9195159
fbshipit-source-id: dfec79f14
Summary: This should be functionally equivalent but removes one call to `Summary.get`
Reviewed By: jvillard
Differential Revision: D9153924
fbshipit-source-id: d49789d2f
Summary:
Because of the custom formatting we do on top of `Cmdliner.Manpage` in
`CommandLineOption`, the long `$(b,strings inside bold block)` would sometimes
end up split across several lines and then `Cmdliner` complains about the line
ending before having seen the closing parenthesis `)`.
Instead of allowing these long strings, remove then from the help message as
they don't seem very useful to me. Replace them with just a mention of
`--test-determinator` so all the options related to Test Determinator are easy
to look up.
Also change the relevant options from `CLOpt.mk_string` to `CLOpt.mk_path`
because they look like they are supposed to be paths.
Reviewed By: ddino
Differential Revision: D9133505
fbshipit-source-id: d82acf5bf
Summary: This code is no longer necessary because the bug hash does not depend on the name of the anonymous classes
Reviewed By: mbouaziz
Differential Revision: D9176205
fbshipit-source-id: 9a8e9c9f8
Summary: It uses a SymbolPath map to Symbol in Inferbo's summary instead of an entry memory of callee, which is used for instantiations of the abstract memories on function calls.
Reviewed By: mbouaziz
Differential Revision: D9081631
fbshipit-source-id: 478cda0de
Summary: Errors that include temporary variables are difficult to understand. Do not report stack variable address escape on temporary variables.
Reviewed By: jvillard
Differential Revision: D9117517
fbshipit-source-id: 9ebd75ecc
Summary:
Print the following for each source file to analyse in non-interactive mode:
```
path/to/source_file.c starting
[...]
path/to/source_file.c DONE in <time>
```
This should help diagnose when infer is stuck. It also logs this information to
the log file regardless of the form of the progress bar.
Also add a `--progress-bar-style` option to allow the user to force a
particular rendering: plain (as above), multiline (The Glorious One), or auto
(selection depends on whether infer is connected to a TTY on stdin *and*
stderr).
Reviewed By: mbouaziz
Differential Revision: D9120509
fbshipit-source-id: 4b43b7464
Summary: Treat calls to Thread.sleep as blocking, even when the timeouts are less than the ANR limit.
Reviewed By: da319
Differential Revision: D9027950
fbshipit-source-id: 001409896
Summary:
The current message is confusing when the current class is marked UIThread.
See picture attached to task.
Reviewed By: jeremydubreil
Differential Revision: D8996593
fbshipit-source-id: cf52ee5d6
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: This avoid cases where the type definition is not found when trying to lookup the type definition for the class starting from the method name.
Reviewed By: ngorogiannis
Differential Revision: D9027983
fbshipit-source-id: 1add7692f
Summary: Added variant type for statement node to make it cleaner to match a particular statement node.
Reviewed By: mbouaziz
Differential Revision: D8997124
fbshipit-source-id: e19f6eacd
Summary:
Guava subclasses Future in ways that make .get() calls safe from the UI thread.
Treat such methods as skip.
Reviewed By: jeremydubreil
Differential Revision: D9013475
fbshipit-source-id: 38373aa5f
Summary:
Infer does the right thing now, make sure it doesn't regress.
https://github.com/facebook/infer/issues/86
Reviewed By: mbouaziz, dulmarod
Differential Revision: D8442855
fbshipit-source-id: 3df29b88c
Summary:
This previous FP does not occur anymore, make sure it doesn't regress.
https://github.com/facebook/infer/issues/49
Reviewed By: dulmarod
Differential Revision: D8442842
fbshipit-source-id: b3fde1ad1
Summary:
Litho uses an idiom as follows. `Component.Builder` has an abstract method `T getThis()` which is supposed to be implemented as `{return this;}`.
I believe the reason it's there is to have covariant return types in subclasses, though this doesn't really matter.
We don't do dynamic dispatch, so instead of summarising `getThis` as having a return ownership of `OwnedIf({ 0 })` we just return `Unowned`.
This is generating many false positives, which are really hard to debug.
Here I'm special-casing any abstract method whose return type is equal to that of it's only argument, to return conditional ownership.
Reviewed By: da319
Differential Revision: D8947992
fbshipit-source-id: 33c7e952d
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: Exceptional successors were not meant to be created for return nodes, but they were created if try block had a single return statement.
Reviewed By: jvillard
Differential Revision: D8913371
fbshipit-source-id: 6ac85b21d
Summary: This integration rolls out its own parallelisation using `Parmap` and its own error handling. Make it use `Tasks` instead.
Reviewed By: mbouaziz
Differential Revision: D8807109
fbshipit-source-id: ac09b3791
Summary: `IntLit.to_int` could raise, was not documented until recently and was not named `_exn`. Switch to option type and fix uses.
Reviewed By: jeremydubreil
Differential Revision: D8865525
fbshipit-source-id: f5ec2f221
Summary: `ownership_of_expr` is already doing some of the work in `propagate_return`. Also, split and move into abstract domain, where it belongs.
Reviewed By: jeremydubreil
Differential Revision: D8855257
fbshipit-source-id: 7756552d8
Summary:
Currently, some blocking calls are turning up too many false positives. Adjust severities by fix rate/preexisting numbers.
Also, restrict some calls to exact class, as opposed to superclasses.
Reviewed By: mbouaziz
Differential Revision: D8850599
fbshipit-source-id: 47543d04a
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:
When `--reanalyze` is passed, mark the summaries of procedures matching
`--procedures-filter` as needing to be analysed before running the analysis.
This allows one to, for instance, re-run the analysis in debug mode on only
some files or procedures. However, this won't work for the Java Buck
integration since the summaries are hidden away in buck-out.
Reviewed By: mbouaziz
Differential Revision: D8783668
fbshipit-source-id: 9032d83
Summary:
This allows to deduplicate some code related to walking the rows of the results
of a SQLite query. Give more meaningful names to the API while I'm at it.
Reviewed By: mbouaziz
Differential Revision: D8783332
fbshipit-source-id: 4aa6613
Summary: All the rows were wrapped in `Some` but that is not needed anywhere.
Reviewed By: mbouaziz
Differential Revision: D8783310
fbshipit-source-id: b020af3
Summary: Some values in Config.mli were in the wrong section. Also, use ocamldoc formatting for sections.
Reviewed By: mbouaziz
Differential Revision: D8783244
fbshipit-source-id: f9a0729
Summary:
Filtering on the SQLite side was done to be more efficient, but these are debug
options so it should be fine for them to be not very optimised.
Filtering on the OCaml side will allow us to re-use these filtering options for
other purposes, such as re-analysing certain procedures only.
Reviewed By: mbouaziz
Differential Revision: D8767691
fbshipit-source-id: e232660
Summary:
Do no computation of stability abstract state if not explicitly requested via the command line flag.
Also, simplify the reporting.
Reviewed By: jeremydubreil
Differential Revision: D8614885
fbshipit-source-id: 25dd9de
Summary:
Specs do not get invalidated by reactive mode, so we need to delete them all.
Reactive just means that the capture remains valid and the analysis will only
use the freshly captured source files to start the analysis, but all the
dependencies will be re-analysed.
Reviewed By: da319
Differential Revision: D8735171
fbshipit-source-id: dc1eab3
Summary: Do not start with an invalid source file when we can avoid it. Follow up from D8418447.
Reviewed By: jeremydubreil
Differential Revision: D8732168
fbshipit-source-id: 28a183b
Summary:
The addresses of global variables do not need initialisation to exist and be valid as they are part of the code or data segment of the program. This means that taking the address of a global is not in itself a danger for SIOF. However, dereferencing such an address would be. In order to avoid false positives but avoid being too unsound, only ignore them when the address is taken only to set another global. The general case would require a more complicated abstract domain.
Fixes#866
Reviewed By: ngorogiannis
Differential Revision: D8055627
fbshipit-source-id: 92307b2
Summary:
The captured/ directory is not guaranteed to exist when the capture was run without debug mode, but the analysis assumes it will be. So, this crashes infer:
```
infer -- clang -c examples/hello.c
infer -g
```
There's no need for `DB.Results_dir.init` to create infer-out and infer-out/specs/ since this is now done in `ResultsDir`.
Reviewed By: jeremydubreil
Differential Revision: D8732739
fbshipit-source-id: aaac902
Summary: Otherwise the dead code checker sometimes crashes with a not-totally-related error.
Reviewed By: mbouaziz
Differential Revision: D8732546
fbshipit-source-id: 65caabd
Summary:
These just point to expressions that we know how to translate.
Fixes#950
Reviewed By: mbouaziz
Differential Revision: D8713784
fbshipit-source-id: 9eafa39
Summary: The frontend got better and now `assert` is correctly translated.
Reviewed By: dulmarod
Differential Revision: D8731877
fbshipit-source-id: ba11b0c
Summary: This was showing up during memory profiling with statistical-memprof. The surrounding code shows that we are trying not to allocate if nothing changes, but the `List.map` in the middle would defeat that.
Reviewed By: ngorogiannis
Differential Revision: D8661763
fbshipit-source-id: d44f7a7
Summary: This is make the callbacks are always set instead of silently returning `None`
Reviewed By: ngorogiannis
Differential Revision: D8651971
fbshipit-source-id: 7cd1c02
Summary: One step towards elminating the unsafe cache of procedure summaries in `Summary` and only rely on the one in `Ondemand`
Reviewed By: dulmarod, jvillard
Differential Revision: D8619782
fbshipit-source-id: 4096390
Summary:
This was spammy, especially for errors which we already know about and are
caught by the frontend (then the error message would be displayed about a
translation error without context about what the error was).
Reviewed By: dulmarod
Differential Revision: D8640145
fbshipit-source-id: 8b8b8a7
Summary:
The motivation is in a following diff: ensuring symbols do not cross procedure boundaries.
- This diff rewrites `Bound.subst` to be based on the substituted bound rather than folding on the symbol map.
- This way we are sure all symbols are substituted and no symbols from another procedure remains in the result.
- All cases from the previous version should still be here, I think I added a few constant approximations of minmax substituted with minmax (that would be return Top).
Side-effects (good):
- `mult_const` has also more constant approximations for minmax,
- substitution should be faster
Reviewed By: jvillard
Differential Revision: D8369993
fbshipit-source-id: 6ed8be8
Summary:
This changes the behaviour back to before the "fork once then pipe new tasks
for each source files" era: before that we would fork once per source file,
which had the effect of emptying the caches for every source file. Without this
the caches can grow unchecked.
This is probably suboptimal but should at least be the same behaviour as before.
Reviewed By: jeremydubreil
Differential Revision: D8615124
fbshipit-source-id: 69fc101
Summary:
- Do not add actuals of a call as unstable.
- Replace access trie with simple set of paths, which is easier to debug/argue correct.
- Fix bug where a prefix path was searched, as opposed to a *proper* prefix.
- Restrict interface to the minimum so that alternative implementations are easier.
Reviewed By: ilyasergey
Differential Revision: D8573792
fbshipit-source-id: 4c4e174
Summary: This prevents the task bar from scrolling the terminal in case the lines are not wide enough. Instead it will truncate the display to the terminal size. Also display only the most useful info when there is not much room.
Reviewed By: jeremydubreil
Differential Revision: D8590580
fbshipit-source-id: e12d5c9
Summary: `make deadcode` complains about circular dependencies but it works. Document mystery and remove dead code that was introduced while the tests were broken.
Reviewed By: da319
Differential Revision: D8590961
fbshipit-source-id: b52e290
Summary:
Previously we would block indefinitely waiting for that child to send us an
update. Now errors in the child are caught and the main process dies, taking
everyone down with it.
When a child dies, it sends a "Crash" message to the parent, unless it died
receiving a signal (like a segmentation fault, or an external signal). In that
case, the OCaml runtime won't get a chance to notice its death and send the
"Crash" message. Thus, always check if some child has died from under us as
well.
Reviewed By: mbouaziz
Differential Revision: D8577095
fbshipit-source-id: 519992b
Summary: C/C++ code can, in some cases, generate a large number of temporary (Sil) variables. Since we are already not reporting races on these, not recording them gives some perf back.
Reviewed By: mbouaziz, jvillard
Differential Revision: D8566999
fbshipit-source-id: 148ac46
Summary: Trying to convert a large int literal to an OCaml int raises an exception. The use case here actually needed a float anyway, so add an API for that.
Reviewed By: jeremydubreil
Differential Revision: D8550410
fbshipit-source-id: 382495b
Summary:
We inline the .ml and the .mli together using the .cmi rule (for reasons
explained in the Makefile of deadcode). This relies on the fact that rules will
start from the .cmx, which in turns depends on the .cmi as the last dependency
and so all the dependencies of the .cmx are satisfied by the time we hit the
.cmi. But that doesn't always work.
For some reason, making the .cmi depend on its .cmx works, even though it's
supposed to include a circular dependency (`make` should complain but doesn't).
Oh, well...
Reviewed By: jeremydubreil
Differential Revision: D8548032
fbshipit-source-id: 0dc9335
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:
The execution environment is really just a cache. It happens to point to a
particular source file which is where the analysis was started from, but that
is not relevant, and in fact is confusing because it suggests that it is
somewhat tied to that file. In reality, exe_env caches information about any
procedure and source file encountered by the analysis.
This will make it easier to make further changes but I think it also brings a
bit more clarity to the code.
Reviewed By: jeremydubreil
Differential Revision: D8513735
fbshipit-source-id: f4b38ce
Summary: Record that it is not supported: https://github.com/facebook/infer/issues/8
Reviewed By: mbouaziz, dulmarod
Differential Revision: D8442762
fbshipit-source-id: fa271cb
Summary: This makes more sense and avoids printing a pointless backtrace. Give the user some advice while we're at it.
Reviewed By: mbouaziz
Differential Revision: D8442711
fbshipit-source-id: 65a8939
Summary: It's been deprecated for a while now. Use `infer analyze` instead.
Reviewed By: dulmarod
Differential Revision: D8442682
fbshipit-source-id: 0b8c590
Summary:
I realized that control variable analysis was broken when we had multiple back-edges for the same loop. This is often the case when we have a switch statement combined with continue in a loop (see `test_switch` in `switch_continue.c`) or when we have disjunctive guards in do-while loops.
This diff fixes that by
- defining a loop by its loophead (the target of its backedges) rather than its back-edges. Then it converts back-edge list to a map from loop_head to sources of the loop's back-edges.
- collecting multiple guard nodes that come from potentially multiple exit nodes per loop head
In addition, it also removes the wrong assumption that an exit node belongs to a single loop head.
Reviewed By: mbouaziz
Differential Revision: D8398061
fbshipit-source-id: abaf288
Summary: Code auto generated by annotation processors or by the compiler is creating non-actionable reports, so skip it for now.
Reviewed By: jeremydubreil
Differential Revision: D8395781
fbshipit-source-id: 9832814
Summary:
The deadlock reports (the actual string) were too low level, in order to avoid bug hash clashes. Now that we deduplicate this is less of an issue, so it's an opportunity to improve readability.
```
Potential deadlock.
Trace 1 (starts at `void Interproc.interproc1Bad(InterprocA)`) first locks `this` in class `Interproc*` (line 9 in `void Interproc.interproc1Bad(InterprocA)`) and then locks `b` in class `InterprocA*` (line 14 in `void Interproc.interproc2Bad(InterprocA)`).
Trace 2 (starts at `void InterprocA.interproc1Bad(Interproc)`), first locks `this` in class `InterprocA*` (line 37 in `void InterprocA.interproc1Bad(Interproc)`) and then locks `d` in class `Interproc*` (line 42 in `void InterprocA.interproc2Bad(Interproc)`).
```
Reviewed By: mbouaziz
Differential Revision: D8395399
fbshipit-source-id: b4bb48c
Summary:
We need to report on non-private methods (the opposite even leads to FPs sometimes on deadlocks). To do this, the domain needs to change so that the interpretation of an order pair `a,b` is no longer "lock `a` is taken in the *current method* and held until lock `b` is taken". Instead the meaning is now "lock `a` is taken in some method *of the same class with the current method* and is held until `b` is taken".
These changes are quite drastic because the previous implementation optimised extensively around the previous use case.
Reviewed By: mbouaziz
Differential Revision: D8395351
fbshipit-source-id: a2bd22b
Summary:
The deadlock reports (the actual string) were too low level, in order to avoid bug hash clashes. Now that we deduplicate this is less of an issue, so it's an opportunity to improve readability.
```
Potential deadlock.
Trace 1 (starts at `void Interproc.interproc1Bad(InterprocA)`) first locks `this` in class `Interproc*` (line 9 in `void Interproc.interproc1Bad(InterprocA)`) and then locks `b` in class `InterprocA*` (line 14 in `void Interproc.interproc2Bad(InterprocA)`).
Trace 2 (starts at `void InterprocA.interproc1Bad(Interproc)`), first locks `this` in class `InterprocA*` (line 37 in `void InterprocA.interproc1Bad(Interproc)`) and then locks `d` in class `Interproc*` (line 42 in `void InterprocA.interproc2Bad(Interproc)`).
```
Reviewed By: mbouaziz
Differential Revision: D8394978
fbshipit-source-id: 671ccb0
Summary:
The deadlock reports (the actual string) were too low level, in order to avoid bug hash clashes. Now that we deduplicate this is less of an issue, so it's an opportunity to improve readability.
```
Potential deadlock.
Trace 1 (starts at `void Interproc.interproc1Bad(InterprocA)`) first locks `this` in class `Interproc*` (line 9 in `void Interproc.interproc1Bad(InterprocA)`) and then locks `b` in class `InterprocA*` (line 14 in `void Interproc.interproc2Bad(InterprocA)`).
Trace 2 (starts at `void InterprocA.interproc1Bad(Interproc)`), first locks `this` in class `InterprocA*` (line 37 in `void InterprocA.interproc1Bad(Interproc)`) and then locks `d` in class `Interproc*` (line 42 in `void InterprocA.interproc2Bad(Interproc)`).
```
Reviewed By: mbouaziz
Differential Revision: D8379328
fbshipit-source-id: bc33983
Summary: Deadlocks can be very noisy, so dedup reports on same line by showing only the one with the shortest trace and a count of the suppressed ones.
Reviewed By: mbouaziz
Differential Revision: D8351148
fbshipit-source-id: 8913db2
Summary: We were missing reads of `a` if it was used in void cast, i.e. `(void) a;` This caused dead store false positives: we were not using `exp` that was the result of translating `a`. This diff creates a call to built-in skip function with `exp` as its argument, which causes the analyses to see reads of `exp`.
Reviewed By: mbouaziz
Differential Revision: D8332092
fbshipit-source-id: f3b0e10
Summary: Removing an internal error in SIL to HIL translation which I had added before to log how often the particular case was happening. It happens quite often, and I have a task to investigate the issue. Removing it as it spams the analysis output a lot.
Reviewed By: dulmarod
Differential Revision: D8316822
fbshipit-source-id: 4047cbe
Summary: Introduce an annotation that forces the summary of a method to be free of blocking events, without suppressing other reports.
Reviewed By: jeremydubreil
Differential Revision: D8276787
fbshipit-source-id: be9eed8
Summary: I don't understand what this function is for. Let's remove it.
Reviewed By: mbouaziz
Differential Revision: D8320839
fbshipit-source-id: eeb14f7
Summary: The case of nullable properties was already working but there was no test for it.
Reviewed By: dulmarod
Differential Revision: D8266468
fbshipit-source-id: c074d69
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: There is a number of dangling pointer dereference false positives coming from our treatment of union in c/cpp. For now, do not treat union fields as uninitialised.
Reviewed By: mbouaziz
Differential Revision: D8279802
fbshipit-source-id: a339b0e
Summary: We get a lot of false positives for union types as union fields are treated as separate memory locations at the moment. For now we do not treat union fields as uninitialised.
Reviewed By: mbouaziz
Differential Revision: D8277363
fbshipit-source-id: efe5b4a
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:
Use the component of the abstract state `events` to report. This set contains reachability facts about blocking calls and lock acquisitions.
The other component, `order`, contained pairs of a reachable event `e'` from an event option with the semantics that if the option is `None` then we have an element that now goes into `events`, and if the option is `Some e` then the element represents a lock acquired and a trace *from* `e` to `e'`
Now, `order` can be simplified to proper pairs of events, without the option.
Reviewed By: jvillard
Differential Revision: D8227665
fbshipit-source-id: e6f4dac
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
Summary:
It's useful to test that the bucket a given error is classified as doesn't
change over time without notice.
This records the bucket for *all* the tests, even though some never produce a
bucket. This is to be on the safe size instead of risking to forget adding the
bucket information when the test changes, or when copy/pasting from a test that
doesn't have buckets to one that does.
The implementation is pretty crude: it greps the beginning of the qualifier
string for a `[bucket]`.
Reviewed By: mbouaziz
Differential Revision: D8236393
fbshipit-source-id: b3b1eb9
Summary: That name doesn't make sense anymore and could be confusing.
Reviewed By: mbouaziz
Differential Revision: D8235507
fbshipit-source-id: b6a6e71
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: To simplify things, have a separate set of simple trace->event elements. Currently this is not used for reporting, in preparation for another diff.
Reviewed By: mbouaziz
Differential Revision: D8203721
fbshipit-source-id: ecc8bae
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: In preparation for allowing unbalanced locking, we need the lock state in the summary.
Reviewed By: mbouaziz
Differential Revision: D8201932
fbshipit-source-id: 05a1b38
Summary:
Preparing for the future change, we won't see instructions as lists but as an abstract type.
This change may be a very minor perf regression: does a few more (but bounded by a constant) instructions traversals only for the nodes involving a Printf-like function call, only for the PrintfArgs checker...
Reviewed By: jvillard
Differential Revision: D8094124
fbshipit-source-id: e2e2c5e
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: In preparation to change the underlying module structure so as to allow three-point traces (call-site, intermediate call-site and endpoint), rename modules to better reflect function plus use records vs pairs of pairs :P
Reviewed By: mbouaziz
Differential Revision: D8187369
fbshipit-source-id: ed3e4ac
Summary:
There can be multiple reports per line, especially when calling in a method which has itself multiple reports.
When reporting at the callsite, report only the issue with the highest severity (picked manually per type of event).
Deadlocks are not de-duplicated, as they are relatively rare and the info in mupltiple reports may be important.
Reviewed By: mbouaziz
Differential Revision: D8160940
fbshipit-source-id: ea6a5c0
Summary:
The main motivation is preparing for a future change.
This also reduces lifetime of potential garbage.
Reviewed By: jeremydubreil
Differential Revision: D8185648
fbshipit-source-id: 6d0a568
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:
Rely on the underlying CFG preds:
- perf: no need to append lists
- correctness: the underlying CFG may be removing duplicates
Reviewed By: ngorogiannis
Differential Revision: D8185638
fbshipit-source-id: 3b6f70a
Summary:
- do not `List.rev` for `List.last`
- `List.rev_filter_map` rather than `filter |> map |> rev`
Reviewed By: da319
Differential Revision: D8185619
fbshipit-source-id: aeb41a4
Summary: The order of nodes means nothing, and should not matter, let's save the whales!
Reviewed By: ngorogiannis
Differential Revision: D8182137
fbshipit-source-id: bc14a2c
Summary:
Moving away from C++ include-based models means that we cannot reliably detect
anymore whether a file includes <iostream> or not. In order not to be too
spammy, let's always assume standard streams are initialized for now when the
include models are off.
Recent versions of libstdc++ make these models redundant so there is hope that in a
bright future the analysis of std streams initialisation will work correctly without infer
having to have its own models anyway.
Reviewed By: mbouaziz
Differential Revision: D8043467
fbshipit-source-id: d118043
Summary: Prevent the analysis to default to absolute paths which would invalidate the cache.
Reviewed By: mbouaziz
Differential Revision: D6997490
fbshipit-source-id: 3c17658
Summary: We want both pointer and pointer dereference to be uninitialised at the beginning. Forgot to add the expression of type pointer when updating the analysis from access paths to access expressions.
Reviewed By: ddino
Differential Revision: D8117011
fbshipit-source-id: 534f7ef
Summary: Set arguments of pointer type as initialised for indirect function calls.
Reviewed By: mbouaziz
Differential Revision: D8097895
fbshipit-source-id: 830f568
Summary: Track and surface the reasons why a method is assessed to run on the UI thread.
Reviewed By: mbouaziz
Differential Revision: D8096099
fbshipit-source-id: 2403c6c
Summary:
The reported location was always the start of the enclosing procedure, which is wrong in many ways.
A nice side-effect is that some code can then be eliminated and Ondemand.analyze used, avoiding getting the procdescs in the process.
Reviewed By: jeremydubreil
Differential Revision: D8056306
fbshipit-source-id: 67c2c8d
Summary: Treat array accesses as initialised if they are passed by reference.
Reviewed By: jvillard
Differential Revision: D8071247
fbshipit-source-id: 5480e90
Summary: The type of array element is not preserved correctly in the translation from SIL to HIL. When array element is passed by a reference, i.e. `f(&(array[0]))`, the type of array element gets the type of a pointer of array element.
Reviewed By: jvillard
Differential Revision: D8071188
fbshipit-source-id: 3e6635e
Summary:
The deadcode checker is poorly written and as a result is more useful than
intended!
Reviewed By: mbouaziz
Differential Revision: D8088654
fbshipit-source-id: 19a94b8
Summary: Use AccessExpressions instead of AccessPath in uninit analysis. This will allow us to distinguish between pointers and their dereferences.
Reviewed By: jvillard
Differential Revision: D8042359
fbshipit-source-id: 604bcbc
Summary:
It improves the precision of widening operations of interval:
upper_bound_widen (min(n, s), s) = s
lower_bound_widen (max(n, s), s) = s
Reviewed By: mbouaziz
Differential Revision: D8038941
fbshipit-source-id: 61b10cb
Summary:
Labels inside switch statements were causing havoc (see test), and the translation of switch statements in general could be improved to handle more cases.
It turns out that `case` (and `default`) statements are more or less fancy labels into the code. In other words, if you erase all the `case XXX:` and `default:` strings in the `switch` statement you get the real structure of the program, and `switch` just jumps straight to the first `case` directives (and to the second if the first one is not satisfied, etc. until all `case`/`default` have been considered).
This suggests an alternative implementation: translate the body of the `switch` and simply record the list of switch cases inside that body, along with where they point to. Then post-process this list to construct the control flow of the `switch`, which points into the control-flow of the `body`. In order not to modify every function in `CTrans` to propagate the current list of cases, I created an ugly `ref` inside `SwitchCase` instead (but it cannot be directly accessed and it's guaranteed to be well-parenthesised wrt nested switches by the `SwitchCase` API so it's not too bad).
[unrelated] Also make translation failures output more information about what exactly in the source code is causing the crash, and the ancestors in the AST that lead to the crash site.
Reviewed By: martinoluca
Differential Revision: D8011046
fbshipit-source-id: 8455090
Summary: Moving this function since it's about a single procdesc. Slight rewrite too.
Reviewed By: da319
Differential Revision: D8030494
fbshipit-source-id: f7cc58e
Summary:
- Reorder modules in mli for readability.
- Match mli module order in the implementation.
- Move some functions that operate on domains from RacerD.ml to the domain file.
- Kill some module type invocation.
- Use standard module signatures.
Reviewed By: mbouaziz
Differential Revision: D8026386
fbshipit-source-id: ee2af22
Summary: Method overloading creates the potential for report duplication even though the reports are actually distinct. Make the report message unique by not using shortened method names.
Reviewed By: jeremydubreil
Differential Revision: D8005862
fbshipit-source-id: 53d8ea0
Summary: Follow C++ in having local variables owned plus silence reports on paths rooted on logical vars. We need both because when propagating ownership from right to left, the initial status of a temp var as owned is lost.
Reviewed By: sblackshear
Differential Revision: D7988575
fbshipit-source-id: 2e817d7
Summary: There was a bit of code and comments referring to potential soundness. Kill those.
Reviewed By: da319
Differential Revision: D8004256
fbshipit-source-id: c20b62a
Summary:
Preparing for bigger changes...
- Rename `payload` field to `payloads`
- Move `payload` type to `Payloads.t`
- `SummaryPayload`s only have to implement a change on `Payloads.t` rather than `Summary.t`
Reviewed By: sblackshear
Differential Revision: D7987211
fbshipit-source-id: c9d7a74
Summary: Fixing the support for single core analysis in 8ce79a0613 was improving the performance of the genrule-based integration by more that 2X. Running Infer in single core more with the external compiler integration for Buck also improves the performance significantly.
Reviewed By: mbouaziz
Differential Revision: D7989255
fbshipit-source-id: 71fb842
Summary:
This diff:
- translates C++ `catch` blocks
- adds an exceptional control-flow edge from the end of a `try` block to the beginning of a `catch` block
This obviously doesn't reflect the way exceptions actually work, but I think it is better than what we have now. For one thing, we'll see/translate code inside `catch` blocks, which were opaque before. If Clang analyses don't want this behavior, they can simply use `ProcCfg.Normal` (which, up until this diff, behaved identically to `ProcCfg.Exceptional`.
In the future, we can extend `trans_state` to track blocks that might throw an exception, and have each of these blocks transition to `catch` instead.
Reviewed By: jvillard
Differential Revision: D7814521
fbshipit-source-id: 67b86a6
Summary:
- delete getter for `CContext.context.procdesc`
- change API of `CLocation`, in particular to take just a source file instead of a `CContext` since that's all they need (but maybe we'd rather type less?)
- thread `source_range` of source statement to where useful for logging (could do more in the future)
Reviewed By: da319
Differential Revision: D7950573
fbshipit-source-id: 2755f7d
Summary: Makes sense given that they share a lot of the same `Intent`-related sinks.
Reviewed By: mbouaziz
Differential Revision: D7877282
fbshipit-source-id: 38b2040
Summary:
Before we were computing the size of an abstract state (`range`) using the `NonNegativeBound` domain but it wasn't able to express product of symbolic values.
This diff introduces a domain for that.
The range of an interval is still computed in `NonNegativeBound` but then the product is done in `TopLiftedPolynomial` so all costs end up being of that type.
The //symbols// of a polynomial are `NonNegativeBound` (so the polynomial only represent non-negative values, perfect for a cost), which handles substitution correctly, i.e. it gives zero instead of negative values.
Reviewed By: ddino
Differential Revision: D7397229
fbshipit-source-id: 6868bb7
Summary:
The annotation UiThread can, and is, used on classes as opposed to just methods, so extend the modelling to account for this.
Also, consider the annotation hereditary.
Reviewed By: jeremydubreil
Differential Revision: D7910762
fbshipit-source-id: 0df2c81
Summary:
Java arrays have an internal length that can be retrieved with the internal `__get_array_length`.
Here is a model for it.
Reviewed By: jvillard
Differential Revision: D7931572
fbshipit-source-id: fd4c179
Summary:
Attempt at a better naming scheme:
- `Specs.summary` are now `Summary.t`. The `Summary` module (replacing `Specs`) contains the summary of a procedure: the results of all the analyses, etc.
- `Summary.ml` is now `SummaryPayload.ml`. This concerns how each (AI) analysis extracts its payload from the master summary.
- Accordingly, checkers now define a `Payload` module where previously they defined a `Summary` module. The type is also cleaned up to use `t` instead of `payload`, etc.
- Cleaned up some names as a result, for instance `Specs.get_summary` -> `Summary.get`, etc.
Reviewed By: ngorogiannis
Differential Revision: D7935883
fbshipit-source-id: 1766545
Summary:
Move the biabduction-specific payloads (the "`'a spec`" stuff) from specs.ml
into a new `BiabductinoSummary` module, similar to other checkers.
Reviewed By: ngorogiannis
Differential Revision: D7935815
fbshipit-source-id: bdff3b9
Summary:
Previously, the type of `trans_result` contained a list of SIL expressions.
However, most of the time we expect to get exactly one, and getting a different
number is a soft(!) error, usually returning `-1`.
This splits `trans_result` into `control`, which contains the information
needed for temporary computation (hence when we don't necessarily know the
return value yet), and a new version of `trans_result` that includes `control`,
the previous `exps` list but replaced by a single `return` expression instead,
and a couple other values that made sense to move out of `control`. This allows
some flexibility in the frontend compared to enforcing exactly one return
expression always: if they are not known yet we stick to `control` instead (see
eg `compute_controls_to_parent`).
This creates more garbage temporary identifiers, however they do not show up in
the final cfg. Instead, we see that temporary IDs are now often not
consecutive...
The most painful complication is in the treatment of `DeclRefExpr`, which was
actually returning *two* expressions: the method name and the `this` object.
Now the method name is a separate (optional) field in `trans_result`.
Reviewed By: mbouaziz
Differential Revision: D7881088
fbshipit-source-id: 41ad3b5
Summary: When passing `--genrule-mode` option, Infer will remove the logs and the other kind of data that are not compatible with the Buck distributed cache.
Reviewed By: mbouaziz
Differential Revision: D7943346
fbshipit-source-id: 4e7ca4d
Summary: With the genrule approach, the directory the generated script is run from is inside `buck-out`. So we need to specify the project root before calling the `buck` command.
Reviewed By: mbouaziz
Differential Revision: D7938130
fbshipit-source-id: c265476
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: Make errors stand out with colours. Also improve error messages around save states.
Reviewed By: mbouaziz
Differential Revision: D7928794
fbshipit-source-id: c81cfe2
Summary: Without the class name, it is not always clear from the error message where the method expecing non-null parameters defined.
Reviewed By: mbouaziz
Differential Revision: D7919492
fbshipit-source-id: 044fb83
Summary: I needed it for debugging but, to my dismay, it was borked again. This time it was because `jbuilder` moved the object files to another directory since the last jbuilder update.
Reviewed By: mbouaziz
Differential Revision: D7926267
fbshipit-source-id: 42ad26a
Summary:
Make the starvation checker enabled by default.
Add a deadlock issue type, distinct to starvation, which will be kept for UI thread starvation.
Add checks so that checker will do nothing on non-Java code.
Reviewed By: mbouaziz, ddino
Differential Revision: D7908381
fbshipit-source-id: 889f373
Summary: Historically, this option was only used to parallelize the biabduction analysis, which is now run using the checkers framework.
Reviewed By: jvillard
Differential Revision: D7895118
fbshipit-source-id: 2a54bca
Summary: Calling Future.get from UI thread, or under a lock the UI thread may try to take has been associated with ANRs.
Reviewed By: ddino
Differential Revision: D7859296
fbshipit-source-id: b87bd94
Summary:
One source of non-determinism is racing on procedure summaries when reporting. In particular, the summary of a method may be computed and stored by one thread, but another may be trying to report on it (eg, in cluster checkers).
One solution (at least until everything is in sqlite) is to have separate files just for the reports, a la linters. This diff improves the interface of LintIssues and generalises it ahead of using it in other analysers.
Reviewed By: jeremydubreil
Differential Revision: D7859973
fbshipit-source-id: 8672d3b
Summary: Folly has a macro SYNCHRONIZED(..) {...} which boils down to the creation/destruction of a LockedPtr object, doing the locking/unlocking. Add support for that.
Reviewed By: sblackshear
Differential Revision: D7844847
fbshipit-source-id: c7a146d
Summary: std::lock allows for locking multiple lockable objects, while avoiding deadlock. This will fix some FPs in C++.
Reviewed By: da319
Differential Revision: D7844198
fbshipit-source-id: 2b7140a
Summary:
We had a semantics for ownership of prefix paths in mind (see comment), but it was enforced partially in the domain and partially in the transfer functions.
Moving all of the logic into the domain makes things much cleaner/shorter.
Reviewed By: ngorogiannis
Differential Revision: D7845981
fbshipit-source-id: 4a2da95
Summary:
The Cost analysis uses `Bound` for non-negative values only, let's make it a separate module (and abstract type).
This also separates the abstract domain part of `Bound` which we wanted anyway.
Depends on D7844267
Depends on D7843351
Depends on D7782184
Reviewed By: ddino
Differential Revision: D7844572
fbshipit-source-id: 0e6b620
Summary: We were wrongly using the underapproximation of `min` rather than the overapproximation
Reviewed By: ddino
Differential Revision: D7844267
fbshipit-source-id: c9d9247
Summary:
This simplifies the frontends and backends in most cases. Before this diff,
returning `void` could be modelled either with a `None` return, or a dummy
return variable with type `Tvoid`. Now it's always the latter.
Reviewed By: sblackshear, dulmarod
Differential Revision: D7832938
fbshipit-source-id: 0a403d1
Summary:
The abstract interpreter tried to handle exceptional control-flow by propagating the *pre* of a block that threw an exception rather than the *post*.
This was a half-measure that isn't correct when an exception-throwing instruction isn't in the middle of a block.
The handling of exceptions wasn't actually used anywhere and was leading to further hacks in `ProcCfg`, so let's get rid of it.
Reviewed By: mbouaziz, jvillard
Differential Revision: D7843872
fbshipit-source-id: 2a4a815
Summary: Returning the list of sub-expressions is not right and can cause assertion failures elsewhere in the frontend.
Reviewed By: dulmarod
Differential Revision: D7813493
fbshipit-source-id: 33ac9c1
Summary: It's useful for client analyses to be able to see which methods a type defines.
Reviewed By: jvillard
Differential Revision: D7813582
fbshipit-source-id: 675c041
Summary:
Needed to prevent a circular dependency between `CProcname` and `CType_decl`.
An upcoming diff will introduce a function for getting all the methods from a struct that requires both modules.
Reviewed By: dulmarod
Differential Revision: D7813367
fbshipit-source-id: b049d36
Summary: Extracting function from `get_struct_fields` and making it work for everything in the AST.
Reviewed By: jvillard
Differential Revision: D7813040
fbshipit-source-id: 082f087
Summary:
This required a translation unit context, but really all it needs is a bool specifying whether the procname is a cpp name.
Makes it easier to call this function from a place where I'll need it in the near future.
Reviewed By: jvillard
Differential Revision: D7812835
fbshipit-source-id: 7900893
Summary:
Add warning 60 (unused module) to the list of fatal warnings. Whitelisting
modules at toplevel is tricky (see inline comments) but doable.
Reviewed By: mbouaziz
Differential Revision: D7790073
fbshipit-source-id: 6f591c4
Summary:
Previously, the command parsing code filtered out any elements that were `False`y in the Python sense (starting with D5507925).
This meant that a command like `javac -classpath '' -Xmaxerrs 1000 MyFile.java` would be parsed as `javac -classpath -Xmaxerrs 1000 MyFile.java`, which will fail with "unrecognized option 1000".
This diff removes the filtering and fixes that issue.
Reviewed By: jeremydubreil
Differential Revision: D7797560
fbshipit-source-id: 63df06b
Summary:
Now that we have the abstract state at the instruction level, we don't need to reexecute instructions during the checking phase and can just query the invariant map.
Depends on D7608526
Reviewed By: skcho
Differential Revision: D7775889
fbshipit-source-id: be17e2d
Summary: Easy simplification now that we have a set of access snapshots.
Reviewed By: ngorogiannis
Differential Revision: D7754720
fbshipit-source-id: 91d0bd7
Summary:
Add a `--source-files` option to `infer explore` to print information about the source files captured by infer.
More precisely, `infer explore --source-files` will print each row of the "source_files" table in the results database.
Option `--source-files-filter` can be used to filter output to file names matching an SQLite "LIKE" pattern.
Flags `--source-files-cfgs`, `--source-files-type-environment`, `--source-files-procedure-names` and `--source-files-freshly-captured` control which columns to print.
The printers for some existing types have been tweaked to improve the output.
Reviewed By: jvillard
Differential Revision: D7735535
fbshipit-source-id: 572389a
Summary:
Now that the cost analysis doesn't hackily compute the instruction index, we can make this an abstract type to ensure `List.nth_exn` in `OneInstrPerNode` will not fail.
Depends on D7618320
Reviewed By: sblackshear
Differential Revision: D7628908
fbshipit-source-id: 89e8618
Summary:
We want instr-granular invariant maps so let's use the OneInstrPerNode CFG in the AI analyzers.
This requires specializing the TransferFunctions.
Keep using the normal CFG where we only need node-granular informations.
Depends on D7587241
Depends on D7608526
Reviewed By: sblackshear
Differential Revision: D7618320
fbshipit-source-id: 73918f0
Summary:
Now that we have a proper InstrNode, we can kill `instr_ids`!
Of course:
Depends on D7608526
Reviewed By: sblackshear
Differential Revision: D7618124
fbshipit-source-id: b3609cd
Summary:
When looking at large CFGs, at least in `xdot`, it's often difficult to find
the procedure you're looking for. Sorting the proc names puts them in
alphabetical order, which makes searching one procedure easier.
Reviewed By: mbouaziz
Differential Revision: D7758521
fbshipit-source-id: 8e9997f
Summary:
[This is a stepping stone before moving the specs data to sqlite.]
Previously, things worked like this (ignore ObjC):
1. capture & analyse C models
2. capture & analyse C++ models
3. copy C *.specs files to lib/specs/
4. copy C++ *.specs files to lib/specs/
Now it works like this:
1. capture C models
2. capture C++ models
3. analyse both together
4. install *.specs files to lib/specs
Reviewed By: sblackshear
Differential Revision: D7639322
fbshipit-source-id: 58d7c53
Summary:
It works now. Jumping to definition or calling merlin-document on files from
opam libraries doesn't seem to work when several libraries used by infer define
the same module (e.g. string.ml exists in ocaml lib, core_kernel, and base).
Reviewed By: let-def
Differential Revision: D7708218
fbshipit-source-id: 8e74b9b
Summary: Random edits made while reading ZipLib.ml. They're really not interesting, sorry...
Reviewed By: sblackshear
Differential Revision: D7686159
fbshipit-source-id: 19ef1ce
Summary:
Given a difference between two files, return the relevant lines in the new file; a line is relevant when a change took place in it, or nearby. To generate a valid input for this parser, use unix-diff command with the following formatter arguments:
```
diff --unchanged-line-format="U" --old-line-format="O" --new-line-format="N" File1 File2
```
Reviewed By: ezgicicek
Differential Revision: D7385267
fbshipit-source-id: 0cc3143
Summary:
This is to make sure we do not influence the analysis of the models by accident
when a .inferconfig exists in some directory higher up (eg, `$HOME`, infer/,
...).
Reviewed By: sblackshear
Differential Revision: D7686136
fbshipit-source-id: 9a250ff
Summary: It makes sense to run the same prelude and epilogue for `infer analyze` as for `infer run`.
Reviewed By: da319
Differential Revision: D7639363
fbshipit-source-id: 26170c1
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: We already suppress race reports if the field is marked in this way; makes sense to do the same thing for these reports.
Reviewed By: ngorogiannis
Differential Revision: D7589275
fbshipit-source-id: 8f0aeab
Summary:
We were using the "filename" as the key because it's (kinda) unique *and* human
readable, but with the `infer explore --procedures` interface we don't really
need the human readable part anymore, so we can just use the OCaml marshalling
of the pname as the key. The human-readable version (sans unique-fying hash) is
now another column in the table, used to match procedure names in
`--procedures-filter`.
Reviewed By: sblackshear
Differential Revision: D7639158
fbshipit-source-id: e714605
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: Currently when we look for already abduced expression and find an assertion [exp|->strexp:typexp], we use typexp rather than strexp.
Reviewed By: sblackshear
Differential Revision: D7617193
fbshipit-source-id: c089720
Summary:
Now that everything can run at the same time and we have preanalyses, it can be quite hard to read debug sessions.
Here come session names!
Depends on D7607336
Reviewed By: sblackshear
Differential Revision: D7607481
fbshipit-source-id: 676af86
Summary:
- Less `^`
- `pp_print_string` instead of `F.fprintf fmt "%s"`
- and stuff like that
Reviewed By: jvillard
Differential Revision: D7607336
fbshipit-source-id: 5d985ef
Summary:
Use an adhoc type for `StructuralConstraints` instead of hacky `Exp`s.
Also use a cleaner `Node.IdMap` instead of `Int.Map`.
Depends on D7586645
Reviewed By: ddino
Differential Revision: D7587241
fbshipit-source-id: f9d65bb
Summary:
So we can share stuff between analyses using the same CFG and node representation.
Depends on D7586302
Depends on D7586348
Depends on D7568701
Reviewed By: sblackshear
Differential Revision: D7586645
fbshipit-source-id: ed64b2c
Summary:
Run with `SHELL = bash -e -u -o pipefail` to catch many kinds of failures. We
were silently failing during `make install` because of some missing escaping,
and the failure was hidden because it was happening inside a bash `for` loop.
This fixes the escaping issue and makes sure such issues will result in an
error as of now.
Also removes dangerous `find -exec` instances: `find` will `exit 0` event if
some commands failed.
Fixes#887
Reviewed By: mbouaziz
Differential Revision: D7569054
fbshipit-source-id: 542fe50
Summary:
Let's see in later diffs if that's that useful
Instead of rebuilding these modules, let's share them
Reviewed By: sblackshear
Differential Revision: D7586302
fbshipit-source-id: de69b39
Summary:
Try to skip running even `clang -###` when we know there's nothing to capture
in the clang command. Do that by recording in the `ClangCommand.t` whether the
command is pre- or post-running `clang -###`, and apply slightly different
filters in each case. In particular, the filter has to let in more commands
than necessary pre-`clang -###` because the flags are not normalised at that
point.
Also regard `-x cuda` commands as unsupported.
Reviewed By: mbouaziz
Differential Revision: D7584934
fbshipit-source-id: c27bb63
Summary: This will facilitate accessing Inferbo abstract state at the instruction level from the Cost analysis
Reviewed By: ddino
Differential Revision: D7568701
fbshipit-source-id: 84ac648
Summary:
Got rid of `Itv.equal` which was ambiguous and use an abstract boolean type for abstract comparison results
Depends on D7568573
Reviewed By: jvillard
Differential Revision: D7568583
fbshipit-source-id: 0e897e9
Summary:
Convenience function for `prune_eq` with zero (needed for stacked diffs).
Renamed `prune_zero` to `prune_ne_zero` to avoid ambiguity.
Reviewed By: jvillard
Differential Revision: D7568556
fbshipit-source-id: b95ab6d
Summary: Only RacerD uses the Cluster callbacks but we used to compute a lot of things anyway.
Reviewed By: sblackshear
Differential Revision: D7516279
fbshipit-source-id: 22f2b86
Summary:
This information is already available in the trace, and can contain absolute
paths to system includes (or infer's own clang runtime), which confuses the
diff analysis.
Reviewed By: mbouaziz
Differential Revision: D7534609
fbshipit-source-id: 5bd8f8b
Summary:
This can be noticed when the format of the DB changes, and other fun things
like that. No longer require to `make clean` to be able to pass these tests.
Reviewed By: mbouaziz
Differential Revision: D7533559
fbshipit-source-id: 670cb60
Summary:
It renames `eval_locs` to `eval_arr` and we use it for getting array block values the given input expressions are pointing to. For example, when given a program variable `x` as an input, `eval_arr` returns array blocks that `x` is pointing to, on the other hand, `eval` returns an abstract location of `x`.
Depends on D7471891
Reviewed By: mbouaziz
Differential Revision: D7471915
fbshipit-source-id: b994944
Summary: In the pointer arithmetics, it returns top, if we cannot precisely follow the physical memory model, e.g., (&x + 1).
Reviewed By: mbouaziz
Differential Revision: D7453510
fbshipit-source-id: db8738e
Summary:
It feels risky to me to swallow the `Sys_error` here since this could hide deeper issues with the deserialization of summaries.
This is only used with the Buck Integration for Java when extracting the summaries from the jar files.
Reviewed By: sblackshear
Differential Revision: D7490123
fbshipit-source-id: 68cd556
Summary:
This is unused, but the logic for keeping its value up to date was still alive
and kicking.
I don't know that making use of this flag would be easy: we could just use it
in `Ondemand.should_analyze`, but it would be unsound because a procedure might
need to be re-analysed becauese its dependencies have changed. Since there's
not code to deal with that currently I think it's best to remove it and
re-introduce it when we have some idea how to use it.
Reviewed By: sblackshear, jeremydubreil
Differential Revision: D7444179
fbshipit-source-id: 99a1ec5
Summary:
Report nullable inconsistencies by relying on the bytecode, and not on the presence of analysis summary on disk.
This use the `--external-java-packages` to avoid reporting inconsistencies outside of the codebase.
Reviewed By: sblackshear
Differential Revision: D7481101
fbshipit-source-id: 281135d
Summary:
Utility function that's basically `Logging.progress` but with a more obvious
name for debugging.
The `[@deprecated ...]` ensures no uses gets landed, and the `[@warning "-32"]` ensures that it's not a compile error that there are no uses of this function.
Inspired by #716.
Reviewed By: mbouaziz
Differential Revision: D7443224
fbshipit-source-id: e94798f
Summary:
Without it `make` will not rebuild infer when "infer/src/infer.ml" changes
(since D7381842 moved it out of backend/).
Reviewed By: mbouaziz
Differential Revision: D7443275
fbshipit-source-id: 33ea10b
Summary:
Partial revert of a21644685f / D7381857 due to an
issue introduced in 1.0+beta19 that prevents jbuilder from generating the
correct .merlin (https://github.com/ocaml/dune/issues/657).
Reviewed By: mbouaziz
Differential Revision: D7414970
fbshipit-source-id: 10561e9
Summary:
It's already turned of systematically for the Java integration, this just
generalises it. The Buck daemon seems to cause issues with infer from time to
time that are hard to debug.
Reviewed By: jeremydubreil
Differential Revision: D7400068
fbshipit-source-id: f05ee07
Summary:
Looks like the remaining issues were solved. In particular, build the toplevel
with the same ppx as infer so that the ppx information makes it to .merlin.
Reviewed By: mbouaziz
Differential Revision: D7381857
fbshipit-source-id: 5847d56
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:
If an aggregate `a` has a field `f` whose type has a constructor (e.g., `std::string`), we translate creating a local aggregate `A { "hi" }` as `string(&(a.f), "hi")`.
This diff makes sure that we recognize this as initializing `a`.
Reviewed By: jeremydubreil
Differential Revision: D7404624
fbshipit-source-id: 0ba90a7
Summary:
New command line option job-id meant to contain the Sandcastle job id
itslog
- New command line option job-id meant to contain the ID of the job that Infer is running in
- If the id is passed to infer, then log it with every row in EventLogger
Reviewed By: dulmarod
Differential Revision: D7398537
fbshipit-source-id: c5186e9
Summary: - No need to log the string of stats type when registering a perf Epilogue
Reviewed By: dulmarod
Differential Revision: D7398544
fbshipit-source-id: 681a956
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:
- Time only stats are now reported from the driver for
- TotalFrontend
- TotalBackend
Reviewed By: dulmarod
Differential Revision: D7382161
fbshipit-source-id: 6e34ca2
Summary:
- PerfStats can now directly compute the filename / relative path of the stats to be logged
- There is no longer a need to pass in the filename as a parameter, simplifying the API to just be a one-liner
Reviewed By: dulmarod
Differential Revision: D7381886
fbshipit-source-id: e6623c3
Summary: `stats_type` can just include a `SourceFile.t`, as the existence of a `source_file` parameter previously depended on the value of `stats_type` anyway
Reviewed By: dulmarod
Differential Revision: D7381605
fbshipit-source-id: 953ee27
Summary:
`Bottom` is only useful for unreachable code detection, which is already handled.
Let's not check `Bottom` states.
Depends on D7289084
Reviewed By: skcho
Differential Revision: D7289153
fbshipit-source-id: 8333ce7
Summary:
Infer reads the arguments passed to clang, in particular to filter out some
incompatible clang command-line options. But, infer only understands arguments
in arg files if they are presented one per line. That's usually the case, but
infer itself stores clang arguments from compilation databases all on one line.
This breaks filtering.
This changes the type of compilation database items to a list of arguments, so
that they can be stored one per line when possible.
Also does some cleanup/renamings, and remove trailing `_` from temp file names, eg:
clang_command_.tmp.2b2602.txt -> clang_command.tmp.2b2602.txt
Also, do not escape arguments from arg files when printing them in logs (that
was useless and ugly).
Reviewed By: mbouaziz
Differential Revision: D7365907
fbshipit-source-id: 5a3fe70
Summary:
The goal is not to end up with a deep copy when nothing has changed, as this
puts lots of pressure on the memory.
Reviewed By: mbouaziz
Differential Revision: D7113976
fbshipit-source-id: 1b85ecd
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: This makes the code cleaner, and also makes it easier to look at the type of a var (needed in a successor).
Reviewed By: jeremydubreil
Differential Revision: D7359466
fbshipit-source-id: 5acdb7a
Summary: The "advice" section of the error description does not seem to be used in practice.
Reviewed By: mbouaziz
Differential Revision: D7348815
fbshipit-source-id: 1d7c8c7
Summary:
- InferPrint reports time stats only, logged in `reporting_stats/` as well as a `PerformanceStats` event with `stats_type: reporting`
- Perf reporting can now be registered at one point (with desired start real and cpu times) and triggered later
Reviewed By: dulmarod
Differential Revision: D7332435
fbshipit-source-id: 2e17c7f
Summary:
Perf reporting can now be registered at one point (with desired start real and cpu times) and triggered later
- This is accomplished by storing perf file names in a hashtable mapping to the reporting function
- New `stats_kind` parameter that is either Time, Memory, or TimeAndMemory, where Time requires a Unix.process_times and an Mtime_clock.counter to be passed in, but TimeAndMemory just uses the time from the start of the process.
Reviewed By: dulmarod
Differential Revision: D7337158
fbshipit-source-id: 94699cd
Summary:
Perf reporting can now be registered at one point (with desired start real and cpu times) and triggered later
- This is accomplished by storing perf file names in a hashtable mapping to the reporting function
- New `stats_kind` parameter that is either Time, Memory, or TimeAndMemory, where Time requires a Unix.process_times and an Mtime_clock.counter to be passed in, but TimeAndMemory just uses the time from the start of the process.
Reviewed By: dulmarod
Differential Revision: D7337158
fbshipit-source-id: 3890cc7
Summary:
- PerfStats can now report either time and/or memory stats, by default reporting both
- This is in preparation for adding just time or memory related logging in the future
Reviewed By: mbouaziz, dulmarod
Differential Revision: D7324556
fbshipit-source-id: e265b12
Summary:
Show where the invalidation occurred in the trace.
Should make things easier to understand.
Reviewed By: jeremydubreil
Differential Revision: D7312182
fbshipit-source-id: 44ba9cc
Summary: This was causing false positives when returning the constant integer 0.
Reviewed By: sblackshear
Differential Revision: D7330143
fbshipit-source-id: 45d19dd
Summary: Should be no semantic change, just trying to avoid code duplication.
Reviewed By: jeremydubreil
Differential Revision: D7268588
fbshipit-source-id: 8b00125
Summary: This will make it easier to detect regressions, until we can completely solve the issue with the classpath and change the `No_class_found` exception into a hard failure.
Reviewed By: sblackshear
Differential Revision: D7307464
fbshipit-source-id: eab67fb
Jeremy Dubreil
Mehdi Bouaziz
Dino Distefano
Nikos Gorogiannis
Ezgi Çiçek
Jules Villard
Martino Luca
Martin Trojer
Julian Sutherland
Daiva Naudziuniene
Sungkeun Cho
Katie Ots
Dulma Churchill
Kai Yang
Brandon Kieft
Sam Blackshear
Jose Blanco
Oliver Castillo
Tony Hu
Frédéric Bour
Josh Berdine
Varun Arora