Skip to content

Commit 519a237

Browse files
danpoedanpoe
committed
Selective havocking of volatile variables via --nondet-volatile-variable <variable>
1 parent 9ff9be8 commit 519a237

File tree

8 files changed

+207
-30
lines changed

8 files changed

+207
-30
lines changed

‎regression/goto-instrument/nondet-volatile-02/test.c‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#include <assert.h>
2+
3+
volatile int a;
4+
volatile int b;
5+
6+
void main()
7+
{
8+
assert(a == 0);
9+
10+
assert(b == 0);
11+
assert(b != 0);
12+
}

‎regression/goto-instrument/nondet-volatile-02/test.desc‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
test.c
3+
--nondet-volatile-variable b
4+
\[main.assertion.1\] line \d+ assertion a == 0: SUCCESS
5+
\[main.assertion.2\] line \d+ assertion b == 0: FAILURE
6+
\[main.assertion.3\] line \d+ assertion b != 0: FAILURE
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
--
10+
--
11+
Check that volatile global variables are havocked when given via the
12+
--nondet-volatile-variable option. Variable a is initialized to zero (as it has
13+
static storage duration), and is not havocked, thus the assert(a == 0) passes.

‎regression/goto-instrument/nondet-volatile-03/test.c‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
#include <assert.h>
2+
3+
int x;
4+
5+
void main()
6+
{
7+
x;
8+
}

‎regression/goto-instrument/nondet-volatile-03/test.desc‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test.c
3+
--nondet-volatile-variable x
4+
^Invalid User Input$
5+
given name x does not represent a volatile variable with static lifetime$
6+
^EXIT=1$
7+
^SIGNAL=0$
8+
--
9+
--
10+
Check that it is invalid to specify a non-volatile variable to be havocked

‎src/goto-instrument/goto_instrument_parse_options.cpp‎

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -996,6 +996,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
996996
{
997997
optionst options;
998998

999+
parse_nondet_volatile_options(cmdline, options);
1000+
9991001
// disable simplify when adding various checks?
10001002
if(cmdline.isset("no-simplify"))
10011003
options.set_option("simplify", false);
@@ -1622,13 +1624,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
16221624
// label the assertions
16231625
label_properties(goto_model);
16241626

1625-
// nondet volatile?
1626-
if(cmdline.isset("nondet-volatile"))
1627-
{
1628-
log.status() << "Making volatile variables non-deterministic"
1629-
<< messaget::eom;
1630-
nondet_volatile(goto_model);
1631-
}
1627+
nondet_volatile(goto_model, options);
16321628

16331629
// reachability slice?
16341630
if(cmdline.isset("reachability-slice"))
@@ -1803,7 +1799,7 @@ void goto_instrument_parse_optionst::help()
18031799
" --race-check add floating-point data race checks\n"
18041800
"\n"
18051801
"Semantic transformations:\n"
1806-
" --nondet-volatile makes reads from volatile variables non-deterministic\n" // NOLINT(*)
1802+
HELP_NONDET_VOLATILE
18071803
" --unwind <n> unwinds the loops <n> times\n"
18081804
" --unwindset L:B,... unwind loop L with a bound of B\n"
18091805
" --unwindset-file <file> read unwindset from file\n"

‎src/goto-instrument/goto_instrument_parse_options.h‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,7 @@ Author: Daniel Kroening, kroening@kroening.com
3333
#include "code_contracts.h"
3434
#include "generate_function_bodies.h"
3535
#include "insert_final_assert_false.h"
36+
#include "nondet_volatile.h"
3637
#include "replace_calls.h"
3738

3839
#include "count_eloc.h"
@@ -65,7 +66,7 @@ Author: Daniel Kroening, kroening@kroening.com
6566
OPT_INSERT_FINAL_ASSERT_FALSE \
6667
OPT_SHOW_CLASS_HIERARCHY \
6768
"(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
68-
"(nondet-volatile)(isr):" \
69+
"(isr):" \
6970
"(stack-depth):(nondet-static)" \
7071
"(nondet-static-exclude):" \
7172
"(function-enter):(function-exit):(branch):" \
@@ -119,6 +120,7 @@ Author: Daniel Kroening, kroening@kroening.com
119120
OPT_VALIDATE \
120121
OPT_ANSI_C_LANGUAGE \
121122
OPT_RESTRICT_FUNCTION_POINTER \
123+
OPT_NONDET_VOLATILE \
122124
"(ensure-one-backedge-per-target)" \
123125
// empty last line
124126

‎src/goto-instrument/nondet_volatile.cpp‎

Lines changed: 120 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,13 @@ Date: September 2011
1313

1414
#include "nondet_volatile.h"
1515

16+
#include <util/cmdline.h>
17+
#include <util/options.h>
1618
#include <util/std_expr.h>
1719
#include <util/symbol_table.h>
1820

21+
using havoc_predicatet = std::function<bool(const exprt &)>;
22+
1923
static bool is_volatile(const namespacet &ns, const typet &src)
2024
{
2125
if(src.get_bool(ID_C_volatile))
@@ -31,16 +35,19 @@ static bool is_volatile(const namespacet &ns, const typet &src)
3135
return false;
3236
}
3337

34-
static void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
38+
static void nondet_volatile_rhs(
39+
const symbol_tablet &symbol_table,
40+
exprt &expr,
41+
havoc_predicatet should_havoc)
3542
{
3643
Forall_operands(it, expr)
37-
nondet_volatile_rhs(symbol_table, *it);
44+
nondet_volatile_rhs(symbol_table, *it, should_havoc);
3845

3946
if(expr.id()==ID_symbol ||
4047
expr.id()==ID_dereference)
4148
{
4249
const namespacet ns(symbol_table);
43-
if(is_volatile(ns, expr.type()))
50+
if(is_volatile(ns, expr.type()) && should_havoc(expr))
4451
{
4552
typet t=expr.type();
4653
t.remove(ID_C_volatile);
@@ -52,31 +59,42 @@ static void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
5259
}
5360
}
5461

55-
static void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
62+
static void nondet_volatile_lhs(
63+
const symbol_tablet &symbol_table,
64+
exprt &expr,
65+
havoc_predicatet should_havoc)
5666
{
5767
if(expr.id()==ID_if)
5868
{
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());
69+
nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond(), should_havoc);
70+
nondet_volatile_lhs(
71+
symbol_table, to_if_expr(expr).true_case(), should_havoc);
72+
nondet_volatile_lhs(
73+
symbol_table, to_if_expr(expr).false_case(), should_havoc);
6274
}
6375
else if(expr.id()==ID_index)
6476
{
65-
nondet_volatile_lhs(symbol_table, to_index_expr(expr).array());
66-
nondet_volatile_rhs(symbol_table, to_index_expr(expr).index());
77+
nondet_volatile_lhs(
78+
symbol_table, to_index_expr(expr).array(), should_havoc);
79+
nondet_volatile_rhs(
80+
symbol_table, to_index_expr(expr).index(), should_havoc);
6781
}
6882
else if(expr.id()==ID_member)
6983
{
70-
nondet_volatile_lhs(symbol_table, to_member_expr(expr).struct_op());
84+
nondet_volatile_lhs(
85+
symbol_table, to_member_expr(expr).struct_op(), should_havoc);
7186
}
7287
else if(expr.id()==ID_dereference)
7388
{
74-
nondet_volatile_rhs(symbol_table, to_dereference_expr(expr).pointer());
89+
nondet_volatile_rhs(
90+
symbol_table, to_dereference_expr(expr).pointer(), should_havoc);
7591
}
7692
}
7793

