Add three Faultless completeness examples

README.md

@@ -13,7 +13,7 @@ fullWidth: true
 Public Gradio frontend for comparing a binary function with candidate C. Select
 an example or upload an ELF x86-64 binary, supply its function address and candidate
 source, and stream verification results with assembly previews and a JSON download.
-The application includes 60 examples in expandable sections: Basics, Calls and
+The application includes 63 examples in expandable sections: Basics, Calls and
 memory, Types and ABI, Real binaries, Related work, and Ghidra exports. Each section
 has a short description with relevant paper or tool links. Basics starts open;
 expand any other section to browse its examples.
@@ -117,9 +117,12 @@ to clone private code before the Docker build. Local developers use the explicit
 Startup retains the pinned private core checkout in `core/` after removing its Git
 metadata. The UI reads example sources from that checkout and compiles originals
 when preparing examples. Local development uses the same loader and submodule.
-The Related work section combines six Faultless cases with nine cases from D-Helix,
+The Related work section combines nine Faultless cases with nine cases from D-Helix,
 DiscScope, and Decompile-Diverge, including a deliberately uncompilable export. See `core/docs/related-work-examples.md`
 for provenance, interface adaptations, and published counterexamples.
+The three O0 completeness pairs (`my_putchar_count`, `upper`, and `print_page_header`)
+are stored in `demo/cases/`, including raw exports, source metadata, and documented
+runnable adaptations in [demo/cases/README.md](demo/cases/README.md).
 Reference C is a display aid; uploaded binaries have none. DiscScope `orig.c`
 excerpts are stored alongside their `raw.c` and `cand.c` in the shared core cases.
 They come from binutils 2.29, libsmi 0.4.8, and JasPer 1.900.16, with source

demo/cases/README.md

@@ -0,0 +1,36 @@
+# Faultless examples
+
+Original/decompiled pairs extracted verbatim from the O0 completeness dataset. Decompiled files retain decompiler syntax and are not standalone compilation units.
+
+- `my_putchar_count` (Ismuur/Magic): Faultless treats the entire decompiled buffer as involved in write, although write consumes only the first byte (count = 1). Equivalence depends on modeling the callee behavior.
+- `upper` (aaronokano/ecs150-hw1): The decompiled loop exits through an early break; Faultless loop pairing can be brittle around breaks.
+- `print_page_header` (achasse/cse220): The original uses a static local integer, represented as a global in the decompiled code; Faultless has difficulty with static integers.
+
+The three directories preserve `original.c`, `decompiled.c`, and `metadata.json`
+from `/tmp/decompile-verify-faultless-examples` unchanged. The metadata records
+the dataset index, canonical function name, source repository, and Faultless's
+reported failure. That failure is distinct from this verifier's result.
+
+`candidate.c` is the runnable version. It adds standard headers and removes the
+decompiler's `__fastcall` spelling. `my_putchar_count` restores the original
+32-bit return type. `upper` restores the original void return and writable
+`char *` parameter, retaining the early break and repeated `strlen` calls.
+`print_page_header` restores the void return while retaining the increment,
+and declares the exported counter as an external integer. The original static
+local remains intact; its `page_number.0` symbol supplies the global binding.
+These examples compare behavior under the original interfaces, including these
+documented corrections to the inferred signatures.
+
+`runnable.json` records declarations, original and candidate symbols, callee and
+global bindings, and interfaces. Originals are compiled with GCC at `-O0` and
+`-fno-builtin`. Linker stubs resolve `write`, `strlen`, and `printf`; the verifier
+intercepts them with shared synthetic responses. The stubs do not model libc.
+The `write` interface explicitly compares one byte of its second argument;
+`printf` specifies its four variadic argument types.
+
+The one-byte write can remain inconclusive because this verifier requires the
+whole escaped stack frame to agree even with an explicit one-byte range.
+The uppercase loop uses synthetic `strlen` responses, so budget exhaustion is
+possible; it does not demonstrate real libc string handling or loop equivalence.
+Agreement for the page header covers the bound counter and intercepted `printf`
+arguments on tested inputs.

