lib/smt/src/choir/test.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const namespace = @import("root.zig");
2 const std = @import("std");
3 const choir = @import("choir");
4
5 const ir = choir.ir;
6
7 const dialect = namespace.dialect;
8 const names = namespace.names;
9 const attr_names = namespace.attr_names;
10 const loadDialect = namespace.loadDialect;
11 const registerDialect = namespace.registerDialect;
12 const registry = namespace.registry;
13 const SmtDialect = namespace.SmtDialect;
14 const type_names = namespace.type_names;
15
16 test {
17 std.testing.refAllDecls(names);
18 std.testing.refAllDecls(dialect);
19 }
20
21 test "SMT dialect registers parameterized bit-vector type" {
22 var ctx = try ir.Context.init(std.testing.allocator, ir.Context.Limits.testing);
23 defer ctx.deinit(std.testing.allocator);
24
25 try ir.dialects.loadDialectSpec(&ctx, SmtDialect.spec);
26 const bool_type = try SmtDialect.getBoolType(&ctx);
27 const bv64 = try SmtDialect.getBitVecType(&ctx, 64);
28 const array = try SmtDialect.getArrayType(&ctx, 8, 32);
29 try std.testing.expectEqualStrings(type_names.boolean, bool_type.getDialectTypeName().?);
30 try std.testing.expectEqualStrings(type_names.bv, bv64.getDialectTypeName().?);
31 try std.testing.expectEqualStrings(type_names.array, array.getDialectTypeName().?);
32 try std.testing.expectEqualStrings("64", bv64.getDialectParamKey().?);
33 try std.testing.expectEqualStrings("8:32", array.getDialectParamKey().?);
34 try std.testing.expectEqual(@as(u32, 64), SmtDialect.bitVecWidth(&ctx, bv64).?);
35 try std.testing.expectEqual(SmtDialect.ArrayTypePayload{ .index_width = 8, .element_width = 32 }, SmtDialect.arrayShape(&ctx, array).?);
36 }
37
38 test "SMT dialect creates symbolic bit-vector assertion operations" {
39 var ctx = try ir.Context.init(std.testing.allocator, ir.Context.Limits.testing);
40 defer ctx.deinit(std.testing.allocator);
41
42 try ir.dialects.loadDialectSpec(&ctx, SmtDialect.spec);
43 const loc = ir.Location.getUnknown();
44 const bool_type = try SmtDialect.getBoolType(&ctx);
45 const bv8 = try SmtDialect.getBitVecType(&ctx, 8);
46 const x = try SmtDialect.VarOp.create(&ctx, loc, "x", bv8);
47 const one = try SmtDialect.BitVecConstOp.create(&ctx, loc, 8, 1);
48 const sum = try SmtDialect.BvAddOp.create(&ctx, loc, x.getResult(), one.getResult());
49 const difference = try SmtDialect.BvSubOp.create(&ctx, loc, x.getResult(), one.getResult());
50 const inverted = try SmtDialect.BvNotOp.create(&ctx, loc, x.getResult());
51 const masked = try SmtDialect.BvAndOp.create(&ctx, loc, inverted.getResult(), one.getResult());
52 const either = try SmtDialect.BvOrOp.create(&ctx, loc, x.getResult(), one.getResult());
53 const toggled = try SmtDialect.BvXorOp.create(&ctx, loc, either.getResult(), masked.getResult());
54 const shifted = try SmtDialect.BvShlOp.create(&ctx, loc, toggled.getResult(), one.getResult());
55 const restored = try SmtDialect.BvLshrOp.create(&ctx, loc, shifted.getResult(), one.getResult());
56 const signed_restored = try SmtDialect.BvAshrOp.create(&ctx, loc, shifted.getResult(), one.getResult());
57 const rotated_left = try SmtDialect.BvRotlOp.create(&ctx, loc, shifted.getResult(), 1);
58 const rotated_right = try SmtDialect.BvRotrOp.create(&ctx, loc, shifted.getResult(), 7);
59 const quotient = try SmtDialect.BvUdivOp.create(&ctx, loc, shifted.getResult(), one.getResult());
60 const remainder = try SmtDialect.BvUremOp.create(&ctx, loc, shifted.getResult(), one.getResult());
61 const signed_quotient = try SmtDialect.BvSdivOp.create(&ctx, loc, shifted.getResult(), one.getResult());
62 const signed_remainder = try SmtDialect.BvSremOp.create(&ctx, loc, shifted.getResult(), one.getResult());
63 const signed_modulo = try SmtDialect.BvSmodOp.create(&ctx, loc, shifted.getResult(), one.getResult());
64 const overflow = try SmtDialect.BvUaddoOp.create(&ctx, loc, x.getResult(), one.getResult());
65 const signed_add_overflow = try SmtDialect.BvSaddoOp.create(&ctx, loc, x.getResult(), one.getResult());
66 const signed_sub_overflow = try SmtDialect.BvSsuboOp.create(&ctx, loc, x.getResult(), one.getResult());
67 const signed_mul_overflow = try SmtDialect.BvSmuloOp.create(&ctx, loc, x.getResult(), one.getResult());
68 const signed_less = try SmtDialect.BvSltOp.create(&ctx, loc, x.getResult(), one.getResult());
69 const signed_less_equal = try SmtDialect.BvSleOp.create(&ctx, loc, x.getResult(), one.getResult());
70 const applied = try SmtDialect.ApplyOp.create(&ctx, loc, "f", &.{x.getResult()}, bv8);
71 const no_overflow = try SmtDialect.NotOp.create(&ctx, loc, overflow.getResult());
72 const assertion = try SmtDialect.AssertOp.createGrouped(&ctx, loc, "no-overflow", "overflow", no_overflow.getResult());
73
74 try std.testing.expectEqualStrings("x", x.getName().?);
75 try std.testing.expectEqual(@as(u128, 1), one.getValue().?);
76 try std.testing.expect(sum.getResult().type.eql(bv8));
77 try std.testing.expect(difference.getResult().type.eql(bv8));
78 try std.testing.expect(inverted.getResult().type.eql(bv8));
79 try std.testing.expect(masked.getResult().type.eql(bv8));
80 try std.testing.expect(either.getResult().type.eql(bv8));
81 try std.testing.expect(toggled.getResult().type.eql(bv8));
82 try std.testing.expect(shifted.getResult().type.eql(bv8));
83 try std.testing.expect(restored.getResult().type.eql(bv8));
84 try std.testing.expect(signed_restored.getResult().type.eql(bv8));
85 try std.testing.expect(rotated_left.getResult().type.eql(bv8));
86 try std.testing.expect(rotated_right.getResult().type.eql(bv8));
87 try std.testing.expectEqual(@as(u32, 1), rotated_left.getAmount().?);
88 try std.testing.expectEqual(@as(u32, 7), rotated_right.getAmount().?);
89 try std.testing.expect(quotient.getResult().type.eql(bv8));
90 try std.testing.expect(remainder.getResult().type.eql(bv8));
91 try std.testing.expect(signed_quotient.getResult().type.eql(bv8));
92 try std.testing.expect(signed_remainder.getResult().type.eql(bv8));
93 try std.testing.expect(signed_modulo.getResult().type.eql(bv8));
94 try std.testing.expect(signed_add_overflow.getResult().type.eql(bool_type));
95 try std.testing.expect(signed_sub_overflow.getResult().type.eql(bool_type));
96 try std.testing.expect(signed_mul_overflow.getResult().type.eql(bool_type));
97 try std.testing.expect(signed_less.getResult().type.eql(bool_type));
98 try std.testing.expect(signed_less_equal.getResult().type.eql(bool_type));
99 try std.testing.expectEqualStrings("f", applied.getName().?);
100 try std.testing.expect(applied.getResult().type.eql(bv8));
101 try std.testing.expect(assertion.getAssertion() == no_overflow.getResult());
102 try std.testing.expectEqualStrings("no-overflow", assertion.getName().?);
103 try std.testing.expectEqualStrings("overflow", assertion.getGroup().?);
104
105 var assertion_summary = try choir.passes.effects.EffectSummary.init(
106 std.testing.allocator,
107 assertion.op,
108 );
109 defer assertion_summary.deinit();
110 try std.testing.expect(!assertion_summary.complete);
111 try std.testing.expect(!assertion_summary.discard());
112 }
113
114 test "SMT dialect creates bit-vector width-changing operations" {
115 var ctx = try ir.Context.init(std.testing.allocator, ir.Context.Limits.testing);
116 defer ctx.deinit(std.testing.allocator);
117
118 try ir.dialects.loadDialectSpec(&ctx, SmtDialect.spec);
119 const loc = ir.Location.getUnknown();
120 const bv4 = try SmtDialect.getBitVecType(&ctx, 4);
121 const bv8 = try SmtDialect.getBitVecType(&ctx, 8);
122 const high = try SmtDialect.VarOp.create(&ctx, loc, "high", bv4);
123 const low = try SmtDialect.VarOp.create(&ctx, loc, "low", bv4);
124 const word = try SmtDialect.BvConcatOp.create(&ctx, loc, high.getResult(), low.getResult());
125 const upper = try SmtDialect.BvExtractOp.create(&ctx, loc, word.getResult(), 7, 4);
126 const lower = try SmtDialect.BvExtractOp.create(&ctx, loc, word.getResult(), 3, 0);
127 const zeroed = try SmtDialect.BvZeroExtOp.create(&ctx, loc, low.getResult(), 4);
128 const signed = try SmtDialect.BvSignExtOp.create(&ctx, loc, high.getResult(), 4);
129
130 try std.testing.expect(word.getResult().type.eql(bv8));
131 try std.testing.expect(upper.getResult().type.eql(bv4));
132 try std.testing.expect(lower.getResult().type.eql(bv4));
133 try std.testing.expect(zeroed.getResult().type.eql(bv8));
134 try std.testing.expect(signed.getResult().type.eql(bv8));
135 try std.testing.expectEqual(@as(u32, 7), upper.getHigh().?);
136 try std.testing.expectEqual(@as(u32, 4), upper.getLow().?);
137 try std.testing.expectEqual(@as(u32, 4), zeroed.getExtra().?);
138 try std.testing.expectEqual(@as(u32, 4), signed.getExtra().?);
139 }
140
141 test "SMT dialect creates bit-vector array operations" {
142 var ctx = try ir.Context.init(std.testing.allocator, ir.Context.Limits.testing);
143 defer ctx.deinit(std.testing.allocator);
144
145 try ir.dialects.loadDialectSpec(&ctx, SmtDialect.spec);
146 const loc = ir.Location.getUnknown();
147 const array_type = try SmtDialect.getArrayType(&ctx, 2, 4);
148 const index_type = try SmtDialect.getBitVecType(&ctx, 2);
149 const element_type = try SmtDialect.getBitVecType(&ctx, 4);
150 const memory = try SmtDialect.VarOp.create(&ctx, loc, "memory", array_type);
151 const index = try SmtDialect.VarOp.create(&ctx, loc, "index", index_type);
152 const value = try SmtDialect.VarOp.create(&ctx, loc, "value", element_type);
153 const written = try SmtDialect.ArrayStoreOp.create(&ctx, loc, memory.getResult(), index.getResult(), value.getResult());
154 const loaded = try SmtDialect.ArraySelectOp.create(&ctx, loc, written.getResult(), index.getResult());
155
156 try std.testing.expect(written.getResult().type.eql(array_type));
157 try std.testing.expect(loaded.getResult().type.eql(element_type));
158 try std.testing.expectError(error.InvalidArrayIndexType, SmtDialect.ArraySelectOp.create(&ctx, loc, memory.getResult(), value.getResult()));
159 try std.testing.expectError(error.InvalidArrayElementType, SmtDialect.ArrayStoreOp.create(&ctx, loc, memory.getResult(), index.getResult(), index.getResult()));
160 }
161
162 fn countOpsNamed(op: *ir.Operation, name: []const u8) usize {
163 var count: usize = if (std.mem.eql(u8, op.name.name, name)) 1 else 0;
164 for (op.regions.items) |*region| {
165 var block_iter = region.getBlocks();
166 while (block_iter.next()) |block| {
167 var current: ?*ir.Operation = @ptrCast(@alignCast(block.operations.head));
168 while (current) |current_op| {
169 count += countOpsNamed(current_op, name);
170 current = current_op.next_op;
171 }
172 }
173 }
174 return count;
175 }
176
177 fn runCsePass(allocator: std.mem.Allocator, module: *ir.Operation, ctx: *ir.Context) !choir.passes.PassManager {
178 var pm = choir.passes.PassManager.init(allocator);
179 errdefer pm.deinit();
180 try pm.addPass(choir.passes.createCommonSubexpressionEliminationPass());
181 try std.testing.expectEqual(choir.passes.PassResult.success, pm.run(module, ctx));
182 return pm;
183 }
184
185 fn createReturn(ctx: *ir.Context, block: *ir.Block, operands: []const *ir.Value) !choir.dialects.FuncDialect.ReturnOp {
186 const op = try choir.dialects.FuncDialect.ReturnOp.create(ctx, ir.Location.getUnknown(), operands);
187 try block.addOperation(op.op);
188 return op;
189 }
190
191 test "SMT commutative traits grant no CSE permission" {
192 const testing = std.testing;
193 const allocator = testing.allocator;
194
195 var ctx = try ir.Context.init(allocator, ir.Context.Limits.testing);
196 defer ctx.deinit(allocator);
197 try loadDialect(&ctx);
198
199 const add_info = ctx.lookupOperation(SmtDialect.BvUaddoOp.operation_name).?;
200 const sub_info = ctx.lookupOperation(SmtDialect.BvSsuboOp.operation_name).?;
201 try testing.expect(add_info.traits.is_commutative);
202 try testing.expect(!sub_info.traits.is_commutative);
203
204 const module = try choir.dialects.BuiltinDialect.ModuleOp.create(&ctx, ir.Location.getUnknown());
205 const block = module.getBodyBlock();
206 const bv4 = try SmtDialect.getBitVecType(&ctx, 4);
207 const lhs = try SmtDialect.VarOp.create(&ctx, ir.Location.getUnknown(), "lhs", bv4);
208 try block.addOperation(lhs.op);
209 const rhs = try SmtDialect.VarOp.create(&ctx, ir.Location.getUnknown(), "rhs", bv4);
210 try block.addOperation(rhs.op);
211
212 const first_add = try SmtDialect.BvUaddoOp.create(&ctx, ir.Location.getUnknown(), lhs.getResult(), rhs.getResult());
213 try block.addOperation(first_add.op);
214 const second_add = try SmtDialect.BvUaddoOp.create(&ctx, ir.Location.getUnknown(), rhs.getResult(), lhs.getResult());
215 try block.addOperation(second_add.op);
216 const first_sub = try SmtDialect.BvSsuboOp.create(&ctx, ir.Location.getUnknown(), lhs.getResult(), rhs.getResult());
217 try block.addOperation(first_sub.op);
218 const swapped_sub = try SmtDialect.BvSsuboOp.create(&ctx, ir.Location.getUnknown(), rhs.getResult(), lhs.getResult());
219 try block.addOperation(swapped_sub.op);
220 const ret = try createReturn(&ctx, block, &.{ second_add.getResult(), first_sub.getResult(), swapped_sub.getResult() });
221
222 var pm = try runCsePass(allocator, module.op, &ctx);
223 defer pm.deinit();
224
225 try testing.expectEqual(
226 @as(usize, 2),
227 countOpsNamed(module.op, SmtDialect.BvUaddoOp.operation_name),
228 );
229 try testing.expectEqual(@as(usize, 2), countOpsNamed(module.op, SmtDialect.BvSsuboOp.operation_name));
230 try testing.expectEqual(second_add.getResult(), ret.op.getOperand(0).?);
231 try testing.expectEqual(first_sub.getResult(), ret.op.getOperand(1).?);
232 try testing.expectEqual(swapped_sub.getResult(), ret.op.getOperand(2).?);
233 try testing.expectEqual(@as(u64, 0), pm.stats.passes_modified);
234 }
235
236 test "SMT fixed rotates remain unqualified for CSE" {
237 const testing = std.testing;
238 const allocator = testing.allocator;
239
240 var ctx = try ir.Context.init(allocator, ir.Context.Limits.testing);
241 defer ctx.deinit(allocator);
242 try loadDialect(&ctx);
243
244 const module = try choir.dialects.BuiltinDialect.ModuleOp.create(&ctx, ir.Location.getUnknown());
245 const block = module.getBodyBlock();
246 const loc = ir.Location.getUnknown();
247 const bv4 = try SmtDialect.getBitVecType(&ctx, 4);
248 const x = try SmtDialect.VarOp.create(&ctx, loc, "x", bv4);
249 try block.addOperation(x.op);
250
251 const first = try SmtDialect.BvRotlOp.create(&ctx, loc, x.getResult(), 1);
252 try block.addOperation(first.op);
253 const duplicate = try SmtDialect.BvRotlOp.create(&ctx, loc, x.getResult(), 1);
254 try block.addOperation(duplicate.op);
255 const other = try SmtDialect.BvRotlOp.create(&ctx, loc, x.getResult(), 2);
256 try block.addOperation(other.op);
257 const ret = try createReturn(&ctx, block, &.{ duplicate.getResult(), other.getResult() });
258
259 var pm = try runCsePass(allocator, module.op, &ctx);
260 defer pm.deinit();
261
262 try testing.expectEqual(
263 @as(usize, 3),
264 countOpsNamed(module.op, SmtDialect.BvRotlOp.operation_name),
265 );
266 try testing.expectEqual(duplicate.getResult(), ret.op.getOperand(0).?);
267 try testing.expectEqual(other.getResult(), ret.op.getOperand(1).?);
268 try testing.expectEqual(@as(u64, 0), pm.stats.passes_modified);
269 }
270
271 test "SMT effect declarations remain unqualified for generic optimization" {
272 var ctx = try ir.Context.init(std.testing.allocator, ir.Context.Limits.testing);
273 defer ctx.deinit(std.testing.allocator);
274 try loadDialect(&ctx);
275 const constant = try SmtDialect.BoolConstOp.create(&ctx, .unknown, true);
276 var declaration = try ir.interfaces.effects.inspect(std.testing.allocator, constant.op);
277 defer declaration.deinit(std.testing.allocator);
278 try std.testing.expect(!declaration.facts.complete);
279 try std.testing.expect(!ir.interfaces.effects.discard(declaration.facts));
280 }