trailofbits / binary_type_inference

GNU General Public License v3.0
15 stars 2 forks source link

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

Closed 2over12 closed 2 years ago

2over12 commented 2 years ago
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