CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
convert_java_nondet.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Convert side_effect_expr_nondett expressions
4
5Author: Reuben Thomas, reuben.thomas@diffblue.com
6
7\*******************************************************************/
8
11
12#include "convert_java_nondet.h"
13
16
18
19#include "java_object_factory.h" // gen_nondet_init
21#include "java_utils.h"
22
25static bool is_nondet_pointer(exprt expr)
26{
27 // If the expression type doesn't have a subtype then I guess it's primitive
28 // and we do not want to convert it. If the type is a ptr-to-void or a
29 // function pointer then we also do not want to convert it.
30 const typet &type = expr.type();
32 type.id() == ID_pointer &&
33 to_pointer_type(type).base_type().id() != ID_empty &&
34 to_pointer_type(type).base_type().id() != ID_code;
37}
38
44 symbol_table_baset &symbol_table,
45 message_handlert &message_handler,
46 const java_object_factory_parameterst &object_factory_parameters,
47 const irep_idt &mode)
48{
50 const bool skip_classid = true;
54 symbol_table,
58 object_factory_parameters,
60 message_handler);
61
62 goto_programt instructions;
64 gen_nondet_init_code, symbol_table, instructions, message_handler, mode);
65 return instructions;
66}
67
81static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
82 const irep_idt &function_identifier,
83 goto_programt &goto_program,
84 const goto_programt::targett &target,
85 symbol_table_baset &symbol_table,
86 message_handlert &message_handler,
87 java_object_factory_parameterst object_factory_parameters,
88 const irep_idt &mode)
89{
90 const auto next_instr = std::next(target);
91
92 // We only expect to find nondets in the rhs of an assignments, and in return
93 // statements if remove_returns has not been run, but we do a more general
94 // check on all operands in case this changes
95 for(exprt &op : target->code_nonconst().operands())
96 {
97 if(!is_nondet_pointer(op))
98 {
99 continue;
100 }
101
102 const auto &nondet_expr = to_side_effect_expr_nondet(op);
103
104 if(!nondet_expr.get_nullable())
105 object_factory_parameters.min_null_tree_depth = 1;
106
107 const source_locationt &source_loc = target->source_location();
108
109 // Currently the code looks like this
110 // target: instruction containing op
111 // When we are done it will look like this
112 // target : declare aux_symbol
113 // . <gen_nondet_init_instructions - many lines>
114 // . <gen_nondet_init_instructions - many lines>
115 // . <gen_nondet_init_instructions - many lines>
116 // target2: instruction containing op, with op replaced by aux_symbol
117 // dead aux_symbol
118
120 op.type(), "nondet_tmp", source_loc, function_identifier, symbol_table);
121
122 const symbol_exprt aux_symbol_expr = aux_symbol.symbol_expr();
123 op = aux_symbol_expr;
124
125 // Insert an instruction declaring `aux_symbol` before `target`, being
126 // careful to preserve jumps to `target`
129 goto_program.insert_before_swap(target, decl_aux_symbol);
130
131 // Keep track of the new location of the instruction containing op.
132 const goto_programt::targett target2 = std::next(target);
133
138 symbol_table,
139 message_handler,
140 object_factory_parameters,
141 mode);
143
144 goto_program.insert_after(
146
147 // In theory target could have more than one operand which should be
148 // replaced by convert_nondet, so we return target2 so that it
149 // will be checked again
150 return std::make_pair(target2, true);
151 }
152
153 return std::make_pair(next_instr, false);
154}
155
167 const irep_idt &function_identifier,
168 goto_programt &goto_program,
169 symbol_table_baset &symbol_table,
170 message_handlert &message_handler,
172 const irep_idt &mode)
173{
174 java_object_factory_parameterst object_factory_parameters =
176 object_factory_parameters.function_id = function_identifier;
177
178 bool changed = false;
179 auto instruction_iterator = goto_program.instructions.begin();
180
181 while(instruction_iterator != goto_program.instructions.end())
182 {
184 function_identifier,
185 goto_program,
187 symbol_table,
188 message_handler,
189 object_factory_parameters,
190 mode);
192 changed |= ret.second;
193 }
194
195 if(changed)
196 {
197 goto_program.update();
198 }
199}
200
202 goto_model_functiont &function,
203 message_handlert &message_handler,
204 const java_object_factory_parameterst &object_factory_parameters,
205 const irep_idt &mode)
206{
208 function.get_function_id(),
209 function.get_goto_function().body,
210 function.get_symbol_table(),
211 message_handler,
212 object_factory_parameters,
213 mode);
214
215 function.compute_location_numbers();
216}
217
219 goto_functionst &goto_functions,
220 symbol_table_baset &symbol_table,
221 message_handlert &message_handler,
222 const java_object_factory_parameterst &object_factory_parameters)
223{
224 const namespacet ns(symbol_table);
225
226 for(auto &f_it : goto_functions.function_map)
227 {
228 const symbolt &symbol=ns.lookup(f_it.first);
229
230 if(symbol.mode==ID_java)
231 {
233 f_it.first,
234 f_it.second.body,
235 symbol_table,
236 message_handler,
237 object_factory_parameters,
238 symbol.mode);
239 }
240 }
241
242 goto_functions.compute_location_numbers();
243
244 remove_skip(goto_functions);
245}
246
248 goto_modelt &goto_model,
249 message_handlert &message_handler,
250 const java_object_factory_parameterst &object_factory_parameters)
251{
253 goto_model.goto_functions,
254 goto_model.symbol_table,
255 message_handler,
256 object_factory_parameters);
257}
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A codet representing sequential composition of program statements.
Definition std_code.h:130
A goto_instruction_codet representing the declaration of a local variable.
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
typet & type()
Return the type of the expression.
Definition expr.h:84
A collection of goto functions.
function_mapt function_map
void compute_location_numbers()
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition goto_model.h:190
const irep_idt & get_function_id()
Get function id.
Definition goto_model.h:239
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition goto_model.h:232
void compute_location_numbers()
Re-number our goto_function.
Definition goto_model.h:216
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition goto_model.h:225
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
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.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void update()
Update all indices.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
instructionst::iterator targett
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
const irep_idt & id() const
Definition irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression to hold a symbol (variable)
Definition std_expr.h:131
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
irep_idt mode
Language mode.
Definition symbol.h:49
The type of an expression, extends irept.
Definition type.h:29
static bool is_nondet_pointer(exprt expr)
Returns true if expr is a nondet pointer that isn't a function pointer or a void* pointer as these ca...
static std::pair< goto_programt::targett, bool > insert_nondet_init_code(const irep_idt &function_identifier, goto_programt &goto_program, const goto_programt::targett &target, symbol_table_baset &symbol_table, message_handlert &message_handler, java_object_factory_parameterst object_factory_parameters, const irep_idt &mode)
Checks an instruction to see whether it contains an assignment from side_effect_expr_nondet.
static goto_programt get_gen_nondet_init_instructions(const symbol_exprt &aux_symbol_expr, const source_locationt &source_loc, symbol_table_baset &symbol_table, message_handlert &message_handler, const java_object_factory_parameterst &object_factory_parameters, const irep_idt &mode)
Populate instructions with goto instructions to nondet init aux_symbol_expr
void convert_nondet(const irep_idt &function_identifier, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler, const java_object_factory_parameterst &user_object_factory_parameters, const irep_idt &mode)
For each instruction in the goto program, checks if it is an assignment from nondet and replaces it w...
Convert side_effect_expr_nondett expressions using java_object_factory.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Program Transformation.
Symbol Table + CFG.
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place, message_handlert &log)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
symbolt & fresh_java_symbol(const typet &type, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &function_name, symbol_table_baset &symbol_table)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
Definition std_code.h:1540
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
Definition std_code.h:1548
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
size_t min_null_tree_depth
To force a certain depth of non-null objects.