#include <shoop/common.hpp>
#include <shoop/analyser.hpp>

#include <brick-fs>
#include <brick-cmd>

#include <iostream>
#include <string_view>

constexpr std::string_view shoop_help =
    "SHOOP is a prototype implementation of an incomplete-program analyser.\n"
    "Given an LLVM module, it traverses the functions in that module and\n"
    "computes their preconditions, writing them out in standard SMT-LIB format.\n"
    "By default, it uses several methods meant as means of optimisation, but\n"
    "those can be disabled at will (see help for the `check` command).\n\n"
    "Note that it supports only modules working with scalar data, that is\n"
    "integers and floating-point numbers. It also cannot handle recursion and\n"
    "loops with unknown upper bound on the number of iterations at the moment.";

constexpr std::string_view check_help =
    "Analyse the given LLVM bitcode module, that is compute function\n"
    "preconditions.\n\n"
    "Note that at the moment, the given file must be a compiled bitcode module\n"
    "generated by a compatible Clang (that is Clang 7.0, which is built\n"
    "together with DIVINE).";

struct command : brq::cmd_base
{
    virtual void setup() {}
    virtual void cleanup() {}
    virtual ~command() {}
};

struct check : command
{
    // TODO: We probably also want to compile c++ files.
    brq::cmd_file _input_file;              // The input bitcode that we are to check.
    brq::cmd_path _dump_dir;                // The directory where we can dump constructed bitcode modules.
    brq::cmd_flag _divine_log;              // Should we print divine output?
    brq::cmd_flag _no_precondition_asserts; // Disable fast-fail asserts made from computed preconditions.
    brq::cmd_flag _no_lattice_climb;        // Disable unit/sunit lattice climb, run f(term, term, term) for every function
    brq::cmd_flag _no_callgraph;            // Disable callgraph traversal, verify only outermost functions

    void options( brq::cmd_options &c ) override
    {
        command::options( c ); // This basically just adds --help from brq::cmd_base::options.

        c.opt( "--dump", _dump_dir )
            << "dump generated bitcode modules in the specified directory WARNING: lots of large files";
        c.opt( "--divine-log", _divine_log )
            << "print output of DIVINE interleaved with standard SHOOP log";
        c.opt( "--no-precondition-asserts", _no_precondition_asserts )
            << "disable inserting of assert(pre) with computed preconditions";
        c.opt( "--terms-only", _no_lattice_climb )
            << "disable SHOOP lattice climbing algorithm, run every analysed function with terms only";
        c.opt( "--outermost-calls-only", _no_callgraph )
            << "disable compositional callgraph analysis, check only outermost nodes of the callgraph";

        c.pos( _input_file, true );
    }

    std::string_view help() override { return check_help; }

    void setup() override
    {
        if ( _dump_dir.name != "" )
            brq::create_dir( _dump_dir.name );
    }

    void run() override
    {
        const auto *const tested_file_path = _input_file.name.c_str();

        std::cout << "SHOOP running..." << std::endl;

        auto opts = shoop::analyser_opts{};

        if ( _dump_dir.name != "" )
            opts.dump_to( _dump_dir.name );
        if ( _divine_log )
            opts.enable_divine_log();
        if ( _no_precondition_asserts )
            opts.no_preconditions();
        if ( _no_lattice_climb )
            opts.no_lattice_climb();
        if ( _no_callgraph )
            opts.outer_calls_only();

        auto analyser = shoop::make_analyser( tested_file_path, std::move( opts ) );
        analyser->run();
    }
};

int main( int argc, char **argv ) try
{
    auto parser = brq::cmd_parser( argc, argv, shoop_help );
    auto cmd = parser.parse< check >();

    cmd.match(
        [ & ]( brq::cmd_help &help )
        {
            help.run();
        },
        [ & ]( command &c )
        {
            c.setup();
            c.run();
            c.cleanup();
        }
    );

    return 0;
}
catch ( brq::error &e )
{
    std::cerr << "ERROR:\n" << e.what() << std::endl;
    return e._exit;
}
catch ( brq::assert_failed &e )
{
    std::cerr << "Assert failed: " << e.what() << std::endl;
    return 0;
}