CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
replace_java_nondet.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Replace Java Nondet expressions
4
5Author: 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
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 {
79 }
80
83}
84
91{
92 if(!(instr->is_function_call() && instr->code().id() == ID_code))
93 {
95 }
96 const auto &code = instr->code();
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
108static 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
119static 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
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
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
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(
233 !return_value_assignment.has_operands()))
234 {
235 return next_instr;
236 }
237
238 // Otherwise it's the temporary variable.
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(
248 end,
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(
258 end,
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(
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
279 nondet_var.type(), target_instruction->source_location());
280 inserted_expr.set_nullable(
281 instr_info.get_nullable_type() ==
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
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
309static 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 {
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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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
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_functiont & get_goto_function()
Get GOTO function.
Definition goto_model.h:232
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void update()
Update all indices.
instructionst::iterator targett
instructionst::const_iterator const_targett
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
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
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 typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272