lib/choir/src/properties/cfg.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const alloc_arena = @import("alloc_arena");
3 const hypothesis = @import("hypothesis");
4 const pretty = @import("pretty");
5 const choir = @import("choir");
6
7 const block_count = 4;
8 const operation_count = 6;
9 const successor_limit = 3;
10 const action_count_min = 1;
11 const action_count_max = 64;
12 const example_count = 200;
13 const property_seed: u64 = 0xc6f0_2026_0728;
14
15 comptime {
16 std.debug.assert(block_count > 0);
17 std.debug.assert(operation_count > 0);
18 std.debug.assert(successor_limit <= block_count);
19 std.debug.assert(action_count_min > 0);
20 std.debug.assert(action_count_min <= action_count_max);
21 }
22
23 pub const EvidenceBounds = struct {
24 blocks: usize = block_count,
25 operations: usize = operation_count,
26 successors_per_operation_max: usize = successor_limit,
27 actions_per_example_min: usize = action_count_min,
28 actions_per_example_max: usize = action_count_max,
29 examples: usize = example_count,
30 seed: u64 = property_seed,
31 };
32
33 pub const EvidenceCoverage = struct {
34 examples: u64 = 0,
35 attach: u64 = 0,
36 replace: u64 = 0,
37 detach: u64 = 0,
38 move: u64 = 0,
39 remove: u64 = 0,
40 parent: u64 = 0,
41 has_predecessor: u64 = 0,
42 predecessor_count: u64 = 0,
43 verifier: u64 = 0,
44
45 pub fn complete(self: EvidenceCoverage) bool {
46 return self.examples == example_count and
47 self.attach > 0 and
48 self.replace > 0 and
49 self.detach > 0 and
50 self.move > 0 and
51 self.remove > 0 and
52 self.parent > 0 and
53 self.has_predecessor > 0 and
54 self.predecessor_count > 0 and
55 self.verifier > 0;
56 }
57 };
58
59 const ModelOperation = struct {
60 block: ?usize = null,
61 successors: [successor_limit]usize = undefined,
62 successor_count: usize = 0,
63 };
64
65 const ActionKind = enum {
66 attach,
67 replace,
68 detach,
69 move,
70 remove,
71 };
72
73 const Action = struct {
74 step: usize,
75 kind: ActionKind,
76 operation: usize,
77 block: ?usize = null,
78 successors: [successor_limit]usize = undefined,
79 successor_count: usize = 0,
80 };
81
82 const State = struct {
83 blocks: *[block_count]choir.Block,
84 operations: *const [operation_count]*choir.Operation,
85 model: *[operation_count]ModelOperation,
86 };
87
88 const Mismatch = union(enum) {
89 parent: struct {
90 operation: usize,
91 expected: ?usize,
92 actual: ?usize,
93 actual_is_null: bool,
94 },
95 predecessor: struct {
96 source: usize,
97 target: usize,
98 expected: bool,
99 actual: bool,
100 },
101 predecessor_count: struct {
102 target: usize,
103 expected: usize,
104 actual: usize,
105 },
106 verifier: struct {
107 target: usize,
108 err: anyerror,
109 },
110 };
111
112 fn settings() hypothesis.Settings {
113 var value = hypothesis.Settings.quick()
114 .withSeed(property_seed)
115 .withDatabase("zig-out/hypothesis-failures/choir-cfg-predecessor-mirror");
116 value.max_examples = example_count;
117 value.target_examples = example_count;
118 return value;
119 }
120
121 pub fn evidenceSettings() hypothesis.Settings {
122 var value = hypothesis.Settings.quick().withSeed(property_seed);
123 value.max_examples = example_count;
124 value.max_replays = 0;
125 value.target_examples = 0;
126 return value;
127 }
128
129 fn drawUsize(
130 conjecture: *hypothesis.ConjectureData,
131 min: usize,
132 max: usize,
133 shrink_towards: usize,
134 ) !usize {
135 return @intCast(try conjecture.drawInteger(
136 @intCast(min),
137 @intCast(max),
138 @intCast(shrink_towards),
139 ));
140 }
141
142 fn modelContains(
143 model: *const [operation_count]ModelOperation,
144 source: usize,
145 target: usize,
146 ) bool {
147 for (model) |operation| {
148 if (operation.block != source) continue;
149 for (operation.successors[0..operation.successor_count]) |successor| {
150 if (successor == target) return true;
151 }
152 }
153 return false;
154 }
155
156 fn blockIndex(
157 blocks: *const [block_count]choir.Block,
158 block: *choir.Block,
159 ) ?usize {
160 for (blocks, 0..) |*candidate, index| {
161 if (candidate == block) return index;
162 }
163 return null;
164 }
165
166 fn parentMismatch(state: State, coverage: *EvidenceCoverage) ?Mismatch {
167 for (state.model, state.operations, 0..) |operation, live, index| {
168 coverage.parent += 1;
169 const actual_parent = live.parent_block;
170 if (operation.block) |expected| {
171 if (actual_parent == &state.blocks[expected]) continue;
172 } else if (actual_parent == null) {
173 continue;
174 }
175 return .{ .parent = .{
176 .operation = index,
177 .expected = operation.block,
178 .actual = if (actual_parent) |block| blockIndex(state.blocks, block) else null,
179 .actual_is_null = actual_parent == null,
180 } };
181 }
182 return null;
183 }
184
185 fn mirrorMismatch(state: State, coverage: *EvidenceCoverage) ?Mismatch {
186 for (0..block_count) |target| {
187 var expected_count: usize = 0;
188 for (0..block_count) |source| {
189 const expected = modelContains(state.model, source, target);
190 const actual = state.blocks[target].hasPredecessor(&state.blocks[source]);
191 coverage.has_predecessor += 1;
192 if (expected) expected_count += 1;
193 if (actual != expected) return .{ .predecessor = .{
194 .source = source,
195 .target = target,
196 .expected = expected,
197 .actual = actual,
198 } };
199 }
200 const actual_count = state.blocks[target].getNumPredecessors();
201 coverage.predecessor_count += 1;
202 if (actual_count != expected_count) return .{ .predecessor_count = .{
203 .target = target,
204 .expected = expected_count,
205 .actual = actual_count,
206 } };
207 }
208 return null;
209 }
210
211 fn verifierMismatch(state: State, coverage: *EvidenceCoverage) ?Mismatch {
212 for (state.blocks, 0..) |*block, target| {
213 coverage.verifier += 1;
214 choir.ir.verifyBlock(block, .{
215 .check_terminators = false,
216 .check_local_dominance = false,
217 }) catch |err| return .{ .verifier = .{
218 .target = target,
219 .err = err,
220 } };
221 }
222 return null;
223 }
224
225 fn findMismatch(state: State, coverage: *EvidenceCoverage) ?Mismatch {
226 if (parentMismatch(state, coverage)) |mismatch| return mismatch;
227 if (mirrorMismatch(state, coverage)) |mismatch| return mismatch;
228 return verifierMismatch(state, coverage);
229 }
230
231 fn applyAttach(
232 conjecture: *hypothesis.ConjectureData,
233 state: State,
234 action: Action,
235 ) !?Action {
236 if (state.model[action.operation].block != null) return null;
237 const block = try drawUsize(conjecture, 0, block_count - 1, 0);
238 try state.blocks[block].addOperation(state.operations[action.operation]);
239 state.model[action.operation].block = block;
240 var executed = action;
241 executed.block = block;
242 return executed;
243 }
244
245 fn applyReplace(
246 conjecture: *hypothesis.ConjectureData,
247 state: State,
248 action: Action,
249 ) !Action {
250 const count = try drawUsize(conjecture, 0, successor_limit, 0);
251 var successors: [successor_limit]*choir.Block = undefined;
252 var executed = action;
253 executed.successor_count = count;
254 for (0..count) |index| {
255 const target = try drawUsize(conjecture, 0, block_count - 1, 0);
256 successors[index] = &state.blocks[target];
257 executed.successors[index] = target;
258 }
259 try state.operations[action.operation].setSuccessors(successors[0..count]);
260 state.model[action.operation].successor_count = count;
261 @memcpy(
262 state.model[action.operation].successors[0..count],
263 executed.successors[0..count],
264 );
265 return executed;
266 }
267
268 fn applyDetach(state: State, action: Action) ?Action {
269 const block = state.model[action.operation].block orelse return null;
270 state.blocks[block].detachOperation(state.operations[action.operation]);
271 state.model[action.operation].block = null;
272 var executed = action;
273 executed.block = block;
274 return executed;
275 }
276
277 fn applyMove(
278 conjecture: *hypothesis.ConjectureData,
279 state: State,
280 action: Action,
281 ) !?Action {
282 if (state.model[action.operation].block == null) return null;
283 const block = try drawUsize(conjecture, 0, block_count - 1, 0);
284 try state.operations[action.operation].moveToEnd(&state.blocks[block]);
285 state.model[action.operation].block = block;
286 var executed = action;
287 executed.block = block;
288 return executed;
289 }
290
291 fn applyRemove(state: State, action: Action) ?Action {
292 const block = state.model[action.operation].block orelse return null;
293 state.blocks[block].removeOperation(state.operations[action.operation]);
294 state.model[action.operation].block = null;
295 state.model[action.operation].successor_count = 0;
296 var executed = action;
297 executed.block = block;
298 return executed;
299 }
300
301 fn applyAction(
302 conjecture: *hypothesis.ConjectureData,
303 state: State,
304 step: usize,
305 coverage: *EvidenceCoverage,
306 ) !?Action {
307 const kind: ActionKind = @fromBackingInt(@intCast(try drawUsize(conjecture, 0, 4, 0)));
308 const operation = try drawUsize(conjecture, 0, operation_count - 1, 0);
309 const action = Action{ .step = step, .kind = kind, .operation = operation };
310 const executed = switch (kind) {
311 .attach => try applyAttach(conjecture, state, action),
312 .replace => try applyReplace(conjecture, state, action),
313 .detach => applyDetach(state, action),
314 .move => try applyMove(conjecture, state, action),
315 .remove => applyRemove(state, action),
316 };
317 if (executed != null) switch (kind) {
318 .attach => coverage.attach += 1,
319 .replace => coverage.replace += 1,
320 .detach => coverage.detach += 1,
321 .move => coverage.move += 1,
322 .remove => coverage.remove += 1,
323 };
324 return executed;
325 }
326
327 fn writeAction(report: *pretty.diagnostic.Report, action: Action) !void {
328 try report.field("step", "{d}", .{action.step});
329 try report.field("action", "{s}", .{@tagName(action.kind)});
330 try report.field("operation", "{d}", .{action.operation});
331 if (action.block) |block| try report.field("block", "{d}", .{block});
332 if (action.kind == .replace) {
333 try report.field(
334 "successors",
335 "{any}",
336 .{action.successors[0..action.successor_count]},
337 );
338 }
339 }
340
341 fn writeMismatch(report: *pretty.diagnostic.Report, mismatch: Mismatch) !void {
342 switch (mismatch) {
343 .parent => |value| {
344 try report.field("mismatch", "operation parent", .{});
345 try report.field("mismatch operation", "{d}", .{value.operation});
346 try report.field("expected block", "{any}", .{value.expected});
347 try report.field("actual block", "{any}", .{value.actual});
348 try report.field("actual parent null", "{any}", .{value.actual_is_null});
349 },
350 .predecessor => |value| {
351 try report.field("mismatch", "predecessor relation", .{});
352 try report.field("source", "{d}", .{value.source});
353 try report.field("target", "{d}", .{value.target});
354 try report.field("expected", "{any}", .{value.expected});
355 try report.field("actual", "{any}", .{value.actual});
356 },
357 .predecessor_count => |value| {
358 try report.field("mismatch", "predecessor count", .{});
359 try report.field("target", "{d}", .{value.target});
360 try report.field("expected", "{d}", .{value.expected});
361 try report.field("actual", "{d}", .{value.actual});
362 },
363 .verifier => |value| {
364 try report.field("mismatch", "live verifier", .{});
365 try report.field("target", "{d}", .{value.target});
366 try report.field("error", "{s}", .{@errorName(value.err)});
367 },
368 }
369 }
370
371 fn writeModel(
372 report: *pretty.diagnostic.Report,
373 model: *const [operation_count]ModelOperation,
374 ) !void {
375 try report.section("independent model");
376 for (model, 0..) |operation, index| {
377 try report.line(
378 "operation {d}: block {any}, successors {any}",
379 .{
380 index,
381 operation.block,
382 operation.successors[0..operation.successor_count],
383 },
384 );
385 }
386 }
387
388 fn writeLive(report: *pretty.diagnostic.Report, blocks: *[block_count]choir.Block) !void {
389 try report.section("live predecessor matrix");
390 for (blocks, 0..) |*target, target_index| {
391 var predecessors: [block_count]bool = undefined;
392 for (blocks, 0..) |*source, source_index| {
393 predecessors[source_index] = target.hasPredecessor(source);
394 }
395 try report.line(
396 "target {d}: count {d}, sources {any}",
397 .{ target_index, target.getNumPredecessors(), predecessors },
398 );
399 }
400 }
401
402 fn diagnose(
403 allocator: std.mem.Allocator,
404 state: State,
405 action: Action,
406 mismatch: Mismatch,
407 ) void {
408 var arena_state = alloc_arena.Arena.init(allocator);
409 defer arena_state.deinit();
410 var report = pretty.diagnostic.Report.init(
411 arena_state.allocator(),
412 "Choir CFG predecessor mirror property failed",
413 ) catch return;
414 defer report.deinit();
415 writeAction(&report, action) catch return;
416 writeMismatch(&report, mismatch) catch return;
417 writeModel(&report, state.model) catch return;
418 writeLive(&report, state.blocks) catch return;
419 pretty.diagnostic.writeStderr(&report, .{ .width = 100 });
420 }
421
422 fn initializeOperations(
423 ctx: *choir.Context,
424 operations: *[operation_count]*choir.Operation,
425 ) !void {
426 for (operations) |*operation| {
427 operation.* = try ctx.createOperation(
428 choir.Operation.State.init("property.cfg.operation", .unknown),
429 );
430 }
431 }
432
433 fn runActions(
434 conjecture: *hypothesis.ConjectureData,
435 allocator: std.mem.Allocator,
436 state: State,
437 coverage: *EvidenceCoverage,
438 ) !void {
439 const action_count = try drawUsize(
440 conjecture,
441 action_count_min,
442 action_count_max,
443 action_count_min,
444 );
445 for (0..action_count) |step| {
446 const action = try applyAction(conjecture, state, step, coverage) orelse continue;
447 if (findMismatch(state, coverage)) |mismatch| {
448 diagnose(allocator, state, action, mismatch);
449 return error.CfgPredecessorMirrorMismatch;
450 }
451 }
452 }
453
454 pub fn propertyWithCoverage(
455 conjecture: *hypothesis.ConjectureData,
456 allocator: std.mem.Allocator,
457 coverage: *EvidenceCoverage,
458 ) !void {
459 std.debug.assert(coverage.examples < std.math.maxInt(u64));
460 coverage.examples += 1;
461 var ctx = try choir.Context.init(allocator, choir.Context.Limits.testing);
462 var blocks: [block_count]choir.Block = undefined;
463 for (&blocks) |*block| block.* = choir.Block.init(allocator);
464 defer {
465 ctx.deinit(allocator);
466 for (&blocks) |*block| block.deinit();
467 }
468 try ctx.allowUnregistered();
469
470 var operations: [operation_count]*choir.Operation = undefined;
471 try initializeOperations(&ctx, &operations);
472 var model: [operation_count]ModelOperation = undefined;
473 for (&model) |*operation| operation.* = .{};
474 try runActions(conjecture, allocator, .{
475 .blocks = &blocks,
476 .operations = &operations,
477 .model = &model,
478 }, coverage);
479 }
480
481 pub const PredecessorMirrorProperty = struct {
482 pub fn property(
483 conjecture: *hypothesis.ConjectureData,
484 allocator: std.mem.Allocator,
485 ) !void {
486 var coverage = EvidenceCoverage{};
487 try propertyWithCoverage(conjecture, allocator, &coverage);
488 }
489 };
490
491 test "property: CFG predecessor mirror matches attached operation edges" {
492 try hypothesis.checkNamed(
493 PredecessorMirrorProperty,
494 "choir-cfg-predecessor-mirror",
495 settings(),
496 );
497 }