symex_goto.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symbolic Execution
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/

 
#include <util/exception_utils.h>
#include <util/expr_util.h>
#include <util/invariant.h>
#include <util/pointer_offset_size.h>
#include <util/simplify_expr.h>
#include <util/std_expr.h>
 
#include <langapi/language_util.h>
 
#include "goto_symex.h"
#include "path_storage.h"
#include "simplify_expr_with_value_set.h"
 
#include <algorithm>
#include <map>
 
void goto_symext::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)
{
  // It would be better to call try_filter_value_sets after apply_condition,
  // and pass nullptr for value sets which apply_condition successfully updated
  // already. However, try_filter_value_sets calls rename to do constant
  // propagation, and apply_condition can update the constant propagator. Since
  // apply condition will never succeed on both jump_taken_state and
  // jump_not_taken_state, it should be possible to pass a reference to an
  // unmodified goto_statet to use for renaming. But renaming needs a
  // goto_symex_statet, not just a goto_statet, and we only have access to one
  // of those. A future improvement would be to split rename into two parts:
  // one part on goto_symex_statet which is non-const and deals with
  // l2 thread reads, and one part on goto_statet which is const and could be
  // used in try_filter_value_sets.
 
  try_filter_value_sets(
    current_state,
    original_guard,
    jump_taken_state.value_set,
    &jump_taken_state.value_set,
    &jump_not_taken_state.value_set,
    ns);
 
  if(!symex_config.constant_propagation)
    return;
 
  jump_taken_state.apply_condition(new_guard, current_state, ns);
 
  // Could use not_exprt + simplify, but let's avoid paying that cost on quite
  // a hot path:
  const exprt negated_new_guard = boolean_negate(new_guard);
  jump_not_taken_state.apply_condition(negated_new_guard, current_state, ns);
}
 
