AA 2016-2017 18. Interpre+, compilatori e semanca...

51
18. Interpre+, compilatori e seman+ca operazionale AA 2016-2017 1

Transcript of AA 2016-2017 18. Interpre+, compilatori e semanca...

Page 1: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

18.Interpre+,compilatorieseman+caoperazionale

AA2016-2017

1

Page 2: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Linguaggidiprogrammazione

  Comesicomprendonolecara:eris;chediunlinguaggiodiprogrammazione?Molterispostediverse…o  manuali,documentazioneon-line,esempi,consultazionestackoverflow.com,…

  Lanostrarispostao  lacomprensionediunlinguaggiodiprogrammazionesioDenedallaseman+cadellinguaggio

Seman;cacomeguidaallaproge:azione,all’implementazioneeall’usodiunlinguaggiodiprogrammazione

2

Page 3: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Elemen+diseman+caoperazionale

3

Page 4: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Sintassieseman;ca

  Unlinguaggiodiprogrammazionepossiedeo  unasintassi,chedefinisce

!  le“formulebenformate”dellinguaggio,cioèiprogrammisintaDcamentecorreD,;picamentegenera;daunagramma;ca

o  unaseman+ca,chefornisce! un’interpretazionedei“token”interminidien;tà(matema;che)note

! unsignificatoaiprogrammisintaDcamentecorreD  Lateoriadeilinguaggiformalifornisceformalismidispecifica(gramma;che)etecnichedianalisi(automi)pertra:areaspeDsintaDci

  Perlaseman;caesistonodiversiapproccio  denotazionale,operazionale,assioma+ca,…

  Laseman;caformalevienedisolitodefinitasuunarappresentazionedeiprogrammiinsintassiastra;a

4

Page 5: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Sintassiconcreta

  Lasintassiconcretadiunlinguaggiodiprogrammazioneèdefinitadisolitodaunagramma+caliberadacontesto(comevistoaPR1)Esempio:gramma;cadisempliciespressionilogiche(inBackus-NaurForm,BNF)o  e::=v|Note|(eAnde)|(eOre)|(eImpliese)o  v::=True|FalseNotazionecomodaperprogrammatori(operatoriinfissi,associa;vità-commuta;vitàdioperatori,precedenze)Menocomodaperunages;onecomputazionale(sipensiaproblemidiambiguità)

5

Page 6: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Sintassiastra:a

L’alberosintaKco(abstractsyntaxtree)diun’espressioneexpmostra(risolvendoleambiguità)comeexppuòesseregeneratadallagramma;ca  Lasintassiastra;aèunarappresentazionelinearedell’alberosintaDcoo  glioperatorisononodidell’alberoeglioperandisonorappresenta;daiso:oalberi

  PergliASTabbiamoquindisiaunanotazionelinearecheunarappresentazionegrafica

6

Page 7: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Dallasintassiconcretaall’AST

7

(True And False) Implies ((Not True) And False)

SINTASSICONCRETA

Implies(And(True,False), And(Not(True),False) )

SINTASSIASTRATTA

ALBEROSINTATTICO

Page 8: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Seman;cadeilinguaggi

Tremetodiprincipalidianalisiseman;cao  Seman2caoperazionale:descriveilsignificatodiunprogrammainterminidell’evoluzione(cambiamen;distato)diunamacchinaastra:a

o  Seman2cadenotazionale:ilsignificatodiunprogrammaèunafunzionematema;cadefinitasuopportunidomini

o  Sema2caassioma2ca:descriveilsignificatodiunprogrammainbasealleproprietàchesonosoddisfa:eprimaedopolasuaesecuzione

Ognimetodohavantaggiesvantaggirispe:oadaspeDmatema;ci,facilitàdiusonelledimostrazioni,ou;litàneldefinireuninterpreteouncompilatoreperillinguaggio

8

Page 9: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

