ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
BÙI THỊ THƯ
ỨNG DỤNG KỸ THUẬT DIỄN GIẢI TRỪU
TƯỢNG TRONG PHÂN TÍCH BỘ NHỚ HEAP
LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN
Hà Nội – 2014
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
BÙI THỊ THƯ
ỨNG DỤNG KỸ THUẬT DIỄN GIẢI TRỪU
TƯỢNG TRONG PHÂN TÍCH BỘ NHỚ HEAP
Ngành: Công nghệ thông tin
Chuyên ngành: Kỹ thuật phần mềm
Mã số: 60480103
LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN
NGƯỜI HƯỚNG DẪN KHOA HỌC: TS. Nguyễn Trường Thắng
Hà Nội – 2014
Bùi Thị Thư
3
MỤC LỤC
LỜI CAM ĐOAN .............................................................................................. 1
LỜI CẢM ƠN .................................................................................................... 2
MỤC LỤC ......................................................................................................... 3
DANH MỤC CÁC KÝ HIỆU VÀ CHỮ VIẾT TẮT.......................................... 5
DANH SÁCH HÌNH VẼ ................................................................................... 6
MỞ ĐẦU ........................................................................................................... 7
CHƯƠNG 1. GIỚI THIỆU CHUNG.................................................................. 9
1.1.
Vấn đề quản lý bộ nhớ ........................................................................ 9
1.2.
Phân tích chương trình tĩnh ................................................................. 9
1.3.
Các kỹ thuật phân tích chương trình tĩnh........................................... 10
CHƯƠNG 2. LÝ THUYẾT NỀN TẢNG ......................................................... 14
2.1.
Nền tảng phân tích ngữ nghĩa của chương trình ................................ 14
Ứng dụng kỹ thuật diễn giải trừu tượng trong phân tích heap............ 36
3.1.1. Heap cụ thể ............................................................................. 36
3.1.2. Trừu tượng hóa heap ............................................................... 37
3.2.
Thực nghiệm ..................................................................................... 39
3.2.1. Giới thiệu TVLA ..................................................................... 39
3.2.2. Đặc tả hệ thống trong TVLA ................................................... 40
3.2.3. Biểu diễn ngữ nghĩa và chương trình....................................... 41
3.2.4. Tinh chỉnh sự trừu tượng hóa .................................................. 43
3.2.5. Ví dụ minh họa........................................................................ 44
KẾT LUẬN...................................................................................................... 50
TÀI LIỆU THAM KHẢO ................................................................................ 51
PHỤ LỤC A..................................................................................................... 53
PHỤ LỤC B ..................................................................................................... 54
PHỤ LỤC C ..................................................................................................... 56
PHỤ LỤC D..................................................................................................... 59
PHỤ LỤC E ..................................................................................................... 60
5
DANH MỤC CÁC KÝ HIỆU VÀ CHỮ VIẾT TẮT
Ký hiệu
CFG
TVLA
Hình 2.2. Quan hệ thứ tự từng phần không phải giàn .............................. 15
Hình 2.3. Tính toán điểm cố định trên giàn ............................................. 16
Hình 2.4. Ngữ nghĩa cụ thể của chương trình .......................................... 22
Hình 2.5. Thuộc tính an toàn ................................................................... 23
Hình 2.6. Kỹ thuật kiểm thử .................................................................... 23
Hình 2.7. Trừu tượng hóa ngữ nghĩa cụ thể ............................................. 24
Hình 2.8. Trừu tượng hóa không đảm bảo tính đủ ................................... 25
Hình 2.9. Trừu tượng hóa không đủ chính xác ........................................ 26
Hình 2.10. Sự trừu tượng hóa bằng kết nối
........................................... 27
Hình 2.11. Cây phân cấp các ngữ nghĩa ................................................... 33
Hình 3.1. Biểu diễn heap cụ thể ............................................................... 37
Hình 3.2. Các toán tử logic ...................................................................... 38
Hình 3.3. Trừu tượng hóa heap ................................................................ 38
Hình 3.4. Kết quả heap trừu tượng đầu ra ................................................ 42
Hình 3.5. Kết quả truy cập trường f ......................................................... 44
Hình 3.6. Thông số phân tích của TVLA ................................................. 49
7
MỞ ĐẦU
Ngày nay với sự phát triển vượt bậc của công nghệ thông tin, thì phần mềm
có vai trò cốt lõi và ngày càng chiếm vị trí quan trọng không những trong công
nghệ thông tin mà còn trong đời sống kinh tế xã hội. Khi đó sự phụ thuộc của
kinh tế xã hội vào phần mềm ngày càng lớn. Chính vì vậy, vấn đề chất lượng
phần mềm (software quality) chắc chắn là mối quan tâm và thách thức đối với
xã hội hiện đại ngày càng phụ thuộc vào các dịch vụ do máy tính đem lại này.
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 đó.
Mục tiêu của luận văn này là tìm hiểu về kỹ thuật phân tích chương trình
tĩnh, cập nhật những xu hướng nghiên cứu trong và ngoài nước về lĩnh vực phân
tích chương trình tĩnh, và cải tiến những kỹ thuật này. Cụ thể, luận văn tập trung
vào nghiên cứu kỹ thuật liên quan tới xấp xỉ ngữ nghĩa được gọi là diễn giải trừu
tượng (abstract interpretation), và thể hiện kỹ thuật này thông qua phân tích
hình dạng bộ nhớ heapdựa trên 3 giá trị logic (shape analysis via three-valued
logic). Tiến hành thực nghiệm trên công cụ TVLA, một công cụ mã nguồn mở
phân tích chương trình viết bằng Java.
Luận văn có cấu trúc như sau:
Chương 1 giới thiệu tổng quan về phân tích chương trình tĩnh. Trong chương
này trình bày định nghĩa kỹ thuật phân tích chương trình tĩnh, ứng dụng, điểm
mạnh và điểm yếu của kỹ thuật này. Tiếp đó luận văn trình bày một vài kỹ thuật
phân tích chương trình tĩnh phổ biến hiện nay, bài toán và kỹ thuật mà luận văn
thực hiện tìm hiểu.
Chương 2 trình bày nền tảng bài toán phân tích chương trình, lý thuyết của
kỹ thuật diễn giải trừu tượng (abstract interpretation).
Chương 3 trình bày về kỹ thuật phân tích hình dạng bộ nhớ heap dựa trên 3
giá trị logic. Thực nghiệm với TVLA – một công cụ mã nguồn mở để phân tích
chương trình.
Cuối cùng là phần kết luận và tài liệu tham khảo.
9
CHƯƠNG 1. GIỚI THIỆU CHUNG
1.1.
Vấn đề quản lý bộ nhớ
Có rất nhiều câu hỏi thú vị liên quan tới chương trình hoặc các điểm (point)
riêng lẻ trong chương trình:
Chương trình có dừng hay không?
Độ lớn có thể của vùng nhớheap trong quá trình chạy như thế nào?
Đầu ra (output) có thể là gì?
10
Giá trị của sẽ được đọc trong tương lai?
Điểm và có cấu trúc tách rời nhau trong heap?
Con trỏ có thể null?
Phân tích chương trình tĩnh có một số ưu điểm sau:
Chỉ ra được chính xác vị trí lỗi trong chương trình.
Lỗi được phát hiện sớm trong quy trình phát triển phần mềm nên chi
phí sửa thấp.
Tự động hóa nhanh: thông qua các công cụ hỗ trợ như TVLA, Astree,
SOOT …
Ngoài ra phân tích này có một số nhược điểm sau:
Không phát hiện được lỗi chỉ xuất hiện khi chạy chương trình.
Mất thời gian nếu thực hiện bằng tay.
Việc tự động hóa chỉ hướng vào một số ngôn ngữ nhất định.
Đòi hỏi nhân lực phải có kiến thức về ngôn ngữ lập trình.
Theo lý thuyết Rice[13], tất cả các câu hỏi liên quan tới hành vi chương
trình là không giải được (undecidable). Việc xử lý vấn đề này luôn đi kèm một
hoàn toàn tự động mà có thể cần sự tương tác với người dùng để tinh chỉnh
(refinement) các ánh xạ trừu tượng thông qua các tham số đưa vào, bởi vì có
thể đầu tiên tạo ra
(là ngữ nghĩa trừu tượng từ chương trình ) không thỏa
mãn đặc tả , trước hết phải tinh chỉnh chứ không kết luận ngay là không
thỏa mãn do tính không hoàn chỉnh (incompleteness) của kỹ thuật diễn giải
trừu tượng. Thay vì kiểm chứng đặc tả trên , chúng ta kiểm chứng đối với
ngữ nghĩa trừu tượng của . Nếu thỏa mãn bởi , do tính đúng đắn của kỹ
thuật diễn giải trừu tượng, đương nhiên thỏa mãn . Tính ưu việt của kỹ thuật
này là độ phức tạp của nhỏ hơn rất nhiều tùy theo quá trình trừu tượng hóa
(ánh xạ trừu tượng hóa từ vào ) như thế nào.
Trong thực tế, kỹ thuật diễn giải trừu tượng có một thành phần là bộ sinh
(generator) ngữ nghĩa trừu tượng đọc mã nguồn chương trình và tạo ra các ràng
buộc hoặc hệ các phương trình cần được giải bởi máy tính thông qua một thành
phần khác là bộ giải (solver). Cấu trúc các thành phần của kỹ thuật này được mô
tả trong hình 1.1.
12
Hình 1.1.
Các thành phần chính của kỹ thuật diễn giải trừu tượng
Một phương pháp phổ biến là dùng hàm lặp khi giải. Việc tìm nghiệm thông
qua hàm lặp có hạn chế về mặt thời gian (phương pháp không hội tụ sau vô hạn
lần lặp). Các kỹ thuật liên quan tới việc tăng tốc hội tụ cũng được nghiên cứu.
Thứ ba, nhóm kỹ thuật liên quan tới mô hình được gọi là kỹ thuật kiểm
chứng mô hình (Model checking). Kiểm chứng mô hình là kỹ thuật kiểm tra xem
một mô hình của hệ thống có thỏa mãn một tính chất nào đó hay không. Cụ thể
nguồn, trong khi hai nhóm sau xử lý phần mềm tại mức trừu tượng cao hơn là
mô hình.Hiện nay ở Việt Nam việc sử dụng các phương pháp hình thứctrong
thực tế kiểm chứng phần mềm còn nhiều hạn chế. Trong các mảng của phương
pháp hình thức thì mảng phân tích chương trình tĩnh sử đụng diễn giải trừu
tượng có nhiều lợi thế khi sử dụng thực tế, với khả năng tự động sinh được mô
hình ngữ nghĩa trừu tượng từ mã nguồn để kiểm chứng và có thể áp dụng cho
các hệ thống vô hạn trạng thái. Tuy nhiên đây lại là mảng chưa nhận được nhiều
sự quan tâm nghiên cứu như hai mảng còn lại.
Với tình hình nghiên cứu cơ bản và xu thế công nghệ phần mềm trên thế giới
hiện nay tập trung vào các vấn đề lớn như quy mô và chất lượng của các sản
phẩm phần mềm, kỹ thuật diễn giải trừu tượng là một dải nghiên cứu và ứng
dụng quan trọng đối với ngành công nghệ phần mềm. Việc tiến hành nghiên cứu
trong lĩnh vực này là cần thiết trong việc nâng cao chất lượng nghiên cứu ứng
dụng vào thực tế kiểm soát chất lượng phần. Do đó, luận văn sẽ tập trung vào
nhóm các kỹ thuật liên quan tới xấp xỉ ngữ nghĩa là diễn giải trừu tượng.
14
CHƯƠNG 2. LÝ THUYẾT NỀN TẢNG
2.1.
Nền tảng phân tích ngữ nghĩa của chương trình
2.1.1. Lý thuyết giàn
Một thứ tự từng phần (Partial order) là một cấu trúc toán học[15]: = ( , ⊑
), trong đó là một tập hợp và ⊑ là một quan hệ 2 ngôi trên thỏa mãn các điều
kiện sau:
Phản xạ: ∀ ∈ ∶ ⊑
Bắc cầu: ∀ , , ∈ ∶
∈
∶
⊑
⇒⊔
⊑
Tương tự, cận dưới lớn nhất, kí hiệu là ⊓ , được định nghĩa như sau:
⊓
⊑
∧∀
∈
∶
⊑
⇒
⊑⊓
Giàn (Lattice) là một quan hệ thứ tự từng phần mà trong đó ⊔ và ⊓ tồn
tại đối với tất cả ⊆ . Lưu ý rằng một giàn có duy nhất một phần tử lớn nhất
⊤ được định nghĩa là ⊤ = ⊔S và duy nhất một phần tử nhỏ nhất ⊥ được định
Hàm ∶
→ là đơn điệu khi∀ , ∈ ∶ ⊑
hợp của hai hàm đơn điệu là một hàm đơn điệu [15].
⇒ ( ) ⊑ ( ). Lưu ý
Lý thuyết về điểm cố định như sau: trong một giàn L có chiều cao hữu hạn,
mỗi hàm đơn điệu f có duy nhất một điểm cố định nhỏ nhất (least fixed-point)
định nghĩa như sau:
( )=
(⊥)
16
thỏa mãn ( ( )) =
( ). Chứng minh lý thuyết này như sau. Ta có
⊥⊑ (⊥) do ⊥là phần tử nhỏ nhất. Do f là hàm đơn điệu nên (⊥) ⊑ (⊥) và
bằng phép quy nạp ta có (⊥) ⊑
(⊥). Do đó, ta có chuỗi tăng dần:
⊥⊑
Do
(⊥) ⊑
(⊥) · · ·
được giả định là có chiều cao hữu hạn nên sẽ tồn tại
mà
17
2.1.3. Hệ dịch chuyển
Chương trình thường được biểu diễn bằng các hệ dịch chuyển (transition
systems) = 〈Σ, Σ, 〉 với Σ là tập các trạng thái, Σ ⊆ Σ là tập các trạng thái khởi
tạo và ⊆ Σ × Σ là một quan hệ dịch chuyển giữa một trạng thái và các trạng
thái kế tiếp có thể của nó[8].
Ví dụ: Xét chương trình sau
x := 0;
while x < 100 do
x := x + 1;
Chương trình này có thể được biểu diễn như sau:
〈 , {0}, {〈 ,
〉| < 100 ∧
=
+ 1}〉
trong đó Z là tập số nguyên.
2.1.4. Ngữ nghĩa vết
Một phân đoạn vết thực thi hữu hạn
… bắt đầu từ trạng thái bất kỳ
∈ Σ và sau đó di chuyển thông qua các dịch chuyển từ một trạng thái ,
18
Chứng minh như sau :
ℱ ∗⃗ Σ ∗⃗ = ℱ ∗⃗ (
= { | ∈ Σ} ∪ {
= { | ∈ Σ} ∪
|
{
|
Với
=
Σ
Σ ∧ 〈 , ′〉 ∈ }
∈
=Σ ∪
=
Σ )
∈ Σ ∧ 〈 , ′〉 ∈ }
Σ
∅ℱ
( )=
= ⋃
và
→
ℱ ∗ (∅)
( )= (
( )) là hàm lặp của .
Phân tích hình dạng
Phân tích hình dạng là việc xác định tĩnh và tự động các tính chất của heap
của một chương trình (còn được gọi là Store). Mỗi trạng thái của heap có thể
được biểu diễn thông qua một đồ thị gồm các nút đại diện cho các khối bộ nhớ
đã được cấp phát và các cạnh biểu diễn con trỏ giữa các khối bộ nhớ, cùng với
các biến của chương trình cũng có thể trỏ tới các nút trong heap[12]. Hiện nay,
phân tích hình dạng bộ nhớ heap có thể tiếp cận theo nhiều cách khác nhau, và
có thể thực hiện ở nhiều mức (mức cụ thể, mức trừu tượng). Nhưng đều sử dụng
19
lý thuyết giàn ngữ nghĩa của chương trình. Từng nút trong mã nguồn sẽ được
gắn một giá trị ngữ nghĩa(semantic). Ngữ nghĩa của một nút chịu sự ràng buộc
trong mối quan hệ với các nút ở trước và sau nó trong mã nguồn chương trình
tùy theo ngữ nghĩa của các câu lệnh đối với thuộc tính cần xem xét. Từ sự ràng
20
được tất cả các thực thi có thể. Ngược lại, nếu thuộc tính không được chứng
minh thì điều này có thể xảy ra do cảnh báo sai vì vấn đề xấp xỉ.
Trong trường hợp phân tích hình dạng của heap, chúng ta thường phải đối
mặt với các chương trình thao tác với cấu trúc có kích cỡ không giới hạn. Ví dụ
độ dài của danh sách là không giới hạn. Tuy nhiên, chúng ta cần một biểu diễn
giới hạn trong phân tích của chúng ta. Điều này cho thấy sự cần thiết của các kỹ
thuật xấp xỉ. Kỹ thuật diễn giải trừu tượng trong phân tích tĩnh cho phép tóm tắt
hành vi (ngữ nghĩa cụ thể) của lệnh chương trình trên tập vô hạn các trạng thái
có thể có của bộ nhớ. Kết quả sau tóm tắt được gọi là ngữ nghĩa trừu tượng của
lệnh đó. Ngữ nghĩa cụ thể của một lệnh trong chương trình thường được biểu
diễn thông qua các phương pháp hình thức và được sử dụng khá tự nhiên. Tuy
nhiên, trừu tượng hóa ngữ nghĩa cụ thể để tạo ra ngữ nghĩa trừu tượng đảm bảo
tính mạnh, chính xác và có khả năng lập luận được lại là một vấn đề khó khăn.
Điều này đặc biệt đúng với một số vấn đề trong thực tế như: Phân tích hình dạng
(Shape Analysis), phân tích con trỏ, trong đó ngữ nghĩa cụ thể liên quan trực tiếp
tới cấu trúc dữ liệu và bộ nhớ.Trừu tượng hóa heap được chứng minh là một vấn
đề khó khăn trong phân tích tĩnh.
2.3.
Nền tảng diễn giải trừu tượng
Diễn giải trừu tượng là một lý thuyết xấp xỉ đúng đắn ngữ nghĩa của chương
trình, dựa trên các hàm đơn điệu của các tập có thứ tự đặc biệt là giàn. Nó có thể
được xem như một phần thực thi của chương trình máy tính, và thông tin thu
được của nó là ngữ nghĩa của chương trình mà không cần thực hiện tất cả các
tính toán.
Ứng dụng chính của diễn giải trừu tượng là phân thích hình thức tĩnh, và tự
Trong khoa học máy tính, thông tin cụ thể và chính xác nói chung không thể
tính toán được với giới hạn về thời gian và bộ nhớ. Sự trừu tượng được xem như
là câu trả lời tổng quát cho các câu hỏi (ví dụ: trả lời maybe cho câu hỏi yes/no,
tức là “ có thể có hoặc không” khi không thể đưa ra được câu trả lời chính xác
một cách chắc chắn); điều này giúp đơn giản hóa vấn đề, làm cho tuân theo các
giải pháp tự động. Một yêu cầu quan trọng là sự không rõ ràng vẫn đủ để quản
lý các vấn đề trong khi vẫn duy trì được độ chính xác các câu trả lời cho các câu
hỏi quan trọng.
2.3.1. Phân tích trên miền trừu tượng
Lý thuyết diễn giải trừu tượng hình thức hóa ý tưởng: việc chứng minh tính
chất của chương trình có thể được thực hiện trên một số mức độ trừu tượng, ở
đó các chi tiết không liên quan đến ngữ nghĩa cũng như đặc tả chương trình của
chương trình được bỏ qua. Khi đó vấn đề được chuyển về chứng minh một ngữ
nghĩa trừu tượng (abstract semantic) thỏa mãn một đặc tả trừu tượng (abstract
specification). Một ví dụ về ngữ nghĩa trừu tượng là biểu diễn của chương trình
qua Logic Hoare và đặc tả trừu tượng là các bất biến, tính đúng đắn cục bộ
(partial correctness), hoặc tính đúng đắn toàn cục (total correctness) [4]. Lý
22
thuyết diễn giải trừu tượng nghiên cứu về ngữ nghĩa của chương trình, phương
pháp trừu tượng hóa ngữ nghĩa của chương trình,tính đúng đắn (sound) – nếu
chứng minh được rằng ngữ nghĩa trừu tượng thỏa mãn đặc tả trừu tượng thì có
thể chỉ ra rằng ngữ nghĩa cụ thể cũng thỏa mãn đặc tả cụ thể, và tính đầy đủ
(complete) – nếu chứng mình được rằng ngữ nghĩa cụ thể thỏa mãn đặc tả cụ thể
thì cũng có thể chứng minh được trên miền trừu tượng,của phương pháp xấp xỉ
để tạo ra ngữ nghĩa trừu tượng[4].
Quá trình phân tích một chương trình luôn bắt đầu với ngữ nghĩa cụ thể
(concrete semantics) của chương trình đó. Ngữ nghĩa cụ thể là mô hình toán học
mô tả tập tất cả các thực thi trong tất cả các môi trường có thể của chương trình.
Hình 2.6. Kỹ thuật kiểm thử
Copyright: Tài liệu đại học ©