78-
static void
79-
nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
94+
static void nondet_volatile(
95+
symbol_tablet &symbol_table,
96+
goto_programt &goto_program,
97+
havoc_predicatet should_havoc)
8098
{
8199
namespacet ns(symbol_table);
82100

@@ -86,8 +104,10 @@ nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
86104

87105
if(instruction.is_assign())
88106
{
89-
nondet_volatile_rhs(symbol_table, to_code_assign(instruction.code).rhs());
90-
nondet_volatile_lhs(symbol_table, to_code_assign(instruction.code).lhs());
107+
nondet_volatile_rhs(
108+
symbol_table, to_code_assign(instruction.code).rhs(), should_havoc);
109+
nondet_volatile_lhs(
110+
symbol_table, to_code_assign(instruction.code).lhs(), should_havoc);
91111
}
92112
else if(instruction.is_function_call())
93113
{
@@ -101,25 +121,105 @@ nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
101121
it=code_function_call.arguments().begin();
102122
it!=code_function_call.arguments().end();
103123
it++)
104-
nondet_volatile_rhs(symbol_table, *it);
124+
nondet_volatile_rhs(symbol_table, *it, should_havoc);
105125

106126
// do return value
107-
nondet_volatile_lhs(symbol_table, code_function_call.lhs());
127+
nondet_volatile_lhs(symbol_table, code_function_call.lhs(), should_havoc);
108128
}
109129
else if(instruction.has_condition())
110130
{
111131
// do condition
112132
exprt cond = instruction.get_condition();
113-
nondet_volatile_rhs(symbol_table, cond);
133+
nondet_volatile_rhs(symbol_table, cond, should_havoc);
114134
instruction.set_condition(cond);
115135
}
116136
}
117137
}
118138

