ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ

TRẦN MẠNH ĐÔNG NGHIÊN CỨU KỸ THUẬT PHÂN TÍCH CHƯƠNG TRÌNH
TĨNH TRONG VIỆC NÂNG CAO CHẤT LƯỢNG PHẦN MỀM
Ngành: Công nghệ thông tin
Chuyên ngành: Công nghệ phần mềm
Mã số: 60 48 10

TÓM TẮT LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN
trình (formal methods) cố gắng chứng minh một cách tự động rằng
chương trình sẽ thực thi đúng đắn trên mọi môi trường được đặc tả.
Mảng nghiên cứu này bao gồm các phương pháp suy dẫn (deductive
methods), kiểm chứng mô hình (model checking), định kiểu chương
trình (program typing) và phân tích chương tr ình tĩnh (static program
analysis). Ba nhóm đầu tập trung vào việc kiểm chứng phần mềm tại
2
mức mô hình, trong khi nhóm cuối cùng xử lý phần mềm tại mức mã
nguồn. Phân tích chương trình tĩnh thu hút sự quan tâm nhất do nền
tảng lý thuyết hình thức của nó cũng như mục đích của nó đối với các
ứng dụng của nó trong thực tế. Kỹ thuật này phát hiện tính chất/hành vi
của một chương trình mà không yêu cầu chạy chương trình đó. Ngoài
ra, một số lỗi chương trình như việc khởi tạo/sử dụng biến chương
trình, biến con trỏ NULL, có thể được phát hiện bởi kỹ thuật này.
Chương 1: Giới thiệu
1.1 Giới thiệu về phân tích chương trình
Phân tích chương trình tĩnh là kỹ thuật xác định tính chất/hành
vi của một chương trình mà không cần phải chạy chương trình đó.
Phân tích tĩnh được xây dựng dựa trên lý thuyết diễn giải trừu tượng
(abstract interpretation) để chứng minh tính chính xác của các phân
tích liên quan đến ngữ nghĩa của một ngôn ngữ lập trình.
1.2 Điểm mạnh và điểm yếu
Phân tích chương trình tĩnh có những ưu điểm sau:
• Chỉ ra lỗi tại vị trí chính xác trong chương trình
• Dễ dàng thực hiện bởi những chuyên gia kiểm định chất lượng
phần mềm hiểu rõ về mã nguồn
• Khoảng thời gian ngắn từ lúc phát hiện tới khi sửa lỗi
• Có thể tự động hóa nhanh (thông qua các bộ công cụ hỗ trợ ví
dụ: SOOT, Astree, TVLA, )
• Lỗi được phát hiện sớm trong qui trình phát triển phần mềm nên

có hướng, trong đó các nút tương ứng là các điểm trong chương trình
và các cạnh thể hiện cho luồng điểu khiển. Một CFG luôn luôn có một
điểm vào, ký hiệu là entry, và một điểm ra, ký hiệu exit. Ngoài ra, nếu
v là một nút trong CFG thì những ký hiệu pred(v) là tập các nút kế
trước (predecessor) và succ(v) là tập các nút kế sau (successor).
CFG cho các lệnh
• Các lệnh cơ bản
id = E printf(E) return E int id
Hình 1: CFG cho các lệnh cơ bản.
• Các lệnh tuần tự
S1
S2
S1 S2
Hình 2: CFG cho các lệnh tuần tự.
• Các lệnh cấu trúc điều khiển
5
E E
S
S1 S2
if(E) S; if(E) S1; else S2;
Hình 3: CFG cho các lệnh if, if-else.
E
S
E1
E2
S
E3
for(E1; E2; E3;) S;while(E) S;
Hình 4: CFG cho các lệnh while, for.
Ví dụ CFG của một chương trình

