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);
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,
83 {
84  namespacet ns(symbol_table);
85 
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 a generic exprt to an if_exprt.
Definition: std_expr.h:3426
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:188
The type of an expression.
Definition: type.h:22
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
typet & type()
Definition: expr.h:56
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:3328
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
const irep_idt & id() const
Definition: irep.h:189
argumentst & arguments()
Definition: std_code.h:860
exprt & rhs()
Definition: std_code.h:213
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
A function call.
Definition: std_code.h:828
Volatile Variables.
Author: Diffblue Ltd.
const symbolst & symbols
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
Base class for all expressions.
Definition: expr.h:42
#define Forall_goto_functions(it, functions)
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
goto_programt & goto_program
Definition: cover.cpp:63
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
void remove(const irep_namet &name)
Definition: irep.cpp:270
bool is_volatile(const symbol_tablet &symbol_table, const typet &src)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
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:879