CBMC: /home/runner/work/cbmc/cbmc/src/goto-symex/symex_goto.cpp Source File

28 void goto_symext::apply_goto_condition(

29 goto_symex_statet &current_state,

30 goto_statet &jump_taken_state,

31 goto_statet &jump_not_taken_state,

32 const exprt &original_guard,

33 const exprt &new_guard,

34 const namespacet &ns)

35{

36 // It would be better to call try_filter_value_sets after apply_condition,

37 // and pass nullptr for value sets which apply_condition successfully updated

38 // already. However, try_filter_value_sets calls rename to do constant

39 // propagation, and apply_condition can update the constant propagator. Since

40 // apply condition will never succeed on both jump_taken_state and

41 // jump_not_taken_state, it should be possible to pass a reference to an

42 // unmodified goto_statet to use for renaming. But renaming needs a

43 // goto_symex_statet, not just a goto_statet, and we only have access to one

44 // of those. A future improvement would be to split rename into two parts:

45 // one part on goto_symex_statet which is non-const and deals with

46 // l2 thread reads, and one part on goto_statet which is const and could be

47 // used in try_filter_value_sets.

48

49 try_filter_value_sets(

50 current_state,

51 original_guard,

52 jump_taken_state.value_set,

53 &jump_taken_state.value_set,

54 &jump_not_taken_state.value_set,

55 ns);

56

57 if(!symex_config.constant_propagation)

58 return;

59

60 jump_taken_state.apply_condition(new_guard, current_state, ns);

61

62 // Could use not_exprt + simplify, but let's avoid paying that cost on quite

63 // a hot path:

64 const exprt negated_new_guard = boolean_negate(new_guard);

65 jump_not_taken_state.apply_condition(negated_new_guard, current_state, ns);

66}

68 void goto_symext::symex_goto(statet &state)

