I think we may have a conceptual mismatch with how Vivado treats clock objects. The clock object on both sides of a IBUF and BUFG are the same clock object. So for example, there should really just be 1 clock clk, which has multiple netss that are on that clock. PLL's / MMCM's and BUFGCTRL's do split clock definitions because the underlying properties of the clock change across the elements.

Clock objects have properties (e.g. waveform, period, is generated)
Clocks can have relationships to each other (e.g. false path, jitter, https://docs.verilogtorouting.org/en/latest/vpr/sdc_commands/#set-max-delay-set-min-delay)
Nets may have a clock object they are associated with. The propagation step should associate nets with their clocks as needed (e.g. propagate through IBUF/BUFG).
Some cells (PLL/MMCM) define generated clocks using a relationship between the source clock and output clock. The propagate through PLL/MMCM should generate these related clocks.

The propagation that occurs should probably be something akin too:

• Does this element change the clock -> No:

  • If the output net has no explicit clock membership, mark the net as being part of the same clock

• Does this element change the clock -> Yes:

  • If the output net has an explicit clock definition, do nothing
  • If the output net has no explicit clock definition, create a new generated clock with the new properties based on the elements configuration (e.g. PLL creates a new clock with period X, waveform Y Z).