[SMT-LIB] logic for ESC/Java and Boogie benchmarks

[Michal Moskal]

Hi,

for the past couple of days I've been trying to implement a converter
taking formulas in Simplify format and generating ones in SMT-LIB
format.

As you probably know the main problem here is that Simplify's input
language is unsorted. This is why the translation of the ESC/Java
examples in AUFLIA/Simplify uses an encoding where everything is
treated as an integer. In particular it defines its own versions of
select/store axioms.

While I still haven't got the original Simplify files that were used
to generate those (maybe somebody has them around?), I have some other
ESC/Java benchmarks generated by running it on parts of its own source
code. I also used Boogie benchmarks available on the Spec# web page.

My converter takes sort specifications for any number of function and
constant symbols, a special set of "casting" functions and a Simplify
input file and then tries to infer the types of other symbols. I used
four sorts: Int, Object, Array and Heap.

Array and Heap are a bit different. ESC/Java uses single-dimensional
arrays, treating each object as a separate array. This is the Array
sort. Now Boogie uses a different approach, where all the arrays are
two-dimensional and represent heaps, where h[o,f] means to dereference
field f of an object o in the heap h.

I assumed the select/store functions to operate on the Object sort,
and used casting in case of problems. This is the main (and almost
only in case of Boogie) reason we need the cast functions and I think
the only way to fix it is to use dependant polymorphic types, because
the arrays used are not homogeneous. For example if you have a class
like:

class A {
  int x;
  A other_a;
}

Then definitely (select some_a x) and (select some_a other_a) are
going to have different types. This is even more true in Boogie
encoding (where the entire heap is a single array).

On the other hand casting functions are easily axiomatized and can be
just dropped by type-less provers.

The following "casting" functions seem to be required:

   (int_to_object Int Object)
   (object_to_int Object Int)

and for ESC/Java (not needed in Boogie), additionally:

   (array_to_object Array Object)
   (object_to_array Object Array)

The axioms I used for them are:

  (forall (?o Object)
    (= ?o (int_to_object (object_to_int ?o))))

  (forall (?i Int)
    (= ?i (object_to_int (int_to_object ?i))))

  (forall (?o Object)
    (= ?o (array_to_object (object_to_array ?o))))

  (forall (?i Array)
    (= ?i (object_to_array (array_to_object ?i))))

I think this should be enough.

It would be probably possible to get away from cast functions in
Boogie by assuming Object=Int, but I don't really think this would be
a faithful translation.

I've also defined single and two-dimensional arrays:

   (select2 Heap Object Object Object)
   (store2  Heap Object Object Object Heap)

   (select Array Object Object)
   (store  Array Object Object Array)

with the usual axioms (without extensionality, which is not needed
here). Again it would be probably possible to get away with only
single, or two-dimensional arrays, but again it wouldn't be very
faithful.

Additionally, I've added a partial order called 'subtypes' ( '<:' in
both ESC/Java and Boogie, but this is illegal name in SMT format).

I've also translated the (PATS ...) hints, using annotations:

  (PATS t1 (MPAT t2 t3) t4) => :pat { t1 } :pat { t2 t3 } :pat { t4 }
  (NOPATS t1 t2) => :nopat { t1 } :nopat { t2 }

The theory and logic files are here:

  http://nemerle.org/svn.fx7/trunk/smt/AUFLIA2.smt
  http://nemerle.org/svn.fx7/trunk/smt/Int_Heaps.smt

(yes, I know, I could have come out with better names).

This file defines the initial sort annotations:

  http://nemerle.org/svn.fx7/trunk/smt/functions.ax

The converter itself is embedded in the Fx7 theorem prover available
at the SVN server at:

  http://nemerle.org/svn.fx7/trunk/

(it requires a recent mono and a SVN version of Nemerle compiler; if
somebody needs more info, please drop me a line).

To see the initial results, you can have a look at the SX and SMT
files in the tarballs at:

  http://nemerle.org/~malekith/smt/benchmarks/

All the benchmarks pass the verification with the smtlib parser and
seem to give the right answers in Fx7. The "unsat"/"sat" status is
based on Simplify's responses (which means you cannot trust "sat").

I'll continue to work on this (like throw away sill or similar
examples and so on), but need some feedback -- what do you think about
the cast functions and the entire idea of separate logic for such
verification systems?

Cheers!
   Michał