demo/cases/my_putchar_count/candidate.c

@@ -0,0 +1,10 @@
+#include <unistd.h>
+
+int func0(char a1)
+{
+char buf[4]; // [rsp+Ch] [rbp-4h] BYREF
+
+buf[0] = a1;
+write(1, buf, 1uLL);
+return 1LL;
+}

demo/cases/my_putchar_count/decompiled.c

@@ -0,0 +1,8 @@
+__int64 __fastcall func0(char a1)
+{
+char buf[4]; // [rsp+Ch] [rbp-4h] BYREF
+
+buf[0] = a1;
+write(1, buf, 1uLL);
+return 1LL;
+}

demo/cases/my_putchar_count/metadata.json

@@ -0,0 +1,10 @@
+{
+  "repo": "Ismuur/Magic",
+  "name": "my_putchar_count",
+  "index": 74,
+  "canonical_name": "func0",
+  "status": "failure",
+  "nonequivalence_reason": "Function write in the original function has no equivalent in the decompiled function.",
+  "source_report": "O0_opt_parity_test/report.md",
+  "note": "Faultless treats the entire decompiled buffer as involved in write, although write consumes only the first byte (count = 1). Equivalence depends on modeling the callee behavior."
+}

demo/cases/my_putchar_count/original.c

@@ -0,0 +1,5 @@
+int my_putchar_count(char c)
+{
+  write(1, &c, 1);
+  return (1);
+}

demo/cases/my_putchar_count/runnable.json

@@ -0,0 +1,17 @@
+{
+  "original_symbol": "my_putchar_count",
+  "candidate_symbol": "func0",
+  "declarations": "#include <unistd.h>\n",
+  "stubs": "#include <unistd.h>\nssize_t write(int fd, const void *buffer, size_t count) { return 0; }\n",
+  "callees": {
+    "write": "write"
+  },
+  "interfaces": {
+    "original_prototype": "int my_putchar_count(char c);",
+    "memory_ranges": {
+      "write": {
+        "1": 1
+      }
+    }
+  }
+}

demo/cases/print_page_header/candidate.c

@@ -0,0 +1,8 @@
+#include <stdio.h>
+extern int page_number_0;
+
+void func9(const char *a1, const char *a2)
+{
+printf("Page %3d %*s\t %s\t \n", (unsigned int)page_number_0, 26, a1, a2);
+++page_number_0;
+}

demo/cases/print_page_header/decompiled.c

@@ -0,0 +1,5 @@
+__int64 __fastcall func9(const char *a1, const char *a2)
+{
+printf("Page %3d %*s\t %s\t \n", (unsigned int)page_number_0, 26, a1, a2);
+return (unsigned int)++page_number_0;
+}

demo/cases/print_page_header/metadata.json

@@ -0,0 +1,10 @@
+{
+  "repo": "achasse/cse220",
+  "name": "print_page_header",
+  "index": 194,
+  "canonical_name": "func9",
+  "status": "failure",
+  "nonequivalence_reason": "Function printf in the original function has no equivalent in the decompiled function.",
+  "source_report": "O0_opt_parity_test/report.md",
+  "note": "The original uses a static local integer, represented as a global in the decompiled code; Faultless has difficulty with static integers."
+}

demo/cases/print_page_header/original.c

@@ -0,0 +1,6 @@
+static void print_page_header(char source_name[], char date[])
+{
+ static int page_number = 0;
+ printf("Page %3d %*s\t %s\t \n", page_number, 80/3, source_name, date);
+ page_number++;
+}

demo/cases/print_page_header/runnable.json

