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

charon_lib/ast/
values.rs
