You can run SAFARI from the command line. This page introduces the reader to the two main aspects of running SAFARI: how to write input files and which options should/must be enabled for successful verification.
Example
SAFARI takes in input a transition system made by one initial set of states, some transitions and some unsafe configurations.
The example constitutes a function "find" which takes in input an array and two integers denoting respectively the length of the array and an element we want to search for inside the array. The function is annotated with precondition and postcondition.
procedure Find( a: [int]int , L:int , n:int ) returns ( c:int )
requires L > 0;
ensures ( (c >= L) ==> (forall x:int :: (x >= 0 && x < L) ==> a[x] != n ) ) ;
{
c := 0;
while ( c < L && a[c] != n ) {
c := c+1 ;
}
}From this source code we can generate the input code for SAFARI by adding a fresh variable pc taking value over a finite set of locations.
The Find function is represented by the following code:
* define a new domain for the program counter */
define-type locations { pc_1 , pc_2 };
/* definition of the variables */
locations pc;
int c, L, n;
int a[int];
/* set of initial states */
initial ( ) {
pc = pc_1 && L >= 0 && c = 0
}
/* set of error states */
unsafe ( exists x:int ) {
pc = pc_2 && c >= L && x >= 0 && x < L && a[x] = n
}
/* transitions */
transition ( exists x:int ) {
guard: pc = pc_1 && c < L && x = c && a[x] != n
update:
c := c + 1;
}
transition ( ) {
guard: pc = pc_1 && c >= L
update:
pc := pc_2;
}
transition ( exists x:int ) {
guard: pc = pc_1 && x = c && a[x] = n
update:
pc := pc_2;
}
SAFARI will display the following output:
# This is SAFARI (www.verify.inf.usi.ch/safari) # Compiled with gcc 4.7.0 on Jun 17 2012 # Using an external SMT-Solver as the main SMT-Solver ================================================================== Trying to execute an external solver with these parameters: Solver path: /Users/francesco/usi/oprover/smt_solvers/z3 Solver options: -smt2 -in -nw ================================================================== ================================================================== SMT-solver is running as a child process with pid 28339 ================================================================== Assigned 'pc_1' --> 1 Assigned 'pc_2' --> 2 - Solver initialization... done. - Adding a node-container to the mc... done. - Setting user defined domains (1) in the mc... done. - Setting variables (5) in the mc... done. - Adding system axioms (1) to the mc... done. - Adding transitions (3) to the mc... done. - Setting initial configuration in the mc... done. - Adding program settings to the mc... done. - Setting the unsafe configurations (1) in the mc... done. Unwinding the transition system... node 1 = [t1][0] node 2 = [t2_z0][0] node 3 = [t2_z1][0] node 3 is covered node 4 = [t0_z0][t1][0] Checking counterexample... counterexample is infeasible. Refining abstraction... node 1 has been refined node 4 is deleted (empty label) node 5 = [t0_z1][t1][0] node 5 is covered node 6 = [t1][t1][0] node 6 is covered node 7 = [t2_z0][t1][0] node 8 = [t2_z1][t1][0] node 8 is covered # Result.........................: safe # Max.depth.reached..............: 2 # Nodes..........................: 9 # Covered.nodes..................: 4 # SMT-solver.calls...............: 89 # Index.variables................: 2 # CEGAR.iterations...............: 1 # WARNING: the following data refer *only* to SAFARI internals! # CPU.Time.used..................: 0.010214 s # Memory.used....................: 1.656 MB
Solvers
Enabling the (main) solver
The current version of SAFARI needs an external SMT-Solver. The communication interface relies on the SMT-LIB v.2 format. In order to use the external solver, you need to create a config file with these two lines:
SMT_solver_path "/Users/francesco/usi/oprover/smt_solvers/z3"
SMT_solver_options "-smt2 -in -nw"
where SMT_solver_path is the path of the binary of the solver, and SMT_solver_options are the options required to read from stdin SMT-LIB v.2 formulae. The two lines above are used to exploit z3 as the main SMT-Solver.
Enabling the (interpolating) solver
SAFARI integrates an interpolating procedure, which is used by default with options -r2. If you wish to combine SAFARI with another interpolating solver, you need to enable the option -r with parameter 1, and add to the config file the two lines:
Interpolating_solver_path "/Users/francesco/usi/opensmt/opensmt_interp"
Interpolating_solver_options "--config=opensmt.conf"
The first option tells SAFARI where is the binary of the interpolating prover, the second option tells SAFARI which options are required to execute it. The current version of SAFARI does not support external interpolating provers and term abstraction together. SAFARI generates a file called ''ceLog.smt2", which contains the partitions of the trace. SAFARI reads the interpolants from another file after the interpolating prover exists. This file must be called 'SAFARI_interpolants.smt2', and must be located in the folder where the SAFARI binary is. All the interpolants need to be written according to the SMT-LIB2 syntax, one for each line, starting from 'false' and ending with 'true'.
