자바언어에정확한타입을추가한 ThisJava 소개 나현익, 류석영 프로그래밍언어연구실 KAIST 2014 년 1 월 14 일 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 1/29
APLAS 2013 나현익, 류석영 자바 언어에 정확한 타입을 추가한 ThisJava 소개 2/29
실제로부딪힌문제 자바스크립트프로그램분석을위한요약도메인 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 3/29
실제로부딪힌문제 자바스크립트프로그램분석을위한요약도메인 SAFE: Scalable Analysis Framework for ECMAScript 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 4/29
실제로부딪힌문제 자바스크립트프로그램분석을위한요약도메인 ˆv Value = PValue ( Loc) pv ˆ PValue = Ûndef Null Bool Number Ŝtring 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 5/29
실제로부딪힌문제 자바스크립트프로그램분석을위한요약도메인 ˆv Value = PValue ( Loc) pv ˆ PValue = Ûndef Null Bool Number Ŝtring 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 6/29
실제로부딪힌문제 자바스크립트프로그램분석을위한요약도메인 abstract class AbsBase { def istop(): Boolean def isbottom(): Boolean def isconcrete(): Boolean def toabsstring(): AbsString 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 7/29
실제로부딪힌문제 자바스크립트프로그램분석을위한요약도메인 sealed abstract class AbsNull extends AbsBase { /* partial order */ def <= (that: AbsNull) = {... /* join */ def + (that: AbsNull) = {... /* meet */ def <> (that: AbsNull) = {...... 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 8/29
실제로부딪힌문제 자바스크립트프로그램분석을위한요약도메인 sealed abstract class AbsString extends AbsBase { /* partial order */ def <= (that: AbsString) = {... /* join */ def + (that: AbsString) = {... /* meet */ def <> (that: AbsString) = {...... 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 9/29
실제로부딪힌문제 자바스크립트프로그램분석을위한요약도메인 abstract class AbsBase { /* partial order */ def <= (that: ThisType): Boolean /* join */ def + (that: ThisType): ThisType /* meet */ def <> (that: ThisType): ThisType... 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 10/29
실제로부딪힌문제 자바스크립트프로그램분석을위한요약도메인 AbsBase 에서요구하는함수의인자와결과타입실행시간에정확한클래스타입매칭 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 11/29
실제로부딪힌문제 자바스크립트프로그램분석을위한요약도메인 AbsBase 에서요구하는함수의인자와결과타입실행시간에정확한클래스타입매칭 Bruno Oliveira s solution abstract class AbsBase { type ThisType <: AbsBase def + (that: ThisType): ThisType... case class AbsString extends AbsBase { type ThisType = AbsString override def + (that : ThisType): ThisType =... new AbsString()... 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 12/29
실제로부딪힌문제 자바스크립트프로그램분석을위한요약도메인 AbsBase 에서요구하는함수의인자와결과타입실행시간에정확한클래스타입매칭한요약도메인의여러구현 abstract class AbsDomain {... abstract class AbsBase[A] extends AbsDomain {... class AbsString extends AbsBase[String] {... class AbsStringSet extends AbsString {... class AbsStringAutomata extends AbsString {... 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 13/29
실제로부딪힌문제 자바스크립트프로그램분석을위한요약도메인 AbsBase 에서요구하는함수의인자와결과타입실행시간에정확한클래스타입매칭한요약도메인의여러구현 abstract class AbsDomain {... abstract class AbsBase[A] extends AbsDomain {... class AbsString extends AbsBase[String] {... class AbsStringSet extends AbsString {... class AbsStringAutomata extends AbsString {... 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 13/29
실제로부딪힌문제 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 14/29
이론적배경 This-typed 메소드 : 메소드의인자타입이나결과타입에메소드주인의타입을사용하는경우 abstract class AbsBase { /* partial order */ def <= (that: ThisType): Boolean /* join */ def + (that: ThisType): ThisType /* meet */ def <> (that: ThisType): ThisType... 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 15/29
이론적배경 This-typed 메소드 : 메소드의인자타입이나결과타입에메소드주인의타입을사용하는경우전통적인 This 타입클래스를 선언한 타입부정확한컴파일시간타입우리가제안하는 This 타입객체의 실행시간 타입정확한실행시간타입컴파일시에존재하지는않지만부를수는있는타입 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 16/29
이론적배경 This-typed 메소드 : 메소드의인자타입이나결과타입에메소드주인의타입을사용하는경우전통적인 This 타입클래스를 선언한 타입부정확한컴파일시간타입우리가제안하는 This 타입객체의 실행시간 타입정확한실행시간타입컴파일시에존재하지는않지만부를수는있는타입 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 16/29
이론적해결방안 새로운타입성질클래스 C 의정확한클래스타입 #C 를추가 This 타입변수이름붙인타입변수 </X/> 를사용하여서로같은정확한타입을더많이명시가능정확한타입유추를사용하여프로그래머의타입명시부담감소새로운언어성질가상생성자를사용하여 This 타입의값을만들어내는메소드생성 classesmatch 를추가하여실행시간에정확한타입검사가능 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 17/29
실제적해결방안 ThisJava, JastAddJ 를기반한공개소프트웨어구현 : http://plrg.kaist.ac.kr/research/software 기존자바코드와문제없이혼용가능자바바이트코드로컴파일 실용적기존자바언어의특이한성질과부드럽게작용 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 18/29
자바바이트코드로컴파일 정확한타입자바의 type erasure 와비슷한부정확한타입만들기적용클래스 C 의정의안에나오는 This 타입은 C 로변환클래스 D 와이름붙인타입변수 X 에대해서 #D 와 D</X/> 는 D 로변환 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 19/29
자바바이트코드로컴파일 정확한타입 가상생성자 class C { int fi; Point fp; This(int i, Point p) { fi = i; fp = p; This copy() { return new This(fi, fp); 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 20/29
자바바이트코드로컴파일 정확한타입 가상생성자 class C { int fi; Point fp; C(int i, Point p) { fi = i; fp = p; C vcstub0(int i, Point p) { Object[] pack = new Object[] {Integer.valueOf(i), p; return vcstub1(pack); C vcstub0(object[] pack) { int i = ((Integer)pack[0]).intValue(); Point p = (Point)pack[1]; return new C(i, p); C copy() { return vcstub0(fi, fp); 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 21/29
자바바이트코드로컴파일 정확한타입 가상생성자 정확한타입을사용한타입테스트와변환... (o instanceof #Point)...... (#Point) o... Object o;... if (o instanceof This) { This t = (This) o;... Object o;... classesmatch (o, this) {... 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 22/29
자바바이트코드로컴파일 정확한타입 가상생성자 정확한타입을사용한타입테스트와변환... (o instanceof #Point)...... (#Point) o... Object o;... if (o instanceof This) { This t = (This) o;... Object o;... classesmatch (o, this) {... 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 22/29
자바바이트코드로컴파일 정확한타입 가상생성자 정확한타입을사용한타입테스트와변환... (o instanceof #Point)...... (#Point) o... Object o;... if (o instanceof This) { This t = (This) o;... Object o;... classesmatch (o, this) {... 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 22/29
기존자바언어성질과의관계 같은이름의여러메소드부정확한타입으로만들고이름변환을거친후호출된메소드검사 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 23/29
기존자바언어성질과의관계 같은이름의여러메소드 Covariant 배열타입 #C[], This[][], 와 C</X/>[] 같이 invariant 배열타입사용 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 24/29
기존자바언어성질과의관계 같은이름의여러메소드 Covariant 배열타입 타입변수 class C<X extends #Point> {... class I<Y extends This> {... void m(point</e/> p) { class L<Z extends Point</E/>> {...... 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 25/29
기존자바언어성질과의관계 같은이름의여러메소드 Covariant 배열타입 타입변수 class C { /* #Point instead of X */... class I { /* C.This instead of Y */... void m(point</e/> p) { class L { /* Point</E/> instead of Z */...... 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 26/29
기존자바언어성질과의관계 같은이름의여러메소드 Covariant 배열타입 타입변수타입검사 OpenJDK 1.6 소스에있는 7637 자바파일중수정이필요한한가지경우 public static <T> List<T> aslist(t... a) {... List<C> l = Arrays.asList(new C(...)); List<C> l = Arrays.asList(new C(...)); // List<#C> List<C> l = Arrays.<C>asList(new C(...)); 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 27/29
기존자바언어성질과의관계 같은이름의여러메소드 Covariant 배열타입 타입변수타입검사 OpenJDK 1.6 소스에있는 7637 자바파일중수정이필요한한가지경우 public static <T> List<T> aslist(t... a) {... List<C> l = Arrays.asList(new C(...)); List<C> l = Arrays.asList(new C(...)); // List<#C> List<C> l = Arrays.<C>asList(new C(...)); 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 27/29
기존자바언어성질과의관계 같은이름의여러메소드 Covariant 배열타입 타입변수타입검사 OpenJDK 1.6 소스에있는 7637 자바파일중수정이필요한한가지경우 public static <T> List<T> aslist(t... a) {... List<C> l = Arrays.asList(new C(...)); List<C> l = Arrays.asList(new C(...)); // List<#C> List<C> l = Arrays.<C>asList(new C(...)); 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 27/29
정리 This-typed 메소드는실제상황에서발생하는중요한문제 약간의타입과언어성질을추가해서자바와같은기존언어에 This-typed 메소드추가가능 구현내용공개 : http://plrg.kaist.ac.kr/research/software 하지만, 자바언어의제약때문에 SAFE 는 ThisJava 을사용하지않을예정 ThisScala? 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 28/29
뒷이야기 Jacques Garrigue 의 OCaml 로흉내내기 Scala 플러그인으로 ThisScala 구현? 나현익, 류석영 자바언어에정확한타입을추가한 ThisJava 소개 29/29