cprover
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 
17 
18 #include <algorithm>
19 #include <regex>
20 
24 {
25 public:
26  enum class is_nondett : bool
27  {
28  FALSE,
29  TRUE
30  };
31  enum class is_nullablet : bool
32  {
33  FALSE,
34  TRUE
35  };
36 
39  {
40  }
41 
44  {
45  }
46 
48  {
49  return is_nondet;
50  }
52  {
53  return is_nullable;
54  }
55 
56 private:
59 };
60 
68 {
69  const auto &function_symbol = to_symbol_expr(function_call.function());
70  const auto function_name = id2string(function_symbol.get_identifier());
71  const std::regex reg(
72  R"(.*org\.cprover\.CProver\.nondet)"
73  R"((?:Boolean|Byte|Char|Short|Int|Long|Float|Double|With(out)?Null.*))");
74  std::smatch match_results;
75  if(!std::regex_match(function_name, match_results, reg))
76  {
77  return nondet_instruction_infot();
78  }
79 
81  nondet_instruction_infot::is_nullablet(!match_results[1].matched));
82 }
83 
90 {
91  if(!(instr->is_function_call() && instr->code.id() == ID_code))
92  {
93  return nondet_instruction_infot();
94  }
95  const auto &code = instr->code;
96  INVARIANT(
97  code.get_statement() == ID_function_call,
98  "function_call should have ID_function_call");
99  const auto &function_call = to_code_function_call(code);
100  return is_nondet_returning_object(function_call);
101 }
102 
107 static bool is_symbol_with_id(const exprt &expr, const irep_idt &identifier)
108 {
109  return expr.id() == ID_symbol &&
110  to_symbol_expr(expr).get_identifier() == identifier;
111 }
112 
118 static bool is_typecast_with_id(const exprt &expr, const irep_idt &identifier)
119 {
120  if(!(expr.id() == ID_typecast && expr.operands().size() == 1))
121  {
122  return false;
123  }
124  const auto &typecast = to_typecast_expr(expr);
125  if(!(typecast.op().id() == ID_symbol && !typecast.op().has_operands()))
126  {
127  return false;
128  }
129  const auto &op_symbol = to_symbol_expr(typecast.op());
130  // Return whether the typecast has the expected operand
131  return op_symbol.get_identifier() == identifier;
132 }
133 
140 static bool is_assignment_from(
141  const goto_programt::instructiont &instr,
142  const irep_idt &identifier)
143 {
144  // If not an assignment, return false
145  if(!instr.is_assign())
146  {
147  return false;
148  }
149  const auto &rhs = to_code_assign(instr.code).rhs();
150  return is_symbol_with_id(rhs, identifier) ||
151  is_typecast_with_id(rhs, identifier);
152 }
153 
161  const goto_programt::instructiont &instr,
162  const irep_idt &identifier)
163 {
164  if(!instr.is_return())
165  {
166  return false;
167  }
168  const auto &rhs = to_code_return(instr.code).return_value();
169  return is_symbol_with_id(rhs, identifier) ||
170  is_typecast_with_id(rhs, identifier);
171 }
172 
196  goto_programt &goto_program,
197  const goto_programt::targett &target)
198 {
199  // Check whether this is a nondet library method, and return if not
200  const auto instr_info = get_nondet_instruction_info(target);
201  const auto next_instr = std::next(target);
202  if(
203  instr_info.get_instruction_type() ==
205  {
206  return next_instr;
207  }
208 
209  // If we haven't removed returns yet, our function call will have a variable
210  // on its left hand side.
211  const bool remove_returns_not_run =
212  to_code_function_call(target->code).lhs().is_not_nil();
213 
214  irep_idt return_identifier;
215  if(remove_returns_not_run)
216  {
217  return_identifier =
218  to_symbol_expr(to_code_function_call(target->code).lhs())
219  .get_identifier();
220  }
221  else
222  {
223  // If not, we need to look at the next line instead.
225  next_instr->is_assign(),
226  "the code_function_callt for a nondet-returning library function should "
227  "either have a variable for the return value in its lhs() or the next "
228  "instruction should be an assignment of the return value to a temporary "
229  "variable");
230  const exprt &return_value_assignment =
231  to_code_assign(next_instr->code).lhs();
232 
233  // If the assignment is null, return.
234  if(
235  !(return_value_assignment.id() == ID_symbol &&
236  !return_value_assignment.has_operands()))
237  {
238  return next_instr;
239  }
240 
241  // Otherwise it's the temporary variable.
242  return_identifier =
243  to_symbol_expr(return_value_assignment).get_identifier();
244  }
245 
246  // Look for the assignment of the temporary return variable into our target
247  // variable.
248  const auto end = goto_program.instructions.end();
249  auto target_instruction = std::find_if(
250  next_instr,
251  end,
252  [&return_identifier](const goto_programt::instructiont &instr) {
253  return is_assignment_from(instr, return_identifier);
254  });
255 
256  // If we can't find an assign, it might be a direct return.
257  if(target_instruction == end)
258  {
259  target_instruction = std::find_if(
260  next_instr,
261  end,
262  [&return_identifier](const goto_programt::instructiont &instr) {
263  return is_return_with_variable(instr, return_identifier);
264  });
265  }
266 
267  INVARIANT(
268  target_instruction != end,
269  "failed to find return of the temporary return variable or assignment of "
270  "the temporary return variable into a target variable");
271 
272  std::for_each(
273  target, target_instruction, [](goto_programt::instructiont &instr) {
274  instr.make_skip();
275  });
276 
277  if(target_instruction->is_return())
278  {
279  const auto &nondet_var =
280  to_code_return(target_instruction->code).return_value();
281 
282  side_effect_expr_nondett inserted_expr(
283  nondet_var.type(), target_instruction->source_location);
284  inserted_expr.set_nullable(
285  instr_info.get_nullable_type() ==
287  target_instruction->code = code_returnt(inserted_expr);
288  target_instruction->code.add_source_location() =
289  target_instruction->source_location;
290  }
291  else if(target_instruction->is_assign())
292  {
293  // Assume that the LHS of *this* assignment is the actual nondet variable
294  const auto &nondet_var = to_code_assign(target_instruction->code).lhs();
295 
296  side_effect_expr_nondett inserted_expr(
297  nondet_var.type(), target_instruction->source_location);
298  inserted_expr.set_nullable(
299  instr_info.get_nullable_type() ==
301  target_instruction->code = code_assignt(nondet_var, inserted_expr);
302  target_instruction->code.add_source_location() =
303  target_instruction->source_location;
304  }
305 
306  goto_program.update();
307 
308  return std::next(target_instruction);
309 }
310 
315 static void replace_java_nondet(goto_programt &goto_program)
316 {
317  for(auto instruction_iterator = goto_program.instructions.begin(),
318  end = goto_program.instructions.end();
319  instruction_iterator != end;)
320  {
321  instruction_iterator =
322  check_and_replace_target(goto_program, instruction_iterator);
323  }
324 }
325 
330 {
331  goto_programt &program = function.get_goto_function().body;
332  replace_java_nondet(program);
333 
334  remove_skip(program);
335 }
336 
338 {
339  for(auto &goto_program : goto_functions.function_map)
340  {
341  replace_java_nondet(goto_program.second.body);
342  }
343 
344  remove_skip(goto_functions);
345 }
346 
351 {
353 }
void update()
Update all indices.
const exprt & return_value() const
Definition: std_code.h:1205
Holds information about any discovered nondet methods, with extreme type- safety.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
const irep_idt & get_identifier() const
Definition: std_expr.h:176
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 ...
function_mapt function_map
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:400
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
void set_nullable(bool nullable)
Definition: std_code.h:1655
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
const irep_idt & id() const
Definition: irep.h:259
#define FALSE
Definition: driver.h:8
exprt & lhs()
Definition: std_code.h:269
Symbol Table + CFG.
instructionst::iterator targett
Definition: goto_program.h:414
is_nondett get_instruction_type() const
exprt & rhs()
Definition: std_code.h:274
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
static bool is_symbol_with_id(const exprt &expr, const irep_idt &identifier)
Return whether the expression is a symbol with the specified identifier.
instructionst::const_iterator const_targett
Definition: goto_program.h:415
nondet_instruction_infot(is_nullablet is_nullable)
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 ...
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1238
codet representation of a function call statement.
Definition: std_code.h:1036
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
Replace Java Nondet expressions.
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 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...
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
static bool is_typecast_with_id(const exprt &expr, const irep_idt &identifier)
Return whether the expression is a typecast with the specified identifier.
exprt & function()
Definition: std_code.h:1099
Base class for all expressions.
Definition: expr.h:54
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
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.
#define TRUE
Definition: driver.h:7
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.
codet representation of a "return from a function" statement.
Definition: std_code.h:1191
Program Transformation.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
operandst & operands()
Definition: expr.h:78
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
A codet representing an assignment in the program.
Definition: std_code.h:256
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:153
is_nullablet get_nullable_type() const