Method refine_parameters

src/analysis/memory/symbolic_value.rs:345–433

Returns a value that is simplified (refined) by replacing parameter values with their corresponding argument values. If no refinement is possible the result is simply a clone of this value.

(
        &self,
        arguments: &[(Rc<Path>, Rc<SymbolicValue>)],
        // fresh: usize,
    )

    /// with their corresponding argument values. If no refinement is possible
    /// the result is simply a clone of this value.
    fn refine_parameters(
        &self,
        arguments: &[(Rc<Path>, Rc<SymbolicValue>)],
        // fresh: usize,
    ) -> 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_parameters(arguments)
                .and(right.refine_parameters(arguments)),
            Expression::CompileTimeConstant(..) => self.clone(),
            Expression::Cast {
                operand,
                target_type,
            } => operand
                .refine_parameters(arguments)
                .cast(target_type.clone()),
            Expression::Equals { left, right } => left
                .refine_parameters(arguments)
                .equals(right.refine_parameters(arguments)),
            Expression::GreaterOrEqual { left, right } => left
                .refine_parameters(arguments)
                .greater_or_equal(right.refine_parameters(arguments)),
            Expression::GreaterThan { left, right } => left
                .refine_parameters(arguments)
                .greater_than(right.refine_parameters(arguments)),
            Expression::HeapBlock { .. } => self.clone(),
            Expression::Join { left, right } => left
                .refine_parameters(arguments)
                .join(right.refine_parameters(arguments)),
            Expression::LessOrEqual { left, right } => left
                .refine_parameters(arguments)
                .less_or_equal(right.refine_parameters(arguments)),
            Expression::LessThan { left, right } => left
                .refine_parameters(arguments)
                .less_than(right.refine_parameters(arguments)),
            Expression::LogicalNot { operand } => {
                operand.refine_parameters(arguments).logical_not()
            }
            Expression::Ne { left, right } => left
                .refine_parameters(arguments)
                .not_equals(right.refine_parameters(arguments)),
            Expression::Mul { left, right } => left
                .refine_parameters(arguments)
                .mul(right.refine_parameters(arguments)),
            Expression::Or { left, right } => left
                .refine_parameters(arguments)
                .or(right.refine_parameters(arguments)),
            Expression::Reference(path) => {
                // if the path is a parameter, the reference is an artifact of its type
                // and needs to be removed in the call context
                match &path.value {
                    PathEnum::Parameter { ordinal } => arguments[*ordinal - 1].1.clone(),
                    _ => {
                        let refined_path = path.refine_parameters(arguments);
                        SymbolicValue::make_reference(refined_path)