symex_bmc.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Bounded Model Checking for ANSI-C
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#include "symex_bmc.h"
 
#include <util/simplify_expr.h>
#include <util/source_location.h>
 
#include <goto-programs/unwindset.h>
 
#include <limits>
 
symex_bmct::symex_bmct(
  message_handlert &mh,
  const symbol_tablet &outer_symbol_table,
  symex_target_equationt &_target,
  const optionst &options,
  path_storaget &path_storage,
  guard_managert &guard_manager,
  unwindsett &unwindset)
  : goto_symext(
      mh,
      outer_symbol_table,
      _target,
      options,
      path_storage,
      guard_manager),
    record_coverage(!options.get_option("symex-coverage-report").empty()),
    unwindset(unwindset),
    symex_coverage(ns)
{
}
 
void symex_bmct::symex_step(
  const get_goto_functiont &get_goto_function,
  statet &state)
{
  const source_locationt &source_location = state.source.pc->source_location();
 
  if(!source_location.is_nil() && last_source_location != source_location)
  {
    log.debug() << "BMC at " << source_location.as_string() << " (depth "
                << state.depth << ')' << log.eom;
 
    last_source_location = source_location;
  }
 
  const goto_programt::const_targett cur_pc = state.source.pc;
  const guardt cur_guard = state.guard;
 
  if(
    !state.guard.is_false() && state.source.pc->is_assume() &&
    simplify_expr(state.source.pc->condition(), ns).is_false())
  {
    log.statistics() << "aborting path on assume(false) at "
                     << state.source.pc->source_location() << " thread "
                     << state.source.thread_nr;
 
    const irep_idt &c = state.source.pc->source_location().get_comment();
    if(!c.empty())
      log.statistics() << ": " << c;
 
    log.statistics() << log.eom;
  }
 
  goto_symext::symex_step(get_goto_function, state);
 
  if(
    record_coverage &&
    // avoid an invalid iterator in state.source.pc
    (!cur_pc->is_end_function() ||
     state.source.function_id != goto_functionst::entry_point()))
  {
    // forward goto will effectively be covered via phi function,
    // which does not invoke symex_step; as symex_step is called
    // before merge_gotos, also state.guard will be false (we have
    // taken an impossible transition); thus we synthesize a
    // transition from the goto instruction to its target to make
    // sure the goto is considered covered
    if(
      cur_pc->is_goto() && cur_pc->get_target() != state.source.pc &&
      cur_pc->condition().is_true())
      symex_coverage.covered(cur_pc, cur_pc->get_target());
    else if(!state.guard.is_false())
      symex_coverage.covered(cur_pc, state.source.pc);
  }
}
 
void symex_bmct::merge_goto(
  const symex_targett::sourcet &prev_source,
  goto_statet &&goto_state,
  statet &state)
{
  const goto_programt::const_targett prev_pc = prev_source.pc;
  const guardt prev_guard = goto_state.guard;
 
  goto_symext::merge_goto(prev_source, std::move(goto_state), state);
 
  PRECONDITION(prev_pc->is_goto());
  if(
    record_coverage &&
    // could the branch possibly be taken?
    !prev_guard.is_false() && !state.guard.is_false() &&
    // branches only, no single-successor goto
    !prev_pc->condition().is_true())
    symex_coverage.covered(prev_pc, state.source.pc);
}
 
bool symex_bmct::should_stop_unwind(
  const symex_targett::sourcet &source,
  const call_stackt &context,
  unsigned unwind)
{
  const irep_idt id = goto_programt::loop_id(source.function_id, *source.pc);
 
  tvt abort_unwind_decision;
  unsigned this_loop_limit = std::numeric_limits<unsigned>::max();
 
  for(auto handler : loop_unwind_handlers)
  {
    abort_unwind_decision =
      handler(context, source.pc->loop_number, unwind, this_loop_limit);
    if(abort_unwind_decision.is_known())
      break;
  }
 
  // If no handler gave an opinion, use standard command-line --unwindset
  // / --unwind options to decide:
  if(abort_unwind_decision.is_unknown())
  {
    auto limit = unwindset.get_limit(id, source.thread_nr);
 
    if(!limit.has_value())
      abort_unwind_decision = tvt(false);
    else
      abort_unwind_decision = tvt(unwind >= *limit);
  }
 
  INVARIANT(
    abort_unwind_decision.is_known(), "unwind decision should be taken by now");
  bool abort = abort_unwind_decision.is_true();
 
  log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id
                   << " iteration " << unwind;
 
  if(this_loop_limit != std::numeric_limits<unsigned>::max())
    log.statistics() << " (" << this_loop_limit << " max)";
 
  log.statistics() << " " << source.pc->source_location() << " thread "
                   << source.thread_nr << log.eom;
 
  return abort;
}
 
bool symex_bmct::get_unwind_recursion(
  const irep_idt &id,
  unsigned thread_nr,
  unsigned unwind)
{
  tvt abort_unwind_decision;
  unsigned this_loop_limit = std::numeric_limits<unsigned>::max();
 
  for(auto handler : recursion_unwind_handlers)
  {
    abort_unwind_decision = handler(id, unwind, this_loop_limit);
    if(abort_unwind_decision.is_known())
      break;
  }
 
  // If no handler gave an opinion, use standard command-line --unwindset
  // / --unwind options to decide:
  if(abort_unwind_decision.is_unknown())
  {
    auto limit = unwindset.get_limit(id, thread_nr);
 
    if(!limit.has_value())
      abort_unwind_decision = tvt(false);
    else
      abort_unwind_decision = tvt(unwind > *limit);
  }
 
  INVARIANT(
    abort_unwind_decision.is_known(), "unwind decision should be taken by now");
  bool abort = abort_unwind_decision.is_true();
 
  if(unwind > 0 || abort)
  {
    const symbolt &symbol = ns.lookup(id);
 
    log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " recursion "
                     << symbol.display_name() << " iteration " << unwind;
 
    if(this_loop_limit != std::numeric_limits<unsigned>::max())
      log.statistics() << " (" << this_loop_limit << " max)";
 
    log.statistics() << log.eom;
  }
 
  return abort;
}