SPARKSimp Utility

User Manual

 

 

 

 

 

 

 

 

 

 

 

SPARKSIMP/UM

Issue: 1.0

Status: Definitive

12th November 2010

 

DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date author:varchar=author projectname:varchar=DocumentSet

Issue 1.0, Definitive, 12th November 2010

000_000 User Manual

 

 

Originator

 

 

SPARK Team

 

 

Approver

 

 

SPARK Team Line Manager

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 


Copyright

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 Altran Praxis Limited.

 

Limited Warranty

Altran Praxis 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.

Altran Praxis 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 Altran Praxis Limited accepts no liability for any programs or data stored or processed using Altran Praxis Limited products, including the costs of recovering such programs or data.

SPADE is a registered trademark of Altran Praxis Limited.

Note:  The SPARK programming language is not sponsored by or affiliated with SPARC International Inc. and is not based on SPARC™ architecture.


 

Contents

1          Introduction

1.1      Basic functionality

1.2      Command-line switches and options

1.3      Examples

1.4      Limitations

Document Control and References

Changes history

Changes forecast

Document references

 

 


1                       Introduction

SPARKSimp is a simple “make” style tool for the SPARK analysis tools. Currently, it supports the Simplifier, ZombieScope and ViCToR. It applies the Simplifier (and ViCToR, if requested, please see the Victor_Wrapper user manual [1] for more information) to all .vcg files and ZombieScope to all .dpc files it finds in a directory tree.

1.1               Basic functionality

With no options or switches SPARKSimp performs the following operations:

·          The commands “spadesimp” and “zombiescope” are searched for on the user’s current PATH environment variable. If one of them cannot be found, then an error is reported and SPARKSimp terminates. If the binaries are found, then their locations are noted.

·          The tree of directories and files rooted at the current working directory is searched for any files ending in .vcg or .dpc. For each .vcg file, SPARKSimp attempts to find the corresponding .siv file and compares their time-stamps[1]. Similarly, for each .dpc file, SPARKSimp attempts to find the corresponding .sdp file and compares their time-stamps.

·          If the .siv file is out of date or does not exist, then the .vcg file is added to a list of files to be simplified. If the .sdp file is out of date or does not exist, then the .dpc file is added to a list of files to be zombiescoped.

·          SPARKSimp runs the “spadesimp” command found in step 1 for each .vcg file on the list and runs the “zombiescope” command found in step 1 for each .dpc file on the list. The screen output of these commands is not recorded by default (although the .siv, .slg, .sdp and .zlg files, of course, remain.)

·          If there are errors which prevent the Simplifier or ZombieScope from completing – for example Simplifier or ZombieScope is unable to open a file to be analysed – SPARKSimp prints the file name and the reason for failure to the screen.

The use of SPARKSimp is normally combined with the POGS tool to manage and record the status of a large program proof effort.


1.2               Command-line switches and options

The syntax of the command line for SPARKSimp is as follows:

sparksimp [-a] [-v] [-V] [-n] [-ns] [-nz] [-t] [-r] [-l] [-e] [-p=N]

          [-x=Sexec] [-z=Zexec]

          [-sargs {simplifier_options}]

          [-zargs {zombiescope_options}]

Please note that the SPARKSimp options relating to ViCToR are not supported yet and are not documented here. For further details please see the ViCToR Wrapper user manual [1].

The various switches have the following effect:

-a               All Files.  All eligible .vcg and .dpc files found are added to the list of those to be analysed, ignoring their time-stamps.

-v                Version.  Reports SPARKSimp version and then terminates.

-V               Verbose.  Additional details of directory and file searching are produced.

-n               Don’t Run.  SPARKSimp prints the Simplifier and ZombieScope commands but does not actually run the tools. Useful for a “dry run” to see what analysis is required in a directory tree.

-ns             No Simplifier  SPARKSimp ignores VCG files when searching and hence Simplifier will not be invoked.

-nz             No ZombieScope  SPARKSimp ignores DPC files when searching and hence ZombieScope will not be invoked.

-t                Sort files.  The list of .vcg  files to be simplified is sorted by size so that the largest file is simplified first.  Without this option, the list is processed in the order in which the files were found.

