2.21 Hệ thống kiểu và phân tích tĩnh

Tổng quan và động lực

Phần lớn khiếm khuyết bị bắt muộn, lúc chạy, bởi một bài kiểm thử, một người dùng hay một sự cố. Cả một lớp trong số chúng không bao giờ cần đi xa đến vậy. Một hệ thống kiểu và một công cụ phân tích chương trình tĩnh tốt đọc mã của bạn trước khi nó chạy và chứng minh rằng một số sai lầm nhất định không thể xảy ra: một chuỗi được dùng ở nơi cần một số, một giá trị rỗng bị truy cập, một biến được đọc trước khi được ghi, một trường hợp bị bỏ sót. Chương này nói về việc đẩy tính đúng đắn sang trái, gần hơn với khoảnh khắc bạn viết dòng mã, nơi một bản sửa tốn vài giây thay vì một trang trong báo cáo rà soát sự cố.

Phân tích tĩnh là bất kỳ kỹ thuật nào kiểm tra mã nguồn hoặc mã đã biên dịch mà không thực thi nó. Kiểm tra kiểu là dạng phổ biến nhất, nhưng họ này còn bao gồm linter (công cụ đánh dấu các mẫu phong cách và tính đúng đắn), bộ phân tích luồng dữ liệu, và, ở thái cực xa, kiểm chứng hình thức. Lời hứa chung là một lớp đảm bảo bạn nhận miễn phí trên mọi bản dựng, mãi mãi, không cần viết kiểm thử và không cần người đánh giá nhớ. Lời hứa đó là lý do kỷ luật này nằm cạnh tiêu chuẩn viết mã (chương 2.1), nguyên tắc thiết kế phần mềm (chương 2.2) và chiến lược kiểm thử (chương 2.4): nó là một cách tự động nữa để làm một cơ sở mã lớn an toàn để thay đổi.

Với các đội lớn, giá trị cộng dồn. Khi hàng trăm kỹ sư chạm vào một hệ thống dùng chung, một chữ ký kiểu là một hợp đồng mà trình biên dịch thực thi với từng người, và một bộ kiểm tra trong đường ống là một người đánh giá không bao giờ mệt và không bao giờ thiên vị. Trong bối cảnh doanh nghiệp điều này cắt giảm chi phí hội nhập và tích hợp, vì các kiểu ghi lại ý định và các bộ phân tích bắt những sai lầm mà người mới mắc. Trong chính phủ và các hệ thống rủi ro cao khác, nơi một câu trả lời sai có thể từ chối một khoản trợ cấp hoặc làm lộ dữ liệu, các đảm bảo được máy kiểm tra là bằng chứng: chúng cho kiểm toán viên thấy cả các loại khiếm khuyết là bất khả theo cấu trúc, không chỉ là chưa được kiểm thử. Điều này kết nối trực tiếp với chất lượng phần mềm (chương 2.11) và bảo mật ứng dụng (chương 4.2).

Các nguyên tắc chính

Đẩy tính đúng đắn sang trái: bắt khiếm khuyết tại thời điểm soạn thảo, không phải trên môi trường thực.
Ưu tiên các đảm bảo máy kiểm tra hơn các quy ước mà con người phải nhớ.
Mã hóa ý định vào các kiểu để các trạng thái bất hợp lệ hoàn toàn không thể biểu diễn.
Áp dụng kiểu dần dần trong mã động; bạn không cần tất cả hay không gì.
Coi cảnh báo là lỗi, và vặn chặt đường cơ sở để nó chỉ cải thiện.
Chạy cùng các bộ phân tích trong trình soạn thảo và trong đường ống, với các quy tắc giống hệt.
Quản lý dương tính giả bằng sự ngăn chặn có kỷ luật, có lý do, rà soát được.

Khuyến nghị

Chọn kiểu tĩnh hay kiểu động với đôi mắt mở to

Trong một ngôn ngữ định kiểu tĩnh, các kiểu được kiểm tra trước khi chương trình chạy; trong một ngôn ngữ định kiểu động, chúng được kiểm tra khi nó chạy, nếu có. Không cái nào đúng phổ quát, và cách đóng khung trung thực là một sự đánh đổi các đảm bảo lấy sự linh hoạt. Định kiểu tĩnh mua cho bạn các hợp đồng được máy kiểm tra, tái cấu trúc bạn có thể tin, và công cụ (tự động hoàn thành, đổi tên an toàn, nhảy tới định nghĩa) biết mọi thứ là gì. Định kiểu động mua cho bạn tạo bản mẫu nhanh, mã ngắn gọn, và nghi thức thấp phù hợp với tập lệnh và công việc thăm dò. Hệ thống càng lớn, càng tồn tại lâu và càng nhiều rủi ro, phía tĩnh càng hoàn vốn, vì cả chi phí của một lần tái cấu trúc toàn cơ sở mã lẫn chi phí của một lỗi kiểu lúc chạy đều tăng theo quy mô.

Hãy chính xác về một trục thứ hai, trực giao: kiểu mạnh so với kiểu yếu. Một ngôn ngữ kiểu mạnh từ chối âm thầm ép các kiểu không tương thích (cộng một số với một chuỗi sinh ra lỗi); một ngôn ngữ kiểu yếu lặng lẽ chuyển đổi, tạo ra những bất ngờ như "3" + 4 cho ra thứ bạn không định. Bạn có thể có tĩnh và yếu, hoặc động và mạnh. Khi bạn đánh giá một ngôn ngữ, hãy hỏi hai câu riêng biệt, vì “mạnh” thường là thứ mọi người thực sự muốn khi họ nói “có kiểu”.

Dựa vào suy luận kiểu để giữ chi phí kiểu thấp

