d261f94624
[inferbo] Use algebraic data type for allocsite
...
Summary: It revises the type of Allocsite.t.
Reviewed By: mbouaziz
Differential Revision: D9569574
fbshipit-source-id: 62865a5c8
6 years ago
bdc1ad751d
[eradicate] fix the shaddowing between the annotated signature of the caller and the one of the callee
...
Reviewed By: mbouaziz
Differential Revision: D9565743
fbshipit-source-id: dbccc3879
6 years ago
19c7f0497f
[eradicate] remove commented out code
...
Reviewed By: mbouaziz
Differential Revision: D9566651
fbshipit-source-id: 1c77a92f5
6 years ago
9349f0d6e2
[eradicate] remove the constant flags remove_temps
...
Summary: This flag was always set to `true`
Reviewed By: mbouaziz
Differential Revision: D9512798
fbshipit-source-id: 085e73a4b
6 years ago
808dd8ee91
[Perf] Merge costs report files coming from buck-based analyses
...
Reviewed By: jeremydubreil
Differential Revision: D9540204
fbshipit-source-id: 665271a32
6 years ago
5894258f43
[ownership] do not warn on returning ref to outer local
...
Summary:
Lambdas can capture references to locals of the enclosing method as long as
they are not propagated outside the method. However to keep things simple
always allow them to capture locals of the enclosing method at the price of
some false negatives.
Reviewed By: da319
Differential Revision: D8974434
fbshipit-source-id: 957ae44bd
6 years ago
8e753c2b74
[deadstore] Do not report on __tmp
...
Reviewed By: mbouaziz
Differential Revision: D9482603
fbshipit-source-id: 303b74eb4
6 years ago
40ab73037e
[ocamlformat] upgrade to ocamlformat 0.7
...
Reviewed By: mbouaziz
Differential Revision: D9496601
fbshipit-source-id: 83c6fd241
6 years ago
060924adff
[inferbo] Get rid of condition trace for proof obligations in summary
...
Summary:
- Was not used by the caller
- Gives smaller summaries
- Will allow adding a intra-proc info, e.g. `node` for reporting (not sure yet)
Reviewed By: skcho
Differential Revision: D9373763
fbshipit-source-id: 322001b53
6 years ago
b4b54025bf
Remove C++ mutex DOUBLE_LOCK checker
...
Reviewed By: jeremydubreil
Differential Revision: D9496910
fbshipit-source-id: 7a4138978
6 years ago
066204fcf0
[eradicate] always allow to refine nullable types using repeated calls
...
Reviewed By: mbouaziz
Differential Revision: D9494876
fbshipit-source-id: e17c91bdb
6 years ago
93e42a5a25
[eradicate] fix the Ambiguous or-pattern variables under guard warning
...
Summary: The pattern matching could previously be missing some valid cases (in theory).
Reviewed By: mbouaziz, jberdine
Differential Revision: D9491441
fbshipit-source-id: 2bc1fc1aa
6 years ago
1bf8ed95b8
[inferbo] Simplify stack/heap memory domain
...
Summary:
In SIL, (1) some program variables (e.g., array parameter) are used as pointers to heap addresses and (2) the other program variables (e.g., local array) are used as addresses themselves. So, the values of (1) are retrieved by the `Load` command, while that of (2) are by `Exp.Lvar` expressions directly.
To address them differently, we had managed two maps (`Mem.Stack` and `Mem.Heap`), but which introduced function duplications on abstract memory and increased complexity. This diff merges the two maps, and instead a location set is used for distinguishing two types of abstract locations during analysis.
Reviewed By: mbouaziz
Differential Revision: D9420388
fbshipit-source-id: 13f824850
6 years ago
49e582fa49
[Loop-hoisting] Add a new checker for hoisting invariant function calls
...
Reviewed By: mbouaziz
Differential Revision: D9460455
fbshipit-source-id: 7488c1a69
6 years ago
66ef5f5c15
[eradicate] always check that non-nullable fields are initialized
...
Summary: It is easier to filter out those reports in `.inferconfig` if we want them that modifying a boolean value ddirectly in the code
Reviewed By: mbouaziz
Differential Revision: D9494082
fbshipit-source-id: 9fb042313
6 years ago
f8380f9480
Trying to fix comments on Localise.ml
...
Reviewed By: da319
Differential Revision: D9496535
fbshipit-source-id: b73c89633
6 years ago
14556f52b4
[starvation] whitelist @WorkerThread methods
...
Reviewed By: mbouaziz, ddino
Differential Revision: D9480061
fbshipit-source-id: 4648319e1
6 years ago
a06685c517
[inferbo] Add mli for proof obligations
...
Reviewed By: skcho
Differential Revision: D9480149
fbshipit-source-id: 305ab24b1
6 years ago
426ddb5e1c
[nullable] make the Eradicate flag use_models to be the default mode
...
Summary: There no clear alternative to using models of the standard library at this point so we can simplify the code a little bit
Reviewed By: mbouaziz
Differential Revision: D9491062
fbshipit-source-id: 9e5a6eeea
6 years ago
524ae3a7e2
[inferbo] Return unknown value on non-const function calls
...
Summary:
It returns unknown values on non-const function calls like on unknown
function calls.
Reviewed By: mbouaziz
Differential Revision: D9478862
fbshipit-source-id: 4b795ec55
6 years ago
a3d5f0283d
[clang] only pass `--Xclang` args to driver commands
...
Summary:
Not all clang commands are happy with all arguments, but the driver is usually
the place we want to add arguments to.
Reviewed By: martinoluca
Differential Revision: D9421403
fbshipit-source-id: fa6d39a9b
6 years ago
76bf31bc17
[inferbo] Add a test case of global constant
...
Summary: `CONDITION_ALWAYS_**` can be introduced by global constants.
Reviewed By: ezgicicek, mbouaziz
Differential Revision: D9478528
fbshipit-source-id: 7b1a46e7a
6 years ago
ed638de189
[eradicate] remove the check extension flag which was always false
...
Reviewed By: mbouaziz
Differential Revision: D9130163
fbshipit-source-id: 4510eb4a5
6 years ago
277fd06782
[inferbo] Simplify condition trace
...
Reviewed By: skcho
Differential Revision: D9372262
fbshipit-source-id: 5338d5437
6 years ago
5817ff6adc
[inferbo] Do not re-report issues if the precision hasn't improved
...
Reviewed By: Julek
Differential Revision: D9400004
fbshipit-source-id: 916de6db1
6 years ago
735b28f359
[infer] remove the bug_class from the Infer report
...
Summary: This field does not seem to be used anywhere
Reviewed By: mbouaziz
Differential Revision: D9184595
fbshipit-source-id: d6eb62bca
6 years ago
3cffdb9745
[infer] remove the field procedure_id in the analysis report
...
Summary: The `procedure_id` is not used in the final report
Reviewed By: mbouaziz
Differential Revision: D9176276
fbshipit-source-id: 2397b01c4
6 years ago
5a4d4f0882
[inferbo] Fail if trying to substitute non-symbolic conditions
...
Reviewed By: ezgicicek
Differential Revision: D9377804
fbshipit-source-id: 609fd1594
6 years ago
6bb429ef63
Reporting cleanup 13: log_issue_external
...
Reviewed By: jvillard
Differential Revision: D9369295
fbshipit-source-id: faf56b177
6 years ago
9dad4c3648
Reporting cleanup 12: node_id_key -> node
...
Reviewed By: jvillard
Differential Revision: D9360943
fbshipit-source-id: 6f2c5720c
6 years ago
3986a823f8
Reporting cleanup 11: node_id
...
Reviewed By: jvillard
Differential Revision: D9360697
fbshipit-source-id: 688aae944
6 years ago
3f4cb5cae9
[dune] upgrade to 1.1.1
...
Summary:
This seems to fix intermittent "Corrupted compilation unit description" failures in the build: https://github.com/ocaml/dune/issues/1157
It also fixes build warnings 58: https://github.com/ocaml/dune/issues/1107
Reviewed By: mbouaziz
Differential Revision: D9420579
fbshipit-source-id: d63adee67
6 years ago
1a75fa9ebd
[inferbo] Propagate INFERBO_ALLOC_MAY_BE_ even when the bound is infinity
...
Reviewed By: skcho
Differential Revision: D9398450
fbshipit-source-id: 7b676615e
6 years ago
693089ab08
[inferbo] Alloc site in the trace for INFERBO_ALLOC_xx issues
...
Reviewed By: skcho
Differential Revision: D9398353
fbshipit-source-id: 0d2e5c961
6 years ago
364099530e
[inferbo] Retrieve callee_pdesc and payload at the same time
...
Reviewed By: jvillard
Differential Revision: D9378011
fbshipit-source-id: c67c46e12
6 years ago
1938c4b758
[eradicate] remove TypeState extensions
...
Reviewed By: mbouaziz
Differential Revision: D9388068
fbshipit-source-id: dd63c8863
6 years ago
370f33c8dc
Added predicate for CXX11ConstantExpr
...
Reviewed By: jvillard
Differential Revision: D9313716
fbshipit-source-id: 24588b600
6 years ago
af14da6a13
[starvation] stop considering View.get... as blocking.
...
Reviewed By: ddino
Differential Revision: D9397992
fbshipit-source-id: da6d5a987
6 years ago
527fb90bbe
[Cost] Add a Java model for functions to be considered invariant
...
fbshipit-source-id: e2fa74b19
6 years ago
070f541226
[infer][nullsafe] cleanup of the Eradicate code 1
...
Summary: Remove unecessary level of functorisation
Reviewed By: jberdine
Differential Revision: D9387985
fbshipit-source-id: e0bcf1b13
6 years ago
98c596c546
[infer][biabduction] generate the Objective C and C++ models in single core mode
...
Reviewed By: mbouaziz
Differential Revision: D9370381
fbshipit-source-id: 5da2d2e76
6 years ago
7c8f00eb76
Update ocamlformat hash to match git release hash
...
Reviewed By: jberdine
Differential Revision: D9378850
fbshipit-source-id: c245a8cfd
6 years ago
789fcaff4c
Add file containing hash of required ocamlformat version
...
Reviewed By: jvillard
Differential Revision: D9360792
fbshipit-source-id: 0e8725ea0
6 years ago
07f22daada
[inferbo] Report calls without ()
...
Summary: This is not needed.
Reviewed By: skcho
Differential Revision: D9372037
fbshipit-source-id: 9c9a90ba6
6 years ago
34a6a487c5
Reporting cleanup 10: log_frontend_issue
...
Summary: Actually only `CFrontend_errors` is calling `log_issue_from_errlog` directly, let's rename it, and specify `node_id_key` to `node_key`
Reviewed By: jeremydubreil
Differential Revision: D9360651
fbshipit-source-id: 5d63e51e9
6 years ago
cc18f9883d
[Cost] Fix invariant variable analysis to be based on all reaching defns
...
Reviewed By: mbouaziz
Differential Revision: D9337572
fbshipit-source-id: f7f5f7572
6 years ago
eb282797ab
Reporting cleanup 9: move NodeKey to Procdesc
...
Reviewed By: jeremydubreil
Differential Revision: D9351622
fbshipit-source-id: f8c5690f8
6 years ago
d9e12850b9
[biabd] do not try to bypass `Ondemand` to get proc desc of models
...
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
6 years ago
55c2188615
[Perf] Emit costs to a separate file named costs-report.json
...
Reviewed By: mbouaziz
Differential Revision: D9337974
fbshipit-source-id: 392410736
6 years ago
04af716fba
Reporting cleanup 8: move errlog to summary
...
Reviewed By: jeremydubreil
Differential Revision: D9351379
fbshipit-source-id: 7056c6e87
6 years ago
Sungkeun Cho
Jeremy Dubreil
Martino Luca
Jules Villard
Daiva Naudziuniene
Josh Berdine
Mehdi Bouaziz
Ezgi Çiçek
Nikos Gorogiannis
Dino Distefano
Katie Ots