1. problema generale: cost analysis at source level because...
2. problema specifico: indurre cost model sul sorgente
3. idea generale (labelling approach citato)
   costo assembly = big_sum costo(basic block)
   assunzione1: compilazione basic-block preserving
     (citare lavoro sui loop)
   assunzione2: costo basic blocks determinabile staticamente
     (citare lavoro sull'hardware)
   quindi: costo C = big_sum cost(basic block) = costo assembly

4. problemi
   a) label emitting instructions:
      una istruzione con due predecessori di cui uno if-then-else
       compilabile solo come sequenza => impossibile da compilare

      soluzione: gli archi determinano i costi e non i nodi

   b) chiamate di funzione e linguaggi non strutturati

      soluzione: tracce strutturate

  [c) hardware: funzione di costo non commutativa => una label dopo ogni
      chiamata; ma difficile ragionarci sopra nel caso di costo commutativo

      soluzione: passata che mette le post-label
  ]

5. sugo:

   1. prova della passata che mette le post-label (work in progress, why
      SOS is hard)

   2. predicato di simulazione fra tracce strutturate + prova che tale
      simulazione dimostra la preservazione dei costi

   3. prova della statico-dinamica: vedi cerco, certificata dal fatto di usare
      solo chiamate post-label