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

[Michal Moskal]

On 1/10/07, Jim Saxe <jim.saxe at hp.com> wrote:
> 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.

I guess the name Object is not the most fortunate one. I was rather
thinking of something like "symbolic object", or maybe something that
is neither integer nor an array.

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

Ha! That makes perfect sense. I should have noticed it myself, it
seems I'm just being flawed by OO thinking, while here we're is the
true, functional, pure world, where a field a just a map from objects
to values instead of some attribute.

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

OK, that makes perfect sense.

You needed some representation of the heap, where particular objects
are not structural, but just point to it, therefore you decided to
have a "separate heap" for each field (which makes sense, assuming
Java type safety, where you cannot mix up memory used by different
fields).


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

Thanks, I definitely will.

Also thanks for the design notes link!

-- 
   Michał