cprover
invariant.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Martin Brain, martin.brain@diffblue.com
6 
7 \*******************************************************************/
8 
9 #include "invariant.h"
10 
11 #include "freer.h"
12 
13 #include <iomanip>
14 #include <memory>
15 #include <sstream>
16 #include <string>
17 
18 #include <iostream>
19 
20 #ifdef _WIN32
21 // the ordering of includes is required
22 // clang-format off
23 #include <windows.h>
24 #include <dbghelp.h>
25 // clang-format on
26 #endif
27 
29 
30 // Backtraces compiler and C library specific
31 // So we should include something explicitly from the C library
32 // to check if the C library is glibc.
33 #include <assert.h>
34 #if defined(__GLIBC__) || defined(__APPLE__)
35 
36 // GCC needs LINKFLAGS="-rdynamic" to give function names in the backtrace
37 #include <execinfo.h>
38 #include <cxxabi.h>
39 
49 static bool output_demangled_name(
50  std::ostream &out,
51  const std::string &stack_entry)
52 {
53  bool return_value=false;
54 
55  std::string working(stack_entry);
56 
57  std::string::size_type start=working.rfind('('); // Path may contain '(' !
58  std::string::size_type end=working.find('+', start);
59 
60  if(start!=std::string::npos &&
61  end!=std::string::npos &&
62  start+1<=end-1)
63  {
64  std::string::size_type length=end-(start+1);
65  std::string mangled(working.substr(start+1, length));
66 
67  int demangle_success=1;
68  std::unique_ptr<char, freert> demangled(
69  abi::__cxa_demangle(
70  mangled.c_str(), nullptr, nullptr, &demangle_success));
71 
72  if(demangle_success==0)
73  {
74  out << working.substr(0, start+1)
75  << demangled.get()
76  << working.substr(end);
77  return_value=true;
78  }
79  }
80 
81  return return_value;
82 }
83 #endif
84 
85 
89  std::ostream &out)
90 {
91 #if defined(__GLIBC__) || defined(__APPLE__)
92  void * stack[50] = {};
93 
94  std::size_t entries=backtrace(stack, sizeof(stack) / sizeof(void *));
95  std::unique_ptr<char*, freert> description(
96  backtrace_symbols(stack, entries));
97 
98  for(std::size_t i=0; i<entries; i++)
99  {
100  if(!output_demangled_name(out, description.get()[i]))
101  out << description.get()[i];
102  out << '\n' << std::flush;
103  }
104 
105 #elif defined(_WIN32)
106 
107  void *stack[50];
108  HANDLE process = GetCurrentProcess();
109 
110  SymInitialize(process, NULL, TRUE);
111 
112  auto number_of_frames =
113  CaptureStackBackTrace(0, sizeof(stack) / sizeof(void *), stack, NULL);
114 
115  // Read
116  // https://docs.microsoft.com/en-us/windows/win32/api/dbghelp/ns-dbghelp-symbol_info
117  // for the rationale behind the size of 'symbol'
118  const auto max_name_len = 255;
119  auto symbol = static_cast<SYMBOL_INFO *>(
120  calloc(sizeof SYMBOL_INFO + (max_name_len - 1) * sizeof(TCHAR), 1));
121  symbol->MaxNameLen = max_name_len;
122  symbol->SizeOfStruct = sizeof SYMBOL_INFO;
123 
124  for(std::size_t i = 0; i < number_of_frames; i++)
125  {
126  SymFromAddr(process, (DWORD64)(stack[i]), 0, symbol);
127  out << std::setw(3) << i;
128  out << " 0x" << std::hex << std::setw(8) << symbol->Address;
129  out << ' ' << symbol->Name;
130  out << '\n' << std::flush;
131  }
132 
133  free(symbol);
134 #else
135  out << "Backtraces not supported\n" << std::flush;
136 #endif
137 }
138 
141 std::string get_backtrace()
142 {
143  std::ostringstream ostr;
144  print_backtrace(ostr);
145  return ostr.str();
146 }
147 
150 {
151  std::cerr << "--- begin invariant violation report ---\n";
152  std::cerr << reason.what() << '\n';
153  std::cerr << "--- end invariant violation report ---\n";
154 }
155 
156 std::string invariant_failedt::what() const noexcept
157 {
158  std::ostringstream out;
159  out << "Invariant check failed\n"
160  << "File: " << file << ":" << line << " function: " << function << '\n'
161  << "Condition: " << condition << '\n'
162  << "Reason: " << reason << '\n'
163  << "Backtrace:" << '\n'
164  << backtrace << '\n';
165  return out.str();
166 }
167 
168 std::string invariant_with_diagnostics_failedt::what() const noexcept
169 {
170  std::string s(invariant_failedt::what());
171 
172  if(!s.empty() && s.back() != '\n')
173  s += '\n';
174 
175  return s + "Diagnostics: " + diagnostics + '\n';
176 }
invariant_failedt::condition
const std::string condition
Definition: invariant.h:117
print_backtrace
void print_backtrace(std::ostream &out)
Prints a back trace to 'out'.
Definition: invariant.cpp:88
TRUE
#define TRUE
Definition: driver.h:7
invariant_failedt
A logic error, augmented with a distinguished field to hold a backtrace.
Definition: invariant.h:110
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
file
Definition: kdev_t.h:19
invariant.h
invariant_with_diagnostics_failedt::diagnostics
const std::string diagnostics
Definition: invariant.h:147
report_exception_to_stderr
void report_exception_to_stderr(const invariant_failedt &reason)
Dump exception report to stderr.
Definition: invariant.cpp:149
invariant_failedt::line
const int line
Definition: invariant.h:115
invariant_failedt::reason
const std::string reason
Definition: invariant.h:118
invariant_failedt::backtrace
const std::string backtrace
Definition: invariant.h:116
freer.h
get_backtrace
std::string get_backtrace()
Returns a backtrace.
Definition: invariant.cpp:141
invariant_failedt::what
virtual std::string what() const noexcept
Definition: invariant.cpp:156
invariant_with_diagnostics_failedt::what
virtual std::string what() const noexcept
Definition: invariant.cpp:168
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
cbmc_invariants_should_throw
bool cbmc_invariants_should_throw
Set this to true to cause invariants to throw a C++ exception rather than abort the program.
Definition: invariant.cpp:28