void goto_symext::symex_goto(statet &state)
{
  PRECONDITION(state.reachable);
 
  const goto_programt::instructiont &instruction=*state.source.pc;
 
  exprt new_guard = clean_expr(instruction.condition(), state, false);
 
  renamedt<exprt, L2> renamed_guard = state.rename(std::move(new_guard), ns);
  if(symex_config.simplify_opt)
  {
    simplify_expr_with_value_sett simp{state.value_set, language_mode, ns};
    renamed_guard.simplify(simp);
  }
  new_guard = renamed_guard.get();
 
  if(new_guard == false)
  {
    target.location(state.guard.as_expr(), state.source);
 
    // next instruction
    symex_transition(state);
    return; // nothing to do
  }
 
  target.goto_instruction(state.guard.as_expr(), renamed_guard, state.source);
 
  DATA_INVARIANT(
    !instruction.targets.empty(), "goto should have at least one target");
 
  // we only do deterministic gotos for now
  DATA_INVARIANT(
    instruction.targets.size() == 1, "no support for non-deterministic gotos");
 
  goto_programt::const_targett goto_target=
    instruction.get_target();
 
  const bool backward = instruction.is_backwards_goto();
 
  if(backward)
  {
    // is it label: goto label; or while(cond); - popular in SV-COMP
    if(
      symex_config.self_loops_to_assumptions &&
      // label: goto label; or do {} while(cond);
      (goto_target == state.source.pc ||
       // while(cond);
       (instruction.incoming_edges.size() == 1 &&
        *instruction.incoming_edges.begin() == goto_target &&
        goto_target->is_goto() && new_guard == true)))
    {
      // generate assume(false) or a suitable negation if this
      // instruction is a conditional goto
      exprt negated_guard = boolean_negate(new_guard);
      do_simplify(negated_guard, state.value_set);
      log.statistics() << "replacing self-loop at "
                       << state.source.pc->source_location() << " by assume("
                       << from_expr(ns, state.source.function_id, negated_guard)
                       << ")" << messaget::eom;
      if(symex_config.unwinding_assertions)
      {
        log.warning()
          << "no unwinding assertion will be generated for self-loop at "
          << state.source.pc->source_location() << messaget::eom;
      }
      symex_assume_l2(state, negated_guard);
 
      // next instruction
      symex_transition(state);
      return;
    }
 
    const auto loop_id =
      goto_programt::loop_id(state.source.function_id, *state.source.pc);
 
    unsigned &unwind = state.call_stack().top().loop_iterations[loop_id].count;
    unwind++;
 
    if(should_stop_unwind(state.source, state.call_stack(), unwind))
    {
      // we break the loop
      loop_bound_exceeded(state, new_guard);
 
      // next instruction
      symex_transition(state);
      return;
    }
 
    if(new_guard == true)
    {
      // we continue executing the loop
      if(check_break(loop_id, unwind))
      {
        should_pause_symex = true;
      }
      symex_transition(state, goto_target, true);
      return; // nothing else to do
    }
  }
 
  // No point executing both branches of an unconditional goto.
  if(
    new_guard == true && // We have an unconditional goto, AND
    // either there are no reachable blocks between us and the target in the
    // surrounding scope (because state.guard == true implies there is no path
    // around this GOTO instruction)
    (state.guard.is_true() ||
     // or there is another block, but we're doing path exploration so
     // we're going to skip over it for now and return to it later.
     symex_config.doing_path_exploration))
  {
    DATA_INVARIANT(
      instruction.targets.size() > 0,
      "Instruction is an unconditional goto with no target: " +
        instruction.code().pretty());
    symex_transition(state, instruction.get_target(), true);
    return;
  }
 
  goto_programt::const_targett new_state_pc, state_pc;
  symex_targett::sourcet original_source=state.source;
 
  if(!backward)
  {
    new_state_pc=goto_target;
    state_pc=state.source.pc;
    state_pc++;
 
    // skip dead instructions
    if(new_guard == true)
      while(state_pc!=goto_target && !state_pc->is_target())
        ++state_pc;
 
    if(state_pc==goto_target)
    {
      symex_transition(state, goto_target, false);
      return; // nothing else to do
    }
  }
  else
  {
    new_state_pc=state.source.pc;
    new_state_pc++;
    state_pc=goto_target;
  }
 
  // Normally the next instruction to execute would be state_pc and we save
  // new_state_pc for later. But if we're executing from a saved state, then
  // new_state_pc should be the state that we saved from earlier, so let's
  // execute that instead.
  if(state.has_saved_jump_target)
  {
    INVARIANT(
      new_state_pc == state.saved_target,
      "Tried to explore the other path of a branch, but the next "
      "instruction along that path is not the same as the instruction "
      "that we saved at the branch point. Saved instruction is " +
        state.saved_target->code().pretty() +
        "\nwe were intending "
        "to explore " +
        new_state_pc->code().pretty() +
        "\nthe "
        "instruction we think we saw on a previous path exploration is " +
        state_pc->code().pretty());
    goto_programt::const_targett tmp = new_state_pc;
    new_state_pc = state_pc;
    state_pc = tmp;
 
    log.debug() << "Resuming from jump target '" << state_pc->source_location()
                << "'" << log.eom;
  }
  else if(state.has_saved_next_instruction)
  {
    log.debug() << "Resuming from next instruction '"
                << state_pc->source_location() << "'" << log.eom;
  }
  else if(symex_config.doing_path_exploration)
  {
    // We should save both the instruction after this goto, and the target of
    // the goto.
 
    path_storaget::patht next_instruction(target, state);
    next_instruction.state.saved_target = state_pc;
    next_instruction.state.has_saved_next_instruction = true;
 
    path_storaget::patht jump_target(target, state);
    jump_target.state.saved_target = new_state_pc;
    jump_target.state.has_saved_jump_target = true;
    // `forward` tells us where the branch we're _currently_ executing is
    // pointing to; this needs to be inverted for the branch that we're saving,
    // so let its truth value for `backwards` be the same as ours for `forward`.
 
    log.debug() << "Saving next instruction '"
                << next_instruction.state.saved_target->source_location() << "'"
                << log.eom;
    log.debug() << "Saving jump target '"
                << jump_target.state.saved_target->source_location() << "'"
                << log.eom;
    path_storage.push(next_instruction);
    path_storage.push(jump_target);
 
    // It is now up to the caller of symex to decide which path to continue
    // executing. Signal to the caller that states have been pushed (therefore
    // symex has not yet completed and must be resumed), and bail out.
    should_pause_symex = true;
    return;
  }
 
  // put a copy of the current state into the state-queue, to be used by
  // merge_gotos when we visit new_state_pc
  framet::goto_state_listt &goto_state_list =
    state.call_stack().top().goto_state_map[new_state_pc];
 
  // On an unconditional GOTO we don't need our state, as it will be overwritten
  // by merge_goto. Therefore we move it onto goto_state_list instead of copying
  // as usual.
  if(new_guard == true)
  {
    // The move here only moves goto_statet, the base class of goto_symex_statet
    // and not the entire thing.
    goto_state_list.emplace_back(state.source, std::move(state));
 
    symex_transition(state, state_pc, backward);
 
    state.guard = guardt(false_exprt(), guard_manager);
    state.reachable = false;
  }
  else
  {
    goto_state_list.emplace_back(state.source, state);
 
    symex_transition(state, state_pc, backward);
 
    if(!symex_config.doing_path_exploration)
    {
      // This doesn't work for --paths (single-path mode) yet, as in multi-path
      // mode we remove the implied constants at a control-flow merge, but in
      // single-path mode we don't run merge_gotos.
      auto &taken_state = backward ? state : goto_state_list.back().second;
      auto &not_taken_state = backward ? goto_state_list.back().second : state;
 
      apply_goto_condition(
        state,
        taken_state,
        not_taken_state,
        instruction.condition(),
        new_guard,
        ns);
    }
 
    // produce new guard symbol
    exprt guard_expr;
 
    if(
      new_guard.id() == ID_symbol ||
      (new_guard.id() == ID_not &&
       to_not_expr(new_guard).op().id() == ID_symbol))
    {
      guard_expr=new_guard;
    }
    else
    {
      symbol_exprt guard_symbol_expr =
        symbol_exprt(statet::guard_identifier(), bool_typet());
      exprt new_rhs = boolean_negate(new_guard);
 
      ssa_exprt new_lhs =
        state.rename_ssa<L1>(ssa_exprt{guard_symbol_expr}, ns).get();
      new_lhs =
        state.assignment(std::move(new_lhs), new_rhs, ns, true, false).get();
 
      guardt guard{true_exprt{}, guard_manager};
 
      log.conditional_output(
        log.debug(),
        [this, &new_lhs](messaget::mstreamt &mstream)
        {
          mstream << "Assignment to " << new_lhs.identifier() << " ["
                  << pointer_offset_bits(new_lhs.type(), ns).value_or(0)
                  << " bits]" << messaget::eom;
        });
 
      target.assignment(
        guard.as_expr(),
        new_lhs, new_lhs, guard_symbol_expr,
        new_rhs,
        original_source,
        symex_targett::assignment_typet::GUARD);
 
      guard_expr = state.rename(boolean_negate(guard_symbol_expr), ns).get();
    }
 
    if(state.has_saved_jump_target)
    {
      if(!backward)
        state.guard.add(guard_expr);
      else
        state.guard.add(boolean_negate(guard_expr));
    }
    else
    {
      goto_statet &new_state = goto_state_list.back().second;
      if(!backward)
      {
        new_state.guard.add(guard_expr);
        state.guard.add(boolean_negate(guard_expr));
      }
      else
      {
        state.guard.add(guard_expr);
        new_state.guard.add(boolean_negate(guard_expr));
      }
    }
  }
}
 
