cprover
java_bytecode_concurrency_instrumentation.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java Convert Thread blocks
4 
5 Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com
6 
7 \*******************************************************************/
8 
10 #include "expr2java.h"
11 #include "java_types.h"
12 #include "java_utils.h"
13 
14 #include <util/expr_iterator.h>
15 #include <util/namespace.h>
16 #include <util/cprover_prefix.h>
17 #include <util/std_types.h>
18 #include <util/arith_tools.h>
19 
20 // Disable linter to allow an std::string constant.
21 const std::string next_thread_id = CPROVER_PREFIX "_next_thread_id";// NOLINT(*)
22 const std::string thread_id = CPROVER_PREFIX "_thread_id";// NOLINT(*)
23 
34  symbol_tablet &symbol_table,
35  const irep_idt &name,
36  const irep_idt &base_name,
37  const typet &type,
38  const exprt &value,
39  const bool is_thread_local,
40  const bool is_static_lifetime)
41 {
42  const symbolt *psymbol = nullptr;
43  namespacet ns(symbol_table);
44  ns.lookup(name, psymbol);
45  if(psymbol != nullptr)
46  return *psymbol;
47  symbolt new_symbol;
48  new_symbol.name = name;
49  new_symbol.pretty_name = name;
50  new_symbol.base_name = base_name;
51  new_symbol.type = type;
52  new_symbol.value = value;
53  new_symbol.is_lvalue = true;
54  new_symbol.is_state_var = true;
55  new_symbol.is_static_lifetime = is_static_lifetime;
56  new_symbol.is_thread_local = is_thread_local;
57  new_symbol.mode = ID_java;
58  symbol_table.add(new_symbol);
59  return new_symbol;
60 }
61 
66 static const std::string get_first_label_id(const std::string &id)
67 {
68  return CPROVER_PREFIX "_THREAD_ENTRY_" + id;
69 }
70 
75 static const std::string get_second_label_id(const std::string &id)
76 {
77  return CPROVER_PREFIX "_THREAD_EXIT_" + id;
78 }
79 
84 static const std::string get_thread_block_identifier(
85  const code_function_callt &f_code)
86 {
87  PRECONDITION(f_code.arguments().size() == 1);
88  const exprt &expr = f_code.arguments()[0];
89  const mp_integer lbl_id =
90  numeric_cast_v<mp_integer>(to_constant_expr(to_multi_ary_expr(expr).op0()));
91  return integer2string(lbl_id);
92 }
93 
102  const symbol_tablet &symbol_table,
103  bool is_enter,
104  const exprt &object)
105 {
106  const irep_idt symbol =
107  is_enter ? "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V"
108  : "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
109 
110  auto it = symbol_table.symbols.find(symbol);
111 
112  // If the 'java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V' or
113  // 'java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V' method is not
114  // found symex will rightfully complain as it cannot find the symbol
115  // associated with the method in question. To avoid this and thereby ensuring
116  // JBMC works both with and without the models, we replace the aforementioned
117  // methods with skips when we cannot find them.
118  //
119  // Note: this can only happen if the java-core-models library is not loaded.
120  //
121  // Note': we explicitly prevent JBMC from stubbing these methods.
122  if(it == symbol_table.symbols.end())
123  return code_skipt();
124 
125  // Otherwise we create a function call
126  return code_function_callt(symbol_exprt(symbol, it->second.type), {object});
127 }
128 
133 static void monitor_exits(codet &code, const codet &monitorexit)
134 {
135  const irep_idt &statement = code.get_statement();
136  if(statement == ID_return)
137  {
138  // Replace the return with a monitor exit plus return block
139  code = code_blockt({monitorexit, code});
140  }
141  else if(
142  statement == ID_label || statement == ID_block ||
143  statement == ID_decl_block)
144  {
145  // If label or block found, explore the code inside the block
146  Forall_operands(it, code)
147  {
148  codet &sub_code = to_code(*it);
149  monitor_exits(sub_code, monitorexit);
150  }
151  }
152 }
153 
207  symbol_tablet &symbol_table,
208  symbolt &symbol,
209  const exprt &sync_object)
210 {
211  PRECONDITION(!symbol.type.get_bool(ID_is_static));
212 
213  codet &code = to_code(symbol.value);
214 
215  // Get the calls to the functions that implement the critical section
216  codet monitorenter = get_monitor_call(symbol_table, true, sync_object);
217  codet monitorexit = get_monitor_call(symbol_table, false, sync_object);
218 
219  // Create a unique catch label and empty throw type (i.e. any)
220  // and catch-push them at the beginning of the code (i.e. begin try)
221  code_push_catcht catch_push;
222  irep_idt handler("pc-synchronized-catch");
223  irep_idt exception_id;
224  code_push_catcht::exception_listt &exception_list =
225  catch_push.exception_list();
226  exception_list.push_back(
227  code_push_catcht::exception_list_entryt(exception_id, handler));
228 
229  // Create a catch-pop to indicate the end of the try block
230  code_pop_catcht catch_pop;
231 
232  // Create the finally block with the same label targeted in the catch-push
233  const symbolt &tmp_symbol = fresh_java_symbol(
234  java_reference_type(struct_tag_typet("java::java.lang.Throwable")),
235  "caught-synchronized-exception",
236  code.source_location(),
237  id2string(symbol.name),
238  symbol_table);
239  symbol_exprt catch_var(tmp_symbol.name, tmp_symbol.type);
240  catch_var.set(ID_C_base_name, tmp_symbol.base_name);
241  code_landingpadt catch_statement(catch_var);
242  codet catch_instruction = catch_statement;
243  code_labelt catch_label(handler, code_blockt());
244  code_blockt &catch_block = to_code_block(catch_label.code());
245  catch_block.add(catch_instruction);
246  catch_block.add(monitorexit);
247 
248  // Re-throw exception
249  side_effect_expr_throwt throw_expr(irept(), typet(), code.source_location());
250  throw_expr.copy_to_operands(catch_var);
251  catch_block.add(code_expressiont(throw_expr));
252 
253  // Write a monitorexit before every return
254  monitor_exits(code, monitorexit);
255 
256  // Wrap the code into a try finally
257  code = code_blockt({monitorenter, catch_push, code, catch_pop, catch_label});
258 }
259 
270  const code_function_callt &f_code,
271  codet &code,
272  symbol_tablet &symbol_table)
273 {
274  PRECONDITION(f_code.arguments().size() == 1);
275 
276  // Create global variable __CPROVER__next_thread_id. Used as a counter
277  // in-order to to assign ids to new threads.
278  const symbol_exprt next_symbol_expr = add_or_get_symbol(
279  symbol_table,
282  java_int_type(),
284  false,
285  true)
286  .symbol_expr();
287 
288  // Create thread-local variable __CPROVER__thread_id. Holds the id of
289  // the thread.
290  const symbolt &current_symbol =
292  symbol_table, thread_id, thread_id, java_int_type(),
293  from_integer(0, java_int_type()), true, true);
294 
295  // Construct appropriate labels.
296  // Note: java does not have labels so this should be safe.
297  const std::string &thread_block_id = get_thread_block_identifier(f_code);
298  const std::string &lbl1 = get_first_label_id(thread_block_id);
299  const std::string &lbl2 = get_second_label_id(thread_block_id);
300 
301  // Instrument the following codet's:
302  //
303  // A: codet(id=ID_start_thread, destination=__CPROVER_THREAD_ENTRY_<ID>)
304  // B: codet(id=ID_goto, destination=__CPROVER_THREAD_EXIT_<ID>)
305  // C: codet(id=ID_label, label=__CPROVER_THREAD_ENTRY_<ID>)
306  // C.1: codet(id=ID_atomic_begin)
307  // D: CPROVER__next_thread_id += 1;
308  // E: __CPROVER__thread_id = __CPROVER__next_thread_id;
309  // F: codet(id=ID_atomic_end)
310 
311  codet tmp_a(ID_start_thread);
312  tmp_a.set(ID_destination, lbl1);
313  code_gotot tmp_b(lbl2);
314  const code_labelt tmp_c(lbl1, code_skipt());
315 
316  const plus_exprt plus(next_symbol_expr, from_integer(1, java_int_type()));
317  const code_assignt tmp_d(next_symbol_expr, plus);
318  const code_assignt tmp_e(current_symbol.symbol_expr(), next_symbol_expr);
319 
320  code = code_blockt({tmp_a,
321  tmp_b,
322  tmp_c,
323  codet(ID_atomic_begin),
324  tmp_d,
325  tmp_e,
326  codet(ID_atomic_end)});
327  code.add_source_location() = f_code.source_location();
328 }
329 
340  const code_function_callt &f_code,
341  codet &code,
342  const symbol_tablet &symbol_table)
343 {
344  PRECONDITION(f_code.arguments().size() == 1);
345  (void)symbol_table; // unused parameter
346 
347  // Build id, used to construct appropriate labels.
348  // Note: java does not have labels so this should be safe
349  const std::string &thread_block_id = get_thread_block_identifier(f_code);
350  const std::string &lbl2 = get_second_label_id(thread_block_id);
351 
352  // Instrument the following code:
353  //
354  // A: codet(id=ID_end_thread)
355  // B: codet(id=ID_label,label= __CPROVER_THREAD_EXIT_<ID>)
356  codet tmp_a(ID_end_thread);
357  const code_labelt tmp_b(lbl2, code_skipt());
358 
359  const auto location = code.source_location();
360  code = code_blockt({tmp_a, tmp_b});
361  code.add_source_location() = location;
362 }
363 
374  const code_function_callt &f_code,
375  codet &code,
376  symbol_tablet &symbol_table)
377 {
378  PRECONDITION(f_code.arguments().size() == 0);
379 
380  const symbolt& current_symbol =
381  add_or_get_symbol(symbol_table,
382  thread_id,
383  thread_id,
384  java_int_type(),
386  true, true);
387 
388  code_assignt code_assign(f_code.lhs(), current_symbol.symbol_expr());
389  code_assign.add_source_location() = f_code.source_location();
390 
391  code = code_assign;
392 }
393 
455 {
456  using instrument_callbackt =
457  std::function<void(const code_function_callt&, codet&, symbol_tablet&)>;
458  using expr_replacement_mapt =
459  std::unordered_map<const exprt, instrument_callbackt, irep_hash>;
460 
461  namespacet ns(symbol_table);
462 
463  for(const auto &entry : symbol_table)
464  {
465  expr_replacement_mapt expr_replacement_map;
466  const symbolt &symbol = entry.second;
467 
468  // Look for code_function_callt's (without breaking sharing)
469  // and insert each one into a replacement map along with an associated
470  // callback that will handle their instrumentation.
471  for(auto it = symbol.value.depth_begin(), itend = symbol.value.depth_end();
472  it != itend; ++it)
473  {
474  instrument_callbackt cb;
475 
476  const exprt &expr = *it;
477  if(expr.id() != ID_code)
478  continue;
479 
480  const codet &code = to_code(expr);
481  if(code.get_statement() != ID_function_call)
482  continue;
483 
484  const code_function_callt &f_code = to_code_function_call(code);
485  const std::string &f_name = expr2java(f_code.function(), ns);
486  if(f_name == "org.cprover.CProver.startThread:(I)V")
487  cb = std::bind(
489  std::placeholders::_1,
490  std::placeholders::_2,
491  std::placeholders::_3);
492  else if(f_name == "org.cprover.CProver.endThread:(I)V")
493  cb = std::bind(
495  std::placeholders::_1,
496  std::placeholders::_2,
497  std::placeholders::_3);
498  else if(f_name == "org.cprover.CProver.getCurrentThreadID:()I")
499  cb = std::bind(
501  std::placeholders::_1,
502  std::placeholders::_2,
503  std::placeholders::_3);
504 
505  if(cb)
506  expr_replacement_map.insert({expr, cb});
507  }
508 
509  if(!expr_replacement_map.empty())
510  {
511  symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first);
512  // Use expr_replacment_map to look for exprt's that need to be replaced.
513  // Once found, get a non-const exprt (breaking sharing in the process) and
514  // call it's associated instrumentation function.
515  for(auto it = w_symbol.value.depth_begin(),
516  itend = w_symbol.value.depth_end(); it != itend;)
517  {
518  expr_replacement_mapt::iterator m_it = expr_replacement_map.find(*it);
519  if(m_it != expr_replacement_map.end())
520  {
521  codet &code = to_code(it.mutate());
522  const code_function_callt &f_code = to_code_function_call(code);
523  m_it->second(f_code, code, symbol_table);
524  it.next_sibling_or_parent();
525 
526  expr_replacement_map.erase(m_it);
527  if(expr_replacement_map.empty())
528  break;
529  }
530  else
531  ++it;
532  }
533  }
534  }
535 }
536 
566  symbol_tablet &symbol_table,
567  message_handlert &message_handler)
568 {
569  namespacet ns(symbol_table);
570  for(const auto &entry : symbol_table)
571  {
572  const symbolt &symbol = entry.second;
573 
574  if(symbol.type.id() != ID_code)
575  continue;
576  if(symbol.value.is_nil())
577  continue;
578  if(!symbol.type.get_bool(ID_is_synchronized))
579  continue;
580 
581  if(symbol.type.get_bool(ID_is_static))
582  {
583  messaget message(message_handler);
584  message.warning() << "Java method '" << entry.first
585  << "' is static and synchronized."
586  << " This is unsupported, the synchronized keyword"
587  << " will be ignored."
588  << messaget::eom;
589  continue;
590  }
591 
592  // find the object to synchronize on
593  const irep_idt this_id(id2string(symbol.name) + "::this");
594  exprt this_expr(this_id);
595 
596  auto it = symbol_table.symbols.find(this_id);
597 
598  if(it == symbol_table.symbols.end())
599  // failed to find object to synchronize on
600  continue;
601 
602  // get writeable reference and instrument the method
603  symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first);
605  symbol_table, w_symbol, it->second.symbol_expr());
606  }
607 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:150
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
convert_synchronized_methods
void convert_synchronized_methods(symbol_tablet &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
Definition: java_bytecode_concurrency_instrumentation.cpp:565
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
get_thread_block_identifier
static const std::string get_thread_block_identifier(const code_function_callt &f_code)
Retrieves a thread block identifier from a function call to CProver.startThread:(I)V or CProver....
Definition: java_bytecode_concurrency_instrumentation.cpp:84
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
arith_tools.h
java_reference_type
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:89
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:331
thread_id
const std::string thread_id
Definition: java_bytecode_concurrency_instrumentation.cpp:22
typet
The type of an expression, extends irept.
Definition: type.h:29
add_or_get_symbol
static symbolt add_or_get_symbol(symbol_tablet &symbol_table, const irep_idt &name, const irep_idt &base_name, const typet &type, const exprt &value, const bool is_thread_local, const bool is_static_lifetime)
Adds a new symbol to the symbol table if it doesn't exist.
Definition: java_bytecode_concurrency_instrumentation.cpp:33
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
monitor_exits
static void monitor_exits(codet &code, const codet &monitorexit)
Introduces a monitorexit before every return recursively.
Definition: java_bytecode_concurrency_instrumentation.cpp:133
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
exprt
Base class for all expressions.
Definition: expr.h:53
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
code_push_catcht
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
Definition: std_code.h:2248
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
convert_threadblock
void convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
Definition: java_bytecode_concurrency_instrumentation.cpp:454
messaget::eom
static eomt eom
Definition: message.h:297
get_first_label_id
static const std::string get_first_label_id(const std::string &id)
Retrieve the first label identifier.
Definition: java_bytecode_concurrency_instrumentation.cpp:66
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
code_pop_catcht
Pops an exception handler from the stack of active handlers (i.e.
Definition: std_code.h:2342
namespace.h
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
code_labelt::code
codet & code()
Definition: std_code.h:1393
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
instrument_end_thread
static void instrument_end_thread(const code_function_callt &f_code, codet &code, const symbol_tablet &symbol_table)
Transforms the codet stored in in f_code, which is a call to function CProver.endThread:(I)V into a b...
Definition: java_bytecode_concurrency_instrumentation.cpp:339
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
next_thread_id
const std::string next_thread_id
Definition: java_bytecode_concurrency_instrumentation.cpp:21
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1127
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1375
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
code_push_catcht::exception_list_entryt
Definition: std_code.h:2256
std_types.h
Pre-defined types.
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
code_push_catcht::exception_list
exception_listt & exception_list()
Definition: std_code.h:2303
get_second_label_id
static const std::string get_second_label_id(const std::string &id)
Retrieve the second label identifier.
Definition: java_bytecode_concurrency_instrumentation.cpp:75
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
get_monitor_call
static codet get_monitor_call(const symbol_tablet &symbol_table, bool is_enter, const exprt &object)
Creates a monitorenter/monitorexit code_function_callt for the given synchronization object.
Definition: java_bytecode_concurrency_instrumentation.cpp:101
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
java_int_type
signedbv_typet java_int_type()
Definition: java_types.cpp:32
cprover_prefix.h
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
fresh_java_symbol
symbolt & fresh_java_symbol(const typet &type, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &function_name, symbol_table_baset &symbol_table)
Definition: java_utils.cpp:566
java_bytecode_concurrency_instrumentation.h
goto_symext::ns
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:256
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
code_skipt
A codet representing a skip statement.
Definition: std_code.h:270
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
code_landingpadt
A statement that catches an exception, assigning the exception in flight to an expression (e....
Definition: std_code.h:2379
code_push_catcht::exception_listt
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:2292
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
expr2java
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:455
instrument_start_thread
static void instrument_start_thread(const code_function_callt &f_code, codet &code, symbol_tablet &symbol_table)
Transforms the codet stored in in f_code, which is a call to function CProver.startThread:(I)V into a...
Definition: java_bytecode_concurrency_instrumentation.cpp:269
side_effect_expr_throwt
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:2200
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:256
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
expr2java.h
java_types.h
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
java_utils.h
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:333
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:866
instrument_synchronized_code
static void instrument_synchronized_code(symbol_tablet &symbol_table, symbolt &symbol, const exprt &sync_object)
Transforms the codet stored in symbol.value.
Definition: java_bytecode_concurrency_instrumentation.cpp:206
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
instrument_get_current_thread_id
static void instrument_get_current_thread_id(const code_function_callt &f_code, codet &code, symbol_tablet &symbol_table)
Transforms the codet stored in in f_code, which is a call to function CProver.getCurrentThreadID:()I ...
Definition: java_bytecode_concurrency_instrumentation.cpp:373
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1810
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106