|
|
||
|
Many of the checks in FMT rely on several assumptions with regard to how the target machine operates. One of the most important is the assumption of object boundaries - in other words, that operations on distinct data objects do not interfere with each other. For example, there is an implicit rule that in the following operation, assignment to y does not interfere with x’s value:
The code above seems obvious and the assumption that it works properly is fundamental - without it there is no way to prove the assertion.
Yet such assumptions are more difficult to retain in more complex code:
The problem with above code is that there is not enough information regarding object accesses within the foo operation. If x is a local variable, then it can be assumed that foo has no access to it. This assumption is straightforward taking into account a rigorous modeling language (the complete analysis would be more involving in a language that supports pointers and references), but what if x is a package-level data object?
In such cases the operation’s pre- and post-conditions could be used to promise that x is not changed, form example:
Still, it would be very tedious to write all such post-conditions properly, especially in the context of an evolving system, where new entities are added to existing packages, as potentially all existing operations would need to have updated post-conditions when new data objects are added.
An alternative approach is to extend the annotation language so that it is possible (or necessary) to explicitly declare which data objects are accessed by the operation. For example, the foo operation might declare something like:
Such an annotation would mean that the operation promises to update only z, m and n objects (of course, separate checks generated for the operation’s body would need to ensure that the operation delivers on this promise) and that would be sufficient to prove the earlier assertion that x was not modified while foo was executing - but this kind of annotations was considered too tedious, either, and is not supported by FMT.
The solution is to perform the whole-system analysis and detect cases where a single data object is modified on such hidden paths. This also includes the situation where a variable is renamed by means of passing it via inOut or out parameter in operation calls.
First, the complete example demonstrating the above case - two operations, main and foo calling one another and accessing the same package-level data object:
The data aliasing that is hidden in the call to foo can be reported with the following command:
The “Show details” button displays complete description:
As in other reports that span potentially large number of operation (and the whole system by default), here the report is structured with operations grouped by their package. The foo operation on its own is not causing problems, so is reported with green “OK” - but its use within main is potentially dangerous, as it accesses the same global data object. The line listed for main contains the statement number and the “show” button displays the control flow diagram highlighting the exact place where the problem was found.
The same report is also available in the raw format, for further processing:
Similarly to other raw-format reports, this one is a nested Association object where for each package and each operation the errors are listed - in this particular structure, a single report is a pair containing the statement number and a human-readable error description.
Data aliasing can be also introduced when a single data object or variable is used more than once in a single call, where at least one of the uses is of the “updating” kind - that is, via inOut or out parameter, for example:
In this case, the same variable temp was used twice in a single call and both uses are intended for update:
Data aliasing is less obvious, but also potentially dangerous when the global data object is passed for update to an operation that uses the same data object directly or indirectly. The following example defines an operation that updates its argument based on the value of some package-level data object:
The getNextValue operation returns the next counter value, but is wrongly used in the baz operation, where the same data object is used for update:
This error is similar in nature to the one found in the main operation earlier and is reported with the same error message:
The possibility to selectively pick operations for analysis should be used with care, as constrained set of operations might hide some of the aliasing problems. In the previous call to swap, it was possible to detect the error by analyzing the bar operation only, as the aliasing was present at the call site. In the case of baz and getNextValue, however, both operations need to be involved in the analysis, otherwise the body of getNextValue will not be analyzed and since there is no local problem at the call site, the data aliasing might remain undetected:
Similarly to other analyzes that operate on operation collected from multiple operation bodies (like with call cycle analysis), narrowing the scope of analysis should be done with care - occasional whole-model invocations should be performed to ensure that all errors are found.
Previous: Call graph checks and analysis, next: Proof checks
See also Table of Contents.