Skip to content

Commit 21afd2f

Browse files
tautschnigtautschnig
committed
Initialise loop counters at loop entry
The previous approach would reset loop counters when reaching an unwinding bound, which was broken as shown by newly added regression tests.
1 parent 5fc1ca6 commit 21afd2f

File tree

4 files changed

+64
-34
lines changed

4 files changed

+64
-34
lines changed

‎src/goto-symex/goto_symex.h‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -155,6 +155,16 @@ class goto_symext
155155
irep_idt guard_identifier;
156156

157157
// symex
158+
virtual void symex_transition(
159+
statet &state,
160+
goto_programt::const_targett to,
161+
bool is_backwards_goto=false);
162+
virtual void symex_transition(statet &state)
163+
{
164+
goto_programt::const_targett next=state.source.pc;
165+
++next;
166+
symex_transition(state, next);
167+
}
158168

159169
virtual void symex_goto(statet &state);
160170
virtual void symex_start_thread(statet &state);

‎src/goto-symex/symex_function_call.cpp‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -254,7 +254,7 @@ void goto_symext::symex_function_call_code(
254254
state.guard.add(false_exprt());
255255
}
256256

257-
state.source.pc++;
257+
symex_transition(state);
258258
return;
259259
}
260260

@@ -276,7 +276,7 @@ void goto_symext::symex_function_call_code(
276276
symex_assign_rec(state, code);
277277
}
278278

279-
state.source.pc++;
279+
symex_transition(state);
280280
return;
281281
}
282282

@@ -314,7 +314,7 @@ void goto_symext::symex_function_call_code(
314314
frame.loop_iterations[identifier].count++;
315315

316316
state.source.is_set=true;
317-
state.source.pc=goto_function.body.instructions.begin();
317+
symex_transition(state, goto_function.body.instructions.begin());
318318
}
319319

320320
/// pop one call frame
@@ -326,7 +326,7 @@ void goto_symext::pop_frame(statet &state)
326326
statet::framet &frame=state.top();
327327

328328
// restore program counter
329-
state.source.pc=frame.calling_location.pc;
329+
symex_transition(state, frame.calling_location.pc);
330330

331331
// restore L1 renaming
332332
state.level1.restore_from(frame.old_level1);

‎src/goto-symex/symex_goto.cpp‎

Lines changed: 6 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -36,12 +36,8 @@ void goto_symext::symex_goto(statet &state)
3636
if(!state.guard.is_false())
3737
target.location(state.guard.as_expr(), state.source);
3838

39-
// reset unwinding counter
40-
if(instruction.is_backwards_goto())
41-
frame.loop_iterations[goto_programt::loop_id(state.source.pc)].count=0;
42-
4339
// next instruction
44-
state.source.pc++;
40+
symex_transition(state);
4541
return; // nothing to do
4642
}
4743

@@ -77,7 +73,7 @@ void goto_symext::symex_goto(statet &state)
7773
symex_assume(state, negated_cond);
7874

7975
// next instruction
80-
state.source.pc++;
76+
symex_transition(state);
8177
return;
8278
}
8379

@@ -91,17 +87,14 @@ void goto_symext::symex_goto(statet &state)
9187
// no!
9288
loop_bound_exceeded(state, new_guard);
9389

94-
// reset unwinding
95-
unwind=0;
96-
9790
// next instruction
98-
state.source.pc++;
91+
symex_transition(state);
9992
return;
10093
}
10194

10295
if(new_guard.is_true())
10396
{
104-
state.source.pc=goto_target;
97+
symex_transition(state, goto_target, true);
10598
return; // nothing else to do
10699
}
107100
}
@@ -122,7 +115,7 @@ void goto_symext::symex_goto(statet &state)
122115

123116
if(state_pc==goto_target)
124117
{
125-
state.source.pc=goto_target;
118+
symex_transition(state, goto_target);
126119
return; // nothing else to do
127120
}
128121
}
@@ -140,7 +133,7 @@ void goto_symext::symex_goto(statet &state)
140133
goto_state_list.push_back(statet::goto_statet(state));
141134
statet::goto_statet &new_state=goto_state_list.back();
142135

143-
state.source.pc=state_pc;
136+
symex_transition(state, state_pc, !forward);
144137

145138
// adjust guards
146139
if(new_guard.is_true())

‎src/goto-symex/symex_main.cpp‎

Lines changed: 44 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,30 @@ Author: Daniel Kroening, kroening@kroening.com
2020

2121
#include "goto_symex.h"
2222

