Make the web page's argv string encoding a faithful round trip

Fixes scrutineer finding #2519.

In fiat-html/main.js, splitUnescapedSpaces and joinWithEscaping convert
between the "Input String" text box and the argv array passed to the
worker.  The decoder used U+0000 and U+0001 as internal placeholders and
dropped empty strings, so `splitUnescapedSpaces(joinWithEscaping(a))` was
not `a` for arguments containing those characters or for empty arguments.
When the page was opened via a crafted `?argv=...&interactive` link, the
text box was filled with the lossy re-encoding while synthesis ran on the
original argv, so the visitor saw one command line and ran another.

Rewrite the decoder as a character-by-character parser with no
placeholder characters.  `\ ` and `\\` keep their meaning, `\"` is a
literal quote, and a bare `""` token is the empty argument; any other
backslash is kept literally, as before.  The encoder emits `""` for an
empty argument and escapes the quotes of an argument that is literally
`""`.  With the pair an exact inverse, the displayed string always decodes
to the argv that ran.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016Rbn2gww3MGhvrh52fNjpD

Author: JasonGross

fiat-html/main.js

@@ -20,23 +20,40 @@ document.addEventListener('DOMContentLoaded', function () {
     const isSafari = /^((?!chrome|android).)*safari/i.test(navigator.userAgent);
     const isMacOrIOS = /Macintosh|MacIntel|MacPPC|Mac68K|iPhone|iPad|iPod/.test(navigator.platform);
 
+    // Format of the "Input String" text box: arguments are separated by
+    // unescaped spaces; `\ ` is a literal space, `\\` a literal backslash,
+    // `\"` a literal double quote, and a bare `""` token is an empty argument.
+    // Any other backslash is kept literally.  splitUnescapedSpaces and
+    // joinWithEscaping must be exact inverses of each other, so that the
+    // command line shown in the box is the one that actually runs.
     function splitUnescapedSpaces(input) {
-        return input
-            .replace(/\\\\/g, '\u0000')  // Temporarily replace \\ with a placeholder
-            .replace(/\\ /g, '\u0001')  // Temporarily replace escaped spaces with a placeholder
-            .split(/ +/)               // Split by spaces
-            .filter(s => s)
-            .map(s => s
-                .replace(/\u0000/g, '\\')  // Restore backslashes
-                .replace(/\u0001/g, ' ')   // Restore spaces
-            );
+        const args = [];
+        let current = null;  // null between arguments
+        for (let i = 0; i < input.length; i++) {
+            const c = input[i], next = input[i + 1];
+            if (c === ' ') {
+                if (current !== null) args.push(current);
+                current = null;
+            } else if (c === '\\' && (next === ' ' || next === '\\' || next === '"')) {
+                current = (current || '') + next;
+                i++;
+            } else if (c === '"' && current === null && next === '"' && (i + 2 >= input.length || input[i + 2] === ' ')) {
+                args.push('');
+                i++;
+            } else {
+                current = (current || '') + c;
+            }
+        }
+        if (current !== null) args.push(current);
+        return args;
     }
 
     function joinWithEscaping(inputArray) {
         return inputArray
-            .map(s => s
+            .map(s => s === '' ? '""' : s
                 .replace(/\\/g, '\\\\')  // Escape backslashes
                 .replace(/ /g, '\\ ')   // Escape spaces
+                .replace(/^""$/, '\\"\\"')  // A literal "" must not read as the empty argument
             )
             .join(' ');
     }