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 = to_code(instr->code);
96  if(code.get_statement() != ID_function_call)
97  {
98  return nondet_instruction_infot();
99  }
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 = to_code_assign(instr.code).rhs();
151  return is_symbol_with_id(rhs, identifier) ||
152  is_typecast_with_id(rhs, identifier);
153 }
154 
176  const goto_programt::targett &target)
177 {
178  // Check whether this is a nondet library method, and return if not
179  const auto instr_info = get_nondet_instruction_info(target);
180  const auto next_instr = std::next(target);
181  if(
182  instr_info.get_instruction_type() ==
184  {
185  return next_instr;
186  }
187 
188  // If we haven't removed returns yet, our function call will have a variable
189  // on its left hand side.
190  const bool remove_returns_not_run =
191  to_code_function_call(target->code).lhs().is_not_nil();
192 
193  irep_idt return_identifier;
194  if(remove_returns_not_run)
195  {
196  return_identifier =
197  to_symbol_expr(to_code_function_call(target->code).lhs())
198  .get_identifier();
199  }
200  else
201  {
202  // If not, we need to look at the next line instead.
204  next_instr->is_assign(),
205  "the code_function_callt for a nondet-returning library function should "
206  "either have a variable for the return value in its lhs() or the next "
207  "instruction should be an assignment of the return value to a temporary "
208  "variable");
209  const exprt &return_value_assignment =
210  to_code_assign(next_instr->code).lhs();
211 
212  // If the assignment is null, return.
213  if(
214  !(return_value_assignment.id() == ID_symbol &&
215  !return_value_assignment.has_operands()))
216  {
217  return next_instr;
218  }
219 
220  // Otherwise it's the temporary variable.
221  return_identifier =
222  to_symbol_expr(return_value_assignment).get_identifier();
223  }
224 
225  // Look for the assignment of the temporary return variable into our target
226  // variable.
227  const auto end = goto_program.instructions.end();
228  auto assignment_instruction = std::find_if(
229  next_instr,
230  end,
231  [&return_identifier](const goto_programt::instructiont &instr) {
232  return is_assignment_from(instr, return_identifier);
233  });
234 
235  INVARIANT(
236  assignment_instruction != end,
237  "failed to find assignment of the temporary return variable into our "
238  "target variable");
239 
240  // Assume that the LHS of *this* assignment is the actual nondet variable
241  const auto &code_assign = to_code_assign(assignment_instruction->code);
242  const auto nondet_var = code_assign.lhs();
243  const auto source_loc = target->source_location;
244 
245  // Erase from the nondet function call to the assignment
246  const auto after_matching_assignment = std::next(assignment_instruction);
247  INVARIANT(
248  after_matching_assignment != end,
249  "goto_program missing END_FUNCTION instruction");
250 
251  std::for_each(
252  target, after_matching_assignment, [](goto_programt::instructiont &instr) {
253  instr.make_skip();
254  });
255 
256  const auto inserted = goto_program.insert_before(after_matching_assignment);
257  inserted->make_assignment();
258  side_effect_expr_nondett inserted_expr(nondet_var.type());
259  inserted_expr.set_nullable(
260  instr_info.get_nullable_type() ==
262  inserted->code = code_assignt(nondet_var, inserted_expr);
263  inserted->code.add_source_location() = source_loc;
264  inserted->source_location = source_loc;
265 
267 
268  return after_matching_assignment;
269 }
270 
276 {
277  for(auto instruction_iterator = goto_program.instructions.begin(),
278  end = goto_program.instructions.end();
279  instruction_iterator != end;)
280  {
281  instruction_iterator =
282  check_and_replace_target(goto_program, instruction_iterator);
283  }
284 }
285 
287 {
288  goto_programt &program = function.get_goto_function().body;
289  replace_java_nondet(program);
290 
291  remove_skip(program);
292 }
293 
295 {
296  for(auto &goto_program : goto_functions.function_map)
297  {
298  replace_java_nondet(goto_program.second.body);
299  }
300 
301  remove_skip(goto_functions);
302 }
303 
305 {
307 }
void update()
Update all indices.
Holds information about any discovered nondet methods, with extreme type- safety. ...
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
targett insert_before(const_targett target)
Insertion before the given target.
Definition: goto_program.h:473
const irep_idt & get_identifier() const
Definition: std_expr.h:128
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)
Definition: invariant.h:205
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
void set_nullable(bool nullable)
Definition: std_code.h:1315
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
const irep_idt & id() const
Definition: irep.h:189
#define FALSE
Definition: driver.h:8
exprt & lhs()
Definition: std_code.h:208
Symbol Table + CFG.
instructionst::iterator targett
Definition: goto_program.h:397
is_nondett get_instruction_type() const
exprt & rhs()
Definition: std_code.h:213
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
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:398
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 &#39;nondet&#39; library functions ...
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
A function call.
Definition: std_code.h:828
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
Replace Java Nondet expressions.
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:70
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:848
Base class for all expressions.
Definition: expr.h:42
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 a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
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.
goto_programt & goto_program
Definition: cover.cpp:63
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
#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...
Program Transformation.
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
operandst & operands()
Definition: expr.h:66
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
Assignment.
Definition: std_code.h:195
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:147
is_nullablet get_nullable_type() const