Bufferoverrun analysis - small fixes and improvements

[dhauzar]

This PR contains small fixes and improvements to bufferoverrun analysis. They were originally implemented to fix the problems we discovered when using BO to analyze Ada code:

1) Get also transitively reachable locations.

Refactor get_reachable_locs_from_aux and get also transitively reachable locations.

2) Remove also frontend generated vars from the scope.

The instruction ExitScope is generated for all variables (both Var.LogicalVar and Var.ProgramVar) which become dead according to the Liveness preanalysis.

BO implements this instruction by removing all variables of the type Var.LogicalVar out of the abstract state and doing nothing for variables of the type Var.ProgramVar. The rationale is that the Liveness analysis doesn't take aliasing into account and program variables can be aliased. That is, they can be accessed after the instruction ExitScope through a pointer and removing them from the abstract state is thus undesirable.

However, keeping all program variables in the abstract state poses a performance problem - an example is an analysis of a file gen_il-gen-gen_nodes.adb from GNAT sources. So this commit removes the frontend generated variables from abstract states. Such variables cannot be aliased so normally, it should be safe to remove them. However, it seems that the content of these variables is used by cost analysis so this is why this is put into a flag. Perhaps, it would be safe to remove the variables also with respect to the cost analysis when we are not in a loop.

3) Improve pruning of simple aliases.

Create pruning expression when pruning a simple alias equal to the pruned logical variable.

4) More precise handling of symbolic intervals.

Handle symbolic intervals in more precise way. In particular (1) improve the conversion of (symbolic) intervals to boolean values, and (2) improve the equality of (symbolic) intervals. This is important to make evaluation of expressions more precise.

• infer/src/bufferoverrun/itv.ml (is_false): instead of comparing the interval with False (zero) directly, return True if the interval is <= and >= zero. As the result, is_false returns True also for [B(u), 0] and [max (I(s), 0), min (I(s), 0)]. (eq_sem): Return True also in the case when the bounds of two intervals itv1 and itv2 are not equal and it holds that itv1 <= itv2 <= itv1. (ne_sem): Use eq_sem instead of duplicating the logic of eq_sem.

5) Fix importing of an alias bound to the return variable.

The problem was that while an alias bound to a return variable was always imported, it can be precisely imported only for locations corresponding to global variables and locations reachable from formal parameters passed by reference. Trying to import locations reachable from formal parameters passed by value produced locations which are dereferences of the locations that should be the correct result of the import.

Fix the problem by (1) fixing importing locations involving parameters passed by value by importing them as unknown locations and (2) importing only global locations and locations involving parameters passed by reference when importing return value alias.

6) Make the import of dereferences more robust.

When importing a location representing a dereference from a callee to a caller, fallback to attempting to create a symbolic location if the target of the dereference is unknown in the caller.

Note the standard mechanism for creating symbolic locations can fail because of the lack of type information. For example, in the case of Ada, when calling a method on an abstract type that modifies a field of a concretization of this type, we don't have type information for the field in the caller.

Lift the condition on using the type passed to BufferOverrunDomain.Valon_path when creating a value of a location to always use this type when the type cannot be induced from formal, actual parameters and type environment (computed by BufferOverrunOnDemand.typ_of_param_path). The rationale is that some instructions give type information which cannot be computed by the mechanism above and it is too bad to not use it. Since having type information means creating a symbolic value, the consequence of this change can be that a symbolic value can be created even for local variable. This is no that bad since such value behaves as top and won't be imported to callers of the current subprogram.

[facebook-github-bot]

@skcho has imported this pull request. If you are a Meta employee, you can view this diff on Phabricator.

[facebook-github-bot]

@dhauzar has updated the pull request. You must reimport the pull request before landing.

[skcho]

Ooops, sorry for the late review. I was waiting an email or a github notification, but somehow I seem to have messed my notification setting. I will get back to you soon.

[facebook-github-bot]

@skcho has imported this pull request. If you are a Meta employee, you can view this diff on Phabricator.

[facebook-github-bot]

@skcho merged this pull request in facebook/infer@1f6063846b770daa30d00225235930fa2eecb816.