Whiley v0.4.0 Released!

Thursday, November 24th, 2016

The next release is finally upon us. This one has been a long time coming, and its going to take a while before it settles down again!! Work on this release has been ongoing since February, though partial changes were released in v0.3.40 . In that time, a significant portion of the compiler has been rewritten (hence why it’ll take time to stabilise). The main updates are:

  • Bytecode Format (#563, #620).   Perhaps the most significant change is a complete overhaul of the Whiley Intermediate Language (WyIL).  This was previously an unstructured bytecode, roughly based on JVM bytecode.  However, the unstructured nature of WyIL made Verification Condition Generation overly challenging.  Hence, WyIL is now a structured bytecode format and, in fact, is now very similar to a binary version of Whiley source.

  • Plugin System (#476).  Another significant difference from previous releases is the organisation of the Whiley compiler itself.   Firstly, the github repository has been split into multiple smaller repositories.  Secondly, the compiler is now really a plugin framework called the “Whiley Compiler Collection”.  The Whiley Compiler is then a plugin within this framework.  The entire system is now also available on Maven central as a set of plugins and can be incorporated relatively easily for use with other (e.g. Java) projects.  A new command-line interface has been developed to provide a consistent interface with these plugins as well.

  • Type System (#629).  The way in which types are handled within the compiler has been redesigned.  In particular, types within WyIL are no longer represented using directed graphs (i.e. automata) and, instead, are represented just as trees.  To deal with subtyping properly, types are then expanded at the point of subtype testing to ensure completeness.  This resolves some outstanding issues pertaining to the manner in which nominal information was retained within the compiler.  It also simplifies the compiler in many ways by restricting the complexity of fully-expanded types to just one component (namely the TypeSystem ).  This also affects other aspects of the language.  For example, we can now overload on nominal types.  That is, have two functions with distinct signatures that expand to equivalent types (though whether or not this is useful remains to be seen).

  • Verification Condition Generator (#501).  Perhaps the main reason for redesigning the WyIL bytecode format was to simplify the process of verification condition generation.  Hence, the verification condition generator has been completely rewritten to exploit this.  And, it is indeed much simpler, especially with respect to the handling of flow typing.  At this stage, however, there remains further work needed in order to realise the full benefits from the new bytecode format.  These improvements will be rolling out over subsequent releases.

These changes are all extremely positive from my perspective.  The primary goal for the next phase of the project is to consolidate the system as it stands (i.e. to make what we have work better).  After that, I’ll be interested in further evolving the language and exploring alternative targets (e.g. JavaScript, LLVM) more seriously.  Here are the main areas that need consolidation:

  • Reimplement Subtype Operator (#697).  The subtype operator has long been known as suffering some serious flaws in its design.  For the most part, these went unnoticed.  However, with recent changes to the compiler, the limitations are becoming more noticeable and something needs to be done here.  Unfortunately, the full solution is not completely known to me … so some serious thinking is required.

  • Reimplement Automated Theorem Prover (#22).  Whilst the automated theorem prover works quite well for small examples, it quickly starts to hit problems beyond that.  The main problem lies in the relative difficulty within the existing framework to experiment with different heuristics and search strategies for quantifier instantiation.

  • Syntax Evolution. There are several important changes to the language syntax which are planned.  This includes removing operator precedence (#506), lifetime parameters for nominal types (#648), templates (#540), match statements (#81) and updating constant declarations (#692).  Most of these require more details to be worked through first though.

Right, that’s enough for now.  Of course, there are lots of other things needing to be done.  For example, updating the instructions on how to setup and run Whiley, updating the Whiley Language Specification document, and general testing of the system.