các điều kiện sau:
• Phản xạ: ∀x ∈ S : x ⊑ s
• Phản xứng: ∀x, y ∈ S : x ⊑ y ∧ y ⊑ x ⇒ x = y
• Bắc cầu: ∀x, y, z ∈ S : x ⊑ y ∧ y ⊑ z ⇒ x ⊑ z
Biểu diễn Dàn thông qua biểu đồ Hasse
Ví dụ, biểu diễn Dàn (2
{x,y,x}
, ⊆) (Hình 6 (a)) hoặc Dàn đảo
ngược (Dàn được sắp bởi thứ tự ngược của các tập con và quan hệ hai
ngôi ⊑ được định nghĩa là ⊇) (2
{x,y,x}
, ⊇) (Hình 6 (b)) bằng biểu đồ
Hasse:
{x}
{x,y,z}
{x,y} {x,z} {y,z}
{}
{y} {z}
{}
{y} {z}
{x,y,z}
{x,z} {y,z}
{x,y}
{x}
(a) (b)
Hình 6: Biểu đồ Hasse biểu diễn Dàn.
Cận trên, cận dưới
Cho X ⊆ S . Ta nói rằng y ∈ S là một cận trên của X, ký hiệu X ⊑ y,
nếu ∀x ∈ X : x ⊑ y. Tương tự, y ∈ S là một cận dưới của X, ký hiệu
y ⊑ X, nếu ∀x ∈ X : y ⊑ x. Một cận trên nhỏ nhất, ký hiệu ⊔X, được

mọi hàm đơn điệu f có duy nhất điểm cố định nhỏ nhất được định
nghĩa:
f ix( f ) =
⊔
i≥0
f
i
(⊥)
Thuộc tính đóng
Nếu L
1
, L
2
, , L
n
là những Dàn với độ cao hữu hạn, từ đó một phép
toán tích (product):
L
1
× L
2
× × L
n
= {(x
1
, x
2
, , x
n
)|x

n
]|x
i
∈ L}
Phương trình và bất phương trình
Cho L là một Dàn với độ cao hữu hạn. Một hệ phương trình được
biểu diễn:
x
1
= F
1
(x
1
, , x
n
)
x
2
= F
2
(x
1
, , x
n
)

x
n
= F
n

