[e-lang] JSONSerializer review, further study of reviewable coding techniques

Tyler Close tyler.close at gmail.com
Tue Aug 19 13:50:38 CDT 2008


On Mon, Aug 18, 2008 at 2:41 PM, Tyler Close <tyler.close at gmail.com> wrote:
> Let's assume the existence of a variable annotation: "@inert". For
> variables with this annotation, the Joe-E verifier checks that:
> 1. On access to a field of the referent, the field MUST be final and
> the accessed value MUST be assigned to another variable that either:
>    a. has the @inert annotation,
>    b. or is of type Immutable.
> 2. On invocation of a method of the referent, the referent MUST be Immutable.

...

> If a caller provides an @inert argument to a constructor or method,
> the returned object MUST be assigned to either an @inert variable, an
> Immutable variable, or be the caller's return value. A constructor can
> initialize a field using an @inert argument.

I think the above constraints are good enough for enforcing the
JSONSerializer claims, but I think it needs to be more restrictive for
enforcing some of the claims in the ref_send library, so I suggest:

Let's assume the existence of a variable annotation: "@inert". For
variables with this annotation, the Joe-E verifier checks that:
1. On access to a field of the referent, the field MUST be final and
the accessed value MUST be assigned to another variable that either:
   a. is the caller's return value
   b. has the @inert annotation,
   c. or is a scalar type,
   d. or is java.lang.String,
   e. or is java.math.BigInteger,
   f. or is java.math.BigDecimal
2. Invocation of a method of the referent is forbidden.
3. If a caller provides an @inert argument to a constructor or method,
the return value MUST be assigned to a variable meeting the same
conditions listed in case 1.
4. A constructor can initialize a field using an @inert argument, but
MUST NOT access that field.

The tightening of constraint #1 ensures that an @inert argument cannot
be given access to a mutable object via a method invocation. For
example, this will be a useful check in the implementation of
org.ref_send.promise.eventual.Eventual, which has mutable state, but
must treat certain arguments as @inert.

> This meets our stated goal for the reviewer, but we don't yet have the
> implementation flexibility we need. The Exporter's job is to hold onto
> a map of [ exported URL string => value ]. The values in this map may
> at some later time be subjected to mutations, and so cannot be @inert.
> Since the caller of JSONSerializer.write() possesses non- at inert access
> to the values argument, it should be able to get non- at inert access to
> anything passed to the Exporter. Let's say the caller looks like:
>
> final ConstArray<?> values = ...
> final String text = JSONSerializer.write(new Exporter() {
>    public String
>    run(final Object value) {
>         ...
>    }
> }, values);

The escape analysis on the anonymous Exporter instance is trickier
than it at first appears.

Say the body of Exporter.run() is as in:

final Exporter[] evil = { null };
final Map<?> exported = ...
final ConstArray<?> values = ...
final String text = JSONSerializer.write(new Exporter() {
   public String
   run(final Object value) {
        if (value == this) {
            evil[0] = value;
        } else if (value instanceof Victim) {
             ((Victim)value).kill();
        }
        final String r = generateURL();
        exported.add(r, value);
        return r;
   }
}, values);
return evil[0];

The caller of the above code can then do:
final @inert Victim victim = ...
final Exporter evil = callAboveCode();
evil.run(victim);

In summary, the JSONSerializer.write() implementation could pass a
reference to the anonymous Exporter as the value parameter in a call
to Exporter.run(). The Exporter.run() implementation stashes away this
reference in a place where it can be used by code that does have in
scope @inert variables. Nuts.

Given that the Exporter needs to be able to save the value argument
for later use, it seems really hard to code the implementation such
that we know the Exporter doesn't survive the call to
JSONSerializer.write(). So far, the best I've got is:

final Map<?> exported = ...
final ConstArray<?> values = ...
final Milestone done = new Milestone();
final Exporter export = new Exporter() {
   public String
   run(final Object value) {
        if (done.is()) { throw new AssertionError(); }

        if (value == this) {
            evil[0] = value;
        } else if (value instanceof Victim) {
             ((Victim)value).kill();
        }
        final String r = generateURL();
        exported.add(r, value);
        return r;
   }
};
final String text = JSONSerializer.write(export, values);
done.mark();

That's pretty awkward to write and verify. Can anyone do any better?

--Tyler


More information about the e-lang mailing list