Method refine_paths

src/analysis/memory/symbolic_value.rs:259–340

Replaces occurrences of Expression::Variable(path) with the value at that path in the given environment (if there is such a value).

(&self, environment: &AbstractDomain<DomainType>)

    /// Replaces occurrences of Expression::Variable(path) with the value at that path
    /// in the given environment (if there is such a value).
    fn refine_paths(&self, environment: &AbstractDomain<DomainType>) -> Rc<SymbolicValue> {
        match &self.expression {
            Expression::Drop(..) => self.clone(),
            Expression::Numerical(..) => self.clone(),
            Expression::Bottom | Expression::Top => self.clone(),
            Expression::And { left, right } => left
                .refine_paths(environment)
                .and(right.refine_paths(environment)),
            Expression::CompileTimeConstant(..) => self.clone(),
            Expression::Cast {
                operand,
                target_type,
            } => operand.refine_paths(environment).cast(target_type.clone()),
            Expression::Equals { left, right } => left
                .refine_paths(environment)
                .equals(right.refine_paths(environment)),
            Expression::GreaterOrEqual { left, right } => left
                .refine_paths(environment)
                .greater_or_equal(right.refine_paths(environment)),
            Expression::GreaterThan { left, right } => left
                .refine_paths(environment)
                .greater_than(right.refine_paths(environment)),
            Expression::HeapBlock { .. } => self.clone(),
            Expression::Join { left, right } => left
                .refine_paths(environment)
                .join(right.refine_paths(environment)),
            Expression::LessOrEqual { left, right } => left
                .refine_paths(environment)
                .less_or_equal(right.refine_paths(environment)),
            Expression::LessThan { left, right } => left
                .refine_paths(environment)
                .less_than(right.refine_paths(environment)),
            Expression::Ne { left, right } => left
                .refine_paths(environment)
                .not_equals(right.refine_paths(environment)),
            Expression::Mul { left, right } => left
                .refine_paths(environment)
                .mul(right.refine_paths(environment)),
            Expression::LogicalNot { operand } => operand.refine_paths(environment).logical_not(),
            Expression::Or { left, right } => left
                .refine_paths(environment)
                .or(right.refine_paths(environment)),
            Expression::Reference(path) => {
                let refined_path = path.refine_paths(environment);
                SymbolicValue::make_reference(refined_path)
            }
            Expression::Variable { path, var_type } => {
                if let Some(val) = environment.value_at(&path) {
                    val
                } else {
                    let refined_path = path.refine_paths(environment);
                    if let PathEnum::Alias { value } = &refined_path.value {
                        value.clone()
                    } else if let Some(val) = environment.value_at(&refined_path) {
                        val
                    } else if refined_path == *path {
                        self.clone()
                    } else {