lib/choir/src/properties/rewriter.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const ir = choir.ir;
2 const rewrite = ir.rewrite;
3 const std = @import("std");
4 const hypothesis = @import("hypothesis");
5 const choir = @import("choir");
6
7 fn settings() hypothesis.Settings {
8 var value = hypothesis.Settings.quick()
9 .withSeed(0xe2a5_e0f1_2026_0710)
10 .withDatabase("zig-out/hypothesis-failures/choir-erase-only-rewriter");
11 value.max_examples = 100;
12 value.target_examples = 100;
13 return value;
14 }
15
16 fn drawUsize(conjecture: *hypothesis.ConjectureData, min: usize, max: usize, shrink_towards: usize) !usize {
17 return @intCast(try conjecture.drawInteger(@intCast(min), @intCast(max), @intCast(shrink_towards)));
18 }
19
20 const EventCounts = struct {
21 modified: usize = 0,
22 replaced: usize = 0,
23 erased: usize = 0,
24
25 pub fn notifyRewriteEvent(self: *EventCounts, event: rewrite.PatternRewriter.RewriteEvent) void {
26 switch (event) {
27 .modified => self.modified += 1,
28 .replaced => self.replaced += 1,
29 .erased => self.erased += 1,
30 }
31 }
32 };
33
34 pub const EraseOnlyRewriterProperty = struct {
35 pub fn property(conjecture: *hypothesis.ConjectureData, allocator: std.mem.Allocator) !void {
36 var ctx = try choir.Context.init(allocator, choir.Context.Limits.testing);
37 defer ctx.deinit(allocator);
38 try ctx.allowUnregistered();
39
40 const block_count = try drawUsize(conjecture, 1, 16, 1);
41 const ops_per_block = try drawUsize(conjecture, 1, 64, 1);
42 const op_count = block_count * ops_per_block;
43 const ops = try allocator.alloc(*choir.Operation, op_count);
44 defer allocator.free(ops);
45 const erased = try allocator.alloc(bool, op_count);
46 defer allocator.free(erased);
47
48 var body = choir.ir.context.initRegion(&ctx);
49 defer body.deinit();
50 for (0..block_count) |block_index| {
51 const block = try body.addBlock();
52 for (0..ops_per_block) |op_index| {
53 const index = block_index * ops_per_block + op_index;
54 const op = try ctx.createOperation(choir.Operation.State.init("test.erase_candidate", .unknown));
55 try block.addOperation(op);
56 ops[index] = op;
57 erased[index] = try conjecture.drawBoolean();
58 }
59 }
60
61 var root_state = choir.Operation.State.init("test.erase_root", .unknown);
62 root_state.addRegionBodies(&.{&body});
63 const root = try ctx.createOperation(root_state);
64
65 var events = EventCounts{};
66 var rewriter = rewrite.PatternRewriter.init(allocator, &ctx);
67 defer rewriter.deinit();
68 rewriter.setListener(rewrite.PatternRewriter.Listener.bind(&events));
69
70 var erased_count: usize = 0;
71 for (ops, erased) |op, should_erase| {
72 if (!should_erase) continue;
73 try rewriter.eraseOp(op);
74 erased_count += 1;
75 }
76 try conjecture.target(op_count, "operation count");
77 try conjecture.target(erased_count, "erased count");
78
79 rewriter.finalize(root);
80
81 try std.testing.expectEqual(@as(usize, 0), events.modified);
82 try std.testing.expectEqual(@as(usize, 0), events.replaced);
83 try std.testing.expectEqual(erased_count, events.erased);
84
85 var blocks = root.getRegion(0).?.getBlocks();
86 var block_index: usize = 0;
87 while (blocks.next()) |block| : (block_index += 1) {
88 var actual = block.getOperations();
89 for (0..ops_per_block) |op_index| {
90 const index = block_index * ops_per_block + op_index;
91 if (erased[index]) continue;
92 try std.testing.expect(actual.next().? == ops[index]);
93 }
94 try std.testing.expect(actual.next() == null);
95 }
96 try std.testing.expectEqual(block_count, block_index);
97 }
98 };
99
100 test "property: erase-only rewriter preserves survivors and listener events" {
101 try hypothesis.checkNamed(EraseOnlyRewriterProperty, "choir-erase-only-rewriter", settings());
102 }