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.turn_into_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 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
nondet_instruction_infot::nondet_instruction_infot
nondet_instruction_infot()
Definition: replace_java_nondet.cpp:37
nondet_instruction_infot::is_nondet
is_nondett is_nondet
Definition: replace_java_nondet.cpp:57
TRUE
#define TRUE
Definition: driver.h:7
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
nondet_instruction_infot::is_nullablet::FALSE
@ FALSE
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:541
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:53
is_typecast_with_id
static bool is_typecast_with_id(const exprt &expr, const irep_idt &identifier)
Return whether the expression is a typecast with the specified identifier.
Definition: replace_java_nondet.cpp:118
goto_modelt
Definition: goto_model.h:26
nondet_instruction_infot::is_nondett
is_nondett
Definition: replace_java_nondet.cpp:27
goto_convert.h
Program Transformation.
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
nondet_instruction_infot::is_nullablet::TRUE
@ TRUE
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
goto_programt::instructiont::turn_into_skip
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
Definition: goto_program.h:351
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:92
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
side_effect_expr_nondett::set_nullable
void set_nullable(bool nullable)
Definition: std_code.h:1953
is_assignment_from
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 ...
Definition: replace_java_nondet.cpp:140
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
is_return_with_variable
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...
Definition: replace_java_nondet.cpp:160
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
to_code_return
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1359
nondet_instruction_infot::is_nullablet
is_nullablet
Definition: replace_java_nondet.cpp:32
is_symbol_with_id
static bool is_symbol_with_id(const exprt &expr, const irep_idt &identifier)
Return whether the expression is a symbol with the specified identifier.
Definition: replace_java_nondet.cpp:107
FALSE
#define FALSE
Definition: driver.h:8
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
is_nondet_returning_object
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.
Definition: replace_java_nondet.cpp:67
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
nondet_instruction_infot::get_nullable_type
is_nullablet get_nullable_type() const
Definition: replace_java_nondet.cpp:51
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
nondet_instruction_infot::get_instruction_type
is_nondett get_instruction_type() const
Definition: replace_java_nondet.cpp:47
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:460
nondet_instruction_infot::is_nondett::FALSE
@ FALSE
check_and_replace_target
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 ...
Definition: replace_java_nondet.cpp:195
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
replace_java_nondet
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.
Definition: replace_java_nondet.cpp:315
nondet_instruction_infot::is_nullable
is_nullablet is_nullable
Definition: replace_java_nondet.cpp:58
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
nondet_instruction_infot
Holds information about any discovered nondet methods, with extreme type- safety.
Definition: replace_java_nondet.cpp:24
exprt::operands
operandst & operands()
Definition: expr.h:95
get_nondet_instruction_info
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...
Definition: replace_java_nondet.cpp:89
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
remove_skip.h
Program Transformation.
code_returnt::return_value
const exprt & return_value() const
Definition: std_code.h:1320
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
nondet_instruction_infot::is_nondett::TRUE
@ TRUE
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
nondet_instruction_infot::nondet_instruction_infot
nondet_instruction_infot(is_nullablet is_nullable)
Definition: replace_java_nondet.cpp:42
goto_programt::instructiont::is_return
bool is_return() const
Definition: goto_program.h:459
replace_java_nondet.h
Replace Java Nondet expressions.