-r                Reverse order.  Reverse the order in which the list of .vcg files is simplified. Can be used in conjunction with -t to get smallest-file-first order.

-l                 Log output.  The screen output of Simplifier and ZombieScope is logged to files when this option is present.  For a VCG file xxx.vcg, the screen output is recorded in the file xxx.log and for a DPC file yyy.dpc, the screen output is recorded in the file yyy.zsl. Without this option, Simplifier’s and ZombieScope’s screen output is discarded.

-e               Echo output.  The output of Simplifier is echoed to the screen.  Note that “-e” and “-l” may be used together.

-p=N          Number of processes.  The number (N) of instances of the Simplifier and/or ZombieScope to run concurrently.  If this option is not specified then the default is to run a single instance.  Each concurrent instance of the Simplifier will require a licence. When this option is used the -e option is ignored.

-x=Simpexec

                   Simplifier Executable.  The parameter Simpexec specifies an alternative version of the Simplifier to use.  Simpexec may include an absolute or relative path name or a simple filename may be given provided the file is in a directory in the user’s PATH environment variable.  The standard executable extension (e.g. .exe for Windows) is appended to the file name if an extension is not specified.  If -x option is not specified the standard Simplifier ‘spadesimp’ is run provided that it is located within a directory in the user’s PATH environment variable.

z=Zombexec

                   ZombieScope Executable. The parameter Zombexec specifies an alternative version of ZombieScope to use. Zombexec may include an absolute or relative path name or a simple filename may be given provided the file is in a directory in the user’s PATH environment variable. The standard executable extension (e.g. .exe for Windows) is appended to the file name if an extension is not specified.  If -z option is not specified the standard ZombieScope ‘zombiescope’ is run provided that it is located within a directory in the user’s PATH environment variable.

-sargs        Additional Simplifier arguments.  All options following this switch (but before the zargs switch) are passed to all invocations of the Simplifier unchanged.  This can be used to set Simplifier options, such as plain output and so on.

-zargs        Additional ZombieScope arguments.  All options following this switch are passed to all invocations of ZombieScope unchanged.  This can be used to set ZombieScope options, such as plain output and so on.


1.3               Examples

This section gives some examples of the use of SPARKSimp:

Command

Action

sparksimp

Simplify and ZombieScope all out-of-date .vcg and .dpc files in this directory tree, in the order found.

sparksimp -nz

Simplify out-of-date .vcg files, ignore any .dpc files. Does not invoke ZombieScope.

sparksimp -ns

ZombieScope out-of-date .dpc files, ignore any .vcg files. Does not invoke Simplifer.

sparksimp -a -sargs -plain –zargs -plain

Simplify and ZombieScope all .vcg and .dpc files , ignoring timestamps, and passing argument “-plain” to both Simplifier and ZombieScope.

sparksimp -n

Find all .vcg files that require simplification and .dpc files that require ZombieScope in this directory tree, print the Simplifier and ZombieScope commands that would be run, but don not actually run the Simplifier or ZombieScope.

sparksimp -x=spadesimp2p22

Use the simplifier spadesimp2p22 rather than the default simplifier.  The executable ‘spadesimp2p22’ must be in a directory on the user’s PATH.

sparksimp -x=C:\praxis\simplifier\spadesimp2p24

Use the Simplifier located on the given absolute path.


1.4               Limitations

A number of limitations exist in this release of SPARKSimp. These may be addressed in a future release.

·          [TN J312-007] SPARKSimp cannot exploit multiple networked computers to distribute Simplification jobs.

We welcome suggestions and ideas for improvement of SPARKSimp. 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.

Changes history

Issue 0.1  (1st November 2010): Split Simp_UM into two documents: One for the Simplifier itself and one for SPARKSimp. Quote TN for the distributed sparksimp. Reword to emphasise that sparksimp is a general purposes analysis tool and no longer is limited to just running the Simplifier.

                   Issue 0.2 (5th November 2010): Addressed review comments.

Issue 1.0 (12th November 2010): Definitive issue for release 9.1.

Changes forecast

None.

Document references

1               ViCToR Wrapper User Manual



[1] These are the time-stamps as recorded by the filesystem.