[Guideline] Add do not divide by 0 (#132)

* [Guideline] Add do not divide by 0

* Remove example code from compliant example

As stated there is no compliant way to do this, so no example should be
present.

* 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.

* Lowercasing of guideline metadata

Co-authored-by: Pete LeVasseur <[email protected]>

* Add Rust std link transformation

Co-authored-by: Pete LeVasseur <[email protected]>

* Clarify scope of expressions this applies to

* Remove "Note" phrase

It is not recommended for normative language

Co-authored-by: Alex Eris Celeste née Gilding <[email protected]>

* Add missing phrase to NonZero recommendation

Also moved to the Rationale.

* Example compliant example with a match expression

* Downgrade guideline to Required

Mandatory is a bit strong for panics as determined in today's meeting.

* Add compliant manual check example

* Add defect tag

* Formatting and prose improvements

Co-authored-by: Félix Fischer <[email protected]>

* Adding more explanation to the examples

Co-authored-by: Félix Fischer <[email protected]>

---------

Co-authored-by: Pete LeVasseur <[email protected]>
Co-authored-by: Alex Eris Celeste née Gilding <[email protected]>
Co-authored-by: Alex Eris Celeste née Gilding <[email protected]>
Co-authored-by: Félix Fischer <[email protected]>

Author: 4 people

src/coding-guidelines/expressions.rst

@@ -83,6 +83,75 @@ Expressions
          fn with_base(_: &Base) { ... }
 
 
+.. guideline:: Do not divide by 0
+   :id: gui_kMbiWbn8Z6g5
+   :category: required
+   :status: draft
+   :release: latest
+   :fls: fls_Q9dhNiICGIfr
+   :decidability: undecidable
+   :scope: system
+   :tags: numerics, defect
+
+   This guideline applies when unsigned integer or two’s complement division is performed during the
+   evaluation of an `ArithmeticExpression
+   <https://rust-lang.github.io/fls/expressions.html#arithmetic-expressions>`_.
+
+   This includes the evaluation of a `RemainderExpression
+   <https://rust-lang.github.io/fls/expressions.html#syntax_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 <https://rust-lang.github.io/fls/types-and-traits.html#integer-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. 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
+      :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 y = 5 / x; // This line will panic.
+
+   .. compliant_example::
+      :id: compl_ex_Ri9pP5Ch3kbb
+      :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`.
+
+      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
+
+         // 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;
+         let y = if x != 0 {
+             5 / x
+         } else {
+             0
+         };
+
+
+
+
 .. guideline:: The 'as' operator should not be used with numeric operands
    :id: gui_ADHABsmK9FXz
    :category: advisory