[e-lang] Defensive consistency and integer overflow

[Mark Miller]

On 9/23/07, David Wagner <daw at cs.berkeley.edu> wrote:
> Yes, that's basically what I had in mind, possibly along with some
> promotion rules so that (for instance) adding an "int" and a "BigInteger"
> gives you a "BigInteger".
>
> The unwieldiness I had in mind is the issues associated with
> source-code transformation and its effect on existing Java tools
> (IDEs, debuggers, build tools, etc.).  I presume .java files would be
> generated automatically from .joee files,

Oh heavens no! I wasn't for a moment suggesting that Joe-E do this
transform. That would lose us Joe-E's main advantage -- that it's 100%
compatible with the legacy Java tool chains. Rather, I was suggesting
that this be incorporated into a future version of Java. Were this to
happen (which I admit is unlikely), then Joe-E would then allow it as
well.


> and the programmer would only
> be expected to look at the contents of the .joee files.  What changes
> to Eclipse/IntelliJ/etc.  would we have to make to support this kind of
> programming?  What would be the impact on debugging if line numbers (e.g.,
> in stacktraces) refer to .java files rather than the .joee files that
> the developer writes?  How easy would it be to write a source-to-source
> transformer that stays up to date with new versions of the Java language?
> All of this seems like mundane engineering stuff, so perhaps it is not
> worth mentioning, but I don't know whether the annoyance of this would
> outweight the security benefits of easy-to-use BigIntegers.

Yes, I believe they would outweigh security to the point of preventing
Joe-E from being adopted. Let's continue to avoid *any*
transformation.


> Yup, the attractiveness of C# as a basis for an objcap language hasn't
> escaped my notice.

The name "Irony" would seem appropriate in several ways ;).


> P.S. In Java, with or without extensions to reduce the notational overhead
> of using big integers, there's a minor bit of ugliness: BigInteger is
> not a final class.  This means that code that receives a BigInteger "a"
> cannot rely upon the expression "a + b" to actually perform addition,
> unless the code somehow has knowledge of the exact runtime type of "a".

I hadn't realized that. Bletch.


> At a recent meeting with Adrian and Ping, they raised the suggestion
> that perhaps we should introduce a notion of 'honorarily final' into
> Joe-E.  The idea: add a marker interface, with some name like Library or
> Standard or Final or Semifinal.  Some library classes like BigInteger
> could be marked honorarily Library.  The Joe-E verifier would prevent
> Joe-E classes from subclassing any Library class.  Other Java library
> classes might still be allowed to subclass a Library class, but because
> we know that Joe-E code cannot do so, we can rely upon the behavior of
> objects of that type.

I like it. I will point out that it's an incremental step towards the
kind of open auditing framework I've proposed, where a class could
implement/extend BigInteger iff it could satisfy a BigIntegerAuditor
that it obeyed the BigInteger contract. Here, the BigIntegerAuditor in
effect adopts the auditing rule: if it's in the TCB and it says it
obeys the BigInteger contract, then I believe it.


> The advantage of this idea is that it would allow Joe-E code to use
> the static type system to establish trust in the behavior of objects
> it receives.  The disadvantage is that we would have to make a decision,
> for once and for all, about which classes are marked Library.  If some
> Joe-E apps would like to be able to subclass BigInteger and others would
> like to be able to rely upon the impossibility of subclassing BigInteger,
> this approach becomes problematic.

I agree. And I think most legacy Java classes should be marked
Library, but very few legacy Java interfaces should be. A data point
on how surprisingly non-disruptive this will be in practice: E objects
can implement most Java interfaces. But E object cannot extend Java
classes. I know of only two cases where this became painful enough to
add a workaround to E's Java libraries. Perhaps legacy Java classes
should be Library by default, and would need to be explicitly marked
somehow in order to be non-Library?

As a good start on which Java interfaces should be marked Library, it
might be good to see E's list of Java interfaces that cannot be
implemented by E objects. I'm not sure that this list includes any
legacy Java interfaces. As best I can recall, it includes only
interfaces defined by E's Java libraries.


> Ping also raised the suggestion of a programming discipline where any
> time a method accepts a parameter of non-final type, the programmer should
> annotate it (e.g., @nonfinal) to help indicate that the behavior of that
> parameter cannot be relied upon.  Then one could build a lint-like type
> that warns about any method parameters whose type is non-final and that
> doesn't have a @nonfinal annotation.  This would not make sense for
> inclusion in the Joe-E verifier but might be an interesting idea for
> a caplint.

1) Please don't make a special case for parameters. Whatever rule we
adopt there should also apply to all other variable declarations as
well as method return types.

2) An interface or abstract class is necessarily non-final, so no
annotation should be needed for them. At Agorics, many of us learned
not to create non-abstract non-final classes. So long as these are
avoided, the ambiguity solved by this annotation doesn't arise.
Perhaps it would be better for caplint to warn instead on a
non-abstract non-final class definition?

But this still leaves the problem of legacy Java libraries that don't
follow the Agorics style. For these, @nonfinal isn't the right hammer.
The previous suggestion of an honorary Library marker is.

-- 
Text by me above is hereby placed in the public domain

    Cheers,
    --MarkM