Incorrect support for two-phase borrows

[xldenis]

@jhaye reports that the following code creates ill typed why3 code.

use creusot_contracts::*;

/// A sparse map representation over a totally ordered key type.
///
/// Used in [crate::ExecutableReactions]
///
pub struct VecMap<K, V>
where
    K: Eq + Ord,
{
    v: Vec<(K, V)>,
}

impl<K, V> VecMap<K, V>
where
    K: Eq + Ord + DeepModel,
    K::DeepModelTy: OrdLogic,
{
    #[logic]
    #[trusted]
    #[ensures(result.len() == (@self.v).len() &&
              forall<i: Int> i >= 0 && i < (@self.v).len() ==>
              result[i] == (@self.v)[i].0.deep_model())]
    fn key_seq(self) -> Seq<K::DeepModelTy> {
        pearlite! { absurd }
    }

    #[predicate]
    fn is_sorted(self) -> bool {
        pearlite! {
            forall<m: Int, n: Int> m >= 0 && n >= 0 && m < (@self.v).len() && n < (@self.v).len() && m < n ==>
                self.key_seq()[m] < self.key_seq()[n]
        }
    }
}

impl<K, V> VecMap<K, V>
where
    K: Eq + Ord + DeepModel,
    K::DeepModelTy: OrdLogic,
{
    /// Directly insert into the underlying `Vec`. This does not maintain the sorting of elements
    /// by itself.
    #[requires(@idx <= (@self.v).len())]
    #[ensures((@(^self).v).len() == (@self.v).len() + 1)]
    #[ensures(forall<i: Int> 0 <= i && i < @idx ==> (@(^self).v)[i] == (@self.v)[i])]
    #[ensures((@(^self).v)[@idx] == (key, value))]
    #[ensures(forall<i: Int> @idx < i && i < (@(^self).v).len() ==> (@(^self).v)[i] == (@self.v)[i - 1])]
    #[ensures(self.is_sorted() && (@self.v).len() == 0 ==> (^self).is_sorted())]
    #[ensures(self.is_sorted() && (@self.v).len() > 0 && @idx > 0 && @idx < (@self.v).len() &&
              (@self.v)[@idx].0.deep_model() > key.deep_model() &&
              (@self.v)[@idx - 1].0.deep_model() < key.deep_model() ==>
              (^self).is_sorted()
    )]
    #[ensures(self.is_sorted() && (@self.v).len() > 0 && @idx == 0 &&
              (@self.v)[@idx].0.deep_model() > key.deep_model() ==>
              (^self).is_sorted()
    )]
    #[ensures(self.is_sorted() && (@self.v).len() > 0 && @idx == (@self.v).len() &&
              (@self.v)[@idx - 1].0.deep_model() < key.deep_model() ==>
              (^self).is_sorted()
    )]
    fn insert_internal(&mut self, idx: usize, key: K, value: V) {
        self.v.insert(idx, (key, value))
    }
}

/// A vacant Entry.
pub struct VacantEntry<'a, K, V>
where
    K: Ord + Eq,
{
    map: &'a mut VecMap<K, V>,
    key: K,
    index: usize,
}

impl<K, V> VacantEntry<'_, K, V>
where
    K: Ord + Eq + Clone + DeepModel,
    K::DeepModelTy: OrdLogic,
{
    /// Sets the value of the entry with the VacantEntry's key.
    #[requires(self.map.is_sorted())]
    #[requires(@self.index <= (@self.map.v).len())]
    #[requires(forall<i: Int> i >= 0 && i < @self.index ==>
               self.map.key_seq()[i] < self.key.deep_model())]
    #[requires(forall<i: Int> i >= @self.index && i < (@self.map.v).len() ==>
               self.map.key_seq()[i] > self.key.deep_model())]
    #[ensures((^self).map.is_sorted())]
    pub fn insert(&mut self, value: V) {
        self.map
            .insert_internal(self.index, self.key.clone(), value)
    }
}

[jhjourdan]

Minified example:

extern crate creusot_contracts;
use creusot_contracts::*;

/// A vacant Entry.
pub struct VacantEntry<'a, K>
where
    K: Ord + Eq,
{
    map: &'a mut Vec<K>,
    key: K,
    index: usize,
}

impl<K> VacantEntry<'_, K>
where
    K: Ord + Eq + Clone + DeepModel,
    K::DeepModelTy: OrdLogic,
{
    pub fn insert(&mut self) {
        self.map.insert(self.index, self.key.clone())
    }
}

[jhjourdan]

That should not be very hard to debug.

Basically, Creusot uses the same temporary variable for self.map and self.index.

[Lysxia]

Is this an instance of #1239 ?

[jhjourdan]

Probably. But could you please check this specific test case is still an issue?

[Lysxia]

Yes, the error still happens.

[jhjourdan]

Looking at the coma code generated, this does not seem to be related to #1239. I don't know where this comes from, but this can probably be used for unsoundness.

[jhjourdan]

The bug is in compute_ref_place, which computes garbage in this case. This has nothing to do with #1239.

[jhjourdan]

More generally, our handling of two-phase borrows is broken.

[jhjourdan]

After discussions, it seems that a solution would be to delay the creation of the prophecy a the activation point of two phases borrows : at this point, the borrowed place should not have moved, and the borrow should not have been used yet.