1. Summary
Laurel is an intermediate analysis language. Its purpose is to reduce the cost of analysing code for popular languages. Currently Laurel is focused on enabling analysis of Java, Python, and JavaScript, but this list will grow and you can already use it for other languages as well.
Laurel is a good target when your source language has mutation and a function-like construct. Some source-language features must be compiled away before or during translation, because Laurel does not model them directly:
-
metaprogramming (macros, reflection, runtime code generation);
-
type-system features that do not fit Laurel's type system, which is close to C#'s (for example higher-kinded types or advanced generics);
-
pointers and pointer arithmetic (Laurel does not yet model these).
Laurel is not a good target for languages that use none of its features — typically languages with no procedure-like construct, such as assembly, or inputs that are not programming languages at all. A stack-based language like JVM bytecode still benefits from targeting Laurel.
You use Laurel by building a compiler from your source language to Laurel. This guide will help you understand Laurel and thus help build such compilers.
Laurel supports several types of analysis and some of these require additional information besides the implementation code. You can enable your users to provide this information through annotations in the source program, and those annotations should then be used in the compilation to Laurel, where the analysis specific information lives in first class language constructs.
Using just the Strata CLI — without writing any Strata extensions — a Laurel program can be put through these kinds of analysis. Laurel does not implement them itself; it lowers to Strata Core, which performs the analysis:
-
Property-based testing (planned)
-
Bounded verification
-
Unbounded verification
Front-end compilers targeting Laurel can recover from some errors in user code rather than abort:
when a side-effect-free sub-expression cannot be translated, emit a diagnostic and put a hole
(<?>) in its place. The program still compiles and the analyses still run, so users see your
diagnostic plus any further genuine errors instead of a cascade caused by the first one. Holes
stand for an unknown value only — they do not model mutation — so replacing code that may have side
effects with a hole silently drops those effects and can make an analysis prove properties the
original program does not have. For untranslatable constructs that may have effects, and for
unrecoverable errors (for example resolution failures), abort with a diagnostic instead.