void goto_symext::symex_unreachable_goto(statet &state)
{
  PRECONDITION(!state.reachable);
  // This is like symex_goto, except the state is unreachable. We try to take
  // some arbitrary choice that maintains the state guard in a reasonable state
  // in order that it simplifies properly when states are merged (in
  // merge_gotos). Note we can't try to evaluate the actual GOTO guard because
  // our constant propagator might be out of date, since we haven't been
  // executing assign instructions.
 
  // If the guard is already false then there's no value in this state; just
  // carry on and check the next instruction.
  if(state.guard.is_false())
  {
    symex_transition(state);
    return;
  }
 
  const goto_programt::instructiont &instruction = *state.source.pc;
  PRECONDITION(instruction.is_goto());
  goto_programt::const_targett goto_target = instruction.get_target();
 
  auto queue_unreachable_state_at_target = [&]() {
    framet::goto_state_listt &goto_state_list =
      state.call_stack().top().goto_state_map[goto_target];
    goto_statet new_state(state.guard_manager);
    new_state.guard = state.guard;
    new_state.reachable = false;
    goto_state_list.emplace_back(state.source, std::move(new_state));
  };
 
  if(instruction.condition() == true)
  {
    if(instruction.is_backwards_goto())
    {
      // Give up trying to salvage the guard
      // (this state's guard is squashed, without queueing it at the target)
    }
    else
    {
      // Take the branch:
      queue_unreachable_state_at_target();
    }
 
    state.guard.add(false_exprt());
  }
  else
  {
    // Arbitrarily assume a conditional branch is not-taken, except for when
    // there's an incoming backedge, when we guess that the taken case is less
    // likely to lead to that backedge than the not-taken case.
    bool maybe_loop_head = std::any_of(
      instruction.incoming_edges.begin(),
      instruction.incoming_edges.end(),
      [&instruction](const goto_programt::const_targett predecessor) {
        return predecessor->location_number > instruction.location_number;
      });
 
    if(instruction.is_backwards_goto() || !maybe_loop_head)
    {
      // Assume branch not taken (fall through)
    }
    else
    {
      // Assume branch taken:
      queue_unreachable_state_at_target();
      state.guard.add(false_exprt());
    }
  }
 
  symex_transition(state);
}
 