EdiquestocosasivedeinPR2?

  MetodologieperOOPo  qualcosadiseman;caassioma;ca,informalmenteo  clausoleRequires&Effecto  Representa;onInvariant

  Comprensionedeiparadigmideilinguaggidiprogrammazioneo  useremounaseman;caoperazionale

9

Page 10: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Seman;caoperazionale

  Idea:laseman;caoperazionalediunlinguaggioLdefinisceinmodoformale,construmen2matema2ci,unamacchinaastra:aMLingradodieseguireiprogrammiscriDinL  Definizione:unsistemaditransizioniècos;tuitodao  uninsiemeConfigdiconfigurazioni(sta;)o  unarelazioneditransizione−→⊆Config×Config  Notazione:c−→dsignificachecedsononellarelazione−→  Intuizione:c−→dlostatocevolvenellostatod

10

Page 11: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Seman;caoperazionale“smallstep”

  Nellaseman;caoperazionale“smallstep”larelazioneditransizionedescriveunpassodelprocessodicalcolo  Abbiamounatransizionee−→dsepartendodall’espressione(oprogramma)el’esecuzionediunpassodicalcolociportanell’espressioned  Unavalutazionecompletadieavràquindilaformae−→e1−→e2…−→endoveenpuòrappresentareilvalorefinaledie  Nellaseman;casmall-steplavalutazionediunprogrammaprocedea:raversoleconfigurazioniintermediechepuòassumereilprogramma

11

Page 12: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Seman;caoperazionale“bigstep”

  Nellaseman;caoperazionale“bigstep”larelazioneditransizionedescrivelavalutazionecompletadiunprogramma/espressione  Scriviamoe=>vsel’esecuzionedelprogramma/espressioneeproduceilvalorev  Notazionealterna;va(equivalente)u;lizzatainmol;tes;:e⇓v  Comevedremo,unavalutazionecompletadiun’espressioneèo:enutacomponendolevalutazionicompletedellesueso:o-espressioni

12

Page 13: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Seman;caoperazionaleinPR2

  Lavisionedelcorso:u;lizzeremolaseman;caoperazionale“bigstep”comemodelloperdescrivereimeccanismidicalcolodeilinguaggidiprogrammazione  Laseman;caoperazionale“smallstep”sarebbeu;lenelcasodilinguaggiconcorren;perdescriverelecomunicazionieproprietàqualiladeadlockfreedom

13

Page 14: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Seman;caoperazionale“bigstep”diespressionilogiche

14

true⇒ truefalse⇒ false

VALORI

e1⇒ v1 e2 ⇒ v2e1 and e2 ⇒ v1∧v2

(and)

RegoledivalutazioneanalogheperOReIMPLIESUsiamoOPERATORILOGICIsul

dominiodeivaloricontabellediverità

e⇒ v not e⇒¬v

(not)

Page 15: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Regoleederivazioni

  Leregoledivalutazionepossonoesserecompostepero:enerelavalutazionediunaespressionepiùcomplessa  Questofornisceunaprovadiunaderivazioneoperazionaledicalcolo

15

Page 16: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Regolediderivazione

  Leregoledivalutazionecos;tuisconounproofsystem(sistemadidimostrazione)

  Tipicamenteleregolesonodefiniteperinduzionestru:uralesullasintassidellinguaggio

  Le“formule”checiinteressadimostraresonotransizionidel;poe=>v

  Componiamoleregoleinbaseallastru:urasintaDcadieo:enendounprooftree

16

premessa1 ... premessakconclusione

Page 17: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Regoleeinterprete

  Leregoledivalutazionedefinisconol’interpretedellamacchinaastra:a“formale”definitadallaseman;caoperazionale  Quindileregoledescrivonoilprocessodicalcolo  NelcorsoforniremounacodificaOCamldellaseman;caoperazionale  Diconseguenzao:erremounmodelloeseguibiledell’interpretedellinguaggio

17

Page 18: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Interpreteespressionilogiche

18

Page 19: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Passo1:sintassiastra:a

19

