message.h

Go to the documentation of this file.

#pragma once
 
#include <cstdio>
#include <fmt/format.h>
#include <fmt/color.h>
#include <fmt/ranges.h>
#include <util/message/format.h>
#include <ctime>
#include <chrono>
#include <iomanip>

enum class VerbosityLevel : char
{
  None,     // No message output
  Error,    // fatal errors are printed
  Warning,  // warnings are printend
  Result,   // results of the analysis (including CE)
  Progress, // progress notifications
  Success,  // verification success/claim holds
  Fail,     // verification/claim fails
  Status,   // all kinds of things esbmc is doing that may be useful to the user
  Debug     // messages that are only useful if you need to debug.
};
 
struct messaget
{
  static inline class statet
  {
    static void println(
      FILE *f,
      VerbosityLevel lvl,
      fmt::string_view format,
      fmt::format_args args);
 
  public:
    VerbosityLevel verbosity;
    std::unordered_map<std::string, VerbosityLevel> modules;
    FILE *out;
 
    FILE *target(const char *mod, VerbosityLevel lvl) const;
 
    void set_flushln() const;
 
    template <typename... Args>
    bool logln(
      const char *mod,
      VerbosityLevel lvl,
      const char *file,
      int line,
      fmt::format_string<Args...> format,
      Args &&...args) const
    {
      FILE *f = target(mod, lvl);
      if (!f)
        return false;
      if (config.options.get_bool_option("log-message"))
      {
        std::time_t currentTime = std::chrono::system_clock::to_time_t(
          std::chrono::system_clock::now());
        std::string timeStr =
          (std::ostringstream{}
           << std::put_time(std::localtime(&currentTime), "%Y-%m-%d %H:%M:%S"))
            .str();
        fmt::print(f, "[{}] File: {}, Line: {} ", timeStr, file, line);
      }
      println(f, lvl, format, fmt::make_format_args(args...));
      return true;
    }
  } state = {VerbosityLevel::Status, {}, stderr};
};
 
#define log_error(fmt, ...)                                                    \
  messaget::state.logln(                                                       \
    nullptr, VerbosityLevel::Error, __FILE__, __LINE__, FMT_STRING(fmt), ##__VA_ARGS__)
#define log_result(fmt, ...)                                                   \
  messaget::state.logln(                                                       \
    nullptr, VerbosityLevel::Result, __FILE__, __LINE__, FMT_STRING(fmt), ##__VA_ARGS__)
#define log_warning(fmt, ...)                                                  \
  messaget::state.logln(                                                       \
    nullptr, VerbosityLevel::Warning, __FILE__, __LINE__, FMT_STRING(fmt), ##__VA_ARGS__)
#define log_progress(fmt, ...)                                                 \
  messaget::state.logln(                                                       \
    nullptr, VerbosityLevel::Progress, __FILE__, __LINE__, FMT_STRING(fmt), ##__VA_ARGS__)
#define log_success(fmt, ...)                                                  \
  messaget::state.logln(                                                       \
    nullptr, VerbosityLevel::Success, __FILE__, __LINE__, FMT_STRING(fmt), ##__VA_ARGS__)
#define log_fail(fmt, ...)                                                     \
  messaget::state.logln(                                                       \
    nullptr, VerbosityLevel::Fail, __FILE__, __LINE__, FMT_STRING(fmt), ##__VA_ARGS__)
#define log_status(fmt, ...)                                                   \
  messaget::state.logln(                                                       \
    nullptr, VerbosityLevel::Status, __FILE__, __LINE__, FMT_STRING(fmt), ##__VA_ARGS__)
#define log_debug(mod, fmt, ...)                                               \
  messaget::state.logln(                                                       \
    mod, VerbosityLevel::Debug, __FILE__, __LINE__, FMT_STRING(fmt), ##__VA_ARGS__)