Ezgi Çiçek
19eac53f0e
[cost] Add models for Collections.max/min
...
Reviewed By: ngorogiannis
Differential Revision: D15673503
fbshipit-source-id: 5450ec63f
6 years ago
Ezgi Çiçek
0ef038332d
[purity] More models for Java Map
...
Reviewed By: mbouaziz
Differential Revision: D15659378
fbshipit-source-id: 2fa613281
6 years ago
Ezgi Çiçek
bb9f44dee2
[cost] Fix and refactor cost models
...
Reviewed By: mbouaziz
Differential Revision: D15604679
fbshipit-source-id: 210c86f37
6 years ago
Ezgi Çiçek
99eda7e3a8
[inferbo,cost] Fix java arrays
...
Reviewed By: mbouaziz, ddino
Differential Revision: D15602327
fbshipit-source-id: d17253a15
6 years ago
Ezgi Çiçek
5b2a36409c
[inferbo] Add models for org.json.JSONArray
...
Reviewed By: jvillard
Differential Revision: D15577727
fbshipit-source-id: 829a93fc0
6 years ago
Ezgi Çiçek
98ecc13a5e
[inferbo,cost] Add models for java.util.Arrays and java.util.List
...
Reviewed By: jvillard
Differential Revision: D15577408
fbshipit-source-id: f9e94dc35
6 years ago
Ezgi Çiçek
c14b917e7f
[purity] Rename tests
...
Summary:
Consistent renaming of tests: replace
- `bad` -> `impure`
- `ok` -> `pure`
Reviewed By: mbouaziz
Differential Revision: D15536214
fbshipit-source-id: eab8b1cc3
6 years ago
Ezgi Çiçek
a01a4a3658
[purity] Enhance purity models with invalidated arguments
...
Summary:
- Rename `invariantModels` to `purityModels`
- Track which arguments are modified in purity models. Before we were invalidating all arguments of impure modeled functions. Instead, now we only invalidate modified args given in the model. This should ideally result in more precision in the analysis.
- Add some more purity models for :`cast`, `new`, `new_array` and `Math.random`
Reviewed By: mbouaziz
Differential Revision: D15535332
fbshipit-source-id: 5395800d9
6 years ago
Ezgi Çiçek
a092c4f3f9
[cost] Generalize Java's sort model
...
Reviewed By: mbouaziz
Differential Revision: D15516930
fbshipit-source-id: 23dd3858d
6 years ago
Ezgi Çiçek
bc082da199
[cost] Make unmodeled functions pure by default
...
Reviewed By: mbouaziz
Differential Revision: D15470254
fbshipit-source-id: ef3833778
6 years ago
Ezgi Çiçek
b455baae5d
[loop-invariance] Invalidate args to T function calls
...
Reviewed By: ngorogiannis
Differential Revision: D15451671
fbshipit-source-id: 20653f34e
6 years ago
Ezgi Çiçek
639c91c29f
[loop-invariance] Add FPs for modified global and static invalidation
...
Reviewed By: mbouaziz, ngorogiannis
Differential Revision: D15451632
fbshipit-source-id: 67f5f4c89
6 years ago
Jeremy Dubreil
c96e72b990
[eradicate] record example of false positive with invariants between variables
...
Reviewed By: ezgicicek
Differential Revision: D15442303
fbshipit-source-id: 8fda0f0f1
6 years ago
Jeremy Dubreil
79b0b8172d
[eradicate] add a model for java.nio.file.Path.getParent()
...
Reviewed By: ezgicicek
Differential Revision: D15447277
fbshipit-source-id: ed7f61940
6 years ago
Ezgi Çiçek
d033e72196
[purity] Add tests for locality
...
Reviewed By: ngorogiannis
Differential Revision: D15373797
fbshipit-source-id: 8cb0de6b5
6 years ago
Andrew Adams-Moran
0ad15356c2
Add @Cleanup annotation
...
Reviewed By: jeremydubreil
Differential Revision: D15318692
fbshipit-source-id: fd6debace
6 years ago
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