Khi port logic kiểm tra kiểu từ JavaScript (duyc.js) sang DUY native (tc_subset.duy), chúng tôi phải đối mặt với một vấn đề: làm sao chắc chắn rằng compiler mới có chung một phán quyết với compiler cũ trên mọi tình huống phức tạp? Nếu hai checker lệch pha, ngôn ngữ sẽ bị phân mảnh ngay từ lõi ngữ nghĩa.
Sprint 109 giải quyết bài toán này bằng Differential Type Checking.
Chúng tôi xây dựng một mismatch matrix chạy tự động. Lần lượt chạy cả hai trình biên dịch (JS oracle và DUY native) trên toàn bộ suite test. Trình so sánh sẽ đối chiếu đầu ra: file nào được accept, file nào bị reject, và nếu reject thì lỗi báo ở vị trí nào.
source.duy -> [ JS Typechecker ] -> OK / Error at line L \ Must agree
-> [ Native Typechecker ] -> OK / Error at line L / on verdict!
Differential check lập tức chỉ ra những góc khuất. Có những trường hợp JS checker do tính chất động của ngôn ngữ đã bỏ qua một lỗi gán giá trị, trong khi DUY native checker do tính tĩnh nghiêm ngặt đã từ chối thẳng thừng. Ngược lại, có những đoạn code mượn vùng nhớ hợp lệ bị DUY checker từ chối oan vì phân tích dòng dữ liệu chưa đủ tinh tế.
Tôi nhớ có một test case liên quan đến việc gán một view[u8] vào một struct tạm thời. JS checker báo xanh, còn native checker báo đỏ lừ vì cho rằng view bị escape scope. Đọc kỹ đặc tả thì cả hai bên đều có lý do của riêng mình. Tôi phải ngồi lại phân tích cặn kẽ xem đâu là hành vi đúng chuẩn của ngôn ngữ (source of truth) và sửa đổi compiler tương ứng. Con đường tiến về parity 100% không có chỗ cho cảm giác hay phỏng đoán; nó chỉ có số liệu và sự đồng thuận tuyệt đối giữa hai thế hệ trình biên dịch.
Bình luận (0)
Đang tải bình luận...