Skip to content

Commit 8e177a5

Browse files
Group symex options into symex_config structure
This makes it easy to separate the constant parameters of that class from the other fields.
1 parent 8a75ce4 commit 8e177a5

7 files changed

+48
-35
lines changed

src/goto-symex/goto_symex.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ unsigned goto_symext::dynamic_counter=0;
1717

1818
void goto_symext::do_simplify(exprt &expr)
1919
{
20-
if(simplify_opt)
20+
if(symex_config.simplify_opt)
2121
simplify(expr, ns);
2222
}
2323

src/goto-symex/goto_symex.h

Lines changed: 19 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,22 @@ class symex_nondet_generatort
4848
unsigned nondet_count = 0;
4949
};
5050

51+
/// Configuration of the symbolic execution
52+
struct symex_configt final
53+
{
54+
unsigned max_depth;
55+
bool doing_path_exploration;
56+
bool allow_pointer_unsoundness;
57+
bool constant_propagation;
58+
bool self_loops_to_assumptions;
59+
bool simplify_opt;
60+
bool unwinding_assertions;
61+
bool partial_loops;
62+
std::string debug_level;
63+
64+
explicit symex_configt(const optionst &options);
65+
};
66+
5167
/// \brief The main class for the forward symbolic simulator
5268
///
5369
/// Higher-level architectural information on symbolic execution is
@@ -65,18 +81,8 @@ class goto_symext
6581
const optionst &options,
6682
path_storaget &path_storage)
6783
: should_pause_symex(false),
68-
max_depth(options.get_unsigned_int_option("depth")),
69-
doing_path_exploration(options.is_set("paths")),
70-
allow_pointer_unsoundness(
71-
options.get_bool_option("allow-pointer-unsoundness")),
84+
symex_config(options),
7285
language_mode(),
73-
constant_propagation(options.get_bool_option("propagation")),
74-
self_loops_to_assumptions(
75-
options.get_bool_option("self-loops-to-assumptions")),
76-
simplify_opt(options.get_bool_option("simplify")),
77-
unwinding_assertions(options.get_bool_option("unwinding-assertions")),
78-
partial_loops(options.get_bool_option("partial-loops")),
79-
debug_level(options.get_option("debug-level")),
8086
outer_symbol_table(outer_symbol_table),
8187
ns(outer_symbol_table),
8288
target(_target),
@@ -150,6 +156,8 @@ class goto_symext
150156
bool should_pause_symex;
151157

152158
protected:
159+
const symex_configt symex_config;
160+
153161
/// Initialise the symbolic execution and the given state with <code>pc</code>
154162
/// as entry point.
155163
/// \param state Symex state to initialise.
@@ -176,23 +184,13 @@ class goto_symext
176184
const get_goto_functiont &,
177185
statet &);
178186

179-
const unsigned max_depth;
180-
const bool doing_path_exploration;
181-
const bool allow_pointer_unsoundness;
182-
183187
public:
184188

185189
/// language_mode: ID_java, ID_C or another language identifier
186190
/// if we know the source language in use, irep_idt() otherwise.
187191
irep_idt language_mode;
188192

189193
protected:
190-
const bool constant_propagation;
191-
const bool self_loops_to_assumptions;
192-
const bool simplify_opt;
193-
const bool unwinding_assertions;
194-
const bool partial_loops;
195-
const std::string debug_level;
196194

197195
/// The symbol table associated with the goto-program that we're
198196
/// executing. This symbol table will not additionally contain objects

src/goto-symex/symex_assign.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -247,9 +247,9 @@ void goto_symext::symex_assign_symbol(
247247
ssa_lhs,
248248
ssa_rhs,
249249
ns,
250-
simplify_opt,
251-
constant_propagation,
252-
allow_pointer_unsoundness);
250+
symex_config.simplify_opt,
251+
symex_config.constant_propagation,
252+
symex_config.allow_pointer_unsoundness);
253253

254254
exprt ssa_full_lhs=full_lhs;
255255
ssa_full_lhs=add_to_lhs(ssa_full_lhs, ssa_lhs);