n
), , F
n
(x
1
, x
2
, , x
n
))
1.4.3 Thuật toán điểm cố định
Thuật toán lặp chaotic
x
1
= ⊥; x
n
= ⊥;
do {
t
1
= x
1
; t
n
= x
n
;
x
1
= F

= ⊥;
W = {1, , n};
while (W  ∅) {
i = W.removeNext();
y = Fi(x
1
, , x
n
);
if (y  x
i
) {
for (v
j
∈ dep(v
i
))W.add( j);
x
i
= y;
}
}
Chương 2: Phân tích chương trình tĩnh
2.1: Phân tích luồng dữ liệu nội thủ tục Phân tích luồng dữ liệu hay
còn gọi là khung đơn điệu (monotone framework), là kỹ thuật phân tích
chương trình tĩnh nhằm thu thập các hành vi của chương trình và phát
11
hiện lỗi thông qua đồ thị luồng dữ liệu (CFG) và Dàn L có độ cao hữu
hạn.
Các bước để phân tích luồng dữ liệu bao gồm:

Trong một chương trình việc xác định tính sống của biến tại mỗi
điểm của chương trình là rất cần thiết, việc này giúp chương trình
12
xác định và loại bỏ được các biến chết giúp tối ưu hóa bộ nhớ/
tối ưu hoá chương trình dịch và làm tăng tốc độ tính toán của
chương trình. Một biến được gọi là biến sống tại một điểm của
chương trình ( liveness) nếu giá trị hiện tại của nó được đọc trong
nút hiện tại hoặc được đọc trong một số nút kế tiếp (không được
ghi ở nút hiện tại). Thuộc tính này có thể được xấp xỉ bởi phân
tích tĩnh dựa trên CFG với một dàn là một tập các biến trong
chương trình. Gọi các biến ràng buộc cho mỗi nút v trên CFG là
v, khi đó các ràng buộc cho tính sống của biến tại các nút với
các cấu trúc lệnh trong chương trình được xác định như sau:
– Đối với nút exit, có ràng buộc là:
exit = ∅
– Đối với những lệnh điều kiện, lệnh return và lệnh printf(E),
ràng buộc là:
v =
∪
w∈succ(v)
w ∪ vars(E)
– Đối với những phép gán id = E, ràng buộc là:
v =
∪
w∈succ(v)
w \ {id} ∪ vars(E)
– Đối với một khai báo biến intid
1
, , id
n

return f = exit ∪ {f}
f = f*n = (n = n-1 \ {f}) ∪ {n,f}
n = n-1 = (n > 0 \ {n}) ∪ {n}
exit = ∅
Hệ phương trình trên là để giải thông qua Dàn: L = (2
{f, uu_f, n}
, ⊆
). Hơn nữa, nó dễ dàng thấy rằng tất cả vế phải ràng buộc của
phương trình định nghĩa những hàm đơn điệu. Theo kết quả,
lý thuyết của điểm cố định nhỏ nhất có thể được áp dụng [? ].
Nghiệm nhỏ nhất cho hệ phương trình (Được giải trong Phụ lục
A) là duy nhất là:
entry = ∅
int f = ∅
int uu_f = ∅
f = 1 = {n}
uu_f = 0 = {n,f}
n > 0 = {n,f}
return f = {f}
f = f*n = {n,f}
n = n-1 = {n,f}
exit = ∅
Phân tích biểu thức bận rộn
Việc tính toán các biểu thức trong chương trình làm tăng bộ nhớ
và làm chậm thời gian chạy kết quả của chương trình. Do vậy,
trong chương trình nếu hạn chế tính toán lại một biểu thức trong
tương lai sẽ giúp chương trình chạy nhanh hơn và giúp bộ nhớ
tối ưu hơn.
14
Một biểu thức E là bận rộn (busy) tại điểm p của chương trình

được bắt đầu từ nút entry của CFG và di chuyển chuyển tiếp
trong CFG. Một số phân tích điển hình: Phân tích biểu thức có
sẵn(Available Expression), phân tích định nghĩa tới được(Reaching
Denitions)
15
Phân tích biểu thức có sẵn
Một biểu thức không bình thường (nontrivial) trong một chương
trình là có sẵn (available) tại một điểm trong chương trình nếu
giá trị của nó đã được tính toán sẵn trước đó trong khi thực thi.
Việc xác định các biểu thức đã có sẵn trước khi thực thi sẽ giúp
cho việc tính toán nhanh và đơn giản hơn. Do vậy, trong phân
tích này chúng ta sử dụng các thông tin về hành vi trong quá
khứ. Và, Dàn cho phân tích này là tập hợp các biểu thức xảy ra
cho tất cả các điểm chương trình và được sắp bởi các tập con đảo
ngược (reverse). Đối với mỗi nút v trên CFG tương ứng với một
biến ràng buộc v trên Dàn L chứa các tập con của các biểu thức
mà nó được đảm bảo luôn luôn có sẵn tại điểm chương trình kế
sau nút đó. Ví dụ, biểu thức a+ b là có sẵn ở điều kiện trong vòng
lặp, nhưng nó không phải là có sẵn tại các phép gán trong vòng
lặp. Phân tích đưa ra sẽ bảo toàn kể từ khi thiết lập tính toán có
thể là quá nhỏ. Từ đó, có các ràng buộc luồng dữ liệu cho các
cấu trúc lệnh trong phân tích như sau:
– Với mỗi nút entry ta có ràng buộc:
entry = {}
– Nếu v chứa một điều kiện E hoặc lệnh output E, khi đó
ràng buộc là:
v =
∩
w∈pred(v)
w ∪ exps(E)

là có sẵn trong v nếu nó có sẵn từ tất cả các cạnh hoặc được tính
toán trong nút v, trừ khi giá trị của nó đã được hủy bởi lệnh gán.
Một lần nữa, phía vế phải của những ràng buộc là những hàm
đơn điệu.
Phân tích định nghĩa tới được
Trong lĩnh vực kiểm thử và đảm bảo chất lượng phần mềm, việc
xác định đồ thị def-use là việc làm quan trọng trong việc hạn
chế các mã chết (dead code) và những mã chuyển động (code
motion). Vì vậy, mục đích của kỹ phân tích định nghĩa tới được
là xác định mối quan hệ của các biến tại có các điểm của chương
trình với nhau.
Các định nghĩa tới được (reaching denitions) cho những điểm
của chương trình là những phép gán mà có thể được xác định là
giá trị hiện tại của các biến. Đối với phân tích này, chúng ta cần
một dàn là tập tất cả các phép gán xảy ra trong chương trình. Với
mọi nút v trên CFG biến v là tập các phép gán mà có thể xác
định giá trị của biến tại điểm chương trình. Ta có các ràng buộc
cho các lệnh chương trình trong phân tích như sau:
– Với những phép gán có ràng buộc:
v = (
∪
w∈pred(v)
w) ↓ id ∪ {v}
17
– Với tất cả các nút khác, ràng buộc là:
v =
∪
w∈pred(v)
w
Trong đó, hàm

Bây giờ, xem xét các CFG cho lời gọi và hàm được gọi, nếu các
tham số chính thức của hàm gọi là a
1
, , a
n
và của hàm bị gọi là
b
1
, , b
m
, thì lời gọi hàm được chuyển thành đồ thị như sau:
18
call-i=ret-f;
bj=save-i-bj;
xj=save-i-xj;
x=call-I;
int x1,x2,…xk;
save-i-bj=bj;
save-i-xj=xj;
temp-i-aj=Ej;
aj=temp-i-aj;
ret-f=E;
Hình 7: Ví dụ CFG tổng quát cho chương trình có chứa lời gọi hàm.
2.2.2 Tính cảm ngữ cảnh (context sensitivity)
Một vấn đề được quan tâm trong phân tích liên thủ tục là phân
tích ngữ cảnh phụ thuộc của sự gọi hàm. Đối với một hàm chỉ
được gọi một lần ta gọi là đơn biến (monovariant), và đối với
hàm được sử dụng nhiều lần gọi là đa biến (polyvariant). Xét ví
dụ cho phân tích đa biến cho chương trình sau:
int f() {

cảnh nhạy cảm này, ta sử dụng phân tích đa biến, tạo ra các sao
chép CFG hàm được gọi cho mỗi lời gọi hàm. Việc xác định số
bản sao chép đơn giản nhất là mỗi lời gọi sẽ tạo ra một sao chép
như sau:
20
save-1-x=x
z=20
int x
call-1=ref-test
save-2-y=y
z=10
int y
call-2=ref-testref -test=z
save-2-y=ysave-1-x=x
y=call-2x=call-1
ret-g=yret-f=x
ref -test=z
Hình 9: CFG đa biến.
Tuy nhiên, đối với những hàm đệ quy thì số bản sao chép có thể vô hạn.
2.2.3 Ứng dụng phân tích luồng dữ liệu liên thủ tục
Một ứng dụng cho phân tích liên thủ tục được gọi là rung cây (tree
shaking), đây là ứng dụng để xác định và loại bỏ những hàm không bao
giờ được gọi hay hàm chết và từ đó có thể loại bỏ nó từ chương trình
mà vẫn đảm bảo tính an toàn. Điều này thực sự hữu ích nếu chương
trình thực hiện với thư viện hàm lớn.
Với CFG có thể được xây dựng như phần trên đã trình bày, ở đây
ta sử dụng Dàn là tập các tên hàm trong chương trình này. Với mỗi nút
v trên CFG, đưa vào một biến hạn chế v biểu thị tập các hàm có thể
được gọi đến trong tương lai. Tiếp theo, sử dụng ký hiệu entry(id) cho
các nút vào (entry) của hàm id. Khi đó, các ràng buộc:

1
) ∪ ∪ f uncs(E
n
)
Trong phân tích này, vế phải trong các ràng buộc là các hàm đơn
điệu. Khi đó, với cách xây dựng CFG cho cả chương trình như trên và
các ràng buộc cho ứng dụng như trên ta sẽ có hệ phương trình ràng
buộc và việc giải nghiệm cố định nhỏ nhất (Mục ) để tìm ra các hàm
tất cả các hàm không được sử dụng trong chương trình. Như vậy, ta có
thể loại bỏ các hàm này mà vẫn đảm bảo sự an toàn cho chương trình.
Chương 3: Thực nghiệm
Trong phần thực nghiệm này, luận văn tiến hành dựa trên công cụ
mã nguồn mở SOOT, hỗ trợ cho chương tr ình viết bởi ngôn ngữ Java,
và là một plugin tích hợp vào Eclipse.
3.1 Tổng quan về SOOT
SOOT là một framework tối ưu hóa cho Java do một nhóm nghiên
cứu tại đại học McGill (Canada), năm 2000. Đây là phần mềm nguồn
mở.
Các bước phân tích trong SOOT
• Bước 1: Cài đặt kiểu phân tích: BackwarkFlowAnalysis(), For-
warkFlowAnalysis()
22
• Bước 2: Cài đặt các trừu tượng: merge(), copy()
• Bước 3: Cài đặt hàm luồng: flowThrough()
• Bước 4: Cài đặt khởi tạo các giá trị: newInitialFlow() và entryIni-
tialFlow()
• Bước 5: Xây dựng phân tích: doAnalysis()
3.2 Phân tích chương trình ví dụ với Soot
Trong phần này, luận văn thực nghiệm với phân tích tính sống của
biến.