From 322685a893bad1d10e6c07dae86a17a567eb506b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 22 Nov 2023 16:04:24 -0800 Subject: [PATCH 1/9] Deploy wasm to fiat-html --- fiat-html/fiat-crypto.html | 3 ++ fiat-html/main.js | 91 ++++++++++++++++++++++++-------------- 2 files changed, 62 insertions(+), 32 deletions(-) diff --git a/fiat-html/fiat-crypto.html b/fiat-html/fiat-crypto.html index 2beea09b2d..69b37b4842 100644 --- a/fiat-html/fiat-crypto.html +++ b/fiat-html/fiat-crypto.html @@ -49,6 +49,9 @@ + diff --git a/fiat-html/main.js b/fiat-html/main.js index 13ca34c8e6..26cf6fd37a 100644 --- a/fiat-html/main.js +++ b/fiat-html/main.js @@ -8,6 +8,7 @@ document.addEventListener('DOMContentLoaded', function() { const stdoutBox = document.getElementById('stdout'); const stderrBox = document.getElementById('stderr'); const versionBox = document.getElementById('version'); + const wasmCheckbox = document.getElementById('wasm'); const inputForm = document.getElementById('inputForm'); const inputArgs = document.getElementById('inputArgs'); const synthesizeButton = document.getElementById('synthesizeButton'); @@ -122,7 +123,8 @@ document.addEventListener('DOMContentLoaded', function() { } function updatePermalink(args) { - const queryString = `?argv=${encodeURIComponent(JSON.stringify(args.slice(1)))}&interactive`; + const wasmString = wasmCheckbox.checked ? '&wasm' : ''; + const queryString = `?argv=${encodeURIComponent(JSON.stringify(args.slice(1)))}&interactive${wasmString}`; // Handle both file and http(s) URLs let baseUrl = window.location.href.split('?')[0]; // Get base URL without query string permalink.href = baseUrl + queryString; @@ -173,7 +175,10 @@ document.addEventListener('DOMContentLoaded', function() { } function handleSynthesisResult(result, cached) { - const extraCachedString = result.fiat_crypto_version == fiat_crypto_version ? '' : ` in ${result.fiat_crypto_version}`; + const extraCachedString = [ + result.fiat_crypto_version == fiat_crypto_version ? '' : ` in ${result.fiat_crypto_version}`, + result.method === undefined ? '' : ` via ${result.method}`, + ].join(''); const cachedString = cached ? ` (cached on ${result.timestamp}${extraCachedString})` : ''; if (result.success) { clearOutput(); @@ -185,26 +190,31 @@ document.addEventListener('DOMContentLoaded', function() { } } - let synthesisWorker; + let fiatCryptoWorker; + let wasmFiatCryptoWorker; - function setupSynthesisWorker() { - synthesisWorker = new Worker("fiat_crypto_worker.js"); + function setupWorkers() { + fiatCryptoWorker = new Worker("fiat_crypto_worker.js"); + wasmFiatCryptoWorker = new Worker("wasm_fiat_crypto_worker.js"); - synthesisWorker.onmessage = function(e) { - console.log(`Early synthesis result: ${e.data}`); - }; + // Common setup for both workers + [fiatCryptoWorker, wasmFiatCryptoWorker].forEach(worker => { + worker.onmessage = function(e) { + console.log(`Early synthesis result: ${e.data}`); + }; - synthesisWorker.onerror = function(err) { - handleException(err); - }; + worker.onerror = function(err) { + handleException(err); + }; + }); } - function cancelSynthesisWorker() { - if (synthesisWorker) { - synthesisWorker.terminate(); - console.log("Synthesis worker terminated."); - } - setupSynthesisWorker(); // Re-setup the worker for future use + function cancelWorkers() { + [fiatCryptoWorker, wasmFiatCryptoWorker].forEach(worker => worker.terminate()); + console.log("Synthesis workers terminated."); + + // Re-setup workers + setupWorkers(); } // https://betterprogramming.pub/serializing-error-in-javascript-27c3a048dc3b @@ -239,6 +249,8 @@ document.addEventListener('DOMContentLoaded', function() { } } + const useWasm = wasmCheckbox.checked; + const recieveMessage = function (success) { return function(e) { const endTime = performance.now(); @@ -251,6 +263,7 @@ document.addEventListener('DOMContentLoaded', function() { timestamp: now.toISOString(), version: SYNTHESIS_CACHE_VERSION, fiat_crypto_version: fiat_crypto_version, + method: useWasm ? 'wasm_of_ocaml' : 'js_of_ocaml', }; try { localStorage.setItem(cacheKey, JSON.stringify(resultData, errorJSONReplacer)); @@ -261,9 +274,10 @@ document.addEventListener('DOMContentLoaded', function() { }; }; - synthesisWorker.postMessage(args); - synthesisWorker.onmessage = recieveMessage(true); - synthesisWorker.onerror = recieveMessage(false); + const currentWorker = useWasm ? wasmFiatCryptoWorker : fiatCryptoWorker; + currentWorker.postMessage(args); + currentWorker.onmessage = recieveMessage(true); + currentWorker.onerror = recieveMessage(false); } function parseAndRun(argv) { @@ -276,23 +290,36 @@ document.addEventListener('DOMContentLoaded', function() { } } - setupSynthesisWorker(); + function nonFalseQueryParam(value) { + return value !== null && value != 'false' && value != '0'; + } + + function parseQueryParams() { + const queryParams = new URLSearchParams(window.location.search); + const argv = queryParams.get('argv'); + const interactive = queryParams.get('interactive'); + const wasm = queryParams.get('wasm') - const queryParams = new URLSearchParams(window.location.search); - const argv = queryParams.get('argv'); - const interactive = queryParams.get('interactive'); + if (nonFalseQueryParam(wasm)) { + wasmCheckbox.checked = true; + } - if (argv) { - if (interactive !== null && interactive != 'false' && interactive != '0') { - inputArgs.value = decodeURIComponent(argv); - document.querySelector('input[value="json"]').checked = true; + if (argv) { + if (nonFalseQueryParam(interactive)) { + inputArgs.value = decodeURIComponent(argv); + document.querySelector('input[value="json"]').checked = true; + inputForm.classList.remove('hidden'); + } + parseAndRun(argv); + } else { inputForm.classList.remove('hidden'); } - parseAndRun(argv); - } else { - inputForm.classList.remove('hidden'); + + setupWorkers(); } + parseQueryParams(); + inputArgs.addEventListener('input', validateInput); document.querySelectorAll('input[name="inputType"]').forEach(radio => { @@ -331,7 +358,7 @@ document.addEventListener('DOMContentLoaded', function() { synthesizeButton.disabled = false; cancelButton.disabled = true; updateStatus(""); - cancelSynthesisWorker(); + cancelWorkers(); }); clearCacheButton.addEventListener('click', function() { From 0eb8dc859e8e0cc7b541b97e33d3c4478ae433b3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 22 Nov 2023 19:58:06 -0800 Subject: [PATCH 2/9] WIP inline wasm via promise --- fiat-html/fiat-crypto.html | 1 + fiat-html/main.js | 46 ++++++++++++++++++++++++++++++++------ 2 files changed, 40 insertions(+), 7 deletions(-) diff --git a/fiat-html/fiat-crypto.html b/fiat-html/fiat-crypto.html index 69b37b4842..1b3e7f74a6 100644 --- a/fiat-html/fiat-crypto.html +++ b/fiat-html/fiat-crypto.html @@ -71,6 +71,7 @@ + diff --git a/fiat-html/main.js b/fiat-html/main.js index 26cf6fd37a..5908ba7588 100644 --- a/fiat-html/main.js +++ b/fiat-html/main.js @@ -195,10 +195,10 @@ document.addEventListener('DOMContentLoaded', function() { function setupWorkers() { fiatCryptoWorker = new Worker("fiat_crypto_worker.js"); - wasmFiatCryptoWorker = new Worker("wasm_fiat_crypto_worker.js"); + //wasmFiatCryptoWorker = new Worker("wasm_fiat_crypto_worker.js"); // Common setup for both workers - [fiatCryptoWorker, wasmFiatCryptoWorker].forEach(worker => { + [fiatCryptoWorker/*, wasmFiatCryptoWorker*/].forEach(worker => { worker.onmessage = function(e) { console.log(`Early synthesis result: ${e.data}`); }; @@ -209,8 +209,10 @@ document.addEventListener('DOMContentLoaded', function() { }); } + let curSynthesisPromise; function cancelWorkers() { - [fiatCryptoWorker, wasmFiatCryptoWorker].forEach(worker => worker.terminate()); + [fiatCryptoWorker/*, wasmFiatCryptoWorker*/].forEach(worker => worker.terminate()); + curSynthesisPromise = null; console.log("Synthesis workers terminated."); // Re-setup workers @@ -231,6 +233,32 @@ document.addEventListener('DOMContentLoaded', function() { return value; } + function wasmSynthesize(args, onmessage, onerror) { + const synthesisPromise = new Promise((resolve, reject) => { + try { + resolve(synthesize(args)) + } catch (error) { + reject(error); + } + }); + curSynthesisPromise = synthesisPromise; + synthesisPromise + .then((value) => { + if (curSynthesisPromise === synthesisPromise) { + onmessage({data: {result: value}}); + } else { + console.log(`Synthesis of ${args} completed after being canceled: ${value}`); + } + }) + .catch((err) => { + if (curSynthesisPromise === synthesisPromise) { + onerror({data: err}); + } else { + console.log(`Synthesis of ${args} errored after being canceled: ${err}`); + } + }); + } + function handleSynthesis(args) { const startTime = performance.now(); const cacheKey = 'synthesize_' + JSON.stringify(args); @@ -274,10 +302,14 @@ document.addEventListener('DOMContentLoaded', function() { }; }; - const currentWorker = useWasm ? wasmFiatCryptoWorker : fiatCryptoWorker; - currentWorker.postMessage(args); - currentWorker.onmessage = recieveMessage(true); - currentWorker.onerror = recieveMessage(false); + if (useWasm) { + wasmSynthesize(args, recieveMessage(true), recieveMessage(false)); + } else { + const currentWorker = /*useWasm ? wasmFiatCryptoWorker :*/ fiatCryptoWorker; + currentWorker.postMessage(args); + currentWorker.onmessage = recieveMessage(true); + currentWorker.onerror = recieveMessage(false); + } } function parseAndRun(argv) { From 032340d5f251bb43566fd3e326435c8ab44c9203 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 22 Nov 2023 20:17:11 -0800 Subject: [PATCH 3/9] HACK setTimeout wasm --- fiat-html/main.js | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/fiat-html/main.js b/fiat-html/main.js index 5908ba7588..ae9082a0f6 100644 --- a/fiat-html/main.js +++ b/fiat-html/main.js @@ -342,7 +342,12 @@ document.addEventListener('DOMContentLoaded', function() { document.querySelector('input[value="json"]').checked = true; inputForm.classList.remove('hidden'); } - parseAndRun(argv); + // hack around synthesize not being ready :-( + if (wasmCheckbox.checked) { + setTimeout(function () { parseAndRun(argv); }, 1000); + } else { + parseAndRun(argv); + } } else { inputForm.classList.remove('hidden'); } From 0e737d9d5572a1805b57ef40d82b615ec5649319 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Nov 2023 12:04:07 -0800 Subject: [PATCH 4/9] Revert "HACK setTimeout wasm" This reverts commit 739dc5ad31d9ad99f9a5c5c1491a974792585733. --- fiat-html/main.js | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/fiat-html/main.js b/fiat-html/main.js index ae9082a0f6..5908ba7588 100644 --- a/fiat-html/main.js +++ b/fiat-html/main.js @@ -342,12 +342,7 @@ document.addEventListener('DOMContentLoaded', function() { document.querySelector('input[value="json"]').checked = true; inputForm.classList.remove('hidden'); } - // hack around synthesize not being ready :-( - if (wasmCheckbox.checked) { - setTimeout(function () { parseAndRun(argv); }, 1000); - } else { - parseAndRun(argv); - } + parseAndRun(argv); } else { inputForm.classList.remove('hidden'); } From a0d7954f8b6710f34ded97f47e1e4dd680c3e0f0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Nov 2023 12:04:12 -0800 Subject: [PATCH 5/9] Revert "WIP inline wasm via promise" This reverts commit fc02c0bfad6d09e88e325ce0b681f614920ad875. --- fiat-html/fiat-crypto.html | 1 - fiat-html/main.js | 46 ++++++-------------------------------- 2 files changed, 7 insertions(+), 40 deletions(-) diff --git a/fiat-html/fiat-crypto.html b/fiat-html/fiat-crypto.html index 1b3e7f74a6..69b37b4842 100644 --- a/fiat-html/fiat-crypto.html +++ b/fiat-html/fiat-crypto.html @@ -71,7 +71,6 @@ - diff --git a/fiat-html/main.js b/fiat-html/main.js index 5908ba7588..26cf6fd37a 100644 --- a/fiat-html/main.js +++ b/fiat-html/main.js @@ -195,10 +195,10 @@ document.addEventListener('DOMContentLoaded', function() { function setupWorkers() { fiatCryptoWorker = new Worker("fiat_crypto_worker.js"); - //wasmFiatCryptoWorker = new Worker("wasm_fiat_crypto_worker.js"); + wasmFiatCryptoWorker = new Worker("wasm_fiat_crypto_worker.js"); // Common setup for both workers - [fiatCryptoWorker/*, wasmFiatCryptoWorker*/].forEach(worker => { + [fiatCryptoWorker, wasmFiatCryptoWorker].forEach(worker => { worker.onmessage = function(e) { console.log(`Early synthesis result: ${e.data}`); }; @@ -209,10 +209,8 @@ document.addEventListener('DOMContentLoaded', function() { }); } - let curSynthesisPromise; function cancelWorkers() { - [fiatCryptoWorker/*, wasmFiatCryptoWorker*/].forEach(worker => worker.terminate()); - curSynthesisPromise = null; + [fiatCryptoWorker, wasmFiatCryptoWorker].forEach(worker => worker.terminate()); console.log("Synthesis workers terminated."); // Re-setup workers @@ -233,32 +231,6 @@ document.addEventListener('DOMContentLoaded', function() { return value; } - function wasmSynthesize(args, onmessage, onerror) { - const synthesisPromise = new Promise((resolve, reject) => { - try { - resolve(synthesize(args)) - } catch (error) { - reject(error); - } - }); - curSynthesisPromise = synthesisPromise; - synthesisPromise - .then((value) => { - if (curSynthesisPromise === synthesisPromise) { - onmessage({data: {result: value}}); - } else { - console.log(`Synthesis of ${args} completed after being canceled: ${value}`); - } - }) - .catch((err) => { - if (curSynthesisPromise === synthesisPromise) { - onerror({data: err}); - } else { - console.log(`Synthesis of ${args} errored after being canceled: ${err}`); - } - }); - } - function handleSynthesis(args) { const startTime = performance.now(); const cacheKey = 'synthesize_' + JSON.stringify(args); @@ -302,14 +274,10 @@ document.addEventListener('DOMContentLoaded', function() { }; }; - if (useWasm) { - wasmSynthesize(args, recieveMessage(true), recieveMessage(false)); - } else { - const currentWorker = /*useWasm ? wasmFiatCryptoWorker :*/ fiatCryptoWorker; - currentWorker.postMessage(args); - currentWorker.onmessage = recieveMessage(true); - currentWorker.onerror = recieveMessage(false); - } + const currentWorker = useWasm ? wasmFiatCryptoWorker : fiatCryptoWorker; + currentWorker.postMessage(args); + currentWorker.onmessage = recieveMessage(true); + currentWorker.onerror = recieveMessage(false); } function parseAndRun(argv) { From fef0885ebcdf64c2901544f58ac3dac462b1263b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Nov 2023 12:06:57 -0800 Subject: [PATCH 6/9] Work around asnyc wasm code cf https://github.com/ocaml-wasm/wasm_of_ocaml/issues/11 --- fiat-html/wasm_fiat_crypto_worker.js | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/fiat-html/wasm_fiat_crypto_worker.js b/fiat-html/wasm_fiat_crypto_worker.js index f596fc6aa6..1e0f747f2a 100644 --- a/fiat-html/wasm_fiat_crypto_worker.js +++ b/fiat-html/wasm_fiat_crypto_worker.js @@ -1,9 +1,15 @@ self.importScripts("wasm_fiat_crypto.js"); -self.onmessage = function(e) { - try { - const result = synthesize(e.data); - postMessage({result: result}); - } catch (err) { - postMessage({error: err}); - } -}; +let pending = []; +self.onmessage = function (e) { pending.push(e); }; +setTimeout(function () { + self.onmessage = function(e) { + try { + const result = synthesize(e.data); + postMessage({result: result}); + } catch (err) { + postMessage({error: err}); + } + }; + pending.forEach(e => { self.onmessage(e); }); + pending = []; +}, 1000); From 47586854c2e5436996564c4899813c477f70c4a0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Nov 2023 12:24:58 -0800 Subject: [PATCH 7/9] Add check for tail call support --- fiat-html/disable-wasm-option.js | 21 +++++++++++++++++++++ fiat-html/fiat-crypto.html | 16 +++++++++++----- 2 files changed, 32 insertions(+), 5 deletions(-) create mode 100644 fiat-html/disable-wasm-option.js diff --git a/fiat-html/disable-wasm-option.js b/fiat-html/disable-wasm-option.js new file mode 100644 index 0000000000..2c907f8a61 --- /dev/null +++ b/fiat-html/disable-wasm-option.js @@ -0,0 +1,21 @@ +document.addEventListener('DOMContentLoaded', async function() { + const wasmCheckbox = document.getElementById('wasm'); + const extraWasmLabel = document.getElementById('extraWasmLabel'); + wasmCheckbox.disabled = true; // Initially disable the checkbox + + try { + if (await wasmFeatureDetect.tailCall()) { + wasmCheckbox.disabled = false; // Re-enable the checkbox if tail calls are supported + } else { + wasmCheckbox.checked = false; + + if (navigator.userAgent.includes('Firefox')) { + extraWasmLabel.innerHTML = '(enable javascript.options.wasm_tail_calls in about:config)'; + } else { + extraWasmLabel.innerHTML = '(wasm tail calls not supported)'; + } + } + } catch (error) { + console.error('Error checking wasm tail call support:', error); + } +}); diff --git a/fiat-html/fiat-crypto.html b/fiat-html/fiat-crypto.html index 69b37b4842..425c68af41 100644 --- a/fiat-html/fiat-crypto.html +++ b/fiat-html/fiat-crypto.html @@ -5,7 +5,7 @@ Fiat Cryptography Web Interface