Function-name handling in WitnessFactory.extractTransitionForStates is dubious
There are several problematic things in WitnessFactory.extractTransitionForStates
relating to the handling of the name of the current function.
-
The
functionName
variable is potentially overridden based on the name of variables used in expressions (lines 680-692). Furthermore, this is done by parsing the name of variables for the occurrence of the the stringsstatic
and::
. Even if the code is correct currently, this is error-prone and should be avoided, because the way how variable names look is an implementation detail and could change at any time. Instead the code should get the desired name directly from the declaration. -
The code uses
CFACloner.extractFunctionName
to revert function renamings byCFACloner
(line 811). This is either unnecessary, or again error-prone, because if all code that wants to properly output function names needs to callCFACloner
, we have a lot of bugs (there is just this single call toCFACloner.extractFunctionName
in the whole code base). So we must add a discoverable way to get the correct function name without needing to call a static function from some other arbitrary component (also cf. #698 (closed) for what kind of problems this creates) and then deleteCFACloner.extractFunctionName
. -
The way how
functionName
is modified is extremely error-prone.
First, it is set using the function name of the current location (line 628).
Then it is overridden using the name of local variables, but only under some conditions (lines 680-692). If there are several variables that match this condition, it is random which of them is used last and determines the resulting function name. There is neither a check whether all variables lead to the same function name, nor abreak
in the loop to at least use the first variable instead of the last one if it really does not matter. Then the function name is used for the first time for some scope-related filtering (line 761). The last two steps are done in a loop, so it could happen that thefunctionName
value that is overridden in the first loop iteration (if there are matching variables in it) leaks into theScope
of the second loop iteration (if there are no matching variables in the second iteration). This definitely seems like a bug.
Finally, the function name is changed again (usingCFACloner.extractFunctionName
in line 811) and then used for theassumption.scope
field (line 815). Note that the value here still depends on which value happens to be set last in the nested for loop above.
So at different times the same variable means different things (sometimes our internal function name and sometimes the original function name). If new code is added that usesfunctionName
it is quite likely that the developer does not notice this and the new code will use the wrong function name in some circumstances, because in all standard situations the function name actually is never modified, only in some specific circumstances that are not likely to appear in tests.
This is prime example for why immutability in code is a good thing. My suggestion is to use different variables for each specific variant of the function name, each having the smallest possible scope, and eaching beingfinal
. If this method with 220 lines would be refactored into several methods this would probably also be good. Note that a subset of these problems also occurs with other variables likeresultFunction
.
#479 (closed) and #698 (closed) are related and a solution for properly handling original names of functions could probably fix much of these three issues in one go.