Spaces:
Running
Running
| """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] | |
| 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" | |