src/goto-symex/symex_builtin_functions.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -458,7 +458,7 @@ void goto_symext::symex_trace(
458458
{
459459
PRECONDITION(code.arguments().size() >= 2);
460460

461-
int debug_thresh = unsafe_string2int(debug_level);
461+
int debug_thresh = unsafe_string2int(symex_config.debug_level);
462462

463463
mp_integer debug_lvl;
464464
optionalt<mp_integer> maybe_debug =

src/goto-symex/symex_function_call.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -236,13 +236,13 @@ void goto_symext::symex_function_call_code(
236236
// see if it's too much
237237
if(stop_recursing)
238238
{
239-
if(partial_loops)
239+
if(symex_config.partial_loops)
240240
{
241241
// it's ok, ignore
242242
}
243243
else
244244
{
245-
if(unwinding_assertions)
245+
if(symex_config.unwinding_assertions)
246246
vcc(false_exprt(), "recursion unwinding assertion", state);
247247

248248
// add to state guard to prevent further assignments

src/goto-symex/symex_goto.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ void goto_symext::symex_goto(statet &state)
6161
{
6262
// is it label: goto label; or while(cond); - popular in SV-COMP
6363
if(
64-
self_loops_to_assumptions &&
64+
symex_config.self_loops_to_assumptions &&
6565
(goto_target == state.source.pc ||
6666
(instruction.incoming_edges.size() == 1 &&
6767
*instruction.incoming_edges.begin() == goto_target)))
@@ -109,7 +109,7 @@ void goto_symext::symex_goto(statet &state)
109109
(simpl_state_guard.is_true() ||
110110
// or there is another block, but we're doing path exploration so
111111
// we're going to skip over it for now and return to it later.
112-
doing_path_exploration))
112+
symex_config.doing_path_exploration))
113113
{
114114
DATA_INVARIANT(
115115
instruction.targets.size() > 0,
@@ -176,7 +176,7 @@ void goto_symext::symex_goto(statet &state)
176176
log.debug() << "Resuming from next instruction '"
177177
<< state_pc->source_location << "'" << log.eom;
178178
}
179-
else if(doing_path_exploration)
179+
else if(symex_config.doing_path_exploration)
180180
{
181181
// We should save both the instruction after this goto, and the target of
182182
// the goto.
@@ -490,9 +490,9 @@ void goto_symext::loop_bound_exceeded(
490490
else
491491
negated_cond=not_exprt(guard);
492492

493-
if(!partial_loops)
493+
if(!symex_config.partial_loops)
494494
{
495-
if(unwinding_assertions)
495+
if(symex_config.unwinding_assertions)
496496
{
497497
// Generate VCC for unwinding assertion.
498498
vcc(negated_cond,

src/goto-symex/symex_main.cpp

Lines changed: 17 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,21 @@ Author: Daniel Kroening, [email protected]
2222

2323
#include <analyses/dirty.h>
2424

25+
symex_configt::symex_configt(const optionst &options)
26+
: max_depth(options.get_unsigned_int_option("depth")),
27+
doing_path_exploration(options.is_set("paths")),
28+
allow_pointer_unsoundness(
29+
options.get_bool_option("allow-pointer-unsoundness")),
30+
constant_propagation(options.get_bool_option("propagation")),
31+
self_loops_to_assumptions(
32+
options.get_bool_option("self-loops-to-assumptions")),
33+
simplify_opt(options.get_bool_option("simplify")),
34+
unwinding_assertions(options.get_bool_option("unwinding-assertions")),
35+
partial_loops(options.get_bool_option("partial-loops")),
36+
debug_level(options.get_option("debug-level"))
37+
{
38+
}
39+
2540
void symex_transition(
2641
goto_symext::statet &state,
2742
goto_programt::const_targett to,
@@ -317,11 +332,11 @@ void goto_symext::symex_step(
317332

318333
const goto_programt::instructiont &instruction=*state.source.pc;
319334

320-
if(!doing_path_exploration)
335+
if(!symex_config.doing_path_exploration)
321336
merge_gotos(state);
322337

323338
// depth exceeded?
324-
if(max_depth != 0 && state.depth > max_depth)
339+
if(symex_config.max_depth != 0 && state.depth > symex_config.max_depth)
325340
state.guard.add(false_exprt());
326341
state.depth++;
327342

0 commit comments

Comments
 (0)