#pragma once

#include "common.hpp"
#include "lattice_climb.hpp"
#include "smt.hpp"

#include <string>
#include <vector>
#include <deque>
#include <optional>

#include <divine/mc/bitcode.hpp>

DIVINE_RELAX_WARNINGS
#include <llvm/IR/Function.h>
DIVINE_UNRELAX_WARNINGS

namespace shoop
{

// Should we analyse the whole module function by function in topological ordering,
// or just the outermost functions and let failures happen "down the call stack"?
enum class module_strategy
{
    topsort_traversal,
    outer_only
};

// For every analysed function `f`, should we run the whole SHOOP unit/sunit lattice
// climb algorithm, or just try `f(term, term, term)` and call it a day?
enum class function_strategy
{
    lattice_climb,
    terms_only
};

struct analyser_opts
{
    std::optional< std::string > _dump_dir; // No dumping if nullopt.
    bool                         _divine_log           = false;
    bool                         _insert_preconditions = true;
    module_strategy              _traversal_strategy   = module_strategy::topsort_traversal;
    function_strategy            _analyser_strategy    = function_strategy::lattice_climb;

    auto &dump_to          ( std::string d ) { _dump_dir             = std::move( d );                return *this; }
    auto &enable_divine_log()                { _divine_log           = true;                          return *this; }
    auto &no_preconditions ()                { _insert_preconditions = false;                         return *this; }
    auto &outer_calls_only ()                { _traversal_strategy   = module_strategy::outer_only;   return *this; }
    auto &no_lattice_climb ()                { _analyser_strategy    = function_strategy::terms_only; return *this; }
};

struct divine_result
{
    bool found_error;
    formula path_condition;
};

struct function_analyser;

// An abstract module analyser.
struct module_analyser
{
    ctx_ptr _context;
    mod_ptr _module;

    analyser_opts _opts;

    // The queue of functions ordered by dependencies.
    std::deque< llvm::Function * > _functions;

    module_analyser( ctx_ptr context, mod_ptr module, analyser_opts opts )
        : _context{ context }, _module{ std::move( module ) }, _opts{ std::move( opts ) }
    {
        ASSERT( _context );
        ASSERT( _module );
    }

    virtual ~module_analyser() = default;

    void run();

    virtual void load_function_queue() = 0;

    // At the moment, we only support functions with simple enough signatures — parameter types and the
    // return type must be scalar types, i.e. 8, 16, 32 or 64 bit (signer or unsigned) integers, floats
    // doubles and void. Functions also must have a fixed number of parameters not greater than 64.
    //
    // Go through '_functions' and return all functions that have a signatures we do not support.
    void check_unsupported_functions() const;

    void analyse_queue();

    std::unique_ptr< function_analyser > make_analyser( const llvm::Function &fun ) const;

    // If _dump_dir is set, dump the module in 'bc' to '_dump_dir/file_name'.
    void dump( const divine::mc::BitCode &bc, const std::string &file_name ) const;

    // Changes the analyzed module in the following way:
    // Original module (when verifying `fun`):
    //     T_0 fun( T_1 x_1, T_2 x_2, ... ) { `fun code` }
    // New module:
    //     T_0 fun( T_1 x_1, T_2 x_2, ... ) { ASSERT( `pre` ); `fun code` }
    void insert_precondition_assert( llvm::Function *fun, const formula &pre );
};

struct topsort_analyser : module_analyser
{
    using module_analyser::module_analyser;

    // Order the functions in the tested module by dependencies, that is, return
    // the topological order of the functions.
    // TODO: We also need to work with recursive and mutually recursive funcions,
    // so we need to decompose the callgraph and verify whole components at once.
    void load_function_queue() override;
};

struct outer_only_analyser : module_analyser
{
    using module_analyser::module_analyser;

    // Return only the functions on which no other function in the module depends
    // (in arbitrary order).
    void load_function_queue() override;
};

std::unique_ptr< module_analyser > make_analyser( const char *path, analyser_opts opts );

// An abstract function analyser. Owned by a module analyser, analyses a single function.
struct function_analyser
{
    const module_analyser *_owner;
    const llvm::Function *_function;

    // Dump file counter, so we won't override previous dumps of the same function/node
    // combination, but with different precondition.
    size_t _dump_no = 0;

    function_analyser( const module_analyser &owner, const llvm::Function &function )
        : _owner{ &owner }, _function{ &function }
    {}

    virtual ~function_analyser() = default;

    void dump( const divine::mc::BitCode &bc, const std::string &file_name );

    // Find the weakest precondition that guarantees the function is error-free.
    virtual formula run() = 0;

    // For a given node in the invocation latice (e.g. (+, +, -)) and a given precondition,
    // find whether there is an error reachable in the function under test.
    // This actually runs Divine, whoa.
    divine_result find_error( const invocation_lattice_node &param_domains, const formula &precondition );
};

struct lattice_climb_analyser : function_analyser
{
    using function_analyser::function_analyser;

    formula run() override;
};

struct all_terms_analyser : function_analyser
{
    using function_analyser::function_analyser;

    formula run() override;
};

}