typeBoolExp=|True|False|NotofBoolExp|AndofBoolExp*BoolExp

Definizionedellasintassiastra;atramitei+pialgebricidiOCaml

Page 20: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Passo2:dalleregoledivalutazioneall’interpreteOCaml

ObieDvo:definireunafunzioneevaltalecheeval(e)=vseesolosee=>vEsempio:dallaregolao:eniamoilseguentecodiceOCaml

20

eval Not(exp0) -> match eval exp0 with True -> False | False -> True€

e⇒ v not e ⇒ ¬v

Page 21: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Passo3:Interpretediespressionilogiche(True,False,And,Not)

21

let rec eval exp = match exp with True -> True | False -> False | Not(exp0) -> match eval exp0 with True -> False | False -> True | And(exp0,exp1) ->

match (eval exp0, eval exp1) with (True,True) -> True | (_,False) -> False | (False,_) -> False

Page 22: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Espressioniavaloriinteri

22

Page 23: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

SintassiOCaml(astra:a)

23

typeexpr=|CstIofint //costan;intere|Varofstring //variabili|Primofstring*expr*expr //operatoribinari

Page 24: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Ambiente(1)

  Perdefinirel’interpretedobbiamointrodurreunastru9uradiimplementazione(run-2mestructure)cheperme:adirecuperareivaloriassocia;agliiden;ficatori  Unbindingèun’associazionetraunnomeeunvaloreo  ilnomesolitamenteèu;lizzatoperreperireilvaloreo  esempioinMLlet x = 2 + 1 in let y = x + x in x * y

o  ilbindingdixè3,ilbindingdiyè6,ilvalorecalcolatodalprogrammaè18

24

Page 25: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Ambiente(2)

  Unambienteenvèunacollezionedibinding  Esempioenv={x->25,y->6}  L’ambienteenvcon;enedue“binding”o  l’associazionetral’iden;ficatorexeilvalore25o  l’associazionetral’iden;ficatoreyeilvalore6o  l’iden;ficatoreznonèlegatonell’ambiente  Astra:amenteunambienteèunafunzionedi;po

Ide"Value+Unbound  L’usodellacostanteUnboundperme:edirenderelafunzionetotale

25

Page 26: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Notazione

Datounambienteenv:Ide"Value+Unboundenv(x)denotailvalorevassociatoaxnell’ambienteoppureilvalorespecialeUnboundenv[v/x]indical’ambientecosìdefinitoo  env[v/x](y)=vsey=xo  env[v/x](y)=env(y)sey!=xEsempio:seenv={x->25,y->7}alloraenv[5/x]={x->5,y->7}

26

Page 27: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Implementazione(naïve)

27

let emptyenv = [](* the empty environment *)

let rec lookup env x = match env with | [] -> failwith ("not found") | (y, v)::r -> if x = y then v else lookup r x

Page 28: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Regoledivalutazione:codiceinterprete

28

eval(Varx)env->lookupenvx

env(x) = venv Var x⇒ v

env e1⇒ v1 env e2⇒ v2env Prim(+,e1,e2) ⇒ v1+ v2

evalPrim("+",e1,e2)env->evale1env+evale2env

Page 29: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Interpretepersempliciespressioniintere

29

(* la valutazione è parametrica rispetto a env *)

let rec eval e (env : (string * int) list) : int = match e with | CstI i -> i | Var x -> lookup env x | Prim("+", e1, e2) -> eval e1 env + eval e2 env | Prim("*", e1, e2) -> eval e1 env * eval e2 env | Prim("-", e1, e2) -> eval e1 env - eval e2 env | Prim _ -> failwith "unknown primitive”

Page 30: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

AmbientecomeTDA

Qualisonoleoperazionisignifica;veperoperaresuambien;?  Create()//EFFECTS:creal’ambientevuoto  voidBind(x:Ide,v:Value)//EFFECTS:estendethisconillegametraxev  ValueLoookup(x:Ide)throwUnboundExcep;on//EFFECTS:res;tuisceilvaloreassociatoaxinthis.Solleval’eccezionesethisnoncon;enelegamiperx

