CBMC
replace_java_nondet.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Replace Java Nondet expressions
4 
5 Author: Reuben Thomas, reuben.thomas@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #include "replace_java_nondet.h"
13 
16 
17 #include <util/std_code.h>
18 
19 #include <algorithm>
20 #include <regex>
21 
25 {
26 public:
27  enum class is_nondett : bool
28  {
29  FALSE,
30  TRUE
31  };
32  enum class is_nullablet : bool
33  {
34  FALSE,
35  TRUE
36  };
37 
39  : is_nondet(is_nondett::FALSE), is_nullable(is_nullablet::FALSE)
40  {
41  }
42 
45  {
46  }
47 
49  {
50  return is_nondet;
51  }
53  {
54  return is_nullable;
55  }
56 
57 private:
60 };
61 
69 {
70  const auto &function_symbol = to_symbol_expr(function_call.function());
71  const auto function_name = id2string(function_symbol.get_identifier());
72  const std::regex reg(
73  R"(.*org\.cprover\.CProver\.nondet)"
74  R"((?:Boolean|Byte|Char|Short|Int|Long|Float|Double|With(out)?Null.*))");
75  std::smatch match_results;
76  if(!std::regex_match(function_name, match_results, reg))
77  {
78  return nondet_instruction_infot();
79  }
80 
82  nondet_instruction_infot::is_nullablet(!match_results[1].matched));
83 }
84 
91 {
92  if(!(instr->is_function_call() && instr->code().id() == ID_code))
93  {
94  return nondet_instruction_infot();
95  }
96  const auto &code = instr->code();
97  INVARIANT(
98  code.get_statement() == ID_function_call,
99  "function_call should have ID_function_call");
100  const auto &function_call = to_code_function_call(code);
101  return is_nondet_returning_object(function_call);
102 }
103 
108 static bool is_symbol_with_id(const exprt &expr, const irep_idt &identifier)
109 {
110  return expr.id() == ID_symbol &&
111  to_symbol_expr(expr).get_identifier() == identifier;
112 }
113 
119 static bool is_typecast_with_id(const exprt &expr, const irep_idt &identifier)
120 {
121  if(!(expr.id() == ID_typecast && expr.operands().size() == 1))
122  {
123  return false;
124  }
125  const auto &typecast = to_typecast_expr(expr);
126  if(!(typecast.op().id() == ID_symbol && !typecast.op().has_operands()))
127  {
128  return false;
129  }
130  const auto &op_symbol = to_symbol_expr(typecast.op());
131  // Return whether the typecast has the expected operand
132  return op_symbol.get_identifier() == identifier;
133 }
134 
141 static bool is_assignment_from(
142  const goto_programt::instructiont &instr,
143  const irep_idt &identifier)
144 {
145  // If not an assignment, return false
146  if(!instr.is_assign())
147  {
148  return false;
149  }
150  const auto &rhs = instr.assign_rhs();
151  return is_symbol_with_id(rhs, identifier) ||
152  is_typecast_with_id(rhs, identifier);
153 }
154 
162  const goto_programt::instructiont &instr,
163  const irep_idt &identifier)
164 {
165  if(!instr.is_set_return_value())
166  {
167  return false;
168  }
169  const auto &rhs = instr.return_value();
170  return is_symbol_with_id(rhs, identifier) ||
171  is_typecast_with_id(rhs, identifier);
172 }
173 
197  goto_programt &goto_program,
198  const goto_programt::targett &target)
199 {
200  // Check whether this is a nondet library method, and return if not
201  const auto instr_info = get_nondet_instruction_info(target);
202  const auto next_instr = std::next(target);
203  if(
204  instr_info.get_instruction_type() ==
206  {
207  return next_instr;
208  }
209 
210  // If we haven't removed returns yet, our function call will have a variable
211  // on its left hand side.
212  const bool remove_returns_not_run = target->call_lhs().is_not_nil();
213 
214  irep_idt return_identifier;
215  if(remove_returns_not_run)
216  {
217  return_identifier = to_symbol_expr(target->call_lhs()).get_identifier();
218  }
219  else
220  {
221  // If not, we need to look at the next line instead.
223  next_instr->is_assign(),
224  "the code_function_callt for a nondet-returning library function should "
225  "either have a variable for the return value in its lhs() or the next "
226  "instruction should be an assignment of the return value to a temporary "
227  "variable");
228  const exprt &return_value_assignment = next_instr->assign_lhs();
229 
230  // If the assignment is null, return.
231  if(
232  !(return_value_assignment.id() == ID_symbol &&
233  !return_value_assignment.has_operands()))
234  {
235  return next_instr;
236  }
237 
238  // Otherwise it's the temporary variable.
239  return_identifier =
240  to_symbol_expr(return_value_assignment).get_identifier();
241  }
242 
243  // Look for the assignment of the temporary return variable into our target
244  // variable.
245  const auto end = goto_program.instructions.end();
246  auto target_instruction = std::find_if(
247  next_instr,
248  end,
249  [&return_identifier](const goto_programt::instructiont &instr) {
250  return is_assignment_from(instr, return_identifier);
251  });
252 
253  // If we can't find an assign, it might be a direct return.
254  if(target_instruction == end)
255  {
256  target_instruction = std::find_if(
257  next_instr,
258  end,
259  [&return_identifier](const goto_programt::instructiont &instr) {
260  return is_return_with_variable(instr, return_identifier);
261  });
262  }
263 
264  INVARIANT(
265  target_instruction != end,
266  "failed to find return of the temporary return variable or assignment of "
267  "the temporary return variable into a target variable");
268 
269  std::for_each(
270  target, target_instruction, [](goto_programt::instructiont &instr) {
271  instr.turn_into_skip();
272  });
273 
274  if(target_instruction->is_set_return_value())
275  {
276  const auto &nondet_var = target_instruction->return_value();
277 
278  side_effect_expr_nondett inserted_expr(
279  nondet_var.type(), target_instruction->source_location());
280  inserted_expr.set_nullable(
281  instr_info.get_nullable_type() ==
283  target_instruction->code_nonconst() = code_returnt(inserted_expr);
284  target_instruction->code_nonconst().add_source_location() =
285  target_instruction->source_location();
286  }
287  else if(target_instruction->is_assign())
288  {
289  // Assume that the LHS of *this* assignment is the actual nondet variable
290  const auto &nondet_var = target_instruction->assign_lhs();
291 
292  side_effect_expr_nondett inserted_expr(
293  nondet_var.type(), target_instruction->source_location());
294  inserted_expr.set_nullable(
295  instr_info.get_nullable_type() ==
297  target_instruction->assign_rhs_nonconst() = inserted_expr;
298  }
299 
300  goto_program.update();
301 
302  return std::next(target_instruction);
303 }
304 
309 static void replace_java_nondet(goto_programt &goto_program)
310 {
311  for(auto instruction_iterator = goto_program.instructions.begin(),
312  end = goto_program.instructions.end();
313  instruction_iterator != end;)
314  {
315  instruction_iterator =
316  check_and_replace_target(goto_program, instruction_iterator);
317  }
318 }
319 
324 {
325  goto_programt &program = function.get_goto_function().body;
326  replace_java_nondet(program);
327 
328  remove_skip(program);
329 }
330 
332 {
333  for(auto &goto_program : goto_functions.function_map)
334  {
335  replace_java_nondet(goto_program.second.body);
336  }
337 
338  remove_skip(goto_functions);
339 }
340 
345 {
347 }
goto_instruction_codet representation of a function call statement.
goto_instruction_codet representation of a "return from a function" statement.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:91
operandst & operands()
Definition: expr.h:94
A collection of goto functions.
function_mapt function_map
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:190
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
Definition: goto_program.h:467
bool is_set_return_value() const
Definition: goto_program.h:492
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
Definition: goto_program.h:258
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:214
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
void update()
Update all indices.
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
const irep_idt & id() const
Definition: irep.h:388
Holds information about any discovered nondet methods, with extreme type- safety.
is_nullablet get_nullable_type() const
is_nondett get_instruction_type() const
nondet_instruction_infot(is_nullablet is_nullable)
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
void set_nullable(bool nullable)
Definition: std_code.h:1528
const irep_idt & get_identifier() const
Definition: std_expr.h:160
const code_function_callt & to_code_function_call(const goto_instruction_codet &code)
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:87
Program Transformation.
static nondet_instruction_infot is_nondet_returning_object(const code_function_callt &function_call)
Checks whether the function call is one of our nondet library functions.
static void replace_java_nondet(goto_programt &goto_program)
Checks each instruction in the goto program to see whether it is a method returning nondet.
static bool is_symbol_with_id(const exprt &expr, const irep_idt &identifier)
Return whether the expression is a symbol with the specified identifier.
static bool is_return_with_variable(const goto_programt::instructiont &instr, const irep_idt &identifier)
Return whether the instruction is a return, and the rhs is a symbol or typecast expression with the s...
static bool is_assignment_from(const goto_programt::instructiont &instr, const irep_idt &identifier)
Return whether the instruction is an assignment, and the rhs is a symbol or typecast expression with ...
static nondet_instruction_infot get_nondet_instruction_info(const goto_programt::const_targett &instr)
Check whether the instruction is a function call which matches one of the recognised nondet library m...
static goto_programt::targett check_and_replace_target(goto_programt &goto_program, const goto_programt::targett &target)
Given an iterator into a list of instructions, modify the list to replace 'nondet' library functions ...
static bool is_typecast_with_id(const exprt &expr, const irep_idt &identifier)
Return whether the expression is a typecast with the specified identifier.
Replace Java Nondet expressions.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2107