1use crate::entity::SecondaryMap;
4use crate::ir;
5use crate::ir::entities::{AnyEntity, Block, Inst, Value};
6use crate::ir::function::Function;
7use crate::ir::pcc::Fact;
8use crate::result::CodegenError;
9use crate::verifier::{VerifierError, VerifierErrors};
10use crate::write::{decorate_function, FuncWriter, PlainWriter};
11use alloc::boxed::Box;
12use alloc::string::{String, ToString};
13use alloc::vec::Vec;
14use core::fmt;
15use core::fmt::Write;
16
17pub fn pretty_verifier_error<'a>(
19 func: &ir::Function,
20 func_w: Option<Box<dyn FuncWriter + 'a>>,
21 errors: VerifierErrors,
22) -> String {
23 let mut errors = errors.0;
24 let mut w = String::new();
25 let num_errors = errors.len();
26
27 decorate_function(
28 &mut PrettyVerifierError(func_w.unwrap_or_else(|| Box::new(PlainWriter)), &mut errors),
29 &mut w,
30 func,
31 )
32 .unwrap();
33
34 writeln!(
35 w,
36 "\n; {} verifier error{} detected (see above). Compilation aborted.",
37 num_errors,
38 if num_errors == 1 { "" } else { "s" }
39 )
40 .unwrap();
41
42 w
43}
44
45struct PrettyVerifierError<'a>(Box<dyn FuncWriter + 'a>, &'a mut Vec<VerifierError>);
46
47impl<'a> FuncWriter for PrettyVerifierError<'a> {
48 fn write_block_header(
49 &mut self,
50 w: &mut dyn Write,
51 func: &Function,
52 block: Block,
53 indent: usize,
54 ) -> fmt::Result {
55 pretty_block_header_error(w, func, block, indent, &mut *self.0, self.1)
56 }
57
58 fn write_instruction(
59 &mut self,
60 w: &mut dyn Write,
61 func: &Function,
62 aliases: &SecondaryMap<Value, Vec<Value>>,
63 inst: Inst,
64 indent: usize,
65 ) -> fmt::Result {
66 pretty_instruction_error(w, func, aliases, inst, indent, &mut *self.0, self.1)
67 }
68
69 fn write_entity_definition(
70 &mut self,
71 w: &mut dyn Write,
72 func: &Function,
73 entity: AnyEntity,
74 value: &dyn fmt::Display,
75 maybe_fact: Option<&Fact>,
76 ) -> fmt::Result {
77 pretty_preamble_error(w, func, entity, value, maybe_fact, &mut *self.0, self.1)
78 }
79}
80
81fn pretty_block_header_error(
83 w: &mut dyn Write,
84 func: &Function,
85 cur_block: Block,
86 indent: usize,
87 func_w: &mut dyn FuncWriter,
88 errors: &mut Vec<VerifierError>,
89) -> fmt::Result {
90 let mut s = String::new();
91 func_w.write_block_header(&mut s, func, cur_block, indent)?;
92 write!(w, "{s}")?;
93
94 let mut i = 0;
96 let mut printed_error = false;
97 while i != errors.len() {
98 match errors[i].location {
99 ir::entities::AnyEntity::Block(block) if block == cur_block => {
100 if !printed_error {
101 print_arrow(w, &s)?;
102 printed_error = true;
103 }
104 let err = errors.remove(i);
105 print_error(w, err)?;
106 }
107 _ => i += 1,
108 }
109 }
110
111 if printed_error {
112 w.write_char('\n')?;
113 }
114
115 Ok(())
116}
117
118fn pretty_instruction_error(
120 w: &mut dyn Write,
121 func: &Function,
122 aliases: &SecondaryMap<Value, Vec<Value>>,
123 cur_inst: Inst,
124 indent: usize,
125 func_w: &mut dyn FuncWriter,
126 errors: &mut Vec<VerifierError>,
127) -> fmt::Result {
128 let mut s = String::new();
129 func_w.write_instruction(&mut s, func, aliases, cur_inst, indent)?;
130 write!(w, "{s}")?;
131
132 let mut i = 0;
134 let mut printed_error = false;
135 while i != errors.len() {
136 match errors[i].location {
137 ir::entities::AnyEntity::Inst(inst) if inst == cur_inst => {
138 if !printed_error {
139 print_arrow(w, &s)?;
140 printed_error = true;
141 }
142 let err = errors.remove(i);
143 print_error(w, err)?;
144 }
145 _ => i += 1,
146 }
147 }
148
149 if printed_error {
150 w.write_char('\n')?;
151 }
152
153 Ok(())
154}
155
156fn pretty_preamble_error(
157 w: &mut dyn Write,
158 func: &Function,
159 entity: AnyEntity,
160 value: &dyn fmt::Display,
161 maybe_fact: Option<&Fact>,
162 func_w: &mut dyn FuncWriter,
163 errors: &mut Vec<VerifierError>,
164) -> fmt::Result {
165 let mut s = String::new();
166 func_w.write_entity_definition(&mut s, func, entity, value, maybe_fact)?;
167 write!(w, "{s}")?;
168
169 let mut i = 0;
171 let mut printed_error = false;
172 while i != errors.len() {
173 if entity == errors[i].location {
174 if !printed_error {
175 print_arrow(w, &s)?;
176 printed_error = true;
177 }
178 let err = errors.remove(i);
179 print_error(w, err)?;
180 } else {
181 i += 1
182 }
183 }
184
185 if printed_error {
186 w.write_char('\n')?;
187 }
188
189 Ok(())
190}
191
192fn print_arrow(w: &mut dyn Write, entity: &str) -> fmt::Result {
195 write!(w, ";")?;
196
197 let indent = entity.len() - entity.trim_start().len();
198 if indent != 0 {
199 write!(w, "{1:0$}^", indent - 1, "")?;
200 }
201
202 for _ in 0..entity.trim().len() - 1 {
203 write!(w, "~")?;
204 }
205
206 writeln!(w)
207}
208
209fn print_error(w: &mut dyn Write, err: VerifierError) -> fmt::Result {
212 writeln!(w, "; error: {}", err.to_string())?;
213 Ok(())
214}
215
216pub fn pretty_error(func: &ir::Function, err: CodegenError) -> String {
218 if let CodegenError::Verifier(e) = err {
219 pretty_verifier_error(func, None, e)
220 } else {
221 err.to_string()
222 }
223}