30

Page 31: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Acosaserve?

  Lanozionediambiente(inle:eraturaanchenotaconilnomediNameSpaceAlgebra)vieneu;lizzatapermodellarediversiaspeDdeilinguaggidiprogrammazioneo  tabelladeisimbolio  recorddiaDvazioneo  record(lestructdelC)o  oggeDo  …

31

Page 32: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Aggiungiamoledichiarazioni

32

let z = 17 in z + z CORPO

DICHIARAZIONE

Page 33: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Espressionicondich.:sintassiastra:a

33

type expr = | CstI of int | Var of string | Let of string * expr * expr | Prim of string * expr * expr

EsempioLet("z", CstI 17, Prim("+", Var "z", Var "z"))

In sintassi concreta

let z = 17 in z + z

Page 34: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

RegoladelLet

34

env▹ erhs⇒ xval env[xval / x]▹ ebody⇒ venv▹ Let x = erhs in ebody⇒ v

eval (Let(x, erhs, ebody)) env -> let xval = eval erhs env in let env1 = (x, xval) :: env in eval ebody env1

•  Sivalutaehrsnell’ambientecorrenteo:enendoxval•  Sivalutaebodynell’ambienteestesoconillegametraxexval

o:enendoilvalorev•  Lavalutazionedel“let”nell’ambientecorrenteproduceilvalorev

Page 35: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Interpreteperespressionicondichiarazioni

35

let rec eval e (env : (string * int) list) : int = match e with | CstI i -> i | Var x -> lookup env x | Let(x, erhs, ebody) -> let xval = eval erhs env in let env1 = (x, xval) :: env in eval ebody env1 | Prim("+", e1, e2) -> eval e1 env + eval e2 env | Prim("*", e1, e2) -> eval e1 env * eval e2 env | Prim("-", e1, e2) -> eval e1 env - eval e2 env | Prim _ -> failwith "unknown primitive”

Page 36: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Variabililibere

  Inlogicaunavariabileinunaformulaèliberasenoncomparenellaportatadiunquan;ficatoreassociatoatalevariabile,altrimen;èlegata

  Esempio:∀x.(P(x)⋀Q(y)) [o (∀x.P(x)⋀Q(y))nellasintassidiLPP]

o  xèlegatao  yèlibera

36

Page 37: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Occorrenzelibere

o  Lanozionedivariabileliberaolegatasiapplicaanchealcasodelcostru:olet

o  InfaDilcostru:oletsicomportacomeunquan;ficatoreperlavariabilecheintroduce

o  Uniden;ficatorexsidice“legato”seapparenelebodydell’espressioneletx=ehrsinebody,altrimen;sidicelibero

o  Esempio  let z = x in z + x(*zlegata,xlibera*)o  let z = 3 in let y = z + 1 in x + y

(*z,ylegate,xlibera*)

37

Page 38: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Interpretazionediespressioni

  L’interpreteintrodo:ociperme:edivalutareespressionicostruiteconlasintassiindicata

38

Program Inter- preter Output

Input eval e

env

Page 39: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Versolacompilazione

  Ilnostrointerpretediespressioniognivoltachedevedeterminareilvaloreassociatoaunavariabileeffe:uaunaoperazionedilookupnell’ambiente:questopotrebbeessereoneroso  Idea:oDmizzarel’esecuzioneintroducendounpiccolocompilatorechetraducetu:eleoccorrenzediiden;ficatoriin“indicidiaccesso”,inmodotalechel’operazionedilookupsiaeseguitasenzaeffe:uarericerchesull’ambiente,mainmododire:o(complessitàO(1))

39

Page 40: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Ricordiamoloschemamistocompilazione/interpretazione

40

Program Compiler Machine code Machine Output

Input Javacode javac

args[]

bytecode Java

