cprover
convert_java_nondet.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Convert side_effect_expr_nondett expressions
4 
5 Author: Reuben Thomas, reuben.thomas@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #include "convert_java_nondet.h"
13 
17 
18 #include <util/fresh_symbol.h>
19 #include <util/irep_ids.h>
20 
21 #include <memory>
22 
23 #include "java_object_factory.h" // gen_nondet_init
24 
27 static bool is_nondet_pointer(exprt expr)
28 {
29  // If the expression type doesn't have a subtype then I guess it's primitive
30  // and we do not want to convert it. If the type is a ptr-to-void or a
31  // function pointer then we also do not want to convert it.
32  const typet &type = expr.type();
33  const bool non_void_non_function_pointer = type.id() == ID_pointer &&
34  type.subtype().id() != ID_empty &&
35  type.subtype().id() != ID_code;
37  non_void_non_function_pointer;
38 }
39 
43  const symbol_exprt &aux_symbol_expr,
44  const source_locationt &source_loc,
45  symbol_table_baset &symbol_table,
47  const object_factory_parameterst &object_factory_parameters,
48  const irep_idt &mode)
49 {
50  code_blockt gen_nondet_init_code;
51  const bool skip_classid = true;
53  aux_symbol_expr,
54  gen_nondet_init_code,
55  symbol_table,
56  source_loc,
57  skip_classid,
59  object_factory_parameters,
61 
62  goto_programt instructions;
64  gen_nondet_init_code, symbol_table, instructions, message_handler, mode);
65  return instructions;
66 }
67 
80 static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
82  const goto_programt::targett &target,
83  symbol_table_baset &symbol_table,
85  object_factory_parameterst object_factory_parameters,
86  const irep_idt &mode)
87 {
88  const auto next_instr = std::next(target);
89 
90  // We only expect to find nondets in the rhs of an assignments, and in return
91  // statements if remove_returns has not been run, but we do a more general
92  // check on all operands in case this changes
93  for(exprt &op : target->code.operands())
94  {
95  if(!is_nondet_pointer(op))
96  {
97  continue;
98  }
99 
100  const auto &nondet_expr = to_side_effect_expr_nondet(op);
101 
102  if(!nondet_expr.get_nullable())
103  object_factory_parameters.max_nonnull_tree_depth = 1;
104 
105  const source_locationt &source_loc = target->source_location;
106 
107  // Currently the code looks like this
108  // target: instruction containing op
109  // When we are done it will look like this
110  // target : declare aux_symbol
111  // . <gen_nondet_init_instructions - many lines>
112  // . <gen_nondet_init_instructions - many lines>
113  // . <gen_nondet_init_instructions - many lines>
114  // target2: instruction containing op, with op replaced by aux_symbol
115  // dead aux_symbol
116 
117  symbolt &aux_symbol = get_fresh_aux_symbol(
118  op.type(),
120  "nondet_tmp",
121  source_loc,
122  ID_java,
123  symbol_table);
124 
125  const symbol_exprt aux_symbol_expr = aux_symbol.symbol_expr();
126  op = aux_symbol_expr;
127 
128  // Insert an instruction declaring `aux_symbol` before `target`, being
129  // careful to preserve jumps to `target`
130  goto_programt::instructiont decl_aux_symbol;
131  decl_aux_symbol.make_decl(code_declt(aux_symbol_expr));
132  decl_aux_symbol.source_location = source_loc;
133  goto_program.insert_before_swap(target, decl_aux_symbol);
134 
135  // Keep track of the new location of the instruction containing op.
136  const goto_programt::targett target2 = std::next(target);
137 
138  goto_programt gen_nondet_init_instructions =
140  aux_symbol_expr,
141  source_loc,
142  symbol_table,
144  object_factory_parameters,
145  mode);
146  goto_program.destructive_insert(target2, gen_nondet_init_instructions);
147 
148  goto_programt::targett dead_aux_symbol = goto_program.insert_after(target2);
149  dead_aux_symbol->make_dead();
150  dead_aux_symbol->code = code_deadt(aux_symbol_expr);
151  dead_aux_symbol->source_location = source_loc;
152 
153  // In theory target could have more than one operand which should be
154  // replaced by convert_nondet, so we return target2 so that it
155  // will be checked again
156  return std::make_pair(target2, true);
157  }
158 
159  return std::make_pair(next_instr, false);
160 }
161 
173  symbol_table_baset &symbol_table,
175  const object_factory_parameterst &object_factory_parameters,
176  const irep_idt &mode)
177 {
178  bool changed = false;
179  auto instruction_iterator = goto_program.instructions.begin();
180 
181  while(instruction_iterator != goto_program.instructions.end())
182  {
183  auto ret = insert_nondet_init_code(
184  goto_program,
185  instruction_iterator,
186  symbol_table,
188  object_factory_parameters,
189  mode);
190  instruction_iterator = ret.first;
191  changed |= ret.second;
192  }
193 
194  if(changed)
195  {
197  }
198 }
199 
201  goto_model_functiont &function,
203  const object_factory_parameterst &object_factory_parameters,
204  const irep_idt &mode)
205 {
206  object_factory_parameterst parameters = object_factory_parameters;
207  parameters.function_id = function.get_function_id();
209  function.get_goto_function().body,
210  function.get_symbol_table(),
212  parameters,
213  mode);
214 
215  function.compute_location_numbers();
216 }
217 
219  goto_functionst &goto_functions,
220  symbol_table_baset &symbol_table,
222  const 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  {
232  object_factory_parameterst parameters = object_factory_parameters;
233  parameters.function_id = f_it.first;
235  f_it.second.body,
236  symbol_table,
238  object_factory_parameters,
239  symbol.mode);
240  }
241  }
242 
243  goto_functions.compute_location_numbers();
244 
245  remove_skip(goto_functions);
246 }
247 
249  goto_modelt &goto_model,
251  const object_factory_parameterst& object_factory_parameters)
252 {
254  goto_model.goto_functions,
255  goto_model.symbol_table,
257  object_factory_parameters);
258 }
The type of an expression.
Definition: type.h:22
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
void update()
Update all indices.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:441
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
irep_idt mode
Language mode.
Definition: symbol.h:52
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
Definition: std_code.h:1378
Fresh auxiliary symbol creation.
function_mapt function_map
typet & type()
Definition: expr.h:56
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
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 object_factory_parameterst &object_factory_parameters, const irep_idt &mode)
Populate instructions with goto instructions to nondet init aux_symbol_expr
const irep_idt & id() const
Definition: irep.h:259
Symbol Table + CFG.
void compute_location_numbers()
instructionst::iterator targett
Definition: goto_program.h:397
A declaration of a local variable.
Definition: std_code.h:254
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Convert side_effect_expr_nondett expressions.
targett insert_after(const_targett target)
Insertion after the given target.
Definition: goto_program.h:480
static bool is_nondet_pointer(exprt expr)
Returns true if expr is a nondet pointer that isn&#39;t a function pointer or a void* pointer as these ca...
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
Definition: goto_program.h:495
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
Definition: std_code.h:1370
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
Allocate dynamic objects (using MALLOC)
void convert_nondet(goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler, const object_factory_parameterst &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...
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:182
Base class for all expressions.
Definition: expr.h:42
The symbol table base class interface.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, allocation_typet alloc_type, const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
static std::pair< goto_programt::targett, bool > insert_nondet_init_code(goto_programt &goto_program, const goto_programt::targett &target, symbol_table_baset &symbol_table, message_handlert &message_handler, 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.
Program Transformation.
A removal of a local variable.
Definition: std_code.h:307
static const irep_idt get_function_id(const_targett l)
Definition: goto_program.h:418
goto_programt & goto_program
Definition: cover.cpp:63
Sequential composition.
Definition: std_code.h:89
Expression to hold a symbol (variable)
Definition: std_expr.h:90
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
const typet & subtype() const
Definition: type.h:33
Program Transformation.
operandst & operands()
Definition: expr.h:66
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
size_t max_nonnull_tree_depth
To force a certain depth of non-null objects.
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:147