1) Sull'assembler:
    - fattorizzare l'abstract interpretation in analisi dei basic block (analisi statica) /analisi dei flussi (dinamica)
      NOTA: tenere conto che per associare staticamente un costo ai basic blocks un interprete astratto inferisce ed usa il
           control flow;
           un compilatore abs-interpretation aware trasferisce informazione quantitativa da sorgente a assmbler, noi non lo 
           facciamo, ma potremmo. Perchè pensiamo di essere meglio?
    - assumiamo che ogni basic block inizi e termini con una label ed introduciamo una nozione di misurabile 
      (che tenga conto anche dell'input/output ovvero istruzioni che sfuggono all'interpretazione astratta poiche' 
       difficilmente predicibili o che introdurrebbero una approssimazione eccessiva)
   - teorema statico dinamico
2) Fanta-compilatore:
   assumere che il compilatore mandi i basic block nel sorgente in basic block nell'assembler ed inoltre che sia composizionale
   in quanto la prima/ultima istruzione che emette l'etichetta si mapperebbe in un blocco la cui prima/ultima istruzione emetta
   l'etichetta
   Concludere che misurabile nel source implica misurabile nel target
   Teorema: l'analisi statica del sorgente ovvero liftare l'analisi statica dell'assembler compilato nel sorgente per determinare
   il costo delle etichette nel sorgente, ovvero teorema statico dinamico nel sorgente.
   Capire come usarlo nell'instrumentazione (FRAMA C ?).
3) Compilatore più realistico -> assumere che il control flow venga preservato ma non la composizionalità
  (un basic block nel sorgente viene mappato con le premesse e code silenti nell'assembler.
  - Fare esempi: chiamate di funzione per passaggio di parametri, switch
  - nuova definizione di misurabile e nuovo teorema di simulazione con code.
4) Chiamate di funzione/annidamento dei basic blocks
   - monoide non abeliano -> non c'e' niente da fare, le chiamate sono tutte postlabelled
   - monoide abeliano -> possibilità di effettuare una passata che trasforma le chiamate in chiamate post-labelled -> simulazione + statico dinamico
5) Classificazione passate 
   - preservano il control flow e le labels : simulation condition
   - mancata preservazione del control flow: spiegare la soluzione di Paolo e come non impatti su tutte le altre passate (similarità/differenze con la prima passata post-labelled).
6) Formalizzazione.



=================================================================================
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