SPARK 16: Generating Counterexamples for Failed Proofs
by David Hauzar –
While the analysis of failed proofs is one of the most challenging aspects of formal verification, it would be much easier if a tool would automatically find values of variables showing why a proof fails. SPARK Pro 16, to be released in 2016, is going to introduce such a feature. If a proof fails, it attempts to generate a counterexample exhibiting the problem.
Example 1: Saturation Function
Let’s demonstrate this feature on an example of a saturation function. Saturation function is used to ensure that values are in a given range. In our case, we require that the saturation function ensures that a non-negative value is less or equal to 255. The specification of such a function could be:
with Interfaces; use Interfaces;
function Saturate (Val : Unsigned_16) return Unsigned_16 with
SPARK_Mode,
Post => Saturate'Result <= 255 and then
(if Val <= 255 then Saturate'Result = Val);That is, the returned value should be in the required range and moreover, if the input already is in the range, the return value should be equal to the input value. Here is the first implementation of the function:
with Interfaces; use Interfaces;
function Saturate (Val : Unsigned_16) return Unsigned_16 with
SPARK_Mode,
Post => Saturate'Result <= 255 and then
(if Val <= 255 then Saturate'Result = Val)
is
begin
return Unsigned_16'Max (Val, 255);
end Saturate;Running GNATprove, the proof of the postcondition fails and the following counterexample is generated:
Indeed, if the input is 65535, it is bigger than 255 and thus it is returned as a result. The problem here is that Unsigned_16'Min should be used instead of Unsigned_16'Max. If we correct the mistake, the postcondition is proven:
Example 2: Implementation Using Bitwise And
Now let’s try to implement saturation using bitwise and:
with Interfaces; use Interfaces;
function Saturate (Val : Unsigned_16) return Unsigned_16
with SPARK_Mode,
Post => Saturate'Result <= 255 and then
(if Val <= 255 then Saturate'Result = Val)
is
Mask : constant Unsigned_16 := 16#0FFF#;
begin
return Val and Mask;
end Saturate;Running GNATProve, the proof of the postcondition fails and following counterexample is generated:
The counterexample shows us that the bitwise and of input 62464 (01111010000000000) and mask 16#0FFF# (00000111111111111) is 1024 (00000010000000000), which is not in the range. Really, the correct mask is not16#0FFF# (00000111111111111), but 16#FF# (0000000011111111). If we correct the mask, GNATProve proves the postcondition:
Example 3: Stricter Specification
Looking back at the our specification of saturation function, we can see that it does not uniquely define what should be returned for values that are outside the range. Indeed, for these values, the function is allowed to return any value from the range. We could require that a saturation function must for a value outside the range return the closest value from the range. That is, 255 in our case. Let’s specify this using Contract Cases:
with Interfaces; use Interfaces;
function Saturate (Val : Unsigned_16) return Unsigned_16 with
SPARK_Mode,
Contract_Cases => (Val <= 255 => Saturate'Result = Val,
Val > 255 => Saturate'Result = 255);Now let’s try whether our implementations conform this specification. Running GNATProve on the first one shows that it does:
However, GNATProve fails to prove the bitwise implementation and generates the following counterexample:
Really, bitwise and of 32768 (1000000000000000) with a mask 255 (0000000011111111) results in 0. That is, the implementation using bitwise and does conform to this stricter specification.
Example 4: Variable Saturation Range
Finally, we may want to use different saturation ranges for different values. To do this, we can define type Saturable_Value with fields Value representing the actual value and Upper_Bound being an upper bound of the saturation range:
type Saturable_Value is record
Value : Unsigned_16;
Upper_Bound : Unsigned_16;
end record;The specification of the saturation function is as follows:
function Saturate (Val : Saturable_Value) return Saturable_Value with
SPARK_Mode,
Contract_Cases => (Val.Value <= Val.Threshold => Saturate'Result = Val,
Val.Value > Val.Threshold => Saturate'Result =
Val'Update (Value => Val.Upper_Bound));Let’s implement it:
with Interfaces; use Interfaces;
package body Saturate is
type Saturable_Value is record
Value : Unsigned_16;
Upper_Bound : Unsigned_16;
Threshold : Unsigned_16;
end record;
function Saturate (Val : Saturable_Value) return Saturable_Value with
SPARK_Mode,
Contract_Cases => (Val.Value <= Val.Threshold => Saturate'Result = Val,
Val.Value > Val.Threshold => Saturate'Result =
Val'Update (Value => Val.Upper_Bound))
is
begin
return Val'Update
(Value => Unsigned_16'Max (Val.Value, Val.Upper_Bound));
end Saturate;
end Saturate;And try to prove that it is correct:
GNATProve failed to prove both contract cases. The counterexample for the first one shows that if Val.Value is 32767 and Val.Upper_Bound is 65535, Saturate’Result.Value is 65535. Indeed, there is again the same mistake - Unsigned_16'Max is used instead of Unsigned_16'Min.
To get more information about counterexamples, see the Section Understanding Counterexamples of the User’s Guide.