From 538c49cd18ad261733e158010b1f525bdf12b7f0 Mon Sep 17 00:00:00 2001 From: Douglas Deslauriers Date: Tue, 10 Jun 2025 18:24:44 +0000 Subject: [PATCH 01/14] [Guideline] Add do not divide by 0 --- src/coding-guidelines/expressions.rst | 40 +++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/src/coding-guidelines/expressions.rst b/src/coding-guidelines/expressions.rst index b73b172..00deec3 100644 --- a/src/coding-guidelines/expressions.rst +++ b/src/coding-guidelines/expressions.rst @@ -81,3 +81,43 @@ Expressions } fn with_base(_: &Base) { ... } + +.. guideline:: Do not divide by 0 + :id: gui_kMbiWbn8Z6g5 + :category: Mandatory + :status: draft + :release: latest + :fls: fls_Q9dhNiICGIfr + :decidability: Undecidable + :scope: System + :tags: numerics + + This guideline applies when unsigned integer or two’s complement division is performed. This includes the + evaluation of a remainder expression. + + .. rationale:: + :id: rat_h84NjY2tLSBW + :status: draft + + Integer division by zero results in a panic, which is an abnormal program state and may terminate the process. + + .. non_compliant_example:: + :id: non_compl_ex_LLs3vY8aGz0F + :status: draft + + When the division is performed, the right operand is evaluated to zero and the program panics. + + .. code-block:: rust + + let x = 0; + let x = 5 / x; + + .. compliant_example:: + :id: compl_ex_Ri9pP5Ch3kbb + :status: draft + + There is no compliant way to perform integer division by zero + + .. code-block:: rust + + let x = 5 % 5; From a9760357bfe29359ca0ded83dbd354357003c3aa Mon Sep 17 00:00:00 2001 From: Douglas Deslauriers Date: Tue, 24 Jun 2025 17:23:21 +0000 Subject: [PATCH 02/14] Remove example code from compliant example As stated there is no compliant way to do this, so no example should be present. --- src/coding-guidelines/expressions.rst | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/coding-guidelines/expressions.rst b/src/coding-guidelines/expressions.rst index 00deec3..9bb6197 100644 --- a/src/coding-guidelines/expressions.rst +++ b/src/coding-guidelines/expressions.rst @@ -117,7 +117,3 @@ Expressions :status: draft There is no compliant way to perform integer division by zero - - .. code-block:: rust - - let x = 5 % 5; From 899d8266d25903d9ddb3dd9a620c145fca1f9c18 Mon Sep 17 00:00:00 2001 From: Douglas Deslauriers Date: Wed, 25 Jun 2025 13:56:39 +0000 Subject: [PATCH 03/14] Add compliant example with a suggestion While the guideline does not strictly apply to this example, it is a good suggestion for what to do instead. --- src/coding-guidelines/expressions.rst | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/coding-guidelines/expressions.rst b/src/coding-guidelines/expressions.rst index 9bb6197..6babfdb 100644 --- a/src/coding-guidelines/expressions.rst +++ b/src/coding-guidelines/expressions.rst @@ -116,4 +116,9 @@ Expressions :id: compl_ex_Ri9pP5Ch3kbb :status: draft - There is no compliant way to perform integer division by zero + There is no compliant way to perform integer division by zero. A checked division will prevent any + division by zero from happening. The programmer can then handle the returned Option. + + .. code-block:: rust + + let x = 5u8.checked_div(0); From 982d7e9e479b835e89dd4015b3acf2e9017dbe07 Mon Sep 17 00:00:00 2001 From: Douglas Deslauriers Date: Mon, 14 Jul 2025 16:33:32 -0400 Subject: [PATCH 04/14] Lowercasing of guideline metadata Co-authored-by: Pete LeVasseur --- src/coding-guidelines/expressions.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/coding-guidelines/expressions.rst b/src/coding-guidelines/expressions.rst index 6babfdb..f51927d 100644 --- a/src/coding-guidelines/expressions.rst +++ b/src/coding-guidelines/expressions.rst @@ -84,12 +84,12 @@ Expressions .. guideline:: Do not divide by 0 :id: gui_kMbiWbn8Z6g5 - :category: Mandatory + :category: mandatory :status: draft :release: latest :fls: fls_Q9dhNiICGIfr - :decidability: Undecidable - :scope: System + :decidability: undecidable + :scope: system :tags: numerics This guideline applies when unsigned integer or two’s complement division is performed. This includes the From 681be7efa528ec16c3f9bbeeaee7b5f8e82cc360 Mon Sep 17 00:00:00 2001 From: Douglas Deslauriers Date: Mon, 14 Jul 2025 16:34:15 -0400 Subject: [PATCH 05/14] Add Rust std link transformation Co-authored-by: Pete LeVasseur --- src/coding-guidelines/expressions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coding-guidelines/expressions.rst b/src/coding-guidelines/expressions.rst index f51927d..305d6a5 100644 --- a/src/coding-guidelines/expressions.rst +++ b/src/coding-guidelines/expressions.rst @@ -117,7 +117,7 @@ Expressions :status: draft There is no compliant way to perform integer division by zero. A checked division will prevent any - division by zero from happening. The programmer can then handle the returned Option. + division by zero from happening. The programmer can then handle the returned :std:``std::option::Option``. .. code-block:: rust From 7fd5a7b5b94a17393b507d515229ee7ba00568ed Mon Sep 17 00:00:00 2001 From: Douglas Deslauriers Date: Thu, 17 Jul 2025 17:36:18 +0000 Subject: [PATCH 06/14] Clarify scope of expressions this applies to --- src/coding-guidelines/expressions.rst | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/coding-guidelines/expressions.rst b/src/coding-guidelines/expressions.rst index 305d6a5..f31a2de 100644 --- a/src/coding-guidelines/expressions.rst +++ b/src/coding-guidelines/expressions.rst @@ -92,8 +92,18 @@ Expressions :scope: system :tags: numerics - This guideline applies when unsigned integer or two’s complement division is performed. This includes the - evaluation of a remainder expression. + This guideline applies when unsigned integer or two’s complement division is performed during the + evaluation of an `ArithmeticExpression + `_. + + Note that this includes the evaluation of a `RemainderExpression + `_, which uses unsigned integer or two's + complement division. + + This rule does not apply to evaluation of a :std:`core::ops::Div` trait on types other than `integer + types `_. The use of + :std:`std::num::NonZero` or is therefore a recommended way to avoid the undecidability of this + guideline. .. rationale:: :id: rat_h84NjY2tLSBW From 6538defd29cbc2b430a93fe59cfe7cb1a4254e87 Mon Sep 17 00:00:00 2001 From: Douglas Deslauriers Date: Wed, 30 Jul 2025 08:41:14 -0400 Subject: [PATCH 07/14] Remove "Note" phrase MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit It is not recommended for normative language Co-authored-by: Alex Eris Celeste née Gilding --- src/coding-guidelines/expressions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coding-guidelines/expressions.rst b/src/coding-guidelines/expressions.rst index c9bcfeb..da01834 100644 --- a/src/coding-guidelines/expressions.rst +++ b/src/coding-guidelines/expressions.rst @@ -97,7 +97,7 @@ Expressions evaluation of an `ArithmeticExpression `_. - Note that this includes the evaluation of a `RemainderExpression + This includes the evaluation of a `RemainderExpression `_, which uses unsigned integer or two's complement division. From 86fe09a3ddfbda066d0841f8adcb2326aac3f498 Mon Sep 17 00:00:00 2001 From: Douglas Deslauriers Date: Wed, 30 Jul 2025 13:12:16 +0000 Subject: [PATCH 08/14] Add missing phrase to NonZero recommendation Also moved to the Rationale. --- src/coding-guidelines/expressions.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/coding-guidelines/expressions.rst b/src/coding-guidelines/expressions.rst index da01834..764001e 100644 --- a/src/coding-guidelines/expressions.rst +++ b/src/coding-guidelines/expressions.rst @@ -102,15 +102,15 @@ Expressions complement division. This rule does not apply to evaluation of a :std:`core::ops::Div` trait on types other than `integer - types `_. The use of - :std:`std::num::NonZero` or is therefore a recommended way to avoid the undecidability of this - guideline. + types `_. .. rationale:: :id: rat_h84NjY2tLSBW :status: draft - Integer division by zero results in a panic, which is an abnormal program state and may terminate the process. + Integer division by zero results in a panic, which is an abnormal program state and may terminate the + process. The use of :std:`std::num::NonZero` as the divisor is a recommended way to avoid the + undecidability of this guideline. .. non_compliant_example:: :id: non_compl_ex_LLs3vY8aGz0F From a36d8afcc845215a03b9984eeaad14d6979b5476 Mon Sep 17 00:00:00 2001 From: Douglas Deslauriers Date: Wed, 30 Jul 2025 13:28:23 +0000 Subject: [PATCH 09/14] Example compliant example with a match expression --- src/coding-guidelines/expressions.rst | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/coding-guidelines/expressions.rst b/src/coding-guidelines/expressions.rst index 764001e..cd514e0 100644 --- a/src/coding-guidelines/expressions.rst +++ b/src/coding-guidelines/expressions.rst @@ -132,7 +132,10 @@ Expressions .. code-block:: rust - let x = 5u8.checked_div(0); + let result = match 5u8.checked_div(0) { + None => 0 + Some(r) => r + }; .. guideline:: The 'as' operator should not be used with numeric operands From 45349b8c82ce1842b668871752c3a4446bdec2a3 Mon Sep 17 00:00:00 2001 From: Douglas Deslauriers Date: Wed, 6 Aug 2025 16:03:59 +0000 Subject: [PATCH 10/14] Downgrade guideline to Required Mandatory is a bit strong for panics as determined in today's meeting. --- src/coding-guidelines/expressions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coding-guidelines/expressions.rst b/src/coding-guidelines/expressions.rst index cd514e0..082d8d0 100644 --- a/src/coding-guidelines/expressions.rst +++ b/src/coding-guidelines/expressions.rst @@ -85,7 +85,7 @@ Expressions .. guideline:: Do not divide by 0 :id: gui_kMbiWbn8Z6g5 - :category: mandatory + :category: required :status: draft :release: latest :fls: fls_Q9dhNiICGIfr From 10efe3a5740eb7fad3b00506a9c1a640a1850d48 Mon Sep 17 00:00:00 2001 From: Douglas Deslauriers Date: Mon, 11 Aug 2025 13:07:27 +0000 Subject: [PATCH 11/14] Add compliant manual check example --- src/coding-guidelines/expressions.rst | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/src/coding-guidelines/expressions.rst b/src/coding-guidelines/expressions.rst index 082d8d0..5ae5125 100644 --- a/src/coding-guidelines/expressions.rst +++ b/src/coding-guidelines/expressions.rst @@ -130,13 +130,27 @@ Expressions There is no compliant way to perform integer division by zero. A checked division will prevent any division by zero from happening. The programmer can then handle the returned :std:``std::option::Option``. + Alternatively the check for zero can be performed manually, however as the complexity of the control + flow leading to the invariant increases it becomes harder for programmers and static analysis tools to + reason about. + .. code-block:: rust let result = match 5u8.checked_div(0) { - None => 0 - Some(r) => r + None => 0 + Some(r) => r }; + let x = 0; + if (x != 0) { + let x = 5 / x; + } + else { + let x = 0; + } + + + .. guideline:: The 'as' operator should not be used with numeric operands :id: gui_ADHABsmK9FXz From bbae26b9329488a4bd8bea4cc19f5958314fd481 Mon Sep 17 00:00:00 2001 From: Douglas Deslauriers Date: Mon, 11 Aug 2025 13:09:09 +0000 Subject: [PATCH 12/14] Add defect tag --- src/coding-guidelines/expressions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coding-guidelines/expressions.rst b/src/coding-guidelines/expressions.rst index 5ae5125..545ac95 100644 --- a/src/coding-guidelines/expressions.rst +++ b/src/coding-guidelines/expressions.rst @@ -91,7 +91,7 @@ Expressions :fls: fls_Q9dhNiICGIfr :decidability: undecidable :scope: system - :tags: numerics + :tags: numerics, defect This guideline applies when unsigned integer or two’s complement division is performed during the evaluation of an `ArithmeticExpression From d8222dbe7d7da7d2664507295689ac022c460458 Mon Sep 17 00:00:00 2001 From: Douglas Deslauriers Date: Fri, 15 Aug 2025 09:53:09 -0400 Subject: [PATCH 13/14] Formatting and prose improvements MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Félix Fischer --- src/coding-guidelines/expressions.rst | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/coding-guidelines/expressions.rst b/src/coding-guidelines/expressions.rst index 545ac95..1facf02 100644 --- a/src/coding-guidelines/expressions.rst +++ b/src/coding-guidelines/expressions.rst @@ -128,11 +128,10 @@ Expressions :status: draft There is no compliant way to perform integer division by zero. A checked division will prevent any - division by zero from happening. The programmer can then handle the returned :std:``std::option::Option``. + division by zero from happening. The programmer can then handle the returned :std:`std::option::Option`. - Alternatively the check for zero can be performed manually, however as the complexity of the control - flow leading to the invariant increases it becomes harder for programmers and static analysis tools to - reason about. + The check for zero can also be performed manually. However, as the complexity of the control + flow leading to the invariant increases, it becomes increasingly harder to reason about it. For both programmers and static analysis tools. .. code-block:: rust From 1076b36b8eb94d66bf25f9c5b265596a110be1ea Mon Sep 17 00:00:00 2001 From: Douglas Deslauriers Date: Fri, 15 Aug 2025 09:53:50 -0400 Subject: [PATCH 14/14] Adding more explanation to the examples MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Félix Fischer --- src/coding-guidelines/expressions.rst | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/coding-guidelines/expressions.rst b/src/coding-guidelines/expressions.rst index 1facf02..6851d74 100644 --- a/src/coding-guidelines/expressions.rst +++ b/src/coding-guidelines/expressions.rst @@ -121,7 +121,7 @@ Expressions .. code-block:: rust let x = 0; - let x = 5 / x; + let y = 5 / x; // This line will panic. .. compliant_example:: :id: compl_ex_Ri9pP5Ch3kbb @@ -135,18 +135,19 @@ Expressions .. code-block:: rust + // Example 1: using the checked division API let result = match 5u8.checked_div(0) { None => 0 Some(r) => r }; - + + // Example 2: performing zero-checks by hand let x = 0; - if (x != 0) { - let x = 5 / x; - } - else { - let x = 0; - } + let y = if x != 0 { + 5 / x + } else { + 0 + };