@@ -0,0 +1,25 @@
+{
+  "original_symbol": "print_page_header",
+  "candidate_symbol": "func9",
+  "declarations": "#include <stdio.h>\n",
+  "stubs": "int printf(const char *format, ...) { return 0; }\n",
+  "callees": {
+    "printf": "printf"
+  },
+  "globals": {
+    "page_number_0": "page_number.0"
+  },
+  "interfaces": {
+    "original_prototype": "void print_page_header(char *source_name, char *date);",
+    "callee_interfaces": {
+      "printf": {
+        "variadic_types": [
+          "int",
+          "int",
+          "char *",
+          "char *"
+        ]
+      }
+    }
+  }
+}

demo/cases/upper/candidate.c

@@ -0,0 +1,17 @@
+#include <string.h>
+
+void func8(char *a1)
+{
+size_t result; // rax
+int i; // [rsp+1Ch] [rbp-14h]
+
+for ( i = 0; ; ++i )
+{
+result = strlen(a1);
+if ( i >= result )
+break;
+if ( a1[i] > 96 && a1[i] <= 122 )
+a1[i] -= 32;
+}
+return;
+}

demo/cases/upper/decompiled.c

@@ -0,0 +1,15 @@
+size_t __fastcall func8(const char *a1)
+{
+size_t result; // rax
+int i; // [rsp+1Ch] [rbp-14h]
+
+for ( i = 0; ; ++i )
+{
+result = strlen(a1);
+if ( i >= result )
+break;
+if ( a1[i] > 96 && a1[i] <= 122 )
+a1[i] -= 32;
+}
+return result;
+}

demo/cases/upper/metadata.json

@@ -0,0 +1,10 @@
+{
+  "repo": "aaronokano/ecs150-hw1",
+  "name": "upper",
+  "index": 188,
+  "canonical_name": "func8",
+  "status": "failure",
+  "nonequivalence_reason": "Function strlen in the original function has no equivalent in the decompiled function.",
+  "source_report": "O0_opt_parity_test/report.md",
+  "note": "The decompiled loop exits through an early break; Faultless loop pairing can be brittle around breaks."
+}

demo/cases/upper/original.c

@@ -0,0 +1,7 @@
+void upper(char *mystring) {
+  int i; int diff = 'a' - 'A';
+  for( i = 0; i < strlen( mystring ); i++ ) {
+    if( mystring[i] >= 'a' && mystring[i] <= 'z' )
+      mystring[i] -= diff;
+  }
+}

demo/cases/upper/runnable.json

@@ -0,0 +1,12 @@
+{
+  "original_symbol": "upper",
+  "candidate_symbol": "func8",
+  "declarations": "#include <string.h>\n",
+  "stubs": "#include <stddef.h>\nsize_t strlen(const char *s) { return 0; }\n",
+  "callees": {
+    "strlen": "strlen"
+  },
+  "interfaces": {
+    "original_prototype": "void upper(char *mystring);"
+  }
+}

demo/examples.py

@@ -1,4 +1,4 @@
-"""Use the same example sources and preparation as the core tests."""
+"""Combine shared core examples with saved frontend completeness pairs."""
 from pathlib import Path
 import sys
 import json
@@ -6,13 +6,21 @@ import json
 ROOT = Path(__file__).resolve().parents[1]
 sys.path.insert(0, str(ROOT / "core"))
 
-from examples.ui import (EXAMPLE_NAMES, EXAMPLE_LABELS, ORIGINAL_EXAMPLE_NAMES,
-    ORIGINAL_EXAMPLE_LABELS, GHIDRA_EXAMPLE_NAMES,
-    ghidra_metadata)
+from examples.ui import GHIDRA_EXAMPLE_NAMES, ghidra_metadata
 from examples import ui as core_examples
+from demo import faultless
+
+ORIGINAL_EXAMPLE_NAMES = core_examples.ORIGINAL_EXAMPLE_NAMES + faultless.NAMES
+ORIGINAL_EXAMPLE_LABELS = core_examples.ORIGINAL_EXAMPLE_LABELS + faultless.LABELS
+EXAMPLE_NAMES = ORIGINAL_EXAMPLE_NAMES + GHIDRA_EXAMPLE_NAMES
+EXAMPLE_LABELS = ORIGINAL_EXAMPLE_LABELS + tuple(
+    core_examples.EXAMPLE_LABELS[core_examples.EXAMPLE_NAMES.index(name)]
+    for name in GHIDRA_EXAMPLE_NAMES)
 
 
 def example_metadata(name):
