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