charon_lib/ast/
values.rs

1//! Contains definitions for variables and constant values.
2
3use crate::ast::FloatTy;
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// We encode it as `{ value: ??; int_ty: IntegerTy; }` in json and on the ocaml side. We therefore
52// use a custom (de)serializer.
53#[derive(
54    Debug,
55    PartialEq,
56    Eq,
57    Copy,
58    Clone,
59    EnumIsA,
60    EnumAsGetters,
61    VariantName,
62    VariantIndexArity,
63    Hash,
64    PartialOrd,
65    Ord,
66    Drive,
67    DriveMut,
68)]
69#[drive(skip)]
70pub enum ScalarValue {
71    /// Using i64 to be safe
72    Isize(i64),
73    I8(i8),
74    I16(i16),
75    I32(i32),
76    I64(i64),
77    I128(i128),
78    /// Using u64 to be safe
79    Usize(u64),
80    U8(u8),
81    U16(u16),
82    U32(u32),
83    U64(u64),
84    U128(u128),
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
