From b62c379b97663d8125fda499c087a07ca3f9f987 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Tue, 19 May 2020 13:10:31 +0200 Subject: [PATCH] Properly handle input/output errors --- src/error.rs | 15 +++++++++++++++ src/problem.rs | 45 +++++++++++++++++++++++++++------------------ 2 files changed, 42 insertions(+), 18 deletions(-) diff --git a/src/error.rs b/src/error.rs index 0fc3f56..b5052a8 100644 --- a/src/error.rs +++ b/src/error.rs @@ -30,6 +30,7 @@ pub enum Kind // TODO: rename to something Vampire-specific ProveProgram(Option, String, String), ParseVampireOutput(String, String), + IO, } pub struct Error @@ -191,6 +192,11 @@ impl Error { Self::new(Kind::ParseVampireOutput(stdout, stderr)) } + + pub(crate) fn new_io>(source: S) -> Self + { + Self::new(Kind::IO).with(source) + } } impl std::fmt::Debug for Error @@ -275,6 +281,7 @@ impl std::fmt::Debug for Error {}\ ==== stderr ===========================================================\n\ {}", stdout, stderr), + Kind::IO => write!(formatter, "input/output error"), }?; if let Some(source) = &self.source @@ -305,3 +312,11 @@ impl std::error::Error for Error } } } + +impl From for Error +{ + fn from(error: std::io::Error) -> Self + { + Self::new_io(error) + } +} diff --git a/src/problem.rs b/src/problem.rs index 402081e..687de26 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -190,13 +190,16 @@ impl Problem } fn print_step_title(&self, step_title: &str, color: &termcolor::ColorSpec) + -> Result<(), crate::Error> { let longest_possible_key = " Finished"; self.shell.borrow_mut().print( &format!("{:>step_title_width$} ", step_title, step_title_width = longest_possible_key.chars().count()), - color); + color)?; + + Ok(()) } pub fn prove(&self, proof_direction: ProofDirection) -> Result<(), crate::Error> @@ -205,9 +208,9 @@ impl Problem || proof_direction == ProofDirection::Both { self.print_step_title("Started", - termcolor::ColorSpec::new().set_bold(true).set_fg(Some(termcolor::Color::Green))); + termcolor::ColorSpec::new().set_bold(true).set_fg(Some(termcolor::Color::Green)))?; self.shell.borrow_mut().println(&"verification of assertions from translated program", - &termcolor::ColorSpec::new()); + &termcolor::ColorSpec::new())?; let mut statements = self.statements.borrow_mut(); @@ -244,7 +247,7 @@ impl Problem ProofResult::Disproven => step_title_color.set_fg(Some(termcolor::Color::Red)), }; - self.print_step_title("Finished", &step_title_color); + self.print_step_title("Finished", &step_title_color)?; println!("verification of assertions from translated program"); } @@ -257,9 +260,9 @@ impl Problem || proof_direction == ProofDirection::Both { self.print_step_title("Started", - termcolor::ColorSpec::new().set_bold(true).set_fg(Some(termcolor::Color::Green))); + termcolor::ColorSpec::new().set_bold(true).set_fg(Some(termcolor::Color::Green)))?; self.shell.borrow_mut().println(&"verification of translated program from assertions", - &termcolor::ColorSpec::new()); + &termcolor::ColorSpec::new())?; let mut statements = self.statements.borrow_mut(); @@ -295,7 +298,7 @@ impl Problem ProofResult::Disproven => step_title_color.set_fg(Some(termcolor::Color::Red)), }; - self.print_step_title("Finished", &step_title_color); + self.print_step_title("Finished", &step_title_color)?; println!("verification of translated program from assertions"); } @@ -324,7 +327,7 @@ impl Problem fn prove_unproven_statements(&self) -> Result { - let display_statement = |statement: &Statement| + let display_statement = |statement: &Statement| -> Result<(), crate::Error> { let step_title = match statement.proof_status { @@ -349,10 +352,10 @@ impl Problem _ => step_title_color.set_fg(Some(termcolor::Color::Cyan)), }; - self.print_step_title(&step_title, &step_title_color); + self.print_step_title(&step_title, &step_title_color)?; self.shell.borrow_mut().print(&format!("{}: ", statement.kind), - &termcolor::ColorSpec::new()); + &termcolor::ColorSpec::new())?; let format_context = FormatContext { @@ -365,6 +368,8 @@ impl Problem }; print!("{}", foliage::format::display_formula(&statement.formula, &format_context)); + + Ok(()) }; // Show all statements that are assumed to be proven @@ -373,7 +378,7 @@ impl Problem for statement in statements.iter_mut() .filter(|statement| statement.proof_status == ProofStatus::AssumedProven) { - display_statement(statement); + display_statement(statement)?; println!(""); } } @@ -381,16 +386,18 @@ impl Problem loop { match self.next_unproven_statement_do_mut( - |statement| + |statement| -> Result<(), crate::Error> { statement.proof_status = ProofStatus::ToProveNow; print!("\x1b[s"); - display_statement(statement); + display_statement(statement)?; print!("\x1b[u"); use std::io::Write as _; - std::io::stdout().flush(); + std::io::stdout().flush()?; + + Ok(()) }) { Some(_) => (), @@ -412,7 +419,7 @@ impl Problem Some(&["--mode", "casc", "--cores", "8", "--time_limit", "300"]))?; match self.next_unproven_statement_do_mut( - |statement| + |statement| -> Result<(), crate::Error> { statement.proof_status = match proof_result { @@ -423,7 +430,7 @@ impl Problem self.shell.borrow_mut().erase_line(); - display_statement(statement); + display_statement(statement)?; match proof_result { @@ -435,15 +442,17 @@ impl Problem if let Some(proof_time_seconds) = proof_time_seconds { self.shell.borrow_mut().print(&format!(" in {} seconds", proof_time_seconds), - termcolor::ColorSpec::new().set_fg(Some(termcolor::Color::Black)).set_intense(true)); + termcolor::ColorSpec::new().set_fg(Some(termcolor::Color::Black)).set_intense(true))?; } + + Ok(()) }) { Some(_) => (), None => unreachable!(), } - self.shell.borrow_mut().println(&"", &termcolor::ColorSpec::new()); + self.shell.borrow_mut().println(&"", &termcolor::ColorSpec::new())?; if proof_result != ProofResult::Proven {