Skip to content

Commit

Permalink
rust: Annotates literals with their type.
Browse files Browse the repository at this point in the history
Cargo clippy reports unnecessary literal casting, instead
do annotate every literal with its type. This change does not
affect any static cast.

[1] https://rust-lang.github.io/rust-clippy/master/index.html#/unnecessary_cast
  • Loading branch information
armfazh committed Sep 23, 2023
1 parent 85e0822 commit 37ee69f
Showing 1 changed file with 6 additions and 7 deletions.
13 changes: 6 additions & 7 deletions src/Stringification/Rust.v
Original file line number Diff line number Diff line change
Expand Up @@ -107,13 +107,12 @@ Module Rust.
++ [""])%list%string.

(* Instead of "macros for minimum-width integer constants" we tried to
use numeric casts in Rust. It turns out that it wasn't needed and Rust
will figure out the types of the litterals, so disabling this for
now *)
use numeric casts in Rust. *)
Definition cast_literal (prefix : string) (t : ToString.int.type) : option string :=
if Z.ltb (ToString.int.bitwidth_of t) 8
then None
else None.
let width := if Z.ltb (ToString.int.bitwidth_of t) 8
then 8
else (ToString.int.bitwidth_of t) in
Some ( (if int.is_unsigned t then "u" else "i") ++ Decimal.Z.to_string width )%string.


(* Zoe: In fiat-crypto C functions are void and as such, they receive
Expand Down Expand Up @@ -153,7 +152,7 @@ Module Rust.
(* Integer literal to string *)
Definition int_literal_to_string (prefix : string) (t : IR.type.primitive) (v : BinInt.Z) : string :=
match t, cast_literal prefix (ToString.int.of_zrange_relaxed r[v ~> v]) with
| IR.type.Z, Some cast => "(" ++ HexString.of_Z v ++ cast ++ ")"
| IR.type.Z, Some cast => HexString.of_Z v ++ "_" ++ cast
| IR.type.Z, None => (* just print hex value, no cast *) HexString.of_Z v
| IR.type.Zptr, _ => "#error ""literal address " ++ HexString.of_Z v ++ """;"
end.
Expand Down

0 comments on commit 37ee69f

Please sign in to comment.