Add problem case 4 test

[tiif]

It should be impossible to translate this exact test to actual Rust, but I couldn't think of a better one under the current set of expressions we support :)

I think this error is expected

the rule "borrow of disjoint places" at (crates/formality-check/src/borrow_check/nll.rs:532:17) failed because
  condition evaluted to false: `place_disjoint_from_place(&loan.place, &access.place)`
   &loan.place = *(local(list)) . 0
   &access.place = local(list)

full error trace

thread 'test::mir_fn_bodies::problem_case_4' panicked at src/test/mir_fn_bodies.rs:1190:5:
expected program to pass: judgment `loans_in_basic_block_respected { loans_live_on_entry: {}, bb_id: bb0, fn_assumptions: {}, env: TypeckEnv { program: [crate Foo { struct Map { value : u32 } fn min_problem_case_4 <lt> (&mut ^lt0_0 Map, &mut ^lt0_0 Map) -> u32 = minirust(list, list2) -> ret { let list : &mut ^lt0_0 Map ; let list2 : &mut ^lt0_0 Map ; let ret : u32 ; exists <lt> { let num : &mut ^lt0_0 u32 ; bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; } bb1 : { statements{ local(num) = & mut ^lt0_0 *(local(list)) . 0 ; local(list) = & mut ^lt1_0 *(local(list2)) ; place_mention(local(num)) ; } return ; } } } ; }], env: Env { variables: [!lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: u32, local_variables: {list: &mut !lt_1 Map, list2: &mut !lt_1 Map, num: &mut ?lt_2 u32, ret: u32}, blocks: [bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; }, bb1 : { statements{ local(num) = & mut ?lt_2 *(local(list)) . 0 ; local(list) = & mut !lt_1 *(local(list2)) ; place_mention(local(num)) ; } return ; }], ret_id: ret, ret_place_is_initialised: true, declared_input_tys: [&mut !lt_1 Map, &mut !lt_1 Map], callee_input_tys: {}, crate_id: Foo, fn_args: [list, list2], pending_outlives: [], decls: decls(222, [], [], [], [], [], [adt Map { struct { value : u32 } }], {}, {Map}) } }` failed at the following rule(s):
the rule "basic block" at (crates/formality-check/src/borrow_check/nll.rs:258:14) failed because
  judgment `loans_in_terminator_respected { loans_live_on_entry: {}, terminator: goto bb1, fn_assumptions: {}, env: TypeckEnv { program: [crate Foo { struct Map { value : u32 } fn min_problem_case_4 <lt> (&mut ^lt0_0 Map, &mut ^lt0_0 Map) -> u32 = minirust(list, list2) -> ret { let list : &mut ^lt0_0 Map ; let list2 : &mut ^lt0_0 Map ; let ret : u32 ; exists <lt> { let num : &mut ^lt0_0 u32 ; bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; } bb1 : { statements{ local(num) = & mut ^lt0_0 *(local(list)) . 0 ; local(list) = & mut ^lt1_0 *(local(list2)) ; place_mention(local(num)) ; } return ; } } } ; }], env: Env { variables: [!lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: u32, local_variables: {list: &mut !lt_1 Map, list2: &mut !lt_1 Map, num: &mut ?lt_2 u32, ret: u32}, blocks: [bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; }, bb1 : { statements{ local(num) = & mut ?lt_2 *(local(list)) . 0 ; local(list) = & mut !lt_1 *(local(list2)) ; place_mention(local(num)) ; } return ; }], ret_id: ret, ret_place_is_initialised: true, declared_input_tys: [&mut !lt_1 Map, &mut !lt_1 Map], callee_input_tys: {}, crate_id: Foo, fn_args: [list, list2], pending_outlives: [], decls: decls(222, [], [], [], [], [], [adt Map { struct { value : u32 } }], {}, {Map}) } }` failed at the following rule(s):
    the rule "goto" at (crates/formality-check/src/borrow_check/nll.rs:277:18) failed because
      judgment `loans_in_basic_block_respected { loans_live_on_entry: {}, bb_id: bb1, fn_assumptions: {}, env: TypeckEnv { program: [crate Foo { struct Map { value : u32 } fn min_problem_case_4 <lt> (&mut ^lt0_0 Map, &mut ^lt0_0 Map) -> u32 = minirust(list, list2) -> ret { let list : &mut ^lt0_0 Map ; let list2 : &mut ^lt0_0 Map ; let ret : u32 ; exists <lt> { let num : &mut ^lt0_0 u32 ; bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; } bb1 : { statements{ local(num) = & mut ^lt0_0 *(local(list)) . 0 ; local(list) = & mut ^lt1_0 *(local(list2)) ; place_mention(local(num)) ; } return ; } } } ; }], env: Env { variables: [!lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: u32, local_variables: {list: &mut !lt_1 Map, list2: &mut !lt_1 Map, num: &mut ?lt_2 u32, ret: u32}, blocks: [bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; }, bb1 : { statements{ local(num) = & mut ?lt_2 *(local(list)) . 0 ; local(list) = & mut !lt_1 *(local(list2)) ; place_mention(local(num)) ; } return ; }], ret_id: ret, ret_place_is_initialised: true, declared_input_tys: [&mut !lt_1 Map, &mut !lt_1 Map], callee_input_tys: {}, crate_id: Foo, fn_args: [list, list2], pending_outlives: [], decls: decls(222, [], [], [], [], [], [adt Map { struct { value : u32 } }], {}, {Map}) } }` failed at the following rule(s):
        the rule "basic block" at (crates/formality-check/src/borrow_check/nll.rs:252:18) failed because
          judgment `loans_in_statement_respected { loans_live_on_entry: {loan(?lt_2, *(local(list)) . 0, mut)}, statement: local(list) = & mut !lt_1 *(local(list2)) ;, places_live_on_exit: {local(num)}, fn_assumptions: {}, env: TypeckEnv { program: [crate Foo { struct Map { value : u32 } fn min_problem_case_4 <lt> (&mut ^lt0_0 Map, &mut ^lt0_0 Map) -> u32 = minirust(list, list2) -> ret { let list : &mut ^lt0_0 Map ; let list2 : &mut ^lt0_0 Map ; let ret : u32 ; exists <lt> { let num : &mut ^lt0_0 u32 ; bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; } bb1 : { statements{ local(num) = & mut ^lt0_0 *(local(list)) . 0 ; local(list) = & mut ^lt1_0 *(local(list2)) ; place_mention(local(num)) ; } return ; } } } ; }], env: Env { variables: [!lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: u32, local_variables: {list: &mut !lt_1 Map, list2: &mut !lt_1 Map, num: &mut ?lt_2 u32, ret: u32}, blocks: [bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; }, bb1 : { statements{ local(num) = & mut ?lt_2 *(local(list)) . 0 ; local(list) = & mut !lt_1 *(local(list2)) ; place_mention(local(num)) ; } return ; }], ret_id: ret, ret_place_is_initialised: true, declared_input_tys: [&mut !lt_1 Map, &mut !lt_1 Map], callee_input_tys: {}, crate_id: Foo, fn_args: [list, list2], pending_outlives: [], decls: decls(222, [], [], [], [], [], [adt Map { struct { value : u32 } }], {}, {Map}) } }` failed at the following rule(s):
            the rule "assign" at (crates/formality-check/src/borrow_check/nll.rs:370:14) failed because
              judgment `access_permitted_by_loans { loans_live_before_access: {loan(!lt_1, *(local(list2)), mut), loan(?lt_2, *(local(list)) . 0, mut)}, access: access(write, local(list)), places_live_after_access: {local(num)}, assumptions: {}, env: TypeckEnv { program: [crate Foo { struct Map { value : u32 } fn min_problem_case_4 <lt> (&mut ^lt0_0 Map, &mut ^lt0_0 Map) -> u32 = minirust(list, list2) -> ret { let list : &mut ^lt0_0 Map ; let list2 : &mut ^lt0_0 Map ; let ret : u32 ; exists <lt> { let num : &mut ^lt0_0 u32 ; bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; } bb1 : { statements{ local(num) = & mut ^lt0_0 *(local(list)) . 0 ; local(list) = & mut ^lt1_0 *(local(list2)) ; place_mention(local(num)) ; } return ; } } } ; }], env: Env { variables: [!lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: u32, local_variables: {list: &mut !lt_1 Map, list2: &mut !lt_1 Map, num: &mut ?lt_2 u32, ret: u32}, blocks: [bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; }, bb1 : { statements{ local(num) = & mut ?lt_2 *(local(list)) . 0 ; local(list) = & mut !lt_1 *(local(list2)) ; place_mention(local(num)) ; } return ; }], ret_id: ret, ret_place_is_initialised: true, declared_input_tys: [&mut !lt_1 Map, &mut !lt_1 Map], callee_input_tys: {}, crate_id: Foo, fn_args: [list, list2], pending_outlives: [], decls: decls(222, [], [], [], [], [], [adt Map { struct { value : u32 } }], {}, {Map}) } }` failed at the following rule(s):
                the rule "access_permitted_by_loans" at (crates/formality-check/src/borrow_check/nll.rs:513:18) failed because
                  judgment `access_permitted_by_loan { loan: loan(?lt_2, *(local(list)) . 0, mut), access: access(write, local(list)), places_live_after_access: {local(num)}, assumptions: {}, env: TypeckEnv { program: [crate Foo { struct Map { value : u32 } fn min_problem_case_4 <lt> (&mut ^lt0_0 Map, &mut ^lt0_0 Map) -> u32 = minirust(list, list2) -> ret { let list : &mut ^lt0_0 Map ; let list2 : &mut ^lt0_0 Map ; let ret : u32 ; exists <lt> { let num : &mut ^lt0_0 u32 ; bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; } bb1 : { statements{ local(num) = & mut ^lt0_0 *(local(list)) . 0 ; local(list) = & mut ^lt1_0 *(local(list2)) ; place_mention(local(num)) ; } return ; } } } ; }], env: Env { variables: [!lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: u32, local_variables: {list: &mut !lt_1 Map, list2: &mut !lt_1 Map, num: &mut ?lt_2 u32, ret: u32}, blocks: [bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; }, bb1 : { statements{ local(num) = & mut ?lt_2 *(local(list)) . 0 ; local(list) = & mut !lt_1 *(local(list2)) ; place_mention(local(num)) ; } return ; }], ret_id: ret, ret_place_is_initialised: true, declared_input_tys: [&mut !lt_1 Map, &mut !lt_1 Map], callee_input_tys: {}, crate_id: Foo, fn_args: [list, list2], pending_outlives: [], decls: decls(222, [], [], [], [], [], [adt Map { struct { value : u32 } }], {}, {Map}) } }` failed at the following rule(s):
                    the rule "borrow of disjoint places" at (crates/formality-check/src/borrow_check/nll.rs:532:17) failed because
                      condition evaluted to false: `place_disjoint_from_place(&loan.place, &access.place)`
                        &loan.place = *(local(list)) . 0
                        &access.place = local(list)
                    the rule "borrows of disjoint places" at (crates/formality-check/src/borrow_check/nll.rs:551:14) failed because
                      judgment `loan_not_required_by_live_places { loan: loan(?lt_2, *(local(list)) . 0, mut), places_live_after_access: {local(num)}, assumptions: {}, env: TypeckEnv { program: [crate Foo { struct Map { value : u32 } fn min_problem_case_4 <lt> (&mut ^lt0_0 Map, &mut ^lt0_0 Map) -> u32 = minirust(list, list2) -> ret { let list : &mut ^lt0_0 Map ; let list2 : &mut ^lt0_0 Map ; let ret : u32 ; exists <lt> { let num : &mut ^lt0_0 u32 ; bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; } bb1 : { statements{ local(num) = & mut ^lt0_0 *(local(list)) . 0 ; local(list) = & mut ^lt1_0 *(local(list2)) ; place_mention(local(num)) ; } return ; } } } ; }], env: Env { variables: [!lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: u32, local_variables: {list: &mut !lt_1 Map, list2: &mut !lt_1 Map, num: &mut ?lt_2 u32, ret: u32}, blocks: [bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; }, bb1 : { statements{ local(num) = & mut ?lt_2 *(local(list)) . 0 ; local(list) = & mut !lt_1 *(local(list2)) ; place_mention(local(num)) ; } return ; }], ret_id: ret, ret_place_is_initialised: true, declared_input_tys: [&mut !lt_1 Map, &mut !lt_1 Map], callee_input_tys: {}, crate_id: Foo, fn_args: [list, list2], pending_outlives: [], decls: decls(222, [], [], [], [], [], [adt Map { struct { value : u32 } }], {}, {Map}) } }` failed at the following rule(s):
                        the rule "loan_not_required_by_live_places" at (crates/formality-check/src/borrow_check/nll.rs:666:18) failed because
                          judgment `loan_not_required_by_live_place { loan: loan(?lt_2, *(local(list)) . 0, mut), live_place: local(num), assumptions: {}, env: TypeckEnv { program: [crate Foo { struct Map { value : u32 } fn min_problem_case_4 <lt> (&mut ^lt0_0 Map, &mut ^lt0_0 Map) -> u32 = minirust(list, list2) -> ret { let list : &mut ^lt0_0 Map ; let list2 : &mut ^lt0_0 Map ; let ret : u32 ; exists <lt> { let num : &mut ^lt0_0 u32 ; bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; } bb1 : { statements{ local(num) = & mut ^lt0_0 *(local(list)) . 0 ; local(list) = & mut ^lt1_0 *(local(list2)) ; place_mention(local(num)) ; } return ; } } } ; }], env: Env { variables: [!lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: u32, local_variables: {list: &mut !lt_1 Map, list2: &mut !lt_1 Map, num: &mut ?lt_2 u32, ret: u32}, blocks: [bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; }, bb1 : { statements{ local(num) = & mut ?lt_2 *(local(list)) . 0 ; local(list) = & mut !lt_1 *(local(list2)) ; place_mention(local(num)) ; } return ; }], ret_id: ret, ret_place_is_initialised: true, declared_input_tys: [&mut !lt_1 Map, &mut !lt_1 Map], callee_input_tys: {}, crate_id: Foo, fn_args: [list, list2], pending_outlives: [], decls: decls(222, [], [], [], [], [], [adt Map { struct { value : u32 } }], {}, {Map}) } }` failed at the following rule(s):
                            the rule "loan is not required by type" at (crates/formality-check/src/borrow_check/nll.rs:693:14) failed because
                              judgment `loan_not_required_by_parameter { loan: loan(?lt_2, *(local(list)) . 0, mut), live_parameter: &mut ?lt_2 u32, assumptions: {}, env: TypeckEnv { program: [crate Foo { struct Map { value : u32 } fn min_problem_case_4 <lt> (&mut ^lt0_0 Map, &mut ^lt0_0 Map) -> u32 = minirust(list, list2) -> ret { let list : &mut ^lt0_0 Map ; let list2 : &mut ^lt0_0 Map ; let ret : u32 ; exists <lt> { let num : &mut ^lt0_0 u32 ; bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; } bb1 : { statements{ local(num) = & mut ^lt0_0 *(local(list)) . 0 ; local(list) = & mut ^lt1_0 *(local(list2)) ; place_mention(local(num)) ; } return ; } } } ; }], env: Env { variables: [!lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: u32, local_variables: {list: &mut !lt_1 Map, list2: &mut !lt_1 Map, num: &mut ?lt_2 u32, ret: u32}, blocks: [bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; }, bb1 : { statements{ local(num) = & mut ?lt_2 *(local(list)) . 0 ; local(list) = & mut !lt_1 *(local(list2)) ; place_mention(local(num)) ; } return ; }], ret_id: ret, ret_place_is_initialised: true, declared_input_tys: [&mut !lt_1 Map, &mut !lt_1 Map], callee_input_tys: {}, crate_id: Foo, fn_args: [list, list2], pending_outlives: [], decls: decls(222, [], [], [], [], [], [adt Map { struct { value : u32 } }], {}, {Map}) } }` failed at the following rule(s):
                                the rule "rigid-ty" at (crates/formality-check/src/borrow_check/nll.rs:762:14) failed because
                                  judgment `loan_not_required_by_parameters { loan: loan(?lt_2, *(local(list)) . 0, mut), live_parameters: [?lt_2, u32], assumptions: {}, env: TypeckEnv { program: [crate Foo { struct Map { value : u32 } fn min_problem_case_4 <lt> (&mut ^lt0_0 Map, &mut ^lt0_0 Map) -> u32 = minirust(list, list2) -> ret { let list : &mut ^lt0_0 Map ; let list2 : &mut ^lt0_0 Map ; let ret : u32 ; exists <lt> { let num : &mut ^lt0_0 u32 ; bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; } bb1 : { statements{ local(num) = & mut ^lt0_0 *(local(list)) . 0 ; local(list) = & mut ^lt1_0 *(local(list2)) ; place_mention(local(num)) ; } return ; } } } ; }], env: Env { variables: [!lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: u32, local_variables: {list: &mut !lt_1 Map, list2: &mut !lt_1 Map, num: &mut ?lt_2 u32, ret: u32}, blocks: [bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; }, bb1 : { statements{ local(num) = & mut ?lt_2 *(local(list)) . 0 ; local(list) = & mut !lt_1 *(local(list2)) ; place_mention(local(num)) ; } return ; }], ret_id: ret, ret_place_is_initialised: true, declared_input_tys: [&mut !lt_1 Map, &mut !lt_1 Map], callee_input_tys: {}, crate_id: Foo, fn_args: [list, list2], pending_outlives: [], decls: decls(222, [], [], [], [], [], [adt Map { struct { value : u32 } }], {}, {Map}) } }` failed at the following rule(s):
                                    the rule "loan_not_required_by_parameters" at (crates/formality-check/src/borrow_check/nll.rs:898:18) failed because
                                      judgment `loan_not_required_by_parameter { loan: loan(?lt_2, *(local(list)) . 0, mut), live_parameter: ?lt_2, assumptions: {}, env: TypeckEnv { program: [crate Foo { struct Map { value : u32 } fn min_problem_case_4 <lt> (&mut ^lt0_0 Map, &mut ^lt0_0 Map) -> u32 = minirust(list, list2) -> ret { let list : &mut ^lt0_0 Map ; let list2 : &mut ^lt0_0 Map ; let ret : u32 ; exists <lt> { let num : &mut ^lt0_0 u32 ; bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; } bb1 : { statements{ local(num) = & mut ^lt0_0 *(local(list)) . 0 ; local(list) = & mut ^lt1_0 *(local(list2)) ; place_mention(local(num)) ; } return ; } } } ; }], env: Env { variables: [!lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: u32, local_variables: {list: &mut !lt_1 Map, list2: &mut !lt_1 Map, num: &mut ?lt_2 u32, ret: u32}, blocks: [bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; }, bb1 : { statements{ local(num) = & mut ?lt_2 *(local(list)) . 0 ; local(list) = & mut !lt_1 *(local(list2)) ; place_mention(local(num)) ; } return ; }], ret_id: ret, ret_place_is_initialised: true, declared_input_tys: [&mut !lt_1 Map, &mut !lt_1 Map], callee_input_tys: {}, crate_id: Foo, fn_args: [list, list2], pending_outlives: [], decls: decls(222, [], [], [], [], [], [adt Map { struct { value : u32 } }], {}, {Map}) } }` failed at the following rule(s):
                                        the rule "lifetime" at (crates/formality-check/src/borrow_check/nll.rs:852:14) failed because
                                          judgment `loan_cannot_outlive { loan: loan(?lt_2, *(local(list)) . 0, mut), lifetime: ?lt_2, assumptions: {}, env: TypeckEnv { program: [crate Foo { struct Map { value : u32 } fn min_problem_case_4 <lt> (&mut ^lt0_0 Map, &mut ^lt0_0 Map) -> u32 = minirust(list, list2) -> ret { let list : &mut ^lt0_0 Map ; let list2 : &mut ^lt0_0 Map ; let ret : u32 ; exists <lt> { let num : &mut ^lt0_0 u32 ; bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; } bb1 : { statements{ local(num) = & mut ^lt0_0 *(local(list)) . 0 ; local(list) = & mut ^lt1_0 *(local(list2)) ; place_mention(local(num)) ; } return ; } } } ; }], env: Env { variables: [!lt_1, ?lt_2], bias: Soundness, pending: [], allow_pending_outlives: false }, output_ty: u32, local_variables: {list: &mut !lt_1 Map, list2: &mut !lt_1 Map, num: &mut ?lt_2 u32, ret: u32}, blocks: [bb0 : { statements{ local(ret) = constant(0 : u32) ; } goto bb1 ; }, bb1 : { statements{ local(num) = & mut ?lt_2 *(local(list)) . 0 ; local(list) = & mut !lt_1 *(local(list2)) ; place_mention(local(num)) ; } return ; }], ret_id: ret, ret_place_is_initialised: true, declared_input_tys: [&mut !lt_1 Map, &mut !lt_1 Map], callee_input_tys: {}, crate_id: Foo, fn_args: [list, list2], pending_outlives: [], decls: decls(222, [], [], [], [], [], [adt Map { struct { value : u32 } }], {}, {Map}) } }` failed at the following rule(s):
                                            the rule "loan_cannot_outlive" at (crates/formality-check/src/borrow_check/nll.rs:871:17) failed because
                                              condition evaluted to false: `!outlived_by_loan.contains(&lifetime.upcast())`
                                                outlived_by_loan = {?lt_2}
                                                &lifetime.upcast() = ?lt_2

Fixed #208

[tiif]

While we are at this, I also fixed the test_ref_deref test that was previously ignored in the latest commit.