// -*- mode: C++; indent-tabs-mode: nil; c-basic-offset: 4 -*-

/*
 * (c) 2020 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.
 */

#pragma once

#include <brick-smt>
#include <dios.h>


namespace __lava
{
    template< typename >
    using weak_array_adaptor = tagged_array< _VM_PT_Weak >;

    template< typename >
    using marked_array_adaptor = tagged_array< _VM_PT_Marked >;

    template< typename domain, typename base >
    struct expr_ : base, domain_mixin< domain >
    {
        using base::base;

        using ev = domain;
        using er = const domain &;
        using ref = domain_ref< ev >;

        using bw = bitwidth_t;
        using op = brq::smt_op;

        expr_() = default;
        expr_( void *v, __dios::construct_shared_t s ) : base( v, s ) {}

        template< typename imm_t, typename... args_t >
        expr_( const brq::smt_atom_t< imm_t > &o, const args_t & ... args )
            : base()
        {
            base::apply( o, args... );
        }

        static uint16_t array_counter()
        {
            static uint16_t v = 0;
            return ++v;
        }

        template< typename... args_t >
        expr_( const expr_ &o, const args_t & ... args )
            : base()
        {
            base::apply( o, args... );
        }

        static ev cast( er arg, bitwidth_t bw, op o )
        {
            brq::smt_atom_t< uint8_t > atom( o, bw );
            return { arg, atom };
        }

        static ev op_alloca( er size, bitwidth_t bw )
        {
            using array = brq::smt_array_type;

            // TODO get type as argument
            array type{ array_counter(), bw, array::type_t::bitvector };
            return { brq::smt_atom_t( op::array, type ) };
        }

        static ev op_join( er a, er b ) { return { a, b, op::join }; }
        static ev op_meet( er a, er b ) { return { a, b, op::meet }; }

        static ev op_extract( er t, uint8_t from, uint8_t to )
        {
            std::pair arg{ from, to };
            brq::smt_atom_t< std::pair< uint8_t, uint8_t > > atom( op::bv_extract, arg );
            return { t, atom };
        }

        static ev op_not( er a ) { return { a, op::bv_not }; }
        static ev op_neg( er a ) { return { a, op::bv_neg }; }

        static ev op_add ( er a, er b ) { return { a, b, op::bv_add  }; }
        static ev op_sub ( er a, er b ) { return { a, b, op::bv_sub  }; }
        static ev op_mul ( er a, er b ) { return { a, b, op::bv_mul  }; }
        static ev op_sdiv( er a, er b ) { return { a, b, op::bv_sdiv }; }
        static ev op_udiv( er a, er b ) { return { a, b, op::bv_udiv }; }
        static ev op_srem( er a, er b ) { return { a, b, op::bv_srem }; }
        static ev op_urem( er a, er b ) { return { a, b, op::bv_urem }; }

        static ev op_fadd( er a, er b ) { return { a, b, op::fp_add }; }
        static ev op_fsub( er a, er b ) { return { a, b, op::fp_sub }; }
        static ev op_fmul( er a, er b ) { return { a, b, op::fp_mul }; }
        static ev op_fdiv( er a, er b ) { return { a, b, op::fp_div }; }
        static ev op_frem( er a, er b ) { return { a, b, op::fp_rem }; }

        static ev op_shl ( er a, er b ) { return { a, b, op::bv_shl  }; }
        static ev op_ashr( er a, er b ) { return { a, b, op::bv_ashr }; }
        static ev op_lshr( er a, er b ) { return { a, b, op::bv_lshr }; }
        static ev op_and ( er a, er b ) { return { a, b, op::bv_and  }; }
        static ev op_or  ( er a, er b ) { return { a, b, op::bv_or   }; }
        static ev op_xor ( er a, er b ) { return { a, b, op::bv_xor  }; }

