What Interproc does for you Contents

# What Interproc does for you

Interproc takes as input a "Simple" program, annotates it with control points, perform forward and/or backward analysis, and print the annotated programs with invariants associated with each control point, like this:

```
Annotated program after forward analysis:
var x : int, y : int, z : int
begin
/* (L5 C5) top */
assume z >= 10 and z <= 20; /* (L6 C25) [|-z+20>=0; z-10>=0|] */
x = 0; /* (L7 C8) [|x=0; -z+20>=0; z-10>=0|] */
y = 0; /* (L7 C13) [|-3x+y=0; -x+z+1>=0; -z+20>=0; z-10>=0; x>=0|] */
while x <= z do
/* (L8 C17) [|-3x+y=0; -x+z>=0; -z+20>=0; z-10>=0; x>=0|] */
x = x + 1; /* (L9 C12)
[|-3x+y+3=0; -x+z+1>=0; -z+20>=0; z-10>=0; x-1>=0|] */
y = y + 3; /* (L10 C12) [|-3x+y=0; -x+z+1>=0; -z+20>=0; z-10>=0; x-1>=0|] */
done; /* (L11 C7) [|-3x+y=0; -x+z+1=0; -x+21>=0; x-11>=0|] */
if y >= 42 then
/* (L12 C15) [|-3x+y=0; -x+z+1=0; -x+21>=0; x-14>=0|] */
fail; /* (L13 C9) bottom */
endif; /* (L14 C8) [|-3x+y=0; -x+z+1=0; -3x+41>=0; x-11>=0|] */
end
```

### Invariants

An invariant I is a set of environments:

The result of the analyses performed by Interproc is the projection p(X) of sets of stacks on their top elements. The result of this projection is a function that maps control point to invariants:

Intuitively, the invariant on numerical variables associated with each program point, as returned by Interproc, indicates the possible values for these variables at each program point, for any stack tail.

### Single forward/reachability analysis

A forward analysis compute the set of reachable states of the program, which is defined as:

Interproc returns an overapproximation of p(Reach).

### Single backward/coreachability analysis

A backward analysis computes the set of states from which one can reach a fail instruction. The set of states coreachable from a fail instruction is defined as:

Interproc returns an overapproximation of p(Coreach).

### Combined forward/backward analyses

Interproc allows to combine forward and backward analysis any number of time. If X denotes the invariant computed by Interproc at the previous step, at the current step:

• a forward analysis will consider the set of initial states

• a backward analysis will consider the set of final states

For instance, after executing the command

```  interproc -analysis fb essai.spl
```

on the previous program, we get

```
Annotated program after forward analysis
var x : int, y : int, z : int
begin
/* (L5 C5) top */
assume z >= 10 and z <= 20; /* (L6 C25) [|-z+20>=0; z-10>=0|] */
x = 0; /* (L7 C8) [|x=0; -z+20>=0; z-10>=0|] */
y = 0; /* (L7 C13) [|-3x+y=0; -x+z+1>=0; -z+20>=0; z-10>=0; x>=0|] */
while x <= z do
/* (L8 C17) [|-3x+y=0; -x+z>=0; -z+20>=0; z-10>=0; x>=0|] */
x = x + 1; /* (L9 C12)
[|-3x+y+3=0; -x+z+1>=0; -z+20>=0; z-10>=0; x-1>=0|] */
y = y + 3; /* (L10 C12) [|-3x+y=0; -x+z+1>=0; -z+20>=0; z-10>=0; x-1>=0|] */
done; /* (L11 C7) [|-3x+y=0; -x+z+1=0; -x+21>=0; x-11>=0|] */
if y >= 42 then
/* (L12 C15) [|-3x+y=0; -x+z+1=0; -x+21>=0; x-14>=0|] */
fail; /* (L13 C9) bottom */
endif; /* (L14 C8) [|-3x+y=0; -x+z+1=0; -3x+41>=0; x-11>=0|] */
end

Annotated program after backward analysis
var x : int, y : int, z : int
begin
/* (L5 C5) [|-z+20>=0; z-13>=0|] */
assume z >= 10 and z <= 20; /* (L6 C25) [|-z+20>=0; z-13>=0|] */
x = 0; /* (L7 C8) [|x=0; -z+20>=0; z-13>=0|] */
y = 0; /* (L7 C13) [|-3x+y=0; -x+z+1>=0; -z+20>=0; z-13>=0; x>=0|] */
while x <= z do
/* (L8 C17) [|-3x+y=0; -x+z>=0; -z+20>=0; z-13>=0; x>=0|] */
x = x + 1; /* (L9 C12)
[|-3x+y+3=0; -x+z+1>=0; -z+20>=0; z-13>=0; x-1>=0|] */
y = y + 3; /* (L10 C12) [|-3x+y=0; -x+z+1>=0; -z+20>=0; z-13>=0; x-1>=0|] */
done; /* (L11 C7) [|-3x+y=0; -x+z+1=0; -x+21>=0; x-14>=0|] */
if y >= 42 then
/* (L12 C15) [|-3x+y=0; -x+z+1=0; -x+21>=0; x-14>=0|] */
fail; /* (L13 C9) bottom */
endif; /* (L14 C8) bottom */
end
```

 What Interproc does for you Contents