119-
void nondet_volatile(goto_modelt &goto_model)
139+
void nondet_volatile(goto_modelt &goto_model, havoc_predicatet should_havoc)
120140
{
121141
Forall_goto_functions(f_it, goto_model.goto_functions)
122-
nondet_volatile(goto_model.symbol_table, f_it->second.body);
142+
nondet_volatile(goto_model.symbol_table, f_it->second.body, should_havoc);
123143

124144
goto_model.goto_functions.update();
125145
}
146+
147+
void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
148+
{
149+
PRECONDITION(!options.is_set(NONDET_VOLATILE_OPT));
150+
PRECONDITION(!options.is_set(NONDET_VOLATILE_VARIABLE_OPT));
151+
152+
const bool nondet_volatile_opt = cmdline.isset(NONDET_VOLATILE_OPT);
153+
const bool nondet_volatile_variable_opt =
154+
cmdline.isset(NONDET_VOLATILE_VARIABLE_OPT);
155+
156+
if(nondet_volatile_opt && nondet_volatile_variable_opt)
157+
{
158+
throw invalid_command_line_argument_exceptiont(
159+
"only one of " NONDET_VOLATILE_OPT "/" NONDET_VOLATILE_VARIABLE_OPT
160+
"can "
161+
"be given at a time",
162+
NONDET_VOLATILE_OPT "/" NONDET_VOLATILE_VARIABLE_OPT);
163+
}
164+
165+
if(nondet_volatile_opt)
166+
{
167+
options.set_option(NONDET_VOLATILE_OPT, true);
168+
}
169+
else if(cmdline.isset(NONDET_VOLATILE_VARIABLE_OPT))
170+
{
171+
options.set_option(
172+
NONDET_VOLATILE_VARIABLE_OPT,
173+
cmdline.get_values(NONDET_VOLATILE_VARIABLE_OPT));
174+
}
175+
}
176+
177+
void nondet_volatile(goto_modelt &goto_model, const optionst &options)
178+
{
179+
if(options.get_bool_option(NONDET_VOLATILE_OPT))
180+
{
181+
nondet_volatile(goto_model);
182+
}
183+
else if(options.is_set(NONDET_VOLATILE_VARIABLE_OPT))
184+
{
185+
const auto &variable_list =
186+
options.get_list_option(NONDET_VOLATILE_VARIABLE_OPT);
187+
188+
std::set<irep_idt> variables(variable_list.begin(), variable_list.end());
189+
const namespacet ns(goto_model.symbol_table);
190+
191+
// typecheck given variables
192+
for(const auto &id : variables)
193+
{
194+
const symbolt *symbol;
195+
196+
if(ns.lookup(id, symbol))
197+
{
198+
throw invalid_command_line_argument_exceptiont(
199+
"given name " + id2string(id) + " not found in symbol table",
200+
NONDET_VOLATILE_VARIABLE_OPT);
201+
}
202+
203+
if(!symbol->is_static_lifetime || !symbol->type.get_bool(ID_C_volatile))
204+
{
205+
throw invalid_command_line_argument_exceptiont(
206+
"given name " + id2string(id) +
207+
" does not represent a volatile "
208+
"variable with static lifetime",
209+
NONDET_VOLATILE_VARIABLE_OPT);
210+
}
211+
212+
INVARIANT(!symbol->is_type, "symbol must not represent a type");
213+
214+
INVARIANT(
215+
symbol->type.id() != ID_code, "symbol must not represent a function");
216+
}
217+
218+
auto should_havoc = [&variables](const exprt &expr) {
219+
return expr.id() == ID_symbol &&
220+
variables.count(to_symbol_expr(expr).get_identifier()) != 0;
221+
};
222+
223+
nondet_volatile(goto_model, should_havoc);
224+
}
225+
}

‎src/goto-instrument/nondet_volatile.h‎

Lines changed: 37 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,42 @@ Author: Daniel Kroening, kroening@kroening.com
1414

1515
#include <goto-programs/goto_model.h>
1616

17-
void nondet_volatile(goto_modelt &);
17+
class cmdlinet;
18+
class optionst;
19+
20+
// clang-format off
21+
#define NONDET_VOLATILE_OPT "nondet-volatile"
22+
#define NONDET_VOLATILE_VARIABLE_OPT "nondet-volatile-variable"
23+
24+
#define OPT_NONDET_VOLATILE \
25+
"(" NONDET_VOLATILE_OPT ")" \
26+
"(" NONDET_VOLATILE_VARIABLE_OPT "):"
27+
28+
#define HELP_NONDET_VOLATILE \
29+
" --" NONDET_VOLATILE_OPT " makes reads from volatile variables " \
30+
"non-deterministic\n" \
31+
" --" NONDET_VOLATILE_VARIABLE_OPT " <variable>\n" \
32+
" makes reads from given volatile variable " \
33+
"non-deterministic\n"
34+
// clang-format on
35+
36+
void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options);
37+
38+
/// Havoc reads from volatile expressions, if enabled in the options
39+
///
40+
/// \param goto_model: the goto model in which to havoc volatile reads
41+
/// \param options: command line options
42+
void nondet_volatile(goto_modelt &goto_model, const optionst &options);
43+
44+
/// Havoc reads from volatile expressions
45+
///
46+
/// \param goto_model: the goto model in which to havoc volatile reads
47+
/// \param should_havoc: predicate indicating if the given volatile expression
48+
/// should be havocked
49+
void nondet_volatile(
50+
goto_modelt &goto_model,
51+
std::function<bool(const exprt &)> should_havoc = [](const exprt &) {
52+
return true;
53+
});
1854

1955
#endif // CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H

0 commit comments

Comments
 (0)