/** This file contains functionality related to creation of the GenMCDriver,
 * including translating settings set by Miri.  */

#include "MiriInterface.hpp"

// CXX.rs generated headers:
#include "genmc-sys/src/lib.rs.h"

// GenMC headers:
#include "Support/Error.hpp"
#include "Support/Verbosity.hpp"
#include "Verification/InterpreterCallbacks.hpp"

// C++ headers:
#include <cstdint>

/**
 * Translate the Miri-GenMC `LogLevel` to the GenMC `VerbosityLevel`.
 * Downgrade any debug options to `Tip` if `ENABLE_GENMC_DEBUG` is not enabled.
 */
static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel {
    switch (log_level) {
        case LogLevel::Quiet:
            return VerbosityLevel::Quiet;
        case LogLevel::Error:
            return VerbosityLevel::Error;
        case LogLevel::Warning:
            return VerbosityLevel::Warning;
        case LogLevel::Tip:
            return VerbosityLevel::Tip;
#ifdef ENABLE_GENMC_DEBUG
        case LogLevel::Debug1Revisits:
            return VerbosityLevel::Debug1;
        case LogLevel::Debug2MemoryAccesses:
            return VerbosityLevel::Debug2;
        case LogLevel::Debug3ReadsFrom:
            return VerbosityLevel::Debug3;
#else
        // Downgrade to `Tip` if the debug levels are not available.
        case LogLevel::Debug1Revisits:
        case LogLevel::Debug2MemoryAccesses:
        case LogLevel::Debug3ReadsFrom:
            return VerbosityLevel::Tip;
#endif
        default:
            WARN_ONCE(
                "unknown-log-level",
                "Unknown `LogLevel`, defaulting to `VerbosityLevel::Tip`."
            );
            return VerbosityLevel::Tip;
    }
}

/* unsafe */ void set_log_level_raw(LogLevel log_level) {
    // The `logLevel` is a static, non-atomic variable.
    // It should never be changed if `MiriGenmcShim` still exists, since any of its methods may read
    // the `logLevel`, otherwise it may cause data races.
    logLevel = to_genmc_verbosity_level(log_level);
}

