Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Java: Unboxed primitives #472

Merged
merged 12 commits into from
Feb 21, 2020
Merged

Java: Unboxed primitives #472

merged 12 commits into from
Feb 21, 2020

Conversation

lukemaurer
Copy link
Collaborator

@lukemaurer lukemaurer commented Jan 2, 2020 •
edited
Loading

(Depends on #524.)

This would have been easy if it weren't for the unfortunate interaction between primitives, arrays, and generics in Java. Namely, a method taking a T[] can't take a byte[], because T can only stand for a reference type. Thus the only type that can stand for an array of any type is java.lang.Object. We need a fast way to create and operate on arrays of arbitrary type, and Java does not provide it (most methods of java.lang.reflect.Array are very slow). This was a three-step process:

  1. Introduce lvalue abstraction #523: In the base Compiler class, introduce a general system for turning assignments into calls to setter methods so that an assignment to an array of unknown type can be expressed as a method call. (Java already needed this; its implementation of trait fields was buggy.)

  2. Introduce Type objects to Java runtime #524: Replace the strings used for type descriptors with objects, which are much faster and more type-safe. (This also fixes existing bugs.)

  3. This PR: Have all primitive types appear in unboxed form where possible (that is, when the type isn't a parameter). Represent a generic array as a java.lang.Object and use the corresponding dafny.Type for array operations.

@robin-aws
Copy link
Member

AWS CodeBuild CI Report

  • CodeBuild project: Dafny
  • Commit ID: b0c0e38
  • Result: FAILED
  • Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

@seanmcl
Copy link
Collaborator

seanmcl commented Jan 2, 2020

Could you push a branch for the concat change and base this on that branch? As a reviewer I don't want to read the same changes twice.

@lukemaurer lukemaurer changed the base branch from master to lazy-concat-java January 3, 2020 01:50
@lukemaurer
Copy link
Collaborator Author

Could you push a branch for the concat change and base this on that branch? As a reviewer I don't want to read the same changes twice.

!! Good idea, done.

@robin-aws
Copy link
Member

AWS CodeBuild CI Report

  • CodeBuild project: Dafny
  • Commit ID: 2472afe
  • Result: FAILED
  • Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

@robin-aws
Copy link
Member

AWS CodeBuild CI Report

  • CodeBuild project: Dafny
  • Commit ID: 644fcc5
  • Result: FAILED
  • Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

@robin-aws
Copy link
Member

AWS CodeBuild CI Report

  • CodeBuild project: Dafny
  • Commit ID: c65c196
  • Result: FAILED
  • Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

@lukemaurer lukemaurer mentioned this pull request Jan 15, 2020
Merged
@lukemaurer lukemaurer changed the base branch from lazy-concat-java to master January 15, 2020 23:51
@robin-aws
Copy link
Member

AWS CodeBuild CI Report

  • CodeBuild project: Dafny
  • Commit ID: ec6a81d
  • Result: FAILED
  • Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

@robin-aws
Copy link
Member

Hi @lukemaurer! I'm excited to review this but it's a really large change set. Is there any chance you could break it up into 2 or even 3 different PRs in sequence, given the high-level breakdown you gave?

@lukemaurer
Copy link
Collaborator Author

Hi @lukemaurer! I'm excited to review this but it's a really large change set. Is there any chance you could break it up into 2 or even 3 different PRs in sequence, given the high-level breakdown you gave?

I can, though it's a bit of a bumpy road in places—in particular, DafnySequence.java gets overhauled twice. I'll try and rearrange things so there's not too much to re-review.

Luke Maurer added 6 commits January 27, 2020 22:05
Java: Unboxed primitive types
4c4563b 
Primitive types are now represented by the actual primitives, in unboxed form.
Unsigned types are represented by their signed counterparts; UInt and friends
are no more (this was a previous patch).

To represent an array of unknown type, the dafny.Array<T> class is introduced.
It is *only* used when the type T is an unknown parameter, to avoid the
overhead of an object for each array.  (Multi-dimensional arrays always use the
corresponding dafny.Array{n} classes, since we need the object anyway to
remember the dimensions.)  The tricky thing here is coercing, say, byte[] to
dafny.Array<Byte> when calling a generic method expecting dafny.Array<T>, and
coercing in the other direction if a method returns a generic array.
Fixes; base DafnySequence on dafny.Array
2ec0d5a 
Several fixes to the handling of arrays, especially their interaction with
sequences.  ByteArrayDafnySequence is now folded into ArrayDafnySequence, which
is now backed by a dafny.Array.  Also it now takes the element type descriptor
as an argument so that the correct array can be created (this will break extern
code).
Java, Go: Fix conversion from character to native int
022c20b
Java: Dynamically find _type method of extern class
a9114b9 
Since an extern class may be one whose source code the user can't change, and
since the default value of a class is almost always null so an explicit _type
function isn't necessary, Java now does what the other backends do and
dynamically looks for a static _type method for any extern class.  This may be
a performance issue.  TODO: Consider a WeakHashMap from java.lang.Class to
dafny.Type (or some sort of dafny.TypeFunction in the case of a generic type)
to save on reflection.
DafnySequence performance tweaks
23d7f91 
A couple of small issues look to be having outsized influence: Create() loops
over BigInteger and converts each to an int rather than looping over ints and
creating a BigInteger for each; the latter is much faster.  Also,
LazyDafnySequence doesn't override verbatimString(), which was causing
concatenated DafnySequence<Character>s to be very slow in converting to
strings.
Avoid assertion error on ghost method with {:extern} declaration
fda7238
@lukemaurer lukemaurer force-pushed the unboxed-java branch 2 times, most recently from d3bb417 to 5245c1f Compare January 28, 2020 06:37
@robin-aws
Copy link
Member

AWS CodeBuild CI Report

  • CodeBuild project: Dafny
  • Commit ID: d3bb417
  • Result: SUCCEEDED
  • Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

@robin-aws
Copy link
Member

AWS CodeBuild CI Report

  • CodeBuild project: Dafny
  • Commit ID: 5245c1f
  • Result: SUCCEEDED
  • Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

@lukemaurer lukemaurer changed the base branch from master to java-type-descriptors January 28, 2020 07:16
@lukemaurer
Copy link
Collaborator Author

Hi @lukemaurer! I'm excited to review this but it's a really large change set. Is there any chance you could break it up into 2 or even 3 different PRs in sequence, given the high-level breakdown you gave?

Okay, done: There's now #521 (largely unrelated but other changes build on it), #522, #523, and #524. Unfortunately, there's a bit of churn in DafnySequence still ...)

@lukemaurer lukemaurer changed the title Java: Unboxed primitives, type parameter overhaul Java: Unboxed primitives Jan 28, 2020
@robin-aws
Copy link
Member

Thanks @lukemaurer, this is much more digestible now! :) I'll start with #521 and go from there.

