/*
 * (c) 2017 Vladimír Štill <xstill@fi.muni.cz>
 * (c) 2018 Petr Ročkai <code@fixp.eu>
 * (c) 2018 Henrich Lauko <xlauko@mail.muni.cz>
 *
 * Permission to use, copy, modify, and distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 */

/*
 * This file defines the interface between various lart-provided program
 * transformations and their runtime support code (which resides in dios/pts).
 */

#ifndef _SYS_LART_H_
#define _SYS_LART_H_

#ifdef __divine__
#include <sys/divm.h>
#include <dios.h>
#else
#include <divine/vm/divm.h>
#include <stdexcept>
#include <brick-types>
#endif

#if __cplusplus >= 201402L
#include <type_traits>
#include <limits>

namespace lart::weakmem
{

    enum class MemoryOrder : uint8_t
    {
        NotAtomic = 0,
        Unordered  = (1 << 0),
        Monotonic  = (1 << 1) | Unordered,
        Acquire    = (1 << 2) | Monotonic,
        Release    = (1 << 3) | Monotonic,
        AcqRel     = Acquire | Release,
        SeqCst     = (1 << 4) | AcqRel,
        AtomicOp   = (1 << 5),
        WeakCAS    = (1 << 6),
    };

    inline MemoryOrder operator|( MemoryOrder a, MemoryOrder b )
    {
        using uint = typename std::underlying_type< MemoryOrder >::type;
        return MemoryOrder( uint( a ) | uint( b ) );
    }

    inline MemoryOrder operator&( MemoryOrder a, MemoryOrder b )
    {
        using uint = typename std::underlying_type< MemoryOrder >::type;
        return MemoryOrder( uint( a ) & uint( b ) );
    }

    inline bool subseteq( MemoryOrder a, MemoryOrder b )
    {
        return a == (a & b);
    }

}

namespace lart::sym
{

    using VarID = int32_t;

    using RefCount = uint8_t;

    enum class Op : uint8_t
    {
        Invalid,

        Variable,
        Constant,

        BitCast, FirstUnary = BitCast,

        SExt,
        ZExt,
        Trunc,

        IntToPtr,
        PtrToInt,

        FPExt,
        FPTrunc,
        FPToSInt,
        FPToUInt,
        SIntToFP,
        UIntToFP,

        BoolNot,
        Extract, LastUnary = Extract,

        Add, FirstBinary = Add,
        Sub,
        Mul,
        UDiv,
        SDiv,
        URem,
        SRem,

        FpAdd,
        FpSub,
        FpMul,
        FpDiv,
        FpRem,

        Shl,
        LShr,
        AShr,
        And,
        Or,
        Xor,

        // Icmp
        EQ,
        NE,
        UGT,
        UGE,
        ULT,
        ULE,
        SGT,
        SGE,
        SLT,
        SLE,

        // Fcmp
        FpFalse, // no comparison, always returns false
        FpOEQ,   // ordered and equal
        FpOGT,   // ordered and greater than
        FpOGE,   // ordered and greater than or equal
        FpOLT,   // ordered and less than
        FpOLE,   // ordered and less than or equal
        FpONE,   // ordered and not equal
        FpORD,   // ordered (no nans)
        FpUEQ,   // unordered or equal
        FpUGT,   // unordered or greater than
        FpUGE,   // unordered or greater than or equal
        FpULT,   // unordered or less than
        FpULE,   // unordered or less than or equal
        FpUNE,   // unordered or not equal
        FpUNO,   // unordered (either nans)
        FpTrue,  // no comparison, always returns true
        Constraint, // behaves as binary logical and

        Concat, LastBinary = Concat,
    };

    struct Type
    {
        enum T : uint8_t
        {
            Int,
            Float
        };

        static const int bwmask = 0x7fff;

        Type() = default;
        Type( T g, int bitwidth ) : _data( (g << 15) | bitwidth ) { }

        T type() { return T( _data >> 15 ); }
        int bitwidth() { return _data & bwmask; }
        void bitwidth( int x ) {
            _data &= ~bwmask;
            _data |= bwmask & x;
        }

        uint16_t _data;
    };

    static_assert( sizeof( VarID ) == 4, "" );
    static_assert( sizeof( Type ) == 2, "" );

    struct Variable {
        Variable( Type type, VarID id ) :
            op( Op::Variable ), refcount( 0 ), type( type ), id( id )
        { }

        Op op;              // 8B
        RefCount refcount;  // 8B
        Type type;          // 16B
        VarID id;           // 32B
    };

    static_assert( sizeof( Variable ) == 8, "" );

    union ValueU {
        //    ValueT raw;
        uint8_t i8;
        uint16_t i16;
        uint32_t i32;
        uint64_t i64;
        float fp32;
        double fp64;
        //    long double fp80;
    };

