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/std_expr.h>
20 #include <util/string_utils.h>
21 #include <util/symbol_table.h>
22 
24 {
25 public:
28  {
29  typecheck_options(options);
30  }
31 
32  void operator()()
33  {
34  if(!all_nondet && nondet_variables.empty() && variable_models.empty())
35  {
36  return;
37  }
38 
40  {
41  nondet_volatile(goto_model.symbol_table, f.second.body);
42  }
43 
45  }
46 
47 private:
48  static bool is_volatile(const namespacet &ns, const typet &src);
49 
51  exprt &expr,
52  const namespacet &ns,
53  goto_programt &pre,
54  goto_programt &post);
55 
57  const symbol_tablet &symbol_table,
58  exprt &expr,
59  goto_programt &pre,
60  goto_programt &post);
61 
63  const symbol_tablet &symbol_table,
64  exprt &expr,
65  goto_programt &pre,
66  goto_programt &post);
67 
68  void
69  nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program);
70 
71  const symbolt &typecheck_variable(const irep_idt &id, const namespacet &ns);
72 
73  void typecheck_model(
74  const irep_idt &id,
75  const symbolt &variable,
76  const namespacet &ns);
77 
78  void typecheck_options(const optionst &options);
79 
81 
82  // configuration obtained from command line options
83  bool all_nondet;
84  std::set<irep_idt> nondet_variables;
85  std::map<irep_idt, irep_idt> variable_models;
86 };
87 
88 bool nondet_volatilet::is_volatile(const namespacet &ns, const typet &src)
89 {
90  if(src.get_bool(ID_C_volatile))
91  return true;
92 
93  if(
94  src.id() == ID_struct_tag || src.id() == ID_union_tag ||
95  src.id() == ID_c_enum_tag)
96  {
97  return is_volatile(ns, ns.follow(src));
98  }
99 
100  return false;
101 }
102 
104  exprt &expr,
105  const namespacet &ns,
106  goto_programt &pre,
107  goto_programt &post)
108 {
109  // Check if we should replace the variable by a nondet expression
110  if(
111  all_nondet ||
112  (expr.id() == ID_symbol &&
113  nondet_variables.count(to_symbol_expr(expr).get_identifier()) != 0))
114  {
115  typet t = expr.type();
116  t.remove(ID_C_volatile);
117 
118  side_effect_expr_nondett nondet_expr(t, expr.source_location());
119  expr.swap(nondet_expr);
120 
121  return;
122  }
123 
124  // Now check if we should replace the variable by a model
125 
126  if(expr.id() != ID_symbol)
127  {
128  return;
129  }
130 
131  const irep_idt &id = to_symbol_expr(expr).get_identifier();
132  const auto &it = variable_models.find(id);
133 
134  if(it == variable_models.end())
135  {
136  return;
137  }
138 
139  const auto &model_symbol = ns.lookup(it->second);
140 
141  const auto &new_variable = get_fresh_aux_symbol(
142  to_code_type(model_symbol.type).return_type(),
143  "",
144  "modelled_volatile",
146  ID_C,
148  .symbol_expr();
149 
150  pre.instructions.push_back(goto_programt::make_decl(new_variable));
151 
152  code_function_callt call(new_variable, model_symbol.symbol_expr(), {});
153  pre.instructions.push_back(goto_programt::make_function_call(call));
154 
155  post.instructions.push_back(goto_programt::make_dead(new_variable));
156 
157  expr = new_variable;
158 }
159 
161  const symbol_tablet &symbol_table,
162  exprt &expr,
163  goto_programt &pre,
164  goto_programt &post)
165 {
166  Forall_operands(it, expr)
167  nondet_volatile_rhs(symbol_table, *it, pre, post);
168 
169  if(expr.id()==ID_symbol ||
170  expr.id()==ID_dereference)
171  {
172  const namespacet ns(symbol_table);
173 
174  if(is_volatile(ns, expr.type()))
175  {
176  handle_volatile_expression(expr, ns, pre, post);
177  }
178  }
179 }
180 
182  const symbol_tablet &symbol_table,
183  exprt &expr,
184  goto_programt &pre,
185  goto_programt &post)
186 {
187  if(expr.id()==ID_if)
188  {
189  nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond(), pre, post);
190  nondet_volatile_lhs(symbol_table, to_if_expr(expr).true_case(), pre, post);
191  nondet_volatile_lhs(symbol_table, to_if_expr(expr).false_case(), pre, post);
192  }
193  else if(expr.id()==ID_index)
194  {
195  nondet_volatile_lhs(symbol_table, to_index_expr(expr).array(), pre, post);
196  nondet_volatile_rhs(symbol_table, to_index_expr(expr).index(), pre, post);
197  }
198  else if(expr.id()==ID_member)
199  {
201  symbol_table, to_member_expr(expr).struct_op(), pre, post);
202  }
203  else if(expr.id()==ID_dereference)
204  {
206  symbol_table, to_dereference_expr(expr).pointer(), pre, post);
207  }
208 }
209 
211  symbol_tablet &symbol_table,
212  goto_programt &goto_program)
213 {
214  namespacet ns(symbol_table);
215 
216  for(auto i_it = goto_program.instructions.begin();
217  i_it != goto_program.instructions.end();
218  i_it++)
219  {
220  goto_programt pre;
221  goto_programt post;
222 
223  goto_programt::instructiont &instruction = *i_it;
224 
225  if(instruction.is_assign())
226  {
228  symbol_table, to_code_assign(instruction.code).rhs(), pre, post);
230  symbol_table, to_code_assign(instruction.code).lhs(), pre, post);
231  }
232  else if(instruction.is_function_call())
233  {
234  // these have arguments and a return LHS
235 
236  code_function_callt &code_function_call=
237  to_code_function_call(instruction.code);
238 
239  // do arguments
240  for(exprt::operandst::iterator
241  it=code_function_call.arguments().begin();
242  it!=code_function_call.arguments().end();
243  it++)
244  nondet_volatile_rhs(symbol_table, *it, pre, post);
245 
246  // do return value
247  nondet_volatile_lhs(symbol_table, code_function_call.lhs(), pre, post);
248  }
249  else if(instruction.has_condition())
250  {
251  // do condition
252  exprt cond = instruction.get_condition();
253  nondet_volatile_rhs(symbol_table, cond, pre, post);
254  instruction.set_condition(cond);
255  }
256 
257  const auto pre_size = pre.instructions.size();
258  goto_program.insert_before_swap(i_it, pre);
259  std::advance(i_it, pre_size);
260 
261  const auto post_size = post.instructions.size();
262  goto_program.destructive_insert(std::next(i_it), post);
263  std::advance(i_it, post_size);
264  }
265 }
266 
267 const symbolt &
269 {
270  const symbolt *symbol;
271 
272  if(ns.lookup(id, symbol))
273  {
275  "given symbol `" + id2string(id) + "` not found in symbol table",
277  }
278 
279  if(!symbol->is_static_lifetime || !symbol->type.get_bool(ID_C_volatile))
280  {
282  "symbol `" + id2string(id) +
283  "` does not represent a volatile variable "
284  "with static lifetime",
286  }
287 
288  INVARIANT(!symbol->is_type, "symbol must not represent a type");
289 
290  INVARIANT(!symbol->is_function(), "symbol must not represent a function");
291 
292  return *symbol;
293 }
294 
296  const irep_idt &id,
297  const symbolt &variable,
298  const namespacet &ns)
299 {
300  const symbolt *symbol;
301 
302  if(ns.lookup(id, symbol))
303  {
305  "given model name " + id2string(id) + " not found in symbol table",
307  }
308 
309  if(!symbol->is_function())
310  {
312  "symbol `" + id2string(id) + "` is not a function",
314  }
315 
316  const auto &code_type = to_code_type(symbol->type);
317 
318  if(variable.type != code_type.return_type())
319  {
321  "return type of model `" + id2string(id) +
322  "` is not compatible with the "
323  "type of the modelled variable " +
324  id2string(variable.name),
326  }
327 
328  if(!code_type.parameters().empty())
329  {
331  "model `" + id2string(id) + "` must not take parameters ",
333  }
334 }
335 
337 {
340  PRECONDITION(variable_models.empty());
341 
343  {
344  all_nondet = true;
345  return;
346  }
347 
349 
351  {
352  const auto &variable_list =
354 
355  nondet_variables.insert(variable_list.begin(), variable_list.end());
356 
357  for(const auto &id : nondet_variables)
358  {
359  typecheck_variable(id, ns);
360  }
361  }
362 
363  if(options.is_set(NONDET_VOLATILE_MODEL_OPT))
364  {
365  const auto &model_list = options.get_list_option(NONDET_VOLATILE_MODEL_OPT);
366 
367  for(const auto &s : model_list)
368  {
369  std::string variable;
370  std::string model;
371 
372  try
373  {
374  split_string(s, ':', variable, model, true);
375  }
376  catch(const deserialization_exceptiont &e)
377  {
379  "cannot split argument `" + s + "` into variable name and model name",
381  }
382 
383  const auto &variable_symbol = typecheck_variable(variable, ns);
384 
385  if(nondet_variables.count(variable) != 0)
386  {
388  "conflicting options for variable `" + variable + "`",
390  }
391 
392  typecheck_model(model, variable_symbol, ns);
393 
394  const auto p = variable_models.insert(std::make_pair(variable, model));
395 
396  if(!p.second && p.first->second != model)
397  {
399  "conflicting models for variable `" + variable + "`",
401  }
402  }
403  }
404 }
405 
406 void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
407 {
411 
412  const bool nondet_volatile_opt = cmdline.isset(NONDET_VOLATILE_OPT);
413  const bool nondet_volatile_variable_opt =
415  const bool nondet_volatile_model_opt =
417 
418  if(
419  nondet_volatile_opt &&
420  (nondet_volatile_variable_opt || nondet_volatile_model_opt))
421  {
424  " cannot be used with --" NONDET_VOLATILE_VARIABLE_OPT
425  " or --" NONDET_VOLATILE_MODEL_OPT,
428  }
429 
430  if(nondet_volatile_opt)
431  {
432  options.set_option(NONDET_VOLATILE_OPT, true);
433  }
434  else
435  {
436  if(nondet_volatile_variable_opt)
437  {
438  options.set_option(
441  }
442 
443  if(nondet_volatile_model_opt)
444  {
445  options.set_option(
448  }
449  }
450 }
451 
452 void nondet_volatile(goto_modelt &goto_model, const optionst &options)
453 {
454  nondet_volatilet nv(goto_model, options);
455  nv();
456 }
nondet_volatilet::typecheck_model
void typecheck_model(const irep_idt &id, const symbolt &variable, const namespacet &ns)
Definition: nondet_volatile.cpp:295
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:336
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
nondet_volatilet::variable_models
std::map< irep_idt, irep_idt > variable_models
Definition: nondet_volatile.cpp:85
goto_programt::make_dead
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:927
NONDET_VOLATILE_OPT
#define NONDET_VOLATILE_OPT
Definition: nondet_volatile.h:21
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
optionst
Definition: options.h:23
string_utils.h
typet
The type of an expression, extends irept.
Definition: type.h:29
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
fresh_symbol.h
Fresh auxiliary symbol creation.
nondet_volatilet
Definition: nondet_volatile.cpp:24
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
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:53
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:181
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:88
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:920
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
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:160
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:1049
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
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
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:40
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
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:677
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
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:111
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
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:103
goto_programt::instructiont::has_condition
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:279
irept::swap
void swap(irept &irep)
Definition: irep.h:463
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:93
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
nondet_volatilet::nondet_volatile
void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
Definition: nondet_volatile.cpp:210
nondet_volatilet::all_nondet
bool all_nondet
Definition: nondet_volatile.cpp:83
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
parse_nondet_volatile_options
void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
Definition: nondet_volatile.cpp:406
nondet_volatilet::nondet_volatilet
nondet_volatilet(goto_modelt &goto_model, const optionst &options)
Definition: nondet_volatile.cpp:26
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:1945
nondet_volatilet::nondet_variables
std::set< irep_idt > nondet_variables
Definition: nondet_volatile.cpp:84
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
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:51
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:268
nondet_volatilet::goto_model
goto_modelt & goto_model
Definition: nondet_volatile.cpp:80
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:460
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:73
goto_programt::instructiont::set_condition
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:292
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
NONDET_VOLATILE_MODEL_OPT
#define NONDET_VOLATILE_MODEL_OPT
Definition: nondet_volatile.h:23
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:606
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:285
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:461
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:452
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:179
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
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:32
validation_modet::INVARIANT
@ INVARIANT