+    if name in faultless.NAMES:
+        return faultless.metadata(name)
     metadata = core_examples.example_metadata(name)
     if name == "faultless-linked-list":
         metadata["expected_verdict"] = "mismatch"
@@ -34,6 +42,7 @@ def expected_result(name, compiler="gcc"):
 
 def prepare_examples(directory, *, include_ghidra=True):
     rows = dict(zip(core_examples.EXAMPLE_NAMES, core_examples.prepare_examples(directory)))
+    rows.update(zip(faultless.NAMES, faultless.prepare_examples(directory)))
     names = EXAMPLE_NAMES if include_ghidra else tuple(
         name for name in EXAMPLE_NAMES if name not in GHIDRA_EXAMPLE_NAMES)
     selected = [rows[name] for name in names]
@@ -50,7 +59,7 @@ EXAMPLE_GROUPS = (
     ("Types and ABI", ("wide-integer", "float-identity", "signed-zero", "nan-payload",
                       "struct-fields", "struct-indirect", "struct-padding", "pointer-identity")),
     ("Real binaries", ("factor-gcd", "factor-gcd-euclidean", "factor-gcd-even")),
-    ("Related work", core_examples.FAULTLESS_NAMES + core_examples.RESEARCH_NAMES),
+    ("Related work", core_examples.FAULTLESS_NAMES + core_examples.RESEARCH_NAMES + faultless.NAMES),
     ("Ghidra exports", GHIDRA_EXAMPLE_NAMES),
 )
 

demo/faultless.py

@@ -0,0 +1,57 @@
+"""Saved O0 completeness pairs, with explicit runnable interface adaptations."""
+import json
+from pathlib import Path
+import subprocess
+import tempfile
+
+import cle
+import yaml
+
+
+CASES = Path(__file__).with_name("cases")
+NAMES = ("faultless-my-putchar-count", "faultless-upper", "faultless-print-page-header")
+CASE_NAMES = ("my_putchar_count", "upper", "print_page_header")
+LABELS = ("Faultless: One-byte write", "Faultless: Uppercase loop",
+          "Faultless: Static page counter")
+
+
+def source(name, filename):
+    return (CASES / CASE_NAMES[NAMES.index(name)] / filename).read_text()
+
+
+def metadata(name):
+    info = json.loads(source(name, "metadata.json"))
+    info.update(reference=source(name, "original.c"),
+                expected_verdict="inconclusive" if name == NAMES[0] else "agree")
+    return info
+
+
+def prepare_examples(directory):
+    output = Path(directory).resolve()
+    output.mkdir(parents=True, exist_ok=True)
+    rows = []
+    with tempfile.TemporaryDirectory(prefix="faultless-completeness-") as temporary:
+        temporary = Path(temporary)
+        for name in NAMES:
+            case = CASES / CASE_NAMES[NAMES.index(name)]
+            info = json.loads((case / "runnable.json").read_text())
+            original = temporary / "original.c"
+            original.write_text(info["declarations"] + source(name, "original.c"))
+            stubs = temporary / "callees.c"
+            stubs.write_text(info["stubs"])
+            binary = output / (name + ".elf")
+            flags = ["-O0", "-fno-builtin"]
+            subprocess.run(["gcc", *flags, "-fno-pie", "-no-pie", "-fno-stack-protector",
+                            "-nostdlib", "-Wl,--build-id=none", "-Wl,-e," + info["original_symbol"],
+                            str(original), str(stubs), "-o", str(binary)],
+                           check=True, capture_output=True, text=True, timeout=60)
+            obj = cle.Loader(str(binary), auto_load_libs=False).main_object
+            addresses = {symbol.name: symbol.rebased_addr for symbol in obj.symbols
+                         if not symbol.is_import}
+            bindings = {kind: {candidate: addresses[original] for candidate, original in
+                              info.get(kind, {}).items()} for kind in ("callees", "globals")}
+            rows.append([str(binary), f"{addresses[info['original_symbol']]:#x}",
+                         (case / "candidate.c").read_text(), yaml.safe_dump(bindings, sort_keys=True),
+                         info["candidate_symbol"], 100, "0", 1000, "gcc", " ".join(flags),
+                         yaml.safe_dump(info["interfaces"], sort_keys=True)])
+    return rows