    struct Constant {
        Constant( Type type, uint64_t value ) :
            op( Op::Constant ), refcount( 0 ), type( type ), value( value )
        { }

        Op op;            // 8B
        RefCount refcount;// 8B
        Type type;        // 16B
        uint64_t value;
        //    std::array< uint32_t, 3 > value; // 96B - enough to hold long double
    };

    static_assert( sizeof( Constant ) == 16, "" );

    union Formula;

#ifdef __divine__
    static inline void refcount_increment( Formula * ptr );
#endif

    template< typename Formula >
    struct Unary_ {
        Unary_( Op op, Type t, Formula child ) :
            op( op ), refcount( 0 ), type( t ), child( child )
        {
#ifdef __divine__
            refcount_increment( child );
#endif
        }

        Unary_( Op op, Type t, unsigned short from, unsigned short to, Formula child ) :
            op( op ), refcount( 0 ), type( t ), from( from ), to( to ), child( child )
        {
#ifdef __divine__
            refcount_increment( child );
#endif
        }

        Op op;                   // 8B
        RefCount refcount;       // 8B
        Type type;               // 16B
        unsigned short from, to; // 32B, only for Extract
        Formula child;           // 64B
    };

    static_assert( sizeof( Unary_< void * > ) == 16, "" );

    template< typename Formula >
    struct Binary_ {
        Binary_( Op op, Type t, Formula left, Formula right ) :
            op( op ), type( t ), refcount( 0 ), left( left ), right( right )
        {
#ifdef __divine__
            refcount_increment( left );
            refcount_increment( right );
#endif
        }

        Op op;            // 8B
        RefCount refcount;// 8B
        Type type;        // 16B
        Formula left;     // 64B
        Formula right;    // 64B
    };

    static_assert( sizeof( Binary_< void * > ) == 24, "" );

    union Formula;

#ifdef __divine__
    using Binary = Binary_< Formula * >;
    using Unary = Unary_< Formula * >;
#else
    using Unary = Unary_< divine::vm::HeapPointer >;
    using Binary = Binary_< divine::vm::HeapPointer >;
#endif

    union Formula
    {
        Formula() : hdr{ Op::Invalid, 0, Type() } { }

        struct
        {
            Op op;                   // 8B
            RefCount refcount;       // 8B
            Type type;               // 16B
        } hdr;

        Op op() const { return hdr.op; }
        RefCount refcount() const { return hdr.refcount; }
        Type type() const { return hdr.type; }

        void refcount_increment() {
            if ( hdr.refcount != std::numeric_limits<RefCount>::max() )
                ++hdr.refcount;
        }

        void refcount_decrement() {
            if ( hdr.refcount != std::numeric_limits<RefCount>::max() )
                --hdr.refcount;
        }

        Variable var;
        Constant con;
        Unary unary;
        Binary binary;
    };

#ifdef __divine__
    __invisible static inline void refcount_increment( Formula * ptr ) {
        if ( ptr )
            ptr->refcount_increment();
    }
#endif

    inline bool isConstant( Op x ) { return x == Op::Constant; }
    inline bool isConstant( Formula * f ) { return isConstant( f->op() ); }

    inline bool isVariable( Op x ) { return x == Op::Variable; }
    inline bool isVariable( Formula * f ) { return isVariable( f->op() ); }

    inline bool isUnary( Op x ) { return x >= Op::FirstUnary && x <= Op::LastUnary; }
    inline bool isUnary( Formula * f ) { return isUnary( f->op() ); }

    inline bool isBinary( Op x ) { return x >= Op::FirstBinary && x <= Op::LastBinary; }
    inline bool isBinary( Formula * f ) { return isBinary( f->op() ); }
}
#endif

#ifdef __cplusplus
extern "C" {
#endif

// there are 16 flags reserved for transformations, see <sys/divm.h>
static const uint64_t _LART_CF_RelaxedMemRuntime  = _VM_CFB_Transform << 0;
static const uint64_t _LART_CF_RelaxedMemCritSeen = _VM_CFB_Transform << 1;

enum __lart_termsec_kind {
    __lart_termsec_kind_none         = 0,
    __lart_termsec_kind_critical     = 1 << 0,
    __lart_termsec_kind_mutex_wait   = 1 << 1,
    __lart_termsec_kind_cond_wait    = 1 << 2,
    __lart_termsec_kind_barrier_wait = 1 << 3,
    __lart_termsec_kind_join         = 1 << 4,
    __lart_termsec_kind_function     = 1 << 5,
    __lart_termsec_kind_user_excl    = 1 << 6,
    __lart_termsec_kind_user_wait    = 1 << 7,
};

#define _LART_UNUSED __attribute__((__unused__))

__attribute__((__noinline__, __weak__, __nothrow__))
void __lart_termsec_begin( _LART_UNUSED enum __lart_termsec_kind kind,
                       _LART_UNUSED void *obj,
                       _LART_UNUSED void *thr )
#if __cplusplus >= 201103L
    noexcept
#endif
{ }

__attribute__((__noinline__, __weak__, __nothrow__))
void __lart_termsec_end( _LART_UNUSED enum __lart_termsec_kind kind,
                     _LART_UNUSED void *obj,
                     _LART_UNUSED void *thr )
#if __cplusplus >= 201103L
    noexcept
#endif
{ }

#ifdef __cplusplus
}
#endif

