Skip to content

Commit 6197986

Browse files
SeRin-YangSeRin-Yang
committed
Update check_proof_assuming to return Result for error handling
1 parent 9a0db09 commit 6197986

File tree

6 files changed

+81
-66
lines changed

6 files changed

+81
-66
lines changed

‎src/main.rs‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ use tokio::task::JoinError;
3939
use tracing::{error, info, warn};
4040

4141
use vc::explain::VcExplanation;
42-
use z3rro::{prover::ProveResult, util::ReasonUnknown};
42+
use z3rro::{prover::{ProveResult, ProverCommandError}, util::ReasonUnknown};
4343

4444
pub mod ast;
4545
mod driver;
@@ -541,6 +541,10 @@ fn finalize_verify_result(
541541
tracing::error!("Interrupted");
542542
ExitCode::from(130) // 130 seems to be a standard exit code for CTRL+C
543543
}
544+
Err(VerifyError::ProverError(err)) => {
545+
eprintln!("{}", err.to_string());
546+
ExitCode::from(1)
547+
}
544548
}
545549
}
546550

@@ -620,6 +624,8 @@ pub enum VerifyError {
620624
/// The verifier was interrupted.
621625
#[error("interrupted")]
622626
Interrupted,
627+
#[error("{0}")]
628+
ProverError(#[from] ProverCommandError),
623629
}
624630

625631
/// Verify a list of `user_files`. The `options.files` value is ignored here.

‎src/opt/fuzz_test.rs‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -207,13 +207,16 @@ fn prove_equiv(expr: Expr, optimized: Expr, tcx: &TyCtx) -> TestCaseResult {
207207
.add_assumptions_to_prover(&mut prover);
208208
prover.add_provable(&eq_expr_z3);
209209
let x = match prover.check_proof() {
210-
ProveResult::Proof => Ok(()),
211-
ProveResult::Counterexample(model) => Err(TestCaseError::fail(format!(
210+
Ok(ProveResult::Proof) => Ok(()),
211+
Ok(ProveResult::Counterexample(model)) => Err(TestCaseError::fail(format!(
212212
"rewrote {} ...into... {}, but those are not equivalent:\n{}",
213213
expr, optimized, model
214214
))),
215-
ProveResult::Unknown(reason) => {
215+
Ok(ProveResult::Unknown(reason)) => {
216216
Err(TestCaseError::fail(format!("unknown result ({})", reason)))
217+
},
218+
Err(err) => {
219+
Err(TestCaseError::fail(format!("{}", err)))
217220
}
218221
};
219222
x

‎src/slicing/solver.rs‎

Lines changed: 36 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,13 @@ use z3::{
77
};
88
use z3rro::{
99
model::InstrumentedModel,
10-
prover::{ProveResult, Prover},
10+
prover::{ProveResult, Prover, ProverCommandError},
1111
util::ReasonUnknown,
1212
};
1313

1414
use crate::{
1515
ast::{ExprBuilder, Span},
16-
resource_limits::{LimitError, LimitsRef},
16+
resource_limits::LimitsRef,
1717
slicing::{
1818
model::{SliceMode, SliceModel},
1919
util::{PartialMinimizeResult, SubsetExploration},
@@ -232,7 +232,7 @@ impl<'ctx> SliceSolver<'ctx> {
232232
.check_proof_assuming(&active_toggle_values);
233233

234234
let mut slice_searcher = SliceModelSearch::new(active_toggle_values.clone());
235-
if let ProveResult::Proof = res {
235+
if let Ok(ProveResult::Proof) = res {
236236
slice_searcher.found_active(self.prover.get_unsat_core());
237237
}
238238

@@ -322,14 +322,18 @@ impl<'ctx> SliceSolver<'ctx> {
322322

323323
slice_sat_binary_search(&mut self.prover, &active_toggle_values, options, limits_ref)?;
324324
let res = self.prover.check_proof();
325-
let slice_model = if let ProveResult::Counterexample(model) = &res {
326-
let slice_model =
327-
SliceModel::from_model(SliceMode::Error, &self.slice_stmts, selection, model);
328-
Some(slice_model)
329-
} else {
330-
None
331-
};
332-
Ok((res, slice_model))
325+
326+
match res {
327+
Err(err) => Err(VerifyError::ProverError(err)),
328+
Ok(prove_result) => match &prove_result {
329+
ProveResult::Counterexample(model) => {
330+
let slice_model =
331+
SliceModel::from_model(SliceMode::Error, &self.slice_stmts, selection, &model);
332+
Ok((prove_result, Some(slice_model)))
333+
},
334+
_ => Ok((prove_result, None)),
335+
}
336+
}
333337
}
334338
}
335339

@@ -551,36 +555,39 @@ pub fn slice_next_extremal_set<'ctx>(
551555
prover: &mut Prover<'ctx>,
552556
options: &SliceSolveOptions,
553557
limits_ref: &LimitsRef,
554-
) -> Result<Option<ExtremalSet<'ctx>>, LimitError> {
558+
) -> Result<Option<ExtremalSet<'ctx>>, VerifyError> {
555559
let all_variables = exploration.variables().clone();
556560

557561
while let Some(seed) = exploration.next_set() {
558562
limits_ref.check_limits()?;
559563

560564
match check_proof_seed(prover, limits_ref, &seed) {
561-
ProveResult::Proof => {
565+
Ok(ProveResult::Proof) => {
562566
let seed = unsat_core_to_seed(prover, &all_variables);
563567

564568
// now start the shrinking, then block up
565-
let res = exploration.shrink_block_up(seed, |seed| {
566-
match check_proof_seed(prover, limits_ref, seed) {
567-
ProveResult::Proof => Some(unsat_core_to_seed(prover, &all_variables)),
568-
ProveResult::Counterexample(_) | ProveResult::Unknown(_) => None,
569-
}
570-
});
569+
let res_seed = match check_proof_seed(prover, limits_ref, &seed) {
570+
Ok(ProveResult::Proof) => Some(unsat_core_to_seed(prover, &all_variables)),
571+
Ok(ProveResult::Counterexample(_)) | Ok(ProveResult::Unknown(_)) => None,
572+
Err(err) => return Err(VerifyError::ProverError(err)),
573+
};
574+
575+
let res = exploration.shrink_block_up(seed, |_| res_seed.clone());
571576
return Ok(Some(ExtremalSet::MinimalUnsat(res)));
572577
}
573-
ProveResult::Counterexample(_) => {
578+
Ok(ProveResult::Counterexample(_)) => {
574579
// grow the counterexample and then block down
575-
let res = exploration.grow_block_down(seed, |seed| {
576-
match check_proof_seed(prover, limits_ref, seed) {
577-
ProveResult::Counterexample(_) => true,
578-
ProveResult::Proof | ProveResult::Unknown(_) => false,
579-
}
580-
});
580+
581+
let res_seed = match check_proof_seed(prover, limits_ref, &seed) {
582+
Ok(ProveResult::Counterexample(_)) => true,
583+
Ok(ProveResult::Proof) | Ok(ProveResult::Unknown(_)) => false,
584+
Err(err) => return Err(VerifyError::ProverError(err)),
585+
};
586+
587+
let res = exploration.grow_block_down(seed, |_| res_seed);
581588
return Ok(Some(ExtremalSet::MaximalSat(res)));
582589
}
583-
ProveResult::Unknown(_) => {
590+
Ok(ProveResult::Unknown(_)) => {
584591
if options.continue_on_unknown {
585592
// for seeds that result in unknown, just block them to
586593
// ensure progress.
@@ -589,6 +596,7 @@ pub fn slice_next_extremal_set<'ctx>(
589596
return Ok(None);
590597
}
591598
}
599+
Err(err) => return Err(VerifyError::ProverError(err)),
592600
}
593601
}
594602
Ok(None)
@@ -599,7 +607,7 @@ fn check_proof_seed<'ctx>(
599607
prover: &mut Prover<'ctx>,
600608
limits_ref: &LimitsRef,
601609
seed: &HashSet<Bool<'ctx>>,
602-
) -> ProveResult<'ctx> {
610+
) -> Result<ProveResult<'ctx>, ProverCommandError> {
603611
let mut timeout = Duration::from_millis(100);
604612
if let Some(time_left) = limits_ref.time_left() {
605613
timeout = timeout.min(time_left);

‎src/slicing/transform_test.rs‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -138,14 +138,15 @@ fn prove_equiv(
138138
}
139139
prover.add_provable(&eq_expr_z3);
140140
let x = match prover.check_proof() {
141-
ProveResult::Proof => Ok(()),
142-
ProveResult::Counterexample(model) => Err(format!(
141+
Ok(ProveResult::Proof) => Ok(()),
142+
Ok(ProveResult::Counterexample(model)) => Err(format!(
143143
"we want to rewrite {:?} ...into... {:?} under assumptions {:?}, but those are not equivalent:\n{}\n original evaluates to {}\n rewritten evaluates to {}",
144144
stmt1, stmt2, assumptions, model, translate.t_eureal(&stmt1_vc).eval(&model).unwrap(), translate.t_eureal(&stmt2_vc).eval(&model).unwrap()
145145
)),
146-
ProveResult::Unknown(reason) => {
146+
Ok(ProveResult::Unknown(reason)) => {
147147
Err(format!("unknown result ({})", reason))
148-
}
148+
},
149+
Err(err) => Err(format!("{}", err))
149150
};
150151
x
151152
}

‎z3rro/src/prover.rs‎

Lines changed: 23 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ use std::{
77
fmt::Display,
88
io::{self, Write},
99
path::Path,
10-
process::{self, Command},
10+
process::Command,
1111
time::Duration,
1212
};
1313

@@ -25,7 +25,7 @@ use crate::{
2525
};
2626

2727
#[derive(Debug, Error)]
28-
pub enum CommandError {
28+
pub enum ProverCommandError {
2929
#[error("Environment variable error: {0}")]
3030
EnvVarError(#[from] env::VarError),
3131
#[error("Process execution failed: {0}")]
@@ -47,7 +47,7 @@ pub enum ProveResult<'ctx> {
4747
}
4848

4949
/// Execute swine on the file located at file_path
50-
fn execute_swine(file_path: &Path) -> Result<SatResult, CommandError> {
50+
fn execute_swine(file_path: &Path) -> Result<SatResult, ProverCommandError> {
5151
let output = Command::new("swine").arg(file_path).output();
5252

5353
match output {
@@ -62,7 +62,7 @@ fn execute_swine(file_path: &Path) -> Result<SatResult, CommandError> {
6262
Ok(SatResult::Unknown)
6363
}
6464
}
65-
Err(e) => Err(CommandError::ProcessError(e)),
65+
Err(e) => Err(ProverCommandError::ProcessError(e)),
6666
}
6767
}
6868

@@ -161,7 +161,7 @@ impl<'ctx> Prover<'ctx> {
161161
self.min_level_with_provables.get_or_insert(self.level);
162162
}
163163

164-
pub fn check_proof(&mut self) -> ProveResult<'ctx> {
164+
pub fn check_proof(&mut self) -> Result<ProveResult<'ctx>, ProverCommandError> {
165165
self.check_proof_assuming(&[])
166166
}
167167

@@ -170,13 +170,11 @@ impl<'ctx> Prover<'ctx> {
170170
pub fn check_proof_assuming(
171171
&mut self,
172172
assumptions: &[Bool<'ctx>],
173-
) -> ProveResult<'ctx> {
173+
) -> Result<ProveResult<'ctx>, ProverCommandError> {
174174
if self.min_level_with_provables.is_none() {
175-
return ProveResult::Proof;
175+
return Ok(ProveResult::Proof);
176176
}
177177

178-
let res;
179-
180178
match self.smt_solver {
181179
SolverType::SWINE => {
182180
let mut smtlib = self.get_smtlib();
@@ -188,35 +186,33 @@ impl<'ctx> Prover<'ctx> {
188186
.unwrap();
189187
let file_path = smt_file.path();
190188

191-
res = execute_swine(file_path).unwrap_or_else(|e| {
192-
eprintln!("{}", e);
193-
process::exit(1)
194-
});
189+
let res = execute_swine(file_path);
195190
match res {
196-
SatResult::Unsat => ProveResult::Proof,
197-
SatResult::Unknown => {
191+
Ok(SatResult::Unsat) => Ok(ProveResult::Proof),
192+
Ok(SatResult::Unknown) => {
198193
// TODO: Determine the correct reason for Unknown
199-
ProveResult::Unknown(ReasonUnknown::Other("unknown".to_string()))
200-
}
201-
SatResult::Sat => {
194+
Ok(ProveResult::Unknown(ReasonUnknown::Other("unknown".to_string())))
195+
},
196+
Ok(SatResult::Sat) => {
202197
// TODO: Get the model from the output of SWINE
203-
process::exit(1)
204-
}
198+
panic!("no counterexample for swine")
199+
},
200+
Err(err) => Err(err)
205201
}
206202
}
207203
SolverType::Z3 => {
208-
res = if assumptions.is_empty() {
204+
let res = if assumptions.is_empty() {
209205
self.solver.check()
210206
} else {
211207
self.solver.check_assumptions(assumptions)
212208
};
213209
match res {
214-
SatResult::Unsat => ProveResult::Proof,
215-
SatResult::Unknown => ProveResult::Unknown(self.get_reason_unknown().unwrap()),
210+
SatResult::Unsat => Ok(ProveResult::Proof),
211+
SatResult::Unknown => Ok(ProveResult::Unknown(self.get_reason_unknown().unwrap())),
216212
SatResult::Sat => {
217213
let model = self.get_model().unwrap();
218214
let model = InstrumentedModel::new(model);
219-
ProveResult::Counterexample(model)
215+
Ok(ProveResult::Counterexample(model))
220216
}
221217
}
222218
}
@@ -315,16 +311,16 @@ mod test {
315311
fn test_prover() {
316312
let ctx = Context::new(&Config::default());
317313
let mut prover = Prover::new(&ctx, SolverType::Z3);
318-
assert!(matches!(prover.check_proof(), ProveResult::Proof));
314+
assert!(matches!(prover.check_proof(), Ok(ProveResult::Proof)));
319315
assert_eq!(prover.check_sat(), SatResult::Sat);
320316

321317
prover.push();
322318
prover.add_assumption(&Bool::from_bool(&ctx, true));
323-
assert!(matches!(prover.check_proof(), ProveResult::Proof));
319+
assert!(matches!(prover.check_proof(), Ok(ProveResult::Proof)));
324320
assert_eq!(prover.check_sat(), SatResult::Sat);
325321
prover.pop();
326322

327-
assert!(matches!(prover.check_proof(), ProveResult::Proof));
323+
assert!(matches!(prover.check_proof(), Ok(ProveResult::Proof)));
328324
assert_eq!(prover.check_sat(), SatResult::Sat);
329325
}
330326
}

‎z3rro/src/test.rs‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -28,13 +28,14 @@ pub fn test_prove(f: impl for<'ctx> FnOnce(&'ctx Context, &mut SmtScope<'ctx>) -
2828

2929
prover.add_provable(&theorem);
3030
match prover.check_proof() {
31-
ProveResult::Counterexample(model) => panic!(
31+
Ok(ProveResult::Counterexample(model)) => panic!(
3232
"counter-example: {:?}\nsolver:\n{:?}",
3333
model,
3434
prover.solver()
3535
),
36-
ProveResult::Unknown(reason) => panic!("solver returned unknown ({})", reason),
37-
ProveResult::Proof => {}
36+
Ok(ProveResult::Unknown(reason)) => panic!("solver returned unknown ({})", reason),
37+
Ok(ProveResult::Proof) => {},
38+
Err(_) => {}
3839
};
3940
}
4041

0 commit comments

Comments
 (0)