JmlEclipseDeveloperJournal

• [JmlEclipse] Developer Journal
  • 2010.05.03 Commit and Test Results Summary
  • 2010.04.10 Commit and Test Results Summary
  • 2010.04.09 Commit and Test Results Summary
  • 2010.03.30
  • 2010.03.29
  • 2010.03.28
    • Commit r2154, r2155, r2156
    • Test Results
  • 2010.03.26
  • 2009.03.22

[JmlEclipse] Developer Journal

2010.05.03 Commit and Test Results Summary

PatriceChalin Commits for [JmlEclipse]: r2220, r2221.

• Hopefulling this marks final changes necessary to support JmlModifiers? as read from a given compilation unit or a $jir file. Note that the [JmlEclipseSetup] instructions have changed: you'll have to make a minor change by hand to the JDT APT.
• Disabling all of the current RAC tests that are failing simply because they need to be cleaned up.
• Added extra checks for represents clauses (static vs. non-static as compared to the field it represents). Also note that a static represents clause must be declared in the same type as the field it represents.
• All 2583 tests pass now.

2010.04.10 Commit and Test Results Summary

PatriceChalin Commits for [JmlEclipse]: r2193 to r2195.

• [JmlEclipse] preferences
  • Added check box to enable/disable RAC code printing.
  • clean-up also done.
• Finished this round of adjustment to front-end check w.r.t. nullities and other modifiers (for ghost and model fields).
• Updated tests:
  • Some tickets were opened against the RAC (and corresponding tests disabled).
  • Other tests had bugs that were detected by the new front-end checks :).
• All 2545 tests now pass.

PatriceChalin Commits for [JmlEclipse]: r2191, r2192.

Checkpoint.

• In general, fixed various issues concerning resolution and flow analysis w.r.t. members and their nullity as well as JML ghost or model members.
• IProblem: cleaned up some of the [JmlEclipse] specific messages (making them conform to the other JDT messages).
• Tests in Samples.java: turn off some of the advanced JDT settings as this is old code :).
• Test results: 2544 tests with 16 errors and 16 failures.

2010.04.09 Commit and Test Results Summary

PatriceChalin Commits. JIR: r2180 to r2183; [JmlEclipse]: r2184 to r2187.

This commit introduces important redesigns and simplifications. A summary is given below. More details will be given on the [JmlEclipseDesign] page.

• We've created the org.jmlspecs.eclipse.example.rac project containing examples (and JUnit 4 tests) that is intended to be used with [JmlEclipse] RAC. This project also contains the jml-runtime.jar that you need to add to any project compiled with the [JmlEclipse] RAC.
• All JML modifiers are now uniforming parsed, processed and internalized. The old way used different approaches, in particulr, w.r.t. handling nullity annotations using a nullity stack. All of this has been simplified. This change was to be done later, but the double pass strategy of the RAC causes problems because the old way mutated the AST which caused duplicate modifier warnings.
• Initial work on a new way to process .jml files. The old way was a memory hog that made it impossible to process large projects. The new way is based on JIR (itself improved and extended relative to our original paper on the subject).
• The JML AST hierarchy has been simplified. Some node types have been eliminated.
• RAC problem reporting has been improved:
  • Added problem reporter field to various translator classes.
  • Problem reported is now used, e.g. to warn about unsupported JML features (rather than printing to err).
• Conditionally generate code used to implement classical validity:
  • Added new compiler option jmlRacUseClassicalValidity which defaults to false. (Note that support is not yet complete w.r.t. getting and setting it via the IDE, etc.)
  • Used the jmlRacUseClassicalValidity flag to control whether classical or strong validity is used in generated RAC code.
• Source code clean-up (using the Sireum code formatting conventions).
• Various improvements to the front-end static checks; e.g. represents clause.
• Robby created a feature patch and various build scripts so that we can now automatically build the [JmlEclipse] plug-in. Thanks to Stephan Herrmann for pointers on how to do this.

For further details see the revision commit messages.

2010.03.30

PatriceChalin Commits r2167, r2168, r2169:

