<commit_before>/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/
#pragma once
#include <memory>
#include <vector>
#include "util/debug.h"
#include "util/rc.h"
#include "util/numerics/mpz.h"
#include "kernel/environment.h"

namespace lean {
class vm_obj;
enum class vm_obj_kind { Simple, Constructor, Closure, MPZ, External };

/** \brief Base class for VM objects.

    \remark Simple objects are encoded as tagged pointers. */
class vm_obj_cell {
protected:
    MK_LEAN_RC(); // Declare m_rc counter
    vm_obj_kind m_kind;
    void dealloc();
    void dec_ref(vm_obj & o, buffer<vm_obj_cell*> & todelete);
    vm_obj_cell(vm_obj_kind k):m_rc(0), m_kind(k) {}
public:
    vm_obj_kind kind() const { return m_kind; }
};

#define LEAN_VM_IS_PTR(obj) ((reinterpret_cast<size_t>(obj) & 1) == 0)
#define LEAN_VM_BOX(num)    (reinterpret_cast<vm_obj_cell*>((num << 1) | 1))
#define LEAN_VM_UNBOX(obj)  (reinterpret_cast<size_t>(obj) >> 1)

/** \brief VM object */
class vm_obj {
    vm_obj_cell * m_data;
    friend class vm_obj_cell;
    vm_obj_cell * steal_ptr() {
        lean_assert(LEAN_VM_IS_PTR(m_data)); vm_obj_cell * r = m_data; m_data = LEAN_VM_BOX(0); return r;
    }
public:
    vm_obj():m_data(LEAN_VM_BOX(0)) {
        static_assert(sizeof(vm_obj) == sizeof(void *), "unexpected class obj size"); // NOLINT
    }
    vm_obj(unsigned cidx):m_data(LEAN_VM_BOX(cidx)) {}
    vm_obj(vm_obj_cell * c):m_data(c) { m_data->inc_ref(); }
    vm_obj(vm_obj const & o):m_data(o.m_data) { if (LEAN_VM_IS_PTR(m_data)) m_data->inc_ref(); }
    vm_obj(vm_obj && o):m_data(o.m_data) { o.m_data = LEAN_VM_BOX(0); }
    ~vm_obj() { if (LEAN_VM_IS_PTR(m_data)) m_data->dec_ref(); }

    friend void swap(vm_obj & a, vm_obj & b) { std::swap(a.m_data, b.m_data); }

    vm_obj & operator=(vm_obj const & s) {
        if (LEAN_VM_IS_PTR(s.m_data))
            s.m_data->inc_ref();
        auto new_data = s.m_data;
        if (LEAN_VM_IS_PTR(m_data))
            m_data->dec_ref();
        m_data = new_data;
        return *this;
    }

    vm_obj & operator=(vm_obj && s) {
        if (LEAN_VM_IS_PTR(m_data))
            m_data->dec_ref();
        m_data   = s.m_data;
        s.m_data = LEAN_VM_BOX(0);
        return *this;
    }

    vm_obj_kind kind() const {
        return LEAN_VM_IS_PTR(m_data) ? m_data->kind() : vm_obj_kind::Simple;
    }

