Struct c2rust_refactor::analysis::ownership::constraint::ConstraintSet

pub struct ConstraintSet<'lty> { /* fields omitted */ }

A set of constraints over permission expressions, of the form p1 <= p2.

Note that most of the more complex operations are imprecise (unsound) in certain cases involving Min. Fortunately, these cases seem not to come up often in practice.

Methods

impl<'lty, 'tcx> ConstraintSet<'lty>

pub fn new() -> ConstraintSet<'lty>

pub fn iter(&self) -> Iter<(Perm<'lty>, Perm<'lty>)>

pub fn add(&mut self, a: Perm<'lty>, b: Perm<'lty>)

pub fn import(&mut self, other: &ConstraintSet<'lty>)

Add all constraints from other to self.

pub fn import_substituted<F>(
    &mut self,
    other: &ConstraintSet<'lty>,
    arena: &'lty SyncDroplessArena,
    f: F
) where
    F: Fn(Perm<'lty>) -> Perm<'lty>, 

For each constraint in other, substitute all atomic permissions using the callback f, then add the constraint to self.

pub fn clone_substituted<F>(
    &self,
    arena: &'lty SyncDroplessArena,
    f: F
) -> ConstraintSet<'lty> where
    F: Fn(Perm<'lty>) -> Perm<'lty>, 

Clone self, substituting each atomic permission using the callback f.

pub fn for_each_less_than<F>(&self, p: Perm<'lty>, f: F) where
    F: FnMut(Perm<'lty>) -> bool, 

Iterate over all permissions less than p.

This only traverses chains of q <= p, r <= q, etc. It doesn't do anything intelligent regarding Min.

pub fn for_each_greater_than<F>(&self, p: Perm<'lty>, f: F) where
    F: FnMut(Perm<'lty>) -> bool, 

Iterate over all permissions greater than p.

This only traverses chains of p <= q, q <= r, etc. It doesn't do anything intelligent regarding Min.

pub fn lower_bound(&self, p: Perm<'lty>) -> ConcretePerm

Obtain a concrete lower bound on p. Replacing p with any concrete permission less than lower_bound(p) is guaranteed to make the constraint set unsatisfiable.

This function may return a lower result than necessary due to imprecise reasoning about Min.

pub fn upper_bound(&self, p: Perm<'lty>) -> ConcretePerm

Obtain a concrete upper bound on p. Replacing p with any concrete permission greater than upper_bound(p) is guaranteed to make the constraint set unsatisfiable.

This function may return a higher result than necessary due to imprecise reasoning about Min.

pub fn check_partial_assignment<F>(&self, eval: F) -> bool where
    F: Fn(Perm<'lty>) -> Option<ConcretePerm>, 

Given an assignment of concrete permission values to a subset of the variables, check whether any constraints are violated under the partial assignment. Returns false if a constraint is violated, or true if all constraints appear to be satisfiable.

Note this function is only guaranteed to be accurate for complete assignments. On (strictly) partial assignments, it may report that a satisfying assignment is possible when it's not, but never the other way around.

pub fn edit<'a>(&'a mut self) -> EditConstraintSet<'a, 'lty>

Obtain an editing cursor for this constraint set.

pub fn for_each_perm<F: FnMut(Perm<'lty>)>(&self, f: F)

Iterate over each atomic permission in each constraint.

impl<'lty, 'tcx> ConstraintSet<'lty>

pub fn remove_useless(&mut self)

Remove constraints that are obviously useless, like READ <= p.

pub fn expand_min_rhs(&mut self)

Simplify a <= min(b1, b2) into a <= b1, a <= b2.

pub fn simplify_min_lhs(&mut self, arena: &'lty SyncDroplessArena)

Simplify min(...) <= ... constraints as much as possible. Unlike ... <= min(...), it may not always be possible to completely eliminate such constraints.

pub fn simplify(&mut self, arena: &'lty SyncDroplessArena)

Simplify the constraint set as best we can.

pub fn retain_perms<F>(&mut self, arena: &'lty SyncDroplessArena, filter: F) where
    F: Fn(Perm<'lty>) -> bool, 

Eliminate constraints involving permissions on which f(p) returns false, while maintaining relationships between other permissions. For example, when removing q from {p <= q, q <= r}, we would add p <= r before removing the other two constraints.

This may be imprecise if a removed permission appears as an argument of a Min. Simplify the constraint set first to remove as many Mins as possible before using this function.

Trait Implementations

impl<'lty> Eq for ConstraintSet<'lty>

impl<'lty> PartialEq<ConstraintSet<'lty>> for ConstraintSet<'lty>

fn eq(&self, other: &ConstraintSet<'lty>) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &ConstraintSet<'lty>) -> bool

This method tests for !=.

impl<'lty> Clone for ConstraintSet<'lty>

fn clone(&self) -> ConstraintSet<'lty>

Returns a copy of the value.

default fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'lty> Debug for ConstraintSet<'lty>

fn fmt(&self, f: &mut Formatter) -> Result

Formats the value using the given formatter.