#pragma once

#include "base.hpp"
#include "constant.hpp"
#include "tristate.hpp"

#include <sys/divm.h>

#include <limits>

// This domain can be used within SHOOP as a tool for data dependence analysis. We can hand
// out up to 64 "trackers" — abstract values that have their own distinct identity — using
// 'idtrack::any'. Anytime two tracked values are combined in an operation that produces
// another value, the new value remembers the original trackers it came from.
//
// Example:
//
// int foo( int a, int b, int c )
// {
//     int d = a + b;
//     return d;
// }
//
// We can call 'foo' with three abstract values of domain 'idtrack' created using 'any'.
// The value 'd' will remember that it has data dependency on 'a' and 'b', but not 'c'.
//
// See also:
// - dios/lava/unit.hpp
// - dios/lava/silencing-unit.hpp
// - dios/lamp/shoop.cpp

namespace __lava
{
    // The amount of currently tracked values. We can hand out at most 64 of them.
    inline uint8_t __tracked_values = 0;

    // From an implementation standpoint, each value holds a 64 bit bitset. 'any' produces
    // a value with a single unit and 63 zeroes. Requesting more than 64 value results
    // in a fault. Any binary operation results in a bit sum.
    struct idtrack : tagged_storage< uint64_t >, domain_mixin< idtrack >
    {
        using id = uint64_t;
        using cr = const idtrack &;

        idtrack( id i )
            : tagged_storage< id >( i )
        {}

        idtrack( void *v, __dios::construct_shared_t s )
            : tagged_storage< id >( v, s )
        {}

        idtrack clone() const
        {
            return idtrack( this->get() );
        }

        template < typename type >
        static idtrack lift( const type& ) { return { 0 }; }
        static idtrack lift( cr i ) { return i.clone(); }

        static constant lower( cr ) { fail(); }

        template < typename type >
        static idtrack any()
        {
            if ( __tracked_values == sizeof( id ) * 8 )
            {
                fail( "cannot give out more than 64 unique IDs" );
                return { 0 };
            }

            return { static_cast< id >( 1 ) << (__tracked_values++) };
        }

        static void assume( cr, bool ) { }

        static tristate to_tristate( cr a )
        {
            // On every branch, we are tracing the tracked value of the value on which we branch.
            // This allows us to determine the tracker value of every value that was branched on
            // (since we can access trace data from a counterexample provided by Divine).
            // This information can be used to determine the parameters on which the error
            // dependens.

            auto sb = brq::string_builder();
            sb << "IDTRACK ";
            sb << a.get();

            // We don't want OOM when constructing the string.
            if ( sb.truncated() )
                __vm_cancel();

            __vm_trace( _VM_T_Text, sb.data() );

            return brq::maybe;
        }

        static idtrack combine( cr a, cr b )
        {
            return { a.get() | b.get() };
        }

        // We don't need to worry about memory operations yet.

        // template< typename size >
        // static idtrack op_alloca( const size&, uint8_t ) { return {}; }

        // static idtrack op_load( cr, uint8_t ) { return {}; }
        // static idtrack op_load_at( cr, cr, uint8_t ) { return {}; }

        // template< typename scalar >
        // static idtrack op_store( cr, scalar, uint8_t ) { return {}; }

        /* arithmetic operations */
        static idtrack op_add ( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_fadd( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_sub ( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_fsub( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_mul ( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_fmul( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_udiv( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_sdiv( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_fdiv( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_urem( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_srem( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_frem( cr a, cr b ) { return combine( a, b ); }

        static idtrack op_fneg( cr a ) { return a.clone(); }

        /* bitwise operations */
        static idtrack op_shl ( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_lshr( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_ashr( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_and ( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_or  ( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_xor ( cr a, cr b ) { return combine( a, b ); }

        using bw = uint8_t;

        /* comparison operations */
        static idtrack op_foeq( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_fogt( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_foge( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_folt( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_fole( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_fone( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_ford( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_funo( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_fueq( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_fugt( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_fuge( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_fult( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_fule( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_fune( cr a, cr b ) { return combine( a, b ); }

        static idtrack op_eq ( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_ne ( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_ugt( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_uge( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_ult( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_ule( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_sgt( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_sge( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_slt( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_sle( cr a, cr b ) { return combine( a, b ); }

        static idtrack op_ffalse( cr a, cr b ) { return combine( a, b ); }
        static idtrack op_ftrue ( cr a, cr b ) { return combine( a, b ); }

        static idtrack op_fpext   ( cr a, bw ) { return a.clone(); }
        static idtrack op_fptosi  ( cr a, bw ) { return a.clone(); }
        static idtrack op_fptoui  ( cr a, bw ) { return a.clone(); }
        static idtrack op_fptrunc ( cr a, bw ) { return a.clone(); }
        static idtrack op_inttoptr( cr a, bw ) { return a.clone(); }
        static idtrack op_ptrtoint( cr a, bw ) { return a.clone(); }
        static idtrack op_sext    ( cr a, bw ) { return a.clone(); }
        static idtrack op_sitofp  ( cr a, bw ) { return a.clone(); }
        static idtrack op_trunc   ( cr a, bw ) { return a.clone(); }
        static idtrack op_uitofp  ( cr a, bw ) { return a.clone(); }
        static idtrack op_zext    ( cr a, bw ) { return a.clone(); }
        static idtrack op_zfit    ( cr a, bw ) { return a.clone(); }

        // op_release, op_dealloca are empty as a workaround of a double-free bug when calling
        // __lamp_twin with this domain
        // TODO: Delete once this has been properly addressed
        static void op_release( cr ) {}
        static void op_dealloca( cr ) {}
    };
} // namespace __lava