    vm_obj_cell * raw() const {
        return m_data;
    }
};

class vm_composite : public vm_obj_cell {
    unsigned   m_idx;
    unsigned   m_size;
    vm_obj * get_field_ptr() {
        return reinterpret_cast<vm_obj *>(reinterpret_cast<char *>(this)+sizeof(vm_composite));
    }
    friend vm_obj_cell;
    void dealloc(buffer<vm_obj_cell*> & todelete);
public:
    vm_composite(vm_obj_kind k, unsigned idx, unsigned sz, vm_obj const * data);
    unsigned size() const { return m_size; }
    unsigned idx() const { return m_idx; }
    vm_obj const * fields() const {
        return reinterpret_cast<vm_obj const *>(reinterpret_cast<char const *>(this)+sizeof(vm_composite));
    }
};

class vm_mpz : public vm_obj_cell {
    mpz      m_value;
    friend vm_obj_cell;
    void dealloc();
public:
    vm_mpz(mpz const & v);
    mpz const & get_value() const { return m_value; }
};

class vm_external : public vm_obj_cell {
public:
    virtual ~vm_external() = 0;
};

// =======================================
// Constructors
vm_obj mk_vm_simple(unsigned cidx);
vm_obj mk_vm_constructor(unsigned cidx, unsigned sz, vm_obj const * args);
vm_obj mk_vm_closure(unsigned fnidx, unsigned sz, vm_obj const * args);
vm_obj mk_vm_mpz(mpz const & n);
vm_obj mk_vm_external(vm_external * cell);
/* helper functions for creating natural numbers */
vm_obj mk_vm_nat(unsigned n);
vm_obj mk_vm_nat(mpz const & n);
inline vm_obj mk_vm_false() { return mk_vm_simple(0); }
inline vm_obj mk_vm_true() { return mk_vm_simple(1); }
inline vm_obj mk_vm_bool(bool b) { return mk_vm_simple(b); }
// =======================================

// =======================================
// Testers
inline vm_obj_kind kind(vm_obj const & o) { return o.kind(); }
inline bool is_simple(vm_obj const & o) { return !LEAN_VM_IS_PTR(o.raw()); }
inline bool is_constructor(vm_obj const & o) { return kind(o) == vm_obj_kind::Constructor; }
inline bool is_closure(vm_obj const & o) { return kind(o) == vm_obj_kind::Closure; }
inline bool is_composite(vm_obj const & o) { return is_constructor(o) || is_closure(o); }
inline bool is_mpz(vm_obj const & o) { return kind(o) == vm_obj_kind::MPZ; }
inline bool is_external(vm_obj const & o) { return kind(o) == vm_obj_kind::External; }
bool is_small_nat(vm_obj const & o);
// =======================================

// =======================================
// Casting
inline vm_composite * to_composite(vm_obj const & o) {
    lean_assert(is_composite(o)); return static_cast<vm_composite*>(o.raw());
}
inline vm_mpz * to_mpz_core(vm_obj const & o) { lean_assert(is_mpz(o)); return static_cast<vm_mpz*>(o.raw()); }
inline mpz const & to_mpz(vm_obj const & o) { return to_mpz_core(o)->get_value(); }
inline vm_external * to_external(vm_obj const & o) { lean_assert(is_external(o)); return static_cast<vm_external*>(o.raw()); }
// =======================================

// =======================================
// Accessors
inline unsigned cidx(vm_obj const & o) {
    lean_assert(is_simple(o) || is_constructor(o));
    return LEAN_VM_IS_PTR(o.raw()) ? to_composite(o.raw())->idx() : static_cast<unsigned>(LEAN_VM_UNBOX(o.raw()));
}
inline unsigned csize(vm_obj const & o) { lean_assert(is_composite(o)); return to_composite(o)->size(); }
inline unsigned cfn_idx(vm_obj const & o) { lean_assert(is_closure(o)); return to_composite(o)->idx(); }
inline vm_obj const * cfields(vm_obj const & o) {
    lean_assert(is_composite(o)); return to_composite(o)->fields();
}
inline vm_obj const & cfield(vm_obj const & o, unsigned i) { lean_assert(i < csize(o)); return cfields(o)[i]; }
// =======================================

void display(std::ostream & out, vm_obj const & o);

#define LEAN_MAX_SMALL_NAT 1u<<31

/** \brief VM instruction opcode */<commit_msg>fix(library/vm/vm): memory management<commit_after>/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/
#pragma once
#include <memory>
#include <vector>
#include "util/debug.h"
#include "util/rc.h"
#include "util/numerics/mpz.h"
#include "kernel/environment.h"

namespace lean {
class vm_obj;
enum class vm_obj_kind { Simple, Constructor, Closure, MPZ, External };

/** \brief Base class for VM objects.

    \remark Simple objects are encoded as tagged pointers. */
class vm_obj_cell {
protected:
    MK_LEAN_RC(); // Declare m_rc counter
    vm_obj_kind m_kind;
    void dealloc();
    void dec_ref(vm_obj & o, buffer<vm_obj_cell*> & todelete);
    vm_obj_cell(vm_obj_kind k):m_rc(0), m_kind(k) {}
public:
    vm_obj_kind kind() const { return m_kind; }
};

#define LEAN_VM_IS_PTR(obj) ((reinterpret_cast<size_t>(obj) & 1) == 0)
#define LEAN_VM_BOX(num)    (reinterpret_cast<vm_obj_cell*>((num << 1) | 1))
#define LEAN_VM_UNBOX(obj)  (reinterpret_cast<size_t>(obj) >> 1)

void display(std::ostream & out, vm_obj const & o);

/** \brief VM object */
class vm_obj {
    vm_obj_cell * m_data;
    friend class vm_obj_cell;
    vm_obj_cell * steal_ptr() {
        lean_assert(LEAN_VM_IS_PTR(m_data)); vm_obj_cell * r = m_data; m_data = LEAN_VM_BOX(0); return r;
    }
public:
    vm_obj():m_data(LEAN_VM_BOX(0)) {
        static_assert(sizeof(vm_obj) == sizeof(void *), "unexpected class obj size"); // NOLINT
    }
    explicit vm_obj(unsigned cidx):m_data(LEAN_VM_BOX(cidx)) {}
    explicit vm_obj(vm_obj_cell * c):m_data(c) { m_data->inc_ref(); lean_assert(LEAN_VM_IS_PTR(m_data)); }
    vm_obj(vm_obj const & o):m_data(o.m_data) { if (LEAN_VM_IS_PTR(m_data)) m_data->inc_ref(); }
    vm_obj(vm_obj && o):m_data(o.m_data) { o.m_data = LEAN_VM_BOX(0); }
    ~vm_obj() { if (LEAN_VM_IS_PTR(m_data)) m_data->dec_ref(); }

