Bằng cách so sánh các trình biên dịch trên chương trình C ngẫu nhiên, Csmith giúp các nhà nghiên cứu tìm và báo cáo hơn 325 lỗi trình biên dịch

21/10/2026 · VietTechies · Biên tập

Thử hình dung bạn biên dịch cùng một chương trình C được tạo tự động bằng hai trình biên dịch (compiler), rồi nhận được hai kết quả khác nhau: một tệp thực thi in ra 0, tệp còn lại in ra 1. Nếu chương trình tránh được hành vi không xác định, quá trình thực thi không phụ thuộc vào những lựa chọn chưa được đặc tả, và hai compiler dùng các hành vi do bản triển khai quy định tương thích với nhau, thì sự khác biệt ấy cho thấy compiler có lỗi. Được công bố mã nguồn mở vào năm 2009, Csmith đã giúp đưa cách kiểm thử vi sai này vào thực tế: trong bài báo năm 2011, nhóm nghiên cứu tại Đại học Utah đứng sau công cụ này đã báo cáo hơn 325 lỗi compiler chưa từng được biết đến.

Mối nguy âm thầm khi compiler biên dịch sai

Trong kỹ thuật phần mềm, compiler giữ một vai trò đòi hỏi sự tin cậy. Lập trình viên dựa vào compiler để chuyển mã nguồn mà con người đọc được thành các lệnh máy, đồng thời giữ nguyên chính xác ngữ nghĩa của chương trình gốc. Lỗi trong compiler có thể làm mất tính đúng đắn ngay cả khi mã nguồn đã qua kiểm chứng hình thức.

Thế nhưng, compiler là những hệ thống lớn và hết sức phức tạp, thực hiện hàng chục lượt tối ưu hóa đòi hỏi sự cẩn trọng. Lỗi có thể khiến chính compiler dừng đột ngột, hoặc khiến nó biên dịch sai: compiler hoàn tất công việc bình thường nhưng sinh ra các lệnh máy dẫn đến hành vi sai. Những trường hợp biên dịch sai thường không đi kèm bất kỳ cảnh báo nào từ compiler. Các lỗi âm thầm như vậy đặc biệt khó phát hiện, bởi kiểm thử phần mềm thông thường phụ thuộc vào một oracle — chuẩn đối chiếu đã biết hoặc kết quả đầu ra dự kiến dùng để đánh giá một lần chạy thử.

Dùng kết quả khác nhau làm chuẩn đối chiếu kiểm thử

Để tháo gỡ nút thắt này, một nhóm nghiên cứu tại Đại học Utah gồm Xuejun Yang, Yang Chen, Eric Eide và John Regehr đã phát triển Csmith. Csmith giải quyết bài toán tìm chuẩn đối chiếu bằng kiểm thử vi sai ngẫu nhiên. Thay vì cố tính trước hành vi dự kiến của một chương trình phức tạp được tạo ra để kiểm thử, Csmith sinh các chương trình C ngẫu nhiên rồi biên dịch từng chương trình bằng nhiều compiler khác nhau, bằng các phiên bản khác nhau của cùng một bộ công cụ, hoặc bằng cùng một compiler với các cờ cấu hình (flag) tối ưu hóa khác nhau.

Bằng cách chạy các tệp thực thi vừa tạo và so sánh kết quả in ra trên màn hình dòng lệnh, Csmith biến sự khác biệt giữa các compiler thành một chuẩn đối chiếu kiểm thử tự động. Nếu bộ công cụ biên dịch GNU Compiler Collection (GCC) và Clang cho cùng kết quả đầu ra, lần kiểm thử chưa cho thấy dấu hiệu bất thường nào ngay lúc đó. Nhưng nếu một tệp thực thi in ra con số khác hoặc dừng đột ngột trong khi tệp kia kết thúc bình thường, sự khác biệt ấy trực tiếp chỉ ra lỗi ở một trong các compiler — hoặc, trong những trường hợp hiếm gặp, lỗi trong chính bộ sinh chương trình của Csmith.

Tránh những cạm bẫy của hành vi không xác định

Sinh chương trình C ngẫu nhiên khó hơn nhiều so với sinh chương trình bằng các ngôn ngữ an toàn bộ nhớ. Chuẩn ngôn ngữ C có các nhóm hành vi không xác định và hành vi chưa đặc tả, từ tràn số nguyên có dấu, dịch bit với số vị trí dịch âm cho đến truy cập biến chưa khởi tạo và giải tham chiếu con trỏ null. Khi chương trình thực hiện hành vi không xác định, chuẩn C không còn ràng buộc compiler phải bảo đảm bất kỳ hành vi nào; compiler tối ưu hóa được phép giả định rằng các phép toán không xác định sẽ không bao giờ xảy ra, từ đó biến đổi hoặc xóa cả những khối code.

