/******************************************************************************
 * Top contributors (to current version):
 *   Andres Noetzli, Mathias Preiner
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Print functions that are safe to use in a signal handler.
 *
 * Signal handlers only allow a very limited set of operations, e.g. dynamic
 * memory allocation is not possible. This set of functions can be used to
 * print information from a signal handler.
 *
 * The safe_print function takes a template parameter T and prints an argument
 * of type const T& to avoid copying, e.g. when printing std::strings. For
 * consistency, we also pass primitive types by reference (otherwise, functions
 * in statistics_registry.h would require specialization or we would have to
 * use function overloading).
 *
 * If there exists a function `toString(obj)` for a given object, it will be
 * used automatically. This is useful for printing enum values for example.
 * IMPORTANT: The `toString(obj)` function *must not* perform any allocations
 * or call other functions that are not async-signal-safe.
 *
 * This header is a "cvc5_private_library.h" header because it is private but
 * the safe_print functions are used in the driver. See also the description
 * of "statistics_registry.h" for more information on
 * "cvc5_private_library.h".
 */

#include "cvc5_private_library.h"

#ifndef CVC5__SAFE_PRINT_H
#define CVC5__SAFE_PRINT_H

#include <unistd.h>

#include <cstring>
#include <string>

#include "cvc5_export.h"

namespace cvc5 {

/**
 * Prints arrays of chars (e.g. string literals) of length N. Safe to use in a
 * signal handler.
 */
template <size_t N>
void CVC5_EXPORT safe_print(int fd, const char (&msg)[N])
{
  ssize_t nb = N - 1;
  if (write(fd, msg, nb) != nb) {
    abort();
  }
}

/**
 * The default method for converting an object to a string for safe printing.
 * This method simply returns "<unsupported>". The `long` argument is used to
 * indicate that we do not prefer this method over the version that calls
 * `toString()`.
 */
template <typename T>
const char* toStringImpl(const T& obj, long)
{
  return "<unsupported>";
}

/**
 * Returns the result of calling `toString(obj)`. This method is only defined
 * if such an overload of `toString()` exists. To detect the existence of such
 * a method, we use SFINAE and a trailing return type. The trailing return type
 * is necessary because it allows us to refer to `obj`. The `int` argument is
 * used to prefer this version of the function instead of the one that prints
 * "<unsupported>".
 */
template <typename T>
auto toStringImpl(const T& obj, int) -> decltype(toString(obj))
{
  return toString(obj);
}

/**
 * Prints a variable of type T. Safe to use in a signal handler. The default
 * implementation either prints "<unsupported>" or the result of calling
 * `toString(obj)` if such a method exists (this is useful for printing enum
 * values for example without implementing a template specialization here).
 *
 * @param fd The file descriptor to print to
 * @param obj The object to print
 */
template <typename T>
void CVC5_EXPORT safe_print(int fd, const T& obj)
{
  const char* s =
      toStringImpl(obj, /* prefer the method that uses `toString()` */ 0);
  ssize_t slen = static_cast<ssize_t>(strlen(s));
  if (write(fd, s, slen) != slen)
  {
    abort();
  }
}

template <>
void CVC5_EXPORT safe_print(int fd, const std::string& msg);
template <>
void CVC5_EXPORT safe_print(int fd, const int64_t& _i);
template <>
void CVC5_EXPORT safe_print(int fd, const int32_t& i);
template <>
void CVC5_EXPORT safe_print(int fd, const uint64_t& _i);
template <>
void CVC5_EXPORT safe_print(int fd, const uint32_t& i);
template <>
void CVC5_EXPORT safe_print(int fd, const double& _d);
template <>
void CVC5_EXPORT safe_print(int fd, const float& f);
template <>
void CVC5_EXPORT safe_print(int fd, const bool& b);
template <>
void CVC5_EXPORT safe_print(int fd, void* const& addr);
template <>
void CVC5_EXPORT safe_print(int fd, const timespec& t);

/** Prints an integer in hexadecimal. Safe to use in a signal handler. */
void safe_print_hex(int fd, uint64_t i);

/**
 * Prints a right aligned number. Fills up remaining space with zeros. Safe to
 * use in a signal handler.
 */
void safe_print_right_aligned(int fd, uint64_t i, ssize_t width);

}  // namespace cvc5

#endif /* CVC5__SAFE_PRINT_H */