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 
16 
17 #include <algorithm>
18 #include <regex>
19 
23 {
24 public:
25  enum class is_nondett : bool
26  {
27  FALSE,
28  TRUE
29  };
30  enum class is_nullablet : bool
31  {
32  FALSE,
33  TRUE
34  };
35 
38  {
39  }
40 
43  {
44  }
45 
47  {
48  return is_nondet;
49  }
51  {
52  return is_nullable;
53  }
54 
55 private:
58 };
59 
67 {
68  const auto &function_symbol = to_symbol_expr(function_call.function());
69  const auto function_name = id2string(function_symbol.get_identifier());
70  const std::regex reg(
71  R"(.*org\.cprover\.CProver\.nondet)"
72  R"((?:Boolean|Byte|Char|Short|Int|Long|Float|Double|With(out)?Null.*))");
73  std::smatch match_results;
74  if(!std::regex_match(function_name, match_results, reg))
75  {
76  return nondet_instruction_infot();
77  }
78 
80  nondet_instruction_infot::is_nullablet(!match_results[1].matched));
81 }
82 
89 {
90  if(!(instr->is_function_call() && instr->get_code().id() == ID_code))
91  {
92  return nondet_instruction_infot();
93  }
94  const auto &code = instr->get_code();
95  INVARIANT(
96  code.get_statement() == ID_function_call,
97  "function_call should have ID_function_call");
98  const auto &function_call = to_code_function_call(code);
99  return is_nondet_returning_object(function_call);
100 }
101 
106 static bool is_symbol_with_id(const exprt &expr, const irep_idt &identifier)
107 {
108  return expr.id() == ID_symbol &&
109  to_symbol_expr(expr).get_identifier() == identifier;
110 }
111 
117 static bool is_typecast_with_id(const exprt &expr, const irep_idt &identifier)
118 {
119  if(!(expr.id() == ID_typecast && expr.operands().size() == 1))
120  {
121  return false;
122  }
123  const auto &typecast = to_typecast_expr(expr);
124  if(!(typecast.op().id() == ID_symbol && !typecast.op().has_operands()))
125  {
126  return false;
127  }
128  const auto &op_symbol = to_symbol_expr(typecast.op());
129  // Return whether the typecast has the expected operand
130  return op_symbol.get_identifier() == identifier;
131 }
132 
139 static bool is_assignment_from(
140  const goto_programt::instructiont &instr,
141  const irep_idt &identifier)
142 {
143  // If not an assignment, return false
144  if(!instr.is_assign())
145  {
146  return false;
147  }
148  const auto &rhs = instr.get_assign().rhs();
149  return is_symbol_with_id(rhs, identifier) ||
150  is_typecast_with_id(rhs, identifier);
151 }
152 
160  const goto_programt::instructiont &instr,
161  const irep_idt &identifier)
162 {
163  if(!instr.is_set_return_value())
164  {
165  return false;
166  }
167  const auto &rhs = instr.return_value();
168  return is_symbol_with_id(rhs, identifier) ||
169  is_typecast_with_id(rhs, identifier);
170 }
171 
195  goto_programt &goto_program,
196  const goto_programt::targett &target)
197 {
198  // Check whether this is a nondet library method, and return if not
199  const auto instr_info = get_nondet_instruction_info(target);
200  const auto next_instr = std::next(target);
201  if(
202  instr_info.get_instruction_type() ==
204  {
205  return next_instr;
206  }
207 
208  // If we haven't removed returns yet, our function call will have a variable
209  // on its left hand side.
210  const bool remove_returns_not_run = target->call_lhs().is_not_nil();
211 
212  irep_idt return_identifier;
213  if(remove_returns_not_run)
214  {
215  return_identifier = to_symbol_expr(target->call_lhs()).get_identifier();
216  }
217  else
218  {
219  // If not, we need to look at the next line instead.
221  next_instr->is_assign(),
222  "the code_function_callt for a nondet-returning library function should "
223  "either have a variable for the return value in its lhs() or the next "
224  "instruction should be an assignment of the return value to a temporary "
225  "variable");
226  const exprt &return_value_assignment = next_instr->get_assign().lhs();
227 
228  // If the assignment is null, return.
229  if(
230  !(return_value_assignment.id() == ID_symbol &&
231  !return_value_assignment.has_operands()))
232  {
233  return next_instr;
234  }
235 
236  // Otherwise it's the temporary variable.
237  return_identifier =
238  to_symbol_expr(return_value_assignment).get_identifier();
239  }
240 
241  // Look for the assignment of the temporary return variable into our target
242  // variable.
243  const auto end = goto_program.instructions.end();
244  auto target_instruction = std::find_if(
245  next_instr,
246  end,
247  [&return_identifier](const goto_programt::instructiont &instr) {
248  return is_assignment_from(instr, return_identifier);
249  });
250 
251  // If we can't find an assign, it might be a direct return.
252  if(target_instruction == end)
253  {
254  target_instruction = std::find_if(
255  next_instr,
256  end,
257  [&return_identifier](const goto_programt::instructiont &instr) {
258  return is_return_with_variable(instr, return_identifier);
259  });
260  }
261 
262  INVARIANT(
263  target_instruction != end,
264  "failed to find return of the temporary return variable or assignment of "
265  "the temporary return variable into a target variable");
266 
267  std::for_each(
268  target, target_instruction, [](goto_programt::instructiont &instr) {
269  instr.turn_into_skip();
270  });
271 
272  if(target_instruction->is_set_return_value())
273  {
274  const auto &nondet_var = target_instruction->return_value();
275 
276  side_effect_expr_nondett inserted_expr(
277  nondet_var.type(), target_instruction->source_location);
278  inserted_expr.set_nullable(
279  instr_info.get_nullable_type() ==
281  target_instruction->code_nonconst() = code_returnt(inserted_expr);
282  target_instruction->code_nonconst().add_source_location() =
283  target_instruction->source_location;
284  }
285  else if(target_instruction->is_assign())
286  {
287  // Assume that the LHS of *this* assignment is the actual nondet variable
288  const auto &nondet_var = target_instruction->get_assign().lhs();
289 
290  side_effect_expr_nondett inserted_expr(
291  nondet_var.type(), target_instruction->source_location);
292  inserted_expr.set_nullable(
293  instr_info.get_nullable_type() ==
295  target_instruction->code_nonconst() =
296  code_assignt(nondet_var, inserted_expr);
297  target_instruction->code_nonconst().add_source_location() =
298  target_instruction->source_location;
299  }
300 
301  goto_program.update();
302 
303  return std::next(target_instruction);
304 }
305 
310 static void replace_java_nondet(goto_programt &goto_program)
311 {
312  for(auto instruction_iterator = goto_program.instructions.begin(),
313  end = goto_program.instructions.end();
314  instruction_iterator != end;)
315  {
316  instruction_iterator =
317  check_and_replace_target(goto_program, instruction_iterator);
318  }
319 }
320 
325 {
326  goto_programt &program = function.get_goto_function().body;
327  replace_java_nondet(program);
328 
329  remove_skip(program);
330 }
331 
333 {
334  for(auto &goto_program : goto_functions.function_map)
335  {
336  replace_java_nondet(goto_program.second.body);
337  }
338 
339  remove_skip(goto_functions);
340 }
341 
346 {
348 }
A codet representing an assignment in the program.
Definition: std_code.h:293
exprt & rhs()
Definition: std_code.h:315
codet representation of a function call statement.
Definition: std_code.h:1213
exprt & function()
Definition: std_code.h:1248
codet representation of a "return from a function" statement.
Definition: std_code.h:1340
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
operandst & operands()
Definition: expr.h:92
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:183
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
Definition: goto_program.h:513
bool is_set_return_value() const
Definition: goto_program.h:528
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
Definition: goto_program.h:325
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
Definition: goto_program.h:198
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
void update()
Update all indices.
instructionst::iterator targett
Definition: goto_program.h:646
instructionst::const_iterator const_targett
Definition: goto_program.h:647
const irep_idt & id() const
Definition: irep.h:407
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:1966
void set_nullable(bool nullable)
Definition: std_code.h:1974
const irep_idt & get_identifier() const
Definition: std_expr.h:109
#define TRUE
Definition: driver.h:7
#define FALSE
Definition: driver.h:8
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
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:510
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1324
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900