23+
void goto_symext::symex_transition(
24+
statet &state,
25+
goto_programt::const_targett to,
26+
bool is_backwards_goto)
27+
{
28+
if(!state.call_stack().empty())
29+
{
30+
// initialize the loop counter of any loop we are newly entering
31+
// upon this transition; we are entering a loop if
32+
// 1. the transition from state.source.pc to "to" is not a backwards goto
33+
// or
34+
// 2. we are arriving from an outer loop
35+
statet::framet &frame=state.top();
36+
const goto_programt::instructiont &instruction=*to;
37+
for(const auto &i_e : instruction.incoming_edges)
38+
if(i_e->is_goto() && i_e->is_backwards_goto() &&
39+
(!is_backwards_goto ||
40+
state.source.pc->location_number>i_e->location_number))
41+
frame.loop_iterations[goto_programt::loop_id(i_e)].count=0;
42+
}
43+
44+
state.source.pc=to;
45+
}
46+
2347
void goto_symext::new_name(symbolt &symbol)
2448
{
2549
get_new_name(symbol, ns);
@@ -114,6 +138,8 @@ void goto_symext::operator()(
114138
state.symex_target=⌖
115139
state.dirty=new dirtyt(goto_functions);
116140

141+
symex_transition(state, state.source.pc);
142+
117143
assert(state.top().end_of_function->is_end_function());
118144

119145
while(!state.call_stack().empty())
@@ -127,6 +153,7 @@ void goto_symext::operator()(
127153
unsigned t=state.source.thread_nr+1;
128154
// std::cout << "********* Now executing thread " << t << '\n';
129155
state.switch_to_thread(t);
156+
symex_transition(state, state.source.pc);
130157
}
131158
}
132159

@@ -190,20 +217,20 @@ void goto_symext::symex_step(
190217
case SKIP:
191218
if(!state.guard.is_false())
192219
target.location(state.guard.as_expr(), state.source);
193-
state.source.pc++;
220+
symex_transition(state);
194221
break;
195222

196223
case END_FUNCTION:
197224
// do even if state.guard.is_false() to clear out frame created
198225
// in symex_start_thread
199226
symex_end_of_function(state);
200-
state.source.pc++;
227+
symex_transition(state);
201228
break;
202229

203230
case LOCATION:
204231
if(!state.guard.is_false())
205232
target.location(state.guard.as_expr(), state.source);
206-
state.source.pc++;
233+
symex_transition(state);
207234
break;
208235

209236
case GOTO:
@@ -219,7 +246,7 @@ void goto_symext::symex_step(
219246
symex_assume(state, tmp);
220247
}
221248

222-
state.source.pc++;
249+
symex_transition(state);
223250
break;
224251

225252
case ASSERT:
@@ -233,21 +260,21 @@ void goto_symext::symex_step(
233260
vcc(tmp, msg, state);
234261
}
235262

236-
state.source.pc++;
263+
symex_transition(state);
237264
break;
238265

239266
case RETURN:
240267
if(!state.guard.is_false())
241268
return_assignment(state);
242269

243-
state.source.pc++;
270+
symex_transition(state);
244271
break;
245272

246273
case ASSIGN:
247274
if(!state.guard.is_false())
248275
symex_assign_rec(state, to_code_assign(instruction.code));
249276

250-
state.source.pc++;
277+
symex_transition(state);
251278
break;
252279

253280
case FUNCTION_CALL:
@@ -267,58 +294,58 @@ void goto_symext::symex_step(
267294
symex_function_call(goto_functions, state, deref_code);
268295
}
269296
else
270-
state.source.pc++;
297+
symex_transition(state);
271298
break;
272299

273300
case OTHER:
274301
if(!state.guard.is_false())
275302
symex_other(goto_functions, state);
276303

277-
state.source.pc++;
304+
symex_transition(state);
278305
break;
279306

280307
case DECL:
281308
if(!state.guard.is_false())
282309
symex_decl(state);
283310

284-
state.source.pc++;
311+
symex_transition(state);
285312
break;
286313

287314
case DEAD:
288315
symex_dead(state);
289-
state.source.pc++;
316+
symex_transition(state);
290317
break;
291318

292319
case START_THREAD:
293320
symex_start_thread(state);
294-
state.source.pc++;
321+
symex_transition(state);
295322
break;
296323

297324
case END_THREAD:
298325
// behaves like assume(0);
299326
if(!state.guard.is_false())
300327
state.guard.add(false_exprt());
301-
state.source.pc++;
328+
symex_transition(state);
302329
break;
303330

304331
case ATOMIC_BEGIN:
305332
symex_atomic_begin(state);
306-
state.source.pc++;
333+
symex_transition(state);
307334
break;
308335

309336
case ATOMIC_END:
310337
symex_atomic_end(state);
311-
state.source.pc++;
338+
symex_transition(state);
312339
break;
313340

314341
case CATCH:
315342
symex_catch(state);
316-
state.source.pc++;
343+
symex_transition(state);
317344
break;
318345

319346
case THROW:
320347
symex_throw(state);
321-
state.source.pc++;
348+
symex_transition(state);
322349
break;
323350

324351
case NO_INSTRUCTION_TYPE:

0 commit comments

Comments
 (0)