Một phản đối phổ biến với định kiểu tĩnh là nhiễu của việc viết một kiểu trên mỗi dòng. Suy luận kiểu loại bỏ phần lớn chi phí đó: trình biên dịch suy ra kiểu từ ngữ cảnh, nên bạn chú thích các ranh giới (chữ ký hàm, giao diện công khai) và để phần bên trong được suy luận. Các ngôn ngữ hiện đại suy luận quyết liệt, cho bạn sự an toàn của kiểm tra tĩnh với nhiều sự ngắn gọn của mã động. Hãy áp dụng một quy tắc nhà chú thích những phần người đọc dựa vào như một hợp đồng, các hàm được xuất và kiểu công khai, và để các biến cục bộ cho suy luận. Điều này giữ chữ ký trung thực và tự ghi chép trong khi tránh cho phần bên trong khỏi lộn xộn, và nó gắn lại với mục tiêu khả năng đọc của chương 2.1.

Làm cho trạng thái bất hợp lệ không thể biểu diễn

Ý tưởng mạnh nhất trong thiết kế kiểu thực tế là định hình các kiểu của bạn để một trạng thái sai không thể được viết ra. Nếu một đơn hàng hoặc là “bản nháp” không có thanh toán hoặc là “đã đặt” có một thanh toán, đừng mô hình hóa nó như một cấu trúc có các trường nullable nơi một bản nháp có thể vô tình mang thanh toán và một đơn đã đặt có thể không mang gì. Hãy mô hình hóa nó như một kiểu tổng (còn gọi là hợp có thẻ, hợp phân biệt, hoặc biến thể): một giá trị chính xác là một trong một tập cố định các hình dạng, mỗi hình mang dữ liệu riêng. Giờ các tổ hợp không hợp lệ không tồn tại, và mã xử lý giá trị phải tính đến từng trường hợp nếu không trình biên dịch phàn nàn. Điều này biến một “không bao giờ nên xảy ra” lúc chạy thành một “không thể xảy ra” lúc biên dịch, đó là toàn bộ điểm mấu chốt.

Cùng bản năng đó thúc đẩy nhiều công cụ hằng ngày. Dùng một kiểu liệt kê thay vì một chuỗi ma thuật cho một tập trạng thái cố định. Bọc một giá trị đã xác thực trong một kiểu riêng biệt (một EmailAddress thay vì một chuỗi trần) để “đầu vào chưa xác thực” và “email đã xác thực” là các kiểu khác nhau mà trình biên dịch giữ tách biệt. Đây là cách diễn đạt trong hệ thống kiểu của kỷ luật xác thực ranh giới từ xử lý lỗi (chương 2.20): xác thực một lần ở rìa, chuyển thành một kiểu mã hóa đảm bảo, và để phần bên trong tin tưởng nó.

Coi trọng khả năng rỗng và kiểu tổng quát

Con trỏ rỗng, mà người phát minh ra nó gọi là “sai lầm tỷ đô”, là cách phổ biến nhất mà một hệ thống kiểu tĩnh từng nói dối: một giá trị được định kiểu là chuỗi có thể bí mật là rỗng, và bạn biết điều đó nhờ một vụ sập. Các hệ thống kiểu hiện đại sửa điều này bằng cách làm khả năng rỗng tường minh. Một giá trị hoặc là một String không bao giờ rỗng hoặc là một kiểu Option/Maybe/nullable bạn phải mở ra trước khi dùng, và trình biên dịch buộc bạn xử lý trường hợp rỗng. Nếu ngôn ngữ của bạn cung cấp kiểu không thể rỗng hoặc kiểu tùy chọn, hãy dùng chúng ở mọi nơi và coi một nullable trần là một mùi. Điều này loại bỏ cả một chi các sự cố môi trường thực.

Kiểu tổng quát, còn gọi là đa hình tham số, cho phép bạn viết mã hoạt động trên nhiều kiểu mà không từ bỏ an toàn kiểu: một List<T> là một danh sách của một kiểu T cụ thể nào đó, được kiểm tra lúc biên dịch, thay vì một danh sách các thứ không có kiểu mà bạn ép kiểu rồi cầu nguyện. Hãy với tới kiểu tổng quát để xây các vật chứa, hàm và trừu tượng tái sử dụng được mà vẫn định kiểu mạnh. Sự kết hợp của kiểu tổng, kiểu không thể rỗng và kiểu tổng quát là thứ cho phép một hệ thống kiểu hiện đại diễn đạt các quy tắc miền thực thay vì chỉ gắn thẻ các nguyên thủy.

Áp dụng kiểu dần dần trong mã động hiện có

Bạn không phải viết lại một cơ sở mã động để có lợi ích của việc định kiểu. Định kiểu dần dần cho phép mã có kiểu và không kiểu cùng tồn tại, để bạn thêm kiểu từng bước ở nơi chúng hoàn vốn nhiều nhất. Nhiều hệ sinh thái nay hỗ trợ điều này trực tiếp: gợi ý kiểu trong Python được kiểm tra bởi một bộ kiểm tra kiểu riêng, một tập mở rộng có kiểu biên dịch ra một ngôn ngữ động, hoặc chú thích kiểu chồng lên một môi trường chạy hiện có. Hãy bắt đầu ở các ranh giới và các mô-đun quan trọng nhất (mã tiền, mã bảo mật, mô hình dữ liệu), bật bộ kiểm tra ở chế độ dễ dãi, và siết chặt dần theo thời gian. Thêm một quy tắc rằng mã mới phải có kiểu ngay cả khi mã cũ đang bắt kịp. Trong vài quý, một cơ sở mã lớn không có kiểu có thể đạt đến điểm mà phần lớn thay đổi được kiểm tra kiểu, và các phần quan trọng nhất được bao phủ trước.

Chạy linter, bộ kiểm tra kiểu và bộ phân tích sâu cùng nhau

