Spaces:
Running
Running
File size: 6,819 Bytes
826c2df d59b954 586c0fc d59b954 586c0fc 826c2df d59b954 586c0fc 826c2df d59b954 826c2df d76830d 826c2df a0a2eb6 826c2df d76830d a0a2eb6 d76830d a0a2eb6 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 | """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"
|