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

[Jim Saxe]

Michal Moskal wrote:

 >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.
 >...
 >I assumed the select/store functions to operate on the Object sort,

This assumption is incorrect.

 >... 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. ...

In the Simplify encoding used by ESC/Java, the select and store
operators operate on fields.  The value of "some_a.x" at a particular
point in the execution of the target program is modeled by a Simplify
expression like

    (select x some_a)       // Note: NOT "(select some_a x)"

where, intuitively "x" denotes a map from instances of "A" to integers
and "some_a" denotes an instance of "A".  Typically the names "x" and
"some_a" would actually occur in inflected forms (e.g., "|x:1.27.13|").
The inflections serve to distinguish different fields (or local variables,
types, etc) of the same name declared in different places, and also to
distinguish values of the same field (or variable, etc.) at different
points in a program execution.

To see why we use fields rather than objects as the first argument to
"select", consider the following code fragment:

    A some_a;
    A that_a;
    ...
    some_a = ...                           // line 22
    that_a = some_a;                       // line 23
    some_a.x = 1;                          // line 24
    that_a.x = 2;                          // line 25
    //@ assert some_a.x == 2               // line 26

and suppose (somewhat simplifying the rules by which ESC/Java actually
generates verification conditions in general and inflected names in
particular) that we use a name of the form v:n to denote the value of
variable or field "v" just after execution of line n.  Then from line
23, we get

   (EQ that_a:23 some_a:22)

and from line 25 we get

   (EQ x:25 (store x:24 that_a:23 2))

which together (along with the axioms for select and store) suffice
to imply the claim on line 26

   (EQ (select x:25 some_a:22) 2)

If we modeled field selection with the objects as maps (arrays) and
the field names as indices, we would not be able to tell that the
assignment to that_a.x on line 25 affects the value of some_a.x on
line 26.

There are many more details to how ESC/Java generates verification
conditions than I can go into here (or remember!), but to get some
idea of how it models assumptions about type-correctness (given
Simplify's lack of typing), you might look at how the functions "is"
and "asField" are used in the Simplify input (.sx) files it produces.

Regards,
--Jim Saxe