tests/test_examples.py

@@ -5,7 +5,7 @@ from demo import examples
 
 def test_examples_prepare_from_core_checkout(tmp_path):
     rows = examples.prepare_examples(tmp_path)
-    assert len(rows) == len(examples.EXAMPLE_NAMES) == 60
+    assert len(rows) == len(examples.EXAMPLE_NAMES) == 63
     assert len(examples.GHIDRA_EXAMPLE_NAMES) == 21
     assert all(Path(row[0]).is_file() for row in rows)
     assert all(Path(row[0]).is_relative_to(tmp_path) for row in rows)
@@ -18,7 +18,7 @@ def test_example_groups_cover_catalog_once():
     assert len(members) == len(set(members)) == len(examples.EXAMPLE_NAMES)
     assert set(members) == set(examples.EXAMPLE_NAMES)
     groups = examples.example_groups(examples.EXAMPLE_NAMES)
-    assert [len(indices) for _, indices in groups] == [6, 7, 8, 3, 15, 21]
+    assert [len(indices) for _, indices in groups] == [6, 7, 8, 3, 18, 21]
     for _, indices in groups:
         assert list(indices) == sorted(indices)
 

tests/test_faultless.py

@@ -5,6 +5,7 @@ import pytest
 
 from demo.app import run_verification
 from demo.examples import EXAMPLE_NAMES, example_metadata
+from demo.faultless import NAMES as COMPLETENESS_NAMES
 
 
 @pytest.mark.parametrize('compiler', ['gcc', 'clang'])
@@ -37,6 +38,10 @@ def test_faultless_frontend_stream(tmp_path, compiler, name, example_rows):
         assert report['counts']['agree'] == seed_count
     elif name == 'faultless-byte-reinterpretation':
         assert report['counts'][expected] == seed_count
+    elif name in COMPLETENESS_NAMES:
+        assert report['counts'][expected] == seed_count
+        if name == 'faultless-my-putchar-count':
+            assert all(r['reason'] == 'escaped_frame_differs' for r in report['results'])
     else:
         assert report['counts']['mismatch'] == seed_count
         assert all(r['divergence'] == 'call[0]' for r in report['results'])

tests/test_ui.py

@@ -10,6 +10,7 @@ from urllib.parse import quote
 
 from demo.examples import (EXAMPLE_NAMES, EXAMPLE_LABELS, ORIGINAL_EXAMPLE_NAMES,
                            GHIDRA_EXAMPLE_NAMES, ROOT, ghidra_metadata)
+from demo.faultless import NAMES as COMPLETENESS_NAMES
 from demo.presentation import json_detail, mismatch_summary
 from tests.support import check_report
 
@@ -102,8 +103,8 @@ def test_example_reference_pane_events(tmp_path):
         app.close()
 
 
-@pytest.mark.parametrize("names", [ORIGINAL_EXAMPLE_NAMES, GHIDRA_EXAMPLE_NAMES],
-                         ids=["original", "ghidra"])
+@pytest.mark.parametrize("names", [ORIGINAL_EXAMPLE_NAMES, GHIDRA_EXAMPLE_NAMES, COMPLETENESS_NAMES],
+                         ids=["original", "ghidra", "faultless-completeness"])
 def test_queued_ui_upload_streaming_and_download(tmp_path, monkeypatch, names):
     from gradio_client import Client, handle_file
     from gradio_client.exceptions import AppError