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

[Jean-Christophe Filliatre]

Hi,

I don't know if  this can be of any help for you,  but we also wrote a
tool recently to convert the Boogie benchmarks to the native syntax of
other  provers,  including   SMTlib.   More  precisely,  we  translate
Simplify's  syntax  to the  input  syntax of  the  Why  tool (our  own
intermediate language,  see http://why.lri.fr/) and then  the Why tool
can translate it to various provers.

But  our  translation  is  a  trivial  one,  which  does  not  try  to
(re)discover  any sort.  All Simplify  terms are  mapped  to integers.
Thus we simply figure out  the arities of functions and predicates.  I
attach an example of SMTlib file obtained from the Boogie benchmark.

If you are interested by this  tool, you can download Why 2.01 sources
(at http://why.lri.fr/).

You'll have to type "make bin/simplify2why.opt" to get the Simplify to
Why translator.   And you'll get  the Why to SMTlib  translation using
"why --smtlib". 

Hope this helps,
-- 
Jean-Christophe

-------------- next part --------------
A non-text attachment was scrubbed...
Name: boogie_Chunker.simplify_why.smt
Type: application/octet-stream
Size: 121662 bytes
Desc: not available
Url : /pipermail/smt-lib/attachments/20070112/ba60961f/boogie_Chunker.simplify_why-0001.obj
-------------- next part --------------


Michal Moskal writes:
 > 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?
 > 
 > _______________________________________________
 > SMT-LIB mailing list
 > SMT-LIB at cs.nyu.edu
 > http://www.cs.nyu.edu/mailman/listinfo/smt-lib