bool goto_symext::check_break(const irep_idt &loop_id, unsigned unwind)
{
  // dummy implementation
  return false;
}
 
void goto_symext::merge_gotos(statet &state)
{
  framet &frame = state.call_stack().top();
 
  // first, see if this is a target at all
  auto state_map_it = frame.goto_state_map.find(state.source.pc);
 
  if(state_map_it==frame.goto_state_map.end())
    return; // nothing to do
 
  // we need to merge
  framet::goto_state_listt &state_list = state_map_it->second;
 
  for(auto list_it = state_list.rbegin(); list_it != state_list.rend();
      ++list_it)
  {
    merge_goto(list_it->first, std::move(list_it->second), state);
  }
 
  // clean up to save some memory
  frame.goto_state_map.erase(state_map_it);
}
 
static guardt
merge_state_guards(goto_statet &goto_state, goto_symex_statet &state)
{
  // adjust guard, even using guards from unreachable states. This helps to
  // shrink the state guard if the incoming edge is from a path that was
  // truncated by config.unwind, config.depth or an assume-false instruction.
 
  // Note when an unreachable state contributes its guard, merging it in is
  // optional, since the formula already implies the unreachable guard is
  // impossible. Therefore we only integrate it when to do so simplifies the
  // state guard.
 
  // This function can trash either state's guards, since goto_state is dying
  // and state's guard will shortly be overwritten.
 
  if(
    (goto_state.reachable && state.reachable) ||
    state.guard.disjunction_may_simplify(goto_state.guard))
  {
    state.guard |= goto_state.guard;
    return std::move(state.guard);
  }
  else if(!state.reachable && goto_state.reachable)
  {
    return std::move(goto_state.guard);
  }
  else
  {
    return std::move(state.guard);
  }
}
 