69{

70 PRECONDITION(state.reachable);

71

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

73

74 exprt new_guard = clean_expr(instruction.condition(), state, false);

75

76 renamedt<exprt, L2> renamed_guard = state.rename(std::move(new_guard), ns);

77 if(symex_config.simplify_opt)

78 {

79 simplify_expr_with_value_sett simp{state.value_set, language_mode, ns};

80 renamed_guard.simplify(simp);

81 }

82 new_guard = renamed_guard.get();

83

84 if(new_guard == false)

85 {

86 target.location(state.guard.as_expr(), state.source);

87

88 // next instruction

89 symex_transition(state);

90 return; // nothing to do

91 }

92

93 target.goto_instruction(state.guard.as_expr(), renamed_guard, state.source);

94

95 DATA_INVARIANT(

96 !instruction.targets.empty(), "goto should have at least one target");

97

98 // we only do deterministic gotos for now

99 DATA_INVARIANT(

100 instruction.targets.size() == 1, "no support for non-deterministic gotos");

101

102 goto_programt::const_targett goto_target=

103 instruction.get_target();

104

105 const bool backward = instruction.is_backwards_goto();

106

107 if(backward)

108 {

109 // is it label: goto label; or while(cond); - popular in SV-COMP

110 if(

111 symex_config.self_loops_to_assumptions &&

112 // label: goto label; or do {} while(cond);

113 (goto_target == state.source.pc ||

114 // while(cond);

115 (instruction.incoming_edges.size() == 1 &&

116 *instruction.incoming_edges.begin() == goto_target &&

117 goto_target->is_goto() && new_guard == true)))

118 {

119 // generate assume(false) or a suitable negation if this

120 // instruction is a conditional goto

121 exprt negated_guard = boolean_negate(new_guard);

122 do_simplify(negated_guard, state.value_set);

123 log.statistics() << "replacing self-loop at "

124 << state.source.pc->source_location() << " by assume("

125 << from_expr(ns, state.source.function_id, negated_guard)

126 << ")" << messaget::eom;

127 if(symex_config.unwinding_assertions)

128 {

129 log.warning()

130 << "no unwinding assertion will be generated for self-loop at "

131 << state.source.pc->source_location() << messaget::eom;

132 }

133 symex_assume_l2(state, negated_guard);

134

135 // next instruction

136 symex_transition(state);

137 return;

138 }

139

140 const auto loop_id =

141 goto_programt::loop_id(state.source.function_id, *state.source.pc);

142

143 unsigned &unwind = state.call_stack().top().loop_iterations[loop_id].count;

144 unwind++;

145

146 if(should_stop_unwind(state.source, state.call_stack(), unwind))

147 {

148 // we break the loop

149 loop_bound_exceeded(state, new_guard);

150

151 // next instruction

152 symex_transition(state);

153 return;

154 }

155

156 if(new_guard == true)

157 {

158 // we continue executing the loop

159 if(check_break(loop_id, unwind))

160 {

161 should_pause_symex = true;

162 }

163 symex_transition(state, goto_target, true);

164 return; // nothing else to do

165 }

166 }

167

168 // No point executing both branches of an unconditional goto.

169 if(

170 new_guard == true && // We have an unconditional goto, AND

171 // either there are no reachable blocks between us and the target in the

172 // surrounding scope (because state.guard == true implies there is no path

173 // around this GOTO instruction)

174 (state.guard.is_true() ||

175 // or there is another block, but we're doing path exploration so

176 // we're going to skip over it for now and return to it later.

177 symex_config.doing_path_exploration))

178 {

179 DATA_INVARIANT(

180 instruction.targets.size() > 0,

181 "Instruction is an unconditional goto with no target: " +

182 instruction.code().pretty());

183 symex_transition(state, instruction.get_target(), true);

184 return;

185 }

186

187 goto_programt::const_targett new_state_pc, state_pc;

188 symex_targett::sourcet original_source=state.source;

189

190 if(!backward)

191 {

192 new_state_pc=goto_target;

193 state_pc=state.source.pc;

194 state_pc++;

195

196 // skip dead instructions

197 if(new_guard == true)

198 while(state_pc!=goto_target && !state_pc->is_target())

199 ++state_pc;

200

201 if(state_pc==goto_target)

202 {

203 symex_transition(state, goto_target, false);

204 return; // nothing else to do

205 }

206 }

207 else

208 {

209 new_state_pc=state.source.pc;

210 new_state_pc++;

211 state_pc=goto_target;

212 }

213

214 // Normally the next instruction to execute would be state_pc and we save

215 // new_state_pc for later. But if we're executing from a saved state, then

216 // new_state_pc should be the state that we saved from earlier, so let's

217 // execute that instead.

218 if(state.has_saved_jump_target)

219 {

220 INVARIANT(

221 new_state_pc == state.saved_target,

222 "Tried to explore the other path of a branch, but the next "

223 "instruction along that path is not the same as the instruction "

224 "that we saved at the branch point. Saved instruction is " +

225 state.saved_target->code().pretty() +

226 "\nwe were intending "

227 "to explore " +

228 new_state_pc->code().pretty() +

229 "\nthe "

230 "instruction we think we saw on a previous path exploration is " +

231 state_pc->code().pretty());

232 goto_programt::const_targett tmp = new_state_pc;

233 new_state_pc = state_pc;

234 state_pc = tmp;

235

236 log.debug() << "Resuming from jump target '" << state_pc->source_location()

237 << "'" << log.eom;

238 }

239 else if(state.has_saved_next_instruction)

240 {

241 log.debug() << "Resuming from next instruction '"

242 << state_pc->source_location() << "'" << log.eom;

243 }

244 else if(symex_config.doing_path_exploration)

245 {

246 // We should save both the instruction after this goto, and the target of

247 // the goto.

248

249 path_storaget::patht next_instruction(target, state);

250 next_instruction.state.saved_target = state_pc;

251 next_instruction.state.has_saved_next_instruction = true;

252

253 path_storaget::patht jump_target(target, state);

254 jump_target.state.saved_target = new_state_pc;

255 jump_target.state.has_saved_jump_target = true;

256 // `forward` tells us where the branch we're _currently_ executing is

257 // pointing to; this needs to be inverted for the branch that we're saving,

258 // so let its truth value for `backwards` be the same as ours for `forward`.

259

260 log.debug() << "Saving next instruction '"

261 << next_instruction.state.saved_target->source_location() << "'"

262 << log.eom;

263 log.debug() << "Saving jump target '"

264 << jump_target.state.saved_target->source_location() << "'"

265 << log.eom;

266 path_storage.push(next_instruction);

267 path_storage.push(jump_target);

268

269 // It is now up to the caller of symex to decide which path to continue

270 // executing. Signal to the caller that states have been pushed (therefore

271 // symex has not yet completed and must be resumed), and bail out.

272 should_pause_symex = true;

273 return;

274 }

275

276 // put a copy of the current state into the state-queue, to be used by

277 // merge_gotos when we visit new_state_pc

278 framet::goto_state_listt &goto_state_list =

279 state.call_stack().top().goto_state_map[new_state_pc];

280

281 // On an unconditional GOTO we don't need our state, as it will be overwritten

282 // by merge_goto. Therefore we move it onto goto_state_list instead of copying

283 // as usual.

284 if(new_guard == true)

285 {

286 // The move here only moves goto_statet, the base class of goto_symex_statet

287 // and not the entire thing.

288 goto_state_list.emplace_back(state.source, std::move(state));

289

290 symex_transition(state, state_pc, backward);

291

292 state.guard = guardt(false_exprt(), guard_manager);

293 state.reachable = false;

294 }

295 else

296 {

297 goto_state_list.emplace_back(state.source, state);

298

299 symex_transition(state, state_pc, backward);

300

301 if(!symex_config.doing_path_exploration)

302 {

303 // This doesn't work for --paths (single-path mode) yet, as in multi-path

304 // mode we remove the implied constants at a control-flow merge, but in

305 // single-path mode we don't run merge_gotos.

306 auto &taken_state = backward ? state : goto_state_list.back().second;

307 auto &not_taken_state = backward ? goto_state_list.back().second : state;

308

309 apply_goto_condition(

310 state,

311 taken_state,

312 not_taken_state,

313 instruction.condition(),

314 new_guard,

315 ns);

316 }

317

318 // produce new guard symbol

319 exprt guard_expr;

320

321 if(

322 new_guard.id() == ID_symbol ||

323 (new_guard.id() == ID_not &&

324 to_not_expr(new_guard).op().id() == ID_symbol))

325 {

326 guard_expr=new_guard;

327 }

328 else

329 {

330 symbol_exprt guard_symbol_expr =

331 symbol_exprt(statet::guard_identifier(), bool_typet());

332 exprt new_rhs = boolean_negate(new_guard);

333

334 ssa_exprt new_lhs =

335 state.rename_ssa<L1>(ssa_exprt{guard_symbol_expr}, ns).get();

336 new_lhs =

337 state.assignment(std::move(new_lhs), new_rhs, ns, true, false).get();

338

339 guardt guard{true_exprt{}, guard_manager};

340

341 log.conditional_output(

342 log.debug(),

343 [this, &new_lhs](messaget::mstreamt &mstream)

344 {

345 mstream << "Assignment to " << new_lhs.identifier() << " ["

346 << pointer_offset_bits(new_lhs.type(), ns).value_or(0)

347 << " bits]" << messaget::eom;

348 });

349

350 target.assignment(

351 guard.as_expr(),

352 new_lhs, new_lhs, guard_symbol_expr,

353 new_rhs,

354 original_source,

355 symex_targett::assignment_typet::GUARD);

356

357 guard_expr = state.rename(boolean_negate(guard_symbol_expr), ns).get();

358 }

359

360 if(state.has_saved_jump_target)

361 {

362 if(!backward)

363 state.guard.add(guard_expr);

364 else

365 state.guard.add(boolean_negate(guard_expr));

366 }

367 else

368 {

369 goto_statet &new_state = goto_state_list.back().second;

370 if(!backward)

371 {

372 new_state.guard.add(guard_expr);

373 state.guard.add(boolean_negate(guard_expr));

374 }

375 else

376 {

377 state.guard.add(guard_expr);

378 new_state.guard.add(boolean_negate(guard_expr));

379 }

380 }

381 }

382}