#if __cplusplus > 201402L
namespace lart::nontermination {

enum class NonterminationMode : uint32_t
{
    None            = 0,
    CriticalSection = __lart_termsec_kind_critical,
    MutexWait       = __lart_termsec_kind_mutex_wait,
    ConditionWait   = __lart_termsec_kind_cond_wait,
    BarrierWait     = __lart_termsec_kind_barrier_wait,
    ThreadJoin      = __lart_termsec_kind_join,
    FuntionEnd      = __lart_termsec_kind_function,
    UserExclusive   = __lart_termsec_kind_user_excl,
    UserWait        = __lart_termsec_kind_user_wait,
    Local           = CriticalSection | MutexWait | ConditionWait | BarrierWait | ThreadJoin | FuntionEnd | UserExclusive | UserWait,
    Global          = UserWait << 1
};

inline const char *show_kind( __lart_termsec_kind kind ) noexcept
{
    switch ( kind ) {
        case __lart_termsec_kind_critical: return "critical section";
        case __lart_termsec_kind_mutex_wait: return "wait for mutex lock";
        case __lart_termsec_kind_cond_wait: return "condition variable waiting";
        case __lart_termsec_kind_barrier_wait: return "barrier waiting";
        case __lart_termsec_kind_function: return "function return";
        case __lart_termsec_kind_join: return "thread join";
        case __lart_termsec_kind_user_excl: return "user-defined exclusive section";
        case __lart_termsec_kind_user_wait: return "user-defined wait";
        case __lart_termsec_kind_none: return "ERROR (no kind)";
    }
}

#ifndef __divine__
inline std::string to_string( NonterminationMode nm, bool verbose = false ) noexcept
{
    if ( nm == NonterminationMode::None )
        return "none";
    if ( nm == NonterminationMode::Global )
        return "global";
    if ( nm == NonterminationMode::Local && !verbose )
        return "local";

    std::stringstream ss;
    brick::types::StrongEnumFlags< NonterminationMode > flags( nm );
    auto add = [&, sep = ""]( NonterminationMode part, const char *name ) mutable
        {
            if ( flags.has( part ) )
            {
                ss << sep << name;
                sep = ", ";
                flags ^= part;
            }
        };

    add( NonterminationMode::CriticalSection, "critical" );
    add( NonterminationMode::MutexWait, "mutex-wait" );
    add( NonterminationMode::ConditionWait, "condition-wait" );
    add( NonterminationMode::BarrierWait, "barrier-wait" );
    add( NonterminationMode::ThreadJoin, "thread-join" );
    add( NonterminationMode::FuntionEnd, "function-end" );
    add( NonterminationMode::UserExclusive, "user-exclusive" );
    add( NonterminationMode::UserWait, "user-wait" );

    ASSERT_EQ( flags.getUnderlying(), uint32_t( 0 ) );

    return ss.str();
}

inline NonterminationMode read_nonterm( std::string val )
{
    if ( val == "local" )
        return NonterminationMode::Local;
    if ( val == "global" )
        return NonterminationMode::Global;

    auto read_single = []( const std::string &str ) -> NonterminationMode
    {
        for ( uint32_t it = 1; it & uint32_t( NonterminationMode::Local ); it <<= 1 )
        {
            auto mode = NonterminationMode( it );
            if ( str == to_string( mode ) )
                return mode;
        }
        throw std::invalid_argument( "invalid nontermination mode: " + str +
                                     ", expecting one of " +
                                     to_string( NonterminationMode::Local, true ) );
    };

    brick::types::StrongEnumFlags< NonterminationMode > out;
    for ( std::string match : brick::string::splitStringBy( val, "[\t ]*,[\t ]*" ) )
    {
        if ( match == "local" )
        {
            out |= NonterminationMode::Local;
        }
        else if ( match[0] == '!' || match[0] == '~' )
        {
            match.erase( match.begin() );
            out.clear( read_single( match ) );
        } else
            out |= read_single( match );
    }
    return out.get();
}
#endif // !__divine__

} // namespace lart::termsec
#endif // C++ > 14

#endif // _SYS_LART_H_