void goto_symext::merge_goto(
  const symex_targett::sourcet &,
  goto_statet &&goto_state,
  statet &state)
{
  // check atomic section
  if(state.atomic_section_id != goto_state.atomic_section_id)
    throw incorrect_goto_program_exceptiont(
      "atomic sections differ across branches",
      state.source.pc->source_location());
 
  // Merge guards. Don't write this to `state` yet because we might move
  // goto_state over it below.
  guardt new_guard = merge_state_guards(goto_state, state);
 
  // Merge constant propagator, value-set etc. only if the incoming state is
  // reachable:
  if(goto_state.reachable)
  {
    if(!state.reachable)
    {
      // Important to note that we're moving into our base class here.
      // Note this overwrites state.guard, but we restore it below.
      static_cast<goto_statet &>(state) = std::move(goto_state);
    }
    else
    {
      // do SSA phi functions
      phi_function(goto_state, state);
 
      // merge value sets
      state.value_set.make_union(goto_state.value_set);
 
      // adjust depth
      state.depth = std::min(state.depth, goto_state.depth);
    }
  }
 
  // Save the new state guard
  state.guard = std::move(new_guard);
}

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)
{
  const irep_idt l1_identifier = ssa.identifier();
  const irep_idt &obj_identifier = ssa.get_object_name();
 
  if(obj_identifier == goto_symext::statet::guard_identifier())
    return; // just a guard, don't bother
 
  if(goto_count == dest_count)
    return; // not at all changed
 
  // changed - but only on a branch that is now dead, and the other branch is
  // uninitialized/invalid
  if(
    (!dest_state.reachable && goto_count == 0) ||
    (!goto_state.reachable && dest_count == 0))
  {
    return;
  }
 
  // field sensitivity: only merge on individual fields
  if(dest_state.field_sensitivity.is_divisible(ssa, true))
    return;
 
  // shared variables are renamed on every access anyway, we don't need to
  // merge anything
  const symbolt &symbol = ns.lookup(obj_identifier);
 
  // shared?
  if(
    dest_state.atomic_section_id == 0 && dest_state.threads.size() >= 2 &&
    (symbol.is_shared() || dirty(symbol.name)))
  {
    return; // no phi nodes for shared stuff
  }
 
  // don't merge (thread-)locals across different threads, which
  // may have been introduced by symex_start_thread (and will
  // only later be removed from level2.current_names by pop_frame
  // once the thread is executed)
  const irep_idt level_0 = ssa.get_level_0();
  if(
    !level_0.empty() &&
    level_0 != std::to_string(dest_state.source.thread_nr) && dest_count != 0)
  {
    return;
  }
 
  exprt goto_state_rhs = ssa, dest_state_rhs = ssa;
 
  {
    const auto p_it = goto_state.propagation.find(l1_identifier);
 
    if(p_it.has_value())
      goto_state_rhs = *p_it;
    else
      to_ssa_expr(goto_state_rhs).set_level_2(goto_count);
  }
 
  {
    const auto p_it = dest_state.propagation.find(l1_identifier);
 
    if(p_it.has_value())
      dest_state_rhs = *p_it;
    else
      to_ssa_expr(dest_state_rhs).set_level_2(dest_count);
  }
 
  exprt rhs;
 
  // Don't add a conditional to the assignment when:
  //  1. Either guard is false, so we can't follow that branch.
  //  2. Either identifier is of generation zero, and so hasn't been
  //     initialized and therefore an invalid target.
 
  // These rules only apply to dynamic objects and locals.
  if(!dest_state.reachable)
    rhs = goto_state_rhs;
  else if(!goto_state.reachable)
    rhs = dest_state_rhs;
  else if(goto_count == 0)
    rhs = dest_state_rhs;
  else if(dest_count == 0)
    rhs = goto_state_rhs;
  else
  {
    rhs = if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);
    if(do_simplify)
    {
      // Do not value-set supported filtering here as neither dest_state nor
      // goto_state necessarily have a comprehensive value set.
      simplify(rhs, ns);
    }
  }
 
  dest_state.record_events.push(false);
  const ssa_exprt new_lhs =
    dest_state.assignment(ssa, rhs, ns, true, true).get();
  dest_state.record_events.pop();
 
  log.conditional_output(
    log.debug(),
    [ns, &new_lhs](messaget::mstreamt &mstream)
    {
      mstream << "Assignment to " << new_lhs.identifier() << " ["
              << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]"
              << messaget::eom;
    });
 
  target.assignment(
    true_exprt(),
    new_lhs,
    new_lhs,
    new_lhs.get_original_expr(),
    rhs,
    dest_state.source,
    symex_targett::assignment_typet::PHI);
}
 
