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 {
26 public:
29  {
30  typecheck_options(options);
31  }
32 
33  void operator()()
34  {
35  if(!all_nondet && nondet_variables.empty() && variable_models.empty())
36  {
37  return;
38  }
39 
41  {
42  nondet_volatile(goto_model.symbol_table, f.second.body);
43  }
44 
46  }
47 
48 private:
49  static bool is_volatile(const namespacet &ns, const typet &src);
50 
52  exprt &expr,
53  const namespacet &ns,
54  goto_programt &pre,
55  goto_programt &post);
56 
58  const symbol_tablet &symbol_table,
59  exprt &expr,
60  goto_programt &pre,
61  goto_programt &post);
62 
64  const symbol_tablet &symbol_table,
65  exprt &expr,
66  goto_programt &pre,
67  goto_programt &post);
68 
69  void
70  nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program);
71 
72  const symbolt &typecheck_variable(const irep_idt &id, const namespacet &ns);
73 
74  void typecheck_model(
75  const irep_idt &id,
76  const symbolt &variable,
77  const namespacet &ns);
78 
79  void typecheck_options(const optionst &options);
80 
82 
83  // configuration obtained from command line options
84  bool all_nondet;
85  std::set<irep_idt> nondet_variables;
86  std::map<irep_idt, irep_idt> variable_models;
87 };
88 
89 bool nondet_volatilet::is_volatile(const namespacet &ns, const typet &src)
90 {
91  if(src.get_bool(ID_C_volatile))
92  return true;
93 
94  if(
95  src.id() == ID_struct_tag || src.id() == ID_union_tag ||
96  src.id() == ID_c_enum_tag)
97  {
98  return is_volatile(ns, ns.follow(src));
99  }
100 
101  return false;
102 }
103 
105  exprt &expr,
106  const namespacet &ns,
107  goto_programt &pre,
108  goto_programt &post)
109 {
110  // Check if we should replace the variable by a nondet expression
111  if(
112  all_nondet ||
113  (expr.id() == ID_symbol &&
114  nondet_variables.count(to_symbol_expr(expr).get_identifier()) != 0))
115  {
116  typet t = expr.type();
117  t.remove(ID_C_volatile);
118 
119  side_effect_expr_nondett nondet_expr(t, expr.source_location());
120  expr.swap(nondet_expr);
121 
122  return;
123  }
124 
125  // Now check if we should replace the variable by a model
126 
127  if(expr.id() != ID_symbol)
128  {
129  return;
130  }
131 
132  const irep_idt &id = to_symbol_expr(expr).get_identifier();
133  const auto &it = variable_models.find(id);
134 
135  if(it == variable_models.end())
136  {
137  return;
138  }
139 
140  const auto &model_symbol = ns.lookup(it->second);
141 
142  const auto &new_variable = get_fresh_aux_symbol(
143  to_code_type(model_symbol.type).return_type(),
144  "",
145  "modelled_volatile",
147  ID_C,
149  .symbol_expr();
150 
151  pre.instructions.push_back(goto_programt::make_decl(new_variable));
152 
153  code_function_callt call(new_variable, model_symbol.symbol_expr(), {});
154  pre.instructions.push_back(goto_programt::make_function_call(call));
155 
156  post.instructions.push_back(goto_programt::make_dead(new_variable));
157 
158  expr = new_variable;
159 }
160 
162  const symbol_tablet &symbol_table,
163  exprt &expr,
164  goto_programt &pre,
165  goto_programt &post)
166 {
167  Forall_operands(it, expr)
168  nondet_volatile_rhs(symbol_table, *it, pre, post);
169 
170  if(expr.id()==ID_symbol ||
171  expr.id()==ID_dereference)
172  {
173  const namespacet ns(symbol_table);
174 
175  if(is_volatile(ns, expr.type()))
176  {
177  handle_volatile_expression(expr, ns, pre, post);
178  }
179  }
180 }
181 
183  const symbol_tablet &symbol_table,
184  exprt &expr,
185  goto_programt &pre,
186  goto_programt &post)
187 {
188  if(expr.id()==ID_if)
189  {
190  nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond(), pre, post);
191  nondet_volatile_lhs(symbol_table, to_if_expr(expr).true_case(), pre, post);
192  nondet_volatile_lhs(symbol_table, to_if_expr(expr).false_case(), pre, post);
193  }
194  else if(expr.id()==ID_index)
195  {
196  nondet_volatile_lhs(symbol_table, to_index_expr(expr).array(), pre, post);
197  nondet_volatile_rhs(symbol_table, to_index_expr(expr).index(), pre, post);
198  }
199  else if(expr.id()==ID_member)
200  {
202  symbol_table, to_member_expr(expr).struct_op(), pre, post);
203  }
204  else if(expr.id()==ID_dereference)
205  {
207  symbol_table, to_dereference_expr(expr).pointer(), pre, post);
208  }
209 }
210 
212  symbol_tablet &symbol_table,
213  goto_programt &goto_program)
214 {
215  namespacet ns(symbol_table);
216 
217  for(auto i_it = goto_program.instructions.begin();
218  i_it != goto_program.instructions.end();
219  i_it++)
220  {
221  goto_programt pre;
222  goto_programt post;
223 
224  goto_programt::instructiont &instruction = *i_it;
225 
226  if(instruction.is_assign())
227  {
229  symbol_table,
230  to_code_assign(instruction.code_nonconst()).rhs(),
231  pre,
232  post);
234  symbol_table,
235  to_code_assign(instruction.code_nonconst()).lhs(),
236  pre,
237  post);
238  }
239  else if(instruction.is_function_call())
240  {
241  // these have arguments and a return LHS
242 
243  code_function_callt &code_function_call =
244  to_code_function_call(instruction.code_nonconst());
245 
246  // do arguments
247  for(exprt::operandst::iterator
248  it=code_function_call.arguments().begin();
249  it!=code_function_call.arguments().end();
250  it++)
251  nondet_volatile_rhs(symbol_table, *it, pre, post);
252 
253  // do return value
254  nondet_volatile_lhs(symbol_table, code_function_call.lhs(), pre, post);
255  }
256  else if(instruction.has_condition())
257  {
258  // do condition
259  exprt cond = instruction.get_condition();
260  nondet_volatile_rhs(symbol_table, cond, pre, post);
261  instruction.set_condition(cond);
262  }
263 
264  const auto pre_size = pre.instructions.size();
265  goto_program.insert_before_swap(i_it, pre);
266  std::advance(i_it, pre_size);
267 
268  const auto post_size = post.instructions.size();
269  goto_program.destructive_insert(std::next(i_it), post);
270  std::advance(i_it, post_size);
271  }
272 }
273 
274 const symbolt &
276 {
277  const symbolt *symbol;
278 
279  if(ns.lookup(id, symbol))
280  {
282  "given symbol `" + id2string(id) + "` not found in symbol table",
284  }
285 
286  if(!symbol->is_static_lifetime || !symbol->type.get_bool(ID_C_volatile))
287  {
289  "symbol `" + id2string(id) +
290  "` does not represent a volatile variable "
291  "with static lifetime",
293  }
294 
295  INVARIANT(!symbol->is_type, "symbol must not represent a type");
296 
297  INVARIANT(!symbol->is_function(), "symbol must not represent a function");
298 
299  return *symbol;
300 }
301 
303  const irep_idt &id,
304  const symbolt &variable,
305  const namespacet &ns)
306 {
307  const symbolt *symbol;
308 
309  if(ns.lookup(id, symbol))
310  {
312  "given model name " + id2string(id) + " not found in symbol table",
314  }
315 
316  if(!symbol->is_function())
317  {
319  "symbol `" + id2string(id) + "` is not a function",
321  }
322 
323  const auto &code_type = to_code_type(symbol->type);
324 
325  if(variable.type != code_type.return_type())
326  {
328  "return type of model `" + id2string(id) +
329  "` is not compatible with the "
330  "type of the modelled variable " +
331  id2string(variable.name),
333  }
334 
335  if(!code_type.parameters().empty())
336  {
338  "model `" + id2string(id) + "` must not take parameters ",
340  }
341 }
342 
344 {
347  PRECONDITION(variable_models.empty());
348 
350  {
351  all_nondet = true;
352  return;
353  }
354 
356 
358  {
359  const auto &variable_list =
361 
362  nondet_variables.insert(variable_list.begin(), variable_list.end());
363 
364  for(const auto &id : nondet_variables)
365  {
366  typecheck_variable(id, ns);
367  }
368  }
369 
370  if(options.is_set(NONDET_VOLATILE_MODEL_OPT))
371  {
372  const auto &model_list = options.get_list_option(NONDET_VOLATILE_MODEL_OPT);
373 
374  for(const auto &s : model_list)
375  {
376  std::string variable;
377  std::string model;
378 
379  try
380  {
381  split_string(s, ':', variable, model, true);
382  }
383  catch(const deserialization_exceptiont &e)
384  {
386  "cannot split argument `" + s + "` into variable name and model name",
388  }
389 
390  const auto &variable_symbol = typecheck_variable(variable, ns);
391 
392  if(nondet_variables.count(variable) != 0)
393  {
395  "conflicting options for variable `" + variable + "`",
397  }
398 
399  typecheck_model(model, variable_symbol, ns);
400 
401  const auto p = variable_models.insert(std::make_pair(variable, model));
402 
403  if(!p.second && p.first->second != model)
404  {
406  "conflicting models for variable `" + variable + "`",
408  }
409  }
410  }
411 }
412 
413 void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
414 {
418 
419  const bool nondet_volatile_opt = cmdline.isset(NONDET_VOLATILE_OPT);
420  const bool nondet_volatile_variable_opt =
422  const bool nondet_volatile_model_opt =
424 
425  if(
426  nondet_volatile_opt &&
427  (nondet_volatile_variable_opt || nondet_volatile_model_opt))
428  {
431  " cannot be used with --" NONDET_VOLATILE_VARIABLE_OPT
432  " or --" NONDET_VOLATILE_MODEL_OPT,
435  }
436 
437  if(nondet_volatile_opt)
438  {
439  options.set_option(NONDET_VOLATILE_OPT, true);
440  }
441  else
442  {
443  if(nondet_volatile_variable_opt)
444  {
445  options.set_option(
448  }
449 
450  if(nondet_volatile_model_opt)
451  {
452  options.set_option(
455  }
456  }
457 }
458 
459 void nondet_volatile(goto_modelt &goto_model, const optionst &options)
460 {
461  nondet_volatilet nv(goto_model, options);
462  nv();
463 }
nondet_volatilet::typecheck_model
void typecheck_model(const irep_idt &id, const symbolt &variable, const namespacet &ns)
Definition: nondet_volatile.cpp:302
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:343
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
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:86
goto_programt::make_dead
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:911
NONDET_VOLATILE_OPT
#define NONDET_VOLATILE_OPT
Definition: nondet_volatile.h:21
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:442
optionst
Definition: options.h:23
string_utils.h
typet
The type of an expression, extends irept.
Definition: type.h:28
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
fresh_symbol.h
Fresh auxiliary symbol creation.
nondet_volatilet
Definition: nondet_volatile.cpp:25
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2151
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
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:182
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:89
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:904
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1240
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:161
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
NONDET_VOLATILE_VARIABLE_OPT
#define NONDET_VOLATILE_VARIABLE_OPT
Definition: nondet_volatile.h:22
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:1033
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:141
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
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:738
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:661
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:464
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:122
pointer_expr.h
API to expression classes for Pointers.
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
nondet_volatilet::handle_volatile_expression
void handle_volatile_expression(exprt &expr, const namespacet &ns, goto_programt &pre, goto_programt &post)
Definition: nondet_volatile.cpp:104
goto_programt::instructiont::has_condition
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:357
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:102
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
nondet_volatilet::nondet_volatile
void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
Definition: nondet_volatile.cpp:211
nondet_volatilet::all_nondet
bool all_nondet
Definition: nondet_volatile.cpp:84
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
parse_nondet_volatile_options
void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
Definition: nondet_volatile.cpp:413
nondet_volatilet::nondet_volatilet
nondet_volatilet(goto_modelt &goto_model, const optionst &options)
Definition: nondet_volatile.cpp:27
source_locationt
Definition: source_location.h:20
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
nondet_volatilet::nondet_variables
std::set< irep_idt > nondet_variables
Definition: nondet_volatile.cpp:85
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:569
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:52
cmdline.h
symbolt
Symbol table entry.
Definition: symbol.h:28
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:275
nondet_volatilet::goto_model
goto_modelt & goto_model
Definition: nondet_volatile.cpp:81
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:444
nondet_volatile.h
Volatile Variables.
goto_functionst::update
void update()
Definition: goto_functions.h:81
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:74
goto_programt::instructiont::set_condition
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:370
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:639
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2611
NONDET_VOLATILE_MODEL_OPT
#define NONDET_VOLATILE_MODEL_OPT
Definition: nondet_volatile.h:23
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:590
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:363
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:445
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:459
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:180
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:238
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:193
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:33