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

/*
 * (c) 2017, 2022 Petr Ročkai <code@fixp.eu>
 *
 * 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.
 */

#include <divine/ui/cli.hpp>
#include <divine/ui/parser.hpp>
#include <divine/mc/trace.hpp>
#include <divine/sim/cli.hpp>

#include <iostream>
#include <vector>
#include <brick-string>
#include <brick-types>
#include <brick-cmd>
#include <brick-fs>

namespace divcheck
{
    using namespace divine;

    struct wrong : std::runtime_error
    {
        using std::runtime_error::runtime_error;
    };

    struct wrong_result   : wrong { using wrong::wrong; };
    struct wrong_location : wrong { using wrong::wrong; };
    struct wrong_stack    : wrong { using wrong::wrong; };
    struct wrong_trace    : wrong { using wrong::wrong; };
    struct wrong_sim      : wrong { using wrong::wrong; };

    struct expectation : ui::LogSink
    {
        virtual void check( const ui::with_report &, const std::string & ) {}
        virtual void check( const ui::sim &, const std::string & ) {}
        virtual void check( const brq::cmd_base &, const std::string & ) {}
        virtual void setup() {};
    };

    struct expect_result : expectation
    {
        bool _ok;
        mc::Result _result = mc::Result::None;

        void setup() override
        {
            _ok = false;
        }

        void check( const ui::with_report &, const std::string & cmd ) override
        {
            if ( !_ok )
                brq::raise< wrong_result >() << cmd << " failed [result]";
        }

        void result( mc::Result r, const mc::Trace & ) override
        {
            _ok = _result == mc::Result::None || r == _result;
        }
    };

    struct expect_location : expectation
    {
        bool _found, _on_inactive;
        std::string _location, _symbol, _comment;

        void setup() override
        {
            _found = false;
            _on_inactive = false;
        }

        void check( const ui::with_report &, const std::string & cmd ) override
        {
            if ( _location.empty() && _symbol.empty() && _comment.empty() )
                return;
            if ( !_found )
                brq::raise< wrong_location >() << cmd << " failed [location]";
            if ( _on_inactive )
                brq::raise< wrong_stack >() << cmd << " failed [location, match on an inactive stack]";
        }

        void backtrace( ui::DbgContext &ctx, int ) override
        {
            if ( _location.empty() && _symbol.empty() && _comment.empty() )
                return;

            bool active = true;
            auto comment = "/* " + _comment + " */";

            auto bt = [&]( int ) { active = false; };
            auto chk = [&]( auto dn )
            {
                if ( !_location.empty() && dn.attribute( "location" ) == _location ||
                     !_symbol.empty() && dn.attribute( "symbol" ).find( _symbol ) != std::string::npos ||
                     !_comment.empty() && dn.source_line().find( comment ) != std::string::npos )
                {
                    if ( !active && !_found )
                        _on_inactive = true;
                    _found = true;

                    if ( _location.empty() )
                        _location = dn.attribute( "location" );
                }
            };

            mc::backtrace( bt, chk, ctx, ctx.snapshot(), 10000 );
        }
    };

    struct expect_trace : expectation
    {
        int _expect_count = 1, _match_count;
        bool _exact = false;
        std::string _match;

        void setup() override
        {
            _match_count = 0;
        }

        void check( const ui::with_report &, const std::string & ) override
        {
            if ( !_match.empty() )
                if ( _exact ? _match_count != _expect_count : _match_count < _expect_count )
                    brq::raise< wrong_trace >()
                        << _match << " (x" << _expect_count << ( _exact ? "" : " or more" )
                        << ") did not match the trace";
        }

        void result( mc::Result, const mc::Trace &trace ) override
        {
            if ( !_match.empty() )
                for ( auto l : trace.labels )
                    if ( l.find( _match ) != l.npos )
                        ++ _match_count;
        }
    };

    struct expect_sim : expectation
    {
        std::string _location, _symbol;
        std::stringstream *_stream = nullptr;

        void setup() override {}
        void check( const ui::sim &, const std::string &cmd ) override
        {
            if ( !_stream ) /* nothing to check */
                return;

            bool match = false;
            auto output = _stream->str();

            for ( auto line : brq::splitter( output, '\n' ) )
                if ( brq::starts_with( line, "  " ) &&
                     ( _location.empty() || line.find( _location ) != line.npos ) &&
                     ( _symbol.empty() || line.find( _symbol ) != line.npos ) )
                    match = true;

            if ( !match )
                brq::raise< wrong_sim >() << "sim backtrace did not match expectation: "
                                          << cmd << "\n" << output;
        }
    };