void goto_symext::phi_function(
  const goto_statet &goto_state,
  statet &dest_state)
{
  if(
    goto_state.get_level2().current_names.empty() &&
    dest_state.get_level2().current_names.empty())
    return;
 
  guardt diff_guard = goto_state.guard;
  // this gets the diff between the guards
  diff_guard -= dest_state.guard;
 
  symex_renaming_levelt::delta_viewt delta_view;
  goto_state.get_level2().current_names.get_delta_view(
    dest_state.get_level2().current_names, delta_view, false);
 
  std::map<std::string, symex_renaming_levelt::delta_viewt::const_iterator>
    ordered_names_to_merge;
  for(auto it = delta_view.begin(); it != delta_view.end(); ++it)
  {
    const ssa_exprt &ssa = it->m.first;
    bool inserted =
      ordered_names_to_merge.insert({id2string(ssa.get_identifier()), it})
        .second;
    CHECK_RETURN(inserted);
  }
 
  for(const auto &ordered_entry : ordered_names_to_merge)
  {
    const auto &delta_item = *ordered_entry.second;
    const ssa_exprt &ssa = delta_item.m.first;
    std::size_t goto_count = delta_item.m.second;
    std::size_t dest_count = !delta_item.is_in_both_maps()
                               ? 0
                               : delta_item.get_other_map_value().second;
 
    merge_names(
      goto_state,
      dest_state,
      ns,
      diff_guard,
      log,
      symex_config.simplify_opt,
      target,
      path_storage.dirty,
      ssa,
      goto_count,
      dest_count);
  }
 
  delta_view.clear();
  dest_state.get_level2().current_names.get_delta_view(
    goto_state.get_level2().current_names, delta_view, false);
 
  ordered_names_to_merge.clear();
  for(auto it = delta_view.begin(); it != delta_view.end(); ++it)
  {
    if(it->is_in_both_maps())
      continue;
 
    const ssa_exprt &ssa = it->m.first;
    bool inserted =
      ordered_names_to_merge.insert({id2string(ssa.get_identifier()), it})
        .second;
    CHECK_RETURN(inserted);
  }
 
  for(const auto &ordered_entry : ordered_names_to_merge)
  {
    const auto &delta_item = *ordered_entry.second;
    const ssa_exprt &ssa = delta_item.m.first;
    std::size_t goto_count = 0;
    std::size_t dest_count = delta_item.m.second;
 
    merge_names(
      goto_state,
      dest_state,
      ns,
      diff_guard,
      log,
      symex_config.simplify_opt,
      target,
      path_storage.dirty,
      ssa,
      goto_count,
      dest_count);
  }
}
 
void goto_symext::loop_bound_exceeded(
  statet &state,
  const exprt &guard)
{
  const std::string loop_number = std::to_string(state.source.pc->loop_number);
 
  exprt negated_cond = boolean_negate(guard);
 
  if(symex_config.unwinding_assertions)
  {
    // Generate VCC for unwinding assertion.
    const std::string property_id =
      id2string(state.source.pc->source_location().get_function()) +
      ".unwind." + loop_number;
    vcc(
      negated_cond,
      property_id,
      "unwinding assertion loop " + loop_number,
      state);
  }
 
  if(!symex_config.partial_loops)
  {
    // generate unwinding assumption, unless we permit partial loops
    symex_assume_l2(state, negated_cond);
  }
}
 
bool goto_symext::should_stop_unwind(
  const symex_targett::sourcet &,
  const call_stackt &,
  unsigned)
{
  // by default, we keep going
  return false;
}