        static ev op_eq ( er a, er b ) { return { a, b, op::eq }; };
        static ev op_ne ( er a, er b ) { return { a, b, op::neq }; };
        static ev op_ugt( er a, er b ) { return { a, b, op::bv_ugt }; };
        static ev op_uge( er a, er b ) { return { a, b, op::bv_uge }; };
        static ev op_ult( er a, er b ) { return { a, b, op::bv_ult }; };
        static ev op_ule( er a, er b ) { return { a, b, op::bv_ule }; };
        static ev op_sgt( er a, er b ) { return { a, b, op::bv_sgt }; };
        static ev op_sge( er a, er b ) { return { a, b, op::bv_sge }; };
        static ev op_slt( er a, er b ) { return { a, b, op::bv_slt }; };
        static ev op_sle( er a, er b ) { return { a, b, op::bv_sle }; };

        static ev op_foeq( er a, er b ) { return { a, b, op::fp_oeq }; }
        static ev op_fogt( er a, er b ) { return { a, b, op::fp_ogt }; }
        static ev op_foge( er a, er b ) { return { a, b, op::fp_oge }; }
        static ev op_folt( er a, er b ) { return { a, b, op::fp_olt }; }
        static ev op_fole( er a, er b ) { return { a, b, op::fp_ole }; }
        static ev op_fone( er a, er b ) { return { a, b, op::fp_one }; }
        static ev op_ford( er a, er b ) { return { a, b, op::fp_ord }; }
        static ev op_funo( er a, er b ) { return { a, b, op::fp_uno }; }
        static ev op_fueq( er a, er b ) { return { a, b, op::fp_ueq }; }
        static ev op_fugt( er a, er b ) { return { a, b, op::fp_ugt }; }
        static ev op_fuge( er a, er b ) { return { a, b, op::fp_uge }; }
        static ev op_fult( er a, er b ) { return { a, b, op::fp_ult }; }
        static ev op_fule( er a, er b ) { return { a, b, op::fp_ule }; }
        static ev op_fune( er a, er b ) { return { a, b, op::fp_une }; }

        static ev op_ffalse( er a, er b ) { return { a, b, op::fp_false }; }
        static ev op_ftrue( er a, er b ) { return { a, b, op::fp_true }; }

        static ev op_trunc  ( er a, bw w ) { return cast( a, w, op::bv_trunc ); }
        static ev op_fptrunc( er a, bw w ) { return cast( a, w, op::fp_trunc ); }
        static ev op_sitofp ( er a, bw w ) { return cast( a, w, op::bv_stofp ); }
        static ev op_uitofp ( er a, bw w ) { return cast( a, w, op::bv_utofp ); }
        static ev op_zext   ( er a, bw w ) { return cast( a, w, op::bv_zext ); }
        static ev op_zfit   ( er a, bw w ) { return cast( a, w, op::bv_zfit ); }
        static ev op_sext   ( er a, bw w ) { return cast( a, w, op::bv_sext ); }
        static ev op_fpext  ( er a, bw w ) { return cast( a, w, op::fp_ext ); }
        static ev op_fptosi ( er a, bw w ) { return cast( a, w, op::fp_tosbv ); }
        static ev op_fptoui ( er a, bw w ) { return cast( a, w, op::fp_toubv ); }

        template< typename value >
        static void op_store_at( ref arr, ref off, const value &v, bw w )
        {
            if constexpr ( std::is_same_v< value, ev > )
            {
                brq::smt_atom_t< uint8_t > atom{ op::store, w };
                arr.apply( off, v, atom ); // perform inplace store
            }
            else
            {
                __dios_trace_f( "unsupported store %s", __PRETTY_FUNCTION__ );
                __builtin_trap();
            }
        }

        static ev op_load_at( er arr, er off, bw w )
        {
            brq::smt_atom_t< uint8_t > atom( op::load, w );
            return { arr, off, atom };
        }

        static ev op_concat ( er a, er b ) { return { a, b, op::bv_concat }; }
    };
}