Comparison with previous work

Comparison with previous work

Here we will compare our interprocedural method with the one designed by [RS01], see also the corresponding experiments.

What we compare

We will use exactly the same general files as in the first section. We compared the analysis on the 3 following procedures: reversal of a list, (reverse as in the first section), non-deterministic insertion of a cell in a single linked list (insert), non-deterministic deletion of a cell in a single linked list (delete).

We used different versions of the insert and delete procedures defined in [RS01], the difference being that we pass as an input (resp. output) parameter the cell to be inserted (resp. deleted), for precise reasons we develop in the sequel. Thus we obtain much more precise information, as we identify in the resulting list which cell has been inserted (resp. deleted). Unfortunately, but not surprinsingly, the analysis time are much higher.

We also experimented [RS01] method on versions nearer of ours, where the inserted (resp. deleted) cell is pointed to by a global variable cell.

In all cases, we obtain an information of different nature, but which contains the information computed in [RS01]:

Typically, we are able to prove that reversing twice a list gives the same list, whereas [RS01] could only shows that it gives a list with the same head.

We analyze the following programs:

type cell = record
  n: ^cell;
  k: int; (* Abstracted *)
end record
type list = ^cell;

procedure main(list : list; cell : list) is
var res : list;
main_entry: res := insert(list, cell);

(* c is supposed to be a list with one element 
   (eg, with c->n := NULL) *)
function insert(h : list; c : list) : t is
insert_entry: if (h!=NULL && ? (*h->k<c->k*)) then begin
insert1:         t := h->n;
insert2:         t := insert(t,c);
insert3:         h->n := NULL;
insert4:         h->n := t;
insert5:         t := h
              end else begin
insert7:         c->n := h;
insert8:         t := c;

procedure main(list : list) is
var res,cell : list;
main_entry: (res,cell) := delete(list, (*k*));

(* c is the deleted cell *)
function delete(h : list; (*k:int*)) : (t,c) is
delete_entry: if (h==NULL) then begin
delete1:         t := h
delete2:         c := NULL;
              end else begin
delete4:         t := h->n;
delete5:         if (? (*h->k==k*)) then begin
delete6:            h->n := NULL;
delete7:            c := h;
                 end else begin
delete9:            (t,c) := delete(t);
delete10:           h->n := NULL;
delete11:           h->n := t;
delete12:           t := h;

Results and comparison

Results are given in the following table.

In the "Number of Structures" field, we indicate the number of reachable structures at the following control points:

Concerning analysis times,

Input Program Nb of predicates (abs/total) and constraints Iterations Nb of Structures File Time Modified [RS01] Time [RS01] Time reverse.tvp 40/56 & 392 10 3, 4, 8, 7, 3 11s 37s 37s insert.tvp 66/112 & 708 11 6, 8, 35, 23, 9 188s 76s 22s delete.tvp 70/122 & 776 11 6, 8, 47, 32, 13 222s 51s 25s

With respect to analysis time, our method performs better than [RS01] for the list reversal, but worse for the other examples. However, remember that the information computed is not the same, as explained in the previous section. The quite important number of structures in the two last examples comes from the fact that we introduce two additional abstraction instrumentation predicates allowing the invariant to be properly maintained, and that many different cases are distinguished. In the case of insertion, at node main_end the cell may have been inserted at the beginning, at the 2th place, ..., and orthogonnally can be followed by 0, 1, 2 or more than 2 cells: this gives 9 structures.

The greater number of structures for delete compared to insert is due to the fact that delete may not delete any cell which adds additional cases.

Coming back the comparison between our method and [RS01] applied on modified version of their programs, we give some reasons for the greater analysis time of our method:

More detailed description

We already describe the list reversal example here, so we focus on insert and delete.

We mentioned that for list insertion we needed a different version than the one used by [RS01], see also the WEB page. In their version, there is only one parameter to insert, and the inserted node is dynamically allocated by a special mechanism allowing to add a new individual to a logical structures. However this cannot be performed in our case, as we model an input/output relation between memory configurations. Thus we add two choices:

  1. Model the free heap by a linked list of free memory cells, pointed by a variable heap, and taking the inserted cell in this list;
  2. Or passing the cell to be inserted as a parameter.

We choosed solution 2. Solution 1 implies that we pass forth and back to insert the variable heap, as we cannot model directly global variables. This would give an insert procedure with 2 input and 2 output parameters.

As the effect of insert and delete is local, a specific cross-instrumentation predicate modelling it is not necessary. However we should allow the analysis to discover the two patterns:

Insertion of a cell in a list
Deletion of a cell in a list

For this purpose, we introduced the following instrumentation predicates, to identify direct successor and predecessor of a cell pointed by a variable via a field f:

%r succ[f,m,z](v) = E(v_1) z(v_1) & f[m](v_1,v) unique abs
%r pred[f,m,z](v) = E(v_1) z(v_1) & f[m](v,v_1) abs

Comparison with previous work