@robin-aws
Copy link
Member

AWS CodeBuild CI Report

  • CodeBuild project: Dafny
  • Commit ID: edfe97b
  • Result: SUCCEEDED
  • Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

@robin-aws
Copy link
Member

AWS CodeBuild CI Report

  • CodeBuild project: Dafny
  • Commit ID: cb11756
  • Result: FAILED
  • Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

Use java.lang.Object instead of dafny.Array for generic arrays
2cac926 
There was a fatal flaw in the scheme that encoded an array of generic type T as
a `dafny.Array<T>` and an array of known type as a plain array: While we can
unwrap a returned array as necessary to coerce from, say,
`dafny.Array<Integer>` to `int[]`, we cannot expect to do the same for a
`dafny.Array<T>` somewhere inside a class or datatype.  The only alternative
that doesn't add overhead to the known-element-type case is to represent an
array of a type parameter as a `java.lang.Object` (since, sadly, primitive
arrays and object arrays share no other superclass).  Generated code will still
be type-correct since the compiler knows which `java.lang.Object`s are arrays
of which type, and we can use the `dafny.Type<T>` object passed into a generic
method to perform array operations.

The `dafny.Array` class is retained for convenience in programming but is no
longer used by generated code.
@robin-aws
Copy link
Member

AWS CodeBuild CI Report

  • CodeBuild project: Dafny
  • Commit ID: 2cac926
  • Result: FAILED
  • Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

@lukemaurer
Copy link
Collaborator Author

AWS CodeBuild CI Report

* CodeBuild project: Dafny

* Commit ID: [2cac926](https://github.com/dafny-lang/dafny/commit/2cac9263e09192abec69880eb5605e2ee497aed2)

* Result: FAILED

* [Build Logs](https://g85ugprat7.execute-api.us-west-2.amazonaws.com/Prod/buildlogs?key=bc97fafd-c3fa-47b2-ad86-8184eb44ff74%2Fbuild.log) (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

This looks spurious (something to do with thread scheduling). It WFM, at any rate.

@robin-aws
Copy link
Member

AWS CodeBuild CI Report

* CodeBuild project: Dafny

* Commit ID: [2cac926](https://github.com/dafny-lang/dafny/commit/2cac9263e09192abec69880eb5605e2ee497aed2)

* Result: FAILED

* [Build Logs](https://g85ugprat7.execute-api.us-west-2.amazonaws.com/Prod/buildlogs?key=bc97fafd-c3fa-47b2-ad86-8184eb44ff74%2Fbuild.log) (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

This looks spurious (something to do with thread scheduling). It WFM, at any rate.

Known issue: #454 :(

@robin-aws
Copy link
Member

AWS CodeBuild CI Report

  • CodeBuild project: Dafny
  • Commit ID: ed1fb28
  • Result: SUCCEEDED
  • Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

@robin-aws
Copy link
Member

AWS CodeBuild CI Report

  • CodeBuild project: Dafny
  • Commit ID: 0c6f814
  • Result: SUCCEEDED
  • Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

@robin-aws
Copy link
Member

AWS CodeBuild CI Report

  • CodeBuild project: Dafny
  • Commit ID: c78bba8
  • Result: SUCCEEDED
  • Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

@RustanLeino
Copy link
Collaborator

This is a PR against a new branch, java-type-descriptors, rather than master. I tried changing it before merging, but github gave me a scary warning. So, instead, I'll merge this into the java-type-descriptors branch, and will then merge that into master.

@RustanLeino RustanLeino merged commit 36e609b into dafny-lang:java-type-descriptors Feb 21, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@lukemaurer @robin-aws @seanmcl @RustanLeino