cprover
nondet_volatile.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Volatile Variables
4 
5 Author: Daniel Kroening
6 
7 Date: September 2011
8 
9 \*******************************************************************/
10 
13 
14 #include "nondet_volatile.h"
15 
16 #include <util/cmdline.h>
17 #include <util/fresh_symbol.h>
18 #include <util/options.h>
19 #include <util/pointer_expr.h>
20 #include <util/std_expr.h>
21 #include <util/string_utils.h>
22 #include <util/symbol_table.h>
23 
25 
27 {
28 public:
31  {
32  typecheck_options(options);
33  }
34 
35  void operator()()
36  {
37  if(!all_nondet && nondet_variables.empty() && variable_models.empty())
38  {
39  return;
40  }
41 
43  {
44  nondet_volatile(goto_model.symbol_table, f.second.body);
45  }
46 
48  }
49 
50 private:
51  static bool is_volatile(const namespacet &ns, const typet &src);
52 
54  exprt &expr,
55  const namespacet &ns,
56  goto_programt &pre,
57  goto_programt &post);
58 
60  const symbol_tablet &symbol_table,
61  exprt &expr,
62  goto_programt &pre,
63  goto_programt &post);
64 
66  const symbol_tablet &symbol_table,
67  exprt &expr,
68  goto_programt &pre,
69  goto_programt &post);
70 
71  void
72  nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program);
73 
74  const symbolt &typecheck_variable(const irep_idt &id, const namespacet &ns);
75 
76  void typecheck_model(
77  const irep_idt &id,
78  const symbolt &variable,
79  const namespacet &ns);
80 
81  void typecheck_options(const optionst &options);
82 
84 
85  // configuration obtained from command line options
86  bool all_nondet;
87  std::set<irep_idt> nondet_variables;
88  std::map<irep_idt, irep_idt> variable_models;
89 };
90 
91 bool nondet_volatilet::is_volatile(const namespacet &ns, const typet &src)
92 {
93  if(src.get_bool(ID_C_volatile))
94  return true;
95 
96  if(
97  src.id() == ID_struct_tag || src.id() == ID_union_tag ||
98  src.id() == ID_c_enum_tag)
99  {
100  return is_volatile(ns, ns.follow(src));
101  }
102 
103  return false;
104 }
105 
107  exprt &expr,
108  const namespacet &ns,
109  goto_programt &pre,
110  goto_programt &post)
111 {
112  // Check if we should replace the variable by a nondet expression
113  if(
114  all_nondet ||
115  (expr.id() == ID_symbol &&
116  nondet_variables.count(to_symbol_expr(expr).get_identifier()) != 0))
117  {
118  typet t = expr.type();
119  t.remove(ID_C_volatile);
120 
121  side_effect_expr_nondett nondet_expr(t, expr.source_location());
122  expr.swap(nondet_expr);
123 
124  return;
125  }
126 
127  // Now check if we should replace the variable by a model
128 
129  if(expr.id() != ID_symbol)
130  {
131  return;
132  }
133 
134  const irep_idt &id = to_symbol_expr(expr).get_identifier();
135  const auto &it = variable_models.find(id);
136 
137  if(it == variable_models.end())
138  {
139  return;
140  }
141 
142  const auto &model_symbol = ns.lookup(it->second);
143 
144  const auto &new_variable = get_fresh_aux_symbol(
145  to_code_type(model_symbol.type).return_type(),
146  "",
147  "modelled_volatile",
149  ID_C,
151  .symbol_expr();
152 
153  pre.instructions.push_back(goto_programt::make_decl(new_variable));
154 
155  code_function_callt call(new_variable, model_symbol.symbol_expr(), {});
156  pre.instructions.push_back(goto_programt::make_function_call(call));
157 
158  post.instructions.push_back(goto_programt::make_dead(new_variable));
159 
160  expr = new_variable;
161 }
162 
164  const symbol_tablet &symbol_table,
165  exprt &expr,
166  goto_programt &pre,
167  goto_programt &post)
168 {
169  Forall_operands(it, expr)
170  nondet_volatile_rhs(symbol_table, *it, pre, post);
171 
172  if(expr.id()==ID_symbol ||
173  expr.id()==ID_dereference)
174  {
175  const namespacet ns(symbol_table);
176 
177  if(is_volatile(ns, expr.type()))
178  {
179  handle_volatile_expression(expr, ns, pre, post);
180  }
181  }
182 }
183 
185  const symbol_tablet &symbol_table,
186  exprt &expr,
187  goto_programt &pre,
188  goto_programt &post)
189 {
190  if(expr.id()==ID_if)
191  {
192  nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond(), pre, post);
193  nondet_volatile_lhs(symbol_table, to_if_expr(expr).true_case(), pre, post);
194  nondet_volatile_lhs(symbol_table, to_if_expr(expr).false_case(), pre, post);
195  }
196  else if(expr.id()==ID_index)
197  {
198  nondet_volatile_lhs(symbol_table, to_index_expr(expr).array(), pre, post);
199  nondet_volatile_rhs(symbol_table, to_index_expr(expr).index(), pre, post);
200  }
201  else if(expr.id()==ID_member)
202  {
204  symbol_table, to_member_expr(expr).struct_op(), pre, post);
205  }
206  else if(expr.id()==ID_dereference)
207  {
209  symbol_table, to_dereference_expr(expr).pointer(), pre, post);
210  }
211 }
212 
214  symbol_tablet &symbol_table,
215  goto_programt &goto_program)
216 {
217  namespacet ns(symbol_table);
218 
219  for(auto i_it = goto_program.instructions.begin();
220  i_it != goto_program.instructions.end();
221  i_it++)
222  {
223  goto_programt pre;
224  goto_programt post;
225 
226  goto_programt::instructiont &instruction = *i_it;
227 
228  if(instruction.is_assign())
229  {
231  symbol_table, instruction.assign_rhs_nonconst(), pre, post);
233  symbol_table, instruction.assign_lhs_nonconst(), pre, post);
234  }
235  else if(instruction.is_function_call())
236  {
237  // these have arguments and a return LHS
238 
239  code_function_callt &code_function_call =
240  to_code_function_call(instruction.code_nonconst());
241 
242  // do arguments
243  for(exprt::operandst::iterator
244  it=code_function_call.arguments().begin();
245  it!=code_function_call.arguments().end();
246  it++)
247  nondet_volatile_rhs(symbol_table, *it, pre, post);
248 
249  // do return value
250  nondet_volatile_lhs(symbol_table, code_function_call.lhs(), pre, post);
251  }
252  else if(instruction.has_condition())
253  {
254  // do condition
255  exprt cond = instruction.get_condition();
256  nondet_volatile_rhs(symbol_table, cond, pre, post);
257  instruction.set_condition(cond);
258  }
259 
260  const auto pre_size = pre.instructions.size();
261  goto_program.insert_before_swap(i_it, pre);
262  std::advance(i_it, pre_size);
263 
264  const auto post_size = post.instructions.size();
265  goto_program.destructive_insert(std::next(i_it), post);
266  std::advance(i_it, post_size);
267  }
268 }
269 
270 const symbolt &
272 {
273  const symbolt *symbol;
274 
275  if(ns.lookup(id, symbol))
276  {
278  "given symbol `" + id2string(id) + "` not found in symbol table",
280  }
281 
282  if(!symbol->is_static_lifetime || !symbol->type.get_bool(ID_C_volatile))
283  {
285  "symbol `" + id2string(id) +
286  "` does not represent a volatile variable "
287  "with static lifetime",
289  }
290 
291  INVARIANT(!symbol->is_type, "symbol must not represent a type");
292 
293  INVARIANT(!symbol->is_function(), "symbol must not represent a function");
294 
295  return *symbol;
296 }
297 
299  const irep_idt &id,
300  const symbolt &variable,
301  const namespacet &ns)
302 {
303  const symbolt *symbol;
304 
305  if(ns.lookup(id, symbol))
306  {
308  "given model name " + id2string(id) + " not found in symbol table",
310  }
311 
312  if(!symbol->is_function())
313  {
315  "symbol `" + id2string(id) + "` is not a function",
317  }
318 
319  const auto &code_type = to_code_type(symbol->type);
320 
321  if(variable.type != code_type.return_type())
322  {
324  "return type of model `" + id2string(id) +
325  "` is not compatible with the "
326  "type of the modelled variable " +
327  id2string(variable.name),
329  }
330 
331  if(!code_type.parameters().empty())
332  {
334  "model `" + id2string(id) + "` must not take parameters ",
336  }
337 }
338 
340 {
343  PRECONDITION(variable_models.empty());
344 
346  {
347  all_nondet = true;
348  return;
349  }
350 
352 
354  {
355  const auto &variable_list =
357 
358  nondet_variables.insert(variable_list.begin(), variable_list.end());
359 
360  for(const auto &id : nondet_variables)
361  {
362  typecheck_variable(id, ns);
363  }
364  }
365 
366  if(options.is_set(NONDET_VOLATILE_MODEL_OPT))
367  {
368  const auto &model_list = options.get_list_option(NONDET_VOLATILE_MODEL_OPT);
369 
370  for(const auto &s : model_list)
371  {
372  std::string variable;
373  std::string model;
374 
375  try
376  {
377  split_string(s, ':', variable, model, true);
378  }
379  catch(const deserialization_exceptiont &e)
380  {
382  "cannot split argument `" + s + "` into variable name and model name",
384  }
385 
386  const auto &variable_symbol = typecheck_variable(variable, ns);
387 
388  if(nondet_variables.count(variable) != 0)
389  {
391  "conflicting options for variable `" + variable + "`",
393  }
394 
395  typecheck_model(model, variable_symbol, ns);
396 
397  const auto p = variable_models.insert(std::make_pair(variable, model));
398 
399  if(!p.second && p.first->second != model)
400  {
402  "conflicting models for variable `" + variable + "`",
404  }
405  }
406  }
407 }
408 
409 void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
410 {
414 
415  const bool nondet_volatile_opt = cmdline.isset(NONDET_VOLATILE_OPT);
416  const bool nondet_volatile_variable_opt =
418  const bool nondet_volatile_model_opt =
420 
421  if(
422  nondet_volatile_opt &&
423  (nondet_volatile_variable_opt || nondet_volatile_model_opt))
424  {
427  " cannot be used with --" NONDET_VOLATILE_VARIABLE_OPT
428  " or --" NONDET_VOLATILE_MODEL_OPT,
431  }
432 
433  if(nondet_volatile_opt)
434  {
435  options.set_option(NONDET_VOLATILE_OPT, true);
436  }
437  else
438  {
439  if(nondet_volatile_variable_opt)
440  {
441  options.set_option(
444  }
445 
446  if(nondet_volatile_model_opt)
447  {
448  options.set_option(
451  }
452  }
453 }
454 
455 void nondet_volatile(goto_modelt &goto_model, const optionst &options)
456 {
457  nondet_volatilet nv(goto_model, options);
458  nv();
459 }
nondet_volatilet::typecheck_model
void typecheck_model(const irep_idt &id, const symbolt &variable, const namespacet &ns)
Definition: nondet_volatile.cpp:298
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
nondet_volatilet::typecheck_options
void typecheck_options(const optionst &options)
Definition: nondet_volatile.cpp:339
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
nondet_volatilet::variable_models
std::map< irep_idt, irep_idt > variable_models
Definition: nondet_volatile.cpp:88
goto_programt::make_dead
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:985
NONDET_VOLATILE_OPT
#define NONDET_VOLATILE_OPT
Definition: nondet_volatile.h:23
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
optionst
Definition: options.h:23
string_utils.h
typet
The type of an expression, extends irept.
Definition: type.h:28
fresh_symbol.h
Fresh auxiliary symbol creation.
nondet_volatilet
Definition: nondet_volatile.cpp:27
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
deserialization_exceptiont
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Definition: exception_utils.h:73
goto_programt::instructiont::assign_lhs_nonconst
exprt & assign_lhs_nonconst()
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:212
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
nondet_volatilet::nondet_volatile_lhs
void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr, goto_programt &pre, goto_programt &post)
Definition: nondet_volatile.cpp:184
options.h
Options.
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
nondet_volatilet::is_volatile
static bool is_volatile(const namespacet &ns, const typet &src)
Definition: nondet_volatile.cpp:91
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:978
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1238
nondet_volatilet::nondet_volatile_rhs
void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr, goto_programt &pre, goto_programt &post)
Definition: nondet_volatile.cpp:163
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
NONDET_VOLATILE_VARIABLE_OPT
#define NONDET_VOLATILE_VARIABLE_OPT
Definition: nondet_volatile.h:24
goto_programt::make_function_call
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition: goto_program.h:1107
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1213
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:58
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition: string_utils.cpp:39
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
cmdlinet
Definition: cmdline.h:21
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:744
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
symbolt::is_function
bool is_function() const
Definition: symbol.h:100
optionst::is_set
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
Definition: options.cpp:62
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
pointer_expr.h
API to expression classes for Pointers.
nondet_volatilet::handle_volatile_expression
void handle_volatile_expression(exprt &expr, const namespacet &ns, goto_programt &pre, goto_programt &post)
Definition: nondet_volatile.cpp:106
goto_programt::instructiont::has_condition
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:441
irept::swap
void swap(irept &irep)
Definition: irep.h:453
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
irept::id
const irep_idt & id() const
Definition: irep.h:407
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:96
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1324
nondet_volatilet::nondet_volatile
void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
Definition: nondet_volatile.cpp:213
nondet_volatilet::all_nondet
bool all_nondet
Definition: nondet_volatile.cpp:86
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1258
parse_nondet_volatile_options
void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
Definition: nondet_volatile.cpp:409
nondet_volatilet::nondet_volatilet
nondet_volatilet(goto_modelt &goto_model, const optionst &options)
Definition: nondet_volatile.cpp:29
source_locationt
Definition: source_location.h:19
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
nondet_volatilet::nondet_variables
std::set< irep_idt > nondet_variables
Definition: nondet_volatile.cpp:87
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
cmdline.h
symbolt
Symbol table entry.
Definition: symbol.h:28
goto_programt::instructiont::assign_rhs_nonconst
exprt & assign_rhs_nonconst()
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:226
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
symbolt::is_type
bool is_type
Definition: symbol.h:61
nondet_volatilet::typecheck_variable
const symbolt & typecheck_variable(const irep_idt &id, const namespacet &ns)
Definition: nondet_volatile.cpp:271
nondet_volatilet::goto_model
goto_modelt & goto_model
Definition: nondet_volatile.cpp:83
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:529
nondet_volatile.h
Volatile Variables.
goto_functionst::update
void update()
Definition: goto_functions.h:83
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
goto_programt::instructiont::set_condition
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:454
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:645
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
NONDET_VOLATILE_MODEL_OPT
#define NONDET_VOLATILE_MODEL_OPT
Definition: nondet_volatile.h:25
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:673
symbol_table.h
Author: Diffblue Ltd.
goto_programt::instructiont::get_condition
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:447
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:530
nondet_volatile
void nondet_volatile(goto_modelt &goto_model, const optionst &options)
Havoc reads from volatile expressions, if enabled in the options.
Definition: nondet_volatile.cpp:455
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:230
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_programt::instructiont::code_nonconst
codet & code_nonconst()
Set the code represented by this instruction.
Definition: goto_program.h:191
get_fresh_aux_symbol
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, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Definition: fresh_symbol.cpp:32
optionst::get_list_option
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:80
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
nondet_volatilet::operator()
void operator()()
Definition: nondet_volatile.cpp:35