Ezgi Çiçek
b46f55d0bc
[purity] Mark functions with empty modified params as pure
...
Reviewed By: mbouaziz, ngorogiannis
Differential Revision: D13452909
fbshipit-source-id: f0dc419b1
6 years ago
Nikos Gorogiannis
24bd229ada
[infer][eradicate] example of error messages involving the temporary variables used to translate logical operations and conditional assignment
...
Reviewed By: ezgicicek
Differential Revision: D13516477
fbshipit-source-id: 37096f273
6 years ago
Mehdi Bouaziz
de3c7bac45
[inferbo][easy] Shift right zero
...
Reviewed By: ezgicicek
Differential Revision: D13517435
fbshipit-source-id: fa107fc2c
6 years ago
Jules Villard
8d3363f677
[pulse] record simple double free test
...
Summary: Just to make sure it is caught.
Reviewed By: da319
Differential Revision: D13517263
fbshipit-source-id: 976d3a3ae
6 years ago
Mehdi Bouaziz
8f060939d6
[inferbo] Java pointers, arrays and collections
...
Reviewed By: ezgicicek
Differential Revision: D13128600
fbshipit-source-id: 0dd876692
6 years ago
Mehdi Bouaziz
4343f9c8b2
[cost] Adds Log elements to polynomials
...
Reviewed By: ezgicicek
Differential Revision: D13175872
fbshipit-source-id: 2f1337317
6 years ago
Sungkeun Cho
fc26f79b92
[inferbo] Weaken canonical path in on-demand value generation
...
Summary:
It weakens canonical path in order to avoid an explosion of locations when a struct type has pointers to struct.
For example:
```
struct Tree {
struct Tree *root;
struct Tree *left;
struct Tree *right;
};
```
It was able to generate lots of abstract locations before this diff:
```
t->root
t->left
t->right
t->root->left
t->root->right
t->left->root
t->left->right
t->right->root
t->right->left
t->root->left->right
t->root->right->left
t->left->root->right
t->left->right->root
t->right->root->left
t->right->left->root
```
By this diff, pointer fields that have the same type are (unsoundly) canonicalized to the same one. For example,
```
t->root
t->root->left
t->root->right
t->root->left->right
t->root->right->left
```
are canonicalized to `t->root`. This is definitely unsound but I believe it is better than the location explosion by which analyses do not terminate in a reasonable time or giving a fixed limit of depth to the field access.
Reviewed By: mbouaziz
Differential Revision: D13503808
fbshipit-source-id: 867018712
6 years ago
David Lively
1f2b0d4152
Add new predicate has_cxx_qual_name and macro %cxx_full_name%
...
Reviewed By: jvillard
Differential Revision: D13490505
fbshipit-source-id: df66224d6
6 years ago
Mehdi Bouaziz
a130556869
[quandary] Separate insecure intent handling issue type when call is in an exposed class
...
Reviewed By: AmarBhosale
Differential Revision: D13465395
fbshipit-source-id: ad0ed5b17
6 years ago
Nikos Gorogiannis
2d2d861686
[racerd] reduce size of IssueAuxData
...
Reviewed By: jvillard
Differential Revision: D13505031
fbshipit-source-id: 90f1974a7
6 years ago
Mehdi Bouaziz
397f4a1973
[inferbo] pp fields
...
Reviewed By: ezgicicek
Differential Revision: D13505835
fbshipit-source-id: 8179e5134
6 years ago
Martino Luca
3acf5bf2ad
[Cost] Do not flag variations to/from zero-costing functions
...
Reviewed By: ezgicicek
Differential Revision: D13504638
fbshipit-source-id: 9f07b83d7
6 years ago
Mehdi Bouaziz
9f333bb433
[quandary] Different source kinds for endpoints
...
Reviewed By: ngorogiannis
Differential Revision: D13465357
fbshipit-source-id: 0e5f00a93
6 years ago
Mehdi Bouaziz
f6c2bd3f61
[quandary] Insecure Intent Handling
...
Reviewed By: ngorogiannis
Differential Revision: D13163873
fbshipit-source-id: 3f1417f9c
6 years ago
Mehdi Bouaziz
809100d612
[inferbo] Prettier field name for Java in traces
...
Reviewed By: ngorogiannis
Differential Revision: D13505750
fbshipit-source-id: f9a322449
6 years ago
Mehdi Bouaziz
dfd725d46c
[quandary] Also use summary for direct sources
...
Reviewed By: ngorogiannis
Differential Revision: D13488414
fbshipit-source-id: fcf2947cf
6 years ago
Jules Villard
9868f7f763
[pulse] warn on returning address of C++ temporary
...
Summary:
When a C++ temporary goes out of scope, tag its address in the heap with
a new attribute `AddressOfCppTemporary` so that we can later check that
we don't return it.
Reviewed By: da319
Differential Revision: D13466898
fbshipit-source-id: 8808338b4
6 years ago
Jules Villard
db1814b1d1
[pulse] detect stack variable address escape
...
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
6 years ago
Jules Villard
c77f22310a
[pulse] rewrite test to avoid stack variable address escape
...
Summary: Pulse is about to be smart enough to detect that bug.
Reviewed By: da319
Differential Revision: D13466895
fbshipit-source-id: 79afd2d51
6 years ago
Jules Villard
1b79f13a18
[ownership] make heuristic for reporting on lambdas more shareable
...
Summary: I want to use that function in Pulse too so let's share it.
Reviewed By: da319
Differential Revision: D13466897
fbshipit-source-id: 1bf3afee4
6 years ago
Jules Villard
2bb9e5ad85
[pulse] rename function that was never a pulse FP
...
Summary: Naming it `FP_` was a mistake in the original commit that copied the tests over as pulse has never reported on that method.
Reviewed By: da319
Differential Revision: D13465324
fbshipit-source-id: f8b24ebda
6 years ago
Jeremy Dubreil
61d75d9991
[infer][nullsafe] use the same human readable error message for Eradicate and the new Nullsafe backend
...
Reviewed By: mbouaziz
Differential Revision: D13414508
fbshipit-source-id: 06a366177
6 years ago
Sungkeun Cho
6920532e12
[inferbo] Forget only updated locations from latest prune at Store
...
Reviewed By: mbouaziz
Differential Revision: D13414636
fbshipit-source-id: 8dbe7ceb6
6 years ago
Mehdi Bouaziz
a6d78db9b5
[quandary] Simplify endpoints config
...
Reviewed By: ngorogiannis
Differential Revision: D13465306
fbshipit-source-id: 18d25d048
6 years ago
Nikos Gorogiannis
19faf643dc
[racerd] optional arguments and missing actuals
...
Reviewed By: jeremydubreil
Differential Revision: D13488298
fbshipit-source-id: c4bb80769
6 years ago
Nikos Gorogiannis
a3f4bb01f4
[starvation] fix type bug occurring in class references
...
Reviewed By: jeremydubreil
Differential Revision: D13466456
fbshipit-source-id: 0b312d9c3
6 years ago
Mehdi Bouaziz
930dd2eb03
[quandary] Inline internal analyze_call
...
Reviewed By: ngorogiannis
Differential Revision: D13487935
fbshipit-source-id: da748169b
6 years ago
Sungkeun Cho
e52b1e077e
[inferbo] Conditional proof obligation
...
Summary:
In order to avoid FPs due to lack of relational info, we apply a heuristic: proof obligations has a latest pruned values,
then it is instantiated at Call statements. If there is a bottom value in the instantiated pruned values, we can say the
program point where the proof obligation is introduced is unreachable with the given parameters of the function.
Depends on D13414441
Reviewed By: mbouaziz
Differential Revision: D13414483
fbshipit-source-id: 61bd34ebb
6 years ago
Sungkeun Cho
4ad5d38b69
[inferbo] Revise join of LatestPrune
...
Reviewed By: mbouaziz
Differential Revision: D13449197
fbshipit-source-id: a2913c494
6 years ago
Sungkeun Cho
2531c75cea
[inferbo] Add literal string assignment
...
Reviewed By: mbouaziz
Differential Revision: D13335547
fbshipit-source-id: a1c6f6ced
6 years ago
Mehdi Bouaziz
b3c8d1dc67
[HIL] Fix ExitScope
...
Reviewed By: jvillard
Differential Revision: D13399373
fbshipit-source-id: 9fa20fb41
6 years ago
Mehdi Bouaziz
3ad33c979e
[quandary] Split exec_instr
...
Reviewed By: ngorogiannis
Differential Revision: D13465603
fbshipit-source-id: 02799eec4
6 years ago
Nikos Gorogiannis
9d6a9f52ec
[starvation] improve 2-way deadlock reports
...
Reviewed By: mbouaziz
Differential Revision: D13450650
fbshipit-source-id: 0dbd349d1
6 years ago
Nikos Gorogiannis
8d855bdcdb
[access paths] do not print class name of Java fields
...
Reviewed By: jeremydubreil, mbouaziz
Differential Revision: D13450595
fbshipit-source-id: 5e3c5e994
6 years ago
Ezgi Çiçek
89b73e554e
[purity] Mark functions that write to global static vars as impure
...
Reviewed By: ngorogiannis
Differential Revision: D13434587
fbshipit-source-id: 6fb3cf917
6 years ago
Mehdi Bouaziz
b8fb4b5abc
[inferbo] Separate Java from C arrays
...
Reviewed By: skcho, jvillard
Differential Revision: D13190942
fbshipit-source-id: 6b7f4225b
6 years ago
Mehdi Bouaziz
703cec791d
[inferbo] Restore type models
...
Reviewed By: skcho, jvillard
Differential Revision: D13449623
fbshipit-source-id: feebe58f1
6 years ago
Mehdi Bouaziz
fd8b4795b8
[inferbo] Symbolic length for no-size flexible arrays
...
Reviewed By: jvillard
Differential Revision: D13450086
fbshipit-source-id: 645412be2
6 years ago
Sungkeun Cho
879f8d6fe8
[inferbo] Remove deadcode
...
Reviewed By: mbouaziz
Differential Revision: D13463856
fbshipit-source-id: f6a9c4328
6 years ago
Mehdi Bouaziz
af6e4ff9d1
Fix quandary tests output
...
Reviewed By: ngorogiannis
Differential Revision: D13451392
fbshipit-source-id: 965e9d3d6
6 years ago
Daiva Naudziuniene
e2b5a6f941
[pulse] Allow taking address of a field of an invalid object
...
Summary:
It's ok to take an address of a field / array access of an invalid object.
This diff calculates the inner most dereference for an access expression starting with `&` and does not report on the dereference even if the address is invalid.
Reviewed By: jvillard
Differential Revision: D13450758
fbshipit-source-id: 18c038701
6 years ago
Mehdi Bouaziz
bdbf39aaa3
[inferbo] More physical equalities for Bounds
...
Reviewed By: skcho
Differential Revision: D13176079
fbshipit-source-id: e09ebd176
6 years ago
Mehdi Bouaziz
03d3a85f45
Enforce physical equality for Maps
...
Reviewed By: ngorogiannis
Differential Revision: D13164297
fbshipit-source-id: 9ebcf9589
6 years ago
Mehdi Bouaziz
87b3907628
[quandary] Allow several kinds for external sources/sinks
...
Reviewed By: ngorogiannis
Differential Revision: D13417113
fbshipit-source-id: 0838c5704
6 years ago
Mehdi Bouaziz
00b052826a
[inferbo] Enforce physical equality for bottom lifted mem operations
...
Reviewed By: ngorogiannis
Differential Revision: D13164179
fbshipit-source-id: 6ca7244f3
6 years ago
Mehdi Bouaziz
5c4de212fb
[inferbo] New test + more debug
...
Reviewed By: jvillard
Differential Revision: D13450070
fbshipit-source-id: d6f53baca
6 years ago
Mehdi Bouaziz
6a59abd234
[inferbo] HTML debug for checking pass
...
Reviewed By: ezgicicek
Differential Revision: D13450061
fbshipit-source-id: ffe9ba062
6 years ago
Mehdi Bouaziz
e5e7237d9d
[inferbo] Move type models to their own file
...
Reviewed By: ezgicicek
Differential Revision: D13449611
fbshipit-source-id: 6b6170f56
6 years ago
Mehdi Bouaziz
bb1a19b6f9
[inferbo] Move OndemandEnv to its own file
...
Reviewed By: jvillard
Differential Revision: D13449603
fbshipit-source-id: a253ef70b
6 years ago
Mehdi Bouaziz
52e09aed13
[inferbo] Move get_formals from Domain to Procdesc
...
Reviewed By: jvillard
Differential Revision: D13449590
fbshipit-source-id: da435606a
6 years ago