// -*- C++ -*- (c) 2020 Henrich Lauko <xlauko@mail.muni.cz>

DIVINE_RELAX_WARNINGS
#include <llvm/Pass.h>
#include <llvm/IR/Module.h>
#include <llvm/IR/Instructions.h>
#include <llvm/IR/IRBuilder.h>
DIVINE_UNRELAX_WARNINGS

#include <lart/support/pass.h>
#include <lart/support/meta.h>
#include <lart/support/util.h>

#include <llvm/IR/DebugLoc.h>
#include <llvm/IR/DebugInfoMetadata.h>

namespace lart {
namespace svcomp {

    struct TraceNondets
    {
        static PassMeta meta() {
            return passMeta< TraceNondets >( "trace-nondets", "" );
        }

        void run( llvm::Module &m ) {
            _fn_trace = m.getFunction( "__dios_trace_auto" );

            auto *traceT = _fn_trace->getFunctionType();
            traceStay = llvm::ConstantInt::get( traceT->getParamType( 0 ),  0 );

            auto is_verifier_nondet = [] ( auto cs ) {
                auto fn = cs->getCalledOperand()->stripPointerCasts();
                if ( fn && fn->hasName() )
                    return fn->getName().startswith( "__VERIFIER_nondet" );
                return false;
            };

            auto calls = util::callsites_range( m )
                .filter( is_verifier_nondet )
                .freeze();

            for ( auto cs : calls )
                process( cs );
        }

        void process( llvm::CallBase *cs )
        {
            llvm::IRBuilder<> irb( cs );
            irb.CreateCall( _fn_trace, callArgs( cs, irb ) );

        }

        std::vector< llvm::Value * > callArgs( llvm::CallBase *cs, llvm::IRBuilder<> &irb )
        {
            auto name = cs->getCalledOperand()->stripPointerCasts()->getName().str();
            const llvm::DebugLoc &dbg = cs->getDebugLoc();
            std::string fmt = "nondet:" + name + ":" + std::to_string(dbg->getLine());
            std::vector< llvm::Value * > vals;
            vals.push_back( traceStay );
            vals.push_back( getLit( fmt, irb ) );
            return vals;
        }

        llvm::Value *getLit( std::string lit, llvm::IRBuilder<> &irb ) {
            lit.push_back( 0 );
            auto it = litmap.find( lit );
            if ( it != litmap.end() )
                return it->second;
            return litmap.emplace( lit, irb.CreatePointerCast( util::getStringGlobal( lit,
                                        *irb.GetInsertBlock()->getParent()->getParent() ),
                                    irb.getInt8PtrTy() ) ).first->second;
        }

        llvm::Function *_fn_trace;
        llvm::Constant *traceStay = nullptr;

        util::Map< std::string, llvm::Value * > litmap;
    };

    PassMeta svcTraceNondetsPass() {
        return compositePassMeta< TraceNondets >( "svc-trace-nondets", "" );
    }

}
}