The contents of this manual are the subject of copyright and all rights in it are reserved. The manual may not be copied, in whole or in part, without the written consent of Praxis High Integrity Systems Limited.
Limited Warranty
Praxis High Integrity Systems Limited save as required by law makes no warranty or representation, either express or implied, with respect to this software, its quality, performance, merchantability or fitness for a purpose. As a result, the licence to use this software is sold ‘as is’ and you, the purchaser, are assuming the entire risk as to its quality and performance.
Praxis High Integrity Systems Limited accepts no liability for direct, indirect, special or consequential damages nor any other legal liability whatsoever and howsoever arising resulting from any defect in the software or its documentation, even if advised of the possibility of such damages. In particular Praxis High Integrity Systems Limited accepts no liability for any programs or data stored or processed using Praxis High Integrity Systems Limited products, including the costs of recovering such programs or data.
2.1 Sources of run-time errors
2.2 Detection of run-time errors
3 The SPARK Examiner with Run-time Checker Tool
3.2 Additional command line switches
3.3 Additional warning messages
4 Generation and Interpretation of RTCs
5 Detection of Intermediate Expression Overflows
6 Strategies for Eliminating Run-time Errors
6.1 Strengthening specifications
Document Control and References
SPADE is a registered trademark of Praxis High Integrity Systems Limited.
Note: The SPARK programming language is not sponsored by or affiliated with SPARC International Inc. and is not based on SPARC™ architecture.
Contents
This manual explains the process of generating and interpreting run-time checks for SPARK programs. Generation and proof of these run-time checks shows a SPARK program to be free of the predefined exceptions CONSTRAINT_ERROR and NUMERIC_ERROR under all execution conditions. The SPARK Examiner with Run-time Checker is an extension of the SPARK Examiner; a description of the use of this tool can be found in the manual “SPARK Examiner User Manual” [1]. The proof obligations generated by the SPARK Examiner with Run-time Checker take the form of Verification Conditions (VCs). The language and interpretation of these is described in the manual “The Generation of Verification Conditions for SPARK Programs” [2]. Finally, effective use of the SPARK Examiner with Run-time Checker involves simplification of the VCs it generates; this is accomplished by the SPADE Automatic Simplifier and, possibly, the Proof Checker which are described separately, in other Praxis High Integrity Systems documents [3,4]. References [1,2,3] form part of the delivered documentation set for the Examiner with RTC; reference [4] forms part of the Proof Checker.
This manual is intended to provide sufficient information to allow the generation of run-time checks for SPARK programs. It covers:
· the theoretical background for the proof of absence of run-time errors;
· the application of the tool;
· the interpretation of the results obtained; and
· methods of avoiding run-time errors.
2.1 Sources of run-time errors
The Ada language definition requires compilers to generate checks for certain error conditions at run time, raising a predefined exception when they occur, unless such checking is suppressed by the user. The predefined exceptions and their causes are tabulated below.
Exception |
Source |
CONSTRAINT_ERROR |
access check, discriminant check, index check, length check, range check, tag check. |
NUMERIC_ERROR |
division check, overflow check |
PROGRAM_ERROR |
erroneous execution, incorrect order dependence, return not executed in function subprogram, elaboration check, accessibility check. |
STORAGE_ERROR |
exhaustion of dynamic heap storage, stack overflow |
TASKING_ERROR |
exceptions raised during intertask communication |
* In Ada 95 Numeric_Error has been subsumed into Constraint_Error.
The use of SPARK removes the possibility of many forms of run-time error either because
· the language subset does not include the Ada feature concerned; or
· the additional static semantic rules of SPARK allow the error to be detected before the program is run.
An example of the former is the elimination of TASKING_ERROR in sequential SPARK as it does not permit tasking. An example of the latter is the Examiner’s ability to detect whether a subtype indication is compatible with the type mark in a subtype definition. By these means, all the errors in italics in the table above are eliminated.
SPARK also greatly reduces the likelihood, and eases the prevention, of STORAGE_ERROR because the programmer does not have direct access to the dynamic heap; furthermore, the rules of SPARK enable a program’s maximum memory requirements to be calculated prior to execution.
We are therefore left with index check, range check, division check and overflow check. It is to the elimination of errors associated with these checks that the SPARK Examiner with Run-time Checker is applicable.
2.2 Detection of run-time errors
Ada compilers insert additional code to check at run time whether certain language rules are being violated. For example, whenever an expression is used as an array index a check will be made that the value of the expression lies within the array’s bounds. The Examiner with Run-time Checker automatically inserts check statements[1] at the same points and generates verification conditions from them. Proof of these verification conditions shows that the associated run-time errors cannot occur. The Examiner also takes advantage of the Ada type system in providing additional information that can be assumed during the proof process.
Consider the following tiny example:
7 type T is range -128 .. 128;
8
9 procedure Inc(X : in out T)
10 --# derives X from X;
11 is
12 begin
13 X := X + 1;
14 end Inc;
On entry to Inc we can assume that T’First £ X £ T’Last because if this were not true then a run-time error would already have occurred at the point where Inc was called. In order to show that the single executable statement in Inc does not cause a run-time error we need to show that at that point T’First £ (X + 1) £ T’Last is true. Both the assumption and required check are automatically inserted by the Examiner which causes VCs to be generated. After simplification these VCs reduce to the following.
For path(s) from start to check associated with statement of line 13:
procedure_inc_1.
H1: x >= - 128 .
H2: x <= 128 .
->
C1: x <= 127 .
There are two hypotheses (which may be assumed true) and a
single conclusion to be proved.
Unfortunately it is clear that the hypotheses are not strong enough to
allow the conclusion to be proved so a potential run-time error exists. From the VC we can readily deduce the
circumstances when the run-time error will occur: when Inc
is called with
X = 128.
Strategies for eliminating such potential run-time errors are discussed later in this manual.
3 The SPARK Examiner with Run-time Checker Tool
This section covers application the SPARK Examiner with Run-time Checker tool. The run-timer checker tool is an extension of that described in [1]. It has additional command line options and may produce a number of new warning messages.
3.2 Additional command line switches
The Examiner with Run-time Checker provides three command line switches additional to those described in the Examiner and Examiner with VCG user manuals. The switches and their meanings are as follows.
Switch |
Meaning |
|
Windows or VAX |
Sun or Linux |
|
/rtc |
-rtc |
Generate, in addition to any VCs that the VCS switch would have produced, VCs associated with index check, range check and division check. |
/exp |
-exp |
Generate, in addition to any VCs that the RTC switch would have produced, VCs associated with overflow check. |
/realrtcs |
-realrtcs |
Causes the Examiner to produce the run-time checks selected by the above two switches for real numbers (float and fixed) as well as for non-real types. Note that this option is not enabled by default. Please contact Praxis High Integrity Systems if you wish to make use of this feature. |
Note that only one of the switches rtc and exp is used at a time; each generates all the VCs produced by its predecessor as well as those it generates itself.
3.3 Additional warning messages
As well as the error and warning messages described in [1] the Examiner with Run-time Checker may also produce the following; these messages appear in the screen echo, listing file and report file as usual.
The generation of VCs requires that all cyclic paths are cut with a suitable loop-invariant assertion. Because run-time checks can be generated from SPARK code without the use of additional annotations the Examiner may encounter an uncut cyclic path. To enable the generation of VCs to continue, the Examiner will choose a suitable location in the loop and insert a default assertion. When this occurs the Examiner issues a warning (which is included in the listing file as usual) as follows:
--- Default assertion planted to cut loop.
The semantics of real, especially floating-point, arithmetic are such as to make the automatic detection of run-time errors difficult or impossible. As standard, the Examiner with Run-time Checker does not attempt to generate VCs for real expressions. The following warning is issued at the end of each subprogram where such expressions have been found:
--- RTCs have not been generated for statements including real numbers.
--- RTCs for statements including real numbers are approximate
3.3.3 Expression ordering
When generating VCs associated with overflow checks (i.e. when the EXP command line switch is used) it is important to know the order in which sub-expressions are evaluated. A compiler is permitted to re-order expressions containing operators of equal precedence even if a run-time error results. The Examiner assumes left to right evaluation of such expressions but issues a warning if it detects an expression vulnerable to re-ordering. Such expressions should be parenthesised if expression checks are being generated.
--- This expression may be re-ordered by a compiler. Left to right
evaluation was assumed for RTC generation.
Output files are generated for each subprogram which is free of SPARK semantic errors. The file names and locations are obtained from the subprogram name and location as described in [1]. Three files are produced for each subprogram as follows.
The verification conditions are contained in files with the extension .vcg. The form and significance of these VCs is described in [2]. Typically the number of VCs generated will be quite large with at least one for every statement in the subprogram; however, they are usually quite simple in form and will be reduced extensively by the SPADE Automatic Simplifier. It is usually not worth expending much effort in manual interpretation of the unsimplified VC output. The validity of the VCs generated depends on some important assumptions, principally that the SPARK source is free from data flow errors; these are described in section 4.4. Note that it is not a requirement that the program is free from information flow errors in the form of reported mismatches between the calculated information flow and that specified in the dependency or derives relation.
The SPADE Simplifier and Checker require some type information for the entities in the VC file. These declarations are contained in a file with the extension .fdl. It should not be necessary manually to interpret this file.
The SPADE Automatic Simplifier is capable of reading and using a file of proof rules during the simplification process. A proof rule states some property which may be assumed, for example, that a constant has a particular numeric value or that a type has particular bounds. A standard set of rules are generated automatically by the Examiner using information from declarations in the SPARK source and placed in a file with the extension .rls. The automatically generated rule file should not be edited and will be overwritten each time the Examiner is applied to the source text.
The SPADE Automatic Simplifier User Manual [3] describes the use of user-defined proof rules that can be written to supplement the automatically generated rules.
4 Generation and Interpretation of RTCs
This section covers the form and meaning of the VCs generated by the run-time checker. Subsections identify:
· the program constructs for which RTCs are generated;
· the hypotheses that are inferred from code and can be used to help discharge the VCs;
· proof of VCs;
· important assumptions affecting the validity of the proof; and
· significant limitations.
This section summarises the language constructs for which VCs are generated. A more detailed description, based on the Formal Semantics of SPARK is given in [5].
Wherever an expression of a scalar type is assigned, a VC is generated to show that the value of the expression lies in the subtype of the object to which it is being assigned. A similar check is made that a function return value is in range.
Note that VCs are generated on the assumption that function calls are evaluated in lexical order (i.e. from left to right) within an expression. The compiler is permitted to reorder evaluation under some circumstances. However, because in SPARK functions cannot have side effects, the order of evaluation is immaterial to the validity of the VCs. The order in which the VCs are generated may affect the ease of proof of an individual VC. For example, if the left hand function has a more severe precondition than that on the right then its proof will provide a hypothesis making proof of the right hand function’s precondition trivial. If the functions are placed in the reverse order then both preconditions will have to be proved separately; however, the overall proof obligation is the same in both cases.
Similar checks are made for the components of a named or positional association. These include procedure calls, function calls and aggregates. Each expression is checked to ensure that it lies in the subtype range of the component with which it is being associated. For a procedure call the required check is that each expression associated with an imported scalar, formal parameter is in range. A check is also required that each exported scalar, formal parameter is in the subtype of its associated actual parameter.
Wherever name argument lists occur (e.g. in array accesses) a check is made that each index expression lies in the subtype range of its corresponding index subtype. These checks are sufficient to show that arrays are never accessed outside their bounds.
4.1.4 Type conversion and qualification
Scalar type conversions and type qualifications require similar checks: the value of the expression must lie in the subtype range of the type to which it is being converted or with which it is qualified. The static semantic rules enforced by the SPARK Examiner ensure that type conversion of arrays cannot give rise to run-time errors so no run-time check is generated for such conversions. Other type conversions are not permitted apart from unchecked type conversions. Unchecked type conversions are not checked and may give rise to invalid values. Dealing with potentially invalid values is covered in section 4.2.2.
4.1.5.1 Succ
A check is made that X ¹ T’Last in the expression T’Succ(X);
4.1.5.2 Pred
A check is made that X ¹ T’First in the expression T’Pred(X);
4.1.5.3 Val
A check is made that X >= T’Pos(T’First) and X <= T’Pos(T’Last) in the expression T’Val(X);
In the case of if-statements, case-statements, while-loops and conditional exits, checks are made, in the same way as all other expressions, that the controlling expression of the condition is free from run-time errors.
4.1.6.1 Short-circuit forms
Modified checks are required in the case of the short-circuit forms and then and or else. When these forms are used a run-time error may not occur even if the right hand side of the short circuit conditional would appear to generate one. For example: if X /= 0 and then Y / X > 10 cannot cause a division by zero. Using the decoration ok to indicate “free from run-time error” the checks required for Left and then Right are:
and for Left or else Right:
A check is made that the right-hand side of all division operators is non zero. A check is also made that the exponent of an exponentiation is not negative if the operand is integral.
If the RealRTC option is enabled and in use an additional check is made that the exponent of an exponentiation is not negative if the operand is the real value zero (0.0).
When expression overflow checks are enabled then checks are made at all unary and binary operators that the result of the operation lies in the base type of the type returned by the operator. Note that this differs from most of the run-time checks so far described where we are typically interested in an expression lying in a particular subtype range.
4.1.8 Private and abstract types
The uses of an object of a private type outside its package of definition are limited to assignment and comparison for equality. Since there are no subtypes of private types, run-time errors cannot occur during such operations. The only other operations defined for a private type are those specifically declared and exported by its declaring package. No run-time error can occur from the use of private types at the interface to these operations (although, of course, one might within the body of such an exported subprogram where the full details of the private type are known).
Similarly, a SPARK subprogram may indirectly import or export global data which is not directly visible according to the rules of Ada; for example, the abstract own variables associated with a package implementing an abstract state machine. Run-time errors cannot occur outside such a package from manipulation of this abstract state although, as with private types, checks will be required within the bodies of the subprograms which provide the exported operations of the abstract state machine.
The Examiner does not, therefore, generate any VCs associated with the assignment of objects of private types nor their passing as parameters. Neither are checks generated where global data, which is not directly visible, is imported or exported.
The static semantic rules of SPARK ensure that Boolean expressions cannot cause run-time errors. For example Boolean’Succ(True) is not permitted. For this reason VCs are not generated from such expressions.
The previous section describes checks “planted” by the Examiner from which verification conditions are generated. To assist in the proof of these VCs the Examiner also provides as hypotheses properties of the code which may be assumed. For example, since a check is made on a procedure call statement that each imported actual parameter lies in the subtype range of its corresponding formal parameter, the Examiner provides hypotheses within a subprogram body that each imported formal parameter, or directly visible global import, is in range. Where a structured object is imported, each of its elements is assumed to be correctly within type. Similarly, it is assumed that any constant used is in range.
Hypotheses that variables exported by called subprograms are within the type exported, and that function return values are within their specified type, are also generated. Hypotheses are also generated from preceding statements in a sequence of statements. Each statement will have associated with it a VC whose proof will show that statement to be free of run-time errors. If the statement is free of run-time errors then control will pass to the next statement where the correctness of the preceding VC may be assumed as a hypothesis.
Additionally, the Examiner exploits the benefit of data flow analysis by assuming that a local variable, anywhere it is referenced in an expression, must be validly in type. The additional hypotheses generated by this are especially helpful in the discharge of VCs associated with code containing loops. Note that this assumption depends on:
1 The absence of data flow errors (see Section 4.4.1) which would otherwise introduce random values to local variables.
2 The absence of invalid values (See section 4.2.2).
For example:
procedure Process(X : in out T)
--# derives X from X;
is
begin -- we can assume X in T here
X := X + 1; -- we must show X + 1 in T here
-- we can assume X + 1 in T here
X := X * 2; -- we must show (X + 1) * 2 in T here
end Process;
-- given subtype ST is T range ? .. ?; and A : ST;
-- a call to Process has the following obligations
we must show A in T here
Process(A);
we can assume A in T here
we must show A in ST here
An invalid value may be read from an external source, occur as the result of an unchecked type conversion, or as a value returned from an external subprogram (for instance written in C or assembler).
For this reason the Examiner makes no assumption that the value read from an external variable (an own variable or refinement constituent with the mode in) or the result of a call to an instantiation of Unchecked_Conversion is in its type. An Unchecked_Conversion is literally unchecked and therefore any value returned may be invalid. External variables are assumed to be connected to the external environment from which any bit pattern (not necessarily a legal value) might be received.
For example:
package Sensor
--# own in Port; -- an external in variable
is
type SensorRange is range 1..10;
procedure Read (X : out SensorRange);
--# global in Port;
--# derives X from Port;
end Sensor;
package body Sensor
is
Port : SensorRange;
for Port'Address use ...;
procedure Read (X : out SensorRange)
is
begin
X := Port;
-- although Port and X are of the same type we cannot assume that
-- the value in Port is valid
end Read;
end Sensor;
The unsimplified run-time checks generated for Read are:
For path(s) from start to finish:
procedure_read_1.
H1: true .
->
C1: true .
C2: port >= sensorrange__first .
C3: port <= sensorrange__last .
which, correctly, cannot be proved.
4.2.2 Avoiding potentially invalid values
To avoid the potential for an invalid value ensure that the variable to receive the external input or result of the unchecked conversion is of a type which guarantees that any bit pattern received is a valid value. The example from 4.2.1 can be recast as:
package Sensor
--# own in Port;
is
type SensorRange is range 1..10;
procedure Read (X : out SensorRange);
--# global in Port;
--# derives X from Port;
end Sensor;
package body Sensor
is
type Word is range 0 .. 65535;
-- type chosen so that any bit pattern is a valid value
Port : Word;
for Port'Address use ...;
--# assert Port’Always_Valid;
procedure Read (X : out SensorRange)
is
Local : Word;
begin
Local := Port;
if Local <= Word (SensorRange'Last) and
Local >= Word (SensorRange'First) then
X := SensorRange (Local);
else
--return default value
X := SensorRange'First;
end if;
end Read;
end Sensor;
The Always_Valid assertion is recommended to inform the SPARK Examiner that an invalid value will not be read from the attributed external variable (see section 4.2.4).
This example results in a provable set of run-time check VCs.
4.2.3 Input validity and the ‘Valid attribute
The Examiner does take note of the fact that Ada does not require a constraint check for an assignment between identical subtypes (although an Ada compiler is at liberty to perform a run-time check) so it is possible, in SPARK 95, to use a local variable and the 'Valid attribute to validate an input data item. For example, the body of procedure Read could be rewritten thus:
procedure Read (X : out SensorRange)
is
Local : SensorRange;
begin
Local := Port; -- Examiner does not generate check because subtypes are same
-- However, the compiler is at liberty to place a run-time check here
if Local'Valid then
X := Local;
else
-- return default value
X := SensorRange'First;
end if;
end Read;
The example assumes that the Ada compiler used to compile the code does not generate a run-time check for the assignment of “Port” to “Local” or that the unit has been compiled with checks suppressed.
This gives the richer set of VCs:
For path(s) from start to run-time check associated with statement of line 156:
procedure_read_1.
H1: true .
H2: sensorrange__valid(port) .
->
C1: port >= sensorrange__first .
C2: port <= sensorrange__last .
For path(s) from start to run-time check associated with statement of line 159:
procedure_read_2.
H1: true .
H2: not (sensorrange__valid(port)) .
->
C1: sensorrange__first >= sensorrange__first .
C2: sensorrange__first <= sensorrange__last .
For path(s) from start to finish:
procedure_read_3.
H1: true .
H2: sensorrange__valid(port) .
H3: port >= sensorrange__first .
H4: port <= sensorrange__last .
->
C1: true .
C2: port >= sensorrange__first .
C3: port <= sensorrange__last .
procedure_read_4.
H1: true .
H2: not (sensorrange__valid(port)) .
H3: sensorrange__first >= sensorrange__first .
H4: sensorrange__first <= sensorrange__last .
->
C1: true .
C2: sensorrange__first >= sensorrange__first .
C3: sensorrange__first <= sensorrange__last .
The last 3 VCs are directly provable and the first is also provable given the defined semantics of the 'Valid attribute and the Examiner VC Generator automatically generates proof rules defining the sensorrange__valid function to complete the proof formally.
4.2.4 Input data validity and the ‘Always_Valid assertion
As described section 4.2.1, the validity of input data is an important topic in ensuring the robustness of SPARK programs. As noted, by default, the Examiner makes no assumption about the range or validity of a value that is read directly from an external variable. This is safe, but is sometimes over-conservative when an external value definitely has no possible invalid values.
To this end, SPARK provides an “Always_Valid” assertion that indicates to the VC Generator that an external variable is to be “trusted” in that a value read from it may be assumed to be valid at all times.
Syntax
Syntactically, the Always_Valid assertion is a type_assertion in the grammar, which is in turn a form of basic_proof_declaration:
type_assertion :
base_type_assertion
| alwaysvalid_variable_assertion ;
alwaysvalid_variable_assertion :
proof_context assert
dotted_simple_name attribute_ident semicolon annotation_end ;
Static Semantics
The attribute_ident in this assertion must be ‘Always_Valid. The prefixing dotted_simple_name must denote either
· An external variable of mode “in” that is of a scalar type
· A field of a record object which is of a scalar type, where the record object is an external variable of mode “in”.
The object denoted by the prefix must have been previously declared within the same declarative region as the assertion itself.
Examples:
Port : Word;
for Port'Address use ...;
--# assert Port’Always_Valid;
Port2 : R; -- where R is a record type with a scalar field F1
-- and Port2 is an “in” mode external variable
for Port2’Address use ...;
--# assert Port2.F1’Always_Valid;
Dynamic semantics
The assertion has three significant effects:
· The generation of warnings 392 and 393 is suppressed for references to that external variable.
· When the external variable is read, the VC Generator generates an additional hypothesis to indicate that the variable is considered to be valid.
· The VC Generator generates additional proof rules indicating that the value of an object that is considered to be “Always Valid” may be assumed to be within the range of its scalar subtype.
Example
The first example in section 4.2 above showed how a normal untrusted external variable results in an unprovable VC:
For path(s) from start to finish:
procedure_read_1.
H1: true .
->
C1: true .
C2: port >= sensorrange__first .
C3: port <= sensorrange__last .
Now consider a similar package, but where the Port being read returns a 16-bit modular type. In this case, we assume that the actual hardware device being read can only ever return 16 bits of information, so that there are no invalid values for this type. In this case, we can indicate to the Examiner that the external variable is considered to be always valid, thus:
package Port
--# own in S : T;
is
type T is mod 2**16;
function Read return T;
--# global in S;
end Port;
package body Port
is
S : T;
for S'Address use 16#FFFF_0000#;
--# assert S'Always_Valid;
function Read return T is
Tmp : T;
begin
Tmp := S;
return Tmp;
end Read;
end Port;
Firstly, the Examiner does not report warning 392 for the body of the function Read:
+++ Flow analysis of subprogram Read performed: no
errors found.
Secondly, the unsimplified VC for Read appears as:
function_read_1.
H1: true .
H2: t__always_valid(s) .
->
C1: true .
C2: s >= t__first .
C3: s <= t__last .
With an additional FDL declaration:
function t__always_valid(integer) : boolean;
and proof rules:
read_rules(3): X <= t__last may_be_deduced_from
[ t__always_valid(X) ].
read_rules(4): X >= t__first may_be_deduced_from
[ t__always_valid(X) ].
read_rules(5): t__always_valid(s__tail(X)) may_be_deduced_from
[ t__always_valid(X) ].
read_rules(6): t__size >= 0 may_be_deduced.
read_rules(7): t__first may_be_replaced_by 0.
read_rules(8): t__last may_be_replaced_by 65535.
Rules 3, 4, 7 and 8 allow C2 and C3 above to be fully proven by the Simplifier.
Sometimes, one of the hypotheses for a VC will be demonstrably false or the hypotheses will be mutually contradictory. This can only arise from the existence of a non-executable path through the code: either because of a branch which can never be taken or because a previous statement will always generate a run-time error. In the latter case there will always be a preceding VC with a provably false conclusion. All lines following the VC with a false conclusion are non-executable in the sense that they can never be reached.
The proof of a VC obtained from the Examiner with Run-time Checker shows that the error it was generated to guard against cannot occur. Ideally we will wish to prove all the VCs generated to show that the entire SPARK source is free from most potential run-time errors as specified in section 2.1. The Examiner will produce a large number of VCs; however, many of these are of relatively simple form. The SPADE Automatic Simplifier should therefore routinely be applied to the VCs produced and which will typically reduce them very significantly. Where a VC cannot be proved this may indicate a possible run-time error or that the VC is true but beyond the capability of the Simplifier tool. The most common cases where the Simplifier will not be able to prove a VC are:
· The VC depends on the properties of a predefined type or a base type for which no replacement rule is available. Suitable rules for the predefined integer and real types and various system values can be generated by specifying a configuration file for the target platform as described in [1].
· The VC includes a quantifier describing the behaviour of a structured object.
· Proof of the VC requires more information about the contents of particular elements of a structured constant than is available from the proof rules generated from such constants.
In some cases the provision of additional proof rules will allow automatic simplification. VCs which cannot be simplified automatically may be provable with the assistance of the SPADE Proof Checker available from Praxis High Integrity Systems or by use of rigorous argument.
Note that if the SPADE Automatic Simplifier detects false or contradictory hypotheses, it will conclude that the VC is proven by contradiction: this will always indicate a non-executable path as described in section 4.2.5 above.
The validity of a proof that a SPARK program is free from run-time errors depends on some important assumptions; these are discussed below.
4.4.1 Absence of data-flow errors
It is essential that all variables referenced are given well-defined values before use; this condition is achieved if the program concerned is free from data flow errors. The data flow error messages which might invalidate run-time check generation are listed below. Of particular significance is the initialization of objects of structured types. The Examiner generates RTCs on the basis that all elements of such an object are defined and lie within the appropriate subtype range; this assumption is valid if the Examiner has not reported a data flow error because, for example, the object has been fully initialized with an aggregate. There are two common cases where the Examiner will report a data flow error in connection with structured objects and these require special care.
4.4.1.1 Array initialization in a loop
If an array is initialized in a loop, rather than with an aggregate, the Examiner will report a data flow error on the first write to the array. This is because the value of the array after the write is considered to be its value beforehand with one element overridden to a new value. Therefore the final value of the array depends on its initial value. Often this data flow error can safely be ignored provided all required elements of the array are actually correctly initialized. If the validity of the proof of absence of run-time errors is not to be compromised there is an obligation to show that the initialization is complete. It is recommended that array objects are initialized with an aggregate wherever possible.
4.4.1.2 Semantically unnecessary initialization
There are cases where the initialization of a structured object is unnecessary because of the way in which it will be used. For example, a stack might be implemented as an array and a stack pointer. Provided operations are limited to push and pop and that popping an empty stack is prohibited then the stack can safely be emptied by initializing the stack pointer without the need to write to all elements of the array. Any element of the array read by a pop operation must previously have been well-defined by a preceding push operation and the undefined array elements can never be accessed. If this approach is taken then there is an obligation to show that each array element is defined before it is accessed; the Examiner will continue to assume that all array elements are well-defined and will not provide automatic assistance in the discharge of this obligation.
4.4.1.3 Significant data-flow error messages
The following data error messages indicate errors which may invalidate the assumptions required for the effective generation of run-time checks. The messages are listed by their section and reference number in the Examiner User Manual [1].
· Section 8.3.1 Data-flow errors: errors 20, 23, 501, 504; these errors indicate the possible presence of random data values which invalidate the run-time checks for the subprogram in which they appear.
· When generating run-time checks involving procedure call statements, the Examiner assumes that exports from the called procedure are valid, in-type values. This assumption may be invalid if the called subprogram contains data flow errors of the kind listed in the previous bullet. Error 602 from Section 8.3.4 of [1] indicates that an export, which the Examiner assumes is valid, depends on some undefined (random) value.
· Section 8.3.5, Error 34 indicates that a parameter or global which has been identified as an import only has actually been redefined. Run-time checks of any caller of the subprogram which exhibits this error may be invalid.
· Section 8.3.6, Error 31 indicates that a parameter or global is an export of a subprogram but that it has not been given a value. Run-time checks of any caller may be invalid.
4.4.2 Assumption that called subprograms return
As described above, checks are generated for a procedure call statement that imported actual parameters are in the range of the corresponding formals and, on return, assumptions are provided that exported actual parameters are in range. Implicit in this is the assumption that a run-time error does not occur in the body of the called subprogram. A full proof of absence of run-time errors therefore requires a bottom-up analysis with each subprogram being shown to be exception-free (or adequately guarded against the calling conditions that would cause a run-time error) before checking uses of it.
4.4.3 Effects of concurrency when using RavenSPARK
Proof of absence of run-time errors is largely unaffected by concurrency; however, care is needed where multiple tasks communicate via shared data. This is especially true where the shared data is a protected variable of a pragma Atomic type. Consider the case where Task A generates shared data which Task B consumes. An error in task A, such as returning an invalid value form an external variable, may result in a run-time error occurring in Task B even though it has been possible to prove the body of Task B to be exception-free. In this case it will not have been possible to prove Task A to be free from errors. The situation is directly analogous to sequential code where a similar error in a called subprogram may be revealed by an exception in the caller. For sequential code we can protect against this by a bottom-up analysis as described in the preceding section. For concurrent programs we need to extend this to included not just called subprograms but concurrent tasks that share data. In the example given, we need to prove exception freedom for both task A and B to be sure that neither is adversely affected by the other.
Ada real number arithmetic is inexact. For this reason run-time checks for expressions and statements involving real numbers cannot be generated to the same degree of precision as for other scalar types. In particular, cumulative rounding errors may cause run-time errors to occur. As standard, the Examiner with Run-time Checker does not produce VCs for real expressions and warns when they are encountered. Note that particular care is needed when a statement includes both real and discrete expressions, for example updating an array of real numbers; here VCs will be generated for the discrete index expression but not for the real updating expression.
There is one exception to the rule that VCs are not generated for real expressions: a check for division by 0.0 is made.
Some tool support for the proof of absence of run-time errors of programs using real numbers is available (see Section 3.2); users for whom this is important should contact Praxis High Integrity Systems.
VCs cannot be generated for programs containing cyclic paths unless these are first “cut” with a suitable assertion in the form of a loop-invariant. Because the Examiner with Run-time Checker is intended to operate on code containing only the mandatory annotations of SPARK the required loop invariant may not be present. To enable generation of VCs to continue, the Examiner inserts a default loop invariant at the head of any loop in which a user-inserted assertion is not found. When this is done a suitable warning is issued stating where the assertion has been placed.
The default assertion states the subprogram’s precondition is satisfied (decorating variables which are both imported and exported with ~ to show that the precondition is satisfied in terms of the their initial values) and that any imported variables were within their types on entry to the subprogram. If the subprogram does not use unchecked conversions or directly read an external variable and there are no data-flow errors of the sort described in section 4.4.1.3, local variables of the subprogram are considered to be in-type. In the case of for loops, the invariant also states that the loop counter is in its subtype. If a subprogram has neither precondition nor imports or suitable local variables, the default assertion reduces to “true”.
There are two limitations concerning the automatic cutting of loops: incorrect detection of an uncut cyclic path, and the incomplete propagation of information through an assertion. The last of these applies wherever an assertion occurs and is covered later in this section.
The Examiner uses a simple search of the syntax tree to try to find a user-supplied loop-invariant, stopping as soon as one is found. Nested loops are not entered in order to prevent a loop-invariant in an inner loop obscuring the need for one on the outer loop. This simple mechanism should provide the desired behaviour for most common situations; however, there are two situations in which the user needs to be careful.
4.5.2.2 Failure to detect an uncut cyclic path
The first situation occurs when a loop contains an assertion but this does not cut all possible paths through the loop body as shown in the example below. The simple search will find the assertion in the body of the loop but does not know that it does not cover all possible paths within the loop so no default assertion will be inserted. If this occurs the VC file for the subprogram concerned will contain an error message as described in [1].
while i < 10
loop
if j > 5 then
j := j + 1;
else
--# assert j < 20;
j := j + 2;
end if;
i := i + 1;
end loop;
4.5.2.3 Insertion of an unnecessary assertion
The second situation involves user-supplied assertions within nested loops which occur before any exit conditions of the inner loop as in the example below. The simple search does not enter the inner loop and will not find the user-supplied assertion so adds a default assertion at the outer loop head; however, this addition is strictly unnecessary since the position of the user-supplied assertion is such as to cut all paths through both the inner and outer loop. Note that a warning message is always generated when a default assertion is inserted.
while i < 10
loop
loop
--# assert j < 20;
j := j + 1;
exit when j > 10;
end loop;
i := i + 1;
end loop;
4.5.3 Incomplete propagation of information through asserts
Because an assertion is considered as a cut in the control flow graph of a subprogram, information known before the assertion is not known after it. A discussion of this can be found in [2]. Where there is a user-supplied loop cutting assertion the Examiner with RTC will conjoin with it the type and precondition information used as the default assertion which was described in section 4.5.2.1. Where this information is insufficient to prove VCs occurring after the assertion it will be necessary to strengthen it appropriately. In the case of an automatically-inserted, default assertion it may be necessary to replace it with a suitable user-supplied one.
4.5.4 Intermediate expression overflows
With the command line switch /RTC (-rtc for Sun or Linux) the Examiner does not generate VCs to guard against overflow in expressions. For example:
type T is range -128 .. 128;
...
X : T;
...
X := (X + 128) - 128;
While it is clear that no run-time error can occur in the assignment to X if the expression is fully evaluated there is a real possibility of an overflow occurring during evaluation of the sub expression (X + 128). The Examiner does provide protection from such overflows if the /EXP (-exp for Sun or Linux) switch is used; this is discussed in a later section.
The Examiner with Run-time Checker generates replacement rules enabling the SPADE Simplifier to reason about properties of user-defined types such as their bounds. Rules cannot be generated for predefined types such as integer because their bounds are compiler dependent and are consequently not visible to the Examiner. Where a SPARK source makes use of predefined types the Simplifier may not be able to prove the VCs that result. It is possible to obtain values for the bounds of predefined types from the compiler and make them available to the Examiner using a configuration file for the target platform as described in [1].
4.5.6 Package initialization parts
The Examiner does not generate VCs for package initialization parts. Statically-determinable constraint errors will be detected during well-formation checking of package initialization.
4.5.7 Aggregates of multi-dimensional arrays
As described in [2], VCs cannot be generated from aggregates of multi-dimensional arrays. The Examiner issues a suitable warning when this is attempted but still generates VCs. VCs associated with the aggregate will contain references to an identifier unknown_cell_kind, or an illegal Prolog variable, which will cause the SPADE Simplifier to report type checking failures.
5 Detection of Intermediate Expression Overflows
When the command line switch /exp (-exp for Sun or Linux) is used the Examiner generates additional VCs to guard against overflow during expression evaluation. VCs are generated for all unary and binary operators.
Where an expression contains operators of the same precedence a compiler is permitted to re-order the expression even if this results in a run-time error where left-to-right evaluation would not have done so. This permission is given in LRM 11.6(5) for Ada 83 and 4.5(13) for Ada 95. The Examiner generates VCs on the basis of left-to-right evaluation but will issue a warning message (included in the listing and report files) if an expression is vulnerable to change in this way. It is highly recommended that such expressions are parenthesised to make their evaluation order unambiguous.
An overflow occurs during expression evaluation when the result of applying an operator cannot be contained in the base type of the type returned by the operator. The size of this base type is determined by the compiler and is not normally available to the Examiner for the purpose of generating rules, unless it is specified using a type assertion annotation. This section illustrates the use of this facility.
Suppose we have the following type declaration:
type T is range 1 .. 10;
The examiner cannot know the range of the corresponding base type chosen by a compiler. The user, though, may be able to determine which base type is used through inspection of a compiler's documentation, or by experiment, so SPARK allows a base type assertionannotation to assert the compiler's choice in the source text. It is used as follows:
type T is range 1 .. 10;
--# assert T'Base is Short_Integer;
The type on the right-hand side must be one of the predefined numeric types defined in package Standard, which is supplied by the target configuration file. To be useful, the configuration file for the target platform must supply a well-formed type declaration for any such predefined numeric types, such as Short_Integer. For example, the target configuration file might contain a declaration of Short_Integer as follows:
type Short_Integer is range -32768 .. 32767;
This declaration, along with the base type assertion annotation, allows the Examiner to generate proof rules for the Simplifier that allows VCs arising from Overflow_Check to be fully discharged.
5.2.1 Overflow checks and dynamic universal integer expressions
Rarely, a universal integer expression is evaluated dynamically (i.e. at run-time) in SPARK. In this case, the expression is evaluated using a base type whose range is equivalent to System.Min_Int .. System.Max_Int. Again, the target configuration file (in SPARK95 only) or a shadow specification of package System can be used to specify these constants so that such VCs may be automatically discharged by the Simplifier.
5.3.1 Provide actual values as proof rules
As for predefined types such as integer we can provide rules giving the Simplifier the actual value of the bounds of base types. These can either be obtained by writing a test program to obtain the exact values or by using information supplied by the compiler vendor. This approach allows proof of absence of overflow to be established for a particular compiler and target processor.
5.3.2 Use of conservative values
The Examiner generates rules for base types of the following form:
integer__base__first <= integer__first may_be_deduced.
integer__base__last >= integer__last may_be_deduced.
If a value has been provided for integer’first and integer’last using a configuration file for the target platform then these rules are sufficient to show that overflow will not occur provided intermediate expression values remain in the range integer’first.. integer’last.
Alternatively, user defined proof rules can be provided allowing the bounds of base types to be replaced by arbitrary but conservative values. For example integer__base__last may_be_replaced_by 32767. would allow proof of absence of overflow for all target platforms where the underlying integer type was at least 16 bits long.
5.3.3 Use of explicit type conversion
Given: type T is range -128..128; we can guard against expression overflow, without knowing the size of T’Base’First and T’Base’Last by using some larger, intermediate, user-defined type within the expression. For example we can replace the statement:
X := X * X + X; (where X is of type T)
by
X := T(ET(X) * ET(X) + ET(X));
(where ET is a user-defined type somewhat larger than T)
With expression checks enabled we will get VCs in terms of ET’Base’First and ET’Base’Last as before; however, we will have proof rules for ET’First and ET’Last and with these (if ET is big enough) we will be able to show that the sub-expression results lie within the type ET. Since we also know that a base type is always at least as big as any subtype of it we will have also proved that the sub-expression results lie in the base type of ET.
6 Strategies for Eliminating Run-time Errors
Elimination of run-time errors requires the SPARK code to be considered procedure by procedure in a mostly bottom-up order showing that each is exception-free. Where the use of the Examiner with Run-time Checker shows a subprogram to contain a potential run-time error there are a number of approaches that can be used to eliminate it or show that the risk it poses is not significant.
6.1 Strengthening specifications
One way of removing a potential run-time error from a subprogram is to strengthen its specification with a precondition which disallows calling it under the conditions which would cause it to produce a run-time error. For example the Inc procedure at section 2.3 can be made safe from run-time errors by adding the precondition --# pre X < T’Last; The presence of a suitable precondition provides additional hypotheses allowing the VCs to be proved. Where a subprogram is annotated in this way the Examiner will generate an additional VC in all the places from which it is called so that it can be proved that it is being called within the limits permitted by its precondition.
Alternatively, it may sometimes be useful to strengthen the postcondition of a called subprogram in order to provide the information needed to show that the caller is free from run-time errors; an example of this approach is given in section 6.1.5 below.
The ease with which a suitable precondition can be expressed for a subprogram depends on the nature of the imports and exports it manipulates. If these are all of concrete Ada types then a simple expression can be used. If, however, they are of private types then they can only be expressed in terms of a proof function. Finally, if the subprogram manipulates truly abstract state contained in a package implementing an abstract state machine then it may not be possible to express a precondition at all unless additional Ada functions are introduced. All three cases are illustrated below using a stack package as an example.
6.1.1 Concrete imports and exports
package Stack
--# own Vector, Ptr;
is
type Index is range 1..10;
type Vectors is array(Index) of Integer;
Ptr : Index;
Vector : Vectors;
procedure Push(X : in Integer);
--# global Vector, Ptr;
--# derives Vector from Vector, Ptr, X &
--# Ptr from Ptr;
--# pre Ptr < Index’Last;
end Stack;
With the state of the stack package visible and expressed in concrete Ada terms we can express a precondition as a SPARK expression.
6.1.2 Private imports and exports
package Stack
is
type Stacks is private;
--# function NotFull(S : Stacks) return Boolean;
procedure Push(S : in out Stacks;
X : in Integer);
--# derives S from S, X;
--# pre NotFull(S);
private
...
end Stack;
Where the push operation modifies an abstract data type in the form of a private type the precondition can only be expressed in terms of a suitably-declared proof function (or by use of a suitable SPARK function as in the following example).
6.1.3 Abstract imports and exports
package Stack
--# own State;
is
function NotFull return Boolean;
--# global State;
procedure Push(X : in Integer);
--# global State;
--# derives State from State, X;
--# pre NotFull(State);
end Stack;
Where the stack is in the form of an abstract state machine a precondition can only be expressed if there is a suitable SPARK function available. In any case it would not be possible for users of the push operation to check that they met the precondition if such a function was not available. Here function NotFull has been declared and exported and the precondition of Push expressed in terms of the implicitly declared proof function associated with it. See [2] for a discussion of implicitly declared proof functions.
With Release 5.0 of the Examiner, the ability to announce abstract own variables as being of a named proof type may provide another means of expressing preconditions in this case; see [2].
Where a formal parameter of a subprogram is an unconstrained array the size of the array is determined by the size of the actual parameter in the calling environment.
Checks on the validity of index expressions which are made inside the body of the subprogram will be in terms of constants representing ‘First and ‘Last of the actual constrained size of the array for a particular call. In general proof contexts have to written in terms of array attributes to be successful and not in terms of the unconstrained array index type.
Attributes such as ‘First, 'Last and ‘Length of the array will not have a constant value for proof purposes since the value will vary from call to call depending on the actual parameter passed.
For example:
type Atype is array(Integer range <>) of Integer;
|
|
procedure P(A : in out Atype) --# derives A from A; --# pre A’First <= 99 and --# A’Last >= 99; is ... ........A(99)......... ... end P; |
VCs for the index expression here will be a__index__subtype__1__first£ 99 £ a__index__subtype__1__last and in order to complete a general proof of the absence of run-time errors the pre condition in terms of A’First and A’Last is required. |
6.1.5 Strengthened Postcondition
When performing a Push operation using the stack package from section 6.1.2 we would have to show that the precondition — NotFull(State) — is true at the point of call. Given the code sequence:
...
Stack.Pop(TheStack, X);
...
Stack.Push(TheStack, Y);
....
We could obtain the necessary information by strengthening the postcondition of Pop as follows:
--# post NotFull(State);
which states that “a stack from which something has just been popped cannot be full”.
An alternative to strengthening the specification of a subprogram is to make it exception-free under all calling circumstances. This may involve the addition of checks in the form of conditional statements inside the subprogram to guard against error conditions. The use of conditionals in this way is sometimes known as defensive programming: the Examiner with Run-time Checker provides a focused way of applying this technique. Three examples of defensive programming, using the Inc subprogram of section 2.3 follow. In each case the addition of a guard on the statement which increments the variable X makes the subprogram free of run-time errors under all circumstances where it is successfully called.
6.2.1 Indicating failures to the calling environment
procedure Inc(X : in out T;
Overflow : out Boolean)
--# derives X, Overflow from X;
is
begin
if X = T’Last then
Overflow := True;
else
X := X + 1;
Overflow := False;
end if;
end Inc;
6.2.2 Diversion of control to an error handler
procedure Inc(X : in out T)
--# global ErrorHandler.State;
--# derives X, ErrorHandler.State from *, X;
is
begin
if X = T’Last then
ErrorHandler.FatalError(ErrorHandler.OverflowInInc);
else
X := X + 1;
end if;
end Inc;
6.2.3 Limiting or saturation of operations
procedure Inc(X : in out T)
--# derives X from X;
is
begin
if X < T’Last then
X := X + 1;
end if;
end Inc;
In some cases a potential run time error can be shown by system-level argument not to pose a risk in practice. Examples include counters that are incremented at a rate which precludes the possibility of overflow because the limit could not be reached during the life of the system. For example a counter in an aircraft system, implemented as a 32-bit integer and incremented once per second from a start value of zero, would take over 63 years to overflow; this is likely to exceed the maximum flight time (or even service life) of the aircraft! Such system-level arguments justify leaving a particular VC unproved; they should of course be carefully documented and form part of the safety justification for a system.
Document Control and References
Praxis High Integrity Systems Limited, 20 Manvers Street, Bath BA1 1PX, UK.
Copyright Praxis High Integrity Systems Limited 2009. All rights reserved.
$CVSROOT/userdocs/Examiner_GenRTCs.doc (was previously S.P0468.73.30)
Issue 0.1:(25th January 1996) Initial version
Issue 0.2: (23rd February 1996) after review S.P0455.7.14.
Issue 1.0: (1st March 1996) at closure of review S.P0455.7.14.
Issue 2.0: (30th June 1997) conversion to new standard document format.
Issue 2.1: (28th August 1997) Changes for Examiner Release 3.0, made provisional
Issue 3.0:(2nd September 1997) After formal review
Issue 3.1: (28th June 2000) Draft changes for Examiner Release 5.0
Issue 4.0: (5th July 2000) After inspection by Ian O’Neill
Issue 4.1: (12th July 2001) Draft changes for Examiner Release 6.0
Issue 6.0: (13th Aug 2001) After review by jarh
Issue 6.01: (5th February 2002) CFRs 992, 993, 999: describe new support for target configuration file, type assertions, dynamic universal expressions, and how these impact expression overflow checks.
Issue 6.10: (24th June 2002) Updates resulting from review S.60468.79.77
Issue 7.0: (9th April 2003) Updated to new template format.
Issue 8.0: (4 June 2003) Changes to new template, final format.
Issue 8.1: (10 June 2003) Final updates for Release 7.0, following review.
Issue 8.2: (10 March 2004) Explanation of assumption that local values are in type (SEPR 1619). Add note on effect of concurrency.
Issue 8.3: (23 November 2004) Company name change only.
Issue 8.4: (5 January 2005) Definitive issue following review S.P0468.79.88.
Issue 8.5: (22 November 2005) Line Manager change
Issue 8.6: (24 February 2006) Restore italics in table in section 2.1.
Issue 8.7 (24 November 2006) Add section 4.2.2 describing Always_Valid assertion and revise notes on unconstrained arrays.
Issue 8.8 (20 December 2006) Page 18 remove bold and change two effects to three. Definitive issue following review S.P0468.79.92.
Issue 8.9 (8 May 2008) Updated description of VCs generated for assignments from own ‘in’ variables in line with changes for SEPR 2287.
Issue 8.10 (29 May 2008) Updated for modified implementation of SEPR 2287 and tidied up some other subsumed information.
Issue 8.11 (10 June 2008) Final updates for release 7.6 following review of SEPR 2287.
Issue 8.12: (11th July 2008) Updates following review S.P0468.79.93
Issue 8.13: (7th January 2009) Factored out contact details.
Issue 8.14: (2nd February 2009): Modify copyright notice.
None.
1 SPARK Examiner User Manual.
2 The Generation of Verification Conditions for SPARK Programs.
3 SPADE Automatic Simplifier User Manual
4 SPADE Proof Checker User Manual
5 The Specification of Check Statements for the Absence of Run-time Errors