ZombieScope is a new tool in SPARK Pro release 9 that analyses SPARK code to find dead paths, i.e. paths through the code that can never be executed.
Although a program with a dead path may not necessarily be incorrect, a dead path is an indication of a potential code issue. ZombieScope allows the automatic detection of dead paths on a modular basis. Just as the rest of the SPARK toolset, it can be applied to a subprogram even if callers and callees of that subprogram are not yet implemented.
ZombieScope reads .dpc files generated by the Examiner with the -dpc (dead path conjectures) option specified, plus the .fdl file for its data declarations and the .rls file for proof-rules where present. ZombieScope generates two output files: A .sdp (dead path summary) file and a .zlg file which contains a log giving information about the underlying contradiction search performed by ZombieScope. ZombieScope is invoked by SPARKSimp by default and the summary file generated by POGS includes information about the dead path analysis.
Figure 1: Relationship of SPARK Tools for Detecting Dead Paths
This section shows how to use ZombieScope to find a dead path in a very simple example.
2.1 Small Example with Dead Path
Consider the following SPARK program:
1 procedure P (A: in Boolean; X: in out Integer)
2 --# derives X from A, X;
3 is
4 begin
5 if A then
6 if A then
7 P1(X);
8 else
9 P2(X);
10 end if;
11 end if;
12 end P;
The condition of the second if statement, line 6, is redundant. This could for example be due to a cut-and-paste error from the enclosing if statement.
There are three paths through the code from line 5 to 11:
Path 1: 5, 6, 7, 10, 11
Path 2: 5, 6, 9, 10, 11
Path 3: 5, 11
Path 2 is dead since if execution has entered the if branch of the outer if statement, A holds, and for the inner if statement the else branch cannot be executed.
2.2 Generate DPCs and run ZombieScope
Assuming that the above procedure P resides in a package called Dead_Paths, then do:
1) Run Examiner to generate dead path conjectures: spark –dpc dead_paths.adb. This will generate a directory dead_paths containing rls, fdl and dpc files.
2) Run ZombieScope: sparksimp. This will automatically invoke ZombieScope on the dpc files found in the directory dead_paths, producing dead path summary (sdp) files and ZombieScope log (zlg) files. See section 3 for alternative ways to invoke ZombieScope.
3) Run POGS: pogs. This will generate a proof obligation summary file (sum). The summary file shows that ZombieScope has found a dead path.
2.3 Notes on flow analysis mode
Note that the flow_analysis mode chosen (i.e. data or information) does not impact ZombieScope – it will work the same regardless.
Near the end of the POGS summary file, just above the VC summary, we find the ZombieScope summary:
ZombieScope Summary:
-------------------------------------------------------------------------
Total subprograms for which DPCs have been generated: 1
Total number subprograms with dead paths found: 1
Total number of dead paths found: 1
Further up in the summary file, the VC table for procedure P shows that ZombieScope has found a dead path in dpc number 6:
DPCs generated 26-FEB-2010 12:39:16
DPC ZombieScoped 26-FEB-2010 12:39:2
VCs for procedure_p :
-----------------------------------------------------------------------------
| # | From | To | Proved By | Dead Path | Status |
|-----------------------------------------------------------------------------
| 1 | start | rtc check @ 27 | No VCG | Unchecked | -U |
| 2 | start | rtc check @ 27 | No VCG | Unchecked | -U |
| 3 | start | rtc check @ 29 | No VCG | Unchecked | -U |
| 4 | start | rtc check @ 29 | No VCG | Unchecked | -U |
| 5 | start | assert @ finish | No VCG | Live | -L |
| 6 | start | assert @ finish | No VCG | Dead | -D |
| 7 | start | assert @ finish | No VCG | Live | -L |
-----------------------------------------------------------------------------
2.5 Further Information in DPC and ZombieScope Log Files
When POGS reports that ZombieScope has found a dead path, it can be useful to inspect both the corresponding dpc file and zlg file. For our example above, we find the relevant DPC, number 6, in the file p.dpc:
procedure_p_6.
H1: true .
H2: true .
H3: x >= integer__first .
H4: x <= integer__last .
H5: a .
H6: not a .
H7: x >= integer__first .
H8: x <= integer__last .
H9: x__2 >= integer__first .
H10: x__2 <= integer__last .
H11: x__2 >= integer__first .
H12: x__2 <= integer__last .
->
C1: false .
For more detailed information about the analysis ZombieScope has performed on that particular DPC, we can study the file p.zlg:
@@@@@@@@@@ VC: procedure_p_6. @@@@@@@@@@
--- Hypothesis H7 has been replaced by "true". (It is already present, as H3).
--- Hypothesis H8 has been replaced by "true". (It is already present, as H4).
--- Hypothesis H11 has been replaced by "true". (It is already present, as H9)
.
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
### Established a contradiction [P-and-not-P] among the following hypotheses:
H5 & H6.
Here the log points us directly to the two contradicting hypotheses, H5 and H6. The ZombieScope log can be particularly useful when number of hypotheses is very large.
ZombieScope can be run by either
1) command-line invocation of zombiescope directly to a target .dpc file, or
2) command-line invocation of sparksimp, which in turn applies zombiescope to all .dpc files in a directory , or
3) invocation of zombiescope and/or sparksimp from the SPARK menu in the GNAT Programming Studio (GPS).
The command line syntax of zombiescope is given below.
Command-line = “zombiescope [options] Target_File”
Options may be abbreviated by omission of trailing letters, provided that the remaining letters specify the option uniquely.
Where “Target_File” is a .dpc
file. The command line options for ZombieScope are:
|
Option |
Description |
|
help |
Display this command-line usage and list of options. |
|
version |
Display version information and terminate. |
|
nolog |
Do not generate a ZombieScope log file. |
|
log=Log_File |
Specify filename for the ZombieScope log file. |
|
nowrap |
Do not line wrap output files. |
|
plain |
Adopt a plain output style (e.g. no dates or version numbers). |
|
norenum |
Do not renumber hypotheses and conclusions in .sdp files. |
|
hyp_limit=n |
If the number of hypothesis in a DPC exceeds n then ZombieScope will not search for dead paths for the DPC. |
3.2 SPARKSimp - A “Make” Tool for ZombieScope Too
SPARKSimp is a simple “make” style tool for Simplifier and ZombieScope. It finds all the .dpc and .vcg files in a directory tree that require analysis and applies both ZombieScope and Simplifier to them. The detailed functionality of SPARKSimp can be found in the SPARKSimp User Manual [2].
3.3 Running ZombieScope in GPS
In the GNAT Programming Studio (GPS), both zombiescope and sparksimp can be invoked using the SPARK menu, see the document Using SPARK with GPS [5] for detailed instructions.
A dead path is a path through the code that can never be executed, regardless of input. ZombieScope is a tool that can find dead paths. More specifically, ZombieScope will analyse scenarios, called dead path conjectures, that are described both in terms of annotations and executable code. These dead path conjectures may differ from dead paths in the pure executable sense of the word, for example in the presence of subprogram calls and cut-points.
4.1 Soundness and Completeness
ZombieScope is sound, meaning that whenever ZombieScope finds a dead path, the path really is non-executable. However, ZombieScope is incomplete, which means that there may be dead paths in the code that are not detected.
4.2 Subprogram Calls, Contracts and Dead Paths
SPARK toolkit performs modular verification. This means that to verify a subprogram you do not need access to other subprogram bodies, not even the called ones, but only their specifications. This is very useful in incremental development, library usage etc. and it is one of SPARK's main characteristics. A subprogram call will be modelled using the contract of the callee. Simply put, this is done by generating a proof obligation to meet the precondition of the callee at the calling point and an assumption that the post condition of the callee holds after completion of the call. For this reason, ZombieScope will not detect dead paths that depend on interprocedural relations that are not described in contracts.
A cutpoint, specified using the assert statement in SPARK, is a language construct to reduce the number of paths analysed by the SPARK tools. A cutpoint serves as a new root for path exploration and the path exploration tree before the cut point is “forgotten”. This significantly reduces the computational complexity for the SPARK analysis, and is an important feature for example in the reasoning about numerous consecutive conditionals.
Cutpoints also influence dead path analysis. In the presence of a cutpoint, the dead path conjectures will not consist of entire subprogram paths from start to end, but the paths will be cut at the cutpoint. Consequently, ZombieScope will not detect a dead path that is caused by a contradiction between a condition before the cutpoint, and a condition after the cutpoint.
4.4 Dead Statements versus Dead Paths
Readers may be more familiar with the expression “dead statement” or “dead code”, which is different from the concept “dead path”, the latter used in ZombieScope. A statement is called dead if all paths through it are dead. For example, line 9 in example 2.1 is a dead statement because every path passing through it (in this case just path 2) is dead. For another example, consider the following sequence of statements.
1 if A then
2 S1(X);
3 else
4 S2(X);
5 end if;
6 if A then
7 S3(X);
8 else
9 S4(X);
10 end if;
This example contains two dead paths, one with A true, not executing S4, and one with A false, not executing S3. Note that none of the statements S1, …, S4 are dead, because they all have live paths going through them as well. As this example illustrates, it is possible to achieve full branch and statement coverage, but still have dead paths in the code.
4.5 Number of Dead Paths Reported
ZombieScope will report every dead path that it finds when analysing a subprogram from start to finish. A (smallest) dead path is often a subset of many more paths that go from start to finish. Therefore ZombieScope may report many more dead paths than the sub-path where the actual problematic code is. Sometimes the total number of dead paths reported may seem daunting. However, often just one fix gets rid of several dead paths reported.
4.6 ZombieScope Dead Path Analysis
This section very briefly explains the underlying technology of ZombieScope, and points to more detailed documents for the interested reader.
4.6.1 Dead Path Conjectures
Every dead path conjecture produced by the Examiner is of the following form:
Where n is a natural number. The hypotheses H1,…, Hn are the same as for the corresponding VC. They constitute the assumptions that can be made at a particular point in traversing the SPARK program.
4.6.2 Contradiction Search
ZombieScope uses the same underlying technology as the Simplifier does in trying to prove a formula of the above form: it performs a search for contradictions among the hypotheses. If a contradiction can be established, then the execution path through the source code to which this DPC corresponds is non-traversable. Thus, we have found a dead path. The search for a contradiction takes place in five phases. The details of these are described in the SPARK Simplifier User Manual [2].
ZombieScope may be slow to analyse a DPC with a large number of hypotheses. In these cases, if the tool is too slow for practical use, then the analysis of these DPC should be suppressed. One workaround is to have a separate meta-file for packages known to generate problematic DPCs and run spark with the option –dpc for that meta-file. Please report such cases to us so that we can improve ZombieScope for practically relevant problems.
In ZombieScope 9.0.1, users can specify a hypothesis limit (-hyp_limit=n) for ZombieScope and it will not search for dead paths for DPCs that exceeds the limit. A better workaround for 9.0.1 and above is to specify a limit that provides acceptable performance.
We welcome suggestions and ideas for improvement of ZombieScope. Please feel free to contact us.
Document Control and References
Altran Praxis Limited, 20 Manvers Street, Bath BA1 1PX, UK.
Copyright Altran Praxis Limited 2010. All rights reserved.
SVN: trunk/userdocs/ZombieScope_UM.doc.
Issue 0.1: (19th January 2010): Draft sketch.
Issue 0.2: (5th February 2010): Rebrand to Altran Praxis Limited.
Issue 0.3: (26th February 2010): Final version.
Issue 1.0: (1st March 2010): Definitive version following reviews.
Issue 1.1: (12th March 2010): Added description for new hyp_limit flag TN[J302-029].
Issue 1.2: (4th October 2010): Clarified that you can use ZombieScope with code written in flow=data mode. [J929-034]
Issue 1.3: (12th October 2010): Correct references to the Examiner.
Issue 1.4: (5th November 2010): Corrected reference to the SPARKSimp manual.
None.
1 Examiner User Manual
3 SPARKSimp User Manual
4 POGS User Manual