Summary:
This diff prevents that the latest prune value is overwritten as top
from callees.
Reviewed By: jvillard
Differential Revision: D16540391
fbshipit-source-id: bdd5b42ed
Summary: This diff tries to do weak update for the abstract locations by pointer arithmetic, e.g. `p[n]` or `p+n`, even if the type of `p` is declared as a simple pointer, not an array.
Reviewed By: ezgicicek
Differential Revision: D16458367
fbshipit-source-id: 3b4cdd7e4
Summary:
The `represents_multiple_values` flag was adopted to decide whether updating abstract value strongly or weakly. However, the flag was included in the `Val` domain, which is strange, because it is a property of abstract locations, rather than abstract values. This makes the behavior of memory update function depend on the abstract value to update, making its code complicated.
This diff detach the `represents_multiple_values` flag from the `Value` domain, thus the memory update does not depend on the abstract value. Since this is a refactoring, I believe the diff should not make many semantic changes.
Reviewed By: ezgicicek
Differential Revision: D16441734
fbshipit-source-id: 4c10779d7
Summary:
It downgrades issues of void pointer to L5, because of its impreciseness. This is not
ideal but Inferbo cannot analyze arrays pointed by void pointers precisely at the moment.
Reviewed By: jvillard
Differential Revision: D16379911
fbshipit-source-id: f2c016aba
Summary:
Thanks to the newly added `StarField`, path length is better controlled before ondemand is used.
Hence there is no need to (unsoundly) canonicalize paths then anymore.
Reviewed By: ezgicicek
Differential Revision: D15409716
fbshipit-source-id: 9ea7b4717
Summary: Remove from inferbo summary locations that are unreachable from callers
Reviewed By: ezgicicek
Differential Revision: D15064518
fbshipit-source-id: 734e79b4a
Summary: The name was misleading, the function only forget locs for relations.
Reviewed By: ezgicicek
Differential Revision: D15045933
fbshipit-source-id: 7f41a55e7
Summary:
This diff propagates LatestPrune on function calls.
Depends on D14321605
Reviewed By: mbouaziz
Differential Revision: D14321618
fbshipit-source-id: cb2e1b547
Summary:
Given a pointer-typed parameter, Inferbo assumes that it is an array
block. However, when a pointer is given as an actual parameter, it
failed the substitution of the array block value of the parameter, thus
which made some return values to bottom unexpectedly.
This diff revises the substitution of array block, so it can
substitute array block values with actual pointers correctly when it
is possible.
Reviewed By: mbouaziz
Differential Revision: D14663475
fbshipit-source-id: 0477de1ba
Summary:
It does more reachability checks on prunings. Before the diff, it checked the reachability only by the condition expression of prune commands, but now also uses PrunePairs.
Depends on D14321575
Reviewed By: mbouaziz
Differential Revision: D14321605
fbshipit-source-id: f630de842
Summary:
This diff accumulates LatestPrune in sequential prunings. It should be sound since Inferbo invalidates some data of LatestPrune if they are updated.
Depends on D14321534
Reviewed By: mbouaziz
Differential Revision: D14321575
fbshipit-source-id: 233dbae32
Summary:
This diff changes a LatestPrune to use a return variable instead of another local variable, when the function returns a conditional value. This is a preparation to propagate LatestPrune inter-procedurally in the following diffs.
context: If a function returns a conditional value, e.g. `return x == y`, the LatestPrune value includes a temporary local variable introduced by the SIL translation. This diff is to avoid propagating the temporary local variables to its caller.
Reviewed By: mbouaziz
Differential Revision: D14321534
fbshipit-source-id: d157bfdd0
Summary: Unknown locations in the alias domain resulted in unexpected unreachable code.
Reviewed By: mbouaziz
Differential Revision: D14339412
fbshipit-source-id: a5dca6489
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
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
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
Summary: It keeps alias of simple plus/minus arithmetic in order to pruning the value of "++i" expression.
Reviewed By: mbouaziz
Differential Revision: D14080230
fbshipit-source-id: d3af32a32
Summary:
If the result of `fgets` is not-null, the length of `s` should be
bigger than or equal to 1.
Reviewed By: mbouaziz
Differential Revision: D13939994
fbshipit-source-id: 298fe33f4
Summary:
This diff updates the reachability conditions of proof obligations at every function calls.
Depends on D13781124
Reviewed By: mbouaziz
Differential Revision: D13781147
fbshipit-source-id: 3c8768bd9
Summary:
The `oenv` is an option.
This diff ensures that it is `Some` during the analysis and `None` when it is stored in a summary.
It could have been resolved with another type, e.g. `unit`, but an option was needed to avoid duplicating code that is generic up to some point.
The price to pay is a parametric type.
Reviewed By: skcho
Differential Revision: D13825418
fbshipit-source-id: 71824609d
Summary:
This diff extends the abstract domain to keep binary conditions on
prunings, so Inferbo can suppress more proof obligations (i.e., false
positives) that are known to be unreachable according to the binary
conditions.
Depends on D13729600
Reviewed By: mbouaziz
Differential Revision: D13749914
fbshipit-source-id: 314f048f1
Summary: It extends the abstract location for C string length, i.e., the first index of the null character in character array.
Reviewed By: mbouaziz
Differential Revision: D13634241
fbshipit-source-id: d2727d5f5
Summary:
This diff prevents deduplications of issues when they have different
conditions to reach.
Reviewed By: mbouaziz
Differential Revision: D13596220
fbshipit-source-id: 95f802edb
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
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
Summary: It weakly updates array when there are more than two contents.
Reviewed By: mbouaziz
Differential Revision: D13318443
fbshipit-source-id: fa740d8b1
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
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
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
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
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 detaches the Summary module from BufferOverrunDomain.
Depends on D9194130
Reviewed By: jvillard
Differential Revision: D9194375
fbshipit-source-id: 30392b5ce
Summary: It simplifies instantiataion of `ret_alias`. While it got `ret_alias` values by iterating caller's and callee's memory, now it gets `ret_alias` by evaluating symbol paths included in location values.
Reviewed By: mbouaziz
Differential Revision: D9569606
fbshipit-source-id: a3326bb81
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:
- Was not used by the caller
- Gives smaller summaries
- Will allow adding a intra-proc info, e.g. `node` for reporting (not sure yet)
Reviewed By: skcho
Differential Revision: D9373763
fbshipit-source-id: 322001b53
Summary:
In SIL, (1) some program variables (e.g., array parameter) are used as pointers to heap addresses and (2) the other program variables (e.g., local array) are used as addresses themselves. So, the values of (1) are retrieved by the `Load` command, while that of (2) are by `Exp.Lvar` expressions directly.
To address them differently, we had managed two maps (`Mem.Stack` and `Mem.Heap`), but which introduced function duplications on abstract memory and increased complexity. This diff merges the two maps, and instead a location set is used for distinguishing two types of abstract locations during analysis.
Reviewed By: mbouaziz
Differential Revision: D9420388
fbshipit-source-id: 13f824850
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: It moves the functions that constructs array values from BufferOverrunSemantics to ArrayBlk and Val modules.
Reviewed By: mbouaziz
Differential Revision: D9194130
fbshipit-source-id: bf040a01a
Summary: It uses a SymbolPath map to Symbol in Inferbo's summary instead of an entry memory of callee, which is used for instantiations of the abstract memories on function calls.
Reviewed By: mbouaziz
Differential Revision: D9081631
fbshipit-source-id: 478cda0de
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
Sungkeun Cho
Josh Berdine
Mehdi Bouaziz
Ezgi Çiçek
Nikos Gorogiannis