cprover
Loading...
Searching...
No Matches
nondet_volatile.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Volatile Variables
4
5Author: Daniel Kroening
6
7Date: 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_code.h>
21#include <util/std_expr.h>
22#include <util/string_utils.h>
23#include <util/symbol_table.h>
24
26
28{
29public:
35
37 {
38 if(!all_nondet && nondet_variables.empty() && variable_models.empty())
39 {
40 return;
41 }
42
44 {
46 }
47
49 }
50
51private:
52 static bool is_volatile(const namespacet &ns, const typet &src);
53
55 exprt &expr,
56 const namespacet &ns,
58 goto_programt &post);
59
61 const symbol_tablet &symbol_table,
62 exprt &expr,
64 goto_programt &post);
65
67 const symbol_tablet &symbol_table,
68 exprt &expr,
70 goto_programt &post);
71
72 void
73 nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program);
74
75 const symbolt &typecheck_variable(const irep_idt &id, const namespacet &ns);
76
77 void typecheck_model(
78 const irep_idt &id,
79 const symbolt &variable,
80 const namespacet &ns);
81
82 void typecheck_options(const optionst &options);
83
85
86 // configuration obtained from command line options
88 std::set<irep_idt> nondet_variables;
89 std::map<irep_idt, irep_idt> variable_models;
90};
91
93{
94 if(src.get_bool(ID_C_volatile))
95 return true;
96
97 if(
98 src.id() == ID_struct_tag || src.id() == ID_union_tag ||
99 src.id() == ID_c_enum_tag)
100 {
101 return is_volatile(ns, ns.follow(src));
102 }
103
104 return false;
105}
106
108 exprt &expr,
109 const namespacet &ns,
111 goto_programt &post)
112{
113 // Check if we should replace the variable by a nondet expression
114 if(
115 all_nondet ||
116 (expr.id() == ID_symbol &&
118 {
119 typet t = expr.type();
121
123 expr.swap(nondet_expr);
124
125 return;
126 }
127
128 // Now check if we should replace the variable by a model
129
130 if(expr.id() != ID_symbol)
131 {
132 return;
133 }
134
135 const irep_idt &id = to_symbol_expr(expr).get_identifier();
136 const auto &it = variable_models.find(id);
137
138 if(it == variable_models.end())
139 {
140 return;
141 }
142
143 const auto &model_symbol = ns.lookup(it->second);
144
145 const auto &new_variable = get_fresh_aux_symbol(
147 "",
148 "modelled_volatile",
150 ID_C,
152 .symbol_expr();
153
154 pre.instructions.push_back(goto_programt::make_decl(new_variable));
155
156 code_function_callt call(new_variable, model_symbol.symbol_expr(), {});
157 pre.instructions.push_back(goto_programt::make_function_call(call));
158
159 post.instructions.push_back(goto_programt::make_dead(new_variable));
160
161 expr = new_variable;
162}
163
165 const symbol_tablet &symbol_table,
166 exprt &expr,
168 goto_programt &post)
169{
170 Forall_operands(it, expr)
171 nondet_volatile_rhs(symbol_table, *it, pre, post);
172
173 if(expr.id()==ID_symbol ||
174 expr.id()==ID_dereference)
175 {
176 const namespacet ns(symbol_table);
177
178 if(is_volatile(ns, expr.type()))
179 {
180 handle_volatile_expression(expr, ns, pre, post);
181 }
182 }
183}
184
186 const symbol_tablet &symbol_table,
187 exprt &expr,
189 goto_programt &post)
190{
191 if(expr.id()==ID_if)
192 {
193 nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond(), pre, post);
194 nondet_volatile_lhs(symbol_table, to_if_expr(expr).true_case(), pre, post);
195 nondet_volatile_lhs(symbol_table, to_if_expr(expr).false_case(), pre, post);
196 }
197 else if(expr.id()==ID_index)
198 {
199 nondet_volatile_lhs(symbol_table, to_index_expr(expr).array(), pre, post);
200 nondet_volatile_rhs(symbol_table, to_index_expr(expr).index(), pre, post);
201 }
202 else if(expr.id()==ID_member)
203 {
205 symbol_table, to_member_expr(expr).struct_op(), pre, post);
206 }
207 else if(expr.id()==ID_dereference)
208 {
210 symbol_table, to_dereference_expr(expr).pointer(), pre, post);
211 }
212}
213
215 symbol_tablet &symbol_table,
216 goto_programt &goto_program)
217{
218 namespacet ns(symbol_table);
219
220 for(auto i_it = goto_program.instructions.begin();
221 i_it != goto_program.instructions.end();
222 i_it++)
223 {
225 goto_programt post;
226
227 goto_programt::instructiont &instruction = *i_it;
228
229 if(instruction.is_assign())
230 {
232 symbol_table, instruction.assign_rhs_nonconst(), pre, post);
234 symbol_table, instruction.assign_lhs_nonconst(), pre, post);
235 }
236 else if(instruction.is_function_call())
237 {
238 // these have arguments and a return LHS
239
242
243 // do arguments
244 for(exprt::operandst::iterator
245 it=code_function_call.arguments().begin();
246 it!=code_function_call.arguments().end();
247 it++)
248 nondet_volatile_rhs(symbol_table, *it, pre, post);
249
250 // do return value
251 nondet_volatile_lhs(symbol_table, code_function_call.lhs(), pre, post);
252 }
253 else if(instruction.has_condition())
254 {
255 // do condition
256 exprt cond = instruction.get_condition();
257 nondet_volatile_rhs(symbol_table, cond, pre, post);
258 instruction.set_condition(cond);
259 }
260
261 const auto pre_size = pre.instructions.size();
262 goto_program.insert_before_swap(i_it, pre);
263 std::advance(i_it, pre_size);
264
265 const auto post_size = post.instructions.size();
266 goto_program.destructive_insert(std::next(i_it), post);
267 std::advance(i_it, post_size);
268 }
269}
270
271const symbolt &
273{
274 const symbolt *symbol;
275
276 if(ns.lookup(id, symbol))
277 {
279 "given symbol `" + id2string(id) + "` not found in symbol table",
281 }
282
283 if(!symbol->is_static_lifetime || !symbol->type.get_bool(ID_C_volatile))
284 {
286 "symbol `" + id2string(id) +
287 "` does not represent a volatile variable "
288 "with static lifetime",
290 }
291
292 INVARIANT(!symbol->is_type, "symbol must not represent a type");
293
294 INVARIANT(!symbol->is_function(), "symbol must not represent a function");
295
296 return *symbol;
297}
298
300 const irep_idt &id,
301 const symbolt &variable,
302 const namespacet &ns)
303{
304 const symbolt *symbol;
305
306 if(ns.lookup(id, symbol))
307 {
309 "given model name " + id2string(id) + " not found in symbol table",
311 }
312
313 if(!symbol->is_function())
314 {
316 "symbol `" + id2string(id) + "` is not a function",
318 }
319
320 const auto &code_type = to_code_type(symbol->type);
321
322 if(variable.type != code_type.return_type())
323 {
325 "return type of model `" + id2string(id) +
326 "` is not compatible with the "
327 "type of the modelled variable " +
328 id2string(variable.name),
330 }
331
332 if(!code_type.parameters().empty())
333 {
335 "model `" + id2string(id) + "` must not take parameters ",
337 }
338}
339
341{
345
347 {
348 all_nondet = true;
349 return;
350 }
351
353
355 {
356 const auto &variable_list =
358
359 nondet_variables.insert(variable_list.begin(), variable_list.end());
360
361 for(const auto &id : nondet_variables)
362 {
363 typecheck_variable(id, ns);
364 }
365 }
366
368 {
370
371 for(const auto &s : model_list)
372 {
373 std::string variable;
374 std::string model;
375
376 try
377 {
378 split_string(s, ':', variable, model, true);
379 }
380 catch(const deserialization_exceptiont &e)
381 {
383 "cannot split argument `" + s + "` into variable name and model name",
385 }
386
387 const auto &variable_symbol = typecheck_variable(variable, ns);
388
389 if(nondet_variables.count(variable) != 0)
390 {
392 "conflicting options for variable `" + variable + "`",
394 }
395
397
398 const auto p = variable_models.insert(std::make_pair(variable, model));
399
400 if(!p.second && p.first->second != model)
401 {
403 "conflicting models for variable `" + variable + "`",
405 }
406 }
407 }
408}
409
455
456void nondet_volatile(goto_modelt &goto_model, const optionst &options)
457{
458 nondet_volatilet nv(goto_model, options);
459 nv();
460}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
virtual bool isset(char option) const
Definition cmdline.cpp:30
const std::list< std::string > & get_values(const std::string &option) const
Definition cmdline.cpp:109
codet representation of a function call statement.
const typet & return_type() const
Definition std_types.h:645
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
const source_locationt & source_location() const
Definition expr.h:230
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
bool has_condition() const
Does this instruction have a condition?
codet & code_nonconst()
Set the code represented by this instruction.
exprt & assign_lhs_nonconst()
Get the lhs of the assignment for ASSIGN.
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
exprt & assign_rhs_nonconst()
Get the rhs of the assignment for ASSIGN.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
bool get_bool(const irep_idt &name) const
Definition irep.cpp:58
void remove(const irep_idt &name)
Definition irep.cpp:96
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
goto_modelt & goto_model
void typecheck_model(const irep_idt &id, const symbolt &variable, const namespacet &ns)
std::set< irep_idt > nondet_variables
static bool is_volatile(const namespacet &ns, const typet &src)
void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr, goto_programt &pre, goto_programt &post)
nondet_volatilet(goto_modelt &goto_model, const optionst &options)
void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr, goto_programt &pre, goto_programt &post)
void handle_volatile_expression(exprt &expr, const namespacet &ns, goto_programt &pre, goto_programt &post)
std::map< irep_idt, irep_idt > variable_models
void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
const symbolt & typecheck_variable(const irep_idt &id, const namespacet &ns)
void typecheck_options(const optionst &options)
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
bool get_bool_option(const std::string &option) const
Definition options.cpp:44
void set_option(const std::string &option, const bool value)
Definition options.cpp:28
const value_listt & get_list_option(const std::string &option) const
Definition options.cpp:80
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
const irep_idt & get_identifier() const
Definition std_expr.h:109
The symbol table.
Symbol table entry.
Definition symbol.h:28
bool is_static_lifetime
Definition symbol.h:65
bool is_type
Definition symbol.h:61
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
bool is_function() const
Definition symbol.h:100
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
The type of an expression, extends irept.
Definition type.h:29
#define Forall_operands(it, expr)
Definition expr.h:25
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 ...
Fresh auxiliary symbol creation.
const code_function_callt & to_code_function_call(const codet &code)
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
void nondet_volatile(goto_modelt &goto_model, const optionst &options)
Havoc reads from volatile expressions, if enabled in the options.
Volatile Variables.
#define NONDET_VOLATILE_MODEL_OPT
#define NONDET_VOLATILE_OPT
#define NONDET_VOLATILE_VARIABLE_OPT
Options.
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Author: Diffblue Ltd.