charon_lib/ast/
values.rs

1//! Contains definitions for variables and constant values.
2
3use crate::ast::{FloatTy, IntTy, UIntTy};
4use core::hash::Hash;
5use derive_generic_visitor::{Drive, DriveMut};
6use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
7use serde::{Deserialize, Serialize};
8use serde_state::{DeserializeState, SerializeState};
9
10// We need to manipulate a lot of indices for the types, variables, definitions,
11// etc. In order not to confuse them, we define an index type for every one of
12// them (which is just a struct with a unique usize field), together with some
13// utilities like a fresh index generator. Those structures and utilities are
14// generated by using macros.
15// TODO: move
16generate_index_type!(LocalId, "");
17
18/// A primitive value.
19///
20/// Those are for instance used for the constant operands [crate::expressions::Operand::Const]
21#[derive(
22    Debug,
23    PartialEq,
24    Eq,
25    Clone,
26    VariantName,
27    EnumIsA,
28    EnumAsGetters,
29    Serialize,
30    Deserialize,
31    SerializeState,
32    DeserializeState,
33    Drive,
34    DriveMut,
35    Hash,
36    PartialOrd,
37    Ord,
38)]
39#[charon::variants_prefix("V")]
40#[serde_state(stateless)]
41pub enum Literal {
42    Scalar(ScalarValue),
43    Float(FloatValue),
44    #[drive(skip)]
45    Bool(bool),
46    #[drive(skip)]
47    Char(char),
48    #[drive(skip)]
49    ByteStr(Vec<u8>),
50    #[drive(skip)]
51    Str(String),
52}
53
54/// A scalar value.
55#[derive(
56    Debug,
57    PartialEq,
58    Eq,
59    Copy,
60    Clone,
61    EnumIsA,
62    EnumAsGetters,
63    VariantName,
64    VariantIndexArity,
65    Hash,
66    PartialOrd,
67    Ord,
68    Serialize,
69    Deserialize,
70    Drive,
71    DriveMut,
72)]
73#[drive(skip)]
74#[charon::variants_suffix("Scalar")]
75pub enum ScalarValue {
76    Unsigned(
77        UIntTy,
78        #[serde(with = "crate::ast::values_utils::scalar_value_ser_de")] u128,
79    ),
80
81    Signed(
82        IntTy,
83        #[serde(with = "crate::ast::values_utils::scalar_value_ser_de")] i128,
84    ),
85}
86
87/// This is simlar to the Scalar value above. However, instead of storing
88/// the float value itself, we store its String representation. This allows
89/// to derive the Eq and Ord traits, which are not implemented for floats
90#[derive(
91    Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Hash, PartialOrd, Ord, Drive, DriveMut,
92)]
93pub struct FloatValue {
94    #[charon::rename("float_value")]
95    #[drive(skip)]
96    pub value: String,
97    #[charon::rename("float_ty")]
98    pub ty: FloatTy,
99}
charon_lib/ast/values.rs

charon_lib/ast/
values.rs
