Merge pull request #53 from scalexm/overflow-panic

Panic on overflow

Author: nikomatsakis

src/bin/chalki.rs

@@ -11,7 +11,7 @@ use std::sync::Arc;
 
 use chalk::ir;
 use chalk::lower::*;
-use chalk::solve::solver::{Solver, CycleStrategy};
+use chalk::solve::solver::{self, Solver, CycleStrategy};
 
 use rustyline::error::ReadlineError;
 
@@ -44,6 +44,10 @@ impl Program {
 quick_main!(run);
 
 fn run() -> Result<()> {
+    // Initialize global overflow depth before everything
+    let overflow_depth = 10;
+    solver::set_overflow_depth(overflow_depth);
+
     let mut prog = None;
     readline_loop(&mut rustyline::Editor::new(), "?- ", |rl, line| {
         if let Err(e) = process(line, rl, &mut prog) {
@@ -118,7 +122,7 @@ fn read_program(rl: &mut rustyline::Editor<()>) -> Result<String> {
 
 fn goal(text: &str, prog: &Program) -> Result<()> {
     let goal = chalk_parse::parse_goal(text)?.lower(&*prog.ir)?;
-    let mut solver = Solver::new(&prog.env, CycleStrategy::Tabling);
+    let mut solver = Solver::new(&prog.env, CycleStrategy::Tabling, solver::get_overflow_depth());
     let goal = ir::InEnvironment::new(&ir::Environment::new(), *goal);
     match solver.solve_closed_goal(goal) {
         Ok(v) => println!("{}\n", v),

src/coherence/solve.rs

@@ -3,13 +3,17 @@ use std::sync::Arc;
 use itertools::Itertools;
 use errors::*;
 use ir::*;
-use solve::solver::{Solver, CycleStrategy};
+use solve::solver::{self, Solver, CycleStrategy};
 
 impl Program {
     pub(super) fn visit_specializations<F>(&self, mut record_specialization: F) -> Result<()>
         where F: FnMut(ItemId, ItemId)
     {
-        let mut solver = Solver::new(&Arc::new(self.environment()), CycleStrategy::Tabling);
+        let mut solver = Solver::new(
+            &Arc::new(self.environment()),
+            CycleStrategy::Tabling,
+            solver::get_overflow_depth()
+        );
 
         // Create a vector of references to impl datums, sorted by trait ref
         let impl_data = self.impl_data.iter().sorted_by(|&(_, lhs), &(_, rhs)| {

src/solve/solver.rs

@@ -3,6 +3,20 @@ use std::sync::Arc;
 
 use super::*;
 use solve::fulfill::Fulfill;
+use std::cell::Cell;
+
+thread_local! {
+    // Default overflow depth which will be used in tests
+    static OVERFLOW_DEPTH: Cell<usize> = Cell::new(10);
+}
+
+pub fn set_overflow_depth(overflow_depth: usize) {
+    OVERFLOW_DEPTH.with(|depth| depth.set(overflow_depth));
+}
+
+pub fn get_overflow_depth() -> usize {
+    OVERFLOW_DEPTH.with(|depth| depth.get())
+}
 
 /// We use a stack for detecting cycles. Each stack slot contains:
 /// - a goal which is being processed
@@ -31,6 +45,7 @@ pub struct Solver {
     pub(super) program: Arc<ProgramEnvironment>,
     stack: Vec<StackSlot>,
     cycle_strategy: CycleStrategy,
+    overflow_depth: usize,
 }
 
 /// An extension trait for merging `Result`s
@@ -52,11 +67,16 @@ impl<T> MergeWith<T> for Result<T> {
 }
 
 impl Solver {
-    pub fn new(program: &Arc<ProgramEnvironment>, cycle_strategy: CycleStrategy) -> Self {
+    pub fn new(
+        program: &Arc<ProgramEnvironment>,
+        cycle_strategy: CycleStrategy,
+        overflow_depth: usize
+    ) -> Self {
         Solver {
             program: program.clone(),
             stack: vec![],
             cycle_strategy,
+            overflow_depth,
         }
     }
 
@@ -105,6 +125,10 @@ impl Solver {
     pub fn solve_reduced_goal(&mut self, goal: FullyReducedGoal) -> Result<Solution> {
         debug_heading!("Solver::solve({:?})", goal);
 
+        if self.stack.len() > self.overflow_depth {
+            panic!("overflow depth reached");
+        }
+
         // If the goal is already on the stack, we found a cycle and indicate it by setting
         // `slot.cycle = true`. If there is no cached answer, we can't make any more progress
         // and return `Err`. If there is one, use this answer.

src/solve/test.rs

@@ -2,7 +2,7 @@ use chalk_parse;
 use errors::*;
 use ir;
 use lower::*;
-use solve::solver::{Solver, CycleStrategy};
+use solve::solver::{self, Solver, CycleStrategy};
 use std::sync::Arc;
 
 fn parse_and_lower_program(text: &str) -> Result<ir::Program> {
@@ -35,7 +35,7 @@ fn solve_goal(program_text: &str,
             assert!(goal_text.ends_with("}"));
             let goal = parse_and_lower_goal(&program, &goal_text[1..goal_text.len()-1]).unwrap();
 
-            let mut solver = Solver::new(&env, CycleStrategy::Tabling);
+            let mut solver = Solver::new(&env, CycleStrategy::Tabling, solver::get_overflow_depth());
             let goal = ir::InEnvironment::new(&ir::Environment::new(), *goal);
             let result = match solver.solve_closed_goal(goal) {
                 Ok(v) => format!("{}", v),
@@ -349,6 +349,30 @@ fn multiple_ambiguous_cycles() {
     }
 }
 
+#[test]
+#[should_panic]
+fn overflow() {
+    test! {
+        program {
+            trait Q { }
+            struct Z { }
+            struct G<X>
+            struct S<X>
+
+            impl Q for Z { }
+            impl<X> Q for G<X> where X: Q { }
+            impl<X> Q for S<X> where X: Q, S<G<X>>: Q { }
+        }
+
+        // Will try to prove S<G<Z>>: Q then S<G<G<Z>>>: Q etc ad infinitum
+        goal {
+            S<Z>: Q
+        } yields {
+            ""
+        }
+    }
+}
+
 #[test]
 fn normalize_basic() {
     test! {