Skip to content

Commit b4d27ca

Browse files
tautschnigtautschnig
authored
Merge pull request #3848 from diffblue/SSA_stept_constructor
extend constructor of SSA_stept
2 parents bfb2a3c + 2b39c88 commit b4d27ca

File tree

5 files changed

+43
-80
lines changed

5 files changed

+43
-80
lines changed

‎src/goto-symex/partial_order_concurrency.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -56,16 +56,15 @@ void partial_order_concurrencyt::add_init_writes(
5656
e_it->is_shared_read() ||
5757
!e_it->guard.is_true())
5858
{
59-
init_steps.push_back(symex_target_equationt::SSA_stept());
59+
init_steps.emplace_back(
60+
e_it->source, goto_trace_stept::typet::SHARED_WRITE);
6061
symex_target_equationt::SSA_stept &SSA_step=init_steps.back();
6162

6263
SSA_step.guard=true_exprt();
6364
// no SSA L2 index, thus nondet value
6465
SSA_step.ssa_lhs=e_it->ssa_lhs;
6566
SSA_step.ssa_lhs.remove_level_2();
66-
SSA_step.type=goto_trace_stept::typet::SHARED_WRITE;
6767
SSA_step.atomic_section_id=0;
68-
SSA_step.source=e_it->source;
6968
}
7069

7170
init_done.insert(a);

