lib/pluck/src/toplevel/json.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const pretty = @import("pretty");
3 const result_owner = @import("result.zig");
4 const top_types = @import("types.zig");
5
6 const QueryResult = result_owner.QueryResult;
7 const QueryOutcome = top_types.QueryOutcome;
8 const Span = top_types.SourceSpan;
9 const pretty_json = pretty.json;
10
11 pub fn writeQueryResult(result: *const QueryResult, writer: anytype) !void {
12 var stream = pretty_json.Writer.init(writer, .minified);
13 const object = try stream.object();
14 try writeQueryResultFields(result, object);
15 try object.endLine();
16 }
17
18 pub fn writeQueryResultFields(result: *const QueryResult, object: pretty_json.Object) !void {
19 const status: []const u8 = if (result.program_error)
20 "error"
21 else if (result.limit_reason != null)
22 "partial"
23 else if (result.outcomes.len == 0)
24 "error"
25 else
26 "success";
27
28 const outcomes = try object.array("outcomes");
29 for (result.outcomes) |outcome| {
30 const outcome_object = try outcomes.object();
31 try outcome_object.field("value", outcome.value_str);
32 try outcome_object.print("probability", "{d}", .{outcome.probability});
33 try outcome_object.end();
34 }
35 try outcomes.end();
36
37 const stats = try object.object("stats");
38 try stats.field("time_ns", result.stats.time_ns);
39 try stats.field("wmc_time_ns", result.stats.wmc_time_ns);
40 try stats.field("refinement_time_ns", result.stats.refinement_time_ns);
41 try stats.field("refinement_count", result.stats.refinement_count);
42 if (result.stats.num_forward_calls > 0) {
43 try stats.field("forward_calls", result.stats.num_forward_calls);
44 }
45 if (result.stats.num_recursive_calls > 0) {
46 try stats.field("recursive_calls", result.stats.num_recursive_calls);
47 }
48 if (result.stats.variable_count > 0) {
49 try stats.field("bdd_variables", result.stats.variable_count);
50 }
51 if (result.stats.node_count > 0) {
52 try stats.field("bdd_nodes", result.stats.node_count);
53 }
54 const total_cache = result.stats.ite_cache_hits + result.stats.ite_cache_misses;
55 if (total_cache > 0) {
56 try stats.field("ite_cache_hits", result.stats.ite_cache_hits);
57 try stats.field("ite_cache_misses", result.stats.ite_cache_misses);
58 }
59 if (result.stats.unique_table_grows > 0) {
60 try stats.field("bdd_unique_table_grows", result.stats.unique_table_grows);
61 }
62 if (result.stats.ite_cache_grows > 0) {
63 try stats.field("ite_cache_grows", result.stats.ite_cache_grows);
64 }
65 const total_thunks = result.stats.thunk_reuse_hits + result.stats.thunk_reuse_misses;
66 if (total_thunks > 0) {
67 try stats.field("thunk_reuse_hits", result.stats.thunk_reuse_hits);
68 try stats.field("thunk_reuse_misses", result.stats.thunk_reuse_misses);
69 }
70 if (result.stats.thunk_evaluations > 0) {
71 try stats.field("thunk_evaluations", result.stats.thunk_evaluations);
72 try stats.field("thunk_cache_hits", result.stats.thunk_cache_hits);
73 }
74 if (result.stats.bdd_samples_len > 0) {
75 const samples = try stats.array("bdd_samples");
76 var i: usize = 0;
77 while (i < @as(usize, result.stats.bdd_samples_len)) : (i += 1) {
78 const sample = try samples.object();
79 try sample.field("forward_calls", result.stats.bdd_samples_forward_calls[i]);
80 try sample.field("bdd_variables", result.stats.bdd_samples_vars[i]);
81 try sample.field("bdd_nodes", result.stats.bdd_samples_nodes[i]);
82 try sample.end();
83 }
84 try samples.end();
85 }
86 try stats.end();
87 try object.field("program_error", result.program_error);
88 if (result.limit_reason) |reason| {
89 try object.field("limit_reason", @tagName(reason));
90 }
91 try object.field("status", status);
92 }
93
94 pub const JsonError = struct {
95 type: []const u8,
96 message: []const u8,
97 file: ?[]const u8 = null,
98 span: ?Span = null,
99
100 pub fn write(self: JsonError, writer: anytype) !void {
101 var stream = pretty_json.Writer.init(writer, .minified);
102 const object = try stream.object();
103 try object.field("type", self.type);
104 try object.field("message", self.message);
105 if (self.file) |f| {
106 try object.field("file", f);
107 }
108 if (self.span) |s| {
109 const span = try object.object("span");
110 const start = try span.object("start");
111 try start.field("line", s.start.line);
112 try start.field("column", s.start.column);
113 try start.field("offset", s.start.offset);
114 try start.end();
115 const end = try span.object("end");
116 try end.field("line", s.end.line);
117 try end.field("column", s.end.column);
118 try end.field("offset", s.end.offset);
119 try end.end();
120 try span.end();
121 }
122 try object.endLine();
123 }
124 };
125
126 test "writeQueryResult includes bdd stats and samples" {
127 const allocator = std.testing.allocator;
128 const outcomes = try allocator.alloc(QueryOutcome, 1);
129 outcomes[0] = .{
130 .value_str = try allocator.dupe(u8, "True"),
131 .probability = 0.5,
132 };
133
134 var result = QueryResult{
135 .outcomes = outcomes,
136 .stats = .{
137 .time_ns = 123,
138 .wmc_time_ns = 100,
139 .refinement_time_ns = 50,
140 .refinement_count = 2,
141 .num_forward_calls = 4,
142 .num_recursive_calls = 8,
143 .variable_count = 3,
144 .node_count = 10,
145 .ite_cache_hits = 5,
146 .ite_cache_misses = 2,
147 .bdd_samples_len = 1,
148 },
149 .limit_reason = null,
150 .program_error = false,
151 .allocator = allocator,
152 };
153 result.stats.bdd_samples_forward_calls[0] = 4;
154 result.stats.bdd_samples_vars[0] = 3;
155 result.stats.bdd_samples_nodes[0] = 10;
156 defer result.deinit();
157
158 var out_buf: [1024]u8 = undefined;
159 var out_stream = std.Io.Writer.fixed(&out_buf);
160 try writeQueryResult(&result, &out_stream);
161 const written = out_stream.buffered();
162
163 try std.testing.expect(std.mem.indexOf(u8, written, "\"wmc_time_ns\":100") != null);
164 try std.testing.expect(std.mem.indexOf(u8, written, "\"bdd_nodes\":10") != null);
165 try std.testing.expect(std.mem.indexOf(u8, written, "\"bdd_samples\"") != null);
166 }
167
168 test "writeQueryResult includes program_error and limit_reason fields" {
169 const allocator = std.testing.allocator;
170 const outcomes = try allocator.alloc(QueryOutcome, 1);
171 outcomes[0] = .{
172 .value_str = try allocator.dupe(u8, "True"),
173 .probability = 1.0,
174 };
175
176 var result = QueryResult{
177 .outcomes = outcomes,
178 .stats = .{},
179 .limit_reason = .factor_weight_too_complex,
180 .program_error = false,
181 .allocator = allocator,
182 };
183 defer result.deinit();
184
185 var out_buf: [1024]u8 = undefined;
186 var out_stream = std.Io.Writer.fixed(&out_buf);
187 try writeQueryResult(&result, &out_stream);
188 const written = out_stream.buffered();
189
190 try std.testing.expect(std.mem.indexOf(u8, written, "\"program_error\":false") != null);
191 try std.testing.expect(std.mem.indexOf(u8, written, "\"limit_reason\":\"factor_weight_too_complex\"") != null);
192 try std.testing.expect(std.mem.indexOf(u8, written, "\"status\":\"partial\"") != null);
193 }
194
195 test "JsonError includes span when present" {
196 var buf: [512]u8 = undefined;
197 var writer = std.Io.Writer.fixed(&buf);
198
199 const span = Span{
200 .start = .{ .line = 0, .column = 1, .offset = 2 },
201 .end = .{ .line = 0, .column = 2, .offset = 3 },
202 };
203
204 const err = JsonError{
205 .type = "eval_error",
206 .message = "oops\n\"quoted\"",
207 .span = span,
208 };
209
210 try err.write(&writer);
211 try std.testing.expectEqualStrings(
212 "{\"type\":\"eval_error\",\"message\":\"oops\\n\\\"quoted\\\"\",\"span\":{\"start\":{\"line\":0,\"column\":1,\"offset\":2},\"end\":{\"line\":0,\"column\":2,\"offset\":3}}}\n",
213 writer.buffered(),
214 );
215 }