384 void goto_symext::symex_unreachable_goto(statet &state)

385{

386 PRECONDITION(!state.reachable);

387 // This is like symex_goto, except the state is unreachable. We try to take

388 // some arbitrary choice that maintains the state guard in a reasonable state

389 // in order that it simplifies properly when states are merged (in

390 // merge_gotos). Note we can't try to evaluate the actual GOTO guard because

391 // our constant propagator might be out of date, since we haven't been

392 // executing assign instructions.

393

394 // If the guard is already false then there's no value in this state; just

395 // carry on and check the next instruction.

396 if(state.guard.is_false())

397 {

398 symex_transition(state);

399 return;

400 }

401

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

403 PRECONDITION(instruction.is_goto());

404 goto_programt::const_targett goto_target = instruction.get_target();

405

406 auto queue_unreachable_state_at_target = [&]() {

407 framet::goto_state_listt &goto_state_list =

408 state.call_stack().top().goto_state_map[goto_target];

409 goto_statet new_state(state.guard_manager);

410 new_state.guard = state.guard;

411 new_state.reachable = false;

412 goto_state_list.emplace_back(state.source, std::move(new_state));

413 };

414

415 if(instruction.condition() == true)

416 {

417 if(instruction.is_backwards_goto())

418 {

419 // Give up trying to salvage the guard

420 // (this state's guard is squashed, without queueing it at the target)

421 }

422 else

423 {

424 // Take the branch:

425 queue_unreachable_state_at_target();

426 }

427

428 state.guard.add(false_exprt());

429 }

430 else

431 {

432 // Arbitrarily assume a conditional branch is not-taken, except for when

433 // there's an incoming backedge, when we guess that the taken case is less

434 // likely to lead to that backedge than the not-taken case.

435 bool maybe_loop_head = std::any_of(

436 instruction.incoming_edges.begin(),

437 instruction.incoming_edges.end(),

438 [&instruction](const goto_programt::const_targett predecessor) {

439 return predecessor->location_number > instruction.location_number;

440 });

441

442 if(instruction.is_backwards_goto() || !maybe_loop_head)

443 {

444 // Assume branch not taken (fall through)

445 }

446 else

447 {

448 // Assume branch taken:

449 queue_unreachable_state_at_target();

450 state.guard.add(false_exprt());

451 }

452 }

453

454 symex_transition(state);

455}

457 bool goto_symext::check_break(const irep_idt &loop_id, unsigned unwind)

458{

459 // dummy implementation

460 return false;

461}

463 void goto_symext::merge_gotos(statet &state)

