Extending Java with Liquid Types
LiquidJava is an additional type system for Java that uses liquid types to express constraints programs must follow, helping catch more bugs before they run.
+
diff --git a/playground/editor.css b/playground/editor.css
new file mode 100644
index 0000000..f49fb8a
--- /dev/null
+++ b/playground/editor.css
@@ -0,0 +1,47 @@
+.lj-playground { margin: 1.5rem 0; }
+.lj-toolbar { display: flex; align-items: flex-end; justify-content: space-between; flex-wrap: wrap; gap: 1rem; }
+.lj-example-picker { position: relative; display: flex; flex-direction: column; flex: 0 1 15rem; gap: .4rem; min-width: 0; }
+.lj-example-picker::after { content: ''; position: absolute; right: 1rem; bottom: 1.1rem; width: .4rem; height: .4rem; border-right: 2px solid #5f7ea1; border-bottom: 2px solid #5f7ea1; transform: rotate(45deg); pointer-events: none; }
+.lj-toolbar label { color: #555c65; font-size: .8rem; font-weight: 400; }
+.lj-toolbar select,
+.lj-toolbar button { min-height: 2.5rem; border: 1px solid #cbd2d9; border-radius: .5rem; font: inherit; font-size: .875rem; font-weight: 400; line-height: 1.4; }
+.lj-toolbar select { appearance: none; width: 100%; padding: .6rem 2.5rem .6rem .85rem; color: #2a2f36; background: #fff; border-color: #c7d7ea; box-shadow: 0 1px 2px rgba(23, 26, 31, .05); cursor: pointer; }
+.lj-toolbar select:hover { border-color: #5f7ea1; background: #fafcfe; }
+.lj-examples { display: flex; align-items: flex-end; flex: 1 1 25rem; gap: .5rem; min-width: 0; }
+.lj-toolbar button { padding: .5rem .9rem; color: #334e68; background: transparent; box-shadow: none; cursor: pointer; }
+.lj-toolbar button:hover:not(:disabled) { background: #e5eef7; border-color: #5f7ea1; }
+.lj-toolbar #lj-verify,
+.lj-toolbar #lj-reset { min-width: 5rem; padding: .6rem .9rem; color: #fff; background: #334e68; border-color: #334e68; white-space: nowrap; flex-shrink: 0; }
+.lj-toolbar #lj-verify:hover:not(:disabled),
+.lj-toolbar #lj-reset:hover { background: #253b50; border-color: #253b50; }
+.lj-toolbar #lj-verify[data-state="busy"] { background: #c62828; border-color: #c62828; }
+.lj-toolbar #lj-verify[data-state="busy"]:hover { background: #a61f1f; border-color: #a61f1f; }
+.lj-toolbar button:disabled { color: #8a929b; background: #efefec; border-color: #e4e4e7; cursor: default; }
+.lj-toolbar #lj-verify:disabled { color: #fff; background: #7f90a1; border-color: #7f90a1; }
+.lj-toolbar select:focus-visible,
+.lj-toolbar button:focus-visible { outline: 2px solid #5f7ea1; outline-offset: 3px; }
+#lj-editor { margin: 1rem 0; overflow: hidden; }
+.lj-playground .cm-editor { font-size: .75em; border-radius: inherit; overflow: hidden; }
+.lj-playground .cm-scroller { min-height: 200px; max-height: 560px; overflow: auto; font-family: 'JetBrains Mono', 'SFMono-Regular', Menlo, Consolas, monospace; line-height: 1.6; scrollbar-width: thin; scrollbar-color: rgba(255, 255, 255, .72) rgba(255, 255, 255, .16); }
+.lj-playground .cm-focused { outline: 2px solid #7dd3fc; outline-offset: -2px; }
+.lj-output { color: #e6edf7; }
+#lj-status { margin: 0; padding: 1rem 1.15rem; font-family: 'JetBrains Mono', 'SFMono-Regular', Menlo, Consolas, monospace; font-size: .75em; line-height: 1.6; }
+#lj-status.sr-only { position: absolute; width: 1px; height: 1px; padding: 0; margin: -1px; overflow: hidden; clip-path: inset(50%); white-space: nowrap; }
+#lj-status[data-state="success"] { color: #a7f3c1; }
+#lj-status[data-state="warning"] { color: #f6c177; }
+#lj-status:not(.sr-only) + #lj-results:not(:empty) { border-top: 1px solid #ffffff1a; }
+.main-content #lj-results pre { margin: 0; }
+.main-content #lj-results a { color: #e6edf7; text-decoration: underline; text-underline-offset: .2em; }
+.main-content #lj-results a:hover { color: #e6edf7; }
+.main-content #lj-results a:focus-visible { outline: 2px solid #7dd3fc; outline-offset: 3px; }
+#lj-results .ansi-black-fg { color: #111827; }
+#lj-results .ansi-bright-black-fg { color: #9ca3af; }
+#lj-status[data-state="error"],
+#lj-status[data-state="failure"],
+#lj-results :is(.ansi-red-fg, .ansi-bright-red-fg) { color: #f29e9e; }
+#lj-results :is(.ansi-green-fg, .ansi-bright-green-fg) { color: #a7f3c1; }
+#lj-results :is(.ansi-yellow-fg, .ansi-bright-yellow-fg) { color: #f6c177; }
+#lj-results :is(.ansi-blue-fg, .ansi-bright-blue-fg) { color: #93b4f4; }
+#lj-results :is(.ansi-magenta-fg, .ansi-bright-magenta-fg) { color: #c4b5fd; }
+#lj-results :is(.ansi-cyan-fg, .ansi-bright-cyan-fg) { color: #7dd3fc; }
+#lj-results :is(.ansi-white-fg, .ansi-bright-white-fg) { color: #e6edf7; }
diff --git a/playground/index.md b/playground/index.md
new file mode 100644
index 0000000..a979057
--- /dev/null
+++ b/playground/index.md
@@ -0,0 +1,39 @@
+---
+title: Playground
+nav_order: 8
+permalink: /playground/
+has_toc: false
+description: Try LiquidJava refinements and typestates directly in your browser.
+---
+
+# Playground
+
+Run the LiquidJava verification directly in your browser. Edit an example and select **Verify**.
+
+
+
+
+
+
+
+
diff --git a/playground/isolation.js b/playground/isolation.js
new file mode 100644
index 0000000..aef32c9
--- /dev/null
+++ b/playground/isolation.js
@@ -0,0 +1,14 @@
+// GitHub Pages cannot set these response headers; isolate only the playground.
+self.addEventListener('install', () => self.skipWaiting());
+self.addEventListener('activate', event => event.waitUntil(self.clients.claim()));
+self.addEventListener('fetch', event => {
+ if (new URL(event.request.url).origin !== self.location.origin) return;
+ event.respondWith((async () => {
+ const response = await fetch(event.request);
+ if (response.type === 'opaque') return response;
+ const headers = new Headers(response.headers);
+ headers.set('Cross-Origin-Opener-Policy', 'same-origin');
+ headers.set('Cross-Origin-Embedder-Policy', 'require-corp');
+ return new Response(response.body, { status: response.status, statusText: response.statusText, headers });
+ })());
+});
diff --git a/scripts/playground/adapter.mjs b/scripts/playground/adapter.mjs
new file mode 100644
index 0000000..e0875ab
--- /dev/null
+++ b/scripts/playground/adapter.mjs
@@ -0,0 +1,34 @@
+export function createNatives(Z3, methods) {
+ const natives = { Java_com_microsoft_z3_Native_setInternalErrorHandler() {} };
+ for (const { name, types, api } of methods) {
+ natives[`Java_com_microsoft_z3_Native_${name}`] = async (_lib, ...args) => {
+ const input = args.map((value, i) => types[i] === 'long' ? Number(value) : value);
+ // numeric int64 arguments are values, whereas other longs are WASM pointers
+ if (api === 'mk_int64' || api === 'mk_unsigned_int64') input[1] = BigInt(args[1]);
+ if (api === 'model_eval') {
+ const value = await Z3.model_eval(...input.slice(0, 4));
+ if (value === null) return false;
+ args[4].value = value;
+ return true;
+ }
+ if (types.some(type => type.endsWith('Ptr'))) {
+ throw new Error(`Unsupported Z3 output parameter: ${api}`);
+ }
+ // the JS binding derives array counts from the array itself
+ for (let i = types.length - 1; i >= 1; i--) {
+ if (types[i] === 'long[]' && types[i - 1] === 'int') {
+ input[i] = Array.from(input[i], Number);
+ input.splice(i - 1, 1);
+ }
+ }
+ if (typeof Z3[api] !== 'function') throw new Error(`Unsupported Z3 operation: ${api}`);
+ const result = await Z3[api](...input);
+ // the desktop verifier treats unknown as success; the playground must not
+ if ((api === 'solver_check' || api === 'solver_check_assumptions') && result === 0) {
+ throw new Error('Z3 could not determine whether this refinement holds.');
+ }
+ return result;
+ };
+ }
+ return natives;
+}
diff --git a/scripts/playground/adapter.test.mjs b/scripts/playground/adapter.test.mjs
new file mode 100644
index 0000000..ab41234
--- /dev/null
+++ b/scripts/playground/adapter.test.mjs
@@ -0,0 +1,51 @@
+import test from 'node:test';
+import assert from 'node:assert/strict';
+import { readFile } from 'node:fs/promises';
+import z3 from 'z3-solver';
+const { init } = z3;
+import { createNatives } from './adapter.mjs';
+
+const methods = JSON.parse(await readFile(new URL('../../playground/runtime/native-methods.json', import.meta.url)));
+
+test('existing Java ABI checks bounds, evaluates models and passes counted arrays to WASM', async () => {
+ const { Z3, em } = await init();
+ const natives = createNatives(Z3, methods);
+ const call = (name, ...args) => natives[`Java_com_microsoft_z3_Native_INTERNAL${name}`](null, ...args);
+ const ctx = await call('mkContext', 0);
+ try {
+ const sort = await call('mkIntSort', ctx);
+ const name = await call('mkStringSymbol', ctx, 'x');
+ const x = await call('mkConst', ctx, name, sort);
+ const zero = await call('mkInt', ctx, 0, sort);
+ const two = await call('mkInt', ctx, 2, sort);
+ const large = await call('mkInt64', ctx, 9007199254740993n, sort);
+ assert.equal(await call('getNumeralString', ctx, large), '9007199254740993');
+ const lower = await call('mkGt', ctx, x, zero);
+ const upper = await call('mkLt', ctx, x, two);
+ const bounds = await call('mkAnd', ctx, 2, new BigInt64Array([BigInt(lower), BigInt(upper)]));
+ const solver = await call('mkSolver', ctx);
+ await call('solverIncRef', ctx, solver);
+ await call('solverAssert', ctx, solver, bounds);
+ assert.equal(await call('solverCheck', ctx, solver), 1);
+ const model = await call('solverGetModel', ctx, solver);
+ const output = { value: 0 };
+ assert.equal(await call('modelEval', ctx, model, x, true, output), true);
+ assert.equal(await call('getNumeralString', ctx, output.value), '1');
+ await call('solverAssert', ctx, solver, await call('mkLt', ctx, x, zero));
+ assert.equal(await call('solverCheck', ctx, solver), -1);
+ await call('solverDecRef', ctx, solver);
+ } finally {
+ await call('delContext', ctx);
+ em.PThread.terminateAllThreads();
+ }
+});
+
+test('an unknown solver result cannot become a successful verification', async () => {
+ const natives = createNatives({ solver_check: async () => 0 }, methods);
+ await assert.rejects(natives.Java_com_microsoft_z3_Native_INTERNALsolverCheck(null, 1, 2), /could not determine/);
+});
+
+test('unimplemented ABI operations fail explicitly', async () => {
+ const natives = createNatives({}, methods);
+ await assert.rejects(natives.Java_com_microsoft_z3_Native_INTERNALgetNumeralInt(null, 1, 2, { value: 0 }), /Unsupported Z3 output parameter/);
+});
diff --git a/scripts/playground/build.mjs b/scripts/playground/build.mjs
new file mode 100644
index 0000000..298f3f7
--- /dev/null
+++ b/scripts/playground/build.mjs
@@ -0,0 +1,8 @@
+import { build } from 'esbuild';
+import { copyFile } from 'node:fs/promises';
+const output = 'playground/runtime';
+await build({ entryPoints: ['scripts/playground/worker.js'], bundle: true, format: 'iife', platform: 'browser', outfile: `${output}/worker.js` });
+await build({ entryPoints: ['scripts/playground/editor.js'], bundle: true, format: 'esm', platform: 'browser', outfile: `${output}/editor.js` });
+for (const file of ['z3-built.js', 'z3-built.wasm']) {
+ await copyFile(`node_modules/z3-solver/build/${file}`, `${output}/${file}`);
+}
diff --git a/scripts/playground/build.py b/scripts/playground/build.py
new file mode 100644
index 0000000..d4ea394
--- /dev/null
+++ b/scripts/playground/build.py
@@ -0,0 +1,97 @@
+"""Build the browser runner from unmodified published LiquidJava sources."""
+import json
+import re
+import subprocess
+import shutil
+import urllib.request
+import zipfile
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[2]
+WORK = ROOT / '.playground-build'
+OUTPUT = ROOT / 'playground/runtime'
+VERIFIER = '0.0.35'
+API = '0.0.7'
+Z3 = '4.8.17'
+SPOON = '10.4.2'
+
+
+def artifact(group, name, version, classifier=''):
+ filename = f'{name}-{version}{classifier}.jar'
+ target = WORK / filename
+ if not target.exists():
+ url = f'https://repo.maven.apache.org/maven2/{group.replace(".", "/")}/{name}/{version}/{filename}'
+ print(f'Downloading {filename}', flush=True)
+ urllib.request.urlretrieve(url, target)
+ return target
+
+
+def main():
+ properties = subprocess.run(['java', '-XshowSettings:properties', '-version'], capture_output=True, text=True, check=True).stderr
+ java_home = Path(re.search(r'java.home = (.+)', properties).group(1).strip())
+ if not re.search(r'java.version = 17[.\s]', properties):
+ raise RuntimeError('Build the playground with JDK 17 (set JAVA_HOME and PATH)')
+ WORK.mkdir(exist_ok=True)
+ OUTPUT.mkdir(parents=True, exist_ok=True)
+ verifier = artifact('io.github.liquid-java', 'liquidjava-verifier', VERIFIER)
+ sources = artifact('io.github.liquid-java', 'liquidjava-verifier', VERIFIER, '-sources')
+ annotations = artifact('io.github.liquid-java', 'liquidjava-api', API, '-sources')
+ z3_sources = artifact('tools.aqua', 'z3-turnkey', Z3, '-sources')
+ spoon_sources = artifact('fr.inria.gforge.spoon', 'spoon-core', SPOON, '-sources')
+ source_dir = WORK / 'sources'
+ if source_dir.exists():
+ shutil.rmtree(source_dir)
+ source_dir.mkdir()
+ for source in [sources, annotations]:
+ with zipfile.ZipFile(source) as jar:
+ for item in jar.namelist():
+ if item.endswith('.java'):
+ path = source_dir / item
+ path.parent.mkdir(parents=True, exist_ok=True)
+ path.write_bytes(jar.read(item))
+ # CheerpJ casts can have empty stack traces. Select Spoon's existing
+ # exotic-JVM query mode rather than failing its static initialization.
+ query_path = 'spoon/reflect/visitor/chain/CtQueryImpl.java'
+ with zipfile.ZipFile(spoon_sources) as jar:
+ query = jar.read(query_path).decode()
+ original = 'StackTraceElement[] stack = e.getStackTrace();'
+ if query.count(original) != 1:
+ raise RuntimeError('Spoon query adaptation no longer matches its source')
+ query = query.replace(original, original + '\n\t\t\tif (stack.length == 0) return -1;')
+ path = source_dir / query_path
+ path.parent.mkdir(parents=True, exist_ok=True)
+ path.write_text(query)
+ classes = WORK / 'classes'
+ if classes.exists():
+ shutil.rmtree(classes)
+ classes.mkdir()
+ files = list(source_dir.rglob('*.java')) + list((ROOT / 'scripts/playground/java').rglob('*.java'))
+ args = WORK / 'javac.args'
+ args.write_text('\n'.join('"' + str(file) + '"' for file in files))
+ subprocess.run(['javac', '--release', '17', '-cp', str(verifier), '-d', str(classes), '@' + str(args)], check=True)
+ with zipfile.ZipFile(verifier) as jar, zipfile.ZipFile(OUTPUT / 'liquidjava.jar', 'w', zipfile.ZIP_DEFLATED) as out:
+ for item in jar.infolist():
+ # replace compiled classes, keep the remaining dependencies and resources
+ if (classes / item.filename).is_file() or item.filename.endswith(('.dll', '.so', '.dylib')):
+ continue
+ if item.filename.startswith('META-INF/versions/') or item.filename.endswith(('.SF', '.RSA', '.DSA')):
+ continue
+ out.writestr(item.filename, jar.read(item.filename))
+ for file in classes.rglob('*.class'):
+ out.writestr(file.relative_to(classes).as_posix(), file.read_bytes())
+ with zipfile.ZipFile(java_home / 'jmods/java.base.jmod') as jar, zipfile.ZipFile(OUTPUT / 'java-base.jar', 'w', zipfile.ZIP_DEFLATED) as out:
+ for name in jar.namelist():
+ if name.startswith('classes/') and name.endswith('.class') and name != 'classes/module-info.class':
+ out.writestr(name[len('classes/'):], jar.read(name))
+ with zipfile.ZipFile(z3_sources) as jar:
+ native = jar.read('com/microsoft/z3/Native.java').decode()
+ methods = []
+ for name, params in re.findall(r'native\s+\w+\s+(INTERNAL\w+)\(([^)]*)\)', native):
+ types = [param.strip().split()[0] for param in params.split(',') if param.strip()]
+ api = re.sub(r'([a-z0-9])([A-Z])', r'\1_\2', name[len('INTERNAL'):]).lower()
+ methods.append(dict(name=name, types=types, api=api))
+ (OUTPUT / 'native-methods.json').write_text(json.dumps(methods))
+
+
+if __name__ == '__main__':
+ main()
diff --git a/scripts/playground/diagnostics.mjs b/scripts/playground/diagnostics.mjs
new file mode 100644
index 0000000..358de4f
--- /dev/null
+++ b/scripts/playground/diagnostics.mjs
@@ -0,0 +1,19 @@
+import { AnsiUp } from 'ansi_up';
+
+function shortenLocations(output) {
+ return output.replace(/^\/files\/playground\/(?=[^/\r\n]+:\d+)/gm, '/playground/');
+}
+
+export function editorDiagnostic(issue, length) {
+ const { from, to } = issue;
+ if (!Number.isInteger(from) || !Number.isInteger(to) || from < 0 || to <= from || to > length) return null;
+ return { from, to, severity: issue.severity, message: issue.output === undefined ? undefined : shortenLocations(issue.output).replace(/\u001b\[[0-9;]*m/g, '') };
+}
+
+export function diagnosticHtml(output) {
+ const ansi = new AnsiUp();
+ ansi.use_classes = true;
+ return ansi.ansi_to_html(shortenLocations(output).replace(/^(?:\r?\n)+/, ''))
+ .replace(/^(\/playground\/[^<\r\n]+:(\d+))(?=\r?\n|$|<\/span>)/gm,
+ '$1');
+}
diff --git a/scripts/playground/diagnostics.test.mjs b/scripts/playground/diagnostics.test.mjs
new file mode 100644
index 0000000..e6d9146
--- /dev/null
+++ b/scripts/playground/diagnostics.test.mjs
@@ -0,0 +1,65 @@
+import test from 'node:test';
+import assert from 'node:assert/strict';
+import { diagnosticHtml, editorDiagnostic } from './diagnostics.mjs';
+
+test('make diagnostic and declaration locations editor links without linking source excerpts', () => {
+ const html = diagnosticHtml('Error\n6 | String path = "/playground/Example.java:99";\n\n/files/playground/Example.java:6\u001b[0m\n\n--> Refinement declared here:\n/files/playground/Example.java:5\u001b[0m\n');
+ assert.match(html, /\/playground\/Example.java:6<\/a>/);
+ assert.match(html, /\/playground\/Example.java:5<\/a>/);
+ assert.equal((html.match(/ {
+ const diagnostic = '\u001b[31mError\u001b[0m\n6 | code\n | ^^^\n\nExample.java:6\n';
+ assert.equal(diagnosticHtml('\n\n' + diagnostic), diagnosticHtml(diagnostic));
+});
+
+test('show the playground path, filename and line in diagnostic locations', () => {
+ const output = '\u001b[31mError\u001b[0m\n\n/files/playground/Example.java:6\u001b[0m\n\n--> Refinement declared here:\n/files/playground/Example.java:5\u001b[0m\n';
+ const expected = output.replaceAll('/files/playground/', '/playground/');
+ assert.equal(diagnosticHtml(output), diagnosticHtml(expected));
+ assert.equal(editorDiagnostic({ from: 0, to: 1, output }, 1).message,
+ expected.replace(/\u001b\[[0-9;]*m/g, ''));
+});
+
+test('render CLI colors and bold with resets and escaped source text', () => {
+ const html = diagnosticHtml('\u001b[1;31mRefinement Error\u001b[0m: \n\u001b[38;5;208m^^^\u001b[0m\n');
+ assert.match(html, /font-weight:bold/);
+ assert.match(html, /ansi-red-fg/);
+ assert.match(html, /color:rgb\(/);
+ assert.match(html, /rgb\(255,135,0\)/);
+ assert.match(html, /<script>/);
+ assert.doesNotMatch(html, /
+
+
+
+
+