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/irep_ids.h>
19 
20 #include <memory>
21 
22 #include "java_object_factory.h" // gen_nondet_init
23 #include "java_utils.h"
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,
46  message_handlert &message_handler,
47  const java_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  message_handler);
62 
63  goto_programt instructions;
65  gen_nondet_init_code, symbol_table, instructions, message_handler, mode);
66  return instructions;
67 }
68 
82 static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
83  const irep_idt &function_identifier,
84  goto_programt &goto_program,
85  const goto_programt::targett &target,
86  symbol_table_baset &symbol_table,
87  message_handlert &message_handler,
88  java_object_factory_parameterst object_factory_parameters,
89  const irep_idt &mode)
90 {
91  const auto next_instr = std::next(target);
92 
93  // We only expect to find nondets in the rhs of an assignments, and in return
94  // statements if remove_returns has not been run, but we do a more general
95  // check on all operands in case this changes
96  for(exprt &op : target->code.operands())
97  {
98  if(!is_nondet_pointer(op))
99  {
100  continue;
101  }
102 
103  const auto &nondet_expr = to_side_effect_expr_nondet(op);
104 
105  if(!nondet_expr.get_nullable())
106  object_factory_parameters.min_null_tree_depth = 1;
107 
108  const source_locationt &source_loc = target->source_location;
109 
110  // Currently the code looks like this
111  // target: instruction containing op
112  // When we are done it will look like this
113  // target : declare aux_symbol
114  // . <gen_nondet_init_instructions - many lines>
115  // . <gen_nondet_init_instructions - many lines>
116  // . <gen_nondet_init_instructions - many lines>
117  // target2: instruction containing op, with op replaced by aux_symbol
118  // dead aux_symbol
119 
120  symbolt &aux_symbol = fresh_java_symbol(
121  op.type(), "nondet_tmp", source_loc, function_identifier, symbol_table);
122 
123  const symbol_exprt aux_symbol_expr = aux_symbol.symbol_expr();
124  op = aux_symbol_expr;
125 
126  // Insert an instruction declaring `aux_symbol` before `target`, being
127  // careful to preserve jumps to `target`
128  goto_programt::instructiont decl_aux_symbol =
129  goto_programt::make_decl(code_declt(aux_symbol_expr), source_loc);
130  goto_program.insert_before_swap(target, decl_aux_symbol);
131 
132  // Keep track of the new location of the instruction containing op.
133  const goto_programt::targett target2 = std::next(target);
134 
135  goto_programt gen_nondet_init_instructions =
137  aux_symbol_expr,
138  source_loc,
139  symbol_table,
140  message_handler,
141  object_factory_parameters,
142  mode);
143  goto_program.destructive_insert(target2, gen_nondet_init_instructions);
144 
145  goto_program.insert_after(
146  target2, goto_programt::make_dead(aux_symbol_expr, source_loc));
147 
148  // In theory target could have more than one operand which should be
149  // replaced by convert_nondet, so we return target2 so that it
150  // will be checked again
151  return std::make_pair(target2, true);
152  }
153 
154  return std::make_pair(next_instr, false);
155 }
156 
168  const irep_idt &function_identifier,
169  goto_programt &goto_program,
170  symbol_table_baset &symbol_table,
171  message_handlert &message_handler,
172  const java_object_factory_parameterst &user_object_factory_parameters,
173  const irep_idt &mode)
174 {
175  java_object_factory_parameterst object_factory_parameters =
176  user_object_factory_parameters;
177  object_factory_parameters.function_id = function_identifier;
178 
179  bool changed = false;
180  auto instruction_iterator = goto_program.instructions.begin();
181 
182  while(instruction_iterator != goto_program.instructions.end())
183  {
184  auto ret = insert_nondet_init_code(
185  function_identifier,
186  goto_program,
187  instruction_iterator,
188  symbol_table,
189  message_handler,
190  object_factory_parameters,
191  mode);
192  instruction_iterator = ret.first;
193  changed |= ret.second;
194  }
195 
196  if(changed)
197  {
198  goto_program.update();
199  }
200 }
201 
203  goto_model_functiont &function,
204  message_handlert &message_handler,
205  const java_object_factory_parameterst &object_factory_parameters,
206  const irep_idt &mode)
207 {
209  function.get_function_id(),
210  function.get_goto_function().body,
211  function.get_symbol_table(),
212  message_handler,
213  object_factory_parameters,
214  mode);
215 
216  function.compute_location_numbers();
217 }
218 
220  goto_functionst &goto_functions,
221  symbol_table_baset &symbol_table,
222  message_handlert &message_handler,
223  const java_object_factory_parameterst &object_factory_parameters)
224 {
225  const namespacet ns(symbol_table);
226 
227  for(auto &f_it : goto_functions.function_map)
228  {
229  const symbolt &symbol=ns.lookup(f_it.first);
230 
231  if(symbol.mode==ID_java)
232  {
234  f_it.first,
235  f_it.second.body,
236  symbol_table,
237  message_handler,
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,
250  message_handlert &message_handler,
251  const java_object_factory_parameterst &object_factory_parameters)
252 {
254  goto_model.goto_functions,
255  goto_model.symbol_table,
256  message_handler,
257  object_factory_parameters);
258 }
convert_java_nondet.h
Convert side_effect_expr_nondett expressions using java_object_factory.
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
typet::subtype
const typet & subtype() const
Definition: type.h:47
goto_programt::make_dead
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:927
typet
The type of an expression, extends irept.
Definition: type.h:29
object_factory_parameterst::function_id
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
Definition: object_factory_parameters.h:82
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
insert_nondet_init_code
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.
Definition: convert_java_nondet.cpp:82
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:541
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
goto_model.h
Symbol Table + CFG.
goto_functionst::compute_location_numbers
void compute_location_numbers()
Definition: goto_functions.cpp:18
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
goto_convert.h
Program Transformation.
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:920
goto_convert
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Definition: goto_convert.cpp:1846
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
convert_nondet
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...
Definition: convert_java_nondet.cpp:167
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
java_object_factory.h
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
can_cast_expr< side_effect_expr_nondett >
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
Definition: std_code.h:1965
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:677
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
gen_nondet_init
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...
Definition: java_object_factory.cpp:1624
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
fresh_java_symbol
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)
Definition: java_utils.cpp:566
object_factory_parameterst::min_null_tree_depth
size_t min_null_tree_depth
To force a certain depth of non-null objects.
Definition: object_factory_parameters.h:73
source_locationt
Definition: source_location.h:20
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
irep_ids.h
util
symbolt
Symbol table entry.
Definition: symbol.h:28
get_gen_nondet_init_instructions
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
Definition: convert_java_nondet.cpp:42
to_side_effect_expr_nondet
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
Definition: std_code.h:1973
update_in_placet::NO_UPDATE_IN_PLACE
@ NO_UPDATE_IN_PLACE
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_programt::insert_after
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:655
is_nondet_pointer
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...
Definition: convert_java_nondet.cpp:27
lifetimet::DYNAMIC
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
exprt::operands
operandst & operands()
Definition: expr.h:95
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:606
remove_skip.h
Program Transformation.
java_utils.h
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
java_object_factory_parameterst
Definition: java_object_factory_parameters.h:16
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579