‎src/goto-symex/slice_by_trace.cpp

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -87,14 +87,13 @@ void symex_slice_by_tracet::slice_by_trace(
8787

8888
guardt t_guard;
8989
symex_targett::sourcet empty_source;
90-
equation.SSA_steps.push_front(symex_target_equationt::SSA_stept());
90+
equation.SSA_steps.emplace_front(
91+
empty_source, goto_trace_stept::typet::ASSUME);
9192
symex_target_equationt::SSA_stept &SSA_step=equation.SSA_steps.front();
9293

9394
SSA_step.guard=t_guard.as_expr();
9495
SSA_step.ssa_lhs.make_nil();
9596
SSA_step.cond_expr.swap(trace_condition);
96-
SSA_step.type=goto_trace_stept::typet::ASSUME;
97-
SSA_step.source=empty_source;
9897

9998
assign_merges(equation); // Now add the merge variable assignments to eqn
10099

@@ -491,7 +490,8 @@ void symex_slice_by_tracet::assign_merges(
491490

492491
exprt merge_copy(*i);
493492

494-
equation.SSA_steps.push_front(symex_target_equationt::SSA_stept());
493+
equation.SSA_steps.emplace_front(
494+
empty_source, goto_trace_stept::typet::ASSIGNMENT);
495495
symex_target_equationt::SSA_stept &SSA_step=equation.SSA_steps.front();
496496

497497
SSA_step.guard=t_guard.as_expr();
@@ -500,8 +500,6 @@ void symex_slice_by_tracet::assign_merges(
500500
SSA_step.assignment_type=symex_targett::assignment_typet::HIDDEN;
501501

502502
SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
503-
SSA_step.type=goto_trace_stept::typet::ASSIGNMENT;
504-
SSA_step.source=empty_source;
505503
}
506504
}
507505

‎src/goto-symex/symex_target_equation.cpp

Lines changed: 18 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -34,14 +34,12 @@ void symex_target_equationt::shared_read(
3434
unsigned atomic_section_id,
3535
const sourcet &source)
3636
{
37-
SSA_steps.push_back(SSA_stept());
37+
SSA_steps.emplace_back(source, goto_trace_stept::typet::SHARED_READ);
3838
SSA_stept &SSA_step=SSA_steps.back();
3939

4040
SSA_step.guard=guard;
4141
SSA_step.ssa_lhs=ssa_object;
42-
SSA_step.type=goto_trace_stept::typet::SHARED_READ;
4342
SSA_step.atomic_section_id=atomic_section_id;
44-
SSA_step.source=source;
4543

4644
merge_ireps(SSA_step);
4745
}
@@ -52,14 +50,12 @@ void symex_target_equationt::shared_write(
5250
unsigned atomic_section_id,
5351
const sourcet &source)
5452
{
55-
SSA_steps.push_back(SSA_stept());
53+
SSA_steps.emplace_back(source, goto_trace_stept::typet::SHARED_WRITE);
5654
SSA_stept &SSA_step=SSA_steps.back();
5755

5856
SSA_step.guard=guard;
5957
SSA_step.ssa_lhs=ssa_object;
60-
SSA_step.type=goto_trace_stept::typet::SHARED_WRITE;
6158
SSA_step.atomic_section_id=atomic_section_id;
62-
SSA_step.source=source;
6359

6460
merge_ireps(SSA_step);
6561
}
@@ -69,11 +65,9 @@ void symex_target_equationt::spawn(
6965
const exprt &guard,
7066
const sourcet &source)
7167
{
72-
SSA_steps.push_back(SSA_stept());
68+
SSA_steps.emplace_back(source, goto_trace_stept::typet::SPAWN);
7369
SSA_stept &SSA_step=SSA_steps.back();
7470
SSA_step.guard=guard;
75-
SSA_step.type=goto_trace_stept::typet::SPAWN;
76-
SSA_step.source=source;
7771

7872
merge_ireps(SSA_step);
7973
}
@@ -82,11 +76,9 @@ void symex_target_equationt::memory_barrier(
8276
const exprt &guard,
8377
const sourcet &source)
8478
{
85-
SSA_steps.push_back(SSA_stept());
79+
SSA_steps.emplace_back(source, goto_trace_stept::typet::MEMORY_BARRIER);
8680
SSA_stept &SSA_step=SSA_steps.back();
8781
SSA_step.guard=guard;
88-
SSA_step.type=goto_trace_stept::typet::MEMORY_BARRIER;
89-
SSA_step.source=source;
9082

9183
merge_ireps(SSA_step);
9284
}
@@ -97,12 +89,10 @@ void symex_target_equationt::atomic_begin(
9789
unsigned atomic_section_id,
9890
const sourcet &source)
9991
{
100-
SSA_steps.push_back(SSA_stept());
92+
SSA_steps.emplace_back(source, goto_trace_stept::typet::ATOMIC_BEGIN);
10193
SSA_stept &SSA_step=SSA_steps.back();
10294
SSA_step.guard=guard;
103-
SSA_step.type=goto_trace_stept::typet::ATOMIC_BEGIN;
10495
SSA_step.atomic_section_id=atomic_section_id;
105-
SSA_step.source=source;
10696

10797
merge_ireps(SSA_step);
10898
}
@@ -113,12 +103,10 @@ void symex_target_equationt::atomic_end(
113103
unsigned atomic_section_id,
114104
const sourcet &source)
115105
{
116-
SSA_steps.push_back(SSA_stept());
106+
SSA_steps.emplace_back(source, goto_trace_stept::typet::ATOMIC_END);
117107
SSA_stept &SSA_step=SSA_steps.back();
118108
SSA_step.guard=guard;
119-
SSA_step.type=goto_trace_stept::typet::ATOMIC_END;
120109
SSA_step.atomic_section_id=atomic_section_id;
121-
SSA_step.source=source;
122110

123111
merge_ireps(SSA_step);
124112
}
@@ -134,7 +122,7 @@ void symex_target_equationt::assignment(
134122
{
135123
PRECONDITION(ssa_lhs.is_not_nil());
136124

137-
SSA_steps.push_back(SSA_stept());
125+
SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSIGNMENT);
138126
SSA_stept &SSA_step=SSA_steps.back();
139127

140128
SSA_step.guard=guard;
@@ -145,10 +133,8 @@ void symex_target_equationt::assignment(
145133
SSA_step.assignment_type=assignment_type;
146134

147135
SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
148-
SSA_step.type=goto_trace_stept::typet::ASSIGNMENT;
149136
SSA_step.hidden=(assignment_type!=assignment_typet::STATE &&
150137
assignment_type!=assignment_typet::VISIBLE_ACTUAL_PARAMETER);
151-
SSA_step.source=source;
152138

153139
merge_ireps(SSA_step);
154140
}
@@ -161,15 +147,13 @@ void symex_target_equationt::decl(
161147
{
162148
PRECONDITION(ssa_lhs.is_not_nil());
163149

164-
SSA_steps.push_back(SSA_stept());
150+
SSA_steps.emplace_back(source, goto_trace_stept::typet::DECL);
165151
SSA_stept &SSA_step=SSA_steps.back();
166152

167153
SSA_step.guard=guard;
168154
SSA_step.ssa_lhs=ssa_lhs;
169155
SSA_step.ssa_full_lhs=ssa_lhs;
170156
SSA_step.original_full_lhs=ssa_lhs.get_original_expr();
171-
SSA_step.type=goto_trace_stept::typet::DECL;
172-
SSA_step.source=source;
173157
SSA_step.hidden=(assignment_type!=assignment_typet::STATE);
174158

175159
// the condition is trivially true, and only
@@ -192,12 +176,10 @@ void symex_target_equationt::location(
192176
const exprt &guard,
193177
const sourcet &source)
194178
{
195-
SSA_steps.push_back(SSA_stept());
179+
SSA_steps.emplace_back(source, goto_trace_stept::typet::LOCATION);
196180
SSA_stept &SSA_step=SSA_steps.back();
197181

198182
SSA_step.guard=guard;
199-
SSA_step.type=goto_trace_stept::typet::LOCATION;
200-
SSA_step.source=source;
201183

202184
merge_ireps(SSA_step);
203185
}
@@ -209,12 +191,10 @@ void symex_target_equationt::function_call(
209191
const sourcet &source,
210192
const bool hidden)
211193
{
212-
SSA_steps.push_back(SSA_stept());
194+
SSA_steps.emplace_back(source, goto_trace_stept::typet::FUNCTION_CALL);
213195
SSA_stept &SSA_step=SSA_steps.back();
214196

215197
SSA_step.guard = guard;
216-
SSA_step.type = goto_trace_stept::typet::FUNCTION_CALL;
217-
SSA_step.source = source;
218198
SSA_step.called_function = function_identifier;
219199
SSA_step.ssa_function_arguments = ssa_function_arguments;
220200
SSA_step.hidden = hidden;
@@ -227,12 +207,10 @@ void symex_target_equationt::function_return(
227207
const sourcet &source,
228208
const bool hidden)
229209
{
230-
SSA_steps.push_back(SSA_stept());
210+
SSA_steps.emplace_back(source, goto_trace_stept::typet::FUNCTION_RETURN);
231211
SSA_stept &SSA_step=SSA_steps.back();
232212

233213
SSA_step.guard = guard;
234-
SSA_step.type = goto_trace_stept::typet::FUNCTION_RETURN;
235-
SSA_step.source = source;
236214
SSA_step.hidden = hidden;
237215

238216
merge_ireps(SSA_step);
@@ -244,12 +222,10 @@ void symex_target_equationt::output(
244222
const irep_idt &output_id,
245223
const std::list<exprt> &args)
246224
{
247-
SSA_steps.push_back(SSA_stept());
225+
SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
248226
SSA_stept &SSA_step=SSA_steps.back();
249227

250228
SSA_step.guard=guard;
251-
SSA_step.type=goto_trace_stept::typet::OUTPUT;
252-
SSA_step.source=source;
253229
SSA_step.io_args=args;
254230
SSA_step.io_id=output_id;
255231

@@ -263,12 +239,10 @@ void symex_target_equationt::output_fmt(
263239
const irep_idt &fmt,
264240
const std::list<exprt> &args)
265241
{
266-
SSA_steps.push_back(SSA_stept());
242+
SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
267243
SSA_stept &SSA_step=SSA_steps.back();
268244

269245
SSA_step.guard=guard;
270-
SSA_step.type=goto_trace_stept::typet::OUTPUT;
271-
SSA_step.source=source;
272246
SSA_step.io_args=args;
273247
SSA_step.io_id=output_id;
274248
SSA_step.formatted=true;
@@ -283,12 +257,10 @@ void symex_target_equationt::input(
283257
const irep_idt &input_id,
284258
const std::list<exprt> &args)
285259
{
286-
SSA_steps.push_back(SSA_stept());
260+
SSA_steps.emplace_back(source, goto_trace_stept::typet::INPUT);
287261
SSA_stept &SSA_step=SSA_steps.back();
288262

289263
SSA_step.guard=guard;
290-
SSA_step.type=goto_trace_stept::typet::INPUT;
291-
SSA_step.source=source;
292264
SSA_step.io_args=args;
293265
SSA_step.io_id=input_id;
294266

@@ -300,13 +272,11 @@ void symex_target_equationt::assumption(
300272
const exprt &cond,
301273
const sourcet &source)
302274
{
303-
SSA_steps.push_back(SSA_stept());
275+
SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSUME);
304276
SSA_stept &SSA_step=SSA_steps.back();
305277

306278
SSA_step.guard=guard;
307279
SSA_step.cond_expr=cond;
308-
SSA_step.type=goto_trace_stept::typet::ASSUME;
309-
SSA_step.source=source;
310280

311281
merge_ireps(SSA_step);
312282
}
@@ -317,13 +287,11 @@ void symex_target_equationt::assertion(
317287
const std::string &msg,
318288
const sourcet &source)
319289
{
320-
SSA_steps.push_back(SSA_stept());
290+
SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSERT);
321291
SSA_stept &SSA_step=SSA_steps.back();
322292

323293
SSA_step.guard=guard;
324294
SSA_step.cond_expr=cond;
325-
SSA_step.type=goto_trace_stept::typet::ASSERT;
326-
SSA_step.source=source;
327295
SSA_step.comment=msg;
328296

329297
merge_ireps(SSA_step);
@@ -334,13 +302,11 @@ void symex_target_equationt::goto_instruction(
334302
const exprt &cond,
335303
const sourcet &source)
336304
{
337-
SSA_steps.push_back(SSA_stept());
305+
SSA_steps.emplace_back(source, goto_trace_stept::typet::GOTO);
338306
SSA_stept &SSA_step=SSA_steps.back();
339307

340308
SSA_step.guard=guard;
341309
SSA_step.cond_expr=cond;
342-
SSA_step.type=goto_trace_stept::typet::GOTO;
343-
SSA_step.source=source;
344310

345311
merge_ireps(SSA_step);
346312
}
@@ -351,13 +317,11 @@ void symex_target_equationt::constraint(
351317
const sourcet &source)
352318
{
353319
// like assumption, but with global effect
354-
SSA_steps.push_back(SSA_stept());
320+
SSA_steps.emplace_back(source, goto_trace_stept::typet::CONSTRAINT);
355321
SSA_stept &SSA_step=SSA_steps.back();
356322

357323
SSA_step.guard=true_exprt();
358324
SSA_step.cond_expr=cond;
359-
SSA_step.type=goto_trace_stept::typet::CONSTRAINT;
360-
SSA_step.source=source;
361325
SSA_step.comment=msg;
362326

363327
merge_ireps(SSA_step);

‎src/goto-symex/symex_target_equation.h

Lines changed: 16 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -318,21 +318,22 @@ class symex_target_equationt:public symex_targett
318318
// for slicing
319319
bool ignore=false;
320320

321-
SSA_stept():
322-
type(goto_trace_stept::typet::NONE),
323-
hidden(false),
324-
guard(static_cast<const exprt &>(get_nil_irep())),
325-
guard_literal(const_literal(false)),
326-
ssa_lhs(static_cast<const ssa_exprt &>(get_nil_irep())),
327-
ssa_full_lhs(static_cast<const exprt &>(get_nil_irep())),
328-
original_full_lhs(static_cast<const exprt &>(get_nil_irep())),
329-
ssa_rhs(static_cast<const exprt &>(get_nil_irep())),
330-
assignment_type(assignment_typet::STATE),
331-
cond_expr(static_cast<const exprt &>(get_nil_irep())),
332-
cond_literal(const_literal(false)),
333-
formatted(false),
334-
atomic_section_id(0),
335-
ignore(false)
321+
SSA_stept(const sourcet &_source, goto_trace_stept::typet _type)
322+
: source(_source),
323+
type(_type),
324+
hidden(false),
325+
guard(static_cast<const exprt &>(get_nil_irep())),
326+
guard_literal(const_literal(false)),
327+
ssa_lhs(static_cast<const ssa_exprt &>(get_nil_irep())),
328+
ssa_full_lhs(static_cast<const exprt &>(get_nil_irep())),
329+
original_full_lhs(static_cast<const exprt &>(get_nil_irep())),
330+
ssa_rhs(static_cast<const exprt &>(get_nil_irep())),
331+
assignment_type(assignment_typet::STATE),
332+
cond_expr(static_cast<const exprt &>(get_nil_irep())),
333+
cond_literal(const_literal(false)),
334+
formatted(false),
335+
atomic_section_id(0),
336+
ignore(false)
336337
{
337338
}
338339

‎unit/goto-symex/ssa_equation.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,9 +24,10 @@ SCENARIO("Validation of well-formed SSA steps", "[core][goto-symex][validate]")
2424
symbol_exprt fun_foo(fun_name, code_type);
2525

2626
symex_target_equationt equation;
27-
equation.SSA_steps.push_back(symex_target_equationt::SSA_stept());
27+
symex_targett::sourcet empty_source;
28+
equation.SSA_steps.emplace_back(
29+
empty_source, goto_trace_stept::typet::FUNCTION_RETURN);
2830
auto &step = equation.SSA_steps.back();
29-
step.type = goto_trace_stept::typet::FUNCTION_RETURN;
3031
step.called_function = fun_name;
3132

3233
WHEN("Called function is in symbol table")

0 commit comments

Comments
 (0)