Pre19 esentation finale du travail de fin d'e19 etude

Nicolas Baerts Maxime Van De Reyd

Description

´Vers l’interpretation abstraite de Jimple´Semantique standard et domaine abstraitPromoteur : B. LE CHARLIER´ ´Etendre le cadre d’interpretation`abstraite a Java´ ´ `References : These d’Isabelle Pollet, Towards a generic frame work for the abstract interpretation of JavaThe Java Language Specification Second EditionM. Van de Reyd & N. BaertsååPlan de la presentation´ Introduction Jimple´ Elaboration de la semantique´ standardexemple du formalisme utilise´- appel virtuel- implementation´ des regles` de returninterpreteur´ Jimple´ Elaboration du domaine abstrait- booleans- tableaux Conclusion` `- vers une extension de la these a JavaM. Van de Reyd & N. Baerts 1åååååååIntroduction - Jimple - Semantique´ standard - Domaine abstrait - ConclusionIntroduction Cadre theor´ ique pour l’analyse par interpretation´ abstraite de Java[These` d’Isabelle Pollet]concepts les plus importants de Javasyntaxe abstraite : LASbut de notre memoire´ : etendre´ le cadre theor´ ique a` Java tout entier Remplacer LAS par un langage plus etendu,´ Jimple.´redefinir la syntaxe de Jimple´ ` `adapter la semantique concrete a Jimplevalider la s´modifier le domaine abstrait la semantique´ abstraiteM. Van de Reyd & N. Baerts 2ååååIntroduction - Jimple - Semantique´ standard - Domaine abstrait - ConclusionJimple Jimple’ bytecode Java sans pile explicite´ ´semantique operationnelle’ celle du bytecode Java(cfr. spec. de la JVM)´ ´ ` ´developpe dans ...

Informations

• Publié par: Epsu
• Nombre de lectures: 100
• Langue: Français

Extrait

Versl’interpr ´ etationabstraitedeJimple S ´ emantiquestandardetdomaineabstrait

Promoteur : B. L E C HARLIER

´ Etendrelecadred’interpre ´ tation abstraitea  Java

M. Van de Reyd & N. Baerts

R ´ ef ´ erences:The  sed’IsabellePollet, Towards a generic frame- work for the abstract interpretation of Java The Java Language Specication Second Edition

Plan de la p  ´  entation res

• Introduction • Jimple ´ • Elaborationdelase ´ mantiquestandard å exempleduformalismeutilis ´ e - appel virtuel -imple ´ mentationdesre  glesde return å interpre´ teur  Jimple ´ • Elaboration du domaine abstrait - booleans - tableaux • Conclusion -versuneextensiondelathe  sea  Java

M. Van de Reyd & N. Baerts

1

Introduction - Jimple - Se´  mantique standard - Domaine abstrait - Conclusion

Introduction

• Cadreth ´ eoriquepourl’analyseparinterpr ´ etationabstraitedeJava [The  sed’IsabellePollet]

å concepts les plus importants de Java å syntaxe abstraite : LAS

but denotrem ´ emoire:e ´ tendrelecadreth ´ eoriquea  Javatoutentier

• RemplacerLASparunlangageplus ´ etendu,Jimple. å red ´ enirlasyntaxedeJimple er a sem å adaptl ´ antiqueconcre  tea  Jimple å validerlas ´ emantique å modier le domaine abstrait å modierlase ´ mantiqueabstraite

M. Van de Reyd & N. Baerts

2

Introduction -Jimple - Se´  mantique standard - Domaine abstrait - Conclusion

Jimple

• Jimple ' bytecode Java sans pile explicite ´ å se ´ mantiqueoperationnelle ' celle du bytecode Java (cfr. spec. de la JVM) å d ´ eveloppe ´ danslecadreduprojetSoota  l’universite ´ McGill å ´ elabor ´ edanslebutd’analyseretd’optimiserdubytecode ´ å communauted’utilisateursetdede ´ veloppeursactifs

• Outils : Java To Jimple Bytecode To Jimple ) cfr. Soot

M. Van de Reyd & N. Baerts

3

Introduction -Jimple -S ´ emantiquestandard-Domaineabstrait-Conclusion

Jimple vs LAS

• En plus ( = restrictions de LAS) :

X Ensemblese ´ toff ´ es X Modicateursd’accessibilit ´ e X Variables/M ´ ethodesstatiques X Classes internes X Interfaces

X Tableaux X Packages X Exceptions - Concurrence

• Diff ´ erences: -Introductiondevariables“sp ´ eciales”,les atIdentiers - Jimple n’a pas de typage des expressions (pas de typage fort)

M. Van de Reyd & N. Baerts

4

Introduction - Jimple - Se´ mantique  standard - Domaine abstrait - Conclusion

La se´  mantique standard

• Lad ´ enitiond’unese ´ mantiquen ´ ecessiteunformalismeadapte ´ å pasd’ambigu¨ ´ et å permet de justier la correction de l’analyse å permetuneimpl ´ ementationpartraduction“directe”delad ´ enition

• Etapedeformalisationdelase ´ mantique å nede ´ coulepasdirectementdesde ´ nitionsofcielles å adapterunese ´ mantique(celledeJava)a  unautrelangage(Jimple) å processuslent,complique ´ etde ´ licat

M. Van de Reyd & N. Baerts