Kiểm tra kiểu là một tầng; hãy thêm các tầng khác. Một công cụ lint bắt các mẫu đáng ngờ mà bộ kiểm tra kiểu bỏ qua: một phép gán luôn đúng, một biến không dùng, một rơi xuống trong câu lệnh switch, một tài nguyên không bao giờ được đóng. Các bộ phân tích sâu hơn suy luận về hành vi của chương trình. Phân tích luồng dữ liệu theo dõi các giá trị di chuyển qua mã thế nào để trả lời các câu hỏi như “biến này có bao giờ được dùng trước khi được gán không” hoặc “tay cầm tệp này có thể rò rỉ trên đường lỗi không.” Nhiều công cụ này được xây trên diễn giải trừu tượng, một kỹ thuật chạy chương trình trong trừu tượng trên các tập giá trị có thể (ví dụ, “dương”, “không” hoặc “âm” thay vì số chính xác) để chứng minh các thuộc tính trên mọi lần thực thi cùng lúc, mà không chạy bất kỳ cái nào.

Một số bộ phân tích nằm cạnh công cụ bảo mật. Kiểm thử bảo mật ứng dụng tĩnh (SAST) quét mã nguồn tìm các mẫu lỗ hổng như tiêm, giải tuần tự hóa không an toàn, hoặc dữ liệu bị nhiễm đến một điểm nguy hiểm, và nó chia sẻ bộ máy luồng dữ liệu được mô tả ở đây; hãy coi nó là một phần của họ này và điều phối nó với bảo mật ứng dụng (chương 4.2). Khuyến nghị thực tế là một bộ phân tầng: một linter nhanh cho phong cách và lỗi hiển nhiên, một bộ kiểm tra kiểu cho hợp đồng, và một hoặc nhiều bộ phân tích sâu hơn cho các thuộc tính quan trọng với miền của bạn. Hãy cấu hình chúng từ các tệp được quản lý phiên bản để các quy tắc giống nhau cho mọi người.

Coi cảnh báo là lỗi và vặn chặt đường cơ sở

Một cảnh báo không làm hỏng bản dựng là một cảnh báo sẽ bị phớt lờ. Một khi nhật ký đầy hàng trăm cảnh báo được dung thứ, không ai đọc nó, và cảnh báo quan trọng ẩn trong nhiễu. Hãy áp dụng chính sách coi-cảnh-báo-là-lỗi để một cảnh báo mới làm hỏng bản dựng và được sửa ngay khoảnh khắc nó rẻ nhất. Trên một cơ sở mã cũ với hàng nghìn cảnh báo sẵn có, bạn không thể bật công tắc đó qua đêm, vì vậy hãy dùng một bánh cóc: ghi lại số lượng hiện tại làm đường cơ sở, chặn bất kỳ thay đổi nào làm tăng nó, và đẩy nó xuống theo thời gian. Đường cơ sở chỉ có thể giảm. Điều này cho phép bạn bật một quy tắc nghiêm ngặt hôm nay mà không cần dọn dẹp lớn ban đầu, đồng thời đảm bảo tình hình không bao giờ tệ đi và đều đặn tốt lên.

Nối phân tích vào trình soạn thảo và CI, với phản hồi nhanh

Phân tích tĩnh hoàn vốn nhiều nhất khi phản hồi là tức thì. Hãy chạy cùng các kiểm tra trong trình soạn thảo, qua Giao thức Máy chủ Ngôn ngữ hoặc tương đương, để lập trình viên thấy lỗi khi họ gõ, trước cả khi lưu. Rồi chạy bộ quy tắc giống hệt trong tích hợp liên tục (CI) để không gì được hợp nhất mà không đạt, gắn điều này vào đường ống của chương 8.1. Hai bên phải khớp nhau: nếu trình soạn thảo dễ dãi và CI nghiêm ngặt, hoặc ngược lại, mọi người mất niềm tin vào cả hai. Giữ phân tích đủ nhanh để chạy trên mọi thay đổi, lưu đệm kết quả, và chỉ phân tích những gì thay đổi ở nơi có thể, để bộ kiểm tra là sự trợ giúp thay vì một khoản thuế. Khi trình soạn thảo và đường ống thực thi cùng các quy tắc theo cùng cách, tiêu chuẩn thôi là một tài liệu mọi người quên và trở thành thuộc tính của môi trường.

Dành kiểm chứng hình thức cho mã xứng đáng với nó

Ở thái cực xa của phổ là kiểm chứng hình thức: chứng minh bằng toán học rằng một chương trình thỏa mãn một đặc tả chính xác, không chỉ là vượt qua kiểm thử. Các kỹ thuật trải từ kiểm tra mô hình (khám phá vét cạn các trạng thái của hệ thống) đến chứng minh định lý và kiểu phụ thuộc (kiểu đủ biểu đạt để mã hóa đặc tả đầy đủ). Đây là đảm bảo sâu nhất có sẵn và tốn kém nhất để tạo ra, nên nó chỉ xứng đáng có chỗ ở nơi một khiếm khuyết là thảm khốc hoặc nơi chứng nhận đòi hỏi: thư viện mật mã, mã điều khiển bay, một hypervisor, một giao thức quan trọng. Với hầu hết phần mềm, khoản đầu tư đúng là kiểu mạnh cộng bộ phân tích tốt, nắm bắt phần lớn lợi ích với một phần nhỏ chi phí. Hãy biết rằng các phương pháp hình thức (được giới thiệu trong chương 2.12) tồn tại và lằn ranh nằm ở đâu, để bạn với tới chúng có chủ đích cho thành phần hiếm hoi cần chúng.

Giữ sự ngăn chặn trung thực

