Merge pull request rust-lang#19 from Chris-Hawblitzel/mutual-recursion

Add support for mutual recursion

verify/rust_verify/example/recursion.rs

@@ -12,13 +12,6 @@ fn arith_sum_int(i: int) -> int {
     if i <= 0 { 0 } else { i + arith_sum_int(i - 1) }
 }
 
-#[spec]
-fn arith_sum_nat(i: nat) -> nat {
-    decreases(i);
-
-    if i == 0 { 0 } else { i + arith_sum_nat(i - 1) }
-}
-
 #[spec]
 #[opaque]
 fn arith_sum_u64(i: u64) -> u64 {
@@ -40,13 +33,17 @@ fn arith_sum_int_nonneg(i: nat) {
 #[proof]
 fn arith_sum_test1() {
     assert(arith_sum_int(0) == 0);
-    assert(arith_sum_int(1) == 1);
+    // Recursive functions default to 1 fuel, so without the assert above,
+    // the following assert will fail
+    assert(arith_sum_int(1) == 1);  
     assert(arith_sum_int(2) == 3);
     assert(arith_sum_int(3) == 6);
 }
 
 #[proof]
 fn arith_sum_test2() {
+    // Instead of writing out intermediate assertions, 
+    // we can instead boost the fuel setting
     reveal_with_fuel(arith_sum_int, 4);
     assert(arith_sum_int(3) == 6);
 }
@@ -56,3 +53,4 @@ fn arith_sum_test3() {
     reveal_with_fuel(arith_sum_u64, 4);
     assert(arith_sum_u64(3) == 6);
 }
+

verify/rust_verify/src/verifier.rs

@@ -208,6 +208,18 @@ impl Verifier {
             Self::check_internal_result(air_context.command(&command));
         }
 
+        // Pre-declare the function symbols, to allow for the possibility of non-sorted function usage
+        for function in &krate.functions {
+            let commands = vir::func_to_air::func_name_to_air(&ctx, &function)?;
+            if commands.len() > 0 {
+                air_context.blank_line();
+                air_context.comment(&("Function-PreDecl ".to_string() + &function.x.name));
+            }
+            for command in commands.iter() {
+                self.check_result_validity(compiler, &command, air_context.command(&command));
+            }
+        }
+
         for function in &krate.functions {
             let commands = vir::func_to_air::func_decl_to_air(&ctx, &function)?;
             if commands.len() > 0 {

verify/rust_verify/tests/common/mod.rs

@@ -128,3 +128,10 @@ pub fn assert_one_fails(err: Vec<(Option<ErrorSpan>, Option<ErrorSpan>)>) {
     assert_eq!(err.len(), 1);
     assert!(err[0].0.as_ref().expect("span").test_span_line.contains("FAILS"));
 }
+
+#[allow(dead_code)]
+pub fn assert_two_fails(err: Vec<(Option<ErrorSpan>, Option<ErrorSpan>)>) {
+    assert_eq!(err.len(), 2);
+    assert!(err[0].0.as_ref().expect("span").test_span_line.contains("FAILS"));
+    assert!(err[1].0.as_ref().expect("span").test_span_line.contains("FAILS"));
+}

verify/rust_verify/tests/recursion.rs

@@ -0,0 +1,244 @@
+#![feature(rustc_private)]
+#[macro_use]
+mod common;
+use common::*;
+
+test_verify_with_pervasive! {
+    #[test] basic_correctness_expr code! {
+        #[spec]
+        fn arith_sum_nat(i: nat) -> nat {
+            decreases(i);
+
+            if i == 0 { 0 } else { i + arith_sum_nat(i - 1) }
+        }
+    } => Ok(())
+}
+
+test_verify_with_pervasive! {
+    #[test] basic_correctness_stmt code! {
+        #[proof]
+        fn count_down_stmt(i:nat) {
+            decreases(i);
+
+            if i != 0 {
+                count_down_stmt(i - 1);
+            }
+        }
+    } => Ok(())
+}
+
+test_verify_with_pervasive! {
+    // Basic test of mutually recursive expressions
+    #[test] mutually_recursive_expressions code! {
+        #[spec]
+        fn count_down_a(i:nat) -> nat {
+            decreases(i);
+
+            if i == 0 { 0 } else { 1 + count_down_b(i - 1) }
+        }
+
+        #[spec]
+        fn count_down_b(i:nat) -> nat {
+            decreases(i);
+
+            if i == 0 { 0 } else { 1 + count_down_a(i - 1) }
+        }
+
+        #[proof]
+        fn count_down_properties() {
+            assert(count_down_b(0) == 0);
+            assert(count_down_a(1) == 1);
+        }
+    } => Ok(())
+}
+
+test_verify_with_pervasive! {
+    // Test that fuel only provides one definition unfolding
+    #[test] mutually_recursive_expressions_insufficient_fuel code! {
+        #[spec]
+        fn count_down_a(i:nat) -> nat {
+            decreases(i);
+
+            if i == 0 { 0 } else { 1 + count_down_b(i - 1) }
+        }
+
+        #[spec]
+        fn count_down_b(i:nat) -> nat {
+            decreases(i);
+
+            if i == 0 { 0 } else { 1 + count_down_a(i - 1) }
+        }
+
+        #[proof]
+        fn count_down_properties() {
+            assert(count_down_a(1) == 1);   // FAILS
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_with_pervasive! {
+    // Basic test of mutually recursive statements
+    #[test] mutually_recursive_statements code! {
+        #[proof]
+        fn count_down_a_stmt(i:nat) {
+            decreases(i);
+
+            if i != 0 {
+                count_down_b_stmt(i - 1);
+            }
+        }
+
+        #[proof]
+        fn count_down_b_stmt(i:nat) {
+            decreases(i);
+
+            if i != 0 {
+                count_down_a_stmt(i - 1);
+            }
+        }
+    } => Ok(())
+}
+
+test_verify_with_pervasive! {
+    // Expression that fails to decrease
+    #[test] expr_decrease_fail_1 code! {
+        #[spec]
+        fn arith_sum_int(i: int) -> int {
+            decreases(i);
+
+            if i <= 0 { 0 } else { i + arith_sum_int(i + 1) }  // FAILS
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_with_pervasive! {
+    // Statement that fails to decrease
+    #[test] stmt_decrease_fail code! {
+        #[proof]
+        fn count_down_stmt(i:nat) {
+            decreases(i);
+
+            if i != 0 {
+                count_down_stmt(i + 1); // FAILS
+            }
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_with_pervasive! {
+    // Expression that decreases, but not based on the decreases clause provided
+    #[test] expr_wrong_decreases code! {
+        #[spec]
+        fn arith_sum_int(i: int) -> int {
+            decreases(100 - i);
+
+            if i <= 0 { 0 } else { i + arith_sum_int(i - 1) }  // FAILS
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_with_pervasive! {
+    // Expression that decreases, but not based on the decreases clause provided
+    #[test] expr_wrong_decreases_2 code! {
+        #[spec]
+        fn arith_sum_int(x:nat, i: int) -> int {
+            decreases(x);
+
+            if i <= 0 { 0 } else { i + arith_sum_int(x, i - 1) }  // FAILS
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_with_pervasive! {
+    // Expression that decreases, but not based on the decreases clause provided
+    #[test] expr_wrong_decreases_3 code! {
+        #[spec]
+        fn arith_sum_int(i: int) -> int {
+            decreases(5);
+
+            if i <= 0 { 0 } else { i + arith_sum_int(4) }  // FAILS
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_with_pervasive! {
+    // Expression that doesn't decrease due to extra clause
+    #[test] expr_decrease_fail_2 code! {
+        #[spec]
+        fn arith_sum_int(x:nat, y:nat, i: int) -> int {
+            decreases(i);
+
+            if i <= 0 && x < y { 0 } else { i + arith_sum_int(x, y, i - 1) }  // FAILS
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_with_pervasive! {
+    // Expression that fails to decrease
+    #[test] expr_decrease_fail_3 code! {
+        #[spec]
+        fn arith_sum_int(i: int) -> int {
+            decreases(i);
+
+            if i <= 0 { 0 } else { i + arith_sum_int(i) }  // FAILS
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+test_verify_with_pervasive! {
+    // Mutually recursive expressions fail to decrease
+    #[test] mutual_expr_decrease_fail code! {
+        #[spec]
+        fn count_down_a(i:nat) -> nat {
+            decreases(i);
+
+            if i == 0 { 0 } else { 1 + count_down_b(i - 1) }  // FAILS
+        }
+
+        #[spec]
+        fn count_down_b(i:nat) -> nat {
+            decreases(5 - i);
+
+            if i >= 5 { 0 } else { 1 + count_down_a(i + 1) }  // FAILS
+        }
+    } => Err(err) => assert_two_fails(err)
+}
+
+test_verify_with_pervasive! {
+    // Mutually recursive statements fail to decrease
+    #[test] mutual_stmt_decrease_fail code! {
+        #[proof]
+        fn count_down_a_stmt(i:nat) {
+            decreases(i);
+
+            if i != 0 {
+                count_down_b_stmt(i + 1);   // FAILS
+            }
+        }
+
+        #[proof]
+        fn count_down_b_stmt(i:nat) {
+            decreases(i);
+
+            if i != 0 {
+                count_down_a_stmt(i + 1);   // FAILS
+            }
+        }
+    } => Err(err) => assert_two_fails(err)
+}
+
+// TODO: Expression that fails to decrease in a function returning unit
+/*
+test_verify_with_pervasive! {
+    #[test] unit_expr_decrease_fail code! {
+        #[spec]
+        fn count_down_tricky(i:nat) {
+            decreases(i);
+
+            if i != 0 {
+                count_down_tricky(i + 1)
+            }
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+*/

verify/vir/src/context.rs

@@ -1,5 +1,6 @@
 use crate::ast::{Function, Ident, Krate, Mode, Path, Variants, VirErr};
 use crate::def::FUEL_ID;
+use crate::scc::Graph;
 use air::ast::{Command, CommandX, Commands, DeclX, MultiOp, Span};
 use air::ast_util::str_typ;
 use std::collections::HashMap;
@@ -9,6 +10,7 @@ pub struct Ctx {
     pub(crate) datatypes: HashMap<Path, Variants>,
     pub(crate) functions: Vec<Function>,
     pub(crate) func_map: HashMap<Ident, Function>,
+    pub(crate) func_call_graph: Graph<Ident>,
     pub(crate) chosen_triggers: std::cell::RefCell<Vec<(Span, Vec<Vec<String>>)>>, // diagnostics
 }
 
@@ -21,14 +23,16 @@ impl Ctx {
             .collect::<HashMap<_, _>>();
         let mut functions: Vec<Function> = Vec::new();
         let mut func_map: HashMap<Ident, Function> = HashMap::new();
+        let mut func_call_graph: Graph<Ident> = Graph::new();
         for function in krate.functions.iter() {
             func_map.insert(function.x.name.clone(), function.clone());
-            crate::recursion::check_no_mutual_recursion(&func_map, function)?;
+            crate::recursion::expand_call_graph(&mut func_call_graph, function)?;
             functions.push(function.clone());
         }
+        func_call_graph.compute_sccs();
         let chosen_triggers: std::cell::RefCell<Vec<(Span, Vec<Vec<String>>)>> =
             std::cell::RefCell::new(Vec::new());
-        Ok(Ctx { datatypes, functions, func_map, chosen_triggers })
+        Ok(Ctx { datatypes, functions, func_map, func_call_graph, chosen_triggers })
     }
 
     pub fn prelude(&self) -> Commands {