memory.rs

use byteorder::{ReadBytesExt, WriteBytesExt, LittleEndian, BigEndian};
use std::collections::{btree_map, BTreeMap, HashMap, HashSet, VecDeque, BTreeSet};
use std::{fmt, iter, ptr, mem, io};

use rustc::{ty, mir};
use rustc::ty::layout::{self, TargetDataLayout};

use constraints::ConstraintContext;
use error::{EvalError, EvalResult};
use value::{self, PrimVal, PrimValKind, Value};

////////////////////////////////////////////////////////////////////////////////
// Allocations and pointers
////////////////////////////////////////////////////////////////////////////////

#[derive(Copy, Clone, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct AllocId(pub u64);

impl fmt::Display for AllocId {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        write!(f, "{}", self.0)
    }
}

#[derive(Debug, Clone, Copy, Eq, PartialEq)]
pub struct AbstractVariable(pub u32);

#[derive(Debug, Clone, Copy, Eq, PartialEq)]
pub enum SByte {
    Concrete(u8),
    Abstract(AbstractVariable),
}

#[derive(Debug, Clone)]
pub struct Allocation {
    /// The actual bytes of the allocation.
    /// Note that the bytes of a pointer represent the offset of the pointer
    pub bytes: Vec<SByte>,

    /// Maps from byte addresses to allocations.
    /// Only the first byte of a pointer is inserted into the map.
    pub relocations: BTreeMap<u64, AllocId>,

    /// Denotes undefined memory. Reading from undefined memory is forbidden in miri
    pub undef_mask: UndefMask,

    /// The alignment of the allocation to detect unaligned reads.
    pub align: u64,

    /// Whether the allocation may be modified.
    /// Use the `mark_static_initalized` method of `Memory` to ensure that an error occurs, if the memory of this
    /// allocation is modified or deallocated in the future.
    pub static_kind: StaticKind,
}

#[derive(Debug, PartialEq, Copy, Clone)]
pub enum StaticKind {
    /// may be deallocated without breaking miri's invariants
    NotStatic,
    /// may be modified, but never deallocated
    Mutable,
    /// may neither be modified nor deallocated
    Immutable,
}

#[derive(Copy, Clone, Debug, Eq, PartialEq)]
pub struct Pointer {
    pub alloc_id: AllocId,
    pub offset: PointerOffset,
}