Không bộ phân tích nào hoàn hảo, và kỷ luật phân biệt một công cụ được tin cậy với một công cụ bị phớt lờ là cách bạn xử lý sai lầm của nó. Mọi công cụ nghiêm túc đều cho phép bạn ngăn chặn một phát hiện. Hãy yêu cầu mỗi sự ngăn chặn hẹp (một dòng hay một phát hiện, không bao giờ cả tệp hay quy tắc), kèm lý do trong bình luận, và hiển thị trong đánh giá như bất kỳ mã nào khác. Một lệnh tắt hàng loạt ở đầu tệp là cách độ bao phủ lặng lẽ mục nát. Hãy kiểm toán các sự ngăn chặn định kỳ và coi một đống ngày càng lớn của chúng là tín hiệu rằng một quy tắc bị hiệu chuẩn sai hoặc mã có một vấn đề thực mà ai đó đang giấu. Sự ngăn chặn trung thực giữ cho công cụ đáng tin; sự ngăn chặn im lặng, bao trùm biến nó thành sân khấu.

Đánh đổi: ưu và nhược điểm

Cách tiếp cận	Ưu điểm	Nhược điểm
Định kiểu tĩnh	Hợp đồng được máy kiểm tra; tái cấu trúc an toàn; công cụ phong phú	Nhiều nghi thức ban đầu hơn; tạo bản mẫu ban đầu chậm hơn
Định kiểu động	Viết nhanh; linh hoạt; ít nghi thức	Lỗi kiểu nổi lên lúc chạy; tái cấu trúc rủi ro
Suy luận kiểu	An toàn với sự ngắn gọn; ít nhiễu chú thích	Kiểu được suy luận có thể che khuất ý định nếu dùng quá mức
Định kiểu dần dần	Áp dụng từng bước; bao phủ mã quan trọng trước	Rìa không kiểu vẫn rò rỉ; đảm bảo từng phần
Linter và phân tích luồng dữ liệu	Bắt lỗi mà kiểu bỏ sót; rẻ để chạy	Dương tính giả; nhiễu nếu không cấu hình
Cảnh báo-là-lỗi với bánh cóc	Vấn đề mới bị chặn; đường cơ sở chỉ cải thiện	Có thể có cảm giác cản trở; cần chính sách ngăn chặn
Kiểm chứng hình thức	Đảm bảo mạnh nhất; chứng minh thuộc tính cho mọi đầu vào	Tốn kém, chuyên biệt; hiếm khi được biện minh

Căng thẳng lặp lại là các đảm bảo so với ma sát. Mỗi nấc về phía định kiểu chặt hơn và phân tích sâu hơn mua cho bạn một lớp lỗi trở nên bất khả, và mỗi nấc thêm nghi thức, thời gian chạy công cụ, và dương tính giả thỉnh thoảng tốn của lập trình viên vài phút. Hãy giải quyết theo mức độ rủi ro và tuổi thọ. Một tập lệnh dùng một lần hay một thử nghiệm muốn đầu nhẹ, nhanh, động. Một sổ cái thanh toán, một kiểm tra quyền, hay một hệ thống mà chính phủ sẽ vận hành mười lăm năm muốn kiểu mạnh, bộ phân tích phân tầng, cảnh báo-là-lỗi, và, cho lõi nguy hiểm nhất của nó, có lẽ cả chứng minh hình thức. Hãy khớp sự chặt chẽ với chi phí của việc sai, và để suy luận cùng áp dụng dần dần giữ ma sát ở mức gánh được.

Câu hỏi để thảo luận với đội của bạn