Chỉ sinh ngẫu nhiên cú pháp C sẽ không tạo ra những bảo đảm về ngữ nghĩa cần thiết cho kiểm thử vi sai. Nhóm nghiên cứu Utah thiết kế Csmith để kiểm thử con trỏ, mảng, luồng điều khiển, cấu trúc và biểu thức, đồng thời dùng phân tích tĩnh và các bước kiểm tra khi chạy để tránh hành vi không xác định cũng như sự phụ thuộc vào những lựa chọn chưa được đặc tả. Việc so sánh còn đòi hỏi các hành vi do từng bản triển khai quy định phải tương thích, chẳng hạn độ rộng và cách biểu diễn số nguyên. Vì chương trình C có hành vi được xác định rõ vẫn có thể chạy vòng lặp vô hạn, hệ thống chạy kiểm thử của Csmith kết hợp các biện pháp bảo đảm ngữ nghĩa với giới hạn thời gian thực thi nghiêm ngặt.

Hàng trăm lỗi chưa từng được biết đến

Trong bài báo “Finding and Understanding Bugs in C Compilers” tại hội nghị năm 2011 về thiết kế và triển khai ngôn ngữ lập trình của ACM SIGPLAN (PLDI), các tác giả báo cáo hơn 325 lỗi compiler chưa từng được biết đến, tìm thấy trong ba năm kiểm thử. Ngày 18 tháng 3 năm 2011, khi thông báo đã hoàn tất bản thảo cuối cùng để xuất bản, Regehr viết trên blog nghiên cứu của mình rằng sau thời điểm chốt số liệu cho bài báo, tổng số lỗi được báo cáo đã lên tới 344.

Trong toàn bộ nghiên cứu, mỗi compiler được kiểm thử đều có những phiên bản dừng đột ngột và âm thầm biên dịch sai các chương trình C hợp lệ. Csmith tìm thấy lỗi sinh mã sai trong front end (phần xử lý đầu vào) chưa được kiểm chứng của các phiên bản CompCert trước đó, nhưng không tìm thấy lỗi như vậy trong phiên bản đang phát triển được kiểm thử vào đầu năm 2011. Phần lớn lỗi của GCC nằm ở middle end, trong khi LLVM cũng có nhiều lỗi đáng kể ở front end và back end. Trong số các lỗi đã xem xét, các tác giả xác định nguyên nhân gốc rễ phổ biến nhất là những bước kiểm tra không đúng về độ an toàn của phép tối ưu hóa.

Kiểm thử giới hạn của kiểm chứng hình thức

Csmith còn mang đến một phép thử độc lập cho phần mềm đã qua kiểm chứng hình thức. Nhóm nghiên cứu Utah tiến hành kiểm thử ngẫu nhiên nghiêm ngặt đối với CompCert — compiler tối ưu hóa cho ngôn ngữ C do Xavier Leroy cùng các cộng sự phát triển, với các lượt xử lý cốt lõi được chứng minh đúng về mặt toán học bằng công cụ hỗ trợ chứng minh Coq. Vào đầu năm 2011, sau khi dành tổng thời gian xử lý tương đương khoảng sáu năm trên một bộ xử lý cho các lượt chạy ngẫu nhiên để kiểm thử những bản CompCert đang phát triển, Csmith không tìm thấy một lỗi sinh mã sai nào trong các lượt xử lý middle end đã được kiểm chứng của CompCert.

Kết quả này cung cấp bằng chứng thực nghiệm cụ thể rằng các chứng minh toán học được máy kiểm tra thực sự giúp bảo vệ chương trình trước lỗi biên dịch sai. Đồng thời, nhóm nghiên cứu và chính tài liệu CompCert cũng nêu rõ những giới hạn của kiểm chứng trong thực tế. Các chứng minh toán học của CompCert bao phủ những lượt biên dịch đã được kiểm chứng, từ cây cú pháp trừu tượng đến dạng biểu diễn hợp ngữ; các công đoạn chưa được kiểm chứng như tiền xử lý, phân tích cú pháp, dịch hợp ngữ và liên kết vẫn nằm ngoài phạm vi chứng minh hình thức.

Tìm lỗi mà không cần biết trước đáp án

Csmith cho thấy các chương trình ngẫu nhiên có khả năng biểu đạt phong phú có thể tìm ra những lỗi mà các bộ kiểm thử compiler sẵn có bỏ sót. Kiểm thử compiler bằng chương trình ngẫu nhiên đã có lịch sử lâu dài, bắt nguồn từ những công cụ kiểm thử vi sai trước đó nhiều thập kỷ. Đóng góp của Csmith là kết hợp nhiều tính năng của ngôn ngữ C với các biện pháp có hệ thống để tránh hành vi không xác định và sự phụ thuộc vào những lựa chọn chưa được đặc tả.

Nghiên cứu cho thấy một lợi ích thực tế của kiểm thử vi sai: phương pháp này phát hiện hàng trăm lỗi chưa từng được biết đến trong cả compiler mã nguồn mở lẫn compiler thương mại, và phần lớn lỗi được báo cáo đã được sửa. Với các kỹ sư phần mềm kiểm thử hệ thống phức tạp, bài học còn nguyên giá trị là các bản triển khai độc lập có thể giúp phát hiện sai sót của nhau một cách hiệu quả, miễn là đầu vào được ràng buộc chặt chẽ để tránh hành vi mơ hồ.

Bài liên quan

Đọc bằng ngôn ngữ khác: English