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

Post on 23-Jan-2021

0 views 0 download

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

18.Interpre+,compilatorieseman+caoperazionale

AA2016-2017

1

Linguaggidiprogrammazione

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

  Lanostrarispostao  lacomprensionediunlinguaggiodiprogrammazionesioDenedallaseman+cadellinguaggio

Seman;cacomeguidaallaproge:azione,all’implementazioneeall’usodiunlinguaggiodiprogrammazione

2

Elemen+diseman+caoperazionale

3

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

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

Sintassiastra:a

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

  PergliASTabbiamoquindisiaunanotazionelinearecheunarappresentazionegrafica

6

Dallasintassiconcretaall’AST

7

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

SINTASSICONCRETA

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

SINTASSIASTRATTA

ALBEROSINTATTICO

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

EdiquestocosasivedeinPR2?

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

  Comprensionedeiparadigmideilinguaggidiprogrammazioneo  useremounaseman;caoperazionale

9

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

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

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

Seman;caoperazionaleinPR2

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

13

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)

Regoleederivazioni

  Leregoledivalutazionepossonoesserecompostepero:enerelavalutazionediunaespressionepiùcomplessa  Questofornisceunaprovadiunaderivazioneoperazionaledicalcolo

15

Regolediderivazione

  Leregoledivalutazionecos;tuisconounproofsystem(sistemadidimostrazione)

  Tipicamenteleregolesonodefiniteperinduzionestru:uralesullasintassidellinguaggio

  Le“formule”checiinteressadimostraresonotransizionidel;poe=>v

  Componiamoleregoleinbaseallastru:urasintaDcadieo:enendounprooftree

16

premessa1 ... premessakconclusione

Regoleeinterprete

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

17

Interpreteespressionilogiche

18

Passo1:sintassiastra:a

19

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

Definizionedellasintassiastra;atramitei+pialgebricidiOCaml

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

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

Espressioniavaloriinteri

22

SintassiOCaml(astra:a)

23

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

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

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

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

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

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

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”

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

Acosaserve?

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

31

Aggiungiamoledichiarazioni

32

let z = 17 in z + z CORPO

DICHIARAZIONE

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

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

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”

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

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

Interpretazionediespressioni

  L’interpreteintrodo:ociperme:edivalutareespressionicostruiteconlasintassiindicata

38

Program Inter- preter Output

Input eval e

env

Versolacompilazione

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

39

Ricordiamoloschemamistocompilazione/interpretazione

40

Program Compiler Machine code Machine Output

Input Javacode javac

args[]

bytecode Java

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

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

Indicipervariabili

  L’ideadiu;lizzareindicialpostodivariabiliinmodotaledaavereimplementazioniefficien;nascenellateoriadellambda-calcolocongliindicidiDeBruijn

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

43

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

Compilazioneincodiceintermedio

expr tcomp texpr teval Output

int list

ambienterun+me

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

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")

Codiceintermedio

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

48

Cosaabbiamoimparato

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

49

VisioneJava

50

VisioneCommonInterm.Language

51