Ở đâu trong cơ sở mã của chúng ta một hệ thống kiểu sẽ đã ngăn chặn vài sự cố môi trường thực gần nhất, và chúng ta có biết không? Hầu hết các đội tranh luận về định kiểu trong trừu tượng khi bằng chứng nằm trong lịch sử sự cố của chính họ. Hãy lấy mười hay hai mươi khiếm khuyết môi trường thực gần nhất và phân loại: bao nhiêu cái là giá trị rỗng ở nơi mong đợi một giá trị, một hình dạng sai truyền qua một ranh giới, một trường hợp không được xử lý, một giá trị kiểu chuỗi trôi dạt? Đó chính xác là những khiếm khuyết mà bộ kiểm tra kiểu và linter bắt miễn phí. Nếu một phần lớn sự cố của bạn nằm trong nhóm đó, bạn có một lập luận cụ thể, tính bằng đô la cho định kiểu mạnh hơn trong các mô-đun nơi chúng xảy ra. Nếu gần như không có, lỗi của bạn sống ở nơi khác (logic, đồng thời, yêu cầu) và định kiểu nặng hơn có thể không phải bước đi có giá trị cao nhất của bạn. Dù thế nào bạn cũng thay ý kiến bằng dữ liệu.
Nếu chúng ta áp dụng định kiểu dần dần, chúng ta sẽ bắt đầu ở đâu, và “đủ rồi” nghĩa là gì? Bật một bộ kiểm tra trên một cơ sở mã động lớn là một chương trình, không phải bật một công tắc, và trình tự quyết định nó thành công hay đình trệ. Hãy thảo luận mô-đun nào mang nhiều rủi ro nhất (tiền, xác thực, mô hình dữ liệu cốt lõi) và do đó xứng đáng có kiểu trước, so với mô-đun nào ổn định và ít rủi ro đủ để để không kiểu lúc này. Hãy thống nhất một quy tắc cho mã mới (có kiểu từ ngày đầu) để bề mặt không kiểu ngừng lớn lên trong khi bạn gặm dần phần tồn đọng. Xác định một mục tiêu: có lẽ mọi chữ ký hàm công khai có kiểu, mọi ranh giới được xác thực thành một kiểu, bộ kiểm tra chạy ở chế độ nghiêm ngặt trên các gói quan trọng. Không có vạch đích xác định, định kiểu dần dần trở nên vĩnh viễn và được bao phủ một nửa, tệ nhất của cả hai thế giới.
Chính sách của chúng ta là gì khi một bộ phân tích tĩnh sai, và nó có giữ công cụ đáng tin không? Mọi bộ phân tích đều tạo ra dương tính giả, và cách bạn xử lý chúng quyết định công cụ còn hữu ích hay bị tắt trong bực bội. Hãy đi qua các trường hợp cụ thể: khi một phát hiện là dương tính giả thực sự, sự ngăn chặn có hẹp, có bình luận kèm lý do, và hiển thị trong đánh giá không, hay ai đó tắt cả quy tắc cho cả kho mã? Hãy nhìn các sự ngăn chặn hiện tại của bạn: có bao nhiêu, chúng có kèm lý do không, và lần cuối có ai kiểm toán chúng là khi nào? Một đống ngăn chặn rộng, không giải thích nghĩa là độ bao phủ của bạn rỗng một cách lặng lẽ. Mục tiêu là một kỷ luật chung, được thực thi giữ cho bộ phân tích đáng tin, để các phát hiện của nó được tin và hành động theo thay vì bị làm lặng theo phản xạ.
Chúng ta chuẩn hóa trên ngôn ngữ và bộ phân tích nào, và làm thế nào chúng ta giữ một bộ quy tắc khi bộ công nghệ của chúng ta phân mảnh qua các đội? Khi hàng trăm kỹ sư làm việc trong nhiều ngôn ngữ, mỗi đội trôi về bộ kiểm tra, quy tắc lint và thiết lập mức nghiêm ngặt của riêng mình lặng lẽ phá hủy đảm bảo, vì một hợp đồng được thực thi trong một kho mã chỉ là một gợi ý ở kho kế bên. Lực kéo đối lập là thật: chuẩn hóa trung tâm cho bạn kỹ sư di chuyển được và bằng chứng kiểm toán đồng nhất, nhưng một bộ quy tắc áp đặt từ trung tâm có thể chống lại thành ngữ của ngôn ngữ hoặc làm chậm một đội có lý do chính đáng cho cấu hình của riêng họ. Hãy mang một bản kiểm kê các ngôn ngữ trên môi trường thực, các bộ phân tích và phiên bản mỗi đội chạy, và một bản so sánh các bộ quy tắc của họ để sự trôi dạt hiển thị thay vì được giả định. Trong bối cảnh doanh nghiệp hoặc chính phủ, hãy gắn câu trả lời với mua sắm và kiểm toán: một cấu hình duy nhất được quản lý phiên bản mà mọi kho mã thừa kế là thứ cho phép kiểm toán viên xác nhận cùng các kiểm tra đã chạy ở mọi nơi, và là thứ ngăn một nhà cung cấp phát hành mã dưới các quy tắc yếu hơn mà nhân viên của bạn phải đáp ứng.
Phân tích của chúng ta nhanh đến đâu, và đến điểm nào mọi người bắt đầu đi vòng qua nó? Một bộ kiểm tra chỉ là một đảm bảo nếu nó chạy trên mọi thay đổi, và khoảnh khắc nó khiến vòng soạn thảo-dựng đau đớn, kỹ sư học cách bỏ qua nó, tắt nó cục bộ, hoặc hợp nhất khi nó còn đỏ và hứa sẽ sửa sau. Căng thẳng là độ sâu so với tốc độ: một lượt luồng dữ liệu hoặc bảo mật sâu hơn tìm ra lỗi mà một linter nhanh bỏ sót, nhưng nếu bộ đầy đủ mất hai mươi phút mọi người ngừng chờ nó, và một kiểm tra không ai chờ thì không bảo vệ gì. Hãy mang các con số thực vào cuộc thảo luận: độ trễ phản hồi trình soạn thảo, thời gian đồng hồ CI cho giai đoạn phân tích, tỷ lệ trúng bộ nhớ đệm, các bản dựng được hợp nhất thường xuyên thế nào với kiểm tra bị bỏ qua hoặc ghi đè, và bao nhiêu phần của lần chạy là tăng dần so với đầy đủ. Với một tổ chức lớn hoặc công, hãy thêm hóa đơn tính toán và chi phí thông lượng, vì ở quy mô đội máy một giai đoạn phân tích bắt buộc chậm vừa là một khoản mục ngân sách vừa là một hàng đợi trì hoãn mọi bản phát hành, và cách sửa trung thực thường là phân tích tăng dần và lưu đệm thay vì lặng lẽ nới lỏng các quy tắc.
Bằng chứng được máy kiểm tra nào chúng ta thực sự có thể cung cấp cho kiểm toán viên, và nó bao phủ những bất biến quan trọng nào của chúng ta? Trong các hệ thống chịu quy định và rủi ro cao, điểm của định kiểu và phân tích tĩnh là bằng chứng chứng minh được rằng cả các lớp khiếm khuyết là bất khả theo cấu trúc, ngoài các lỗi hằng ngày nó ngăn chặn, và khẳng định đó vô giá trị nếu bạn không thể cho thấy bất biến nào được thực thi và ở đâu. Sự đánh đổi là phạm vi so với chi phí: chứng minh nhiều hơn (không thể rỗng ở mọi nơi, kiểu tổng cho mọi trạng thái hợp lệ, kiểm chứng hình thức của phép tính lõi) mua bằng chứng mạnh hơn, nhưng mỗi bước lên về độ chặt chẽ tốn công sức chú thích, thời gian chuyên gia và độ phức tạp bản dựng mà bạn có thể không cần trên mã ít rủi ro. Hãy mang một bản đồ các mô-đun quan trọng về an toàn của bạn tới các đảm bảo mỗi cái hiện mang, danh sách các sự ngăn chặn còn mở kèm lý do của chúng, và bất kỳ khoảng trống nào nơi một quy tắc quan trọng được thực thi bằng quy ước thay vì trình biên dịch. Với một chính phủ hoặc doanh nghiệp chịu quy định, hãy đóng khung điều này như bằng chứng chứng nhận: một kiểm toán viên nên có thể truy vết một thuộc tính bắt buộc về một kiểu hoặc chứng minh được máy kiểm tra và thấy nhật ký ngăn chặn ghi lại mọi ngoại lệ, để sự tuân thủ dựa trên các hiện vật do bộ công cụ tạo ra thay vì rà soát thủ công sau sự việc.

