Add Blog for safety-of-methods-for-numeric-primitive-types - 2024-12-02 #51
Conversation
| ``` | ||
| Here, the ```#[requires]``` attribute is used to specify that `unchecked_add` requires the addition to not overflow. This ensures that the function operates within defined behavior when called in an unsafe context. While we directly leveraged the existing precondition in `unchecked_add`, not every function has an explicit precondition check. Still, we can write preconditions for unsafe functions based on the `SAFETY` section in the official documentation or the `SAFETY` comments in the source code. | ||
|
|
||
| The same logic applies to the postconditions (`#[ensure]`) of a function. |
There was a problem hiding this comment.
| The same logic applies to the postconditions (`#[ensure]`) of a function. | |
| The same logic applies to the postconditions (`#[ensures]`) of a function. |
There was a problem hiding this comment.
Also, I don't know what "the same logic" really means here?
| title: Safety of Methods for Numeric Primitive Types | ||
| layout: post | ||
| --- | ||
| Authors : Rajath M Kotyal, Yen-Yun Wu, Lanfei Ma, Junfeng Jin |
There was a problem hiding this comment.
| Authors : Rajath M Kotyal, Yen-Yun Wu, Lanfei Ma, Junfeng Jin | |
| Authors: Rajath M Kotyal, Yen-Yun Wu, Lanfei Ma, Junfeng Jin |
| ### 1. Specifying Safety Preconditions | ||
| ```rust |
There was a problem hiding this comment.
I think it would make for slightly nicer reading if there were one or two sentences of text between the heading and the example. Such text should explain what the source code that follows will exemplify.
| } | ||
| } | ||
| ``` | ||
| Here, the ```#[requires]``` attribute is used to specify that `unchecked_add` requires the addition to not overflow. This ensures that the function operates within defined behavior when called in an unsafe context. While we directly leveraged the existing precondition in `unchecked_add`, not every function has an explicit precondition check. Still, we can write preconditions for unsafe functions based on the `SAFETY` section in the official documentation or the `SAFETY` comments in the source code. |
There was a problem hiding this comment.
Would you mind adding a note on what already was there before you arrived and what it is that you added, i.e., really just the requires clause, but I don't think that is as obvious to other potential readers.
| } | ||
| ``` | ||
| The harness contains several parts: | ||
| - Symbolic values: These values (```num1``` and ```num2```) are generated by Kani using ```kani::any```. |
There was a problem hiding this comment.
Perhaps add a reference to https://model-checking.github.io/kani/tutorial-nondeterministic-variables.html.
|
|
||
| The critical ranges include : | ||
| - Small Ranges Near Zero: Includes values around 0, where behavior transitions (e.g., sign changes) are more likely to expose issues like underflows. | ||
| - Boundary Checks: Covers the maximum and minimum values `(i32::MAX, i32::MIN)`, ensuring the method handles edge cases correctly. |
There was a problem hiding this comment.
| - Boundary Checks: Covers the maximum and minimum values `(i32::MAX, i32::MIN)`, ensuring the method handles edge cases correctly. | |
| - Boundary Checks: Covers the maximum and minimum values (`i32::MAX`, `i32::MIN`), ensuring the method handles edge cases correctly. |
to avoid the impression that you are talking about an (open) interval.
| We also verified safe APIs that internally use the previously verified unsafe methods through the above workflow. | ||
|
|
||
| Why Verify Safe APIs? | ||
| Safe APIs, like widening_mul, leverage internally unsafe operations (e.g., unchecked_mul). Even though marked safe, their reliability still depends on the correctness of these underlying operations. Verifying them ensures no overflow occurs in the wider type used internally. When verifying safe APIs like widening_mul, we consider the underlying unsafe functions and target specific input intervals to ensure correctness across critical ranges, balancing thoroughness with practicality. |
There was a problem hiding this comment.
| Safe APIs, like widening_mul, leverage internally unsafe operations (e.g., unchecked_mul). Even though marked safe, their reliability still depends on the correctness of these underlying operations. Verifying them ensures no overflow occurs in the wider type used internally. When verifying safe APIs like widening_mul, we consider the underlying unsafe functions and target specific input intervals to ensure correctness across critical ranges, balancing thoroughness with practicality. | |
| Safe APIs, like `widening_mul`, leverage internally unsafe operations (e.g., `unchecked_mul`). Even though marked safe, their reliability still depends on the correctness of these underlying operations. Verifying them ensures no overflow occurs in the wider type used internally. When verifying safe APIs like `widening_mul`, we consider the underlying unsafe functions and target specific input intervals to ensure correctness across critical ranges, balancing thoroughness with practicality. |
|
@tautschnig @celinval @zhassan-aws @feliperodri We have finished the draft. Appreciate any feedback :) |
There was a problem hiding this comment.
I really liked the blog post. My main suggestion is to improve a little bit the explanation about the need for range partitioning into the checks that involved multiplication.
I think it's good to clarify that the problem here is the complexity of the SAT formula generated for multiplications. For example, the input space for addition and multiplication are the same, but only the multiplication requires partitioning.
@tautschnig do you know any good reference that we can use so we don't have to give too much details on why multiplications are hard for sat solvers?
Towards : model-checking/verify-rust-std#59
Description : This blog post talks about verifying the safety of unsafe methods which use Rust's numeric primitive data types.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.