jdataflow
1.0.0
JDATAFLOW는 Java 소스 코드를위한 Z3 솔버 기반 데이터 유량 분석기입니다.
현재 JDATAFLOW는 논리적 오류 (항상 참/거짓 표현), 널 포인터 피해, 배열 지수 등을 감지 할 수있는 체커가 있습니다.
예를 들어:
void f ( boolean c ) {
int x = 5 ;
int y = c ? 3 : 2 ;
if ( x < y ) {} // <= always false
}
void g ( int x , int y ) {
if ( 2 * x + 3 * y == 12 ) {
if ( 5 * x - 2 * y == 11 ) {
if ( x == 3 ) {} // <= always true
if ( y == 2 ) {} // <= always true
}
}
}
void h ( Something x ) {
if ( x == null ) {
x . f (); // <= null dereference
}
}
void z () {
int [] arr = new int [] { 1 , 2 , 4 , 8 , 16 , 32 };
int x = arr [ 9 ]; // <= array index out of bounds
}더 많은 예를 보려면 테스트 디렉토리를 확인하십시오.
일반적으로 JDATAFLOW는 표현식을 정적으로 평가하고, 상징적 실행을 수행하고, 프로그램의 제어 흐름을 처리 할 수 있습니다. 또한 적절한 메모리 모델을 특징으로하므로 참조 별칭을 잘 처리합니다.
JDataFlow를 빌드하려면 JDK 8 또는 최신이 필요합니다. 또한 Z3를 다운로드하여 설치해야합니다.
gradlew build 실행하십시오참고 : Visual C ++ 2015 재배포 가능이 필요할 수 있습니다.
export LD_LIBRARY_PATH=/path/to/z3/bin./gradlew build 실행하십시오export DYLD_LIBRARY_PATH=/path/to/z3/bin 에 빈 디렉토리를 추가하십시오./gradlew build 실행하십시오IDE에서 여전히 환경 변수 또는 java.lang.path를 설정해야 할 수도 있습니다.
이제 빌드 디렉토리로 이동하여 결과적인 항아리를 실행할 수 있습니다.
java -jar jdataflow.jar --sources <args...> [--classpath <arg>] [--classpath-file <arg>]
JDATAFLOW로 개미, Maven 또는 Gradle 기반 프로젝트를 확인하려면 스캔 유틸리티를 사용해야합니다.
JDataFlow는 Spoon 라이브러리를 사용하여 포스트 주문 방식으로 AST를 구축하고 가로 지릅니다. AST를 가로 지르는 동안 소스 코드를 Z3 솔버가 이해할 수있는 양식으로 변환합니다. 그런 다음 점검은 솔버가 수행합니다.
우선, Z3와 함께 사용하려면 코드는 정적 단일 할당 형식으로 존재해야합니다. 우리는 논리 공식으로 프로그램의 순서를 유지하기 위해이를 수행합니다. 간단한 예는 다음과 같습니다.
원형:
x = 1;
y = 2;
x = x + y;
SSA 양식 :
x0 = 1;
y0 = 2;
x1 = x0 + y0;
IF 문을 통과 한 후 새로운 변수를 만듭니다.이 변수는 Z3에서 제공하는 특수 IF-then-ELSE 기능의 결과입니다. 이 기능은 본질적으로 조건에 따라 분기의 값을 결합합니다.
원형:
if (c) {
x = 1;
} else {
x = 2;
}
SSA 양식 :
if (c) {
x0 = 1;
} else {
x1 = 2;
}
x3 = ITE(c0, x0, x1);
기능 호출을 다루는 가장 분명한 접근법은이를 인화하는 것입니다. 불행히도, 우리는 성능 고려 사항으로 인해 작은 기능 (getters 또는 setters)에 대해서만 할 수 있습니다.
또 다른 방법은 계약, 순도, 반환 값 등에 대한 정보를 포함하는 함수 요약 (자동 또는 수동)을 구축하는 것입니다.
그러나 일반적으로 알려지지 않은 기능은 인수의 가치를 재설정합니다.
루프를 다루는 가장 분명한 접근법은 루프를 풀는 것입니다. 불행히도, 우리는 반복 횟수가 정적으로나 비교적 작을 때만 할 수 있습니다.
따라서 일반적으로 루프 불변량을 찾고 알 수없는 기능과 같은 다른 모든 것을 재설정해야합니다.
그러나 일부 특별한 경우는 다르게 치료할 수 있습니다.
JDATAFLOW는 유형-인덱스 메모리 모델 (Burstall의 메모리 모델)을 사용합니다. 이 메모리 모델에서 각 데이터 유형 또는 필드에는 자체 메모리 배열이 있습니다. 다음과 같은 것을 감지 할 수 있습니다.
void m () {
C a = new C ();
a . x = 10 ;
C b = a ;
b . x = 20 ;
if ( a . x == 20 ) {} // <= always true
}다음은 다양한 메모리 모델에 대한 자세한 설명이있는 유용한 링크입니다.
현재이 프로젝트는 개념의 증거 일 뿐이므로해야 할 일이 많이 있습니다.
