8a37d7caf1
[inferbo] Move get_formals
...
Reviewed By: jvillard
Differential Revision: D13294600
fbshipit-source-id: acd67487a
6 years ago
760fabe825
[inferbo] Ignore __variable_initialization
...
Summary: Avoid introducing unknown values by __variable_initialization.
Reviewed By: mbouaziz
Differential Revision: D13254059
fbshipit-source-id: 75751fa70
6 years ago
2a94e907e2
[inferbo] Revise pp of Symb.partial
...
Reviewed By: mbouaziz
Differential Revision: D13253989
fbshipit-source-id: 87a55a764
6 years ago
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
c3823671f5
[inferbo] Lift the Init module up
...
Reviewed By: mbouaziz
Differential Revision: D13253573
fbshipit-source-id: f50500a05
6 years ago
4e166f3375
[inferbo] Instantiate symbolic locations in function parameters
...
Summary: It instantiates not only symbols for bound but also symbols for locations at function calls.
Reviewed By: mbouaziz
Differential Revision: D13231291
fbshipit-source-id: ce23a943b
6 years ago
f70d6da8f2
[inferbo] Use record type for eval_sym_trace
...
Reviewed By: mbouaziz
Differential Revision: D13231245
fbshipit-source-id: 797f6d795
6 years ago
0086c34364
[inferbo] Add symbolic locations for parameters
...
Summary:
It adds symbolic locations for paramters, which will be used for fixing instantiations of parameters in the
following diffs.
Reviewed By: mbouaziz, jvillard
Differential Revision: D13214293
fbshipit-source-id: f016ea4c3
6 years ago
55586b581b
[preanalysis] do not delay killing variables taken by reference
...
Summary:
Before, the liveness pre-analysis would place extra instructions in the
CFG for either:
1. marking an `Ident.t` as dead, or
2. marking a `Pvar.t` as `= 0`
But we have no way of marking pvars dead without setting them to 0. This
is bad because setting pvars to 0 is not possible everywhere they are
dead. Indeed, we only do it when we haven't seen their address being
taken anyway. This prevents the following situation, recorded in our tests:
```
int address_taken() {
int** x;
int* y;
int i = 7;
y = &i;
x = &y;
// if we don't reason about taken addresses while adding nullify instructions,
// we'll add
// `nullify(y)` here and report a false NPE on the next line
return **x;
}
```
So we want to mark pvars as dead without nullifying them. This diff
extends the `Remove_temps` SIL instruction to accept pvars as well, and
so renames it to `ExitScope`.
Reviewed By: da319
Differential Revision: D13102953
fbshipit-source-id: aa7f03a52
6 years ago
15b77ee8c8
[inferbo] Give semantics for unsigned int casting of minus one
...
Reviewed By: mbouaziz
Differential Revision: D13167389
fbshipit-source-id: 9ad2c8e23
6 years ago
5f925869b6
[infer] Translate more casts (unsigned int)
...
Reviewed By: mbouaziz
Differential Revision: D13167384
fbshipit-source-id: 666a52617
6 years ago
442fecc030
[inferbo] Fix performance of issue deduplication
...
Reviewed By: mbouaziz
Differential Revision: D13151692
fbshipit-source-id: 62bb0a932
6 years ago
52e2fb9f81
[inferbo] Rename is_collection_add -> last_included
...
Reviewed By: skcho
Differential Revision: D13190947
fbshipit-source-id: d435846e8
6 years ago
b92800a716
[inferbo] Do not join traces if Prune changed nothing
...
Reviewed By: skcho
Differential Revision: D13176164
fbshipit-source-id: 35341a99e
6 years ago
e091d229f8
[inferbo] Keep traces for iterators
...
Reviewed By: skcho
Differential Revision: D13176176
fbshipit-source-id: 3a42732c6
6 years ago
6aba4b7ca2
[AI] kill astate type
...
Reviewed By: mbouaziz
Differential Revision: D10119192
fbshipit-source-id: 4868cbcb1
6 years ago
0ec75c587f
[inferbo] Minor simplifications
...
Reviewed By: ezgicicek
Differential Revision: D13190906
fbshipit-source-id: 0bb65fa30
6 years ago
e505fd2dba
[inferbo] Pointer comparison
...
Reviewed By: skcho
Differential Revision: D13066771
fbshipit-source-id: 134b27db8
6 years ago
8de2b93cab
[cost] Abstract type for polynomial degree
...
Reviewed By: ezgicicek
Differential Revision: D13175851
fbshipit-source-id: db9078037
6 years ago
5f60ffaa8f
[inferbo] Trace refactoring
...
Reviewed By: skcho
Differential Revision: D13116116
fbshipit-source-id: 0b885dcfb
6 years ago
f4e9975783
[inferbo] Fix deadcode
...
Reviewed By: skcho
Differential Revision: D13177132
fbshipit-source-id: 58c1fb538
6 years ago
94e723bc82
[inferbo] Use Flat in relational domain
...
Reviewed By: skcho
Differential Revision: D13175923
fbshipit-source-id: e4bfa5ce6
6 years ago
8292323307
[inferbo/cost] Move Polynomials out of Itv.ml
...
Reviewed By: skcho
Differential Revision: D13173440
fbshipit-source-id: d1e699ee6
6 years ago
3cd57849c4
[inferbo] Remove duplicated module NonNegativeBound
...
Reviewed By: skcho
Differential Revision: D13173264
fbshipit-source-id: 4f2477889
6 years ago
8010b27cbd
[inferbo] Prepare delayed integer overflow reporting
...
Reviewed By: mbouaziz
Differential Revision: D13166479
fbshipit-source-id: 758f44512
6 years ago
edc090544a
[inferbo] Improve pp of Inferbo in traceview
...
Reviewed By: mbouaziz
Differential Revision: D13113991
fbshipit-source-id: 149652eff
6 years ago
1f96fd03cc
[inferbo] SymbolPath: rename Index -> Deref
...
Reviewed By: ezgicicek
Differential Revision: D13128441
fbshipit-source-id: f6547ed7c
6 years ago
a93e05e9fe
[inferbo] AliasRet: use AbstractDomain.Flat
...
Reviewed By: skcho
Differential Revision: D13164265
fbshipit-source-id: 66aad24fa
6 years ago
3a5d995369
[inferbo] AliasMap: use AbstractDomain.Map
...
Reviewed By: skcho
Differential Revision: D13164209
fbshipit-source-id: 2a1339d89
6 years ago
d6423cf598
[inferbo] Preparing for trace rewrite
...
Reviewed By: skcho
Differential Revision: D13116106
fbshipit-source-id: 36cdad380
6 years ago
828fa236d4
[Inferbo] represents_multiple_values from path
...
Summary:
It removes the `represents_multiple_values` parameters when we can know them from `path` values.
Depends on D12939124
Reviewed By: skcho
Differential Revision: D12939130
fbshipit-source-id: 30ff768b2
6 years ago
9028b91ec7
Load data from performance profiler
...
Reviewed By: martinoluca
Differential Revision: D9593836
fbshipit-source-id: 923bfc1f3
6 years ago
664978d654
Revert D12819709 to patch OOM events
...
Reviewed By: mbouaziz, ddino
Differential Revision: D13138398
fbshipit-source-id: c9a028c37
6 years ago
b4683d965d
[inferbo] Resize array on casting
...
Summary:
It modifies sizes and offsets of array values on pointer castings.
Currently, it supports only simple castings of pointer-to-integers.
Reviewed By: mbouaziz
Differential Revision: D12920589
fbshipit-source-id: a5ba831b8
6 years ago
c8a17b9d0e
[inferbo] Pass integer type widths to eval for cast
...
Summary: In this diff, it passes the parameter of integer type widths to evaluation functions. The parameter which will be used for casting in the following diff.
Reviewed By: mbouaziz
Differential Revision: D12920581
fbshipit-source-id: 48bbc802b
6 years ago
acf740e145
Print Unicode chars only if the locale allows it
...
Reviewed By: jvillard
Differential Revision: D13118955
fbshipit-source-id: 0d817f45f
6 years ago
8d990d6470
[inferbo] Move Boolean to their own module
...
Reviewed By: skcho
Differential Revision: D13111801
fbshipit-source-id: 6eca0e1c9
6 years ago
8fcbfcb741
[inferbo] Pretty-print more abstract locations
...
Reviewed By: ezgicicek
Differential Revision: D13114228
fbshipit-source-id: 9f4b16817
6 years ago
aa3fa55f05
[inferbo] Fix check of access condition
...
Reviewed By: mbouaziz
Differential Revision: D13114160
fbshipit-source-id: 9e46cf814
6 years ago
e912bf2aa5
[inferbo] Prune more for "(x + e1) < e2" cases
...
Reviewed By: mbouaziz
Differential Revision: D13095472
fbshipit-source-id: 21aef560a
6 years ago
e190325b82
[inferbo] Distinguish collection add against array access in pp
...
Reviewed By: mbouaziz
Differential Revision: D13096380
fbshipit-source-id: d8878749f
6 years ago
0d2b0e1ab7
[inferbo] Fix check function for is_collection_add
...
Summary: It fixes the conditions of the `check` function to address `is_collection_add` cases correctly.
Reviewed By: mbouaziz
Differential Revision: D13081281
fbshipit-source-id: 39ae5ef03
6 years ago
29631b7358
[Inferbo] Differentiate array and pointer in SymbolPaths
...
Reviewed By: jvillard
Differential Revision: D12939124
fbshipit-source-id: 256d0b159
6 years ago
4671bab088
[inferbo] Preparing for one-value symbols
...
Reviewed By: skcho
Differential Revision: D13071832
fbshipit-source-id: d978eead0
6 years ago
7c00591747
[inferbo] Type name for eval_sym
...
Reviewed By: skcho
Differential Revision: D13071774
fbshipit-source-id: 1dc412646
6 years ago
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
1503f63c27
[inferbo] Fix evaluation of multi-dimensional arrays
...
Reviewed By: mbouaziz
Differential Revision: D13082043
fbshipit-source-id: 5a45b4eee
6 years ago
07f8855185
[inferbo] Fix condition check of multi-dimensional array
...
Reviewed By: mbouaziz
Differential Revision: D13082491
fbshipit-source-id: 43775a1a1
6 years ago
716caf91bf
Add is_singleton_or_more to Set and Map
...
Reviewed By: skcho
Differential Revision: D13062696
fbshipit-source-id: 3a7286f55
6 years ago
0ba4c2c892
[cost] Pretty-printing exponents
...
Reviewed By: ezgicicek
Differential Revision: D13050241
fbshipit-source-id: dbac027b7
6 years ago
Sungkeun Cho
Jules Villard
Mehdi Bouaziz
Nikos Gorogiannis
Dino Distefano
Martino Luca