Make the verifier output even prettier (#599)

* Fix verifier printing to print instruction encodings consistently.

Use `FuncWriter::write_instruction` for all instructions so that
encodings are printed consistently.

* Make use-before-def errors mention the relevant value.

* When there are verifier errors, print a message at the end.

* Make verifier errors prettier.

Fix the length of the "^~~~~" to match the printed entity, and print the
error messsage on its own line.

* Clean up "test verifier" failure messages.

* Tidy the uses-value-from-itself error.

The use instruction is the same as the def instruction, so don't print
both. Also, the use instruction is already being printed at the
beginning, so don't print it again at the end.
This commit is contained in:
Dan Gohman
2018-11-26 22:18:18 -08:00
committed by GitHub
parent 737fde04a8
commit 54c388d870
4 changed files with 74 additions and 61 deletions

View File

@@ -23,6 +23,7 @@ pub fn pretty_verifier_error<'a>(
) -> String {
let mut errors = errors.0;
let mut w = String::new();
let num_errors = errors.len();
decorate_function(
&mut PrettyVerifierError(func_w.unwrap_or_else(|| Box::new(PlainWriter)), &mut errors),
@@ -30,6 +31,14 @@ pub fn pretty_verifier_error<'a>(
func,
isa,
).unwrap();
writeln!(
w,
"\n; {} verifier error{} detected (see above). Compilation aborted.",
num_errors,
if num_errors == 1 { "" } else { "s" }
).unwrap();
w
}
@@ -80,25 +89,31 @@ fn pretty_ebb_header_error(
func_w: &mut FuncWriter,
errors: &mut Vec<VerifierError>,
) -> fmt::Result {
let mut i = 0;
let mut printed_ebb = false;
let mut s = String::new();
func_w.write_ebb_header(&mut s, func, isa, cur_ebb, indent)?;
write!(w, "{}", s)?;
while i < errors.len() {
// TODO: Use drain_filter here when it gets stabilized
let mut i = 0;
let mut printed_error = false;
while i != errors.len() {
match errors[i].location {
ir::entities::AnyEntity::Ebb(ebb) if ebb == cur_ebb => {
if !printed_ebb {
func_w.write_ebb_header(w, func, isa, cur_ebb, indent)?;
printed_ebb = true;
if !printed_error {
print_arrow(w, &s)?;
printed_error = true;
}
let err = errors.remove(i);
print_error(w, indent, cur_ebb.to_string(), err)?;
}
_ => {
i += 1;
print_error(w, err)?;
}
_ => i += 1,
}
}
if printed_error {
w.write_char('\n')?;
}
Ok(())
}
@@ -113,35 +128,29 @@ fn pretty_instruction_error(
func_w: &mut FuncWriter,
errors: &mut Vec<VerifierError>,
) -> fmt::Result {
let mut s = String::new();
func_w.write_instruction(&mut s, func, aliases, isa, cur_inst, indent)?;
write!(w, "{}", s)?;
// TODO: Use drain_filter here when it gets stabilized
let mut i = 0;
let mut printed_instr = false;
let mut printed_error = false;
while i != errors.len() {
match errors[i].location {
ir::entities::AnyEntity::Inst(inst) if inst == cur_inst => {
if !printed_instr {
func_w.write_instruction(w, func, aliases, isa, cur_inst, indent)?;
printed_instr = true;
if !printed_error {
print_arrow(w, &s)?;
printed_error = true;
}
let err = errors.remove(i);
print_error(w, indent, cur_inst.to_string(), err)?;
print_error(w, err)?;
}
ir::entities::AnyEntity::Inst(_) => i += 1,
_ => unreachable!(),
_ => i += 1,
}
}
if printed_instr {
if printed_error {
w.write_char('\n')?;
} else {
writeln!(
w,
"{1:0$}{2}",
indent,
"",
func.dfg.display_inst(cur_inst, isa)
)?;
}
Ok(())
@@ -155,45 +164,54 @@ fn pretty_preamble_error(
func_w: &mut FuncWriter,
errors: &mut Vec<VerifierError>,
) -> fmt::Result {
let mut s = String::new();
func_w.write_entity_definition(&mut s, func, entity, value)?;
write!(w, "{}", s)?;
// TODO: Use drain_filter here when it gets stabilized
let indent = 4;
let mut i = 0;
let mut printed_entity = false;
let mut printed_error = false;
while i != errors.len() {
if entity == errors[i].location {
let err = errors.remove(i);
if !printed_entity {
func_w.write_entity_definition(w, func, entity, value)?;
printed_entity = true;
if !printed_error {
print_arrow(w, &s)?;
printed_error = true;
}
print_error(w, indent, entity.to_string(), err)?;
let err = errors.remove(i);
print_error(w, err)?;
} else {
i += 1
}
}
if printed_entity {
if printed_error {
w.write_char('\n')?;
} else {
func_w.write_entity_definition(w, func, entity, value)?;
}
Ok(())
}
/// Prints ; ^~~~~~ verifier [ERROR BODY]
fn print_error(w: &mut Write, indent: usize, s: String, err: VerifierError) -> fmt::Result {
let indent = if indent < 1 { 0 } else { indent - 1 };
/// Prints:
/// ; ^~~~~~
fn print_arrow(w: &mut Write, entity: &str) -> fmt::Result {
write!(w, ";")?;
write!(w, ";{1:0$}^", indent, "")?;
for _c in s.chars() {
let indent = entity.len() - entity.trim_start().len();
if indent != 0 {
write!(w, "{1:0$}^", indent - 1, "")?;
}
for _ in 0..entity.trim().len() - 1 {
write!(w, "~")?;
}
writeln!(w, " verifier {}", err.to_string())?;
writeln!(w)
}
/// Prints:
/// ; error: [ERROR BODY]
fn print_error(w: &mut Write, err: VerifierError) -> fmt::Result {
writeln!(w, "; error: {}", err.to_string())?;
Ok(())
}

View File

@@ -861,18 +861,13 @@ impl<'a> Verifier<'a> {
return fatal!(
errors,
loc_inst,
"uses value from non-dominating {}",
"uses value {} from non-dominating {}",
v,
def_inst
);
}
if def_inst == loc_inst {
return fatal!(
errors,
loc_inst,
"uses value from itself {}, {}",
def_inst,
loc_inst
);
return fatal!(errors, loc_inst, "uses value {} from itself", v);
}
}
}