Góc nhìn theo lĩnh vực

Công ty khởi nghiệp. Tốc độ thắng, vì vậy hãy với tới sự an toàn rẻ nhất không làm bạn chậm: một ngôn ngữ định kiểu mạnh hoặc một bộ kiểm tra kiểu ở chế độ dễ dãi, cộng một linter nhanh trong trình soạn thảo, và định kiểu mã tiền và xác thực của bạn trước. Bỏ qua hoàn toàn kiểm chứng hình thức và các bộ luồng dữ liệu sâu; chúng tốn thời gian bạn không có. Phần thưởng bạn muốn sớm là một lần tái cấu trúc bạn có thể tin ở mười nghìn dòng, vì vậy hãy bật bộ kiểm tra trước khi cơ sở mã quá lớn để thuần hóa.

Doanh nghiệp nhỏ. Không có chuyên gia phân tích tĩnh trong biên chế, hãy ưu tiên một ngôn ngữ và bộ công cụ nơi các mặc định tốt được tích hợp sẵn thay vì một bộ bạn phải điều chỉnh và trông nom. Hãy mua phân tích nhúng trong IDE và CI lưu trữ của bạn thay vì dựng nền tảng riêng, và giữ bộ quy tắc gần với tiêu chuẩn cộng đồng để một nhà thầu hay nhân viên mới nhận ra nó. Hãy coi cảnh báo-là-lỗi và một lõi có kiểu nhỏ là những bước đi có đòn bẩy cao nhất mà ngân sách hạn chế của bạn có thể thực hiện.

Doanh nghiệp lớn. Công việc là quản trị qua nhiều đội: một cấu hình duy nhất được quản lý phiên bản mà mọi kho mã thừa kế, quy tắc giống hệt trong trình soạn thảo và đường ống, và một đường cơ sở được vặn chặt để độ bao phủ của không đội nào có thể lặng lẽ giảm. Chuẩn hóa các bộ phân tích, theo dõi độ bao phủ kiểu và số lượng ngăn chặn như các chỉ số danh mục, và kiểm toán các sự ngăn chặn theo nhịp cố định để các đảm bảo được máy kiểm tra giữ đủ đồng nhất để kiểm toán viên dựa vào. Hãy ngân sách cho nhóm nền tảng sở hữu cấu hình dùng chung, vì tính nhất quán qua hàng nghìn kỹ sư không tự duy trì.

Chính phủ. Mua sắm, tính minh bạch và tuổi thọ dài chi phối. Hãy yêu cầu trong hợp đồng rằng nhà cung cấp đáp ứng cùng các quy tắc phân tích như nhân viên của bạn và bàn giao cấu hình cùng nhật ký ngăn chặn như sản phẩm bàn giao, để đảm bảo sống sót qua việc đổi nhà cung cấp. Hãy ưu tiên bằng chứng được máy kiểm tra hơn đảm bảo thủ công cho logic đủ điều kiện và thanh toán, dành kiểm chứng hình thức cho các phép tính mà thất bại sẽ từ chối một khoản trợ cấp trái pháp luật, và giữ mọi sự ngăn chặn được lập tài liệu để kiểm toán trong cả thập kỷ hoặc hơn mà hệ thống sẽ chạy.

Ví dụ

Công ty khởi nghiệp. Một công ty khởi nghiệp sáu người xây sản phẩm của mình bằng một ngôn ngữ động để có tốc độ, điều phục vụ họ tốt cho đến khi một lần tái cấu trúc ở mười nghìn dòng bắt đầu gây ra lỗi kiểu lúc chạy mà họ chỉ phát hiện trên môi trường thực. Họ áp dụng định kiểu dần dần: bật một bộ kiểm tra kiểu ở chế độ dễ dãi, thêm gợi ý kiểu vào mô hình miền cốt lõi và mã thanh toán của họ trước, và đặt quy tắc rằng mọi mô-đun mới phải có kiểu đầy đủ. Họ nối bộ kiểm tra và một linter vào trình soạn thảo và CI với cấu hình giống hệt, và coi cảnh báo mới là lỗi trong khi vặn chặt các cảnh báo hiện có xuống. Trong hai quý các vụ sập do hình dạng không khớp biến mất, tái cấu trúc thôi đáng sợ, và tính năng tự động hoàn thành của nhân viên mới thực sự biết mỗi hàm trả về gì. Khoản đầu tư tốn vài tuần công kỹ sư và loại bỏ một nguồn lỗi thường xuyên hướng đến khách hàng.

Doanh nghiệp lớn. Một ngân hàng toàn cầu chuẩn hóa phân tích tĩnh qua hàng nghìn kỹ sư. Mọi kho mã thừa kế một cấu hình chung: một bộ kiểm tra kiểu ở chế độ nghiêm ngặt, một linter, một bộ phân tích luồng dữ liệu, và một bộ quét SAST cho các mẫu bảo mật, tất cả chạy trong trình soạn thảo và được thực thi trong đường ống để không gì được hợp nhất mà không đạt. Các kiểu miền khiến trạng thái bất hợp lệ không thể biểu diễn trong mã chuyển tiền: một giao dịch đã ghi và một giao dịch đang chờ là các kiểu khác nhau, tiền tệ được định kiểu để bạn không thể cộng đô la với euro, và đầu vào đã xác thực là các kiểu khác với đầu vào thô. Cảnh báo là lỗi, và đường cơ sở của mỗi đội chỉ có thể giảm. Các sự ngăn chặn đòi hỏi một lý do và được kiểm toán hằng quý. Vì các đảm bảo được máy kiểm tra và đồng nhất, kiểm toán viên có thể thấy cả các lớp khiếm khuyết là bất khả theo cấu trúc, và kỹ sư di chuyển tự tin qua các dịch vụ lạ.