464{

465 framet &frame = state.call_stack().top();

466

467 // first, see if this is a target at all

468 auto state_map_it = frame.goto_state_map.find(state.source.pc);

469

470 if(state_map_it==frame.goto_state_map.end())

471 return; // nothing to do

472

473 // we need to merge

474 framet::goto_state_listt &state_list = state_map_it->second;

475

476 for(auto list_it = state_list.rbegin(); list_it != state_list.rend();

477 ++list_it)

478 {

479 merge_goto(list_it->first, std::move(list_it->second), state);

480 }

481

482 // clean up to save some memory

483 frame.goto_state_map.erase(state_map_it);

484}

487 merge_state_guards(goto_statet &goto_state, goto_symex_statet &state)

488{

489 // adjust guard, even using guards from unreachable states. This helps to

490 // shrink the state guard if the incoming edge is from a path that was

491 // truncated by config.unwind, config.depth or an assume-false instruction.

492

493 // Note when an unreachable state contributes its guard, merging it in is

494 // optional, since the formula already implies the unreachable guard is

495 // impossible. Therefore we only integrate it when to do so simplifies the

496 // state guard.

497

498 // This function can trash either state's guards, since goto_state is dying

499 // and state's guard will shortly be overwritten.

500

501 if(

502 (goto_state.reachable && state.reachable) ||

503 state.guard.disjunction_may_simplify(goto_state.guard))

504 {

505 state.guard |= goto_state.guard;

506 return std::move(state.guard);

507 }

508 else if(!state.reachable && goto_state.reachable)

509 {

510 return std::move(goto_state.guard);

511 }

512 else

513 {

514 return std::move(state.guard);

515 }

516}

518 void goto_symext::merge_goto(

519 const symex_targett::sourcet &,

520 goto_statet &&goto_state,

521 statet &state)

522{

523 // check atomic section

524 if(state.atomic_section_id != goto_state.atomic_section_id)

525 throw incorrect_goto_program_exceptiont(

526 "atomic sections differ across branches",

527 state.source.pc->source_location());

528

529 // Merge guards. Don't write this to `state` yet because we might move

530 // goto_state over it below.

531 guardt new_guard = merge_state_guards(goto_state, state);

532

533 // Merge constant propagator, value-set etc. only if the incoming state is

534 // reachable:

535 if(goto_state.reachable)

536 {

537 if(!state.reachable)

538 {

539 // Important to note that we're moving into our base class here.

540 // Note this overwrites state.guard, but we restore it below.

541 static_cast<goto_statet &>(state) = std::move(goto_state);

542 }

543 else

544 {

545 // do SSA phi functions

546 phi_function(goto_state, state);

547

548 // merge value sets

549 state.value_set.make_union(goto_state.value_set);

550

551 // adjust depth

552 state.depth = std::min(state.depth, goto_state.depth);

553 }

554 }

555

556 // Save the new state guard

557 state.guard = std::move(new_guard);

558}

575 static void merge_names(

576 const goto_statet &goto_state,

577 goto_symext::statet &dest_state,

578 const namespacet &ns,

579 const guardt &diff_guard,

580 messaget &log,

581 const bool do_simplify,

582 symex_target_equationt &target,

583 const incremental_dirtyt &dirty,

584 const ssa_exprt &ssa,

585 const std::size_t goto_count,

586 const std::size_t dest_count)

587{

588 const irep_idt l1_identifier = ssa.identifier();

589 const irep_idt &obj_identifier = ssa.get_object_name();

590

591 if(obj_identifier == goto_symext::statet::guard_identifier())

592 return; // just a guard, don't bother

593

594 if(goto_count == dest_count)

595 return; // not at all changed

596

597 // changed - but only on a branch that is now dead, and the other branch is

598 // uninitialized/invalid

599 if(

600 (!dest_state.reachable && goto_count == 0) ||

601 (!goto_state.reachable && dest_count == 0))

602 {

603 return;

604 }

605

606 // field sensitivity: only merge on individual fields

607 if(dest_state.field_sensitivity.is_divisible(ssa, true))

608 return;

609

610 // shared variables are renamed on every access anyway, we don't need to

611 // merge anything

612 const symbolt &symbol = ns.lookup(obj_identifier);

613

614 // shared?

615 if(

616 dest_state.atomic_section_id == 0 && dest_state.threads.size() >= 2 &&

617 (symbol.is_shared() || dirty(symbol.name)))

618 {

619 return; // no phi nodes for shared stuff

620 }

621

622 // don't merge (thread-)locals across different threads, which

623 // may have been introduced by symex_start_thread (and will

624 // only later be removed from level2.current_names by pop_frame

625 // once the thread is executed)

626 const irep_idt level_0 = ssa.get_level_0();

627 if(

628 !level_0.empty() &&

629 level_0 != std::to_string(dest_state.source.thread_nr) && dest_count != 0)

630 {

631 return;

632 }

633

634 exprt goto_state_rhs = ssa, dest_state_rhs = ssa;

635

636 {

637 const auto p_it = goto_state.propagation.find(l1_identifier);

638

639 if(p_it.has_value())

640 goto_state_rhs = *p_it;

641 else

642 to_ssa_expr(goto_state_rhs).set_level_2(goto_count);

643 }

644

645 {

646 const auto p_it = dest_state.propagation.find(l1_identifier);

647

648 if(p_it.has_value())

649 dest_state_rhs = *p_it;

650 else

651 to_ssa_expr(dest_state_rhs).set_level_2(dest_count);

652 }

653

654 exprt rhs;

655

656 // Don't add a conditional to the assignment when:

657 // 1. Either guard is false, so we can't follow that branch.

658 // 2. Either identifier is of generation zero, and so hasn't been

659 // initialized and therefore an invalid target.

660

661 // These rules only apply to dynamic objects and locals.

662 if(!dest_state.reachable)

663 rhs = goto_state_rhs;

664 else if(!goto_state.reachable)

665 rhs = dest_state_rhs;

666 else if(goto_count == 0)

667 rhs = dest_state_rhs;

668 else if(dest_count == 0)

669 rhs = goto_state_rhs;

670 else

671 {

672 rhs = if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);

673 if(do_simplify)

674 {

675 // Do not value-set supported filtering here as neither dest_state nor

676 // goto_state necessarily have a comprehensive value set.

677 simplify(rhs, ns);

678 }

679 }

