trailofbits/binary_type_inference

When creating polymorphic sketches, parent node labels should not be copied to the child.

Closed this issue · 0 comments

let in_params = orig_repr
            .quotient_graph
            .get_node_mapping()
            .iter()
            .map(|(dtv, _idx)| dtv.clone())
            .filter(|dtv| dtv.get_base_variable().get_cs_tag().is_none() && dtv.is_in_parameter());

        for dtv in in_params.collect::<Vec<DerivedTypeVar>>() {
            self.refine_formal_in(condensed, &mut orig_repr, dtv, target_idx);
        }

        let out_params = orig_repr
            .quotient_graph
            .get_node_mapping()
            .iter()
            .map(|(dtv, _idx)| dtv.clone())
            .filter(|dtv| dtv.get_base_variable().get_cs_tag().is_none() && dtv.is_out_parameter());

        for dtv in out_params.collect::<Vec<DerivedTypeVar>>() {
            self.refine_formal_out(condensed, &mut orig_repr, dtv, target_idx);
        }

So the code above has a bug. When we refine the formal in parameters right now that will copy in information from the parents including nodes labeled by the parents dtvs. Then the parent dtvs (which arent callsite tagged are in the namespace for this sketch) and the out params from the parent will be included in the childs out params which is not correct.

This could be solved by collecting all dtvs before beginning refinement, but this is solving a symptom and not the cause. We shouldnt copy dtvs from the refinement at all. The labels should come from the type being refined