Improvement for data dependency across function calls [blocks: #2871]

[zhixing-xu]

This pull request includes an improvement for the data dependency generation across function calls.

Description of the issue in original data dependency implementation:

When generating dependence for an argument in a function call, its data dependence node is set to be the line this function call happens. The result is unrelated variables are pulled into the dependence, as shown in the following example:

void foo(){
    int a = 1;
    int b = 2;
    bar(a, b);
}

int bar(int a, int b){
   int result = b;
   return result;
}

In the code, result only depends on b in function foo, so when tracing the leaf dependence node for result, the expected node is the line int b = 2.
However, the current data dependence graph would point result's data dependence to the line bar(a,b). And since bar(a,b) depends on both int a = 1 and int b = 2, the leaf nodes of result's dependence graph would be int a = 1 and line int b = 2.
In large code base with many nested function calls, this easily generates too many unnecessary dependences for function call arguments.

The improvement:

The cause of this issue is how reaching definition is constructed. Reaching definition can be considered as a data structure that keeps information about the state of all variables at a program location. The state here means a set of possible locations where the variable could get its current value. In the process of the reaching definition construction, if a given source location call_loc is a function call, every parameter in this function would have this call_loc added to this set. But this call_loc is not exactly where the parameters get their values, and this is why the issue happens.

The fix does a 1-1 mapping between the symbols of function call parameters and the symbols of the arguments given for the call (utilizing information in symbol table and rw_set). Then rather than adding the function call location as the state of the parameter, it adds the current state of its corresponding argument in the call.

The modification in goto_rw.cpp are for the purpose of generating the read set from the expression of a single argument.

[allredj]

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 59e0f00).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102168511
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

• the cbmc commit has disappeared in the mean time (e.g. in a force-push)
• the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

[chrisr-diffblue]

This looks reasonable to me, but it might also be good if @danpoe could review as well, as he knows this code better than I do.

[chrisr-diffblue]

This description comment is really helpful, thanks!

[danpoe]

I think increasing the precision of the data dependencies through function calls is very useful. Just bypassing the function parameters/arguments as proposed here seems like a slightly unclean solution though.

Consider the following program:

 1 void func(int c, int d)
 2 {
 3 }
 4
 5 int main()
 6 {
 7   int a = 0;
 8   int b = 0;
 9
10   func(0, a + b);
11
12   return 0;
13 }

Here saying that d:7 and d:8 (with 7, 8 being the line numbers of the corresponding assignments) are reaching definitions within function func seems wrong. The real definition of d would be a + b in the function call.

Maybe a better solution would be to extend the representation of reaching defintions. We could add a new field index to reaching_definitiont which for function calls indicates the argument index.

[TGWDB]

Closing due to age (no further comment on PR content), please reopen with rebase on develop if you intent to continue this work.