680

681 dest_state.record_events.push(false);

682 const ssa_exprt new_lhs =

683 dest_state.assignment(ssa, rhs, ns, true, true).get();

684 dest_state.record_events.pop();

685

686 log.conditional_output(

687 log.debug(),

688 [ns, &new_lhs](messaget::mstreamt &mstream)

689 {

690 mstream << "Assignment to " << new_lhs.identifier() << " ["

691 << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]"

692 << messaget::eom;

693 });

694

695 target.assignment(

696 true_exprt(),

697 new_lhs,

698 new_lhs,

699 new_lhs.get_original_expr(),

700 rhs,

701 dest_state.source,

702 symex_targett::assignment_typet::PHI);

703}

705 void goto_symext::phi_function(

706 const goto_statet &goto_state,

707 statet &dest_state)

708{

709 if(

710 goto_state.get_level2().current_names.empty() &&

711 dest_state.get_level2().current_names.empty())

712 return;

713

714 guardt diff_guard = goto_state.guard;

715 // this gets the diff between the guards

716 diff_guard -= dest_state.guard;

717

718 symex_renaming_levelt::delta_viewt delta_view;

719 goto_state.get_level2().current_names.get_delta_view(

720 dest_state.get_level2().current_names, delta_view, false);

721

722 std::map<std::string, symex_renaming_levelt::delta_viewt::const_iterator>

723 ordered_names_to_merge;

724 for(auto it = delta_view.begin(); it != delta_view.end(); ++it)

725 {

726 const ssa_exprt &ssa = it->m.first;

727 bool inserted =

728 ordered_names_to_merge.insert({id2string(ssa.get_identifier()), it})

729 .second;

730 CHECK_RETURN(inserted);

731 }

732

733 for(const auto &ordered_entry : ordered_names_to_merge)

734 {

735 const auto &delta_item = *ordered_entry.second;

736 const ssa_exprt &ssa = delta_item.m.first;

737 std::size_t goto_count = delta_item.m.second;

738 std::size_t dest_count = !delta_item.is_in_both_maps()

739 ? 0

740 : delta_item.get_other_map_value().second;

741

742 merge_names(

743 goto_state,

744 dest_state,

745 ns,

746 diff_guard,

747 log,

748 symex_config.simplify_opt,

749 target,

750 path_storage.dirty,

751 ssa,

752 goto_count,

753 dest_count);

754 }

755

756 delta_view.clear();

757 dest_state.get_level2().current_names.get_delta_view(

758 goto_state.get_level2().current_names, delta_view, false);

759

760 ordered_names_to_merge.clear();

761 for(auto it = delta_view.begin(); it != delta_view.end(); ++it)

762 {

763 if(it->is_in_both_maps())

764 continue;

765

766 const ssa_exprt &ssa = it->m.first;

767 bool inserted =

768 ordered_names_to_merge.insert({id2string(ssa.get_identifier()), it})

769 .second;

770 CHECK_RETURN(inserted);

771 }

772

773 for(const auto &ordered_entry : ordered_names_to_merge)

774 {

775 const auto &delta_item = *ordered_entry.second;

776 const ssa_exprt &ssa = delta_item.m.first;

777 std::size_t goto_count = 0;

778 std::size_t dest_count = delta_item.m.second;

779

780 merge_names(

781 goto_state,

782 dest_state,

783 ns,

784 diff_guard,

785 log,

786 symex_config.simplify_opt,

787 target,

788 path_storage.dirty,

789 ssa,

790 goto_count,

791 dest_count);

792 }

793}

795 void goto_symext::loop_bound_exceeded(

796 statet &state,

797 const exprt &guard)

