charon_lib/ast/
values.rs

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
//! Contains definitions for variables and constant values.

use crate::ast::FloatTy;
use core::hash::Hash;
use derive_generic_visitor::{Drive, DriveMut};
use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
use serde::{Deserialize, Serialize};

// We need to manipulate a lot of indices for the types, variables, definitions,
// etc. In order not to confuse them, we define an index type for every one of
// them (which is just a struct with a unique usize field), together with some
// utilities like a fresh index generator. Those structures and utilities are
// generated by using macros.
// TODO: move
generate_index_type!(VarId, "");

/// A primitive value.
///
/// Those are for instance used for the constant operands [crate::expressions::Operand::Const]
#[derive(
    Debug,
    PartialEq,
    Eq,
    Clone,
    VariantName,
    EnumIsA,
    EnumAsGetters,
    Serialize,
    Deserialize,
    Drive,
    DriveMut,
    Hash,
    PartialOrd,
    Ord,
)]
#[charon::variants_prefix("V")]
pub enum Literal {
    Scalar(ScalarValue),
    Float(FloatValue),
    #[drive(skip)]
    Bool(bool),
    #[drive(skip)]
    Char(char),
    #[drive(skip)]
    ByteStr(Vec<u8>),
    #[drive(skip)]
    Str(String),
}

/// A scalar value.
// We encode it as `{ value: ??; int_ty: IntegerTy; }` in json and on the ocaml side. We therefore
// use a custom (de)serializer.
#[derive(
    Debug,
    PartialEq,
    Eq,
    Copy,
    Clone,
    EnumIsA,
    EnumAsGetters,
    VariantName,
    VariantIndexArity,
    Hash,
    PartialOrd,
    Ord,
    Drive,
    DriveMut,
)]
#[drive(skip)]
pub enum ScalarValue {
    /// Using i64 to be safe
    Isize(i64),
    I8(i8),
    I16(i16),
    I32(i32),
    I64(i64),
    I128(i128),
    /// Using u64 to be safe
    Usize(u64),
    U8(u8),
    U16(u16),
    U32(u32),
    U64(u64),
    U128(u128),
}

/// This is simlar to the Scalar value above. However, instead of storing
/// the float value itself, we store its String representation. This allows
/// to derive the Eq and Ord traits, which are not implemented for floats
#[derive(
    Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Hash, PartialOrd, Ord, Drive, DriveMut,
)]
pub struct FloatValue {
    #[charon::rename("float_value")]
    #[drive(skip)]
    pub value: String,
    #[charon::rename("float_ty")]
    pub ty: FloatTy,
}