[GH-ISSUE #7414] [Bug] analyze-javascript-application omits the predicate of a labelled-block break from Electron paths #4422

Closed
opened 2026-10-31 00:49:39 +00:00 by bsakaguchi · 0 comments
Owner

Originally created by @coygeek on GitHub (Oct 27, 2026).
Original GitHub issue: https://github.com/morluto/rea/issues/7414

Before submitting

  • I searched the open and closed issues for a related report.
  • I removed credentials, tokens, private paths, and sensitive target data.

Area

Evidence, artifacts, or reconstruction

Observed behavior

An Electron preload exposes api.ping after if (!ready) break guard; inside the enclosing labelled block. The public CLI recovers that bridge member and its IPC call, but both trace-electron-wrapper-path edges have an empty conditions array. Their Evidence and the application graph report complete coverage. A comparison using a function-local conditional return retains !(!ready) and partial coverage. Both results remain static candidates; neither result establishes runtime execution.

Reproduction

  1. Use the prepared source revision below with its locked dependencies and compiled runtime. Put an empty working directory beside that checkout, accessible from the working directory as ../rea. Use Node 24.22.1 on PATH. No Electron installation or running application is needed.
  2. From the empty working directory, run this exact fixture and CLI program. It redirects HOME, creates two identical labelled-break inputs plus a return control, and analyzes their source without executing it.
python3 - <<'PY'
import json
import os
import subprocess
from pathlib import Path

home = Path('home')
home.mkdir()
env = dict(os.environ, HOME=str(home.resolve()))
main = '''const { BrowserWindow, ipcMain } = require("electron");
ipcMain.handle("ping", () => "pong");
new BrowserWindow({ webPreferences: { preload: "preload.js" } });
'''
imports = '''const { contextBridge, ipcRenderer } = require("electron");
const ready = process.env.APP_READY;
'''
expose = '  contextBridge.exposeInMainWorld("api", { ping: () => ipcRenderer.invoke("ping") });\n'
for name in ('break', 'break-repeat', 'return'):
    app = Path(name)
    app.mkdir()
    (app / 'package.json').write_text('{"name":"guard-probe","version":"1.0.0","main":"main.js"}\n')
    (app / 'main.js').write_text(main)
    body = ('function initialize() {\n  if (!ready) return;\n' + expose + '}\ninitialize();\n'
            if name == 'return' else 'guard: {\n  if (!ready) break guard;\n' + expose + '}\n')
    (app / 'preload.js').write_text(imports + body)
    evidence = name + '.evidence.json'
    command = ['node', '../rea/scripts/rea.mjs', 'analyze-javascript-application', './' + name,
               '--detail', 'summary', '--evidence_output', evidence, '--format', 'json']
    run = subprocess.run(command, env=env, capture_output=True, text=True, check=True)
    Path(name + '.stdout.json').write_text(run.stdout)
    Path(name + '.stderr.txt').write_text(run.stderr)
    graph = json.loads(Path(evidence).read_text())['records'][0]['normalized_result']['graph']
    rows = sorted((edge['relation'], [c['expression'] for c in edge['properties']['conditions']])
                  for edge in graph['edges']
                  if edge['evidence']['extractor']['operation'] == 'trace-electron-wrapper-path')
    print(json.dumps({'fixture': name, 'exit': run.returncode,
                      'path_conditions': rows, 'application_coverage': graph['coverage']['status']}))
PY
  1. Compare the actual output below. Both labelled-break analyses omitted the predicate: 2 failures in 2 attempts. The return control retained it in its single analysis. All three CLI invocations exited successfully.
{"fixture": "break", "exit": 0, "path_conditions": [["calls", []], ["maps_to", []]], "application_coverage": "complete"}
{"fixture": "break-repeat", "exit": 0, "path_conditions": [["calls", []], ["maps_to", []]], "application_coverage": "complete"}
{"fixture": "return", "exit": 0, "path_conditions": [["calls", ["!(!ready)"]], ["maps_to", ["!(!ready)"]]], "application_coverage": "partial"}

Expected behavior

The reconstruction guide, docs/javascript-artifact-reconstruction.md, under “Authority and unknowns” at lines 539–541, states: “Recovered Electron paths retain source ranges, module identities, literal channels and branch conditions as static candidates.” The later exposure in this labelled block can only be reached along the continuing side of if (!ready). Its recovered path should retain an equivalent continuing-path predicate, as the return control does, or explicitly identify that this control flow remains unresolved.

The guide does not explicitly list labelled break as supported condition syntax. Applying its general predicate-retention contract here is an inference supported by the observed return comparison and existing ordinary-source early-return acceptance coverage. This expectation does not require complete JavaScript control-flow modeling or proof that a runtime guard passes; it requires keeping this candidate's omitted condition or its unresolved status visible.

Impact and scope

Both labelled-break inputs in the reproduction lose a source predicate from the reconstructed api.ping path. Inspecting the path's empty condition list does not reveal this guard. The API and IPC candidates remain available, and the command succeeds. Only this labelled-block shape was independently reproduced; continue, other break targets, loop guards, real-application frequency, and downstream tracing consequences are unmeasured. No supported option restoring the condition from the unchanged input was verified. The return comparison changes the source and is a control rather than a demonstrated workaround.

REA version

6.8.0 (source commit a905a71e31)

Runtime and platform

Node 24.22.1; macOS 27.0.1 arm64

Target and artifact context

Authored extracted CommonJS application directories containing a package manifest, Electron main source, and preload source. REA reads them as inert text; no live provider or target process is involved.

Interface

CLI

Earliest failure stage

Native analysis or reconstruction

Relevant output or evidence

The JSONL above is observed output from the executed public CLI reproduction. Inspection of complete retained Evidence also found conditions: [] on the api.ping terminal candidate and complete coverage on its path edges for the labelled-break input. The same candidate remains resolution: "candidate" with runtime limitations. Application coverage is separate from semantic-graph coverage, which remains unknown; the complete application graph is not proof of complete runtime semantics.

Source-only explanation, not runtime instrumentation: src/domain/javascript/electronCallPathBlockPrefixes.ts:42 classifies a preceding statement through symbolicDefiniteExit, and its branch-arm checks at lines 50–51 use the same helper. src/domain/javascript/javascriptSymbolicControlFlow.ts:62 recognizes definite return/throw exits and recursively handles blocks and both-exiting if branches; it does not recognize labelled breaks. src/domain/javascript/electronWrappedCallPaths.ts:292 retains a continuing-path predicate only when its statement fact identifies an exiting arm. Its seed-prefix replay at line 1253 therefore receives no exiting arm for this break guard. src/application/javascript/ElectronBoundaryGraphCallPaths.ts:64 copies the already-recovered path conditions to graph observations. The existing acceptance case at tests/boundary/cli/electronWrappedCallPaths.test.ts:246 covers ordinary-source conditional returns and their partial coverage; it was inspected, not executed in this verification.

Typed outcome or recovery expected

For the labelled-break input, preserve a condition equivalent to !(!ready) with its source range on the recovered api.ping candidate and associated path edges. If this syntax is intentionally outside the model, retain an explicit unresolved-control-flow qualification rather than silently losing the predicate. Keep static-candidate authority and runtime limitations, and preserve the working return control.

Analysis or suspected cause

The observed differential is consistent with a block-prefix exit-classification gap. A labelled break exits the specific enclosing labelled statement, while a return exits a function. That distinction needs to remain intact: classifying every nested break as a function exit would be unsound for statements reached after an inner switch or block. This is a source-derived diagnosis of the tested shape, not a proposed implementation or a claim about untested control flow.

Additional context

Related (closed):

The npm registry reported 6.8.0 as the latest published version during verification. This report executed the assigned source checkout and its prepared runtime, not a separately installed npm package. Nothing was published during verification.

Originally created by @coygeek on GitHub (Oct 27, 2026). Original GitHub issue: https://github.com/morluto/rea/issues/7414 ### Before submitting - [x] I searched the open and closed issues for a related report. - [x] I removed credentials, tokens, private paths, and sensitive target data. ### Area Evidence, artifacts, or reconstruction ### Observed behavior An Electron preload exposes `api.ping` after `if (!ready) break guard;` inside the enclosing labelled block. The public CLI recovers that bridge member and its IPC call, but both `trace-electron-wrapper-path` edges have an empty `conditions` array. Their Evidence and the application graph report complete coverage. A comparison using a function-local conditional `return` retains `!(!ready)` and partial coverage. Both results remain static candidates; neither result establishes runtime execution. ### Reproduction 1. Use the prepared source revision below with its locked dependencies and compiled runtime. Put an empty working directory beside that checkout, accessible from the working directory as `../rea`. Use Node 24.22.1 on PATH. No Electron installation or running application is needed. 2. From the empty working directory, run this exact fixture and CLI program. It redirects HOME, creates two identical labelled-break inputs plus a return control, and analyzes their source without executing it. ```sh python3 - <<'PY' import json import os import subprocess from pathlib import Path home = Path('home') home.mkdir() env = dict(os.environ, HOME=str(home.resolve())) main = '''const { BrowserWindow, ipcMain } = require("electron"); ipcMain.handle("ping", () => "pong"); new BrowserWindow({ webPreferences: { preload: "preload.js" } }); ''' imports = '''const { contextBridge, ipcRenderer } = require("electron"); const ready = process.env.APP_READY; ''' expose = ' contextBridge.exposeInMainWorld("api", { ping: () => ipcRenderer.invoke("ping") });\n' for name in ('break', 'break-repeat', 'return'): app = Path(name) app.mkdir() (app / 'package.json').write_text('{"name":"guard-probe","version":"1.0.0","main":"main.js"}\n') (app / 'main.js').write_text(main) body = ('function initialize() {\n if (!ready) return;\n' + expose + '}\ninitialize();\n' if name == 'return' else 'guard: {\n if (!ready) break guard;\n' + expose + '}\n') (app / 'preload.js').write_text(imports + body) evidence = name + '.evidence.json' command = ['node', '../rea/scripts/rea.mjs', 'analyze-javascript-application', './' + name, '--detail', 'summary', '--evidence_output', evidence, '--format', 'json'] run = subprocess.run(command, env=env, capture_output=True, text=True, check=True) Path(name + '.stdout.json').write_text(run.stdout) Path(name + '.stderr.txt').write_text(run.stderr) graph = json.loads(Path(evidence).read_text())['records'][0]['normalized_result']['graph'] rows = sorted((edge['relation'], [c['expression'] for c in edge['properties']['conditions']]) for edge in graph['edges'] if edge['evidence']['extractor']['operation'] == 'trace-electron-wrapper-path') print(json.dumps({'fixture': name, 'exit': run.returncode, 'path_conditions': rows, 'application_coverage': graph['coverage']['status']})) PY ``` 3. Compare the actual output below. Both labelled-break analyses omitted the predicate: 2 failures in 2 attempts. The return control retained it in its single analysis. All three CLI invocations exited successfully. ```jsonl {"fixture": "break", "exit": 0, "path_conditions": [["calls", []], ["maps_to", []]], "application_coverage": "complete"} {"fixture": "break-repeat", "exit": 0, "path_conditions": [["calls", []], ["maps_to", []]], "application_coverage": "complete"} {"fixture": "return", "exit": 0, "path_conditions": [["calls", ["!(!ready)"]], ["maps_to", ["!(!ready)"]]], "application_coverage": "partial"} ``` ### Expected behavior The reconstruction guide, `docs/javascript-artifact-reconstruction.md`, under “Authority and unknowns” at lines 539–541, states: “Recovered Electron paths retain source ranges, module identities, literal channels and branch conditions as static candidates.” The later exposure in this labelled block can only be reached along the continuing side of `if (!ready)`. Its recovered path should retain an equivalent continuing-path predicate, as the return control does, or explicitly identify that this control flow remains unresolved. The guide does not explicitly list labelled `break` as supported condition syntax. Applying its general predicate-retention contract here is an inference supported by the observed return comparison and existing ordinary-source early-return acceptance coverage. This expectation does not require complete JavaScript control-flow modeling or proof that a runtime guard passes; it requires keeping this candidate's omitted condition or its unresolved status visible. ### Impact and scope Both labelled-break inputs in the reproduction lose a source predicate from the reconstructed `api.ping` path. Inspecting the path's empty condition list does not reveal this guard. The API and IPC candidates remain available, and the command succeeds. Only this labelled-block shape was independently reproduced; `continue`, other break targets, loop guards, real-application frequency, and downstream tracing consequences are unmeasured. No supported option restoring the condition from the unchanged input was verified. The return comparison changes the source and is a control rather than a demonstrated workaround. ### REA version 6.8.0 (source commit a905a71e31f71457cb21fd056b234f872126974e) ### Runtime and platform Node 24.22.1; macOS 27.0.1 arm64 ### Target and artifact context Authored extracted CommonJS application directories containing a package manifest, Electron main source, and preload source. REA reads them as inert text; no live provider or target process is involved. ### Interface CLI ### Earliest failure stage Native analysis or reconstruction ### Relevant output or evidence The JSONL above is observed output from the executed public CLI reproduction. Inspection of complete retained Evidence also found `conditions: []` on the `api.ping` terminal candidate and complete coverage on its path edges for the labelled-break input. The same candidate remains `resolution: "candidate"` with runtime limitations. Application coverage is separate from semantic-graph coverage, which remains unknown; the complete application graph is not proof of complete runtime semantics. Source-only explanation, not runtime instrumentation: `src/domain/javascript/electronCallPathBlockPrefixes.ts:42` classifies a preceding statement through `symbolicDefiniteExit`, and its branch-arm checks at lines 50–51 use the same helper. `src/domain/javascript/javascriptSymbolicControlFlow.ts:62` recognizes definite return/throw exits and recursively handles blocks and both-exiting `if` branches; it does not recognize labelled breaks. `src/domain/javascript/electronWrappedCallPaths.ts:292` retains a continuing-path predicate only when its statement fact identifies an exiting arm. Its seed-prefix replay at line 1253 therefore receives no exiting arm for this break guard. `src/application/javascript/ElectronBoundaryGraphCallPaths.ts:64` copies the already-recovered path conditions to graph observations. The existing acceptance case at `tests/boundary/cli/electronWrappedCallPaths.test.ts:246` covers ordinary-source conditional returns and their partial coverage; it was inspected, not executed in this verification. ### Typed outcome or recovery expected For the labelled-break input, preserve a condition equivalent to `!(!ready)` with its source range on the recovered `api.ping` candidate and associated path edges. If this syntax is intentionally outside the model, retain an explicit unresolved-control-flow qualification rather than silently losing the predicate. Keep static-candidate authority and runtime limitations, and preserve the working return control. ### Analysis or suspected cause The observed differential is consistent with a block-prefix exit-classification gap. A labelled break exits the specific enclosing labelled statement, while a return exits a function. That distinction needs to remain intact: classifying every nested break as a function exit would be unsound for statements reached after an inner switch or block. This is a source-derived diagnosis of the tested shape, not a proposed implementation or a claim about untested control flow. ### Additional context Related (closed): - https://github.com/morluto/rea/issues/3196 fixed predicates after conditional returns; that fix is present in the baseline and the return control works, while the labelled-break input still loses its predicate. - https://github.com/morluto/rea/issues/2668 fixed conditions lost during IPC join projection; this baseline failure already has an empty condition list on the recovered path before any join projection. The npm registry reported 6.8.0 as the latest published version during verification. This report executed the assigned source checkout and its prepared runtime, not a separately installed npm package. Nothing was published during verification.
Sign in to join this conversation.
No milestone
No project
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
morluto/rea#4422
No description provided.