Chính phủ. Một cơ quan thuế quốc gia hiện đại hóa một hệ thống tính toán trợ cấp phải đúng và giải thích được trong nhiều năm. Logic đủ điều kiện cốt lõi được viết bằng một ngôn ngữ định kiểu mạnh nơi mô hình miền mã hóa các quy tắc: tình trạng của người nộp đơn là một kiểu tổng bao phủ mọi trường hợp hợp lệ, số tiền là một kiểu chuyên dụng không thể bị nhầm với số đếm, và không giá trị nào có thể bị thiếu được để thành nullable trần. Phân tích tĩnh chạy trong CI như một cổng, và mô-đun tính toán quan trọng nhất về an toàn được kiểm tra thêm bằng phương pháp hình thức để chứng minh các bất biến chính đúng cho mọi đầu vào, đáp ứng yêu cầu chứng nhận. Mọi sự ngăn chặn được lập tài liệu để kiểm toán. Khi các tác giả gốc đi nơi khác, những người kế nhiệm thừa kế mã có hợp đồng được trình biên dịch thực thi, nên họ có thể thay đổi nó an toàn một thập kỷ sau.

Luận chứng kinh doanh: động lực, ROI và TCO

Lợi tức của định kiểu và phân tích tĩnh là sự dịch chuyển nơi bạn trả giá cho khiếm khuyết. Một khiếm khuyết được bộ kiểm tra kiểu bắt trong trình soạn thảo tốn vài giây; cùng khiếm khuyết đó bị bắt trên môi trường thực tốn một sự cố, một cuộc điều tra, có thể là thiệt hại cho khách hàng và một phát hiện của cơ quan quản lý. Các nghiên cứu về kinh tế khiếm khuyết luôn cho thấy chi phí tăng một bậc độ lớn ở mỗi giai đoạn một lỗi sống sót, từ soạn thảo đến đánh giá đến kiểm thử đến môi trường thực. Phân tích tĩnh chuyển cả một loại khiếm khuyết đến giai đoạn rẻ nhất, trên mọi bản dựng, không tốn lao động cho từng khiếm khuyết. Đó là một chi phí thiết lập cố định, phần lớn một lần mua một dòng khiếm khuyết được ngăn chặn không giới hạn, gần như là đòn bẩy tốt nhất trong kỹ thuật.

Các chi phí là thật nhưng khiêm tốn và dồn về phía trước. Bạn chọn và cấu hình công cụ, bạn trả một chút nghi thức trong chú thích (được làm dịu bởi suy luận), bạn dành thời gian kỹ sư áp dụng định kiểu dần dần trong mã cũ, và bạn chấp nhận dương tính giả thỉnh thoảng. Đối chiếu với đó, hãy cân nhắc tổng chi phí sở hữu của phương án thay thế: mọi lỗi dạng kiểu đến được môi trường thực, mọi lần tái cấu trúc rủi ro bị tránh vì không gì đảm bảo tính đúng đắn, mọi lần hội nhập chậm vì mã không tự ghi lại hợp đồng của nó, và trong bối cảnh chịu quy định mọi cuộc kiểm toán phải được thỏa mãn bằng rà soát thủ công thay vì bằng chứng được máy kiểm tra. Để thuyết phục ban lãnh đạo, hãy gắn nó với các chỉ số họ vốn đã theo dõi: tỷ lệ thay đổi thất bại, tỷ lệ lỗi thoát ra, thời gian phục hồi trung bình, và tỷ lệ sự cố có thể quy cho các lỗi kiểu và rỗng có thể ngăn chặn. Biểu đồ thuyết phục mọi người là lịch sử sự cố của chính bạn được sắp xếp theo việc một bộ kiểm tra có bắt được hay không.

Phản mẫu và cạm bẫy

Lối thoát hiểm như một thói quen: ép kiểu sang any, dynamic hoặc tương đương không kiểu để làm lặng bộ kiểm tra, xóa đảm bảo chính xác ở nơi bạn cần nhất.
Mọi thứ kiểu chuỗi: truyền chuỗi trần và bản đồ không kiểu qua các ranh giới thay vì mô hình hóa trạng thái thành kiểu thực, nên trình biên dịch không thể giúp.
Nullable theo mặc định: để các giá trị nullable khi ngôn ngữ cung cấp kiểu không thể rỗng và tùy chọn, giữ nguyên sai lầm tỷ đô.
Cảnh báo không bao giờ làm hỏng: hàng nghìn cảnh báo được dung thứ trong đó cái quan trọng vô hình, vì không gì từng làm hỏng bản dựng.
Trình soạn thảo và CI bất đồng: dễ dãi cục bộ và nghiêm ngặt trong đường ống, hoặc ngược lại, nên lập trình viên mất niềm tin vào cả hai và các lần hợp nhất làm mọi người bất ngờ.
Ngăn chặn hàng loạt: tắt cả một quy tắc hay tệp thay vì một phát hiện có lý do, lặng lẽ làm rỗng độ bao phủ.
Sân khấu phân tích: chạy các công cụ mà phát hiện của chúng không ai đọc hay hành động, nên báo cáo tích tụ và giá trị bằng không.
Định kiểu tất cả-hoặc-không: từ chối bắt đầu vì bạn không thể định kiểu mọi thứ cùng lúc, bỏ lỡ lợi ích lớn từ việc định kiểu mã quan trọng trước.
Kiểm chứng ở khắp nơi: với tới phương pháp hình thức cho mã thông thường, tiêu tốn nỗ lực chuyên gia khan hiếm ở nơi kiểu mạnh đã đủ.

Mô hình trưởng thành

