fn dereference()

in checker/src/abstract_value.rs [2367:2459]


    fn dereference(&self, target_type: ExpressionType) -> Rc<AbstractValue> {
        match &self.expression {
            Expression::Bottom | Expression::Top => self.clone(),
            Expression::Cast {
                operand,
                target_type: cast_type,
            } => {
                checked_assume!(
                    *cast_type == ExpressionType::NonPrimitive
                        || *cast_type == ExpressionType::ThinPointer
                );
                operand.dereference(target_type)
            }
            Expression::CompileTimeConstant(..) => {
                // de-referencing a constant value is an illegal operation, so return bottom
                BOTTOM.into()
            }
            Expression::ConditionalExpression {
                condition,
                consequent,
                alternate,
            } => condition.conditional_expression(
                consequent.dereference(target_type),
                alternate.dereference(target_type),
            ),
            Expression::HeapBlock { .. } => self.clone(),
            Expression::Join { left, right } => left
                .dereference(target_type)
                .join(right.dereference(target_type)),
            Expression::Offset { .. } => {
                let path = Path::get_as_path(self.clone());
                let deref_path = Path::new_deref(path, target_type);
                if let PathEnum::Computed { value }
                | PathEnum::HeapBlock { value }
                | PathEnum::Offset { value } = &deref_path.value
                {
                    value.clone()
                } else {
                    AbstractValue::make_typed_unknown(target_type, deref_path)
                }
            }
            Expression::InitialParameterValue { path, .. } => {
                AbstractValue::make_initial_parameter_value(
                    target_type,
                    Path::new_deref(path.clone(), target_type),
                )
            }
            Expression::Reference(path) => {
                if target_type != ExpressionType::NonPrimitive {
                    // We don't have to shallow copy the value at the  source path, so *&p is just p.
                    if let PathEnum::Computed { value }
                    | PathEnum::HeapBlock { value }
                    | PathEnum::Offset { value } = &path.value
                    {
                        return value.clone();
                    }
                }
                AbstractValue::make_typed_unknown(target_type, path.clone())
            }
            Expression::Switch {
                discriminator,
                cases,
                default,
            } => discriminator.switch(
                cases
                    .iter()
                    .map(|(case_val, result_val)| {
                        (case_val.clone(), result_val.dereference(target_type))
                    })
                    .collect(),
                default.dereference(target_type),
            ),
            Expression::UninterpretedCall {
                path,
                result_type: var_type,
                ..
            }
            | Expression::Variable { path, var_type } => AbstractValue::make_typed_unknown(
                target_type,
                Path::new_deref(path.clone(), *var_type),
            ),
            Expression::WidenedJoin { path, operand } => operand
                .dereference(target_type)
                .widen(&Path::new_deref(path.clone(), target_type)),
            _ => {
                info!(
                    "found unhandled expression that is of type reference: {:?}",
                    self.expression
                );
                AbstractValue::make_typed_unknown(target_type, Path::new_computed(Rc::new(TOP)))
            }
        }
    }