    struct expect : ui::CompositeMixin< expect >, brq::cmd_base
    {
        std::string _cmd;
        expect_result _result;
        expect_location _backtrace;
        expect_trace _trace;
        expect_sim _sim;

        bool _warn = false;

        std::array< expectation *, 4 > expectations()
        {
            return { &_result, &_backtrace, &_trace, &_sim };
        }

        void setup()
        {
            _sim._location = _backtrace._location;
            _sim._symbol = _backtrace._symbol;

            for ( auto e : expectations() )
                e->setup();
        }

        template< typename cmd_t >
        void check( const cmd_t &c )
        {
            try
            {
                for ( auto e : expectations() )
                    e->check( c, _cmd );
            }
            catch ( const wrong &e )
            {
                if ( _warn )
                    std::cerr << "W: " << e.what();
                else
                    throw;
            }
        }

        template< typename L >
        void each( L l )
        {
            for ( auto e: expectations() )
                l( e );
        }

        void run() override {}
        void options( brq::cmd_options &c ) override
        {
            c.opt( "--result", _result._result );
            c.opt( "--symbol", _backtrace._symbol );
            c.opt( "--location", _backtrace._location );
            c.opt( "--location-comment", _backtrace._comment );
            c.opt( "--trace-count", _trace._expect_count );
            c.opt( "--trace", _trace._match );
        }
    };

    struct load : brq::cmd_base
    {
        brq::cmd_file from;
        brq::cmd_path to;

        void run() override {}
        void options( brq::cmd_options &c ) override
        {
            c.pos( from );
            c.pos( to );
        }
    };

    std::vector< std::string > parse( std::string txt )
    {
        std::vector< std::string > script;

        for ( auto line : brq::splitter( txt, '\n' ) )
        {
            if ( line.empty() || line.at( 0 ) == '#' )
                continue;
            if ( line.at( 0 ) == ' ' && !script.empty() )
                script.back() += line;
            else
                script.emplace_back( line );
        }
        return script;
    }

    template< typename... F >
    void execute( std::string script_txt, F... prepare )
    {
        auto script = parse( script_txt );

        std::vector< std::shared_ptr< expect > > expects;
        std::vector< std::pair< std::string, std::string > > files;
        std::stringstream sim_stream;

        auto prepare_expects = [&]( ui::with_bc &cmd )
        {
            std::vector< ui::SinkPtr > log( expects.begin(), expects.end() );
            log.push_back( cmd._log );
            cmd._log = ui::make_composite( log );
            for ( auto & expect : expects )
                expect->setup();
        };

        auto check_expects = [&]( const auto &cmd )
        {
            for ( auto & expect : expects )
                expect->check( cmd );
        };

        auto prepare_sim = [&]( ui::sim &sim )
        {
            for ( auto e : expects )
                e->_sim._stream = &sim_stream;
            sim._cli->out( sim_stream );
        };

        for ( auto cmdstr : script )
        {
            auto split = brq::splitter( cmdstr, ' ' ); /* FIXME */
            std::vector< std::string_view > tok;
            std::copy_if( split.begin(), split.end(), std::back_inserter( tok ),
                          []( std::string_view s ) { return !s.empty(); } );
            ui::CLI cli( "divine", tok );
            cli._check_files = false;

            auto cmd = cli.parse< expect, load >();
            auto load_file = [&]( load &l )
            {
                files.emplace_back( l.to.name, brq::read_file( l.from.name ) );
                brq::create_file( l.to.name ); /* FIXME trick the CLI parser */
            };

            cmd.match( prepare..., load_file,
                       [&]( ui::cc &cc ) { cc._driver.map_files( files ); },
                       [&]( ui::with_bc &wbc ) { wbc._cc_driver.map_files( files ); } );
            cmd.match( [&]( ui::command &c ) { c.setup(); },
                       [&]( expect e )
                       {
                           e._cmd = cmdstr;
                           expects.emplace_back( std::make_shared< expect >( std::move( e ) ) );
                       } );
            cmd.match( [&]( ui::with_bc &cmd ) { prepare_expects( cmd ); } );
            cmd.match( [&]( ui::sim &sim ) { prepare_sim( sim ); } );
            cmd.match( [&]( ui::command &c ) { c.run(); } );
            cmd.match( [&]( auto &c ) { check_expects( c ); } );
        }
    }
}