Page 41: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Levariabili:danomiaindici

41

Let("z", CstI 17, Prim("+", Var "z", Var "z"))

Let(CstI 17, Prim("+", Var 0, Var 0))

COMPILAZIONE

Ilvalore0indicailbinding(let)piùvicino

Page 42: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Indicipervariabili

42

Let("z", CstI 17, Let("y", CstI 25, Prim("+", Var "z", Var "y")))

Idea:indicediunavariabile=numerodeiletchesia:raversanoperraggiungerla

Let(CstI 17, Let(CstI 25, Prim("+", Var 1, Var 0)))

COMPILAZIONE

Page 43: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Indicipervariabili

  L’ideadiu;lizzareindicialpostodivariabiliinmodotaledaavereimplementazioniefficien;nascenellateoriadellambda-calcolocongliindicidiDeBruijn

h:p://en.wikipedia.org/wiki/De_Bruijn_index

43

Page 44: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Illinguaggiointermedio

44

TARGETEXPRESSIONtype texpr = (* target expression *) | TCstI of int | TVar of int (* indice a run time *) | TLet of texpr * texpr (* erhs e ebody *) | TPrim of string * texpr * texpr

Page 45: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Compilazioneincodiceintermedio

expr tcomp texpr teval Output

int list

ambienterun+me

Page 46: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Compilazioneincodiceintermedio

46

(* Compila Expr in Texpr. Usa lista di identificatori *)

let rec tcomp e (cenv : string list) : texpr = match e with | CstI i -> TCstI i | Var x -> TVar (getindex cenv x) | Let(x, erhs, ebody) -> let cenv1 = x :: cenv in TLet(tcomp erhs cenv, tcomp ebody cenv1) | Prim(ope, e1, e2) ->

TPrim(ope, tcomp e1 cenv, tcomp e2 cenv)

let rec getindex cenv x = match cenv with | [] -> failwith("Variable not found") | y::yr -> if x=y then 0 else 1 + getindex yr x

Page 47: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Interpretaz.incodiceintermedio

47

(* Ambiente a run time e' una lista di interi *)

open list

let rec teval (e : texpr) (renv : int list) : int = match e with | TCstI i -> i | TVar n -> nth renv n | TLet(erhs, ebody) -> let xval = teval erhs renv in let renv1 = xval :: renv in teval ebody renv1 | TPrim("+", e1, e2) -> teval e1 renv + teval e2 renv | TPrim("*", e1, e2) -> teval e1 renv * teval e2 renv | TPrim("-", e1, e2) -> teval e1 renv - teval e2 renv | TPrim _ -> failwith("unknown primitive")

Page 48: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Codiceintermedio

Rappresentareilprogrammasorgenteinuncodiceintermedioèunatecnicacheperme:edidominarelacomplessitàdellaimplementazionediunlinguaggiodiprogrammazione  Larappresentazioneincodiceintermedioperme:edieffe:uarenumeroseoDmizzazionisulcodice(nelnostrocaso,l’eliminazionedeinomiarun-;me)Esempio  Javabytecode:codiceintermediodellaJVMo  Microso}CommonIntermediateLanguage:codiceintermedio.NET

48

Page 49: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

Cosaabbiamoimparato

  Unatecnicageneraleusataneiback-enddeicompilatorinellafasedigenerazionedelcodicepero:enereuncodicemaggiormenteefficiente  UsarecodiceintermedioeoDmizzareilcodiceogge:osulcodiceintermedio  Ar;colodivulga;vo(matecnico)disponibileon-line:FredChow,IntermediateRepresenta;on,Communica;onsofACM56(12)2013

49

Page 50: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

VisioneJava

50

Page 51: AA 2016-2017 18. Interpre+, compilatori e semanca operazionalepages.di.unipi.it/gadducci/oldCorsi/PR2-16/PR2-16-018.pdf · 2016. 11. 16. · o Semaca assioma2ca: descrive il significato

VisioneCommonInterm.Language

51