5

-versiondelathe  se-

M. Van de Reyd & N. Baerts

Introduction - Jimple - Se´ mantique  standard - Domaine abstrait - Conclusion

Un exemple : l’appel virtuel

De´ pend du type re´  el (la classe) de l’instance surlaquellel’appelesteffectu ´ e.

å Versionpre ´ sentedanslathe  se: τ ˜ Nmethod D ( m , int ) = ( void C m int )

å Versiond ´ esir ´ ee: ˜ τ Nmethod A D ( m , int ) = ( void B m int )

6

Introduction - Jimple -S ´ emantiquestandard - Domaine abstrait - Conclusion

˜ τ Nmethod Obtenir un MethTypeClass (signature de la me´  thode ainsi que la classe dans laquelleellesetrouver ´ eellement)delam ´ ethodeidentie ´ eparunesignature donne ´ epouruneclassedonn ´ eeentenantcomptedel’he ´ ritageetduconcept d’ overriding :

τ ˜ Nmethod : Nclass → Nclass 9 ( Nmethod × declTypeList ) 9 MethTypeClass dom ( τ ˜ Nmethod ) = dom ( τ Nmethod ) , dom ( τ ˜ Nmethod nclass 1 ) = C one ( nclass 1 ) , dom ( τ ˜ Nmethod nclass 1 nclass 2 ) = dom ( τ Nmethod nclass 1 ) , ∀ nclass 2 ∈ dom ( τ ˜ Nmethod nclass 2 ) , if s ∈ dom ( τ Nmethod nclass 2 ) ∧ Overrides ( s, nclass 2 , nclass 1 ) then τ ˜ Nmethod nclass 1 nclass 2 s = τ Nmethod nclass 2 s else if nclass 2 ∈ dom ( π ) then τ ˜ Nmethod nclass 1 nclass 2 s = τ ˜ Nmethod nclass 1 π ( nclass 2 ) s

M. Van de Reyd & N. Baerts

7

Introduction - Jimple -S ´ emantiquestandard - Domaine abstrait - Conclusion

Appelvirtueld’uneproc ´ edure:lare  gle

h lab , S, d i v − i − rt − ua − li − nv − o − k − e − nv − ar − . − < − nc − la − ss −− : t − yp − e − R − es − ul − t − nm − e − th − o − d − ( [ − de − cl − Ty − p − eL − is − t ] − ) > − ( [ − n − pa − r − am − L − is − t ] ) → ; h lab 0 , S 0 , d 0 i p 5 ( d ) = false  V al ( nvar ) d 6 = null  v @ this = V al ( nvar ) d v ∗ = V alList ( nparamList ) d T ype ( v @ this ) d = nclass 2 ∈ Nclass methTypeClass = τ ˜ Nmethod nclass 2 nclass ( nmethod , declTypeList )  d 0 = S tart J methTypeClass K ( v s , v ∗ ) d @ thi  l S a 0 b 0 = = S in + it ( ( n m e e x t t h ( l T a y b p ) e , C p l 1 a ( s d s ) ) )

M. Van de Reyd & N. Baerts

 

8

Return simple

Introduction - Jimple -S ´ emantiquestandard - Domaine abstrait - Conclusion

Correspondanceavecuneimpl ´ ementation

h lab, S, d i re − tu − rn h lab’, S’, d’ i − → public void makeOneStep( JReturnStmt stmt) { S 0 + ( lab’ , e 0 ) Object el = ( Object ) s.pop() ;   d S = = ( e, s, ste , ic , em )  StackElementTwo setw = ( StackElementTwo ) el ; if (el instanceof StackElementTwo ) {  d e 0 m = = ( f e 0 a , ls s, e ste , ic , em )   l = setw.getLabel() ; d.setEnvironment(setw.getEnvironment()) ; } Return avec assignation else { StackElementThree setr = ( StackElementThree ) el ; h l b, S, d i return immedi − ate → h lab’, S’, d” i l = setr.getLabel() ; a −−−−−−−− Value immediate = stmt.getOp() ; Value val = d.val(immediate) ; 0 d.setEnvironment(setr.getEnvironment()) ;  d S = = ( S e 0 + ( t l e a , b i ’ c , , e e , m le ) ftExpr )  d = d.assign(setr.getLeftExpr(), val) ; , s, s } em = false }   d 0 = ( e 0 , s, g s n t ( e l , e i f c t , E e x m pr ) , v ) d 0  d v 00 = = V A al s ( s i i mmediate ) d 

M. Van de Reyd & N. Baerts

9

Introduction - Jimple - Se´ mantique  standard - Domaine abstrait - Conclusion

Notreinterpre ´ teurJimple

but :validernotrede ´ nitiondelas ´ emantiquedeJimple

• Impl ´ ementation=traductionaussidirectequepossibledelad ´ ition e n (premie  reversion)delasemantiquedeJimple ´ å interpre´ teur  non complet

• Phase de validation : å comparaisonentrelesre ´ sultatsd’exe ´ cutiondeprogrammesJava et de leur traduction en Jimple å difcult ´ eimportante:concevoirdesjeuxdetests“sufsants” - non complet ⇒ e ´ laborationdestestsparnous-me ˆ me -destestssurdesprogrammesre ´ elsauraient ´ et ´ eint ´ eressants

M. Van de Reyd & N. Baerts

10