Goose  Artifact [21c98da94c]

Artifact 21c98da94c9ec3b497319e2a04571e375952a141cf1176e6abb85fb2effdeb6b:

  • File bs/eir/value.h — part of check-in [914b2e2af1] at 2023-07-05 22:01:09 on branch trunk — Some builtins to work with references during verification:
    • RefToAddr conversion function
    • dot operator overloads to extract the lifetime, origin and path of an address
    (user: zlodo size: 4785)

#ifndef GOOSE_EIR_VALUE_H
#define GOOSE_EIR_VALUE_H

namespace goose::cir
{
    class Instruction;
    using InstrSeq = list< Instruction >;
}

namespace goose::eir
{
    class Value;
    class ValuePattern;

    extern const Term& TypeType();

    extern Term ValueToEIR( const Value& v );
    extern optional< Value > EIRToValue( const Term& t );

    extern Term ValueToEIR( const ValuePattern& v );
    extern optional< ValuePattern > EIRToValuePattern( const Term& t );

    class Value
    {
        public:
            Value() = default;

            template< typename T, typename VL >
            Value( T&& type, VL&& valOrCIR, LocationId loc = LocationId() ) :
                m_type( forward< T >( type ) ),
                m_valOrCIR( forward< VL >( valOrCIR ) ),
                m_locationId( loc )
            {}

            const auto& type() const { return m_type; }
            const auto& payload() const { return m_valOrCIR; }
            const auto& val() const { return get< Term >( m_valOrCIR ); }

            auto& type() { return m_type; }
            auto& val() { return get< Term >( m_valOrCIR ); }

            const ptr< cir::InstrSeq >& cir() const
            {
                static ptr< cir::InstrSeq > null;

                const auto* ppCir = get_if< ptr< cir::InstrSeq > >( &m_valOrCIR );
                if( !ppCir )
                    return null;

                return *ppCir;
            }

            ptr< cir::InstrSeq >& cir()
            {
                static ptr< cir::InstrSeq > null;

                auto* ppCir = get_if< ptr< cir::InstrSeq > >( &m_valOrCIR );
                if( !ppCir )
                    return null;

                return *ppCir;
            }

            template< typename T >
            void setCIR( T&& pInstrSeq )
            {
                m_valOrCIR = forward< T >( pInstrSeq );
            }

            auto locationId() const { return m_locationId; }
            auto&& setLocationId( LocationId id )
            {
                if( !m_locationId.isPoison() )
                    m_locationId = id;
                return *this;
            }

            bool isPoison() const { return m_locationId.isPoison(); }
            auto&& setPoison() { m_locationId.setPoison(); return *this; }

            bool isConstant() const { return holds_alternative< Term >( m_valOrCIR ); }
            bool isType() const;
            bool isMetaType() const;

            friend ostream& operator<<( ostream& out, const Value& val )
            {
                return out << ValueToEIR( val );
            }

            bool operator==( const Value& rhs ) const
            {
                return m_type == rhs.m_type && m_valOrCIR == rhs.m_valOrCIR;
            }

            bool operator!=( const Value& rhs ) const
            {
                return m_type != rhs.m_type || m_valOrCIR != rhs.m_valOrCIR;
            }

            bool operator<( const Value& rhs ) const
            {
                if( m_type != rhs.m_type )
                    return m_type < rhs.m_type;
                return m_valOrCIR < rhs.m_valOrCIR;
            }

        private:
            Term m_type;
            variant< Term, ptr< cir::InstrSeq > > m_valOrCIR;
            LocationId m_locationId = LocationId::Poison();
    };

    class ValuePattern
    {
        public:
            template< typename S, typename T, typename V >
            ValuePattern( S&& sort, T&& type, V&& v, LocationId locationId = LocationId() ) :
                m_sort( forward< T >( sort ) ),
                m_type( forward< T >( type ) ),
                m_val( forward< V >( v ) ),
                m_locationId( locationId )
            {}

            auto locationId() const { return m_locationId; }
            auto&& setLocationId( LocationId id )
            {
                if( !m_locationId.isPoison() )
                    m_locationId = id;
                return *this;
            }

            bool isPoison() const { return m_locationId.isPoison(); }
            void setPoison() { m_locationId.setPoison(); }

            const auto& sort() const { return m_sort; }
            const auto& type() const { return m_type; }
            const auto& val() const { return m_val; }

            auto& sort() { return m_sort; }
            auto& type() { return m_type; }
            auto& val() { return m_val; }

        private:
            Term m_sort;
            Term m_type;
            Term m_val;

            LocationId m_locationId = 0;
    };

    // A generic poisoned value of "type" type.
    extern const Value& PoisonType();

    // A generic poisoned value of "poisontype" type.
    extern const Value& PoisonValue();

    using ValueVec = llvm::SmallVector< Value, 4 >;
}

#endif