From 750b17912bcb3ec259596ca323daae74528853e3 Mon Sep 17 00:00:00 2001 From: Christian Poveda Date: Fri, 23 Aug 2019 04:48:29 -0500 Subject: [PATCH 1/3] Better logging for sire --- src/librustc_interface/passes.rs | 74 ++++++++++++++++++++------------ src/sire | 2 +- 2 files changed, 47 insertions(+), 29 deletions(-) diff --git a/src/librustc_interface/passes.rs b/src/librustc_interface/passes.rs index 43b64d424473c..b747f58e90f8e 100644 --- a/src/librustc_interface/passes.rs +++ b/src/librustc_interface/passes.rs @@ -804,43 +804,61 @@ pub fn default_provide(providers: &mut ty::query::Providers<'_>) { let mut evaluator = Evaluator::from_tcx(tcx); - if let (ConstValue::Unevaluated(def_id_a, _ ), ConstValue::Unevaluated(def_id_b, _)) = (a.val, b.val) { - info!("sire: Both sides are unevaluated"); - if def_id_a == def_id_b { - info!("sire: DefIds are equal"); - return true; - } - if let (Ok(sir_a), Ok(sir_b)) = (evaluator.eval_mir(def_id_a), evaluator.eval_mir(def_id_b)) { - match check_equality(&sir_a, &sir_b) { - Ok(result) => match result { - CheckResult::Sat => { - info!("sire: Both sides are equal"); - true - } - CheckResult::Unsat => { - info!("sire: Sides are not equal"); - false - } - CheckResult::Undecided => { - warn!("sire: Could not decide if sides are equal"); - false - } - CheckResult::Unknown(output) => { - warn!("sire: SMT returned an unknown output {}", output); - false + if let ConstValue::Unevaluated(def_id_a, _ ) = a.val { + if let ConstValue::Unevaluated(def_id_b, _) = b.val { + info!("sire: Both sides are unevaluated"); + if def_id_a == def_id_b { + info!("sire: DefIds are equal"); + return true; + } + match evaluator.eval_mir(def_id_a) { + Ok(sir_a) => { + info!("sire: Evaluation was successful: {}", sir_a); + match evaluator.eval_mir(def_id_b) { + Ok(sir_b) => { + info!("sire: Evaluation was successful: {}", sir_b); + match check_equality(&sir_a, &sir_b) { + Ok(result) => match result { + CheckResult::Sat => { + info!("sire: Both sides are equal"); + true + } + CheckResult::Unsat => { + info!("sire: Sides are not equal"); + false + } + CheckResult::Undecided => { + warn!("sire: Could not decide if sides are equal"); + false + } + CheckResult::Unknown(output) => { + warn!("sire: SMT returned an unknown output {}", output); + false + } + } + Err(error) => { + warn!("sire: SMT failed: {}", error); + false + } + } + } + Err(e) => { + warn!("sire: Evaluation failed: {}", e); + false + } } } - Err(error) => { - warn!("sire: SMT failed {}", error); + Err(e) => { + warn!("sire: Evaluation failed: {}", e); false } } } else { - warn!("sire: Cannot evaluate functions"); + warn!("sire: {} is evaluated", b); false } } else { - warn!("sire: One of the sides is evaluated"); + warn!("sire: {} is evaluated", a); false } }; diff --git a/src/sire b/src/sire index 9bf7e4db232e8..0d64968570d48 160000 --- a/src/sire +++ b/src/sire @@ -1 +1 @@ -Subproject commit 9bf7e4db232e890ca23426a0e888e06749844338 +Subproject commit 0d64968570d48c17253c4518e1ac386801c728cb From 6c29589aa534bd860ed3d4158bdb6d39544777f0 Mon Sep 17 00:00:00 2001 From: Christian Poveda Date: Fri, 23 Aug 2019 23:07:38 -0500 Subject: [PATCH 2/3] Update sire version --- src/sire | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sire b/src/sire index 0d64968570d48..a1b140c4235ac 160000 --- a/src/sire +++ b/src/sire @@ -1 +1 @@ -Subproject commit 0d64968570d48c17253c4518e1ac386801c728cb +Subproject commit a1b140c4235acde1501065624b71f53c6dc3194c From 866be8d928a0636d8122bc4438f068328607c080 Mon Sep 17 00:00:00 2001 From: Christian Poveda Date: Sun, 25 Aug 2019 02:32:14 -0500 Subject: [PATCH 3/3] Support assertions properly --- src/sire | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sire b/src/sire index a1b140c4235ac..03282974dd5ae 160000 --- a/src/sire +++ b/src/sire @@ -1 +1 @@ -Subproject commit a1b140c4235acde1501065624b71f53c6dc3194c +Subproject commit 03282974dd5aecc92d01ade80b57fb87fa50ca6a