Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Print functions that are safe to use in a signal handler.
      11                 :            :  *
      12                 :            :  * Signal handlers only allow a very limited set of operations, e.g. dynamic
      13                 :            :  * memory allocation is not possible. This set of functions can be used to
      14                 :            :  * print information from a signal handler.
      15                 :            :  *
      16                 :            :  * The safe_print function takes a template parameter T and prints an argument
      17                 :            :  * of type const T& to avoid copying, e.g. when printing std::strings. For
      18                 :            :  * consistency, we also pass primitive types by reference (otherwise, functions
      19                 :            :  * in statistics_registry.h would require specialization or we would have to
      20                 :            :  * use function overloading).
      21                 :            :  *
      22                 :            :  * If there exists a function `toString(obj)` for a given object, it will be
      23                 :            :  * used automatically. This is useful for printing enum values for example.
      24                 :            :  * IMPORTANT: The `toString(obj)` function *must not* perform any allocations
      25                 :            :  * or call other functions that are not async-signal-safe.
      26                 :            :  *
      27                 :            :  * This header is a "cvc5_private_library.h" header because it is private but
      28                 :            :  * the safe_print functions are used in the driver. See also the description
      29                 :            :  * of "statistics_registry.h" for more information on
      30                 :            :  * "cvc5_private_library.h".
      31                 :            :  */
      32                 :            : 
      33                 :            : #include "cvc5_private_library.h"
      34                 :            : 
      35                 :            : #ifndef CVC5__SAFE_PRINT_H
      36                 :            : #define CVC5__SAFE_PRINT_H
      37                 :            : 
      38                 :            : #include <cvc5/cvc5_export.h>
      39                 :            : #include <time.h>
      40                 :            : #include <unistd.h>
      41                 :            : 
      42                 :            : #include <cstdlib>
      43                 :            : #include <cstring>
      44                 :            : #include <string>
      45                 :            : 
      46                 :            : namespace cvc5::internal {
      47                 :            : 
      48                 :            : template <size_t N>
      49                 :            : void CVC5_EXPORT safe_print(int fd, const char (&msg)[N]);
      50                 :            : template <typename T>
      51                 :            : void CVC5_EXPORT safe_print(int fd, const T& obj);
      52                 :            : 
      53                 :            : /**
      54                 :            :  * Prints arrays of chars (e.g. string literals) of length N. Safe to use in a
      55                 :            :  * signal handler.
      56                 :            :  */
      57                 :            : template <size_t N>
      58                 :         17 : void safe_print(int fd, const char (&msg)[N])
      59                 :            : {
      60                 :         17 :   ssize_t nb = N - 1;
      61         [ -  + ]:         17 :   if (write(fd, msg, nb) != nb)
      62                 :            :   {
      63                 :          0 :     abort();
      64                 :            :   }
      65                 :         17 : }
      66                 :            : 
      67                 :            : /**
      68                 :            :  * The default method for converting an object to a string for safe printing.
      69                 :            :  * This method simply returns "<unsupported>". The `long` argument is used to
      70                 :            :  * indicate that we do not prefer this method over the version that calls
      71                 :            :  * `toString()`.
      72                 :            :  */
      73                 :            : template <typename T>
      74                 :          1 : const char* toStringImpl(const T&, long)
      75                 :            : {
      76                 :          1 :   return "<unsupported>";
      77                 :            : }
      78                 :            : 
      79                 :            : /**
      80                 :            :  * Returns the result of calling `toString(obj)`. This method is only defined
      81                 :            :  * if such an overload of `toString()` exists. To detect the existence of such
      82                 :            :  * a method, we use SFINAE and a trailing return type. The trailing return type
      83                 :            :  * is necessary because it allows us to refer to `obj`. The `int` argument is
      84                 :            :  * used to prefer this version of the function instead of the one that prints
      85                 :            :  * "<unsupported>".
      86                 :            :  */
      87                 :            : template <typename T>
      88                 :          2 : auto toStringImpl(const T& obj, int) -> decltype(toString(obj))
      89                 :            : {
      90                 :          2 :   return toString(obj);
      91                 :            : }
      92                 :            : 
      93                 :            : /**
      94                 :            :  * Prints a variable of type T. Safe to use in a signal handler. The default
      95                 :            :  * implementation either prints "<unsupported>" or the result of calling
      96                 :            :  * `toString(obj)` if such a method exists (this is useful for printing enum
      97                 :            :  * values for example without implementing a template specialization here).
      98                 :            :  *
      99                 :            :  * @param fd The file descriptor to print to
     100                 :            :  * @param obj The object to print
     101                 :            :  */
     102                 :            : template <typename T>
     103                 :          3 : void safe_print(int fd, const T& obj)
     104                 :            : {
     105                 :            :   const char* s =
     106                 :          3 :       toStringImpl(obj, /* prefer the method that uses `toString()` */ 0);
     107                 :          3 :   ssize_t slen = static_cast<ssize_t>(strlen(s));
     108         [ -  + ]:          3 :   if (write(fd, s, slen) != slen)
     109                 :            :   {
     110                 :          0 :     abort();
     111                 :            :   }
     112                 :          3 : }
     113                 :            : 
     114                 :            : template <>
     115                 :            : void CVC5_EXPORT safe_print(int fd, const std::string& msg);
     116                 :            : template <>
     117                 :            : void CVC5_EXPORT safe_print(int fd, const int64_t& _i);
     118                 :            : template <>
     119                 :            : void CVC5_EXPORT safe_print(int fd, const int32_t& i);
     120                 :            : template <>
     121                 :            : void CVC5_EXPORT safe_print(int fd, const uint64_t& _i);
     122                 :            : template <>
     123                 :            : void CVC5_EXPORT safe_print(int fd, const uint32_t& i);
     124                 :            : template <>
     125                 :            : void CVC5_EXPORT safe_print(int fd, const double& _d);
     126                 :            : template <>
     127                 :            : void CVC5_EXPORT safe_print(int fd, const float& f);
     128                 :            : template <>
     129                 :            : void CVC5_EXPORT safe_print(int fd, const bool& b);
     130                 :            : template <>
     131                 :            : void CVC5_EXPORT safe_print(int fd, void* const& addr);
     132                 :            : template <>
     133                 :            : void CVC5_EXPORT safe_print(int fd, const timespec& t);
     134                 :            : 
     135                 :            : /** Prints an integer in hexadecimal. Safe to use in a signal handler. */
     136                 :            : void safe_print_hex(int fd, uint64_t i);
     137                 :            : 
     138                 :            : /**
     139                 :            :  * Prints a right aligned number. Fills up remaining space with zeros. Safe to
     140                 :            :  * use in a signal handler.
     141                 :            :  */
     142                 :            : void safe_print_right_aligned(int fd, uint64_t i, ssize_t width);
     143                 :            : 
     144                 :            : }  // namespace cvc5::internal
     145                 :            : 
     146                 :            : #endif /* CVC5__SAFE_PRINT_H */