    friend void swap(vm_obj & a, vm_obj & b) { std::swap(a.m_data, b.m_data); }

    operator vm_obj_cell*() const { return m_data; }

    vm_obj & operator=(vm_obj const & s) {
        if (LEAN_VM_IS_PTR(s.m_data))
            s.m_data->inc_ref();
        vm_obj_cell * new_data = s.m_data;
        if (LEAN_VM_IS_PTR(m_data))
            m_data->dec_ref();
        m_data = new_data;
        return *this;
    }

    vm_obj & operator=(vm_obj && s) {
        if (LEAN_VM_IS_PTR(m_data))
            m_data->dec_ref();
        m_data   = s.m_data;
        s.m_data = LEAN_VM_BOX(0);
        return *this;
    }

    vm_obj_kind kind() const {
        return LEAN_VM_IS_PTR(m_data) ? m_data->kind() : vm_obj_kind::Simple;
    }

    vm_obj_cell * raw() const {
        return m_data;
    }
};

class vm_composite : public vm_obj_cell {
    unsigned   m_idx;
    unsigned   m_size;
    vm_obj * get_field_ptr() {
        return reinterpret_cast<vm_obj *>(reinterpret_cast<char *>(this)+sizeof(vm_composite));
    }
    friend vm_obj_cell;
    void dealloc(buffer<vm_obj_cell*> & todelete);
public:
    vm_composite(vm_obj_kind k, unsigned idx, unsigned sz, vm_obj const * data);
    unsigned size() const { return m_size; }
    unsigned idx() const { return m_idx; }
    vm_obj const * fields() const {
        return reinterpret_cast<vm_obj const *>(reinterpret_cast<char const *>(this)+sizeof(vm_composite));
    }
};

class vm_mpz : public vm_obj_cell {
    mpz      m_value;
    friend vm_obj_cell;
    void dealloc();
public:
    vm_mpz(mpz const & v);
    mpz const & get_value() const { return m_value; }
};

class vm_external : public vm_obj_cell {
public:
    virtual ~vm_external() = 0;
};

// =======================================
// Constructors
vm_obj mk_vm_simple(unsigned cidx);
vm_obj mk_vm_constructor(unsigned cidx, unsigned sz, vm_obj const * args);
vm_obj mk_vm_closure(unsigned fnidx, unsigned sz, vm_obj const * args);
vm_obj mk_vm_mpz(mpz const & n);
vm_obj mk_vm_external(vm_external * cell);
/* helper functions for creating natural numbers */
vm_obj mk_vm_nat(unsigned n);
vm_obj mk_vm_nat(mpz const & n);
inline vm_obj mk_vm_false() { return mk_vm_simple(0); }
inline vm_obj mk_vm_true() { return mk_vm_simple(1); }
inline vm_obj mk_vm_bool(bool b) { return mk_vm_simple(b); }
// =======================================

// =======================================
// Testers
inline vm_obj_kind kind(vm_obj_cell const * o) { return LEAN_VM_IS_PTR(o) ? o->kind() : vm_obj_kind::Simple; }
inline bool is_simple(vm_obj_cell const * o) { return !LEAN_VM_IS_PTR(o); }
inline bool is_constructor(vm_obj_cell const * o) { return kind(o) == vm_obj_kind::Constructor; }
inline bool is_closure(vm_obj_cell const * o) { return kind(o) == vm_obj_kind::Closure; }
inline bool is_composite(vm_obj_cell const * o) { return is_constructor(o) || is_closure(o); }
inline bool is_mpz(vm_obj_cell const * o) { return kind(o) == vm_obj_kind::MPZ; }
inline bool is_external(vm_obj_cell const * o) { return kind(o) == vm_obj_kind::External; }
// =======================================

// =======================================
// Casting
inline vm_composite * to_composite(vm_obj_cell * o) { lean_assert(is_composite(o)); return static_cast<vm_composite*>(o); }
inline vm_mpz * to_mpz_core(vm_obj_cell * o) { lean_assert(is_mpz(o)); return static_cast<vm_mpz*>(o); }
inline mpz const & to_mpz(vm_obj_cell * o) { return to_mpz_core(o)->get_value(); }
inline vm_external * to_external(vm_obj_cell * o) { lean_assert(is_external(o)); return static_cast<vm_external*>(o); }
// =======================================

// =======================================
// Accessors
inline unsigned cidx(vm_obj const & o) {
    lean_assert(is_simple(o) || is_constructor(o));
    return LEAN_VM_IS_PTR(o.raw()) ? to_composite(o.raw())->idx() : static_cast<unsigned>(LEAN_VM_UNBOX(o.raw()));
}
inline unsigned csize(vm_obj const & o) { lean_assert(is_composite(o)); return to_composite(o)->size(); }
inline unsigned cfn_idx(vm_obj const & o) { lean_assert(is_closure(o)); return to_composite(o)->idx(); }
inline vm_obj const * cfields(vm_obj const & o) {
    lean_assert(is_composite(o)); return to_composite(o)->fields();
}
inline vm_obj const & cfield(vm_obj const & o, unsigned i) { lean_assert(i < csize(o)); return cfields(o)[i]; }
// =======================================

#define LEAN_MAX_SMALL_NAT 1u<<31

/** \brief VM instruction opcode */
{'fraction_non_alphanumeric': 0.18144231533752087, 'fraction_numerical': 0.0034984495507672736, 'mean_word_length': 4.435609334485739, 'pattern_counts': {'":': 0, '<': 45, '<?xml version=': 0, '>': 64, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7088121', 'n_tokens_mistral': 4637, 'n_tokens_neox': 4583, 'n_words': 974}