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
Summary: We assume multiplication of 1 is safe. It happens sometimes by multiplying `sizeof(char)`.
Reviewed By: mbouaziz
Differential Revision: D10444680
fbshipit-source-id: 2f33be280
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
Summary: It uses big int, instead of 63bits int of OCaml, in the interval domain in order to get preciser numeric values in the future.
Reviewed By: jvillard
Differential Revision: D10123364
fbshipit-source-id: c217f4366
Summary:
It simplifies abstract memory instantiations of function calls. Now it instantiates callee memories by directly evaluating symbol paths, rather than constructing `subst_map`.
main changes are:
- no construction of `subst_map` and `trace_map`
- no symbol table in Inferbo's summary
- no `Symbol_not_found` exception (for when a required symbol was unavailable in `subst_map`)
Reviewed By: mbouaziz
Differential Revision: D9495597
fbshipit-source-id: 18cdcd6f7
Summary: When a typedef-ed structure is defined in another source file, `tenv` returns a structure with empty fields.
Reviewed By: mbouaziz
Differential Revision: D9629200
fbshipit-source-id: 8859803f9
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
Summary: `CONDITION_ALWAYS_**` can be introduced by global constants.
Reviewed By: ezgicicek, mbouaziz
Differential Revision: D9478528
fbshipit-source-id: 7b1a46e7a
Summary:
It adds relational domains to Inferbo: octagon of Apron and polyhedra of Elina.
- Each Mem domain value includes one relational value containing relations among symbols. The relational values are modified by the `Prune` and `Store` commands.
- Each abstract value includes three symbols, which represent integer value, array offset, and array size of an abstract value.
The relational domain is deactivated by default. Use the `--bo-relational-domain {oct, poly}` option for the activation, though Inferbo with the relational domains does not work at this point because some modifications of Apron and Elina we made has not been applied to their opam repositories yet.
Reviewed By: jvillard
Differential Revision: D8874102
fbshipit-source-id: 08e5883cb
Summary:
It adds relational domains to Inferbo: octagon of Apron and polyhedra of Elina.
- Each `Mem` domain value includes one relational value containing relations among *symbols*. The relational values are modified by the `Prune` and `Store` commands.
- Each abstract value includes three *symbols*, which represent integer value, array offset, and array size of an abstract value.
The relational domain is deactivated by default, so this diff should not make any differences in CI.
Use `--bo-relational-domain {oct, poly}` for the activation, though Inferbo with the relational domains does not work at this point because some modifications of Apron and Elina we made has not been applied to their opam repositories yet.
Reviewed By: mbouaziz, jvillard
Differential Revision: D8478542
fbshipit-source-id: 510ff53
Summary:
It's useful to test that the bucket a given error is classified as doesn't
change over time without notice.
This records the bucket for *all* the tests, even though some never produce a
bucket. This is to be on the safe size instead of risking to forget adding the
bucket information when the test changes, or when copy/pasting from a test that
doesn't have buckets to one that does.
The implementation is pretty crude: it greps the beginning of the qualifier
string for a `[bucket]`.
Reviewed By: mbouaziz
Differential Revision: D8236393
fbshipit-source-id: b3b1eb9
Summary:
It improves the precision of widening operations of interval:
upper_bound_widen (min(n, s), s) = s
lower_bound_widen (max(n, s), s) = s
Reviewed By: mbouaziz
Differential Revision: D8038941
fbshipit-source-id: 61b10cb
Summary:
This information is already available in the trace, and can contain absolute
paths to system includes (or infer's own clang runtime), which confuses the
diff analysis.
Reviewed By: mbouaziz
Differential Revision: D7534609
fbshipit-source-id: 5bd8f8b
Summary:
It renames `eval_locs` to `eval_arr` and we use it for getting array block values the given input expressions are pointing to. For example, when given a program variable `x` as an input, `eval_arr` returns array blocks that `x` is pointing to, on the other hand, `eval` returns an abstract location of `x`.
Depends on D7471891
Reviewed By: mbouaziz
Differential Revision: D7471915
fbshipit-source-id: b994944
Summary: In the pointer arithmetics, it returns top, if we cannot precisely follow the physical memory model, e.g., (&x + 1).
Reviewed By: mbouaziz
Differential Revision: D7453510
fbshipit-source-id: db8738e
Summary: It adds an issue type, `BUFFER_OVERRUN_U5`, for alarms involving unknown values, i.e., when the trace set includes an unknown function call.
Reviewed By: mbouaziz
Differential Revision: D7178841
fbshipit-source-id: bfe857b
Summary: It corrects a precision bug in the interval domain, with adding some test cases.
Reviewed By: mbouaziz
Differential Revision: D7230918
fbshipit-source-id: 3ec641a
Summary:
Show some `SymAssign`s (corresponding to parameters) in the trace.
Depends on D7194448
Reviewed By: skcho
Differential Revision: D7194479
fbshipit-source-id: 0deff6c
Summary: It corrects a bug that `&(x.f[n])` was evaluated to `&(x.f[0])`.
Reviewed By: mbouaziz
Differential Revision: D7179620
fbshipit-source-id: 04cbaa7
Summary: It avoids that locations of array fields are evaluated to the `unknown` location incorrectly by addressing the case in the `eval_lindex` function.
Reviewed By: mbouaziz
Differential Revision: D7152736
fbshipit-source-id: 2dc825e
Summary: It collects array accesses from all sub expressions in commands.
Reviewed By: mbouaziz
Differential Revision: D7165098
fbshipit-source-id: 584dc80
Summary: The heuristics to determine the end of a block/procedure was too brittle, the new one ignores non significant instructions.
Reviewed By: jvillard
Differential Revision: D6845380
fbshipit-source-id: feab557
Summary: This should allow to report several occurences of the an issue appearing several times within the same method.
Reviewed By: jvillard
Differential Revision: D6783298
fbshipit-source-id: 5555906
Summary:
Simpler bug hash that is more independent of the underlying analysis. This now computes the hash based on:
- the bug type.
- the base filename: i.e for my/source/File.java, just keep File.java. So the hash will not change when moving files around.
- the simple method name: i.e. without package information and list of parameters. So changing the list of parameters will not affect the bug hash.
- the error message were the line numbers have been removed. So moving code or reformatting will not affect the hash.
Reviewed By: jberdine
Differential Revision: D6445639
fbshipit-source-id: 82e3cbe
Summary:
It seems that the abstraction instructions were not previously added the the CFG.
This is a functional changes to make sure that the abstraction state is always added. We can simplify the code later and just run this step before storing the CFG instead of after loading them.
Reviewed By: sblackshear, jvillard
Differential Revision: D6383672
fbshipit-source-id: cedcb8a
Summary:
- Plug model checkers
- Add alloc size safety condition on alloc of negative, zero or big size
Reviewed By: sblackshear
Differential Revision: D6375144
fbshipit-source-id: bbea6f3
Summary:
Next step to issue deduplication: do not keep safety conditions that are subsumed by others.
Only do it if they do not have infinite bound: replacing `0 < size` by `1 < size` is ok, but replacing it by `+oo < size` is not because it looks much more like a lack of precision.
Reviewed By: skcho
Differential Revision: D5978455
fbshipit-source-id: acc2384
Summary:
Move Inferbo safety conditions to their own file.
Split the old `Condition.t` to a condition together with a trace.
This will ease having: different kind of condition and several traces for the same condition (see following diff)
Reviewed By: jvillard
Differential Revision: D5942030
fbshipit-source-id: d74a612
Summary:
Calling exit at the end of a proc does not create unreachable code, prior to this commit inferbo reports that it does.
We extend collect_instrs to detect when we're at the end of a procedure in C and not report on unreachable code if we call a procedure there.
Reviewed By: mbouaziz
Differential Revision: D5623637
fbshipit-source-id: 0d5f326
Summary:
Bumps facebook-clang-plugins to a version that outputs sizeof() info in bytes and not bits.
update-submodule: facebook-clang-plugins
Reviewed By: akotulski
Differential Revision: D5526747
fbshipit-source-id: 6019542
Summary: Unknown library returns the unknown pointer as well as the top interval.
Reviewed By: mbouaziz, jvillard
Differential Revision: D5282669
fbshipit-source-id: 34c7e18
Summary:
- model `exit` as `Bottom`
- model `fgetc` as returning `[-1; 255]` rather than `[-1; +oo]`
- reduced the number of model functions for simple models
Reviewed By: KihongHeo
Differential Revision: D5137485
fbshipit-source-id: 943eeeb
Summary:
This diff fixes unintentional bottoms in pointer arithmetic of inferbo.
The pointer arithmetic on addresses of variables (not array) just returns
the operand.
Reviewed By: jvillard
Differential Revision: D5060424
fbshipit-source-id: 495d8b8
Summary:
Previously all knowledge of the dynamic length of such arrays was lost to infer:
```
void foo(int len) {
int a[len];
}
```
The translation of this program would make no reference to `len` (except as a
param of `foo`).
Translate this "initialization" using the existing `__set_array_length` infer
builtin, as:
```
# Declare local a[_]
n$0 = len;
__set_array_length(a, len);
```
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz
Differential Revision: D4969446
fbshipit-source-id: dff860f
Summary:
This commit fixes a problem that the buffer overrun checker incorrectly
stops when a global variable (bottom) is involved in control flow.
In the new version, abstract memories return Top for unanalyzed abstract
variables.
Reviewed By: mbouaziz
Differential Revision: D5016447
fbshipit-source-id: 5132448
Summary:
An array has a static or dynamic length (number of elements), but it also has a
stride, determined by the type of the element: `sizeof(element_type)`. We don't
have a good `sizeof()` function available on SIL types, so record that stride
in the array type.
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz
Differential Revision: D4969697
fbshipit-source-id: 98e0670
Summary:
Modify the type of `Exp.Sizeof ...` to include the value that the expression
evaluates to according to the compiler, or None if it cannot be known
statically.
Use this information in inferbo.
Mostly unused in the BiAbduction checker for now, although it could be useful
there too.
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz
Differential Revision: D4953634
fbshipit-source-id: be0999d
Summary:
- Use Logging for logging
- Add a few extra debug (not ON by default)
- No space before colon
Depends on D4961957
Reviewed By: KihongHeo
Differential Revision: D4961989
fbshipit-source-id: 7c8697d
Summary:
- Bottom-lift abstract memory domain to express unreachable node
- Two cases to make a node unreachable
+ constant: when an evaluation result of condition expression is
bottom or false, e.g., "prune(0)".
+ alias: when the same structure e is compared to itself with "<",
">", and "!=", e.g., "prune(e < e)".
- Add test for the new prune (prune_constant.c, prune_alias.c)
- Debug the semantics of comparison
Reviewed By: mbouaziz
Differential Revision: D4938055
fbshipit-source-id: d0fadf0
Sungkeun Cho
Mehdi Bouaziz
Julian Sutherland
Jules Villard
Jeremy Dubreil
Sam Blackshear
Greg Nisbet
Kihong Heo
Martino Luca
Kihong Heo