/* unsafe */ auto MiriGenmcShim::create_handle(const GenmcParams& params, bool estimation_mode)
    -> std::unique_ptr<MiriGenmcShim> {
    auto conf = std::make_shared<Config>();

    // Set whether GenMC should print execution graphs after every explored/blocked execution.
    conf->printExecGraphs =
        (params.print_execution_graphs == ExecutiongraphPrinting::Explored ||
         params.print_execution_graphs == ExecutiongraphPrinting::ExploredAndBlocked);
    conf->printBlockedExecs =
        (params.print_execution_graphs == ExecutiongraphPrinting::Blocked ||
         params.print_execution_graphs == ExecutiongraphPrinting::ExploredAndBlocked);

    // `1024` is the default value that GenMC uses.
    // If any thread has at least this many events, a warning/tip will be printed.
    //
    // Miri produces a lot more events than GenMC, so the graph size warning triggers on almost
    // all programs. The current value is large enough so the warning is not be triggered by any
    // reasonable programs.
    // FIXME(genmc): The emitted warning mentions features not supported by Miri ('--unroll'
    // parameter).
    // FIXME(genmc): A more appropriate limit should be chosen once the warning is useful for
    // Miri.
    conf->warnOnGraphSize = 1024 * 1024;

    // We only support the `RC11` memory model for Rust, and `SC` when weak memory emulation is
    // disabled.
    conf->model = params.disable_weak_memory_emulation ? ModelType::SC : ModelType::RC11;

    // This prints the seed that GenMC picks for randomized scheduling during estimation mode.
    conf->printRandomScheduleSeed = params.print_random_schedule_seed;

    // FIXME(genmc): supporting IPR requires annotations for `assume` and `spinloops`.
    conf->ipr = false;
    // FIXME(genmc): supporting BAM requires `Barrier` support + detecting whether return value
    // of barriers are used.
    conf->disableBAM = true;

    // Instruction caching could help speed up verification by filling the graph from cache, if
    // the list of values read by all load events in a thread have been seen before. Combined
    // with not replaying completed threads, this can also reducing the amount of Mir
    // interpretation required by Miri. With the current setup, this would be incorrect, since
    // Miri doesn't give GenMC the actual values read by non-atomic reads.
    conf->instructionCaching = false;
    // Many of Miri's checks work under the assumption that threads are only executed in an
    // order that could actually happen during a normal execution. Formally, this means that
    // replaying an execution needs to respect the po-rf-relation of the executiongraph (po ==
    // program-order, rf == reads-from). This means, any event in the graph, when replayed, must
    // happen after any events that happen before it in the same graph according to the program
    // code, and all (non-atomic) reads must happen after the write event they read from.
    //
    // Not replaying completed threads means any read event from that thread never happens in
    // Miri's memory, so this would only work if there are never any non-atomic reads from any
    // value written by the skipped thread.
    conf->replayCompletedThreads = true;

    // FIXME(genmc): implement symmetry reduction.
    ERROR_ON(
        params.do_symmetry_reduction,
        "Symmetry reduction is currently unsupported in GenMC mode."
    );
    conf->symmetryReduction = params.do_symmetry_reduction;

    // Set the scheduling policy. GenMC uses `WFR` for estimation mode.
    // For normal verification, `WF` has the best performance and is the GenMC default.
    // Other scheduling policies are used by GenMC for testing and for modes currently
    // unsupported with Miri such as bounding, which uses LTR.
    conf->schedulePolicy = estimation_mode ? SchedulePolicy::WFR : SchedulePolicy::WF;

    // Set the min and max number of executions tested in estimation mode.
    conf->estimationMin = 10; // default taken from GenMC
    conf->estimationMax = params.estimation_max;
    // Deviation threshold % under which estimation is deemed good enough.
    conf->sdThreshold = 10; // default taken from GenMC
    // Set the mode used for this driver, either estimation or verification.
    const auto mode = estimation_mode ? GenMCDriver::Mode(GenMCDriver::EstimationMode {})
                                      : GenMCDriver::Mode(GenMCDriver::VerificationMode {});

    // Running Miri-GenMC without race detection is not supported.
    // Disabling this option also changes the behavior of the replay scheduler to only schedule
    // at atomic operations, which is required with Miri. This happens because Miri can generate
    // multiple GenMC events for a single MIR terminator. Without this option, the scheduler
    // might incorrectly schedule an atomic MIR terminator because the first event it creates is
    // a non-atomic (e.g., `StorageLive`).
    conf->disableRaceDetection = false;

    // Miri can already check for unfreed memory. Also, GenMC cannot distinguish between memory
    // that is allowed to leak and memory that is not.
    conf->warnUnfreedMemory = false;

    // Validate the config and exit if there are any errors
    std::vector<std::string> warnings;
    auto config_valid = conf->validate(warnings);
    for (const auto& w : warnings)
        WARN("{}", w);
    if (auto* errors = std::get_if<ConfigErrorList>(&config_valid); errors) {
        for (const auto& e : *errors)
            LOG(VerbosityLevel::Error, "{}", e);
        exit(EUSER);
    }

    // Create the actual driver and Miri-GenMC communication shim.
    auto driver = std::make_unique<MiriGenmcShim>(std::move(conf), mode);

    // FIXME(genmc,HACK): Until a proper solution is implemented in GenMC, these callbacks will
    // allow Miri to return information about global allocations and override uninitialized memory
    // checks for non-atomic loads (Miri handles those without GenMC, so the error would be wrong).
    auto interpreter_callbacks = InterpreterCallbacks {
        // Miri already ensures that memory accesses are valid, so this check doesn't matter.
        // We check that the address is static, but skip checking if it is part of an actual
        // allocation.
        .isStaticallyAllocated = [](SAddr addr) { return addr.isStatic(); },
        // FIXME(genmc,error reporting): Once a proper a proper API for passing such information is
        // implemented in GenMC, Miri should use it to improve the produced error messages.
        .getStaticName = [](SAddr addr) { return "[UNKNOWN STATIC]"; },
        // This function is called to get the initial value stored at the given address.
        //
        // From a Miri perspective, this API doesn't work very well: most memory starts out
        // "uninitialized";
        // only statics have an initial value. And their initial value is just a sequence of bytes,
        // but GenMC expect this to be already split into separate atomic variables. So we return a
        // dummy value.
        // This value should never be visible to the interpreted program.
        // GenMC does not understand uninitialized memory the same way Miri does, which may cause
        // this function to be called. The returned value can be visible to Miri or the user:
        // - Printing the execution graph may contain this value in place of uninitialized values.
        //   FIXME(genmc): NOTE: printing the execution graph is not yet implemented.
        // - Non-atomic loads may return this value, but Miri ignores values of non-atomic loads.
        // - Atomic loads will *not* see this value once mixed atomic-non-atomic support is added.
        //   Currently, atomic loads can see this value, unless initialized by an *atomic* store.
        //   FIXME(genmc): update this comment once mixed atomic-non-atomic support is added.
        //
        // FIXME(genmc): implement proper support for uninitialized memory in GenMC.
        // Ideally, the initial value getter would return an `optional<SVal>`, since the memory
        // location may be uninitialized.
        .initValGetter = [](const AAccess& a) { return SVal(0xDEAD); },
        // Miri serves non-atomic loads from its own memory and these GenMC checks are wrong in that
        // case. This should no longer be required with proper mixed-size access support.
        .skipUninitLoadChecks = [](const MemAccessLabel* access_label
                                ) { return access_label->getOrdering() == MemOrdering::NotAtomic; },
    };
    driver->setInterpCallbacks(std::move(interpreter_callbacks));

    return driver;
}