• Static checks (i.e. resolution, not static verification) of represents clauses, functional form only:
  • greatly simplified the code.
  • Type checking is now complete. In particular, Java 5 autoboxing works: e.g. represents i = 3 where i is an Integer.
  • An error is now reported for represents f = f, just as an error is reported for an assignment x = x or a field initialization f = f (this resolves an old JML2 bug).
• Refactored and simplified the JmlTypeBodyDeclaration hierarcy. We have fallen back on use the standard resolve(BlockScope) method.
• Documented and started implementing a scheme to be used for disabled JUnit 3 test cases. (The documentation explain why we cannot yet use JUnit 4).
• Added new checker tests for model fields.
• The RAC checkbox will only be selectable if DBC is enabled; this now matches the behavior of ESC and FSPV.

2010.03.29

PatriceChalin Commits r2157, r2158, r2159, r2163, r2164

• Errors are now reported for constraint, invariant, initially and represents (collectively type body declaration) clauses when a non-static member is accessed in a static clause.
• Refactored and cleaned up JmlTypeBodyDeclaration and its subtypes.
• Cleaned up tests (those that violated the access restrictions).
• All 2527 tests pass.

2010.03.28

PatriceChalin

Commit r2154, r2155, r2156

Part I. RAC integration

1. The new RAC is now properly hooked up to run within the IDE; in particular, the RAC can now be enabled and disabled via the JML preferences. (I also removed JML2 preference components that were causing warnings to be reported for the JML preferences.)
2. The JDT compiler behaves differently when run in batch mode vs. in the IDE. One such difference is that when the compiler is run from within the IDE, the field resolvedType of some ASTNode subtypes is not set. Instead one should query the AST node's binding to get the desired type binding. E.g., rather than
   • method.returnType.resolvedType, instead use method.binding.returnType.
   • arg.type.resolvedType, instead use arg.binding.type. Made a few changes in the RAC code generation to this effect.

Part II. The significant changes in this part of the commit had as goal to remove the, by now, outdated copy-pasted JDT code that was found in RAC and RAC test classes. These fixes highlighted some errors in the test cases; these have been fixed.

• In JML4c, the RacCompiler class that extended the JDT Compiler class and the RAC Main class extended the JDT batch Main class. Because the JDT Compiler class and its companion batch Main class are not setup with the right hooks, subclassing either of these also means copy-pasting code from the original parent class. This leads to subtle bugs; there were important changes in these two key classes from Eclipse 3.4 to 3.5 and I expect even more relative to 3.6. In this commit, we have merged RAC specific code from RacCompiler and RAC Main back into the JDT Compiler class and its batch Main class, respectively.
• The merge of the previous item also meant adding full support for the -P option (via JmlCompilerExtension); there are about 5 methods to be adjusted.
• Important refactoring and cleanup of RAC tests, including:
  • RacTestCompiler.java: removal of test helper code copy-pasted from the JDT AbstractRegressionTest; instead added simplified RAC specific helper methods that call the AbstractRegressionTest methods instead.
  • In tests that passed the names of Throwable classes as strings, these were replaced by tests that accept the actual Throwable class. (This helped pin point a few !JUnit tests that were using the wrong helper class.)
  • Where there used to be multiple tests over the same RAC code (in an attempt to try to match the expected output piecemeal) there is now a single test over that code.
  • Fixed some tests (e.g. ClassLevelSpecificationTest: tests were failing due to evaluation errors rather than raising the expected, say, JMLInvariantError. The evaluation errors were due to authentic NPEs in the tested code).

Test Results

All 2528 tests pass. Eclipse 3.5.2, Java 6.

2010.03.26

• PatriceChalin Eclipse 3.5.2, Java 6. All non ESC tests: out of 2588 tests got 9 failures (all from the new RAC suite -- these will be investigated shortly).

2009.03.22

• PatriceChalin Can get all 488 non ESC tests to pass (have not installed provers yet to regression test ESC4). One glitch (at least as of 3.5.2 as compared to the JML4 way of doing things): In order to avoid a security violation exception (which is reported when some of the tests are run), we now need to check out org.eclipse.jdt.compiler.apt. That's it, just check it out and it will be picked up when the tests are run.