Jeremy Dubreil
8d36c33d20
[eradicate] record false positive when testing the return on an assignment
...
Reviewed By: ngorogiannis
Differential Revision: D15321693
fbshipit-source-id: a6aa7068a
6 years ago
Jeremy Dubreil
80ecc959a4
[eradicate] recording false positive example with nullability information stored into a boolean
...
Reviewed By: ezgicicek
Differential Revision: D15326336
fbshipit-source-id: 6918cd36a
6 years ago
Jeremy Dubreil
adbf6861e9
[eradicate] record false positive when incorrectly looking up overriden methods
...
Reviewed By: ezgicicek
Differential Revision: D15327218
fbshipit-source-id: b115eae5b
6 years ago
Jeremy Dubreil
4725c97fc9
[eradicate] record false positive with nullability information lost after assignment
...
Reviewed By: ezgicicek
Differential Revision: D15325267
fbshipit-source-id: 5c6f4143b
6 years ago
Nikos Gorogiannis
1d846ba631
[racerd] kill original paths from summary
...
Reviewed By: mbouaziz
Differential Revision: D15260250
fbshipit-source-id: 1d39d9f01
6 years ago
Jeremy Dubreil
b47e2d13f3
[eradicate] simplify the analysis traces
...
Reviewed By: jberdine
Differential Revision: D15215809
fbshipit-source-id: 584b51ea4
6 years ago
Ezgi Çiçek
da13e52b27
[inferbo] Generalize String.length to CharSequence.length
...
Reviewed By: mbouaziz
Differential Revision: D14951988
fbshipit-source-id: 6c8906d2a
6 years ago
Ezgi Çiçek
c85563d606
[inferbo,cost] Add cost models for java.util.Collections
...
Reviewed By: mbouaziz
Differential Revision: D15080211
fbshipit-source-id: 91c9b6dba
6 years ago
Nikos Gorogiannis
941b63a426
[classloads] remove possible race
...
Reviewed By: mbouaziz
Differential Revision: D15062321
fbshipit-source-id: 3a0781c29
6 years ago
Jeremy Dubreil
07d6ab2dd6
[infer][racerd] report the thread safety violations as warnings instead of errors
...
Reviewed By: ngorogiannis
Differential Revision: D15023740
fbshipit-source-id: 6d38e236a
6 years ago
Ezgi Çiçek
f4cdc23543
[hoisting] Turn on hoisting of expensive functions by default
...
Reviewed By: mbouaziz
Differential Revision: D14971084
fbshipit-source-id: ccbf6055e
6 years ago
Ezgi Çiçek
7e16aafdba
[loop-hoisting] Incorporate cost trace into EXPENSIVE_LOOP_INVARIANT_CALL issues
...
Reviewed By: mbouaziz
Differential Revision: D14934254
fbshipit-source-id: 23af117b6
6 years ago
Ezgi Çiçek
6d25b0990d
[cost,purity] Model java's Map as Collections
...
Reviewed By: jeremydubreil, mbouaziz
Differential Revision: D14935325
fbshipit-source-id: 798feb68e
6 years ago
Ezgi Çiçek
105e50d432
[inferbo,cost] Add models for SparseArray
...
Reviewed By: mbouaziz
Differential Revision: D14936048
fbshipit-source-id: f07b74c38
6 years ago
Ezgi Çiçek
4eec73c2f2
[loop-hoisting] Add complexity to EXPENSIVE_LOOP_INVARIANT_CALL issue message
...
Reviewed By: mbouaziz
Differential Revision: D14933345
fbshipit-source-id: 5a711fd2a
6 years ago
Ezgi Çiçek
a2140c3ae4
[hoisting] Rename LOOP_INVARIANT_CALL to EXPENSIVE_LOOP_INVARIANT_CALL and remove VariantForHoisting
...
Reviewed By: mbouaziz
Differential Revision: D14913784
fbshipit-source-id: 5d5d5bee3
6 years ago
Radu Grigore
344889775b
[infer][PR] Don't join postconditions. Fixes #678 .
...
Summary:
Increases precision a bit. I didn't observe speed problems on what I tested. (But, who knows?)
Closes https://github.com/facebook/infer/pull/799
Reviewed By: jvillard
Differential Revision: D6284206
Pulled By: rgrig
fbshipit-source-id: 6f1e8631f
6 years ago
Ezgi Çiçek
b802620bc8
[cost] Add cost models for loop invariant functions
...
Reviewed By: jvillard
Differential Revision: D14832961
fbshipit-source-id: 0d1b3353d
6 years ago
Nikos Gorogiannis
3e94fc7e16
[racerd] consider interfaces extending android.os.IInterface as automatically threadsafe
...
Reviewed By: jvillard
Differential Revision: D14772236
fbshipit-source-id: fab604f66
6 years ago
Nikos Gorogiannis
cf6ced0580
[racerd] on-annotations
...
Reviewed By: jvillard
Differential Revision: D14756737
fbshipit-source-id: 434859ce7
6 years ago
Nikos Gorogiannis
fdcd4cf591
[racerd] modulo loc
...
Reviewed By: jvillard
Differential Revision: D14616104
fbshipit-source-id: 314a14069
6 years ago
Ezgi Çiçek
857c59e022
[inferbo] Add model for Java's cast
...
Reviewed By: mbouaziz
Differential Revision: D14599837
fbshipit-source-id: 379301463
6 years ago
Ezgi Çiçek
ce0ccc10ec
[inferbo,cost] Add models for Java Strings
...
Reviewed By: mbouaziz, skcho
Differential Revision: D14522624
fbshipit-source-id: 1ec2e0389
6 years ago
Nikos Gorogiannis
f78dfbaeda
[racerd] guardeby checks on uithread
...
Reviewed By: jeremydubreil
Differential Revision: D14597281
fbshipit-source-id: 41bc7d1fc
6 years ago
Nikos Gorogiannis
98e796b006
[racerd] gate GuardedBy
...
Reviewed By: mbouaziz
Differential Revision: D14594051
fbshipit-source-id: 57f580fbe
6 years ago
Nikos Gorogiannis
4a75df2a83
[racerd] report only writes for GuardedBy
...
Reviewed By: mbouaziz
Differential Revision: D14594263
fbshipit-source-id: a8cab1765
6 years ago
Sungkeun Cho
c92d56e4ad
[inferbo] Substitute symbolic value of unknown function call to top
...
Summary: This diff substitutes symbolic values for unknown functions in proof obligations to top. The goal of the diff is to avoid generating too many number of proof obligations that cannot be concretized.
Reviewed By: ezgicicek
Differential Revision: D14537542
fbshipit-source-id: 7f8f3bb4b
6 years ago
Nikos Gorogiannis
f32db5382f
[racerd] restrict guarded by to one field/same or superclass
...
Reviewed By: jeremydubreil
Differential Revision: D14584698
fbshipit-source-id: ab0a7db11
6 years ago
Radu Grigore
8bf65086e3
[topl] Parser for temporal properties
...
Summary:
TOPL properties are essentially automata, which specify a bad pattern.
This commit is just a parser for them.
Reviewed By: jvillard
Differential Revision: D14477671
fbshipit-source-id: c38a8ef37
6 years ago
Ezgi Çiçek
713c308fc7
[inferbo] Generalize models for Java iterators
...
Reviewed By: skcho
Differential Revision: D14539894
fbshipit-source-id: b225aa7de
6 years ago
Nikos Gorogiannis
59a10d00d4
[racerd] guardedby
...
Summary:
Add support for GuardedBy: we deviate from the spec as follows:
- No warnings issued for any access within a private method, unless that method is called from a public method and the lock isn't held when the access occurs.
- Warnings are suppressed with the general RacerD mechanism, ie `ThreadSafe(enableChecks=false)`
- GuardedBy warnings override thread-safety violation warnings on the same access, because GuardedBy has a clearer and simpler contract.
Also, some simplifications, cleanups and perf improvements (eg avoid unreportable procs at the top level as opposed to on each of their accesses).
Reviewed By: jeremydubreil
Differential Revision: D14506161
fbshipit-source-id: b7d794051
6 years ago
Dino Distefano
67b42bf021
Added new issue types for Allocation and IO
...
Reviewed By: ezgicicek
Differential Revision: D14437988
fbshipit-source-id: 3e107d9e9
6 years ago
Ezgi Çiçek
ce190547a5
[java] Add support for openjdk11
...
Reviewed By: jeremydubreil
Differential Revision: D14323194
fbshipit-source-id: afa532c23
6 years ago
Dino Distefano
52b72f4bbe
Added more allocation primitives
...
Reviewed By: mbouaziz
Differential Revision: D14385870
fbshipit-source-id: 7e3ef32bf
6 years ago
Wenzhe Lu
ead4c44f9d
Adding Long.parseLong model to nullsafe/modelTables.ml
...
Reviewed By: jeremydubreil
Differential Revision: D14395623
fbshipit-source-id: f643abc63
6 years ago
Mehdi Bouaziz
564d0113b4
[Cost] More precise traces for Top
...
Reviewed By: ezgicicek
Differential Revision: D14350180
fbshipit-source-id: 2cb8b0cd0
6 years ago
Ezgi Çiçek
88a1dedb90
[cost] Ignore counting dummy loads
...
Reviewed By: mbouaziz
Differential Revision: D14365776
fbshipit-source-id: d84ef9d9e
6 years ago
Dino Distefano
3b8782a6c1
added allocation
...
Reviewed By: mbouaziz
Differential Revision: D14322430
fbshipit-source-id: 5c27a37db
6 years ago
Jeremy Dubreil
130a729674
[infer] report the Fragment Retains View issues as warnings instead of errors
...
Reviewed By: mbouaziz
Differential Revision: D14313596
fbshipit-source-id: 13a6824de
6 years ago
Sungkeun Cho
b55996d01a
[inferbo] Symbolic value for global variable
...
Summary:
It assigns symbolic values for global variables in the load commands. However, it does not instantiate the symbols for the global variables yet, which will be addressed in another diff.
Depends on D14208643
Reviewed By: ezgicicek
Differential Revision: D14257619
fbshipit-source-id: f9113c8a3
6 years ago
Mehdi Bouaziz
b48884bce7
[Cost] Traces for Top values
...
Reviewed By: ezgicicek
Differential Revision: D14247738
fbshipit-source-id: 4270649d2
6 years ago
Mehdi Bouaziz
f20e0737fd
[inferbo] Extract abstract domain functor for 'set represented by its smallest element'
...
Reviewed By: skcho
Differential Revision: D14243106
fbshipit-source-id: 900fbad3b
6 years ago
Ezgi Çiçek
340ac9d1c9
[purity] Fix global modification via argument passing
...
Reviewed By: mbouaziz
Differential Revision: D14208643
fbshipit-source-id: ddb3d435c
6 years ago
Jeremy Dubreil
82c4b716bf
[eradicate] rename the warning raised when dereferencing nullable types
...
Summary:
The Eradicate backend is reporting nullable type errors, that are not always necessarily leading to null pointer exceptions.
For example, the analysis is designed to be consistent with the Java type system and report on the following code:
String foo(boolean test) {
Object object = test ? new Object() : null;
if (test) {
return object.toString(); // the analysis reports here
}
}
even though the code will not crash.
In order to make this aspect clear, this diff renames the warnings `Null Method Call` and `Null Field Access` into `Nullable Dereference`
Reviewed By: ngorogiannis
Differential Revision: D14001979
fbshipit-source-id: ff1285283
6 years ago
Sungkeun Cho
a56902dc9b
[inferbo] Widening threshold by comparison
...
Summary:
This diff adds a constant to the set of widening thresholds if the
constant is compared to an abstract value in condition expressions.
Each abstract value has its own set of thresholds.
Reviewed By: mbouaziz
Differential Revision: D14147150
fbshipit-source-id: ca0db34d4
6 years ago
Sungkeun Cho
8ea92c51e0
[inferbo] Suppress ALLOC_IS_ZERO for C++'s array object
...
Reviewed By: mbouaziz
Differential Revision: D14122889
fbshipit-source-id: d0c99a5e6
6 years ago
Ezgi Çiçek
cab28a9461
[inferbo] Check collection constructor size
...
Reviewed By: mbouaziz
Differential Revision: D14122995
fbshipit-source-id: eeb2fceab
6 years ago
Ezgi Çiçek
11af20ef86
[inferbo] Model list constructors with arguments
...
Reviewed By: mbouaziz, ddino
Differential Revision: D14083727
fbshipit-source-id: 13219330f
6 years ago
Ezgi Çiçek
cd20abfc88
[cost] Add trace to symbols in polynomial bounds
...
Summary: Record where each symbol in a polynomial is coming from: either a loop, function call or a modeled call.
Reviewed By: mbouaziz
Differential Revision: D14047420
fbshipit-source-id: 56d0bd926
6 years ago
Jeremy Dubreil
02e39c8b30
[infer] map issues that only differ by the index of the parameter to the same bug hash
...
Reviewed By: jvillard
Differential Revision: D14061718
fbshipit-source-id: 6f4530d55
6 years ago
Jeremy Dubreil
a3ecfdb8ad
[infer][nullsafe] add a NULLSAFE_ prefix to the internal name of the Nullsafe errors
...
Reviewed By: ngorogiannis
Differential Revision: D13356313
fbshipit-source-id: 77103f723
6 years ago
Sungkeun Cho
82590756d9
[inferbo] Fix array member access in Java
...
Summary: In SIL, Java's array member is a pointer to an array, while C++'s is the array itself. This diff differentiate them in evaluating abstract locations.
Reviewed By: ezgicicek, mbouaziz
Differential Revision: D14021451
fbshipit-source-id: 00f14fe3b
6 years ago
Boris Valkov
ea530390d3
[nullsafe][android] warn when passing null to ImmutableList, ImmutableSet, and ImmutableMap
...
Reviewed By: jeremydubreil
Differential Revision: D13933976
fbshipit-source-id: 771fc985c
6 years ago
Mehdi Bouaziz
17fc4ca5cf
[cost] Simplify & optimize exit cost + threshold
...
Summary:
- There is no need to use AI to compute a dot product: let's just fold over all nodes, but still do it in order (using the WTO) to report at the right place
- The previous version was computing a dot product on nodes for each node, which was quadratic, the new version is linear
- Report only once, the first time the threshold is reached (if in a loop, report at the loop head)
Reviewed By: ddino
Differential Revision: D14028171
fbshipit-source-id: b4a840c6e
6 years ago
Jules Villard
c79f966279
[java] model `Double` like `Integer`
...
Summary:
Get rid of false positive as in the test by modelling `Double`. Longer term we
should probably prevent biabduction from blocking the angelic analysis on
`Nullable` fields but that seems harder.
Reviewed By: jeremydubreil
Differential Revision: D14005228
fbshipit-source-id: 59ef2ed66
6 years ago
Jeremy Dubreil
50eae0739d
[nullsafe] add an example using Guava Verify.verifyNotNull(...)
...
Reviewed By: mbouaziz, ngorogiannis
Differential Revision: D13995158
fbshipit-source-id: 8729a6ef1
6 years ago
Jules Villard
1aa413a65d
[classloads] add `replace` target to tests
...
Summary: The Makefile was missing that target and making `make test-replace` at the root of the repo fail.
Reviewed By: ngorogiannis
Differential Revision: D13990483
fbshipit-source-id: 805b5d2a9
6 years ago
Jeremy Dubreil
adfd5a6418
[nullsafe] consistent models for the scrict containers
...
Reviewed By: mbouaziz
Differential Revision: D13977297
fbshipit-source-id: a32be3431
6 years ago
Ezgi Çiçek
ea486c59d8
[purity] Always show PURE_FUNCTION issues
...
Reviewed By: mbouaziz
Differential Revision: D13973375
fbshipit-source-id: f23dab260
6 years ago
Ezgi Çiçek
6e0682b463
[purity] Mark unmodeled functions as modifying global state
...
Reviewed By: mbouaziz
Differential Revision: D13941653
fbshipit-source-id: 02a15b29c
6 years ago
Jeremy Dubreil
d08cabe7ed
[eradicate] match the different re-definitions of Preconditions.checkState
...
Reviewed By: mbouaziz
Differential Revision: D13966540
fbshipit-source-id: 3cdbb3fbc
6 years ago
Nikos Gorogiannis
374538a02f
[crashcontext] die
...
Reviewed By: jeremydubreil, mbouaziz, jvillard
Differential Revision: D13861427
fbshipit-source-id: 85e340bb5
6 years ago
Mehdi Bouaziz
1b8927badd
[inferbo/cost] Do not produce inferbo issues on Cost and Purity analysis
...
Reviewed By: skcho
Differential Revision: D13827167
fbshipit-source-id: 734950a1e
6 years ago
Mehdi Bouaziz
8a3592c34e
[inferbo] Uncouple numerical analysis and numerical checks
...
Summary:
This will allow to get the numerical results for Cost, Hoisting, Purity without the Inferbo issues.
For now, I still forced Inferbo issues for Cost and Purity to avoid lots of changes in tests, that will go away soon.
Reviewed By: ezgicicek, skcho
Differential Revision: D13826741
fbshipit-source-id: 796d1a50d
6 years ago
Nikos Gorogiannis
2ee8ab2990
[class-loads] catch expressions
...
Reviewed By: ezgicicek
Differential Revision: D13832128
fbshipit-source-id: 1d3778763
6 years ago
Nikos Gorogiannis
b4a22a5bdd
[classloads] prune and multidimensional arrays
...
Reviewed By: ezgicicek
Differential Revision: D13818684
fbshipit-source-id: 8e5289f8f
6 years ago
Nikos Gorogiannis
3e55f8eb60
[classloads] class object expressions
...
Reviewed By: mbouaziz
Differential Revision: D13818059
fbshipit-source-id: 785d557e0
6 years ago
Nikos Gorogiannis
3f9eb37246
[classloads] casts and instanceof
...
Reviewed By: mbouaziz
Differential Revision: D13817582
fbshipit-source-id: c40be6bf8
6 years ago
Nikos Gorogiannis
c1a00b2358
[classloads] restrict loads via fields
...
Reviewed By: ezgicicek
Differential Revision: D13817232
fbshipit-source-id: 470d5ce11
6 years ago
Nikos Gorogiannis
f171d0496b
[classloads] array expressions
...
Reviewed By: mbouaziz
Differential Revision: D13786746
fbshipit-source-id: 9774da835
6 years ago
Nikos Gorogiannis
3fc4ccbc14
[classloads] load super classes recursively
...
Reviewed By: mbouaziz
Differential Revision: D13771265
fbshipit-source-id: da600f912
6 years ago
Nikos Gorogiannis
89e396571d
[classloads] treat loads and stores wrt to field derefs
...
Reviewed By: mbouaziz
Differential Revision: D13761363
fbshipit-source-id: bcaddd13b
6 years ago
Nikos Gorogiannis
5686d67072
[classloads] fix treatment of static initializers
...
Reviewed By: jvillard
Differential Revision: D13751141
fbshipit-source-id: f64af292b
6 years ago
Nikos Gorogiannis
00df708f98
[classloads] record at most one load for each class
...
Reviewed By: ezgicicek
Differential Revision: D13750609
fbshipit-source-id: cd55a3370
6 years ago
Nikos Gorogiannis
39b11619b8
[classloads] overhaul test infra & fix treatment of self-class loading in method calls
...
Reviewed By: ddino
Differential Revision: D13622717
fbshipit-source-id: 233cc5d74
6 years ago
Jeremy Dubreil
87a8ddc8fa
[nullsafe] merge the option names
...
Reviewed By: mbouaziz
Differential Revision: D13682855
fbshipit-source-id: 28c990725
6 years ago
Jeremy Dubreil
910def4262
[nullsafe] rename the method for unsafe access to lists and maps
...
Reviewed By: ezgicicek
Differential Revision: D13668339
fbshipit-source-id: 3b07fff32
6 years ago
Jules Villard
16c0c03050
resource leaks tutorial
...
Summary: Publish solutions to the lab, and a Docker file and image to get started more quickly with infer hacking.
Reviewed By: mbouaziz
Differential Revision: D13648847
fbshipit-source-id: daf48ad03
6 years ago
Ezgi Çiçek
f7deed7593
[cost] Add examples that we can't handle currently
...
Reviewed By: mbouaziz, jvillard
Differential Revision: D13596579
fbshipit-source-id: 7460d430d
6 years ago
Sungkeun Cho
6a8f389c35
[inferbo] Prune (p=null)
...
Summary: This diff unset powloc and arrayblk values of p when assume(p==Null).
Reviewed By: mbouaziz, jvillard
Differential Revision: D13415366
fbshipit-source-id: a491a957f
6 years ago
Mehdi Bouaziz
5616940ec0
[inferbo] Symbols for one value
...
Summary:
For abstract values representing one concrete value, create only one symbol instead of two.
Still create two symbols (lb, ub) for abstract values representing multiple concrete values (like array cells).
As a consequence, comparisons of symbolic values are more precise (we can even prove equality). I expect to remove a bunch of FPs.
Another consequence is the disappearance of `.lb` and `.ub` in many reports.
Reviewed By: skcho
Differential Revision: D13072084
fbshipit-source-id: 9bc0b9881
6 years ago
Mehdi Bouaziz
5d1a213f52
[Hil] Fix failure in exception node
...
Reviewed By: jberdine
Differential Revision: D13541755
fbshipit-source-id: a58458046
6 years ago
Mehdi Bouaziz
85bab87d16
[cost] The first cost model is a log
...
Reviewed By: ezgicicek
Differential Revision: D13175881
fbshipit-source-id: 7718bdf0d
6 years ago
Nikos Gorogiannis
002e470137
[racerd] fix bug in ownership transitivity
...
Reviewed By: jvillard
Differential Revision: D13488078
fbshipit-source-id: 9d40d75bc
6 years ago
Mehdi Bouaziz
33aa07357f
[inferbo] Model Java collections using arrays
...
Reviewed By: ezgicicek, skcho
Differential Revision: D13190960
fbshipit-source-id: fba435f34
6 years ago
Nikos Gorogiannis
b50f56de16
[racerd] properly recognize all non-source variables
...
Reviewed By: jeremydubreil, mbouaziz
Differential Revision: D13505828
fbshipit-source-id: f5a0be17d
6 years ago
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
8f060939d6
[inferbo] Java pointers, arrays and collections
...
Reviewed By: ezgicicek
Differential Revision: D13128600
fbshipit-source-id: 0dd876692
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
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
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
af6e4ff9d1
Fix quandary tests output
...
Reviewed By: ngorogiannis
Differential Revision: D13451392
fbshipit-source-id: 965e9d3d6
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
Nikos Gorogiannis
101283f9d0
[starvation] fix trace description strings for taking locks
...
Reviewed By: mbouaziz
Differential Revision: D13416738
fbshipit-source-id: 02ebb6178
6 years ago
Ezgi Çiçek
61b51b09db
[hoisting] Rename hoisting message
...
Reviewed By: ngorogiannis
Differential Revision: D13415995
fbshipit-source-id: bbf1ee855
6 years ago
Ezgi Çiçek
88850d5119
[cost] Show simplified procname for Callsite paths
...
Reviewed By: mbouaziz
Differential Revision: D13399921
fbshipit-source-id: 8496e6ecf
6 years ago
Nikos Gorogiannis
f8fc40cea9
[starvation] improve debugging output
...
Reviewed By: ezgicicek
Differential Revision: D13399324
fbshipit-source-id: 5f2eb124a
6 years ago
Jeremy Dubreil
1baf723e3e
[infer][nullsafe] make the error message more explicit about the typing nature of the analysis
...
Reviewed By: ngorogiannis
Differential Revision: D13388567
fbshipit-source-id: 0dc4c2b47
6 years ago
Ezgi Çiçek
dde9723926
[inferbo] Add tests for Java collections
...
Reviewed By: mbouaziz
Differential Revision: D13377810
fbshipit-source-id: d57aa740a
6 years ago
Sungkeun Cho
f9161b164f
[inferbo] On-demand heap symbol using path
...
Summary:
It materializes symbolic values of function parameters on-demand. The on-demand materialization is triggered when finding a value from an abstract memory and joining/widening abstract memories.
Depends on D13294630
Main idea:
* Symbolic values are on-demand-ly generated by a symbol path and its type
* In order to avoid infinite generation of symbolic values, symbol paths are canonicalized by structure types and field names (which means they are abstracted to the same value). For example, in a linked list, a symbolic value `x->next->next` is canonicalized to `x->next` when the structures (`*x` and `*x->next`) have the same structure type and the same field name (`next`).
Changes from the previous code:
* `Symbol.t` does not include `id` and `pname` for distinguishing symbols. Now, all symbols are compared by `path:SymbolPath.partial` and `bound_end`.
* `SymbolTable` is no longer used, which was used for generating symbolic values with new `id`s.
Reviewed By: mbouaziz
Differential Revision: D13294635
fbshipit-source-id: fa422f084
6 years ago
Jeremy Dubreil
69af58506d
[infer][nullsafe] rename the option to run the Nullsafe checker
...
Reviewed By: ngorogiannis
Differential Revision: D13352004
fbshipit-source-id: 4be2e361c
6 years ago
Ezgi Çiçek
80de133482
[inferbo,cost] Add symbols for unknown function calls
...
Reviewed By: mbouaziz, skcho
Differential Revision: D13239712
fbshipit-source-id: 1bf24e394
6 years ago
Sungkeun Cho
4b2c65f2e2
Revert "[inferbo] Instantiate symbolic locations in function parameters"
...
Reviewed By: ngorogiannis
Differential Revision: D13301231
fbshipit-source-id: c763a158b
6 years ago
Sungkeun Cho
62d45f9c01
[inferbo] Copy callee's values that are reachable from parameters
...
Summary:
At function calls, it copies callee's values that are reachable from parameters.
Depends on D13231291
Reviewed By: mbouaziz
Differential Revision: D13231711
fbshipit-source-id: 1e8aed1c4
6 years ago
Ezgi Çiçek
305b2a74b8
[hoisting] Add new issue type for only invariant-modeled calls
...
Reviewed By: ngorogiannis
Differential Revision: D13194812
fbshipit-source-id: 0c020789d
6 years ago
Mehdi Bouaziz
e505fd2dba
[inferbo] Pointer comparison
...
Reviewed By: skcho
Differential Revision: D13066771
fbshipit-source-id: 134b27db8
6 years ago
Mehdi Bouaziz
5f60ffaa8f
[inferbo] Trace refactoring
...
Reviewed By: skcho
Differential Revision: D13116116
fbshipit-source-id: 0b885dcfb
6 years ago
Nikos Gorogiannis
2c6a705116
[racerd] kill stability
...
Reviewed By: jvillard
Differential Revision: D13180369
fbshipit-source-id: 5684ed318
6 years ago
Sungkeun Cho
edc090544a
[inferbo] Improve pp of Inferbo in traceview
...
Reviewed By: mbouaziz
Differential Revision: D13113991
fbshipit-source-id: 149652eff
6 years ago
Ezgi Çiçek
613c4a2848
[purity] Fix wrong invalidation of all params
...
Reviewed By: ddino
Differential Revision: D13119156
fbshipit-source-id: a766c16be
6 years ago
Mehdi Bouaziz
8fcbfcb741
[inferbo] Pretty-print more abstract locations
...
Reviewed By: ezgicicek
Differential Revision: D13114228
fbshipit-source-id: 9f4b16817
6 years ago
Sungkeun Cho
aa3fa55f05
[inferbo] Fix check of access condition
...
Reviewed By: mbouaziz
Differential Revision: D13114160
fbshipit-source-id: 9e46cf814
6 years ago
Sungkeun Cho
e912bf2aa5
[inferbo] Prune more for "(x + e1) < e2" cases
...
Reviewed By: mbouaziz
Differential Revision: D13095472
fbshipit-source-id: 21aef560a
6 years ago
Sungkeun Cho
e190325b82
[inferbo] Distinguish collection add against array access in pp
...
Reviewed By: mbouaziz
Differential Revision: D13096380
fbshipit-source-id: d8878749f
6 years ago
Nikos Gorogiannis
68a08a8a09
[starvation] stop reporting on AccountManager.setUserData
...
Reviewed By: da319
Differential Revision: D13097076
fbshipit-source-id: 748acbe2b
6 years ago
Mehdi Bouaziz
fac9932168
[inferbo] Add traces to Conditions always true/false and Unreachable code
...
Reviewed By: ezgicicek
Differential Revision: D13082665
fbshipit-source-id: bb0e4cbf3
6 years ago
Ezgi Çiçek
6683c71f8b
[purity, hoisting] Add more purity models for fblite and instagram
...
Reviewed By: mbouaziz
Differential Revision: D13082201
fbshipit-source-id: e2b3f3e18
6 years ago
Nikos Gorogiannis
f3194e00c9
[starvation] silence some strict mode models
...
Reviewed By: mbouaziz
Differential Revision: D13082383
fbshipit-source-id: 7f16b94c5
6 years ago
Nikos Gorogiannis
a3df8f9f99
[starvation] simplify report format
...
Reviewed By: mbouaziz
Differential Revision: D13065391
fbshipit-source-id: 6e302cf85
6 years ago
Mehdi Bouaziz
0ba4c2c892
[cost] Pretty-printing exponents
...
Reviewed By: ezgicicek
Differential Revision: D13050241
fbshipit-source-id: dbac027b7
6 years ago
Mehdi Bouaziz
5ed59b1655
[Inferbo/cost] Improve pretty-printing
...
Reviewed By: skcho
Differential Revision: D13045247
fbshipit-source-id: 5485b58c8
6 years ago
Ezgi Çiçek
dde0067eec
[purity] Don't report pure functions if hoisting mode is turned-on
...
Reviewed By: ddino
Differential Revision: D13025725
fbshipit-source-id: 44d138418
6 years ago
Ezgi Çiçek
f3d82a0230
[hoisting] Don't report functions modeled as VariantForHoisting but consider them invariant
...
Reviewed By: ddino
Differential Revision: D13025250
fbshipit-source-id: ba1e39591
6 years ago
Ezgi Çiçek
2f06fd768f
[purity, hoisting] Keep track of modified args
...
Reviewed By: mbouaziz
Differential Revision: D12921871
fbshipit-source-id: 17ba48895
6 years ago
Ezgi Çiçek
d5a2198010
[hoisting] Make invalidation stop at already explored (var,node) pairs
...
Reviewed By: mbouaziz
Differential Revision: D12957025
fbshipit-source-id: b51f81966
6 years ago
Ezgi Çiçek
ff722f975d
[hoisting] Stop invalidation at loop head
...
Reviewed By: mbouaziz
Differential Revision: D12925391
fbshipit-source-id: f74ef935e
6 years ago
Ezgi Çiçek
3fb1053b75
[hoisting] Invalidate arguments of type structs
...
Reviewed By: mbouaziz
Differential Revision: D12924850
fbshipit-source-id: b442d37be
6 years ago
Mehdi Bouaziz
9a4416f7d4
[quandary] String concatenation sanitizes class loading
...
Reviewed By: jeremydubreil
Differential Revision: D12943175
fbshipit-source-id: 9e1c92d46
6 years ago
Mehdi Bouaziz
174bdcd22b
[quandary] Add class-loading sinks
...
Reviewed By: jeremydubreil
Differential Revision: D12942819
fbshipit-source-id: c294b4238
6 years ago
Sungkeun Cho
2401f6f6eb
[inferbo] Give a widening threshold of zero
...
Reviewed By: mbouaziz
Differential Revision: D12898540
fbshipit-source-id: 95bdaf4f0
6 years ago
Sungkeun Cho
b2189c1c17
[inferbo] Loosen similar bounds condition
...
Summary:
For more deduplications of issues, this diff loosens the condition of
similar bounds. The previous condition of similar bounds was too
strict, so [0,0] and [0,+oo] were not similar.
Depends on D10851762
Reviewed By: mbouaziz
Differential Revision: D10866127
fbshipit-source-id: 4ba912a88
6 years ago
Sungkeun Cho
bf29bd9772
[inferbo] Fix xcompare of Itv
...
Reviewed By: mbouaziz
Differential Revision: D10851762
fbshipit-source-id: 20e26cc30
6 years ago
Ezgi Çiçek
39335bb095
[hoisting] Invalidate all dependencies of invalidated parameters
...
Reviewed By: mbouaziz
Differential Revision: D10356056
fbshipit-source-id: a5d3b4bbe
6 years ago
Ezgi Çiçek
8a51a70162
[Hoisting] Add FP test for indirect modification in loop
...
Reviewed By: mbouaziz
Differential Revision: D10288095
fbshipit-source-id: 55cd2870a
6 years ago
Ezgi Çiçek
affe3d1d60
[hoisting] Invalidate args of impure function calls
...
Reviewed By: mbouaziz
Differential Revision: D10236724
fbshipit-source-id: f39d4574d
6 years ago
Sungkeun Cho
120c8785eb
[inferbo] Update pp of buffer overflow condition
...
Reviewed By: mbouaziz
Differential Revision: D10851743
fbshipit-source-id: 1f06e3b64
6 years ago
Sungkeun Cho
3f71cf327b
[inferbo] Separate offset and index in condition
...
Summary:
This diff preserves values of offset and index separately, rather than
one value of their addition, because premature addition results in
imprecise FPs by the limited expressiveness of the domain.
Reviewed By: mbouaziz
Differential Revision: D10851393
fbshipit-source-id: 1685ead36
6 years ago
Mehdi Bouaziz
3ee96263a7
[inferbo] Simplify and improve Itv.prune_comp
...
Reviewed By: skcho
Differential Revision: D10386789
fbshipit-source-id: f9c7e33ef
6 years ago
Mehdi Bouaziz
ce34dcb695
Format everything
...
Reviewed By: jeremydubreil
Differential Revision: D10844347
fbshipit-source-id: 5a374da82
6 years ago
Sungkeun Cho
fd3f298156
[inferbo] Add narrowing
...
Reviewed By: jvillard
Differential Revision: D10334140
fbshipit-source-id: afb247866
6 years ago
Mehdi Bouaziz
3dd97cc40f
[inferbo] Use WTO abstract interpreter
...
Reviewed By: jvillard
Differential Revision: D10072723
fbshipit-source-id: aabf3605e
6 years ago
Nikos Gorogiannis
ea7b185b6b
[classloads] add option for specifying root methods and add tests
...
Summary: Reports will now be issued for the class loads of the methods specified by the option `--class-loads-roots`.
Reviewed By: jvillard
Differential Revision: D10466492
fbshipit-source-id: 91456d723
6 years ago
Sungkeun Cho
3f969414fe
[inferbo] Check integer overflow when really need
...
Summary:
It avoids checking integer overflow when it definitely cannot happen.
For example, it does not check integer overflow of addition when one
of parameters is a negative number, or underflow of subtraction when
its first parameter is a positive number.
Reviewed By: mbouaziz
Differential Revision: D10446161
fbshipit-source-id: b8c86e1b2
6 years ago
Sungkeun Cho
cd1981a567
[inferbo] Change pp of BinaryOperationCondition
...
Summary: This diff changes pp of binary operation condition in order to avoid a `make test` failure. For the same `uint64_t` type, it is translated to `unsigned long long` in 64bit mac, but `unsigned long` in 64bit linux, which made a `make test` failure.
Reviewed By: mbouaziz
Differential Revision: D10459466
fbshipit-source-id: 449ab548e
6 years ago
Sungkeun Cho
fb4086c6f6
[inferbo] Add integer overflow issue type
...
Reviewed By: mbouaziz
Differential Revision: D10253878
fbshipit-source-id: 9905d7db4
6 years ago