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
//! Contains definitions for variables and constant values.
use crate::ast::FloatTy;
use core::hash::Hash;
use derive_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),
Bool(bool),
Char(char),
ByteStr(Vec<u8>),
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,
)]
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")]
pub value: String,
#[charon::rename("float_ty")]
pub ty: FloatTy,
}