What InterprocStack does for youContents

What InterprocStack does for you

InterprocStack 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 InterprocStack 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 InterprocStack, 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:

InterprocStack 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:

InterprocStack returns an overapproximation of p(Coreach).

Combined forward/backward analyses

InterprocStack allows to combine forward and backward analysis any number of time.

If X denotes the invariant computed by InterprocStack at the previous step, at the current step:

For instance, after executing the command 

  interprocstack -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 InterprocStack does for youContents