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