798{

799 const std::string loop_number = std::to_string(state.source.pc->loop_number);

800

801 exprt negated_cond = boolean_negate(guard);

802

803 if(symex_config.unwinding_assertions)

804 {

805 // Generate VCC for unwinding assertion.

806 const std::string property_id =

807 id2string(state.source.pc->source_location().get_function()) +

808 ".unwind." + loop_number;

809 vcc(

810 negated_cond,

811 property_id,

812 "unwinding assertion loop " + loop_number,

813 state);

814 }

815

816 if(!symex_config.partial_loops)

817 {

818 // generate unwinding assumption, unless we permit partial loops

819 symex_assume_l2(state, negated_cond);

820 }

821}

823 bool goto_symext::should_stop_unwind(

824 const symex_targett::sourcet &,

825 const call_stackt &,

826 unsigned)

827{

828 // by default, we keep going

829 return false;

830}

guard

static exprt guard(const exprt::operandst &guards, exprt cond)

Definition c_safety_checks.cpp:69

ai_baset::clear

virtual void clear()

Reset the abstract state.

Definition ai.h:269

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

bool_typet

The Boolean type.

Definition std_types.h:35

call_stackt

Definition call_stack.h:15

call_stackt::top

framet & top()

Definition call_stack.h:17

dstringt

dstringt has one field, an unsigned integer no which is an index into a static table of strings.

Definition dstring.h:38

exprt

Base class for all expressions.

Definition expr.h:57

false_exprt

The Boolean constant false.

Definition std_expr.h:3135

framet

Stack frames – these are used for function calls and for exceptions.

Definition solver_types.h:41

framet::goto_state_listt

std::list< std::pair< symex_targett::sourcet, goto_statet > > goto_state_listt

Definition frame.h:25

framet::loop_iterations

std::unordered_map< irep_idt, loop_infot > loop_iterations

Definition frame.h:77

framet::goto_state_map

std::map< goto_programt::const_targett, goto_state_listt, goto_programt::target_less_than > goto_state_map

Definition frame.h:33

goto_programt::instructiont

This class represents an instruction in the GOTO intermediate representation.

Definition goto_program.h:180

goto_programt::instructiont::is_goto

bool is_goto() const

Definition goto_program.h:490

goto_programt::instructiont::code

const goto_instruction_codet & code() const

Get the code represented by this instruction.

Definition goto_program.h:187

goto_programt::instructiont::targets

targetst targets

The list of successor instructions.

Definition goto_program.h:413

goto_programt::instructiont::is_backwards_goto

bool is_backwards_goto() const

Returns true if the instruction is a backwards branch.

Definition goto_program.h:568

goto_programt::instructiont::incoming_edges

std::set< targett, target_less_than > incoming_edges

Definition goto_program.h:449

goto_programt::instructiont::condition

const exprt & condition() const

Get the condition of gotos, assume, assert.

Definition goto_program.h:365

goto_programt::instructiont::get_target

const_targett get_target() const

Returns the first (and only) successor for the usual case of a single target.

Definition goto_program.h:417

goto_programt::loop_id

static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)

Human-readable loop name.

Definition goto_program.h:791

goto_programt::const_targett

instructionst::const_iterator const_targett

Definition goto_program.h:614

goto_statet

Container for data that varies per program point, e.g.

Definition goto_state.h:32

goto_statet::guard

guardt guard

Definition goto_state.h:58

goto_statet::depth

unsigned depth

Distance from entry.

Definition goto_state.h:35

goto_statet::reachable

bool reachable

Is this code reachable? If not we can take shortcuts such as not entering function calls,...

Definition goto_state.h:62

goto_statet::atomic_section_id

unsigned atomic_section_id

Threads.

Definition goto_state.h:76

goto_statet::value_set

value_sett value_set

Uses level 1 names, and is used to do dereferencing.

Definition goto_state.h:51

goto_symex_statet

Central data structure: state.

Definition goto_symex_state.h:42

goto_symex_statet::saved_target

goto_programt::const_targett saved_target

Definition goto_symex_state.h:217

goto_symex_statet::call_stack

call_stackt & call_stack()

Definition goto_symex_state.h:147

goto_symex_statet::guard_identifier

static irep_idt guard_identifier()

Definition goto_symex_state.h:141

goto_symex_statet::assignment

renamedt< ssa_exprt, L2 > assignment(ssa_exprt lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)

Definition goto_symex_state.cpp:78

goto_symex_statet::guard_manager

guard_managert & guard_manager

Definition goto_symex_state.h:70

goto_symex_statet::rename

renamedt< exprt, level > rename(exprt expr, const namespacet &ns)

Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...

Definition goto_symex_state.cpp:163

goto_symex_statet::source

symex_targett::sourcet source

Definition goto_symex_state.h:62

goto_symex_statet::has_saved_jump_target

bool has_saved_jump_target

This state is saved, with the PC pointing to the target of a GOTO.

Definition goto_symex_state.h:220

goto_symex_statet::rename_ssa

renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)

Version of rename which is specialized for SSA exprt.

Definition goto_symex_state.cpp:144

goto_symex_statet::has_saved_next_instruction

bool has_saved_next_instruction

