[e-lang] Joe-E Doc
daw at cs.berkeley.edu
Tue Mar 11 20:27:09 EDT 2008
Tyler Close writes:
>Does the complete supression of java.lang.StringBuffer indicate a bug
>in the Joe-E verifier, since it is used in the expansion of the string
Good spot! This is an not-pretty corner of Joe-E that I wish we
could sweep under the covers (but of course we cannot).
It seems to me it's either a bug in the taming database or in the Joe-E
verifier, and we could debate about where to assign the blame. In this
particular case, I think it's reasonable to call it a bug in the taming
database, though one could classify it either way.
There are, sadly, more than a few cases where the Java compiler will
introduce implicit method calls that aren't explicit in the source code.
This is inconvenient for Joe-E. For each such case, we must adopt at
least one of the following two strategies:
(a) The Joe-E verifier must be aware of every syntactic construct
that could trigger such an implicit call, and consult the taming
database at every such syntactic construct.
(b) If the Joe-E taming database allows every such method call that
might be implicitly introduced, then it's not strictly necessary
for the Joe-E verifier to do anything special.
In some cases strategy (b) is easier to implement, but it creates a subtle
dependency between the verifier and taming database, which is not ideal.
Strategy (a) is more robust. If we think there's a chance that someday
we might want to suppress those methods in our taming database, strategy
(a) is the clear winner.
For StringBuilder/StringBuffer, it seems reasonable to me to adopt
the invariant that the taming database will allow all of those methods
that might be implicitly introduced by the Java compiler. If the taming
database does allow all of those methods, then the Joe-E verifier doesn't
need to predict every implicit call to StringBuffer/StringBuilder that
might be inserted into the .class file. I think that's the current
strategy for StringBuffer/StringBuilder.
There are many other cases like this: auto-boxing/unboxing (implicit calls
to, e.g., methods of Integer to box/unbox ints); for-each loops (implicit
calls to Iterable.iterator(), Iterator.hasNext(), Iterator.next());
and probably several others that I've forgotten. Sadly, I haven't been
able to find any comprehensive list in one place of all of the method
calls or field accesses that the Java compiler might implicitly access,
so Adrian had to construct this list ourselves by hand. He came up with
quite a few. Someday we should probably do the exercise of writing down
that list (as best as we've been able) in one place, so others can review
it and see if we missed anything.
Our approach is dangerous: if we overlook a single case where the Java
compiler implicitly introduces method calls or field accesses, Joe-E code
may be able to bypass the taming checks. We're essentially blacklisting,
and that's always risky.
I'm not especially happy with the situation, but I don't see any better
approach. I don't know of any completely satisfactory solution. Sigh.
I guess one advantage of making the Joe-E Doc output public is that
it forces us to own up to how poor the current version of the taming
More information about the e-lang