diff --git a/anno3/progmobile/consegne/Relazione2.pdf b/anno3/progmobile/consegne/Relazione2.pdf new file mode 100644 index 0000000..eb62c25 Binary files /dev/null and b/anno3/progmobile/consegne/Relazione2.pdf differ diff --git a/anno3/progmobile/consegne/apollon_scheda.pdf b/anno3/progmobile/consegne/apollon_scheda.pdf new file mode 100644 index 0000000..397b0b7 Binary files /dev/null and b/anno3/progmobile/consegne/apollon_scheda.pdf differ diff --git a/anno3/progmobile/relazione.md b/anno3/progmobile/relazione.md deleted file mode 100644 index 3326ce3..0000000 --- a/anno3/progmobile/relazione.md +++ /dev/null @@ -1,91 +0,0 @@ -# Introduzione - -Lo streaming musicale è una pratica sempre più comune. -Un numero sempre maggiore di persone si iscrive a servizi come Spotify e Apple Music per poter ascoltare i propri artisti preferiti in qualunque situazione. -Questi servizi sono in genere supportati da abbonamenti o pubblicità. - -Queste piattaforme, nonostante abbiano raggiunto una grande diffusione, sono molto criticate dagli appassionati, dai critici di musica e dagli artisti stessi. - -Le critiche più diffuse sono le seguenti: -* bassissima qualità di riproduzione: i file audio inviati in streaming da Spotify sono in formato mp3 128kpbs, 192kbps per gli utenti premium. Inoltre Spotify [mente sull'encoding dei dati inviati](https://community.spotify.com/t5/iOS-iPhone-iPad/Spotify-Premium-sound-quality-issues-320-kbps-quot-equivalent/td-p/857381). -* censura: entrambe le piattaforme praticano la censura, sia a [fini](https://www.theverge.com/2019/4/12/18305087/congress-apple-criticism-china-communist-tiananmen-pro-democracy) [politici](https://www.breitbart.com/tech/2015/11/13/spotifys-political-censorship-should-worry-us-all/) che per motivi [puritani](https://www.reddit.com/r/spotify/comments/1znw32/why_the_fuck_are_all_the_songs_getting_censored/), non permettendo agli utenti di disabilitare il filtro per la [censura](https://discussions.apple.com/thread/7105598). -* Catalogazione imprecisa: Spotify ed Apple Music offrono nella maggior parte dei casi una sola versione di ogni disco. Inoltre se l'utente carica un mastering differente di un brano già esistente nel loro database, lo scartano. -* Assenza di artisti di nicchia: i database di queste due grandi piattaforme, oltre ad essere prive di tutta la musica non distribuita da etichette riconosciute, offrono uno scarso catalogo per generi meno [mainstream](https://www.hypebot.com/hypebot/2018/05/why-spotify-may-actually-kill-jazz-soul.html). Ne sono un'esempio i brani di musica classica, che [sono solo l'1% del totale](https://news.allaboutjazz.com/how-spotifys-continued-expansion-is-killing-niche-music-genres). -* Pubblicazioni di falsi dati per motivi di PR: [Spotify ha mentito in varie occasioni riguardo al suo catalogo](https://www.theguardian.com/technology/2017/jul/13/are-spotifys-fake-artists-any-good). -* DRM: il Digital Rights Management è una tecnologia che limita le possibilità di riproduzione del file su dispositivi non autorizzati -* Mancata retribuzione agli artisti: Spotify ed Apple Music obbligano gli artisti a fare contratti con delle case discografiche per poter essere pubblicati nella loro piattaforma. Inoltre i compensi finali sono estramemente limitati e per questo molti artisti [rifiutano](https://time.com/3554468/why-taylor-swift-spotify/) di pubblicare la [loro](https://www.theguardian.com/technology/2013/jul/29/spotify-vs-musicians-streaming-royalties) [musica](https://www.bbc.com/news/newsbeat-43240886). - -La nostra app si propone come un'alternativa per appassionati di musica e collezionisti, che non vogliono rinunciare allo streaming seppur continuando ad usufruire della propria collezione musicale di brani di nicchia ed in alta definizione, scaricati da piattaforme come Bandcamp o "rippati" dai CD audio. - -Il nome, Apollon, è un omaggio alla divinità greca del sole e della musica. - -# Specifiche generali dell'applicazione - -L'applicazione avrà come funzionalità principale quella di riprodurre la collezione musicale personale di ogni singolo utente. -Lo streaming è permesso in tre preset di qualità, alto, medio e basso. -L'applicazione offre funzionalità di ricerca e la possibilità di creare playlists. -L'app all'avvio si connetterà ad un server, programmato con le stesse tecnologie e pattern dell'applicazione, gestito da ogni utente. Una spiegazione più ampia del server è offerta in appendice. Basti notare che il server offre la possibilità di gestire più utenti, autenticati tramite nickname e password. - -# Alternative su play store -Oltre alle piattaforme come Spotify e Apple Music che offrono lo streaming musicale ma con gli svantaggi di cui sopra, -vi sono solamente due alternative per chi vuole usufruire dello streaming della propria collezione musicale. -La prima è subsonic, supportato da [varie](https://f-droid.org/en/packages/org.moire.ultrasonic/) [applicazioni](https://play.google.com/store/apps/details?id=net.sourceforge.subsonic.androidapp) ma che non supporta il database più diffuso in ambito audiofilo di [mpd](https://www.musicpd.org/) e non permette di fare seek della traccia audio. -La seconda alternativa è il già citato mpd, che offre una funzione di streaming originariamente pensato per le webradio. [Vi](https://f-droid.org/en/packages/com.namelessdev.mpdroid) [sono](https://f-droid.org/en/packages/org.gateshipone.malp) [app](https://play.google.com/store/apps/details?id=net.prezz.mpr) che supportano un buon numero di features per mpd ma non permettono di creare playlists o di gestire più utenti. La maggiore limitazione di mpd è che permette lo streaming di un solo brano alla volta qualsiasi sia il numero di ascoltatori. - -# Benefici dell'applicazione - -La comunità di audiofili con un particolare interesse per le tecnologie ha deciso da anni che lo standard per i sistemi di riproduzione di musica digitali sono costituiti da sistemi Linux con kernel real time e MPD come riproduttore. -La nostra applicazione ha come interesse primario quello di attrarre questa comunità permettendo da una parte l'integrazione con le tecnologie già in uso (MPD e Linux), dall'altra ampio margine di controllo sulla riproduzione dei file e la gestione della libreria. -Gli utenti possono condividere la loro vasta libreria musicale con più utenti e fare streaming dei propri file audio in diversi formati in base alle esigenze e alla banda disponibile. -Il catalogo musicale è nel pieno controllo dell'utente che andrà a gestirlo con gli strumenti che già utilizzava. -Il server con il quale l'applicazione comunica supporta la lettura dei metadati dei file e del database di MPD. - -# Implementazione e funzionalità - -## Schema di navigazione di base - -All'avvio l'applicazione richiedere l'inserimento delle credenziali di accesso al server (ip, porta, username, password) da parte dell'utente. Tali credenziali vengono memorizzate per poter essere riutilizzate al prossimo avvio. - -Una volta effettuato il login si potrà navigare la libreria musicale. -La navigazione è gestita da un Fragment parametrizzato dalla modalità scelta per la navigazione, ossia genere, artista o album. -La navigazione è arricchita dalla visualizzazione delle copertine e delle foto degli artisti, scaricate interattivamente. -Una volta selezionata una canzone questa verrà messa in riproduzione. Dal Fragment è possibile selezionare la qualità di riproduzione, ovvero High Quality, Medium Quality e Low Quality. Inoltre, nel caso si stesse ascoltando una canzone, è possibile visualizzare le lyrics. - -Durante l'ascolto è possibile aggiungere il brano in riproduzione alla playlist "Favourites". -Le altre playlists sono visualizzabili attraverso le schermate di navigazione e possono essere modificate tramite apposito menù. -Infine è possibile condividere la canzone in ascolto attraverso il bottone "condividi" inviando un messaggio di testo. - -## Scelte tecniche - -### Riproduzione in streaming - -La riproduzione in streaming presenta notevoli difficoltà se abbinata al transcoding on the fly, ovvero la riduzione di qualità di un brano in alta definizione mentre lo si sta ascoltando. La riproduzione di un sorgente tramite protocllo HTTP è fornita dalla classe MediaPlayer del framework Android. Durante la riproduzione la dimensione del file è in continua crescita poiché la dimensione del file sul server è proporzionale alla percentuale di file del quale è già stato compiuto il transcoding. Inoltre il transcoding effettuato tramite Variabile Bit Rate per definizione non permette di conoscere la dimensione finale del file. Per permettere all'utente di fare seek della traccia audio, Apollon interroga la classe MediaPlayer sulla quantità di buffer disponibile e interroga il server sullo stato del transcoding. Attraverso queste due informazioni Apollon effettua il seek con precisione. Quando il seek non è disponibile per mancanza di buffer, la barra di riproduzione viene leggermente oscurata. - -### Interazione col dispositivo - -Quando un brano è in riproduzione viene mostrata la copertina come wallpaper del blocco schermo. -Inoltre la riproduzione si ferma se vengono staccate le cuffie o se arriva una chiamata. -L'output di Apollon viene ridotto per qualche istante nel caso sopraggiunga una notifica. - -### Servizi di terze parti - -Le lyrics vengono fornite da ChartLyrics tramite api web in formato XML. -Le immagini sono fornite da WikiData e scaricate attraverso la libreria Picasso che si occupa di fare caching talora necessario. - -### Pattern architetturali - -Nel codice risalta un notevole utilizzo di pattern architetturali, alcuni comuni a Java e Kotlin, altri specifici di Kotlin e della programmazione funzionale. Inoltre abbiamo seguito differenti tecniche di programmazione e riuso specifici del framework Android. -All'interno dei pattern tipici della programmazione ad oggetti compaiono: -* Adapters: usato per adattare l'interfaccia di una classe ad un'altra. Nel nostro caso è stato usato questo pattern per le classi che forniscono la logica e la visualizzazione all'interno dei fragments. -* Builder: pattern creazionale utilizzato per l'instanziazione step by step di oggetti complessi. Fra le varie classi in cui usiamo questo pattern, la più importante sono quelle per la gestione dei metadati del brano in riproduzione e per l'instanziazione del mediaplayer. -* Events: gli eventi sono oggetti instanziati in risposta a degli input esterni (quali rete o utente) e vengono gestiti in maniera asincrona da differenti funzioni. Vengono utilizzati nella nostra applicazione per gestire la UI e gli eventi di rete relativi lla riproduzione in streaming. - -Kotlin ci ha permesso da un lato di usare con più facilità e in maniera meno verbosa dei pattern tipi della programmazione ad oggetti, in particolare: -* Singleton: pattern che restringe l'instanziazione di una classe ad un solo oggetto. Utilizzata per la connessione al server e la gestione delle credenziali (che a sua volta è un adapter per SharedPreferences). -* Companion Object: un singleton che ha accesso ai membri privati degli oggetti instanziati dalla classe compagno (ovvero della classe all'interno del quale è dichiarato). Ne facciamo uso per la creazione delle instanze dei fragments. -* Sum Types: pattern tipicamente funzionale in cui una struttura dati può contenere diversi tipi predefiniti. Abbiamo modellato i sum types in Kotlin attraverso l'uso delle **sealed class** che ci ha permesso di codificare lo stato del programma attraverso i tipi. -* Pattern Matching: pattern estremamente correlato all'uso dei sum types. Attraverso il pattern matching siamo sicuri che in ogni branch del nostro codice abbiamo preso in considerazione ogni stato possibile. L'uso di assert(false) ci permette di asserire quali tipi non devono raggiungere quella sezione di codice. - -Infine nella nostra codebase abbiamo fatto un uso estensivo delle componenti del framework Android, in particolare: -* Fragments: componenti che incapsulano il comportamente e l'UI di una singola activity. Ci ha permesso di riciclare della logica complessa e adattare le componenti grafiche a diversi layout. -* Services e AsyncTasks: per fare in modo che il thread principale non si blocchi abbiamo utilizzato dei background service. In particolare ogni operazione bloccante è incapsulata dentro un AsyncTask che ne modella il comportamento in base al risultato. diff --git a/anno3/vpc/2.algebra/extra.04.fairness.pdf b/anno3/vpc/2.algebra/extra.04.fairness.pdf new file mode 100644 index 0000000..5da2ee4 Binary files /dev/null and b/anno3/vpc/2.algebra/extra.04.fairness.pdf differ diff --git a/anno3/vpc/consegne/1/orale.org b/anno3/vpc/consegne/1/orale.org new file mode 100644 index 0000000..cc84983 --- /dev/null +++ b/anno3/vpc/consegne/1/orale.org @@ -0,0 +1,34 @@ +C := Post - Pre +Post := P x T → N + +T-flux := x | C.x = 0 +T-semiflux := x ≥ 0 +∃ m ∃σ | m[σ>m + +∀m∈RS(S) ∑y(pᵢ)m(pᵢ) = ∑y(pᵢ)m₀(pᵢ) + +liveness: +liveness (t) := ∀m∈RS(m0) ∃σ | m[σ>m' ∧ m'[t> +CTL - liveness (t) : AG(EF t) + +SOS: +Algebra := PA + SOS + Label + +E →μ E' +———————— +E || F →μ E' || F + +F →μ F' +————————— +E || F →μ F' + + +CSP (||) := E ||ₙ F | E\\F | E [[l]] F + +E →μ E'  +———————– μ∈Int +E ||ₙ F →τ E' || F + +E →μ E' +————————— μ ∈ Ext +E \\ F →μ E' \\ F diff --git a/anno3/vpc/consegne/2/gspn/Es2-RG of PT.solution/PT.mark b/anno3/vpc/consegne/2/gspn/Es2-RG of PT.solution/PT.mark index f64ce00..cbd14e1 100644 Binary files a/anno3/vpc/consegne/2/gspn/Es2-RG of PT.solution/PT.mark and b/anno3/vpc/consegne/2/gspn/Es2-RG of PT.solution/PT.mark differ diff --git a/anno3/vpc/consegne/2/gspn/Es2-RG of PT.solution/PT.net b/anno3/vpc/consegne/2/gspn/Es2-RG of PT.solution/PT.net index 7a0e34d..0553180 100644 --- a/anno3/vpc/consegne/2/gspn/Es2-RG of PT.solution/PT.net +++ b/anno3/vpc/consegne/2/gspn/Es2-RG of PT.solution/PT.net @@ -1,7 +1,8 @@ |0| | -f 0 12 0 9 0 0 0 -S0 1 2.6666666666666665 0.8333333333333334 2.6279166666666667 1.0289583333333334 0 +f 1 12 0 9 0 0 0 +n -7134 9.296875 0.9322916666666666 0 +S0 -1 2.6666666666666665 0.8333333333333334 2.6279166666666667 1.0289583333333334 0 S1_a 0 1.6666666666666667 2.3333333333333335 1.9716666666666667 2.278958333333333 0 S1_b 0 3.6666666666666665 2.3333333333333335 3.216458333333333 2.278958333333333 0 S2_a 0 1.6666666666666667 3.6666666666666665 1.9716666666666667 3.6122916666666662 0 @@ -9,7 +10,7 @@ S2_b 0 3.6666666666666665 3.6666666666666665 3.1331249999999997 3.61229 S3 0 2.6666666666666665 5.166666666666667 2.6279166666666667 5.362291666666667 0 Buffer_output 0 5.0 4.5 4.570625 4.695625 0 Buffer_input 0 5.0 1.6666666666666667 4.6175 1.8622916666666667 0 -M0 2 7.666666666666667 0.3333333333333333 7.268541666666667 0.11229166666666668 0 +M0 -1 7.666666666666667 0.3333333333333333 7.268541666666667 0.11229166666666668 0 M1 0 7.666666666666667 1.6666666666666667 7.601875 1.8622916666666667 0 M2 0 7.666666666666667 2.5 7.601875 2.195625 0 M3 0 7.666666666666667 4.0 7.351875 4.195625 0 @@ -37,7 +38,7 @@ Fine_Servizio 1.0 0 0 2 0 2.6666666666666665 4.5 1.609375 4.55729166666666 1 6 0 0 1 7 0 0 0 -Reset 1.0 0 0 1 1 1.1666666666666667 5.166666666666667 1.046875 4.973958333333333 1.25 5.234375 0 +Reset_s 1.0 0 0 1 1 1.1666666666666667 5.166666666666667 0.9739583333333334 4.973958333333333 1.25 5.234375 0 1 6 0 0 1 1 1 2 0 diff --git a/anno3/vpc/consegne/4/uppaallC.xml b/anno3/vpc/consegne/4/uppaallC.xml index ae7bd79..09f99d5 100644 --- a/anno3/vpc/consegne/4/uppaallC.xml +++ b/anno3/vpc/consegne/4/uppaallC.xml @@ -109,7 +109,7 @@ fc := 0 - + @@ -292,9 +292,9 @@ bool next = 0; send_pkg - - wait_ack - + + wait_ack + recover_loss @@ -350,8 +350,8 @@ attesa := 0 - - diff --git a/media.py b/media.py new file mode 100644 index 0000000..d3ede41 --- /dev/null +++ b/media.py @@ -0,0 +1,16 @@ +voti = [ + (28, 6), # algoritmi e compl + (30, 9), # visual. reti compl. + (29, 9), # basi dati + (29, 12),# sicurezza + reti + (30, 6), # gestione reti + (29, 6), # economia + (28, 6), # logica + (24, 9), # ling. formali + (30, 6), # mcad + (30, 6), # scpd + (26, 9) # vpc + ] + +crediti, voto = sum(map(lambda x: x[1], voti)), sum(map(lambda x: x[0]*x[1], voti)) +print(voto/crediti, voto/crediti/30*110, crediti) diff --git a/tesi/conv.py b/tesi/conv.py index c99f990..8143856 100644 --- a/tesi/conv.py +++ b/tesi/conv.py @@ -8,7 +8,8 @@ except: allsymbols = json.load(open('../unicode-latex.json')) mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀', 'ε', '₀', '₂', '₁', '₃', '₄', 'ₐ', 'ₖ', 'ᵥ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π', 'α', 'β', '∞', 'σ', '≤', '⊈', '∧', '∨', '∃', '⇒', '∩', '∉', '⋃', 'ᵏ', 'ₗ', 'ˡ', 'ₒ', 'ᵣ', 'ᴵ', '≈', '⊆', '↦' ] -extrasymbols = {'〚': '\llbracket', '〛': r'\rrbracket', '̸': '\neg', '¬̸': '\neg', '∈': '\in ', 'ₛ': '_S', 'ₜ': '_T'} +extrasymbols = {'〚': '\llbracket', '〛': r'\rrbracket', '̸': '\neg', '¬̸': '\neg', + '∈': '\in ', 'ₛ': '_S', 'ₜ': '_T'} symbols = {s: allsymbols[s] for s in mysymbols} symbols.update(extrasymbols) @@ -26,7 +27,7 @@ def read_by_char(fname): words = [w.strip() for w in line.split(' ')] if mathmode_begin.intersection(words): - assert mathmode == False + assert mathmode == False, words mathmode = True if mathmode_end.intersection(words): assert mathmode == True, f'Line: {words}, number: {cnt}' diff --git a/tesi/examples/2.cmi b/tesi/examples/2.cmi new file mode 100644 index 0000000..0271f24 Binary files /dev/null and b/tesi/examples/2.cmi differ diff --git a/tesi/examples/2.cmo b/tesi/examples/2.cmo new file mode 100644 index 0000000..32d2105 Binary files /dev/null and b/tesi/examples/2.cmo differ diff --git a/tesi/examples/2.lambda b/tesi/examples/2.lambda new file mode 100644 index 0000000..40108bd --- /dev/null +++ b/tesi/examples/2.lambda @@ -0,0 +1,7 @@ +(setglobal ll! + (let + (f1/82 = + (function param/83 + (catch (if (!= param/83 0) (observe 1) (exit 1)) with (1) + (observe 0)))) + (makeblock 0 f1/82))) diff --git a/tesi/examples/ex1.lambda b/tesi/examples/ex1.lambda new file mode 100644 index 0000000..f2cf90e --- /dev/null +++ b/tesi/examples/ex1.lambda @@ -0,0 +1,3 @@ +(setglobal Prova! + (let (f1/80 = (function param/81 : int (if (!= param/81 0) 1 0))) + (makeblock 0 f1/80))) diff --git a/tesi/examples/ex1.ml b/tesi/examples/ex1.ml new file mode 100644 index 0000000..bfc1efd --- /dev/null +++ b/tesi/examples/ex1.ml @@ -0,0 +1,6 @@ +external observe : 'a -> 'b = "observe" +external guard : 'a -> 'b = "guard" + +let f1 = function + | true -> observe 1 + | false -> observe 0 diff --git a/tesi/examples/ex2.cmi b/tesi/examples/ex2.cmi new file mode 100644 index 0000000..daf3126 Binary files /dev/null and b/tesi/examples/ex2.cmi differ diff --git a/tesi/examples/ex2.cmo b/tesi/examples/ex2.cmo new file mode 100644 index 0000000..6b6b18b Binary files /dev/null and b/tesi/examples/ex2.cmo differ diff --git a/tesi/examples/ex2.lambda b/tesi/examples/ex2.lambda new file mode 100644 index 0000000..7c15407 --- /dev/null +++ b/tesi/examples/ex2.lambda @@ -0,0 +1,7 @@ +(setglobal Ex2! + (let + (f1/82 = + (function param/83 + (catch (if (!= param/83 0) (observe 1) (exit 1)) with (1) + (observe 0)))) + (makeblock 0 f1/82))) diff --git a/tesi/examples/ex2.ml b/tesi/examples/ex2.ml new file mode 100644 index 0000000..5dee74d --- /dev/null +++ b/tesi/examples/ex2.ml @@ -0,0 +1,6 @@ +external observe : 'a -> 'b = "observe" +external guard : 'a -> 'b = "guard" + +let f1 = function + | true -> observe 1 + | _ -> observe 0 diff --git a/tesi/examples/ex3.cmi b/tesi/examples/ex3.cmi new file mode 100644 index 0000000..9a1b4e9 Binary files /dev/null and b/tesi/examples/ex3.cmi differ diff --git a/tesi/examples/ex3.cmo b/tesi/examples/ex3.cmo new file mode 100644 index 0000000..6ab1533 Binary files /dev/null and b/tesi/examples/ex3.cmo differ diff --git a/tesi/examples/ex3.lambda b/tesi/examples/ex3.lambda new file mode 100644 index 0000000..29d3036 --- /dev/null +++ b/tesi/examples/ex3.lambda @@ -0,0 +1,7 @@ +(setglobal Ex3! + (let + (f1/82 = + (function param/83 + (catch (if (!= param/83 0) (observe 1) (exit 1)) with (1) + (raise (makeblock 0 (global Match_failure/18!) [0: "ex3.ml" 4 9]))))) + (makeblock 0 f1/82))) diff --git a/tesi/examples/ex3.ml b/tesi/examples/ex3.ml new file mode 100644 index 0000000..9f20865 --- /dev/null +++ b/tesi/examples/ex3.ml @@ -0,0 +1,5 @@ +external observe : 'a -> 'b = "observe" +external guard : 'a -> 'b = "guard" + +let f1 = function + | true -> observe 1 diff --git a/tesi/ltximg/org-ltximg_03227fcbc1a148df2a10d29ac6c7c01fcd2e96c8.png b/tesi/ltximg/org-ltximg_03227fcbc1a148df2a10d29ac6c7c01fcd2e96c8.png new file mode 100644 index 0000000..0619f65 Binary files /dev/null and b/tesi/ltximg/org-ltximg_03227fcbc1a148df2a10d29ac6c7c01fcd2e96c8.png differ diff --git a/tesi/ltximg/org-ltximg_0832c2d5d5c8aee334b8e64afad5c41cf88e609a.png b/tesi/ltximg/org-ltximg_0832c2d5d5c8aee334b8e64afad5c41cf88e609a.png new file mode 100644 index 0000000..5a5c7f5 Binary files /dev/null and b/tesi/ltximg/org-ltximg_0832c2d5d5c8aee334b8e64afad5c41cf88e609a.png differ diff --git a/tesi/ltximg/org-ltximg_093cb76489045c01de4d7e5b9dfff1a0b8600496.png b/tesi/ltximg/org-ltximg_093cb76489045c01de4d7e5b9dfff1a0b8600496.png new file mode 100644 index 0000000..404ff12 Binary files /dev/null and b/tesi/ltximg/org-ltximg_093cb76489045c01de4d7e5b9dfff1a0b8600496.png differ diff --git a/tesi/ltximg/org-ltximg_09ccc75c7f1c7b226aaeecfe45f57e456cfd25fa.png b/tesi/ltximg/org-ltximg_09ccc75c7f1c7b226aaeecfe45f57e456cfd25fa.png new file mode 100644 index 0000000..56fdadd Binary files /dev/null and b/tesi/ltximg/org-ltximg_09ccc75c7f1c7b226aaeecfe45f57e456cfd25fa.png differ diff --git a/tesi/ltximg/org-ltximg_0fd5bfb9ea8d511d208850c1a6a0e61970c29865.png b/tesi/ltximg/org-ltximg_0fd5bfb9ea8d511d208850c1a6a0e61970c29865.png new file mode 100644 index 0000000..48e26da Binary files /dev/null and b/tesi/ltximg/org-ltximg_0fd5bfb9ea8d511d208850c1a6a0e61970c29865.png differ diff --git a/tesi/ltximg/org-ltximg_14f9086fc0540216445cc4e1edcb8a626f2414b5.png b/tesi/ltximg/org-ltximg_14f9086fc0540216445cc4e1edcb8a626f2414b5.png new file mode 100644 index 0000000..ad56e7c Binary files /dev/null and b/tesi/ltximg/org-ltximg_14f9086fc0540216445cc4e1edcb8a626f2414b5.png differ diff --git a/tesi/ltximg/org-ltximg_1ef798b9c67cb657e9a47c5347b3052da9a26b4a.png b/tesi/ltximg/org-ltximg_1ef798b9c67cb657e9a47c5347b3052da9a26b4a.png new file mode 100644 index 0000000..4230db9 Binary files /dev/null and b/tesi/ltximg/org-ltximg_1ef798b9c67cb657e9a47c5347b3052da9a26b4a.png differ diff --git a/tesi/ltximg/org-ltximg_20a497ed5bc28892b912021aea32760ac9f7901c.png b/tesi/ltximg/org-ltximg_20a497ed5bc28892b912021aea32760ac9f7901c.png new file mode 100644 index 0000000..7e63e2a Binary files /dev/null and b/tesi/ltximg/org-ltximg_20a497ed5bc28892b912021aea32760ac9f7901c.png differ diff --git a/tesi/ltximg/org-ltximg_228e17c3ded046091f90a52f7019aae445a4204a.png b/tesi/ltximg/org-ltximg_228e17c3ded046091f90a52f7019aae445a4204a.png new file mode 100644 index 0000000..680136d Binary files /dev/null and b/tesi/ltximg/org-ltximg_228e17c3ded046091f90a52f7019aae445a4204a.png differ diff --git a/tesi/ltximg/org-ltximg_25e330f7f372947d286a78e42231651e5b1f1452.png b/tesi/ltximg/org-ltximg_25e330f7f372947d286a78e42231651e5b1f1452.png new file mode 100644 index 0000000..6955860 Binary files /dev/null and b/tesi/ltximg/org-ltximg_25e330f7f372947d286a78e42231651e5b1f1452.png differ diff --git a/tesi/ltximg/org-ltximg_29df46f58155f4d29dade92167da906bf9672278.png b/tesi/ltximg/org-ltximg_29df46f58155f4d29dade92167da906bf9672278.png new file mode 100644 index 0000000..a7c0208 Binary files /dev/null and b/tesi/ltximg/org-ltximg_29df46f58155f4d29dade92167da906bf9672278.png differ diff --git a/tesi/ltximg/org-ltximg_2de05f2df94a432b2f417801e2e2b48e6ab08f6a.png b/tesi/ltximg/org-ltximg_2de05f2df94a432b2f417801e2e2b48e6ab08f6a.png new file mode 100644 index 0000000..1af33f8 Binary files /dev/null and b/tesi/ltximg/org-ltximg_2de05f2df94a432b2f417801e2e2b48e6ab08f6a.png differ diff --git a/tesi/ltximg/org-ltximg_2ee2ff314d1e3841e18db626412f59844788af16.png b/tesi/ltximg/org-ltximg_2ee2ff314d1e3841e18db626412f59844788af16.png new file mode 100644 index 0000000..7663e8a Binary files /dev/null and b/tesi/ltximg/org-ltximg_2ee2ff314d1e3841e18db626412f59844788af16.png differ diff --git a/tesi/ltximg/org-ltximg_338774ab42e9ea749eecdfe6a5500c36900d9eb5.png b/tesi/ltximg/org-ltximg_338774ab42e9ea749eecdfe6a5500c36900d9eb5.png new file mode 100644 index 0000000..03ea11a Binary files /dev/null and b/tesi/ltximg/org-ltximg_338774ab42e9ea749eecdfe6a5500c36900d9eb5.png differ diff --git a/tesi/ltximg/org-ltximg_369a6ac12a095bcbd8374a7245546e957e0390c4.png b/tesi/ltximg/org-ltximg_369a6ac12a095bcbd8374a7245546e957e0390c4.png new file mode 100644 index 0000000..532fa36 Binary files /dev/null and b/tesi/ltximg/org-ltximg_369a6ac12a095bcbd8374a7245546e957e0390c4.png differ diff --git a/tesi/ltximg/org-ltximg_3a2d127e08b72847ba14ddd5391dabc1e6cf8ea2.png b/tesi/ltximg/org-ltximg_3a2d127e08b72847ba14ddd5391dabc1e6cf8ea2.png new file mode 100644 index 0000000..4e09748 Binary files /dev/null and b/tesi/ltximg/org-ltximg_3a2d127e08b72847ba14ddd5391dabc1e6cf8ea2.png differ diff --git a/tesi/ltximg/org-ltximg_3aed8bc808ff090baa6dcb00db97bda8093ae534.png b/tesi/ltximg/org-ltximg_3aed8bc808ff090baa6dcb00db97bda8093ae534.png new file mode 100644 index 0000000..8bc5366 Binary files /dev/null and b/tesi/ltximg/org-ltximg_3aed8bc808ff090baa6dcb00db97bda8093ae534.png differ diff --git a/tesi/ltximg/org-ltximg_3ba6ecae9d79b8b0fe862db2cdafaa40d50a0d9d.png b/tesi/ltximg/org-ltximg_3ba6ecae9d79b8b0fe862db2cdafaa40d50a0d9d.png new file mode 100644 index 0000000..081881a Binary files /dev/null and b/tesi/ltximg/org-ltximg_3ba6ecae9d79b8b0fe862db2cdafaa40d50a0d9d.png differ diff --git a/tesi/ltximg/org-ltximg_3e1a9fcd39cf3568727bffe583267a4d07f50613.png b/tesi/ltximg/org-ltximg_3e1a9fcd39cf3568727bffe583267a4d07f50613.png new file mode 100644 index 0000000..971ccb6 Binary files /dev/null and b/tesi/ltximg/org-ltximg_3e1a9fcd39cf3568727bffe583267a4d07f50613.png differ diff --git a/tesi/ltximg/org-ltximg_3f490f4d01e0298ccd74828e897586624a2949d5.png b/tesi/ltximg/org-ltximg_3f490f4d01e0298ccd74828e897586624a2949d5.png new file mode 100644 index 0000000..ce5a557 Binary files /dev/null and b/tesi/ltximg/org-ltximg_3f490f4d01e0298ccd74828e897586624a2949d5.png differ diff --git a/tesi/ltximg/org-ltximg_4182334f7caa64e526e695a32a79f80459ee8573.png b/tesi/ltximg/org-ltximg_4182334f7caa64e526e695a32a79f80459ee8573.png new file mode 100644 index 0000000..960eece Binary files /dev/null and b/tesi/ltximg/org-ltximg_4182334f7caa64e526e695a32a79f80459ee8573.png differ diff --git a/tesi/ltximg/org-ltximg_453df5070c38153ad5ebc4b440abcf988d9e2637.png b/tesi/ltximg/org-ltximg_453df5070c38153ad5ebc4b440abcf988d9e2637.png new file mode 100644 index 0000000..95d2dc0 Binary files /dev/null and b/tesi/ltximg/org-ltximg_453df5070c38153ad5ebc4b440abcf988d9e2637.png differ diff --git a/tesi/ltximg/org-ltximg_45a48ec6a7468e1ef63760035f1cbd90d1852929.png b/tesi/ltximg/org-ltximg_45a48ec6a7468e1ef63760035f1cbd90d1852929.png new file mode 100644 index 0000000..f9add18 Binary files /dev/null and b/tesi/ltximg/org-ltximg_45a48ec6a7468e1ef63760035f1cbd90d1852929.png differ diff --git a/tesi/ltximg/org-ltximg_47726ffe44ee5e672ca5bf9c706bbf369f9833b1.png b/tesi/ltximg/org-ltximg_47726ffe44ee5e672ca5bf9c706bbf369f9833b1.png new file mode 100644 index 0000000..2efb8ff Binary files /dev/null and b/tesi/ltximg/org-ltximg_47726ffe44ee5e672ca5bf9c706bbf369f9833b1.png differ diff --git a/tesi/ltximg/org-ltximg_48b3b033fc9d7470212a5ff6b2b90806693374ec.png b/tesi/ltximg/org-ltximg_48b3b033fc9d7470212a5ff6b2b90806693374ec.png new file mode 100644 index 0000000..e656326 Binary files /dev/null and b/tesi/ltximg/org-ltximg_48b3b033fc9d7470212a5ff6b2b90806693374ec.png differ diff --git a/tesi/ltximg/org-ltximg_49912678a0f74af68111f72d4351e931bc21b7b3.png b/tesi/ltximg/org-ltximg_49912678a0f74af68111f72d4351e931bc21b7b3.png new file mode 100644 index 0000000..3c79a1b Binary files /dev/null and b/tesi/ltximg/org-ltximg_49912678a0f74af68111f72d4351e931bc21b7b3.png differ diff --git a/tesi/ltximg/org-ltximg_4fdaf8933ec67df23fc7e692c72bb705745b8fb3.png b/tesi/ltximg/org-ltximg_4fdaf8933ec67df23fc7e692c72bb705745b8fb3.png new file mode 100644 index 0000000..e0abfd4 Binary files /dev/null and b/tesi/ltximg/org-ltximg_4fdaf8933ec67df23fc7e692c72bb705745b8fb3.png differ diff --git a/tesi/ltximg/org-ltximg_512b77d569ef6cef1e6631e00039e23e77577890.png b/tesi/ltximg/org-ltximg_512b77d569ef6cef1e6631e00039e23e77577890.png new file mode 100644 index 0000000..695c338 Binary files /dev/null and b/tesi/ltximg/org-ltximg_512b77d569ef6cef1e6631e00039e23e77577890.png differ diff --git a/tesi/ltximg/org-ltximg_54c617f39a8b1c0199526df1f4ce4671395e0d8c.png b/tesi/ltximg/org-ltximg_54c617f39a8b1c0199526df1f4ce4671395e0d8c.png new file mode 100644 index 0000000..c173c4f Binary files /dev/null and b/tesi/ltximg/org-ltximg_54c617f39a8b1c0199526df1f4ce4671395e0d8c.png differ diff --git a/tesi/ltximg/org-ltximg_578b1eab1b58424d9109671f81d743d147e860eb.png b/tesi/ltximg/org-ltximg_578b1eab1b58424d9109671f81d743d147e860eb.png new file mode 100644 index 0000000..b96e211 Binary files /dev/null and b/tesi/ltximg/org-ltximg_578b1eab1b58424d9109671f81d743d147e860eb.png differ diff --git a/tesi/ltximg/org-ltximg_5bc609aa2f2b0071b2569550be7a1026d94dfb6f.png b/tesi/ltximg/org-ltximg_5bc609aa2f2b0071b2569550be7a1026d94dfb6f.png new file mode 100644 index 0000000..8a477d3 Binary files /dev/null and b/tesi/ltximg/org-ltximg_5bc609aa2f2b0071b2569550be7a1026d94dfb6f.png differ diff --git a/tesi/ltximg/org-ltximg_5df257f0a2903d4095c170b512762642e1a87103.png b/tesi/ltximg/org-ltximg_5df257f0a2903d4095c170b512762642e1a87103.png new file mode 100644 index 0000000..d20be7c Binary files /dev/null and b/tesi/ltximg/org-ltximg_5df257f0a2903d4095c170b512762642e1a87103.png differ diff --git a/tesi/ltximg/org-ltximg_5f96745abeeaf24b4c5cfe44c82bfe39268c6142.png b/tesi/ltximg/org-ltximg_5f96745abeeaf24b4c5cfe44c82bfe39268c6142.png new file mode 100644 index 0000000..65767d6 Binary files /dev/null and b/tesi/ltximg/org-ltximg_5f96745abeeaf24b4c5cfe44c82bfe39268c6142.png differ diff --git a/tesi/ltximg/org-ltximg_70e6533a4c84253e499cbdbba3b6ab9438282e59.png b/tesi/ltximg/org-ltximg_70e6533a4c84253e499cbdbba3b6ab9438282e59.png new file mode 100644 index 0000000..dede164 Binary files /dev/null and b/tesi/ltximg/org-ltximg_70e6533a4c84253e499cbdbba3b6ab9438282e59.png differ diff --git a/tesi/ltximg/org-ltximg_71053e15756ca10256f666e2307fdd59a7aadbcb.png b/tesi/ltximg/org-ltximg_71053e15756ca10256f666e2307fdd59a7aadbcb.png new file mode 100644 index 0000000..2275594 Binary files /dev/null and b/tesi/ltximg/org-ltximg_71053e15756ca10256f666e2307fdd59a7aadbcb.png differ diff --git a/tesi/ltximg/org-ltximg_71935c99897cfbec9cc5ecc9340a6e255e975120.png b/tesi/ltximg/org-ltximg_71935c99897cfbec9cc5ecc9340a6e255e975120.png new file mode 100644 index 0000000..7aaf94d Binary files /dev/null and b/tesi/ltximg/org-ltximg_71935c99897cfbec9cc5ecc9340a6e255e975120.png differ diff --git a/tesi/ltximg/org-ltximg_73727cb6bce95bed6293d8e991e92d89d0727318.png b/tesi/ltximg/org-ltximg_73727cb6bce95bed6293d8e991e92d89d0727318.png new file mode 100644 index 0000000..edef270 Binary files /dev/null and b/tesi/ltximg/org-ltximg_73727cb6bce95bed6293d8e991e92d89d0727318.png differ diff --git a/tesi/ltximg/org-ltximg_740ff4936c2062f9319e942c16158798a7931189.png b/tesi/ltximg/org-ltximg_740ff4936c2062f9319e942c16158798a7931189.png new file mode 100644 index 0000000..995bd6c Binary files /dev/null and b/tesi/ltximg/org-ltximg_740ff4936c2062f9319e942c16158798a7931189.png differ diff --git a/tesi/ltximg/org-ltximg_752ef7edb8bb466ab1a8c3d6d69d297f1596ef23.png b/tesi/ltximg/org-ltximg_752ef7edb8bb466ab1a8c3d6d69d297f1596ef23.png new file mode 100644 index 0000000..490dbbd Binary files /dev/null and b/tesi/ltximg/org-ltximg_752ef7edb8bb466ab1a8c3d6d69d297f1596ef23.png differ diff --git a/tesi/ltximg/org-ltximg_76bf33bf378f21e5b7083a1552635b3a9c32655f.png b/tesi/ltximg/org-ltximg_76bf33bf378f21e5b7083a1552635b3a9c32655f.png new file mode 100644 index 0000000..4f9cad8 Binary files /dev/null and b/tesi/ltximg/org-ltximg_76bf33bf378f21e5b7083a1552635b3a9c32655f.png differ diff --git a/tesi/ltximg/org-ltximg_7cd33dee1a75826eaff64ba0a9df42d9eb88d43d.png b/tesi/ltximg/org-ltximg_7cd33dee1a75826eaff64ba0a9df42d9eb88d43d.png new file mode 100644 index 0000000..958205b Binary files /dev/null and b/tesi/ltximg/org-ltximg_7cd33dee1a75826eaff64ba0a9df42d9eb88d43d.png differ diff --git a/tesi/ltximg/org-ltximg_7d262e185963cfbaea8ece011c7f1aa0cef4d3cf.png b/tesi/ltximg/org-ltximg_7d262e185963cfbaea8ece011c7f1aa0cef4d3cf.png new file mode 100644 index 0000000..eff0fd3 Binary files /dev/null and b/tesi/ltximg/org-ltximg_7d262e185963cfbaea8ece011c7f1aa0cef4d3cf.png differ diff --git a/tesi/ltximg/org-ltximg_8109b153ce30d3a51a7e9d1e01950030695e985e.png b/tesi/ltximg/org-ltximg_8109b153ce30d3a51a7e9d1e01950030695e985e.png new file mode 100644 index 0000000..234bbba Binary files /dev/null and b/tesi/ltximg/org-ltximg_8109b153ce30d3a51a7e9d1e01950030695e985e.png differ diff --git a/tesi/ltximg/org-ltximg_838384925f019dbac9b3c0bee1bb5e33599ec72d.png b/tesi/ltximg/org-ltximg_838384925f019dbac9b3c0bee1bb5e33599ec72d.png new file mode 100644 index 0000000..0a4392b Binary files /dev/null and b/tesi/ltximg/org-ltximg_838384925f019dbac9b3c0bee1bb5e33599ec72d.png differ diff --git a/tesi/ltximg/org-ltximg_851b349bf76722d3c7ed5128f1eab4a8fd27ff27.png b/tesi/ltximg/org-ltximg_851b349bf76722d3c7ed5128f1eab4a8fd27ff27.png new file mode 100644 index 0000000..be45b90 Binary files /dev/null and b/tesi/ltximg/org-ltximg_851b349bf76722d3c7ed5128f1eab4a8fd27ff27.png differ diff --git a/tesi/ltximg/org-ltximg_854cd5217288dadfb630427a6d96c474e4b2a4b1.png b/tesi/ltximg/org-ltximg_854cd5217288dadfb630427a6d96c474e4b2a4b1.png new file mode 100644 index 0000000..fe45789 Binary files /dev/null and b/tesi/ltximg/org-ltximg_854cd5217288dadfb630427a6d96c474e4b2a4b1.png differ diff --git a/tesi/ltximg/org-ltximg_85a4f62c7ec1b5ba9dae0c1937ce839eb7d1a88d.png b/tesi/ltximg/org-ltximg_85a4f62c7ec1b5ba9dae0c1937ce839eb7d1a88d.png new file mode 100644 index 0000000..3baea12 Binary files /dev/null and b/tesi/ltximg/org-ltximg_85a4f62c7ec1b5ba9dae0c1937ce839eb7d1a88d.png differ diff --git a/tesi/ltximg/org-ltximg_8afcbe7e285b35ddcf9adfd727f3beb3f1086cf9.png b/tesi/ltximg/org-ltximg_8afcbe7e285b35ddcf9adfd727f3beb3f1086cf9.png new file mode 100644 index 0000000..d2a10d1 Binary files /dev/null and b/tesi/ltximg/org-ltximg_8afcbe7e285b35ddcf9adfd727f3beb3f1086cf9.png differ diff --git a/tesi/ltximg/org-ltximg_919a6d1c6cec9afe325f71d95b8653c4a36b45be.png b/tesi/ltximg/org-ltximg_919a6d1c6cec9afe325f71d95b8653c4a36b45be.png new file mode 100644 index 0000000..f98f185 Binary files /dev/null and b/tesi/ltximg/org-ltximg_919a6d1c6cec9afe325f71d95b8653c4a36b45be.png differ diff --git a/tesi/ltximg/org-ltximg_9a0a62f0ef9b1f3b4a255709e18e2798b19f0894.png b/tesi/ltximg/org-ltximg_9a0a62f0ef9b1f3b4a255709e18e2798b19f0894.png new file mode 100644 index 0000000..149c24c Binary files /dev/null and b/tesi/ltximg/org-ltximg_9a0a62f0ef9b1f3b4a255709e18e2798b19f0894.png differ diff --git a/tesi/ltximg/org-ltximg_9bb98a522146b5a3d6f24ac249579d1441bf3277.png b/tesi/ltximg/org-ltximg_9bb98a522146b5a3d6f24ac249579d1441bf3277.png new file mode 100644 index 0000000..3780c07 Binary files /dev/null and b/tesi/ltximg/org-ltximg_9bb98a522146b5a3d6f24ac249579d1441bf3277.png differ diff --git a/tesi/ltximg/org-ltximg_9e3777c7d65823167b402348024168a5a4ca0277.png b/tesi/ltximg/org-ltximg_9e3777c7d65823167b402348024168a5a4ca0277.png new file mode 100644 index 0000000..c5f1f7d Binary files /dev/null and b/tesi/ltximg/org-ltximg_9e3777c7d65823167b402348024168a5a4ca0277.png differ diff --git a/tesi/ltximg/org-ltximg_a1e8e69891b5dc6ada57e2625442f11bf9eb992b.png b/tesi/ltximg/org-ltximg_a1e8e69891b5dc6ada57e2625442f11bf9eb992b.png new file mode 100644 index 0000000..c065eb7 Binary files /dev/null and b/tesi/ltximg/org-ltximg_a1e8e69891b5dc6ada57e2625442f11bf9eb992b.png differ diff --git a/tesi/ltximg/org-ltximg_ad48f6935074ca074e904584f16e8990d26f3b02.png b/tesi/ltximg/org-ltximg_ad48f6935074ca074e904584f16e8990d26f3b02.png new file mode 100644 index 0000000..4694a9e Binary files /dev/null and b/tesi/ltximg/org-ltximg_ad48f6935074ca074e904584f16e8990d26f3b02.png differ diff --git a/tesi/ltximg/org-ltximg_afdd11944175bcf8ac288bf74a587c740e3fefd1.png b/tesi/ltximg/org-ltximg_afdd11944175bcf8ac288bf74a587c740e3fefd1.png new file mode 100644 index 0000000..c93223e Binary files /dev/null and b/tesi/ltximg/org-ltximg_afdd11944175bcf8ac288bf74a587c740e3fefd1.png differ diff --git a/tesi/ltximg/org-ltximg_b079b3326ff5ebaeb842ff82746defe1d3f411f8.png b/tesi/ltximg/org-ltximg_b079b3326ff5ebaeb842ff82746defe1d3f411f8.png new file mode 100644 index 0000000..68d09eb Binary files /dev/null and b/tesi/ltximg/org-ltximg_b079b3326ff5ebaeb842ff82746defe1d3f411f8.png differ diff --git a/tesi/ltximg/org-ltximg_b1da08fd0d53a682c2d516607e04be71e4e6a9de.png b/tesi/ltximg/org-ltximg_b1da08fd0d53a682c2d516607e04be71e4e6a9de.png new file mode 100644 index 0000000..682a85d Binary files /dev/null and b/tesi/ltximg/org-ltximg_b1da08fd0d53a682c2d516607e04be71e4e6a9de.png differ diff --git a/tesi/ltximg/org-ltximg_b426c13b42ddc1070aa0eb7eded560836f4a2372.png b/tesi/ltximg/org-ltximg_b426c13b42ddc1070aa0eb7eded560836f4a2372.png new file mode 100644 index 0000000..2107ff5 Binary files /dev/null and b/tesi/ltximg/org-ltximg_b426c13b42ddc1070aa0eb7eded560836f4a2372.png differ diff --git a/tesi/ltximg/org-ltximg_b79cd5885bcbf850e0d0c99d18ed2cc590aebc56.png b/tesi/ltximg/org-ltximg_b79cd5885bcbf850e0d0c99d18ed2cc590aebc56.png new file mode 100644 index 0000000..bbef739 Binary files /dev/null and b/tesi/ltximg/org-ltximg_b79cd5885bcbf850e0d0c99d18ed2cc590aebc56.png differ diff --git a/tesi/ltximg/org-ltximg_b8ecb0782e929f5ecaeef819bb11b30254374534.png b/tesi/ltximg/org-ltximg_b8ecb0782e929f5ecaeef819bb11b30254374534.png new file mode 100644 index 0000000..dfd06d3 Binary files /dev/null and b/tesi/ltximg/org-ltximg_b8ecb0782e929f5ecaeef819bb11b30254374534.png differ diff --git a/tesi/ltximg/org-ltximg_bc09d918e9c8b4886cd1dd5f7d7f8ce4affb1188.png b/tesi/ltximg/org-ltximg_bc09d918e9c8b4886cd1dd5f7d7f8ce4affb1188.png new file mode 100644 index 0000000..f0a7771 Binary files /dev/null and b/tesi/ltximg/org-ltximg_bc09d918e9c8b4886cd1dd5f7d7f8ce4affb1188.png differ diff --git a/tesi/ltximg/org-ltximg_becd4f16674467063ae80173a8490a48b2dc9742.png b/tesi/ltximg/org-ltximg_becd4f16674467063ae80173a8490a48b2dc9742.png new file mode 100644 index 0000000..3914ef7 Binary files /dev/null and b/tesi/ltximg/org-ltximg_becd4f16674467063ae80173a8490a48b2dc9742.png differ diff --git a/tesi/ltximg/org-ltximg_c1ad106eeb267d77575a36914b0e6bd242f852a3.png b/tesi/ltximg/org-ltximg_c1ad106eeb267d77575a36914b0e6bd242f852a3.png new file mode 100644 index 0000000..5d0d1f3 Binary files /dev/null and b/tesi/ltximg/org-ltximg_c1ad106eeb267d77575a36914b0e6bd242f852a3.png differ diff --git a/tesi/ltximg/org-ltximg_c43e5a863243bfd83621b6cfb98060825faf0562.png b/tesi/ltximg/org-ltximg_c43e5a863243bfd83621b6cfb98060825faf0562.png new file mode 100644 index 0000000..a5c2497 Binary files /dev/null and b/tesi/ltximg/org-ltximg_c43e5a863243bfd83621b6cfb98060825faf0562.png differ diff --git a/tesi/ltximg/org-ltximg_c5e2f47c4f6877a60924695fbf65cc46fcf62b0c.png b/tesi/ltximg/org-ltximg_c5e2f47c4f6877a60924695fbf65cc46fcf62b0c.png new file mode 100644 index 0000000..cf9db0b Binary files /dev/null and b/tesi/ltximg/org-ltximg_c5e2f47c4f6877a60924695fbf65cc46fcf62b0c.png differ diff --git a/tesi/ltximg/org-ltximg_d30ca72849c17b48e24eb231a6fd296279f4370b.png b/tesi/ltximg/org-ltximg_d30ca72849c17b48e24eb231a6fd296279f4370b.png new file mode 100644 index 0000000..33a3ff2 Binary files /dev/null and b/tesi/ltximg/org-ltximg_d30ca72849c17b48e24eb231a6fd296279f4370b.png differ diff --git a/tesi/ltximg/org-ltximg_d47596ea59535f6b53686f66a0aa25be71f31a04.png b/tesi/ltximg/org-ltximg_d47596ea59535f6b53686f66a0aa25be71f31a04.png new file mode 100644 index 0000000..6a132ce Binary files /dev/null and b/tesi/ltximg/org-ltximg_d47596ea59535f6b53686f66a0aa25be71f31a04.png differ diff --git a/tesi/ltximg/org-ltximg_def3ad282de91b3aaed2083f098445155fa80bd3.png b/tesi/ltximg/org-ltximg_def3ad282de91b3aaed2083f098445155fa80bd3.png new file mode 100644 index 0000000..0190b54 Binary files /dev/null and b/tesi/ltximg/org-ltximg_def3ad282de91b3aaed2083f098445155fa80bd3.png differ diff --git a/tesi/ltximg/org-ltximg_e1d46cb47ee5121fb7a74fff0a5dab84c640d87d.png b/tesi/ltximg/org-ltximg_e1d46cb47ee5121fb7a74fff0a5dab84c640d87d.png new file mode 100644 index 0000000..7593d86 Binary files /dev/null and b/tesi/ltximg/org-ltximg_e1d46cb47ee5121fb7a74fff0a5dab84c640d87d.png differ diff --git a/tesi/ltximg/org-ltximg_e580eadeef26a2cf85bab7985e2280572f699cb2.png b/tesi/ltximg/org-ltximg_e580eadeef26a2cf85bab7985e2280572f699cb2.png new file mode 100644 index 0000000..7a5a6be Binary files /dev/null and b/tesi/ltximg/org-ltximg_e580eadeef26a2cf85bab7985e2280572f699cb2.png differ diff --git a/tesi/ltximg/org-ltximg_e88b511da578bfbe6155b6d3fab600e166aa16ea.png b/tesi/ltximg/org-ltximg_e88b511da578bfbe6155b6d3fab600e166aa16ea.png new file mode 100644 index 0000000..406d7b9 Binary files /dev/null and b/tesi/ltximg/org-ltximg_e88b511da578bfbe6155b6d3fab600e166aa16ea.png differ diff --git a/tesi/ltximg/org-ltximg_f16761e6ee111ffe694dd5f47d9780427d670c48.png b/tesi/ltximg/org-ltximg_f16761e6ee111ffe694dd5f47d9780427d670c48.png new file mode 100644 index 0000000..53dc897 Binary files /dev/null and b/tesi/ltximg/org-ltximg_f16761e6ee111ffe694dd5f47d9780427d670c48.png differ diff --git a/tesi/ltximg/org-ltximg_f5665c8ebc4d2e8bdc3e0c07d78050ceee37962b.png b/tesi/ltximg/org-ltximg_f5665c8ebc4d2e8bdc3e0c07d78050ceee37962b.png new file mode 100644 index 0000000..ba7cfb4 Binary files /dev/null and b/tesi/ltximg/org-ltximg_f5665c8ebc4d2e8bdc3e0c07d78050ceee37962b.png differ diff --git a/tesi/ltximg/org-ltximg_f9d9682a156264cb11c2ce64a5394950c7f1cdf4.png b/tesi/ltximg/org-ltximg_f9d9682a156264cb11c2ce64a5394950c7f1cdf4.png new file mode 100644 index 0000000..b074aa8 Binary files /dev/null and b/tesi/ltximg/org-ltximg_f9d9682a156264cb11c2ce64a5394950c7f1cdf4.png differ diff --git a/tesi/ltximg/org-ltximg_fd2a5b3aa96d8f0753109f8440bb823f534a58c2.png b/tesi/ltximg/org-ltximg_fd2a5b3aa96d8f0753109f8440bb823f534a58c2.png new file mode 100644 index 0000000..7854c94 Binary files /dev/null and b/tesi/ltximg/org-ltximg_fd2a5b3aa96d8f0753109f8440bb823f534a58c2.png differ diff --git a/tesi/ltximg/org-ltximg_fd414a76fbc47ed65287c1e1f4161ac0a8b4916c.png b/tesi/ltximg/org-ltximg_fd414a76fbc47ed65287c1e1f4161ac0a8b4916c.png new file mode 100644 index 0000000..60b25b4 Binary files /dev/null and b/tesi/ltximg/org-ltximg_fd414a76fbc47ed65287c1e1f4161ac0a8b4916c.png differ diff --git a/tesi/notations.sty b/tesi/notations.sty index a7c051c..266a38f 100644 --- a/tesi/notations.sty +++ b/tesi/notations.sty @@ -2,8 +2,14 @@ \newcommand{\bnfor}{\mathrel{\vert}} \newcommand{\paramrel}[3]{#2 \mathrel{\approx_{#1}} #3} +\newcommand{\nparamrel}[3]{#2 \mathrel{{\not\approx}_{#1}} #3} \newcommand{\vrel}[2]{\paramrel{\mathsf{val}}{#1}{#2}} -\newcommand{\trel}[2]{\paramrel{\mathsf{term}}{#1}{#2}} +\newcommand{\erel}[2]{\paramrel{\mathsf{expr}}{#1}{#2}} +\newcommand{\clerel}[2]{\paramrel{\mathsf{cl-expr}}{#1}{#2}} +\newcommand{\envrel}[2]{\paramrel{\mathsf{env}}{#1}{#2}} +\newcommand{\resrel}[2]{\paramrel{\mathsf{res}}{#1}{#2}} +\newcommand{\runrel}[2]{\paramrel{\mathsf{run}}{#1}{#2}} +\newcommand{\progrel}[2]{\paramrel{\mathsf{prog}}{#1}{#2}} \newcommand{\sem}[1]{{\llbracket{#1}\rrbracket}} @@ -16,6 +22,8 @@ \newcommand{\any}{\mathtt{\_}} % \equiv is already taken +\newcommand{\SimpleEquiv}[3]{\mathsf{equiv}(#1, #2, #3)} +\newcommand{\SourceEquiv}[2]{\mathsf{equiv}(#1, #2)} \newcommand{\Equiv}[4]{\mathsf{equiv}(#1, #2, #3, #4)} \newcommand{\Equivrel}[4]{#1 \vdash_{#4} #2 \approx #3} @@ -24,13 +32,23 @@ \newcommand{\Yes}{\mathsf{Yes}} \newcommand{\No}[2]{\mathsf{No}(#1, #2)} +\newcommand{\Root}{\mathsf{Root}} + +\newcommand{\cle}{\underline{e}} +\newcommand{\NoMatch}{\mathsf{NoMatch}} +\newcommand{\Match}[1]{\mathsf{Match}(#1)} + \newcommand{\Leaf}[1]{\mathsf{Leaf}(#1)} \newcommand{\Failure}{\mathsf{Failure}} \newcommand{\Switch}[3]{\mathsf{Switch}(#1, #2, #3)} \newcommand{\Guard}[3]{\mathsf{Guard}(#1, #2, #3)} +\newcommand{\Int}[1]{\mathsf{int}\,#1} +\newcommand{\Tag}[1]{\mathsf{tag}\,#1} + \newcommand{\emptyqueue}{\mathord{[]}} -\newcommand{\Cfb}{C_{\mathsf{fb}}} +\newcommand{\Dfb}{D_{\mathsf{fb}}} + \newcommand{\trim}[2]{\mathsf{trim}(#1, #2)} \ No newline at end of file diff --git a/tesi/tesi.pdf b/tesi/tesi.pdf new file mode 100644 index 0000000..73dea9c Binary files /dev/null and b/tesi/tesi.pdf differ diff --git a/tesi/tesi_unicode.org b/tesi/tesi_unicode.org index 8529d18..af651c2 100644 --- a/tesi/tesi_unicode.org +++ b/tesi/tesi_unicode.org @@ -26,7 +26,7 @@ TODO: chiedi a Gabriel se T e S vanno bene, ma prima controlla che siano coerent #+AUTHOR: Francesco Mecca #+EMAIL: me@francescomecca.eu #+DATE: - +#+OPTIONS: \n:t #+LANGUAGE: en #+LaTeX_CLASS: article #+LaTeX_HEADER: \linespread{1.25} @@ -51,6 +51,13 @@ TODO: chiedi a Gabriel se T e S vanno bene, ma prima controlla che siano coerent #+LaTeX_HEADER: \usepackage{stmaryrd} % llbracket, rrbracket #+LaTeX_HEADER: \usepackage{listings} #+LaTeX_HEADER: \usepackage{notations} +#+LaTeX_HEADER: \usepackage{geometry} +#+LaTeX_HEADER: \usepackage{hyperref} +#+LaTeX_HEADER: \usepackage{amsmath} +#+LaTeX_HEADER: \usepackage{appendix} +#+LaTeX_HEADER: \usepackage{a4} +#+LaTeX_HEADER: \usepackage{amsfonts} +#+LaTeX_HEADER: \usepackage{amsfonts} #+LaTeX_HEADER: \lstset{ #+LaTeX_HEADER: mathescape=true, #+LaTeX_HEADER: language=[Objective]{Caml}, @@ -82,23 +89,26 @@ For the prototype of this algorithm we have chosen a subset of the OCaml language and implemented a prototype equivalence checker along with a formal statement of correctness and its proof. The prototype is to be included in the OCaml compiler infrastructure -and will aid the development. - +and will aid the development. +\begin{comment} +TODO: should this be removed? Our equivalence algorithm works with decision trees. Source patterns are converted into a decision tree using a matrix decomposition algorithm. Target programs, described in the Lambda intermediate representation language of the OCaml compiler, are turned into decision trees by applying symbolic execution. +\end{comment} \subsection{Motivation} -Pattern matching in computer science is widely -employed technique for describing computation as well as deduction. -Pattern matching is central in many programming languages, such as the -ML family languages, Haskell and Scala, model checkers, such as Murphi -and proof assistants such as Coq and Isabelle. The work done in this -thesis provides a general method that can be applied to compilers such -as the Kotlin compiler and the C++ compiler that are considering to -implement pattern matching as a first class citizen in the language. +Pattern matching in computer science is a +widely employed technique for describing computation as well as +deduction. Pattern matching is central in many programming languages +such as the ML family languages, Haskell and Scala, different model +checkers, such as Murphi, and proof assistants such as Coq and +Isabelle. Recently the C++ community is considering [CIT] adding the +support for pattern matching in the compiler. The work done in this +thesis provides a general method that is agnostic with respect to the +compiler implementation and the language used. The work focused on the OCaml pattern matching compiler that is a critical part of the OCaml compiler in terms of correctness because @@ -106,13 +116,13 @@ bugs typically would result in wrong code production rather than triggering compilation failures. Such bugs also are hard to catch by testing because they arise in corner cases of complex patterns which are typically not in the compiler test suite or most user programs. - +\\ The OCaml core developers group considered evolving the pattern matching compiler, either by -using a new algorithm or by incremental refactoring of its code base. -For this reason we want to verify that new implementations of the +using a new algorithm or by incremental refactoring of the current code base. +For this reason we want to verify that future implementations of the compiler avoid the introduction of new bugs and that such modifications don't result in a different behavior than the current one. - +\\ One possible approach is to formally verify the pattern matching compiler implementation using a machine checked proof. Another possibility, albeit with a weaker result, is to verify that @@ -120,11 +130,12 @@ each source program and target program pair are semantically correct. We chose the latter technique, translation validation because is easier to adopt in the case of a production compiler and to integrate with an existing code base. The compiler is treated as a black-box and proof only depends on our equivalence algorithm. - +\\ \subsection{The Pattern Matching Compiler} A pattern matching compiler turns a series of pattern matching clauses -into simple control flow structures such as \texttt{if, switch}, for example: +into simple control flow structures such as \texttt{if, switch}. +For example: \begin{lstlisting} match scrutinee with | [] -> (0, None) @@ -134,11 +145,10 @@ into simple control flow structures such as \texttt{if, switch}, for example: Given as input to the pattern matching compiler, this snippet of code gets translated into the Lambda intermediate representation of the OCaml compiler. The Lambda representation of a program is shown by -calling the \texttt{ocamlc} compiler with \texttt{-drawlambda} flag. +calling the \texttt{ocamlc} compiler with the \texttt{-drawlambda} flag. In this example we renamed the variables assigned in order to ease the understanding of the tests that are performed when the code is translated into the Lambda form. -code phase. \begin{lstlisting} (function scrutinee (if scrutinee ;;; true when scrutinee (list) not empty @@ -158,10 +168,10 @@ code phase. \subsection{Our approach} Our algorithm translates both source and target programs into a common -representation, decision trees. Decision trees where chosen because +representation that we call \texttt{decision trees}. Decision trees where chosen because they model the space of possible values at a given branch of -execution. -Here are the decision trees for the source and target example program. +execution. \\ +Here are the decision trees for the source and target example program. \\ \begin{minipage}{0.5\linewidth} \scriptsize @@ -198,34 +208,29 @@ Here are the decision trees for the source and target example program. 1 (mkblock 0 x)) 2 (mkblock 0 y)) \end{verbatim} \end{minipage} - +\\ \texttt{(Root.0)} is called an \emph{accessor}, that represents the access path to a value that can be reached by deconstructing the scrutinee. In this example \texttt{Root.0} is the first subvalue of the scrutinee. - +\\ Target decision trees have a similar shape but the tests on the branches are related to the low level representation of values in Lambda code. For example, cons cells \texttt{x::xs} or tuples -\texttt{(x,y)} are blocks with tag 0. - -We can define this parametrized grammar for decision trees -A decision tree is defined as either a Leaf, a Failure terminal or -an intermediate node with different children sharing the same accessor /a/ -and an optional fallback. - -The parametrized grammar $D(\pi, e)$ describes the common structure of -source and decision trees. We use $\pi$ for the \emph{conditions} on +\texttt{(x,y)} are memory blocks with tag 0. +\\ +The following parametrized grammar $D(\pi, e)$ describes the common structure of +source and decision trees. We denote as $\pi$ the \emph{conditions} on each branch, and $a$ for our \emph{accessors}, which give a symbolic -description of a sub-value of the scrutinee. Source conditions $\pi_S$ +description of a sub-value of the scrutinee. \\ +Source conditions $\pi_S$ are just datatype constructors; target conditions $\pi_T$ are arbitrary sets of low level OCaml values. +Expressions \texttt{$e_S$} and \texttt{$e_T$} are arbitrary OCaml +expressions that are lowered by the compiler into lambda expressions. \begin{comment} possible immediate-integer or block-tag values. \end{comment} -% -\begin{mathpar} - \begin{mathpar} \begin{array}{l@{~}r@{~}r@{~}l} \text{\emph{decision trees}} & D(\pi, e) @@ -255,36 +260,106 @@ arbitrary sets of low level OCaml values. \end{array} \end{mathpar} The tree $\Leaf \cle$ returns a leaf expression $e$ in a captured -environment $\sigma$ mapping variables to accessors. -% -$\Failure$ expresses match failure, when no clause matches the input +environment $\sigma$ mapping variables to accessors.\\ + +$\Failure$ expresses a match failure that occurs when no clause matches the input value. -% +\\ $\Switch a {\Fam {i \in I} {\pi_i, D_i}} \Dfb$ has one subtree $D_i$ for every head constructor that appears in the pattern matching -clauses, and a fallback case for the constructors. -% +clauses, and a fallback case that is used when at least one variant of +the constructor doesn't appear in the clauses. The presence of the +fallback case does not imply non-exhaustive match clauses. +\begin{minipage}{0.3\linewidth} + \scriptsize +\begin{lstlisting} +let f1 = function +| true -> 1 +| false -> 0 +\end{lstlisting} +\end{minipage} +\hfill\vline\hfill +\begin{minipage}{0.3\linewidth} + \scriptsize +\begin{lstlisting} +let f1 = function +| true -> 1 +| _ -> 0 +\end{lstlisting} +\end{minipage} +\hfill\vline\hfill +\begin{minipage}{0.3\linewidth} + \scriptsize +\begin{lstlisting} +let f1 = function +| true -> 1 +\end{lstlisting} +\end{minipage} + +\begin{minipage}{0.3\linewidth} + \scriptsize +\begin{verbatim} + Switch(Root) + / \ +(Bool true) (Bool false) + / \ +Leaf(Int 1) Leaf(Int 0) +\end{verbatim} +\end{minipage} +\hfill\vline\hfill +\begin{minipage}{0.3\linewidth} + \scriptsize +\begin{verbatim} + Switch(Root) + / \ +(Bool true) (`Fallback`) + / \ +Leaf(Int 1) Leaf(Int 0) +\end{verbatim} +\end{minipage} +\hfill\vline\hfill +\begin{minipage}{0.3\linewidth} + \scriptsize +\begin{verbatim} + Switch(Root) + / \ + (Bool true) (`Fallback`) + / \ +Leaf(Int 1) Failure +\end{verbatim} +\end{minipage} +\hfill \\ +As we can see from these simple examples in which we pattern match on a +boolean constructor the fallback node in the second case implicitly +covers the path in which the value is equal to false while in the +third case the failure terminal signals the presence of non-exahustive clauses. + +\\ $\Guard \cle {D_0} {D_1}$ represents a \texttt{when}-guard on a closed expression $\cle$, expected to be of boolean type, with sub-trees $D_0$ for the \texttt{true} case and $D_1$ for the \texttt{false} case. - -We write $a(v)$ for the sub-value of the (source or target) value $v$ +\\ +We write $a(v)$ for the sub-value of the source or target value $v$ that is reachable at the accessor $a$, and $D(v)$ for the result of -running a value $v$ against a decision tree $D$; this results in -a (source or target) matching run $R(v)$, just like running the value +running a value $v$ against a decision tree $D$. +\begin{comment} +TODO: lascio o tolgo? + this results in +a source or target matching run $R(v)$, just like running the value against a program. - +\end{comment} +\\ To check the equivalence of a source and a target decision tree, we proceed by case analysis. -If we have two terminals, such as leaves in the previous example, +If we have two terminals, such as leaves in the first example, we check that the two right-hand-sides are equivalent. If we have a node $N$ and another tree $T$ we check equivalence for each child of $N$, which is a pair of a branch condition $\pi_i$ and a subtree $C_i$. For every child $(\pi_i, C_i)$ we reduce $T$ by killing all the branches that are incompatible with $\pi_i$ and check that the reduced tree is equivalent to $C_i$. - +\\ \subsection{From source programs to decision trees} Our source language supports integers, lists, tuples and all algebraic datatypes. Patterns support wildcards, constructors and literals, @@ -308,25 +383,7 @@ match w with \end{minipage} We also support \texttt{when} guards, which are interesting as they introduce the evaluation of expressions during matching. -This is the type definition of decision tree as they are used in the -prototype implementation: -\begin{lstlisting} - type decision_tree = - | Unreachable - | Failure - | Leaf of source_expr - | Guard of source_expr * decision_tree * decision_tree - | Switch of accessor * (constructor * decision_tree) list * decision_tree -\end{lstlisting} -In the \texttt{Switch} node we have one subtree for every head constructor -that appears in the pattern matching clauses and a fallback case for -other values. The branch condition $\pi_i$ expresses that the value at the -switch accessor starts with the given constructor. -\texttt{Failure} nodes express match failures for values that are not -matched by the source clauses. -\texttt{Unreachable} is used when we statically know that no value -can flow to that subtree. - +\\ We write 〚tₛ〛ₛ to denote the translation of the source program (the set of pattern matching clauses) into a decision tree, computed by a matrix decomposition algorithm (each column decomposition step gives a \texttt{Switch} node). @@ -338,7 +395,7 @@ The correctness statement intuitively states that for every source program, for every source value that is well-formed input to a source program, running the program tₛ against the input value vₛ is the same as running the compiled source program 〚tₛ〛 (that is a decision tree) against the same input -value vₛ". +value vₛ. \subsection{From target programs to decision trees} The target programs include the following Lambda constructs: @@ -350,9 +407,15 @@ and emits a \texttt{Switch} node. The branch condition $\pi_i$ is expressed as an interval set of possible values at that point. In comparison with the source decision trees, \texttt{Unreachable} nodes are never emitted. -Guards result in branching. In comparison with the source decision -trees, \texttt{Unreachable} nodes are never emitted. - +\\ +Guards are black boxes of OCaml code that branches the execution of +the symbolic engine. Whenever a guard is met, we emit a Guard node +that contains two subtrees, one for each boolean value that can result +from the evaluation of the \texttt{guard condition} at runtime. The +symbolic engine explores both paths because we will see later that for +the equivalence checking the computation of the guard condition can be skipped. +In comparison with the source decision trees, \texttt{Unreachable} nodes are never emitted. +\\ We write $\semTEX{t_T}_T$ to denote the translation of a target program tₜ into a decision tree of the target program $t_T$, satisfying the following correctness statement that is @@ -366,11 +429,6 @@ The equivalence checking algorithm takes as input a domain of possible values \emph{S} and a pair of source and target decision trees and in case the two trees are not equivalent it returns a counter example. Our algorithm respects the following correctness statement: -\begin{comment} -% TODO: we have to define what \coversTEX mean for readers to understand the specifications -% (or we use a simplifying lie by hiding \coversTEX in the statements). -\end{comment} - \begin{align*} \EquivTEX S {C_S} {C_T} = \YesTEX \;\land\; \coversTEX {C_T} S & \implies @@ -476,7 +534,7 @@ type t = Constant | Cell of int * t where a one bit tag is used to distinguish between Constant or Cell. In particular this bit of metadata is stored as the lowest bit of a memory block. - +\\ Given that all the OCaml target architectures guarantee that all pointers are divisible by four and that means that two lowest bits are always 00 storing this bit of metadata at the lowest bit allows an @@ -500,7 +558,7 @@ Elements of s-expressions are: - Variables - Strings: enclosed in double quotes and possibly escaped - S-expressions: allowing arbitrary nesting - +\\ The Lambda form is a key stage where the compiler discards type informations and maps the original source code to the runtime memory model described. @@ -574,7 +632,7 @@ In the Lambda language are several numeric types: - big integers: offer integers with arbitrary precision - floats: that use IEEE754 double-precision (64-bit) arithmetic with the addition of the literals /infinity/, /neg_infinity/ and /nan/. - +\\ The are various numeric operations defined: - Arithmetic operations: +, -, *, /, % (modulo), neg (unary negation) @@ -641,10 +699,10 @@ begin match list with | (element1 :: element2) :: [ ] -> print "two elements" | head :: tail-> print "head followed by many elements" #+END_SRC - +\\ Parenthesized patterns, such as the third one in the previous example, matches the same value as the pattern without parenthesis. - +\\ The same could be done with tuples #+BEGIN_SRC @@ -657,7 +715,7 @@ begin match tuple with The pattern pattern₁ | pattern₂ represents the logical "or" of the two patterns pattern₁ and pattern₂. A value matches pattern₁ | pattern₂ if it matches pattern₁ or pattern₂. - +\\ Pattern clauses can make the use of /guards/ to test predicates and variables can captured (binded in scope). @@ -671,7 +729,7 @@ begin match token_list with | "}"::rest -> error "syntax error: " rest #+END_SRC - +\\ Moreover, the pattern matching compiler emits a warning when a pattern is not exhaustive or some patterns are shadowed by precedent ones. @@ -689,7 +747,7 @@ branch that is being followed. Symbolic execution engines are used to track bugs by modelling the domain of all possible inputs of a program, detecting infeasible paths, dead code and proving that two code segments are equivalent. - +\\ Let's take as example this signedness bug that was found in the FreeBSD kernel and allowed, when calling the getpeername function, to read portions of kernel memory. @@ -736,7 +794,7 @@ We can see that at step 3 the set of possible values of the scrutinee /cast/ directive, that is: π_{α} ⊈ π_{σ}. For this reason the /cast/ may fail when α is /len/ negative number, outside the domain π_{σ}. In C this would trigger undefined behaviour (signed overflow) that made the exploitation possible. - +\\ Every step of evaluation can be modelled as the following transition: \[ (π_{σ}, (πᵢ)ⁱ) → (π'_{σ}, (π'ᵢ)ⁱ) @@ -766,27 +824,27 @@ Execution follows the rules of Hoare logic: \infer{ } { \{P[a/x]\}x:=a\{P\} } \end{mathpar} - +\\ - Composition : c₁ and c₂ are directives that are executed in order; {Q} is called the /midcondition/. \begin{mathpar} \infer { \{P\}c_1\{R\}, \{R\}c_2\{Q\} } { \{P\}c₁;c₂\{Q\} } \end{mathpar} - +\\ - Conditional : \begin{mathpar} \infer { \{P \wedge b \} c_1 \{Q\}, \{P\wedge\neg b\}c_2\{Q\} } { \{P\}\text{if b then $c_1$ else $c_2$}\{Q\} } \end{mathpar} - +\\ - Loop : {P} is the loop invariant. After the loop is finished /P/ holds and ¬̸b caused the loop to end. \begin{mathpar} \infer { \{P \wedge b \}c\{P\} } { \{P\}\text{while b do c} \{P \wedge \neg b\} } \end{mathpar} - +\\ Even if the semantics of symbolic execution engines are well defined, the user may run into different complications when applying such analysis to non trivial codebases. @@ -808,7 +866,7 @@ a translator cannot be generalized and reused to prove another translator. Translation validation is an alternative to the verification of existing translators that consists of taking the source and the target (compiled) program and proving /a posteriori/ their semantic equivalence. - +\\ - [ ] Techniques for translation validation - [ ] What does semantically equivalent mean - [ ] What happens when there is no semantic equivalence @@ -827,9 +885,9 @@ following form: |\vert pattern₃ as var \to expr₃ |⋮ |\vert pₙ \to exprₙ - +\\ Patterns could or could not be exhaustive. - +\\ Pattern matching code could also be written using the more compact form: |function |\vert pattern₁ \to expr₁ @@ -871,11 +929,11 @@ Patterns are encoded in the following way: | p₁ as x | Assignment | | c(p₁,p₂,...,pₙ) | Constructor | | (p₁\vert p₂) | Orpat | - +\\ Once parsed, the type declarations and the list of clauses are encoded in the form of a matrix that is later evaluated using a matrix decomposition algorithm. - +\\ Patterns are of the form | pattern | type of pattern | |-----------------+---------------------| @@ -883,7 +941,7 @@ Patterns are of the form | x | variable | | c(p₁,p₂,...,pₙ) | constructor pattern | | (p₁\vert p₂) | or-pattern | - +\\ The pattern /p/ matches a value /v/, written as p ≼ v, when one of the following rules apply @@ -901,7 +959,7 @@ When a value /v/ matches pattern /p/ we say that /v/ is an /instance/ of /p/. During compilation by the translators, expressions at the right-hand-side are compiled into Lambda code and are referred as lambda code actions lᵢ. - +\\ We define the /pattern matrix/ P as the matrix |m x n| where m bigger or equal than the number of clauses in the source program and n is equal to the arity of the constructor with the gratest arity. @@ -922,14 +980,14 @@ $\vec{v}$ = (v₁, v₂, ..., vᵢ) matches the pattern vector pᵢ in P if and conditions are satisfied: - p_{i,1}, p_{i,2}, \cdots, p_{i,n} ≼ (v₁, v₂, ..., vᵢ) - ∀j < i p_{j,1}, p_{j,2}, \cdots, p_{j,n} ⋠ (v₁, v₂, ..., vᵢ) - +\\ We can define the following three relations with respect to patterns: - Pattern p is less precise than pattern q, written p ≼ q, when all instances of q are instances of p - Pattern p and q are equivalent, written p ≡ q, when their instances are the same - Patterns p and q are compatible when they share a common instance - +\\ Wit the support of two auxiliary functions - tail of an ordered family | tail((xᵢ)^{i ∈ I}) := (xᵢ)^{i ≠ min(I)} @@ -946,14 +1004,14 @@ vector of the same length, that is (pᵢ)ⁱ(vᵢ)ⁱ | (K(qⱼ)ʲ, tail(pᵢ)ⁱ) | (K(v'ⱼ)ʲ,tail(vⱼ)ʲ) | ((qⱼ)ʲ +++ tail(pᵢ)ⁱ)((v'ⱼ)ʲ +++ tail(vᵢ)ⁱ) | | (K(qⱼ)ʲ, tail(pᵢ)ⁱ) | (K'(v'ₗ)ˡ,tail(vⱼ)ʲ) | ⊥ if K ≠ K' | | (q₁\vert{}q₂, tail(pᵢ)ⁱ) | (vᵢ)ⁱ | First((q₁,tail(pᵢ)ⁱ)(vᵢ)ⁱ, (q₂,tail(pᵢ)ⁱ)(vᵢ)ⁱ) | - +\\ A source program tₛ is a collection of pattern clauses pointing to /bb/ terms. Running a program tₛ against an input value vₛ, written tₛ(vₛ) produces a result /r/ belonging to the following grammar: | tₛ ::= (p → bb)^{i∈I} | tₛ(vₛ) → r | r ::= guard list * (Match (σ, bb) \vert{} NoMatch \vert{} Absurd) - +\\ \begin{comment} TODO: running a value against a tree: | Leaf(bb) (vᵢ) := bb @@ -962,7 +1020,7 @@ TODO: running a value against a tree: | Node(a, Cᵢ, C?) := C_min{i | Cᵢ(vᵢ(a)) ≠ ⊥} | Node (a, Cᵢ, None) := ⊥ if ∀Cᵢ, Cᵢ(vᵢ(a)) = ⊥ | Node (a, Cᵢ, C?) := C?(vᵢ(a)) if ∀Cᵢ, Cᵢ(vᵢ(a)) = ⊥ - +\\ \end{comment} \begin{comment} @@ -1050,7 +1108,7 @@ p_{2,1} & p_{2,2} & \cdots & p_{2,n} → l₂ \\ p_{m,1} & p_{m,2} & \cdots & p_{m,n} → lₘ \end{pmatrix}) \end{equation*} - +\\ The base case C₀ of the algorithm is the case in which the $\vec{x}$ is an empty sequence and the result of the compilation C₀ is l₁ @@ -1063,7 +1121,7 @@ C₀((), → lₘ \end{pmatrix}) = l₁ \end{equation*} - +\\ When $\vec{x}$ ≠ () then the compilation advances using one of the following four rules: @@ -1121,7 +1179,7 @@ following four rules: case cₖ: lₖ default: exit \end{lstlisting} - +\\ 3) Orpat rule: there are various strategies for dealing with or-patterns. The most naive one is to split the or-patterns. For example a row p containing an or-pattern: @@ -1239,7 +1297,7 @@ This is the grammar of the target language (TODO: check menhir grammar) | bexpr ::= "(" ("!="\vert{}"=="\vert{}">="\vert{}"<="\vert{}">"\vert{}"<") sexpr digit \vert{} field ")" | label ::= integer The prototype doesn't support strings. - +\\ The AST built by the parser is traversed and evaluated by the symbolic execution engine. Given that the target language supports jumps in the form of "catch - exit" @@ -1297,14 +1355,14 @@ is a series of control-flow conditionals (\texttt{if, switch, Match\_failure, catch, exit}), value access (\texttt{field}), variable bindings (\texttt{let}) and comparison operators in Lambda code, with arbitrary Lambda-code expressions $e_T$ at the leaves. - +\\ We assume given an equivalence relation $\erel {e_S} {e_T}$ on expressions (that are contained in the leaves of the decision trees). In our translation-validation setting, it suffices to relate each source expression to its compiled form -- the compiler computes this relation. We have to lift this relation on leaves into an equivalence procedure for (pattern-matching) programs. - +\\ We already defined what it means to run a value vₛ against a program tₛ: | tₛ(vₛ) := NoMatch \quad if ∀i, pᵢ(vₛ) = ⊥ @@ -1358,14 +1416,42 @@ environment $\sigma$ captured by a program, and what it means to ``run'' a value against a program or a decision, written $t(v)$ and $D(v)$, which returns a trace $(\cle_1, \dots, \cle_n)$ of the executed guards and a \emph{matching result} $r$. - +\\ Once formulated in this way, our equivalence algorithm must check the natural notion of input-output equivalence for matching programs, captured by the relation $\progrel {t_S} {t_T}$. # TODO eq_muovi \subsection{Grammar of the decision trees} +We have already given the parametrized grammar for decision trees that +we will now explore in details. +\begin{mathpar} + \begin{array}{l@{~}r@{~}r@{~}l} + \text{\emph{decision trees}} & D(\pi, e) + & \bnfeq & \Leaf {\cle(a)} \\ + & & \bnfor & \Failure \\ + & & \bnfor & \Switch a {\Fam {i \in I} {\pi_i, D_i}} \Dfb \\ + & & \bnfor & \Guard {\cle(a)} {D_0} {D_1} \\ + & & \bnfor & Unreachable \\ + \text{\emph{accessors}} & a + & \bnfeq & \Root \;\bnfor\; a.n \quad (n \in \mathbb{N}) \\ + \end{array} + \quad + \begin{array}{l} + \pi_S : \text{datatype constructors} + \\ + \pi_T \subseteq \{ \Int n \mid n \in \mathbb{Z} \} + \uplus \{ \Tag n \mid n \in \mathbb{N} \} + \\[1em] + a(v_S), a(v_T), D_S(v_S), D_T(v_T) + \end{array} +\end{mathpar} +While the branches of a decision tree represents intuitively the +possible paths that a program can take, branch conditions πₛ and πₜ +represents the shape of possible values that can flow along that path. +They refine +\\ \subsection{From source programs to decision trees} Let's consider some trivial examples: | function true -> 1 @@ -1386,17 +1472,18 @@ It is possible to produce Unreachable examples by using |\vert{} _ -> . that gets translated into | Switch ([(true, Leaf 1); (false, Leaf 2)], Unreachable) - +\\ We trust this annotation, which is reasonable as the type-checker verifies that it indeed holds. We'll see that while we can build Unreachable nodes from source programs, in the lambda target there isn't a construct equivalent to the refutation clause. - +\\ Guard nodes of the tree are emitted whenever a guard is found. Guards node contains a blackbox of code that is never evaluated and two branches, one that is taken in case the guard evaluates to true and the other one that contains the path taken when the guard evaluates to true. +\begin{comment} Are K and Here clear here? \end{comment} We say that a translation of a source program to a decision tree @@ -1472,7 +1559,7 @@ of the head constructors Kₖ, then running (v_i)^i against m is the same as running it against the submatrix m_{Kₖ}; otherwise (its head constructor ∉ (Kₖ)ᵏ) it is equivalent to running it against the wildcard submatrix. - +\\ We formalize this intuition as follows *** Lemma (Groups): Let /m/ be a matrix with @@ -1495,7 +1582,7 @@ Let /m/ be a matrix ((aᵢ)ⁱ, ((pᵢⱼ)ⁱ → eⱼ)ʲ) with Below we are going to assume that m is a simplified matrix such that the first row does not contain an or-pattern or a binding to a variable. - +\\ Let (vᵢ)ⁱ be an input matrix with v₀ = Kᵥ(v'_{l})ˡ for some constructor Kᵥ. We have to show that: - if Kₖ = Kᵥ for some Kₖ ∈ constrs(p₀ⱼ)ʲ, then @@ -1504,7 +1591,7 @@ We have to show that: m(vᵢ)ⁱ = m_{wild}(tail(vᵢ)ⁱ) Let us call (rₖⱼ) the j-th row of the submatrix mₖ, and rⱼ_{wild} the j-th row of the wildcard submatrix m_{wild}. - +\\ Our goal contains same-behavior equalities between matrices, for a fixed input vector (vᵢ)ⁱ. It suffices to show same-behavior equalities between each row of the matrices for this input @@ -1536,7 +1623,7 @@ By definition of (pᵢ)ⁱ(vᵢ)ⁱ we know that (pᵢⱼ)ⁱ(vᵢ) is equal to | (K(qⱼ)ʲ, tail(pᵢⱼ)ⁱ) (K'(v'ₗ)ˡ,tail(vⱼ)ʲ) := ⊥ if K ≠ K' We prove this first case by a second case analysis on p₀ⱼ. - +\\ TODO \begin{comment} GOAL: @@ -1548,19 +1635,19 @@ case analysis on pₒⱼ: | else | ⊥ | that is exactly the same as rₖⱼ := (qₗ)ˡ +++ tail(pᵢⱼ)ⁱ → eⱼ But I am just putting together the definition given above (in the pdf). - +\\ Second case, below: the wildcard matrix r_{jwild} is | tail(aᵢ)ⁱ, (tail(pᵢⱼ)ⁱ → eⱼ if p₀ⱼ is _ else ⊥)ʲ - +\\ case analysis on p₀ⱼ: | pₒⱼ | (pᵢⱼ)ⁱ | |--------+-----------------------| | Kₖ(qₗ) | (qₗ)ˡ +++ tail(pᵢⱼ)ⁱ | not possible because we are in the second case | _ | (_)ˡ +++ tail(pᵢⱼ)ⁱ | | else | ⊥ | - +\\ Both seems too trivial to be correct. @@ -1683,13 +1770,13 @@ hand side. \begin{mathpar} \infer - {C_S \in {\Leaf t, \Failure} + {D_S \in {\Leaf t, \Failure} \\ - \forall i,\; \EquivTEX {(S \land a \in D_i)} {C_S} {C_i} G + \forall i,\; \EquivTEX {(S \land a \in D_i)} {D_S} {D_i} G \\ - \EquivTEX {(S \land a \notin \Fam i {D_i})} {C_S} \Cfb G} + \EquivTEX {(S \land a \notin \Fam i {D_i})} {D_S} \Dfb G} {\EquivTEX S - {C_S} {\Switch a {\Fam i {D_i} {C_i}} \Cfb} G} + {D_S} {\Switch a {\Fam i {D_i} {D_i}} \Dfb} G} \end{mathpar} \begin{comment} @@ -1713,14 +1800,14 @@ result in an empty intersection. If the accessors are different, {\forall i,\; \EquivTEX {(S \land a = K_i)} - {C_i} {\trim {C_T} {a = K_i}} G + {D_i} {\trim {D_T} {a = K_i}} G \\ \EquivTEX {(S \land a \notin \Fam i {K_i})} - \Cfb {\trim {C_T} {a \notin \Fam i {K_i}}} G + \Dfb {\trim {D_T} {a \notin \Fam i {K_i}}} G } {\EquivTEX S - {\Switch a {\Fam i {K_i, C_i}} \Cfb} {C_T} G} + {\Switch a {\Fam i {K_i, D_i}} \Dfb} {D_T} G} \end{mathpar} The equivalence checking algorithm deals with guards by storing a @@ -1770,7 +1857,7 @@ The result of the proposed equivalence algorithm is /Yes/ or /No(vₛ, vₜ)/. In particular, in the negative case, vₛ and vₜ are a couple of possible counter examples for which the decision trees produce a different result. - +\\ In the presence of guards we can say that two results are equivalent modulo the guards queue, written /r₁ ≃gs r₂/, when: | (gs₁, r₁) ≃gs (gs₂, r₂) ⇔ (gs₁, r₁) = (gs₂ ++ gs, r₂) @@ -1840,7 +1927,7 @@ Covering lemma: The equivalence checking algorithm takes as parameters an input space /S/, a source decision tree /Cₛ/ and a target decision tree /Cₜ/: | equiv(S, Cₛ, Cₜ) → Yes \vert{} No(vₛ, vₜ) - +\\ When the algorithm returns Yes and the input space is covered by /Cₛ/ we can say that the couple of decision trees are the same for every couple of source value /vₛ/ and target value /vₜ/ that are equivalent. @@ -1862,7 +1949,7 @@ There exists and are injective: | tag(k) ∈ ℕ (arity(k) > 0) | π(k) = {n\vert int(k) = n} x {n\vert tag(k) = n} where k is a constructor. - +\\ \begin{comment} TODO: explain: ∀v∈a→π, C_{/a→π}(v) = C(v) diff --git a/todo.org b/todo.org index 0b294a9..3737887 100644 --- a/todo.org +++ b/todo.org @@ -14,30 +14,36 @@ - [X] Vedi bisimulazione ed equivalenze in teoria analisi - [X] Che significa urgente in uppaal? - [X] Uppaal: x = 0 come guardia, non == -- [-] Teoria [8/21] +- [-] Teoria [26/29] - [X] Come metti a parole \to ? - - [ ] Hierarchy of equivalences - - [ ] algebra.extra.lucca: internal/external choices - - [ ] Observer e testing equivalence + - [X] Hierarchy of equivalences + - [X] Automa di Buchi + - [X] Ultimo pacco BDD e CTL + - [ ] Prodotto relazionale BDD + - [X] Def formale struttura Kripke + - [X] algebra.extra.lucca: internal/external choices + - [X] Observer e testing equivalence - [X] Vedi bene legge conservazione token - - [ ] Vedi bene fairness, liveness come formule? - - [ ] Vedi da relazioni procedure dimostrazione deadlock - - [ ] Impara equivalenze come le spiega lei - - [ ] Formalizza algoritmo bisimulazione - - [ ] Vedi slide 42 ltl: liveness, safety, fairness, anche in CTL - - [ ] CTL e LTL: set operatori minimo per derivare altri + - [X] Vedi bene fairness, liveness come formule? + - [X] Vedi da relazioni procedure dimostrazione deadlock + - [X] Impara equivalenze come le spiega lei + - [X] Formalizza algoritmo bisimulazione + - [X] Vedi slide 42 ltl: liveness, safety, fairness, anche in CTL + - [X] CTL e LTL: set operatori minimo per derivare altri - [X] Manca CTL* ? - [X] Pstate? stato che appartiene al linguaggio (o set di label) - della struttura di Kripke - - [ ] BDD e decision diagrams, tutto Amparore + - [X] BDD e decision diagrams, tutto Amparore - [X] Galla`: TCTL z in \phi - [X] Slide 44 TCTL? reset? - - [ ] Slides 49-50 di TCTL + - [X] Slides 49-50 di TCTL - [X] Equivalenza clock. Davvero mantissa e parte frazionaria? - [X] Galla`: che devo dire sulle WN? - - [ ] Rivedi WN - - [ ] Perche` sono utili gli t-semiflussi? PN consistente? - - [ ] Assicurati di sapere le sigle + - [X] Rivedi WN + - [ ] Pagina 2: fondo state eq + - [X] Ripeti preset e postset + - [ ] PN consistente? + - [X] Perche` sono utili gli t-semiflussi? PN consistente? + - [X] Assicurati di sapere le sigle - [X] rete A, b, c, d [6/6] + [X] Spiega p-t-semiflows analysis: deadlock e liveness, boundness + [X] sulle slide, quando si chiede come deve decidere il master @@ -106,11 +112,19 @@ - [ ] Richiedi date esame -* Tesi [3/9] +* Tesi [3/27] - [ ] Rivedere inference rules di Gabriel e aggiustarle con le mie +- [ ] Definisci domain sempre allo stesso modo, con bigcup o | - [ ] Definizione di First(x_i): serve? - [ ] Equivalenza R_s R_T (run) - [ ] TODO t_t +- [ ] Introduzione: Explain covers alla fine (o vedi che si fa nel paper) +- [ ] Paginazione: + + [ ] figura (function scrutinee) fuori pagina + + [ ] figura primo decision tree: migliorala + + [ ] Line breaks + + [ ] Esempio full signature match: allinea + + [ ] correct. stat. di eq. checking: fuori margine - [X] segreteria: tesi inglese - [X] Gatti: inglese - [X] Gatti: Coppo mio relatore @@ -142,3 +156,4 @@ - [ ] TODO on the org file HALP HALP! +