This state is saved, with the PC pointing to the next instruction of a GOTO.

Definition goto_symex_state.h:224

goto_symext::should_stop_unwind

virtual bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind)

Determine whether to unwind a loop.

Definition symex_goto.cpp:823

goto_symext::try_filter_value_sets

void try_filter_value_sets(goto_symex_statet &state, exprt condition, const value_sett &original_value_set, value_sett *jump_taken_value_set, value_sett *jump_not_taken_value_set, const namespacet &ns)

Try to filter value sets based on whether possible values of a pointer-typed symbol make the conditio...

Definition symex_main.cpp:781

goto_symext::apply_goto_condition

void apply_goto_condition(goto_symex_statet &current_state, goto_statet &jump_taken_state, goto_statet &jump_not_taken_state, const exprt &original_guard, const exprt &new_guard, const namespacet &ns)

Propagate constants and points-to information implied by a GOTO condition.

Definition symex_goto.cpp:28

goto_symext::check_break

virtual bool check_break(const irep_idt &loop_id, unsigned unwind)

Defines condition for interrupting symbolic execution for a specific loop.

Definition symex_goto.cpp:457

goto_symext::symex_unreachable_goto

void symex_unreachable_goto(statet &state)

Symbolically execute a GOTO instruction in the context of unreachable code.

Definition symex_goto.cpp:384

goto_symext::language_mode

irep_idt language_mode

language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...

Definition goto_symex.h:240

goto_symext::symex_goto

virtual void symex_goto(statet &state)

Symbolically execute a GOTO instruction.

Definition symex_goto.cpp:68

goto_symext::phi_function

void phi_function(const goto_statet &goto_state, statet &dest_state)

Merge the SSA assignments from goto_state into dest_state.

Definition symex_goto.cpp:705

goto_symext::path_storage

path_storaget & path_storage

Symbolic execution paths to be resumed later.

Definition goto_symex.h:808

goto_symext::target

symex_target_equationt & target

The equation that this execution is building up.

Definition goto_symex.h:264

goto_symext::guard_manager

guard_managert & guard_manager

Used to create guards.

Definition goto_symex.h:261

goto_symext::clean_expr

exprt clean_expr(exprt expr, statet &state, bool write)

Clean up an expression.

Definition symex_clean_expr.cpp:231

goto_symext::loop_bound_exceeded

virtual void loop_bound_exceeded(statet &state, const exprt &guard)

Definition symex_goto.cpp:795

goto_symext::ns

namespacet ns

Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...

Definition goto_symex.h:256

goto_symext::vcc

virtual void vcc(const exprt &cond, const irep_idt &property_id, const std::string &msg, statet &state)

Symbolically execute a verification condition (assertion).

Definition symex_main.cpp:180

goto_symext::merge_goto

virtual void merge_goto(const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state)

Merge a single branch, the symbolic state of which is held in goto_state, into the current overall sy...

Definition symex_goto.cpp:518

goto_symext::do_simplify

virtual void do_simplify(exprt &expr, const value_sett &value_set)

Definition goto_symex.cpp:32

goto_symext::log

messaget log

The messaget to write log messages to.

Definition goto_symex.h:276

goto_symext::symex_config

const symex_configt symex_config

The configuration to use for this symbolic execution.

Definition goto_symex.h:186

goto_symext::should_pause_symex

bool should_pause_symex

Set when states are pushed onto the workqueue If this flag is set at the end of a symbolic execution ...

Definition goto_symex.h:168

goto_symext::symex_assume_l2

void symex_assume_l2(statet &, const exprt &cond)

Definition symex_main.cpp:219

goto_symext::merge_gotos

void merge_gotos(statet &state)

Merge all branches joining at the current program point.

Definition symex_goto.cpp:463

guard_exprt

Definition guard_expr.h:24

guard_exprt::add

void add(const exprt &expr)

Definition guard_expr.cpp:38

guard_exprt::is_true

bool is_true() const

Definition guard_expr.h:60

guard_exprt::disjunction_may_simplify

bool disjunction_may_simplify(const guard_exprt &other_guard)

Returns true if operator|= with other_guard may result in a simpler expression.

Definition guard_expr.cpp:123

guard_exprt::as_expr

exprt as_expr() const

Definition guard_expr.h:46

guard_exprt::is_false

bool is_false() const

Definition guard_expr.h:65

if_exprt

The trinary if-then-else operator.

Definition std_expr.h:2426

incorrect_goto_program_exceptiont

Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...

Definition exception_utils.h:92

incremental_dirtyt

Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...

Definition dirty.h:118

messaget::mstreamt

Definition message.h:216

messaget

Class that provides messages with a built-in verbosity 'level'.

Definition message.h:154

messaget::debug

mstreamt & debug() const

Definition message.h:431

messaget::statistics

mstreamt & statistics() const

Definition message.h:421

messaget::warning

mstreamt & warning() const

Definition message.h:406

messaget::conditional_output

void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const

Generate output to message_stream using output_generator if the configured verbosity is at least as h...

