Fixpoint Calculator

This program is able to infer fixpoints for given disjunctive formulae (postconditions). It makes use of a novel concept called planar affinity, a technique for measuring how related (or similar) are two given formulae. Affinity is used in both hulling and widening operations throughout the fixed point algorithm.

The fixed point algorithm follows from the seminal work of Cousot and Halbwachs for the (conjunctive) polyhedron abstract domain [Cousot:POPL78]. More recent work on disjunctive abstract domains include [Bagnara:VMCAI04, Sankaranarayana:SAS06]. The algorithm implemented in the Fixpoint Calculator is described in more details in the paper ASIAN06.

Fixpoint analysis - Often in program analysis writing formulae that can express relations between inputs and outputs (of a given block or method) necessitates this type of analysis. The blocks requiring fixpoint analysis are the ones containing a recursive construct of some kind. Through successive iterations, the starting formula is modified until its form remains the same for two consecutive computations. Hulling and widening are applied in computing next iterations, at times.

Disjunctive normal form - a standardization (or normalization) of a logical formula which is a disjunction of conjunctive clauses.

Hulling - an aproximation technique that combines related disjunctive formulae into a conjunct. For the Fixpoint Calculator a new selective hull operation is introduced, parameterized with m, maximum number of disjuncts that the resulting formula should have.

Widening - another aproximation operation that drops some conjunctive sub-formulae. The conjunct that is removed is usually one that changes between fixpoint analysis iterations. A pairwise widening technique is used for the Calculator, where only the most related pairs will distribute the widening operator (when applied for two disjunctive formulae).

Omega Calculator - The Fixpoint Calculator is incorporationg this software. It needs to have been installed for running Fixpoint Calculator.

Fixpoint Calculator - Binary compiled under Fedora Core release 4.

Syntax and semantics of input files for our calculator are close to that of Omega Calculator, for ease of understanding.

An example input file (runs with ./fixcalc <filename>.fc) is presented below :

-------------------------------------------------------------------

sumvec:={[s,i,j] -> [] -> [i,j]: exists (PRMi,PRMj: exists (i_1: (i>j ||
           (i<=j && 0<=i<s && i_1=i+1 && sumvec(s,i_1,j)))))};
sumvec;
sumvec0:={[]: 0=1};
sumvec1:=sumvec(sumvec0);
sumvec2:=sumvec(sumvec1);
sumvec3:=sumvec(sumvec2); 
sumvec3h:=selhull(sumvec3,3,SimHeur);
sumvec4:=sumvec(sumvec3h);
sumvec4h:=selhull(sumvec4,3,SimHeur);
sumvec3w:=widen(sumvec3h,sumvec4h,SimHeur);
#sumvec4:=sumvec(sumvec3); 
Fix:=bottomup(sumvec,3,SimHeur);

sumvec0;sumvec1;sumvec2;sumvec3;sumvec4;Fix;sumvec3w;

-------------------------------------------------------------------

- We're calculating a postcondition for the following function:
Float sum (Float[Int] a, Int i, Int j) {
  Float t := 0.0;
  if (i>j) then { 0.0 }
  else { t := a[i] + sum(a,i+1,j); t }
}

- The first line defines the recursive formula for the function's constraint abstraction. These have to be provided by the user. The variables PRMi and PRMj represent the (primed) i' and j', denoting values for these parameters after the function executes (once). However, they aren't used in this particular formula. In general the recursive formula requires three sets of arguments sumvec:={[inputs] -> [outputs] -> [inputs-by-val]: ... }. The first set contains the inputs of the function [s,i,j], the second set contains the outputs of the function (empty for this example). The last set contains those inputs that are passed-by-value and excludes the variables that represent lengths of some array.

- The sumvec; command simply requests the printing of the sumvec formula (function) on the screen. The whole fixpoint iterative process is done using bottomup(sumvec,3,SimHeur); and stored in Fix. We also illustrate some of the fixpoint technique steps with intermediary commands, storing this alternative final result in sumvec3w. Fix and sumvec3w will contain the same formula for the computed postcondition.

- We start with sumvec0 as false, then do three iterations (sumvec1:=sumvec(sumvec0); ...). We do a selective hull on the third and fourth result, then a widening with these two hulls, obtaining sumvec3w.
The last line of the input file prints all final and intermediary formulae.

selhull(f, m, t) - computes a selective hull on formula f, using technique t. Parameter m denotes the maximum number of disjuncts that the resulting formula should have.
We use SimHeur (Planar Affinity) as technique t. HausHeur (Hausdorff Distance) can also be used. Details about these can be found in the papers in next section.

widen(f1, f2, t) - performs a pairwise widening on the input f1 and f2 formulae, using technique t and preserving their (common) number of disjuncts in the result formula.

bottomup(f, m, t) - given the recursive formula f, it computes a postcondition using fixpoint analysis with intermediary formulae having at most m number of disjuncts, using the specified technique t for hulling.

topdown(f, m, t) - given the recursive formula f, it computes a transitive invariant using fixpoint analysis with at most m number of disjuncts and the specified technique t for hulling.

disjunctive.asian06.pdf
Inferring Disjunctive Postconditions
Corneliu Popeea and Wei-Ngan Chin.
ASIAN 2006: 11th Asian Computing Science Conference 2006.

array.pepm08.pdf
A Practical and Precise Inference and Specializer for Array Bound Checks Elimination
Corneliu Popeea, Dana N. Xu, Wei-Ngan Chin.
PEPM 2008: ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation 2008.

dual.pdf
Dual Analysis for Proving Safety and Finding Bugs
Corneliu Popeea and Wei-Ngan Chin.
Technical report - November 2007.

thesis.pdf
Disjunctive Invariants for Modular Static Analysis
Corneliu Popeea
PhD. Thesis - July 2008.

Contributors to this Calculator and its techniques are:

Corneliu Popeea
Wei-Ngan Chin