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
25
27{
28public:
31 {
32 typecheck_options(options);
33 }
34
36 {
37 if(!all_nondet && nondet_variables.empty() && variable_models.empty())
38 {
39 return;
40 }
41
43 {
45 }
46
48 }
49
50private:
51 static bool is_volatile(const namespacet &ns, const typet &src);
52
54 exprt &expr,
55 const namespacet &ns,
56 goto_programt &pre,
57 goto_programt &post);
58
60 const symbol_table_baset &symbol_table,
61 exprt &expr,
62 goto_programt &pre,
63 goto_programt &post);
64
66 const symbol_table_baset &symbol_table,
67 exprt &expr,
68 goto_programt &pre,
69 goto_programt &post);
70
71 void nondet_volatile(
72 symbol_table_baset &symbol_table,
73 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,
110 goto_programt &pre,
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 &&
117 nondet_variables.count(to_symbol_expr(expr).get_identifier()) != 0))
118 {
119 typet t = expr.type();
120 t.remove(ID_C_volatile);
121
122 side_effect_expr_nondett nondet_expr(t, expr.source_location());
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(
146 to_code_type(model_symbol.type).return_type(),
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(), {});
158
159 post.instructions.push_back(goto_programt::make_dead(new_variable));
160
161 expr = new_variable;
162}
163
165 const symbol_table_baset &symbol_table,
166 exprt &expr,
167 goto_programt &pre,
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_table_baset &symbol_table,
187 exprt &expr,
188 goto_programt &pre,
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_table_baset &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 {
224 goto_programt pre;
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
240 code_function_callt &code_function_call =
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
257 symbol_table, instruction.condition_nonconst(), pre, post);
258 }
259
260 const auto pre_size = pre.instructions.size();
261 goto_program.insert_before_swap(i_it, pre);
262 std::advance(i_it, pre_size);
263
264 const auto post_size = post.instructions.size();
265 goto_program.destructive_insert(std::next(i_it), post);
266 std::advance(i_it, post_size);
267 }
268}
269
270const symbolt &
272{
273 const symbolt *symbol;
274
275 if(ns.lookup(id, symbol))
276 {
278 "given symbol `" + id2string(id) + "` not found in symbol table",
280 }
281
282 if(!symbol->is_static_lifetime || !symbol->type.get_bool(ID_C_volatile))
283 {
285 "symbol `" + id2string(id) +
286 "` does not represent a volatile variable "
287 "with static lifetime",
289 }
290
291 INVARIANT(!symbol->is_type, "symbol must not represent a type");
292
293 INVARIANT(!symbol->is_function(), "symbol must not represent a function");
294
295 return *symbol;
296}
297
299 const irep_idt &id,
300 const symbolt &variable,
301 const namespacet &ns)
302{
303 const symbolt *symbol;
304
305 if(ns.lookup(id, symbol))
306 {
308 "given model name " + id2string(id) + " not found in symbol table",
310 }
311
312 if(!symbol->is_function())
313 {
315 "symbol `" + id2string(id) + "` is not a function",
317 }
318
319 const auto &code_type = to_code_type(symbol->type);
320
321 if(variable.type != code_type.return_type())
322 {
324 "return type of model `" + id2string(id) +
325 "` is not compatible with the "
326 "type of the modelled variable " +
327 id2string(variable.name),
329 }
330
331 if(!code_type.parameters().empty())
332 {
334 "model `" + id2string(id) + "` must not take parameters ",
336 }
337}
338
340{
344
346 {
347 all_nondet = true;
348 return;
349 }
350
352
354 {
355 const auto &variable_list =
357
358 nondet_variables.insert(variable_list.begin(), variable_list.end());
359
360 for(const auto &id : nondet_variables)
361 {
362 typecheck_variable(id, ns);
363 }
364 }
365
367 {
368 const auto &model_list = options.get_list_option(NONDET_VOLATILE_MODEL_OPT);
369
370 for(const auto &s : model_list)
371 {
372 std::string variable;
373 std::string model;
374
375 try
376 {
377 split_string(s, ':', variable, model, true);
378 }
379 catch(const deserialization_exceptiont &e)
380 {
382 "cannot split argument `" + s + "` into variable name and model name",
384 }
385
386 const auto &variable_symbol = typecheck_variable(variable, ns);
387
388 if(nondet_variables.count(variable) != 0)
389 {
391 "conflicting options for variable `" + variable + "`",
393 }
394
395 typecheck_model(model, variable_symbol, ns);
396
397 const auto p = variable_models.insert(std::make_pair(variable, model));
398
399 if(!p.second && p.first->second != model)
400 {
402 "conflicting models for variable `" + variable + "`",
404 }
405 }
406 }
407}
408
409void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
410{
414
415 const bool nondet_volatile_opt = cmdline.isset(NONDET_VOLATILE_OPT);
416 const bool nondet_volatile_variable_opt =
418 const bool nondet_volatile_model_opt =
420
421 if(
422 nondet_volatile_opt &&
423 (nondet_volatile_variable_opt || nondet_volatile_model_opt))
424 {
427 " cannot be used with --" NONDET_VOLATILE_VARIABLE_OPT
431 }
432
433 if(nondet_volatile_opt)
434 {
435 options.set_option(NONDET_VOLATILE_OPT, true);
436 }
437 else
438 {
439 if(nondet_volatile_variable_opt)
440 {
441 options.set_option(
444 }
445
446 if(nondet_volatile_model_opt)
447 {
448 options.set_option(
451 }
452 }
453}
454
455void nondet_volatile(goto_modelt &goto_model, const optionst &options)
456{
457 nondet_volatilet nv(goto_model, options);
458 nv();
459}
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
goto_instruction_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:39
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
const source_locationt & source_location() const
Definition expr.h:223
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
bool has_condition() const
Does this instruction have a condition?
exprt & assign_lhs_nonconst()
Get the lhs of the assignment for ASSIGN.
goto_instruction_codet & code_nonconst()
Set the code represented by this instruction.
exprt & condition_nonconst()
Get 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:57
void remove(const irep_idt &name)
Definition irep.cpp:95
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 nondet_volatile(symbol_table_baset &symbol_table, goto_programt &goto_program)
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)
nondet_volatilet(goto_modelt &goto_model, const optionst &options)
void handle_volatile_expression(exprt &expr, const namespacet &ns, goto_programt &pre, goto_programt &post)
std::map< irep_idt, irep_idt > variable_models
const symbolt & typecheck_variable(const irep_idt &id, const namespacet &ns)
void nondet_volatile_rhs(const symbol_table_baset &symbol_table, exprt &expr, goto_programt &pre, goto_programt &post)
void typecheck_options(const optionst &options)
void nondet_volatile_lhs(const symbol_table_baset &symbol_table, exprt &expr, goto_programt &pre, goto_programt &post)
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:142
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
bool is_static_lifetime
Definition symbol.h:70
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:106
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:27
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 goto_instruction_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.
#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:1478
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
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)