Definition message.cpp:149

messaget::eom

static eomt eom

Definition message.h:289

namespacet

A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...

Definition namespace.h:91

namespacet::lookup

bool lookup(const irep_idt &name, const symbolt *&symbol) const override

See documentation for namespace_baset::lookup().

Definition namespace.cpp:134

path_storaget::dirty

incremental_dirtyt dirty

Local variables are considered 'dirty' if they've had an address taken and therefore may be referred ...

Definition path_storage.h:116

path_storaget::push

virtual void push(const patht &)=0

Add a path to resume to the storage.

sharing_mapt< irep_idt, std::pair< ssa_exprt, std::size_t > >::delta_viewt

std::vector< delta_view_itemt > delta_viewt

Delta view of the key-value pairs in two maps.

Definition sharing_map.h:439

simplify_expr_with_value_sett

Definition simplify_expr_with_value_set.h:17

ssa_exprt

Expression providing an SSA-renamed symbol of expressions.

Definition ssa_expr.h:17

symbol_exprt

Expression to hold a symbol (variable)

Definition std_expr.h:132

symbolt

Symbol table entry.

Definition symbol.h:28

symbolt::name

irep_idt name

The unique identifier.

Definition symbol.h:40

symbolt::is_shared

bool is_shared() const

Definition symbol.h:101

symex_target_equationt

Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...

Definition symex_target_equation.h:34

symex_target_equationt::goto_instruction

virtual void goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)

Record a goto instruction.

Definition symex_target_equation.cpp:300

symex_target_equationt::location

virtual void location(const exprt &guard, const sourcet &source)

Record a location.

Definition symex_target_equation.cpp:169

symex_target_equationt::assignment

virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)

Write to a local variable.

Definition symex_target_equation.cpp:113

symex_targett::assignment_typet::GUARD

@ GUARD

symex_targett::assignment_typet::PHI

@ PHI

true_exprt

The Boolean constant true.

Definition std_expr.h:3126

value_sett::make_union

bool make_union(object_mapt &dest, const object_mapt &src) const

Merges two RHS expression sets.

Definition value_set.cpp:320

exception_utils.h

boolean_negate

exprt boolean_negate(const exprt &src)

negate a Boolean expression, possibly removing a not_exprt, and swapping false and true

Definition expr_util.cpp:98

expr_util.h

Deprecated expression utility functions.

goto_symex.h

Symbolic Execution.

symex_transition

void symex_transition(goto_symext::statet &state)

Transition to the next instruction, which increments the internal program counter and initializes the...

Definition symex_main.cpp:144

guardt

guard_exprt guardt

Definition guard.h:29

id2string

const std::string & id2string(const irep_idt &d)

Definition irep.h:44

from_expr

std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)

Definition language_util.cpp:39

language_util.h

log

double log(double x)

Definition math.c:2416

path_storage.h

Storage of symbolic execution paths to resume.

pointer_offset_size.h

Pointer Logic.

L1

@ L1

Definition renamed.h:24

simplify

bool simplify(exprt &expr, const namespacet &ns)

Definition simplify_expr.cpp:3407

simplify_expr.h

simplify_expr_with_value_set.h

invariant.h

CHECK_RETURN

#define CHECK_RETURN(CONDITION)

Definition invariant.h:495

DATA_INVARIANT

#define DATA_INVARIANT(CONDITION, REASON)

This condition should be used to document that assumptions that are made on goto_functions,...

Definition invariant.h:534

PRECONDITION

#define PRECONDITION(CONDITION)

Definition invariant.h:463

INVARIANT

#define INVARIANT(CONDITION, REASON)

This macro uses the wrapper function 'invariant_violated_string'.

Definition invariant.h:423

to_ssa_expr

const ssa_exprt & to_ssa_expr(const exprt &expr)

Cast a generic exprt to an ssa_exprt.

Definition ssa_expr.h:145

std_expr.h

API to expression classes.

to_not_expr

const not_exprt & to_not_expr(const exprt &expr)

Cast an exprt to an not_exprt.

Definition std_expr.h:2408

path_storaget::patht

Information saved at a conditional goto to resume execution.

Definition path_storage.h:42

symex_targett::sourcet

Identifies source in the context of symbolic execution.

Definition symex_target.h:37

symex_targett::sourcet::pc

goto_programt::const_targett pc

Definition symex_target.h:42

symex_targett::sourcet::function_id

irep_idt function_id

Definition symex_target.h:39

merge_names

static void merge_names(const goto_statet &goto_state, goto_symext::statet &dest_state, const namespacet &ns, const guardt &diff_guard, messaget &log, const bool do_simplify, symex_target_equationt &target, const incremental_dirtyt &dirty, const ssa_exprt &ssa, const std::size_t goto_count, const std::size_t dest_count)

Helper function for phi_function which merges the names of an identifier for two different states.

Definition symex_goto.cpp:575

merge_state_guards

static guardt merge_state_guards(goto_statet &goto_state, goto_symex_statet &state)

Definition symex_goto.cpp:487