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/std_expr.h>
17 #include <util/symbol_table.h>
18 
20  const symbol_tablet &symbol_table,
21  const typet &src)
22 {
23  if(src.get_bool(ID_C_volatile))
24  return true;
25 
26  if(src.id()==ID_symbol)
27  {
28  symbol_tablet::symbolst::const_iterator s_it=
29  symbol_table.symbols.find(to_symbol_type(src).get_identifier());
30  assert(s_it!=symbol_table.symbols.end());
31  return is_volatile(symbol_table, s_it->second.type);
32  }
33 
34  return false;
35 }
36 
37 void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
38 {
39  Forall_operands(it, expr)
40  nondet_volatile_rhs(symbol_table, *it);
41 
42  if(expr.id()==ID_symbol ||
43  expr.id()==ID_dereference)
44  {
45  if(is_volatile(symbol_table, expr.type()))
46  {
47  typet t=expr.type();
48  t.remove(ID_C_volatile);
49 
50  // replace by nondet
51  side_effect_expr_nondett nondet_expr(t, expr.source_location());
52  expr.swap(nondet_expr);
53  }
54  }
55 }
56 
57 void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
58 {
59  if(expr.id()==ID_if)
60  {
61  nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond());
62  nondet_volatile_lhs(symbol_table, to_if_expr(expr).true_case());
63  nondet_volatile_lhs(symbol_table, to_if_expr(expr).false_case());
64  }
65  else if(expr.id()==ID_index)
66  {
67  nondet_volatile_lhs(symbol_table, to_index_expr(expr).array());
68  nondet_volatile_rhs(symbol_table, to_index_expr(expr).index());
69  }
70  else if(expr.id()==ID_member)
71  {
72  nondet_volatile_lhs(symbol_table, to_member_expr(expr).struct_op());
73  }
74  else if(expr.id()==ID_dereference)
75  {
76  nondet_volatile_rhs(symbol_table, to_dereference_expr(expr).pointer());
77  }
78 }
79 
81  symbol_tablet &symbol_table,
82  goto_programt &goto_program)
83 {
84  namespacet ns(symbol_table);
85 
86  Forall_goto_program_instructions(i_it, goto_program)
87  {
88  goto_programt::instructiont &instruction=*i_it;
89 
90  if(instruction.is_assign())
91  {
92  nondet_volatile_rhs(symbol_table, to_code_assign(instruction.code).rhs());
93  nondet_volatile_lhs(symbol_table, to_code_assign(instruction.code).rhs());
94  }
95  else if(instruction.is_function_call())
96  {
97  // these have arguments and a return LHS
98 
99  code_function_callt &code_function_call=
100  to_code_function_call(instruction.code);
101 
102  // do arguments
103  for(exprt::operandst::iterator
104  it=code_function_call.arguments().begin();
105  it!=code_function_call.arguments().end();
106  it++)
107  nondet_volatile_rhs(symbol_table, *it);
108 
109  // do return value
110  nondet_volatile_lhs(symbol_table, code_function_call.lhs());
111  }
112  else if(instruction.is_assert() ||
113  instruction.is_assume() ||
114  instruction.is_goto())
115  {
116  // do guard
117  nondet_volatile_rhs(symbol_table, instruction.guard);
118  }
119  }
120 }
121 
122 void nondet_volatile(goto_modelt &goto_model)
123 {
124  Forall_goto_functions(f_it, goto_model.goto_functions)
125  nondet_volatile(goto_model.symbol_table, f_it->second.body);
126 
127  goto_model.goto_functions.update();
128 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3538
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:193
The type of an expression, extends irept.
Definition: type.h:27
const irep_idt & get_identifier() const
Definition: std_expr.h:187
const symbol_typet & to_symbol_type(const typet &type)
Cast a typet to a symbol_typet.
Definition: std_types.h:98
typet & type()
Return the type of the expression.
Definition: expr.h:68
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:228
void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3453
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
const irep_idt & id() const
Definition: irep.h:256
argumentst & arguments()
Definition: std_code.h:1109
exprt & rhs()
Definition: std_code.h:274
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:4014
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
codet representation of a function call statement.
Definition: std_code.h:1036
Volatile Variables.
Author: Diffblue Ltd.
const symbolst & symbols
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
Base class for all expressions.
Definition: expr.h:54
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:228
void swap(irept &irep)
Definition: irep.h:300
#define Forall_operands(it, expr)
Definition: expr.h:26
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
void remove(const irep_namet &name)
Definition: irep.cpp:258
bool is_volatile(const symbol_tablet &symbol_table, const typet &src)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1664
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173