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 
36  const goto_programt::targett &target,
37  symbol_table_baset &symbol_table,
39  object_factory_parameterst object_factory_parameters,
40  const irep_idt &mode)
41 {
42  // Return if the instruction isn't an assignment
43  const auto next_instr=std::next(target);
44  if(!target->is_assign())
45  {
46  return next_instr;
47  }
48 
49  // Return if the rhs of the assignment isn't a side effect expression
50  const auto &assign=to_code_assign(target->code);
51  if(assign.rhs().id()!=ID_side_effect)
52  {
53  return next_instr;
54  }
55 
56  // Return if the rhs isn't nondet
57  const auto &side_effect=to_side_effect_expr(assign.rhs());
58  if(side_effect.get_statement()!=ID_nondet)
59  {
60  return next_instr;
61  }
62 
63  const auto lhs=assign.lhs();
64  // If the lhs type doesn't have a subtype then I guess it's primitive and
65  // we want to bail out now
66  if(!lhs.type().has_subtype())
67  {
68  return next_instr;
69  }
70 
71  // Although, if the type is a ptr-to-void then we also want to bail
72  if(lhs.type().subtype().id()==ID_empty ||
73  lhs.type().subtype().id()==ID_code)
74  {
75  return next_instr;
76  }
77 
78  // Check whether the nondet object may be null
79  if(!to_side_effect_expr_nondet(side_effect).get_nullable())
80  object_factory_parameters.max_nonnull_tree_depth = 1;
81  // Get the symbol to nondet-init
82  const auto source_loc=target->source_location;
83 
84  // Erase the nondet assignment
85  target->make_skip();
86 
87  // Generate nondet init code
88  code_blockt init_code;
90  lhs,
91  init_code,
92  symbol_table,
93  source_loc,
94  true,
96  object_factory_parameters,
98 
99  // Convert this code into goto instructions
100  goto_programt new_instructions;
101  goto_convert(
102  init_code, symbol_table, new_instructions, message_handler, mode);
103 
104  // Insert the new instructions into the instruction list
105  goto_program.destructive_insert(next_instr, new_instructions);
107 
108  return next_instr;
109 }
110 
120  symbol_table_baset &symbol_table,
122  const object_factory_parameterst &object_factory_parameters,
123  const irep_idt &mode)
124 {
125  for(auto instruction_iterator=goto_program.instructions.begin(),
126  end=goto_program.instructions.end();
127  instruction_iterator!=end;)
128  {
129  instruction_iterator = insert_nondet_init_code(
130  goto_program,
131  instruction_iterator,
132  symbol_table,
134  object_factory_parameters,
135  mode);
136  }
137 }
138 
140  goto_model_functiont &function,
142  const object_factory_parameterst &object_factory_parameters,
143  const irep_idt &mode)
144 {
145  object_factory_parameterst parameters = object_factory_parameters;
146  parameters.function_id = function.get_function_id();
148  function.get_goto_function().body,
149  function.get_symbol_table(),
151  parameters,
152  mode);
153 
154  function.compute_location_numbers();
155 }
156 
158  goto_functionst &goto_functions,
159  symbol_table_baset &symbol_table,
161  const object_factory_parameterst &object_factory_parameters)
162 {
163  const namespacet ns(symbol_table);
164 
165  for(auto &f_it : goto_functions.function_map)
166  {
167  const symbolt &symbol=ns.lookup(f_it.first);
168 
169  if(symbol.mode==ID_java)
170  {
171  object_factory_parameterst parameters = object_factory_parameters;
172  parameters.function_id = f_it.first;
174  f_it.second.body,
175  symbol_table,
177  object_factory_parameters,
178  symbol.mode);
179  }
180  }
181 
182  goto_functions.compute_location_numbers();
183 
184  remove_skip(goto_functions);
185 }
186 
188  goto_modelt &goto_model,
190  const object_factory_parameterst& object_factory_parameters)
191 {
193  goto_model.goto_functions,
194  goto_model.symbol_table,
196  object_factory_parameters);
197 }
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
void update()
Update all indices.
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
bool get_nullable() const
Definition: std_code.h:1320
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:1335
Fresh auxiliary symbol creation.
function_mapt function_map
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
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1287
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
Symbol Table + CFG.
void compute_location_numbers()
instructionst::iterator targett
Definition: goto_program.h:397
static goto_programt::targett 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.
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.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
Definition: goto_program.h:495
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...
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...
Program Transformation.
goto_programt & goto_program
Definition: cover.cpp:63
Sequential composition.
Definition: std_code.h:88
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
Program Transformation.
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:130
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