"""Frontend settings and fixed-input replay wiring.""" from dataclasses import replace import json from pathlib import Path import pytest from verifier import InputRecipe, SamplingConfig from demo.app import load_recipe, run_verification, task_from_inputs from demo.examples import EXAMPLE_NAMES def test_mode_inputs_are_validated(example_rows): row = example_rows[EXAMPLE_NAMES.index("faultless-linked-list")].copy() random = task_from_inputs(*row, execution_mode="random", null_probability=0.10, repeated_branch_threshold=0, max_learned_probability=2) assert random.execution.mode == "random" assert random.execution.sampling == SamplingConfig(0.10, 0.10, 0.10) assert random.execution.guidance.repeated_branch_threshold == 8 assert random.execution.guidance.max_learned_probability == 0.75 guided = task_from_inputs(*row, null_probability=0.90, repeated_branch_threshold=4, max_learned_probability=0.60) assert guided.execution.mode == "comparison_guided" assert guided.execution.sampling == SamplingConfig() assert guided.execution.guidance.repeated_branch_threshold == 4 assert guided.execution.guidance.max_learned_probability == 0.60 with pytest.raises(ValueError): task_from_inputs(*row, execution_mode="random", null_probability=2) with pytest.raises(ValueError): task_from_inputs(*row, execution_mode="comparison_guided", repeated_branch_threshold=0) def test_guided_report_download_can_be_replayed(tmp_path, example_rows): row = example_rows[EXAMPLE_NAMES.index("faultless-linked-list")].copy() row[5] = 2 updates = list(run_verification(*row, report_directory=tmp_path / "reports")) downloaded = Path(updates[-1][3]) data = json.loads(downloaded.read_text()) assert data["schema"] == "verifier-report-v4" assert data["verdict"] == "mismatch" assert len(data["recipes"]) == len(data["discoveries"]) == 2 assert "Discovery:" in updates[-1][0] recipe = load_recipe(downloaded) assert recipe == InputRecipe.from_mapping(data["recipes"][0]) standalone = tmp_path / "recipe.json" standalone.write_text(recipe.to_json()) assert load_recipe(standalone) == recipe replayed = list(run_verification(*row, replay_recipe=str(downloaded), report_directory=tmp_path / "replay")) final = json.loads(Path(replayed[-1][3]).read_text()) assert final["completed"] == 1 assert final["results"][0] == data["results"][0] assert "Fixed-input replay" in replayed[-1][0] assert replayed[-1][1][0][1] == "Replay" def test_report_without_recipes_is_rejected(tmp_path): path = tmp_path / "report.json" path.write_text('{"recipes": []}') with pytest.raises(ValueError): load_recipe(path) def test_concolic_ui_settings_and_report(example_rows, tmp_path): row = example_rows[EXAMPLE_NAMES.index("identical")].copy() row[5] = 3 task = task_from_inputs(*row, execution_mode="concolic", null_probability=2, repeated_branch_threshold=0, max_learned_probability=2, max_new_testcases_per_run=2, solver_timeout_ms=500, random_input_probability=0.25) assert task.execution_count == task.run_count == 3 assert task.execution.concolic.max_new_testcases_per_run == 2 assert task.execution.concolic.solver_timeout_ms == 500 with pytest.raises(ValueError): task_from_inputs(*row, execution_mode="concolic", random_input_probability=2) updates = list(run_verification(*row, execution_mode="concolic", report_directory=tmp_path)) report = json.loads(Path(updates[-1][3]).read_text()) assert report["schema"] == "verifier-report-v4" assert report["completed"] == report["task"]["execution_count"] == 3 assert report["verdict"] == "agree" assert len(report["testcases"]) == len(report["recipes"]) == 3 assert [row[0] for row in updates[-1][1]] == ["1", "2", "3"] assert "Concolic:" in updates[-1][0] assert all(row[1] == "Random" for row in updates[-1][1]) def test_concolic_controls_are_connected_and_mode_specific(example_rows, tmp_path): from demo.app import create_app app = create_app(tmp_path / "examples") blocks = list(app.blocks.values()) mode = next(block for block in blocks if getattr(block, "label", None) == "Execution mode") assert "concolic" in [choice[1] for choice in mode.choices] for label in ("Number of executions", "Max new testcases per run", "Solver timeout per query (ms)", "Fresh random input probability"): block = next(block for block in blocks if getattr(block, "label", None) == label) for api_name in ("verify", "assembly"): event = next(event for event in app.fns.values() if event.api_name == api_name) assert block in event.inputs change = next(event for event in app.fns.values() if event.targets == [(mode._id, "change")]) assert [update["visible"] for update in change.fn("concolic")] == [False, False, True] @pytest.mark.parametrize("mode,origin,expected", [ ("concolic", "random", "Random"), ("concolic", "generated", "Concolic"), ("random", "random", "Random"), ("comparison_guided", "random", "Comparison guided"), ("concolic", "replay", "Replay"), ]) def test_execution_source_uses_testcase_origin(mode, origin, expected): from types import SimpleNamespace from demo.app import HEADERS, execution_source, result_row report = SimpleNamespace(task={"execution": {"mode": mode}}, testcases=(SimpleNamespace(origin=origin),)) result = SimpleNamespace(seed=0, difference=None, verdict="agree", reason=None, original=SimpleNamespace(reason=None), candidate=SimpleNamespace(reason=None)) row = result_row(result, 1, execution_source(report)) assert HEADERS[:3] == ["Execution", "Source", "Verdict"] assert row[:3] == ["1", expected, "agree"] assert len(row) == len(HEADERS) def test_concolic_generated_source_is_streamed_per_execution(example_rows, tmp_path): row = example_rows[EXAMPLE_NAMES.index("identical")].copy() row[2] = "unsigned target(unsigned b) { if(b == 42) return 0; return (b << 13) | (b >> 19); }" row[5], row[9] = 2, "-O0" updates = list(run_verification(*row, execution_mode="concolic", random_input_probability=0, report_directory=tmp_path)) rows = updates[-1][1] assert [row[1] for row in rows] == ["Random", "Concolic"] assert [row[2] for row in rows] == ["agree", "mismatch"] assert updates[0][1][0][1] == "Random" assert updates[1][1][1][1] == "Concolic"