Mức 1, Khởi đầu: Định kiểu và phân tích tùy nghi và theo từng lập trình viên. Mã động không có bộ kiểm tra, hoặc một ngôn ngữ tĩnh chạy với cảnh báo bị phớt lờ. Lỗi dạng kiểu (rỗng, hình dạng sai, trường hợp không được xử lý) đến được môi trường thực thường xuyên, và tái cấu trúc bị sợ vì không gì xác minh tính đúng đắn.
Mức 2, Phát triển: Một linter và, ở nơi liên quan, một bộ kiểm tra kiểu chạy trên một số dự án, nhưng quy tắc khác nhau giữa các đội, cảnh báo không làm hỏng bản dựng, và lối thoát hiểm cùng ngăn chặn rộng là phổ biến. Một số lợi ích được hiện thực hóa, nhưng độ bao phủ không nhất quán và niềm tin vào công cụ chắp vá.
Mức 3, Chuẩn hóa: Một cấu hình dùng chung, được quản lý phiên bản thực thi kiểm tra kiểu và lint trong trình soạn thảo và CI với quy tắc giống hệt trong toàn tổ chức. Cảnh báo là lỗi với đường cơ sở được vặn chặt, khả năng rỗng và kiểu tổng được dùng để làm trạng thái bất hợp lệ không thể biểu diễn tại các ranh giới, và mọi sự ngăn chặn đòi hỏi một lý do có tài liệu, rà soát được.
Mức 4, Quản lý: Phân tích được đo và kiểm soát theo các đường cơ sở. Độ bao phủ kiểu trên các mô-đun quan trọng, số cảnh báo, tỷ lệ dương tính giả, số lượng ngăn chặn, và tỷ lệ sự cố môi trường thực mà một bộ kiểm tra sẽ bắt được đều được theo dõi so với các mục tiêu tường minh. Các chỉ số đặt cổng cho thay đổi: độ bao phủ trên mã tiền và xác thực không thể giảm, tỷ lệ dương tính giả tăng kích hoạt hiệu chuẩn lại quy tắc, và bảng điều khiển cho thấy các đảm bảo có thực sự đứng vững thay vì chỉ được cấu hình.
Mức 5, Điều phối: Phân tích được cải tiến liên tục và tích hợp trong toàn tổ chức. Định kiểu dần dần đã đến các mô-đun quan trọng, các bộ phân tích luồng dữ liệu và bảo mật chạy thường lệ, quy tắc thích ứng khi ngôn ngữ và mối đe dọa tiến hóa, và kiểm chứng hình thức được áp dụng có chủ đích cho vài thành phần mà thất bại sẽ là thảm khốc. Bộ công cụ, chỉ số và bộ quy tắc phản hồi vào thiết kế, tuyển dụng và mua sắm, để cả tổ chức đều đặn an toàn hơn để thay đổi.

Ý tưởng để thảo luận

Những lỗi môi trường thực gần đây nào của bạn mà một bộ kiểm tra kiểu hay linter sẽ đã bắt được, và chúng chiếm bao nhiêu phần trong tổng số?
Ở đâu trong mô hình miền của bạn một kiểu tổng hay một kiểu bọc đã xác thực có thể biến một “không bao giờ nên xảy ra” lúc chạy thành một “không thể xảy ra” lúc biên dịch?
Nếu bạn biến cảnh báo thành lỗi vào ngày mai, bao nhiêu cái sẽ làm hỏng bản dựng, và đường cơ sở cùng bánh cóc nào cho phép bạn áp dụng chính sách mà không cần một chiến dịch dọn dẹp?
Trình soạn thảo và đường ống của bạn có chạy chính xác cùng các quy tắc không, và một lập trình viên sẽ phát hiện thế nào nếu chúng đã trôi xa nhau?
Có bao nhiêu sự ngăn chặn sống trong cơ sở mã của bạn ngay bây giờ, bao nhiêu cái kèm lý do, và chúng được kiểm toán lần cuối khi nào?
Có thành phần nào trong hệ thống của bạn mà thất bại là thảm khốc đủ để biện minh cho kiểm chứng hình thức không, và làm sao bạn biết?

Những điểm cần ghi nhớ

Định kiểu tĩnh và phân tích đẩy cả một lớp khiếm khuyết đến khoảnh khắc rẻ nhất để sửa: khi bạn viết mã, trên mọi bản dựng, không tốn lao động cho từng khiếm khuyết.
Ưu tiên các đảm bảo máy kiểm tra hơn các quy ước mà con người phải nhớ, và mã hóa ý định vào các kiểu để các trạng thái bất hợp lệ hoàn toàn không thể biểu diễn.
Bạn không cần tất cả hay không gì: định kiểu dần dần cho phép bạn bao phủ mã quan trọng (tiền, xác thực, mô hình dữ liệu) trước trong khi phần còn lại bắt kịp.
Coi cảnh báo là lỗi với đường cơ sở được vặn chặt, chạy quy tắc giống hệt trong trình soạn thảo và CI, và giữ sự ngăn chặn hẹp, có lý do và được kiểm toán.
Khớp sự chặt chẽ với rủi ro: kiểu mạnh cộng bộ phân tích phân tầng cho hầu hết hệ thống, và kiểm chứng hình thức dành cho thành phần hiếm hoi mà thất bại là thảm khốc.

Tài liệu tham khảo và đọc thêm

Benjamin C. Pierce, Types and Programming Languages
Simon Peyton Jones (biên tập), The Implementation of Functional Programming Languages
Flemming Nielson, Hanne Riis Nielson và Chris Hankin, Principles of Program Analysis
Patrick Cousot và Radhia Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints”
Scott Wlaschin, Domain Modelling Made Functional
Steve McConnell, Code Complete: A Practical Handbook of Software Construction
Michael Barr và MISRA Consortium, MISRA C: Guidelines for the Use of the C Language in Critical Systems
Al Bessey và cộng sự, “A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World,” Communications of the ACM