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 
19 static bool is_volatile(const namespacet &ns, const typet &src)
20 {
21  if(src.get_bool(ID_C_volatile))
22  return true;
23 
24  if(
25  src.id() == ID_struct_tag || src.id() == ID_union_tag ||
26  src.id() == ID_c_enum_tag)
27  {
28  return is_volatile(ns, ns.follow(src));
29  }
30 
31  return false;
32 }
33 
34 void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
35 {
36  Forall_operands(it, expr)
37  nondet_volatile_rhs(symbol_table, *it);
38 
39  if(expr.id()==ID_symbol ||
40  expr.id()==ID_dereference)
41  {
42  const namespacet ns(symbol_table);
43  if(is_volatile(ns, expr.type()))
44  {
45  typet t=expr.type();
46  t.remove(ID_C_volatile);
47 
48  // replace by nondet
49  side_effect_expr_nondett nondet_expr(t, expr.source_location());
50  expr.swap(nondet_expr);
51  }
52  }
53 }
54 
55 void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
56 {
57  if(expr.id()==ID_if)
58  {
59  nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond());
60  nondet_volatile_lhs(symbol_table, to_if_expr(expr).true_case());
61  nondet_volatile_lhs(symbol_table, to_if_expr(expr).false_case());
62  }
63  else if(expr.id()==ID_index)
64  {
65  nondet_volatile_lhs(symbol_table, to_index_expr(expr).array());
66  nondet_volatile_rhs(symbol_table, to_index_expr(expr).index());
67  }
68  else if(expr.id()==ID_member)
69  {
70  nondet_volatile_lhs(symbol_table, to_member_expr(expr).struct_op());
71  }
72  else if(expr.id()==ID_dereference)
73  {
74  nondet_volatile_rhs(symbol_table, to_dereference_expr(expr).pointer());
75  }
76 }
77 
79  symbol_tablet &symbol_table,
80  goto_programt &goto_program)
81 {
82  namespacet ns(symbol_table);
83 
84  Forall_goto_program_instructions(i_it, goto_program)
85  {
86  goto_programt::instructiont &instruction=*i_it;
87 
88  if(instruction.is_assign())
89  {
90  nondet_volatile_rhs(symbol_table, to_code_assign(instruction.code).rhs());
91  nondet_volatile_lhs(symbol_table, to_code_assign(instruction.code).rhs());
92  }
93  else if(instruction.is_function_call())
94  {
95  // these have arguments and a return LHS
96 
97  code_function_callt &code_function_call=
98  to_code_function_call(instruction.code);
99 
100  // do arguments
101  for(exprt::operandst::iterator
102  it=code_function_call.arguments().begin();
103  it!=code_function_call.arguments().end();
104  it++)
105  nondet_volatile_rhs(symbol_table, *it);
106 
107  // do return value
108  nondet_volatile_lhs(symbol_table, code_function_call.lhs());
109  }
110  else if(instruction.has_condition())
111  {
112  // do condition
113  exprt cond = instruction.get_condition();
114  nondet_volatile_rhs(symbol_table, cond);
115  instruction.set_condition(cond);
116  }
117  }
118 }
119 
120 void nondet_volatile(goto_modelt &goto_model)
121 {
122  Forall_goto_functions(f_it, goto_model.goto_functions)
123  nondet_volatile(goto_model.symbol_table, f_it->second.body);
124 
125  goto_model.goto_functions.update();
126 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3395
The type of an expression, extends irept.
Definition: type.h:28
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:279
typet & type()
Return the type of the expression.
Definition: expr.h:81
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:102
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:3305
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:386
const irep_idt & id() const
Definition: irep.h:413
argumentst & arguments()
Definition: std_code.h:1183
exprt & rhs()
Definition: std_code.h:320
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:292
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:91
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:3880
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1931
codet representation of a function call statement.
Definition: std_code.h:1129
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:285
Volatile Variables.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
Author: Diffblue Ltd.
static bool is_volatile(const namespacet &ns, const typet &src)
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:52
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:250
void swap(irept &irep)
Definition: irep.h:458
#define Forall_operands(it, expr)
Definition: expr.h:24
#define Forall_goto_program_instructions(it, program)
void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
void remove(const irep_namet &name)
Definition: irep.cpp:131
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1566
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1249