cprover
java_bytecode_convert_threadblock.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 
13 #include <util/expr_iterator.h>
14 #include <util/namespace.h>
15 #include <util/cprover_prefix.h>
16 #include <util/std_types.h>
17 #include <util/arith_tools.h>
18 
19 // Disable linter to allow an std::string constant.
20 const std::string next_thread_id = CPROVER_PREFIX "_next_thread_id";// NOLINT(*)
21 const std::string thread_id = CPROVER_PREFIX "_thread_id";// NOLINT(*)
22 
33  symbol_tablet &symbol_table,
34  const irep_idt &name,
35  const irep_idt &base_name,
36  const typet &type,
37  const exprt &value,
38  const bool is_thread_local,
39  const bool is_static_lifetime)
40 {
41  const symbolt* psymbol = nullptr;
42  namespacet ns(symbol_table);
43  ns.lookup(name, psymbol);
44  if(psymbol != nullptr)
45  return *psymbol;
46  symbolt new_symbol;
47  new_symbol.name = name;
48  new_symbol.pretty_name = name;
49  new_symbol.base_name = base_name;
50  new_symbol.type = type;
51  new_symbol.value = value;
52  new_symbol.is_lvalue = true;
53  new_symbol.is_state_var = true;
54  new_symbol.is_static_lifetime = is_static_lifetime;
55  new_symbol.is_thread_local = is_thread_local;
56  new_symbol.mode = ID_java;
57  symbol_table.add(new_symbol);
58  return new_symbol;
59 }
60 
65 static const std::string get_first_label_id(const std::string &id)
66 {
67  return CPROVER_PREFIX "_THREAD_ENTRY_" + id;
68 }
69 
74 static const std::string get_second_label_id(const std::string &id)
75 {
76  return CPROVER_PREFIX "_THREAD_EXIT_" + id;
77 }
78 
83 static const std::string get_thread_block_identifier(
84  const code_function_callt &f_code)
85 {
86  PRECONDITION(f_code.arguments().size() == 1);
87  const exprt &expr = f_code.arguments()[0];
88  mp_integer lbl_id = binary2integer(expr.op0().get_string(ID_value), false);
89  return integer2string(lbl_id);
90 }
91 
102  const code_function_callt &f_code,
103  codet &code,
104  symbol_tablet &symbol_table)
105 {
106  PRECONDITION(f_code.arguments().size() == 1);
107 
108  // Create global variable __CPROVER__next_thread_id. Used as a counter
109  // in-order to to assign ids to new threads.
110  const symbolt &next_symbol =
112  symbol_table, next_thread_id, next_thread_id,
113  java_int_type(),
114  from_integer(0, java_int_type()), false, true);
115 
116  // Create thread-local variable __CPROVER__thread_id. Holds the id of
117  // the thread.
118  const symbolt &current_symbol =
120  symbol_table, thread_id, thread_id, java_int_type(),
121  from_integer(0, java_int_type()), true, true);
122 
123  // Construct appropriate labels.
124  // Note: java does not have labels so this should be safe.
125  const std::string &thread_block_id = get_thread_block_identifier(f_code);
126  const std::string &lbl1 = get_first_label_id(thread_block_id);
127  const std::string &lbl2 = get_second_label_id(thread_block_id);
128 
129  // Instrument the following codet's:
130  //
131  // A: codet(id=ID_start_thread, destination=__CPROVER_THREAD_ENTRY_<ID>)
132  // B: codet(id=ID_goto, destination=__CPROVER_THREAD_EXIT_<ID>)
133  // C: codet(id=ID_label, label=__CPROVER_THREAD_ENTRY_<ID>)
134  // C.1: codet(id=ID_atomic_begin)
135  // D: CPROVER__next_thread_id += 1;
136  // E: __CPROVER__thread_id = __CPROVER__next_thread_id;
137  // F: codet(id=ID_atomic_end)
138 
139  codet tmp_a(ID_start_thread);
140  tmp_a.set(ID_destination, lbl1);
141  code_gotot tmp_b(lbl2);
142  code_labelt tmp_c(lbl1);
143  tmp_c.op0() = codet(ID_skip);
144 
145  exprt plus(ID_plus, java_int_type());
146  plus.copy_to_operands(next_symbol.symbol_expr());
148  code_assignt tmp_d(next_symbol.symbol_expr(), plus);
149  code_assignt tmp_e(current_symbol.symbol_expr(), next_symbol.symbol_expr());
150 
151  code_blockt block;
152  block.add(tmp_a);
153  block.add(tmp_b);
154  block.add(tmp_c);
155  block.add(codet(ID_atomic_begin));
156  block.add(tmp_d);
157  block.add(tmp_e);
158  block.add(codet(ID_atomic_end));
159  block.add_source_location() = f_code.source_location();
160 
161  code = block;
162 }
163 
174  const code_function_callt &f_code,
175  codet &code,
176  symbol_tablet symbol_table)
177 {
178  PRECONDITION(f_code.arguments().size() == 1);
179 
180  // Build id, used to construct appropriate labels.
181  // Note: java does not have labels so this should be safe
182  const std::string &thread_block_id = get_thread_block_identifier(f_code);
183  const std::string &lbl2 = get_second_label_id(thread_block_id);
184 
185  // Instrument the following code:
186  //
187  // A: codet(id=ID_end_thread)
188  // B: codet(id=ID_label,label= __CPROVER_THREAD_EXIT_<ID>)
189  codet tmp_a(ID_end_thread);
190  code_labelt tmp_b(lbl2);
191  tmp_b.op0() = codet(ID_skip);
192 
193  code_blockt block;
194  block.add(tmp_a);
195  block.add(tmp_b);
196  block.add_source_location() = code.source_location();
197 
198  code = block;
199 }
200 
211  const code_function_callt &f_code,
212  codet &code,
213  symbol_tablet symbol_table)
214 {
215  PRECONDITION(f_code.arguments().size() == 0);
216 
217  const symbolt& current_symbol =
218  add_or_get_symbol(symbol_table,
219  thread_id,
220  thread_id,
221  java_int_type(),
223  true, true);
224 
225  code_assignt code_assign(f_code.lhs(), current_symbol.symbol_expr());
226  code_assign.add_source_location() = f_code.source_location();
227 
228  code = code_assign;
229 }
230 
292 {
293  using instrument_callbackt =
294  std::function<void(const code_function_callt&, codet&, symbol_tablet&)>;
295  using expr_replacement_mapt =
296  std::unordered_map<const exprt, instrument_callbackt, irep_hash>;
297 
298  namespacet ns(symbol_table);
299 
300  for(auto entry : symbol_table)
301  {
302  expr_replacement_mapt expr_replacement_map;
303  const symbolt &symbol = entry.second;
304 
305  // Look for code_function_callt's (without breaking sharing)
306  // and insert each one into a replacement map along with an associated
307  // callback that will handle their instrumentation.
308  for(auto it = symbol.value.depth_begin(), itend = symbol.value.depth_end();
309  it != itend; ++it)
310  {
311  instrument_callbackt cb;
312 
313  const exprt &expr = *it;
314  if(expr.id() != ID_code)
315  continue;
316 
317  const codet &code = to_code(expr);
318  if(code.get_statement() != ID_function_call)
319  continue;
320 
321  const code_function_callt &f_code = to_code_function_call(code);
322  const std::string &f_name = expr2java(f_code.function(), ns);
323  if(f_name == "org.cprover.CProver.startThread:(I)V")
324  cb = std::bind(instrument_start_thread, std::placeholders::_1,
325  std::placeholders::_2, std::placeholders::_3);
326  else if(f_name == "org.cprover.CProver.endThread:(I)V")
327  cb = std::bind(&instrument_endThread, std::placeholders::_1,
328  std::placeholders::_2, std::placeholders::_3);
329  else if(f_name == "org.cprover.CProver.getCurrentThreadID:()I")
330  cb = std::bind(&instrument_getCurrentThreadID, std::placeholders::_1,
331  std::placeholders::_2, std::placeholders::_3);
332 
333  if(cb)
334  expr_replacement_map.insert({expr, cb});
335  }
336 
337  if(!expr_replacement_map.empty())
338  {
339  symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first);
340  // Use expr_replacment_map to look for exprt's that need to be replaced.
341  // Once found, get a non-const exprt (breaking sharing in the process) and
342  // call it's associated instrumentation function.
343  for(auto it = w_symbol.value.depth_begin(),
344  itend = w_symbol.value.depth_end(); it != itend;)
345  {
346  expr_replacement_mapt::iterator m_it = expr_replacement_map.find(*it);
347  if(m_it != expr_replacement_map.end())
348  {
349  codet &code = to_code(it.mutate());
350  const code_function_callt &f_code = to_code_function_call(code);
351  m_it->second(f_code, code, symbol_table);
352  it.next_sibling_or_parent();
353 
354  expr_replacement_map.erase(m_it);
355  if(expr_replacement_map.empty())
356  break;
357  }
358  else
359  ++it;
360  }
361  }
362  }
363 }
const irep_idt & get_statement() const
Definition: std_code.h:39
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
static void instrument_getCurrentThreadID(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 ...
BigInt mp_integer
Definition: mp_arith.h:22
bool is_thread_local
Definition: symbol.h:67
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
static void instrument_endThread(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.endThread:(I)V into a b...
exprt & op0()
Definition: expr.h:72
#define CPROVER_PREFIX
irep_idt mode
Language mode.
Definition: symbol.h:52
typet java_int_type()
Definition: java_types.cpp:32
void convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
exprt value
Initial value of symbol.
Definition: symbol.h:37
A ‘goto’ instruction.
Definition: std_code.h:774
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:55
depth_iteratort depth_begin()
Definition: expr.cpp:299
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
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...
bool is_static_lifetime
Definition: symbol.h:67
const irep_idt & id() const
Definition: irep.h:189
void add(const codet &code)
Definition: std_code.h:111
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
static const std::string get_first_label_id(const std::string &id)
Retrieve the first label identifier.
argumentst & arguments()
Definition: std_code.h:860
const std::string next_thread_id
const std::string thread_id
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
A label for branch targets.
Definition: std_code.h:947
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
A function call.
Definition: std_code.h:828
typet type
Type of symbol.
Definition: symbol.h:34
API to type classes.
static const std::string get_second_label_id(const std::string &id)
Retrieve the second label identifier.
exprt & function()
Definition: std_code.h:848
Base class for all expressions.
Definition: expr.h:42
bool is_state_var
Definition: symbol.h:63
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
const source_locationt & source_location() const
Definition: expr.h:125
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&#39;t exist.
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:88
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
depth_iteratort depth_end()
Definition: expr.cpp:301
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
A statement in a programming language.
Definition: std_code.h:21
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
Assignment.
Definition: std_code.h:195
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...
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:455
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879
bool is_lvalue
Definition: symbol.h:68