@@ -16,6 +16,7 @@ Date: September 2011
16
16
#include < util/cmdline.h>
17
17
#include < util/options.h>
18
18
#include < util/std_expr.h>
19
+ #include < util/string_utils.h>
19
20
#include < util/symbol_table.h>
20
21
21
22
using havoc_predicatet = std::function<bool (const exprt &)>;
@@ -28,6 +29,9 @@ class nondet_volatilet
28
29
goto_programt &goto_program,
29
30
havoc_predicatet should_havoc);
30
31
32
+ static const symbolt &
33
+ typecheck_variable (const irep_idt &id, const namespacet &ns);
34
+
31
35
private:
32
36
static bool is_volatile (const namespacet &ns, const typet &src);
33
37
@@ -40,6 +44,19 @@ class nondet_volatilet
40
44
const symbol_tablet &symbol_table,
41
45
exprt &expr,
42
46
havoc_predicatet should_havoc);
47
+
48
+ static void typecheck_model (
49
+ const irep_idt &id,
50
+ const symbolt &variable,
51
+ const namespacet &ns);
52
+
53
+ void
54
+ typecheck_options (const goto_modelt &goto_model, const optionst &options);
55
+
56
+ // configuration obtained from command line options
57
+ bool all_nondet;
58
+ std::set<irep_idt> nondet_variables;
59
+ std::map<irep_idt, irep_idt> variable_models;
43
60
};
44
61
45
62
bool nondet_volatilet::is_volatile (const namespacet &ns, const typet &src)
@@ -158,6 +175,146 @@ void nondet_volatilet::nondet_volatile(
158
175
}
159
176
}
160
177
178
+ const symbolt &
179
+ nondet_volatilet::typecheck_variable (const irep_idt &id, const namespacet &ns)
180
+ {
181
+ const symbolt *symbol;
182
+
183
+ if (ns.lookup (id, symbol))
184
+ {
185
+ throw invalid_command_line_argument_exceptiont (
186
+ " given symbol `" + id2string (id) + " ` not found in symbol table" ,
187
+ " --" NONDET_VOLATILE_VARIABLE_OPT);
188
+ }
189
+
190
+ if (!symbol->is_static_lifetime || !symbol->type .get_bool (ID_C_volatile))
191
+ {
192
+ throw invalid_command_line_argument_exceptiont (
193
+ " symbol `" + id2string (id) +
194
+ " ` does not represent a volatile variable "
195
+ " with static lifetime" ,
196
+ " --" NONDET_VOLATILE_VARIABLE_OPT);
197
+ }
198
+
199
+ INVARIANT (!symbol->is_type , " symbol must not represent a type" );
200
+
201
+ INVARIANT (!symbol->is_function (), " symbol must not represent a function" );
202
+
203
+ return *symbol;
204
+ }
205
+
206
+ void nondet_volatilet::typecheck_model (
207
+ const irep_idt &id,
208
+ const symbolt &variable,
209
+ const namespacet &ns)
210
+ {
211
+ const symbolt *symbol;
212
+
213
+ if (ns.lookup (id, symbol))
214
+ {
215
+ throw invalid_command_line_argument_exceptiont (
216
+ " given model name " + id2string (id) + " not found in symbol table" ,
217
+ " --" NONDET_VOLATILE_MODEL_OPT);
218
+ }
219
+
220
+ if (!symbol->is_function ())
221
+ {
222
+ throw invalid_command_line_argument_exceptiont (
223
+ " symbol `" + id2string (id) + " ` is not a function" ,
224
+ " --" NONDET_VOLATILE_MODEL_OPT);
225
+ }
226
+
227
+ const auto &code_type = to_code_type (symbol->type );
228
+
229
+ if (variable.type != code_type.return_type ())
230
+ {
231
+ throw invalid_command_line_argument_exceptiont (
232
+ " return type of model `" + id2string (id) +
233
+ " ` is not compatible with the "
234
+ " type of the modelled variable " +
235
+ id2string (variable.name ),
236
+ " --" NONDET_VOLATILE_MODEL_OPT);
237
+ }
238
+
239
+ if (!code_type.parameters ().empty ())
240
+ {
241
+ throw invalid_command_line_argument_exceptiont (
242
+ " model `" + id2string (id) + " ` must not take parameters " ,
243
+ " --" NONDET_VOLATILE_MODEL_OPT);
244
+ }
245
+ }
246
+
247
+ void nondet_volatilet::typecheck_options (
248
+ const goto_modelt &goto_model,
249
+ const optionst &options)
250
+ {
251
+ PRECONDITION (nondet_variables.empty ());
252
+ PRECONDITION (variable_models.empty ());
253
+
254
+ if (options.get_bool_option (NONDET_VOLATILE_OPT))
255
+ {
256
+ all_nondet = true ;
257
+ return ;
258
+ }
259
+
260
+ const namespacet ns (goto_model.symbol_table );
261
+
262
+ if (options.is_set (NONDET_VOLATILE_VARIABLE_OPT))
263
+ {
264
+ const auto &variable_list =
265
+ options.get_list_option (NONDET_VOLATILE_VARIABLE_OPT);
266
+
267
+ nondet_variables.insert (variable_list.begin (), variable_list.end ());
268
+
269
+ for (const auto &id : nondet_variables)
270
+ {
271
+ typecheck_variable (id, ns);
272
+ }
273
+ }
274
+
275
+ if (options.is_set (NONDET_VOLATILE_MODEL_OPT))
276
+ {
277
+ const auto &model_list = options.get_list_option (NONDET_VOLATILE_MODEL_OPT);
278
+
279
+ for (const auto &s : model_list)
280
+ {
281
+ std::string variable;
282
+ std::string model;
283
+
284
+ try
285
+ {
286
+ split_string (s, ' :' , variable, model, true );
287
+ }
288
+ catch (const deserialization_exceptiont &e)
289
+ {
290
+ throw invalid_command_line_argument_exceptiont (
291
+ " cannot split argument `" + s + " ` into variable name and model name" ,
292
+ " --" NONDET_VOLATILE_MODEL_OPT);
293
+ }
294
+
295
+ const auto &variable_symbol = typecheck_variable (variable, ns);
296
+
297
+ if (nondet_variables.count (variable) != 0 )
298
+ {
299
+ throw invalid_command_line_argument_exceptiont (
300
+ " conflicting options for variable `" + variable + " `" ,
301
+ " --" NONDET_VOLATILE_VARIABLE_OPT " /--" NONDET_VOLATILE_MODEL_OPT);
302
+ }
303
+
304
+ typecheck_model (model, variable_symbol, ns);
305
+
306
+ const auto p = variable_models.insert (std::make_pair (variable, model));
307
+
308
+ if (!p.second && p.first ->second != model)
309
+ {
310
+ throw invalid_command_line_argument_exceptiont (
311
+ " conflicting models for variable `" + variable + " `" ,
312
+ " --" NONDET_VOLATILE_MODEL_OPT);
313
+ }
314
+ }
315
+ }
316
+ }
317
+
161
318
void nondet_volatile (goto_modelt &goto_model, havoc_predicatet should_havoc)
162
319
{
163
320
Forall_goto_functions (f_it, goto_model.goto_functions )
@@ -171,29 +328,45 @@ void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
171
328
{
172
329
PRECONDITION (!options.is_set (NONDET_VOLATILE_OPT));
173
330
PRECONDITION (!options.is_set (NONDET_VOLATILE_VARIABLE_OPT));
331
+ PRECONDITION (!options.is_set (NONDET_VOLATILE_MODEL_OPT));
174
332
175
333
const bool nondet_volatile_opt = cmdline.isset (NONDET_VOLATILE_OPT);
176
334
const bool nondet_volatile_variable_opt =
177
335
cmdline.isset (NONDET_VOLATILE_VARIABLE_OPT);
336
+ const bool nondet_volatile_model_opt =
337
+ cmdline.isset (NONDET_VOLATILE_MODEL_OPT);
178
338
179
- if (nondet_volatile_opt && nondet_volatile_variable_opt)
339
+ if (
340
+ nondet_volatile_opt &&
341
+ (nondet_volatile_variable_opt || nondet_volatile_model_opt))
180
342
{
181
343
throw invalid_command_line_argument_exceptiont (
182
- " only one of " NONDET_VOLATILE_OPT " /" NONDET_VOLATILE_VARIABLE_OPT
183
- " can "
184
- " be given at a time" ,
185
- NONDET_VOLATILE_OPT " /" NONDET_VOLATILE_VARIABLE_OPT);
344
+ " --" NONDET_VOLATILE_OPT
345
+ " cannot be used with --" NONDET_VOLATILE_VARIABLE_OPT
346
+ " or --" NONDET_VOLATILE_MODEL_OPT,
347
+ " --" NONDET_VOLATILE_OPT " /--" NONDET_VOLATILE_VARIABLE_OPT
348
+ " /--" NONDET_VOLATILE_MODEL_OPT);
186
349
}
187
350
188
351
if (nondet_volatile_opt)
189
352
{
190
353
options.set_option (NONDET_VOLATILE_OPT, true );
191
354
}
192
- else if (cmdline. isset (NONDET_VOLATILE_VARIABLE_OPT))
355
+ else
193
356
{
194
- options.set_option (
195
- NONDET_VOLATILE_VARIABLE_OPT,
196
- cmdline.get_values (NONDET_VOLATILE_VARIABLE_OPT));
357
+ if (nondet_volatile_variable_opt)
358
+ {
359
+ options.set_option (
360
+ NONDET_VOLATILE_VARIABLE_OPT,
361
+ cmdline.get_values (NONDET_VOLATILE_VARIABLE_OPT));
362
+ }
363
+
364
+ if (nondet_volatile_model_opt)
365
+ {
366
+ options.set_option (
367
+ NONDET_VOLATILE_MODEL_OPT,
368
+ cmdline.get_values (NONDET_VOLATILE_MODEL_OPT));
369
+ }
197
370
}
198
371
}
199
372
@@ -211,31 +384,9 @@ void nondet_volatile(goto_modelt &goto_model, const optionst &options)
211
384
std::set<irep_idt> variables (variable_list.begin (), variable_list.end ());
212
385
const namespacet ns (goto_model.symbol_table );
213
386
214
- // typecheck given variables
215
387
for (const auto &id : variables)
216
388
{
217
- const symbolt *symbol;
218
-
219
- if (ns.lookup (id, symbol))
220
- {
221
- throw invalid_command_line_argument_exceptiont (
222
- " given name " + id2string (id) + " not found in symbol table" ,
223
- NONDET_VOLATILE_VARIABLE_OPT);
224
- }
225
-
226
- if (!symbol->is_static_lifetime || !symbol->type .get_bool (ID_C_volatile))
227
- {
228
- throw invalid_command_line_argument_exceptiont (
229
- " given name " + id2string (id) +
230
- " does not represent a volatile "
231
- " variable with static lifetime" ,
232
- NONDET_VOLATILE_VARIABLE_OPT);
233
- }
234
-
235
- INVARIANT (!symbol->is_type , " symbol must not represent a type" );
236
-
237
- INVARIANT (
238
- symbol->type .id () != ID_code, " symbol must not represent a function" );
389
+ nondet_volatilet::typecheck_variable (id, ns);
239
390
}
240
391
241
392
auto should_havoc = [&variables](const exprt &expr) {
0 commit comments