bool state_projectiont::is_new(const statet &state, bool use_cache)
{
  // get the right map
  assert(!state.data().previous.is_null());
  
  state_listt &state_list=
    state_map[state.data().previous_PC];

  // first try syntactically
  
  for(state_listt::const_iterator
      it=state_list.begin();
      it!=state_list.end();
      it++)
    if(is_syntactically_equal(*it, state))
      return false; // not new
      
  // now try expensive comparison

  for(state_listt::const_iterator
      it=state_list.begin();
      it!=state_list.end();
      it++)
    if(is_equal(*it, state, use_cache))
    {
      // put into list anyways
      state_list.push_back(state);
      return false; // not new
    }

  // not found, it's new  
  state_list.push_back(state);
  
  return true;
}

bool path_searcht::drop_state(const statet &state) const
{
  // depth
  if(depth_limit!=-1 && state.get_depth()>depth_limit) return true;
  
  // context bound
  if(context_bound!=-1 && state.get_no_thread_interleavings()) return true;
  
  // unwinding limit -- loops
  if(unwind_limit!=-1 && state.get_instruction()->is_backwards_goto())
  {
    for(path_symex_statet::unwinding_mapt::const_iterator
        it=state.unwinding_map.begin();
        it!=state.unwinding_map.end();
        it++)
      if(it->second>unwind_limit)
        return true;
  }
  
  // unwinding limit -- recursion
  if(unwind_limit!=-1 && state.get_instruction()->is_function_call())
  {
    for(path_symex_statet::recursion_mapt::const_iterator
        it=state.recursion_map.begin();
        it!=state.recursion_map.end();
        it++)
      if(it->second>unwind_limit)
        return true;
  }
  
  return false;
}

void simulator_ctt::compute_goto_successors(
  const statet &state,
  queuet &queue)
{
  const instructiont &instruction=*state.data().threads.front().PC;
  unsigned count=0;

  // must have target
  assert(!instruction.targets.empty());

  formulat instantiated_guard=
    instantiate(state, 0, instruction.guard);

  formulat new_guard_taken;

  if(instantiated_guard.is_true())
    new_guard_taken=state.data().guard;
  else
  {
    new_guard_taken=formula_container.gen_and(
      instantiated_guard,
      state.data().guard);

    formulat new_guard_not_taken=formula_container.gen_and(
      formula_container.gen_not(instantiated_guard),
      state.data().guard);

    // do "guard is false" case

    statet new_state=state;
    new_state.data_w().threads.front().PC++;
    new_state.data_w().guard=new_guard_not_taken;
    new_state.data_w().taken=false;
    new_state.set_previous(state, 0);
    queue.add(new_state);

    count++;
  }

  for(program_formulat::formula_goto_programt::
        instructiont::targetst::const_iterator
      t_it=instruction.targets.begin();
      t_it!=instruction.targets.end();
      t_it++)
  {
    statet new_state=state;
    new_state.data_w().threads.front().PC=*t_it;
    new_state.data_w().guard=new_guard_taken;
    new_state.data_w().taken=true;
    new_state.set_previous(state, 0);
    queue.add(new_state);

    count++;
  }
  
  if(count>=2) path_counter+=count-1;
}

void path_searcht::do_show_vcc(
  statet &state,
  const namespacet &ns)
{
  // keep statistics
  number_of_VCCs++;
  
  const goto_programt::instructiont &instruction=
    *state.get_instruction();
    
  mstreamt &out=result();

  if(instruction.location.is_not_nil())
    out << instruction.location << "\n";
  
  if(instruction.location.get_comment()!="")
    out << instruction.location.get_comment() << "\n";
    
  unsigned count=1;
  
  std::vector<path_symex_step_reft> steps;
  state.history.build_history(steps);

  for(std::vector<path_symex_step_reft>::const_iterator
      s_it=steps.begin();
      s_it!=steps.end();
      s_it++)
  {      
    if((*s_it)->guard.is_not_nil())
    {
      std::string string_value=from_expr(ns, "", (*s_it)->guard);
      out << "{-" << count << "} " << string_value << "\n";
      count++;
    }

    if((*s_it)->ssa_rhs.is_not_nil())
    {
      equal_exprt equality((*s_it)->ssa_lhs, (*s_it)->ssa_rhs);
      std::string string_value=from_expr(ns, "", equality);
      out << "{-" << count << "} " << string_value << "\n";
      count++;
    }
  }

  out << "|--------------------------" << "\n";
  
  exprt assertion=state.read(instruction.guard);

  out << "{" << 1 << "} "
      << from_expr(ns, "", assertion) << "\n";

  if(!assertion.is_true())
    number_of_VCCs_after_simplification++;
  
  out << eom;
}

void simulatort::explore(
  const statet &state,
  queuet &queue)
{
  #ifdef DEBUG
  std::cout << "simulatort::explore1\n";
  #endif

  #if 0
  std::cout << "/////////////////////////////////////////////// "
            << "\n";

  for(unsigned thread=0; thread<program_formula.threads.size(); thread++)
  {
    std::cout << "Thread " << thread << " Location: ";
    if(state.data().PCs[thread]==
       program_formula.threads[thread].formula_goto_program.instructions.end())
      std::cout << "END" << std::endl;
    else
    {
      instructiont &instruction=*state.data().PCs[thread];
      std::cout << location_string(instruction.location) << std::endl;
    }
  }
  std::cout << std::endl;
  #endif

  // dump it if the guard is false
  if(state.data().guard.is_false())
    return;
    
  #ifdef DEBUG
  std::cout << "simulatort::explore2\n";
  #endif
  
  if(history.check_history(
    state, enable_qbf_cache, enable_small_history))
  {
    // we have seen it already
    #ifdef DEBUG
    std::cout << ">>>>>>>>>>>>>>>>>>>>>>>> SEEN ALREADY\n";
    #endif
    return;
  }
  
  #ifdef DEBUG
  std::cout << "simulatort::explore3\n";
  #endif
  
  compute_successor_states(state, true, queue);
  
  #ifdef DEBUG
  std::cout << "simulatort::explore4\n";
  #endif
}

void simulator_ctt::execute_assume(
  statet &state,
  const program_formulat::formula_goto_programt::instructiont &instruction)
{
  formulat condition=
    instantiate(state, 0, instruction.guard);
    
  if(condition.is_true()) return;

  // just add it to the guard
  state.data_w().guard=
    formula_container.gen_and(state.data_w().guard, condition);
}

void path_searcht::do_show_vcc(statet &state)
{
  // keep statistics
  number_of_VCCs++;

  const goto_programt::instructiont &instruction=
    *state.get_instruction();

  mstreamt &out=result();

  if(instruction.source_location.is_not_nil())
    out << instruction.source_location << '\n';

  if(instruction.source_location.get_comment()!="")
    out << instruction.source_location.get_comment() << '\n';

  unsigned count=1;

  std::vector<path_symex_step_reft> steps;
  state.history.build_history(steps);

  for(const auto &step_ref : steps)
  {
    if(step_ref->guard.is_not_nil())
    {
      std::string string_value=from_expr(ns, "", step_ref->guard);
      out << "{-" << count << "} " << string_value << '\n';
      count++;
    }

    if(step_ref->ssa_rhs.is_not_nil())
    {
      equal_exprt equality(step_ref->ssa_lhs, step_ref->ssa_rhs);
      std::string string_value=from_expr(ns, "", equality);
      out << "{-" << count << "} " << string_value << '\n';
      count++;
    }
  }

  out << "|--------------------------" << '\n';

  exprt assertion=state.read(instruction.guard);

  out << "{" << 1 << "} "
      << from_expr(ns, "", assertion) << '\n';

  if(!assertion.is_true())
    number_of_VCCs_after_simplification++;

  out << eom;
}

void goto_symext::symex_dead(statet &state)
{
    const goto_programt::instructiont &instruction=*state.source.pc;

    const codet &code=to_code(instruction.code);

    if(code.operands().size()!=1)
        throw "dead expects one operand";

    if(code.op0().id()!=ID_symbol)
        throw "dead expects symbol as first operand";

    // We increase the L2 renaming to make these non-deterministic.
    // We also prevent propagation of old values.

    ssa_exprt ssa(to_symbol_expr(code.op0()));
    state.rename(ssa, ns, goto_symex_statet::L1);

    // in case of pointers, put something into the value set
    if(ns.follow(code.op0().type()).id()==ID_pointer)
    {
        exprt failed=
            get_failed_symbol(to_symbol_expr(code.op0()), ns);

        exprt rhs;

        if(failed.is_not_nil())
        {
            address_of_exprt address_of_expr;
            address_of_expr.object()=failed;
            address_of_expr.type()=code.op0().type();
            rhs=address_of_expr;
        }
        else
            rhs=exprt(ID_invalid);

        state.rename(rhs, ns, goto_symex_statet::L1);
        state.value_set.assign(ssa, rhs, ns, true, false);
    }

    ssa_exprt ssa_lhs=to_ssa_expr(ssa);
    const irep_idt &l1_identifier=ssa_lhs.get_identifier();

    // prevent propagation
    state.propagation.remove(l1_identifier);

    // L2 renaming
    if(state.level2.current_names.find(l1_identifier)!=
            state.level2.current_names.end())
        state.level2.increase_counter(l1_identifier);
}

void goto_symext::operator()(
  statet &state,
  const goto_functionst &goto_functions,
  const goto_programt &goto_program)
{
  assert(!goto_program.instructions.empty());

  state.source=symex_targett::sourcet(goto_program);
  assert(!state.threads.empty());
  assert(!state.call_stack().empty());
  state.top().end_of_function=--goto_program.instructions.end();
  state.top().calling_location.pc=state.top().end_of_function;
  state.symex_target=⌖
  state.dirty=new dirtyt(goto_functions);

  assert(state.top().end_of_function->is_end_function());

  while(!state.call_stack().empty())
  {
    symex_step(goto_functions, state);

    // is there another thread to execute?
    if(state.call_stack().empty() &&
       state.source.thread_nr+1<state.threads.size())
    {
      unsigned t=state.source.thread_nr+1;
      // std::cout << "********* Now executing thread " << t << std::endl;
      state.switch_to_thread(t);
    }
  }

  delete state.dirty;
  state.dirty=0;
}

void goto_symext::vcc(
  const exprt &vcc_expr,
  const std::string &msg,
  statet &state)
{
  total_vccs++;

  exprt expr=vcc_expr;

  // we are willing to re-write some quantified expressions
  rewrite_quantifiers(expr, state);

  // now rename, enables propagation
  state.rename(expr, ns);

  // now try simplifier on it
  do_simplify(expr);

  if(expr.is_true())
    return;

  state.guard.guard_expr(expr);

  remaining_vccs++;
  target.assertion(state.guard.as_expr(), expr, msg, state.source);
}

void path_searcht::check_assertion(
  statet &state,
  const namespacet &ns)
{
  // keep statistics
  number_of_VCCs++;
  
  const goto_programt::instructiont &instruction=
    *state.get_instruction();

  irep_idt property_name=instruction.location.get_property_id();
  property_entryt &property_entry=property_map[property_name];
  
  if(property_entry.status==FAIL)
    return; // already failed
  else if(property_entry.status==NOT_REACHED)
    property_entry.status=PASS; // well, for now!

  // the assertion in SSA
  exprt assertion=
    state.read(instruction.guard);

  if(assertion.is_true()) return; // no error, trivially

  // keep statistics
  number_of_VCCs_after_simplification++;
  
  status() << "Checking property " << property_name << eom;

  // take the time
  absolute_timet sat_start_time=current_time();

  satcheckt satcheck;
  bv_pointerst bv_pointers(ns, satcheck);
  
  satcheck.set_message_handler(get_message_handler());
  bv_pointers.set_message_handler(get_message_handler());

  if(!state.check_assertion(bv_pointers))
  {
    build_goto_trace(state, bv_pointers, property_entry.error_trace);
    property_entry.status=FAIL;
    number_of_failed_properties++;
  }
  
  sat_time+=current_time()-sat_start_time;
}

void goto_symext::dereference(
  exprt &expr,
  statet &state,
  const bool write)
{
  // The expression needs to be renamed to level 1
  // in order to distinguish addresses of local variables
  // from different frames. Would be enough to rename
  // symbols whose address is taken.
  assert(!state.call_stack().empty());
  state.rename(expr, ns, goto_symex_statet::L1);

  // start the recursion!
  guardt guard;
  dereference_rec(expr, state, guard, write);
  // dereferencing may introduce new symbol_exprt
  // (like __CPROVER_memory)
  state.rename(expr, ns, goto_symex_statet::L1);
}

void shared_accesst::rw_sets(
				statet& state,
				std::vector<bool>& is_shared,
				std::vector<sharedt::sett>& reads, 
				std::vector<sharedt::sett>& writes)
{
  
  unsigned nr_threads=state.threads.size();
  
  reads.clear();
  reads.resize(nr_threads);

  writes.clear();
  writes.resize(nr_threads);

  is_shared.clear();
  is_shared.resize(nr_threads, false);

  if(state.atomic_section_count)
  {
    return;
  }

  sharedt shared(state);

  unsigned current_thread=state.get_current_thread();

  for(unsigned 
      thr=0;
      thr<nr_threads;
      ++thr)
  {		
    if(state.threads[thr].active)
    {
      state.set_current_thread(thr);
      shared(reads[thr], writes[thr]);
      is_shared[thr]=!(reads[thr].empty() && writes[thr].empty());
    }                     
  }
  
  state.set_current_thread(current_thread);
}

bool state_projectiont::is_syntactically_equal(
  const statet &old_state,
  const statet &new_state)
{
  if(old_state.data().guard!=new_state.data().guard)
    return false;
  
  unsigned v=0;
  
  for(program_formulat::variablest::const_iterator
      it=program_formula.variables.begin();
      it!=program_formula.variables.end();
      it++, v++)
  {
    if(it->is_global)
    {
      assert(v<old_state.data().globals.size());
      assert(v<new_state.data().globals.size());

      if(old_state.data().globals[v]!=
         new_state.data().globals[v])
        return false;
    }
  }
  
  return true;  
}

void simulator_ctt::execute_assert(
  statet &state,
  const program_formulat::formula_goto_programt::instructiont &instruction)
{
  std::cout << "CHECKING ASSERTION\n";

  formulat condition=
    instantiate(state, 0, instruction.guard);
    
  formulat property=
    formula_container.gen_and(
      state.data().guard,
      formula_container.gen_not(condition));

  // see if it is reachable
  if(!property.is_false() &&
     is_satisfiable(property))
  {
    tracet trace;

    compute_trace(state, trace, true);
    dump_trace(trace, instruction);
    std::cout << "Assertion violated" << std::endl;
    std::cout << std::endl;

    error_state_found=true;
  }
  
  #if 0
  else
  {
    // otherwise, treat this like an assumption
    state.data_w().guard=
      formula_container.gen_and(state.data().guard, condition);
  }
  #endif
}

void simulator_ctt::execute_assign(
  statet &state,
  const program_formulat::formula_goto_programt::instructiont &instruction)
{
  statet new_state(state);
  
  new_state.detatch();

  for(program_formulat::assignst::const_iterator
      it=instruction.code.assigns.begin();
      it!=instruction.code.assigns.end();
      it++)
    if(it->in_use)
    {
      assert(it->variable<program_formula.variables.size());

      new_state.data_w().set_var(
        it->variable,
        0,
        instantiate(state, 0, it->value));
    }
  
  // do constraint
  formulat instantiated_constraint=
    instantiate(
      state,
      new_state,
      0,
      instruction.code.constraint);

  new_state.data_w().guard=
    formula_container.gen_and(
      state.data_w().guard,
      instantiated_constraint);
  
  state.swap(new_state);
}

/// decide whether to drop a state
bool path_searcht::drop_state(const statet &state)
{
  goto_programt::const_targett pc=state.get_instruction();

  // depth limit
  if(depth_limit_set && state.get_depth()>depth_limit)
    return true;

  // context bound
  if(context_bound_set && state.get_no_thread_interleavings()>context_bound)
    return true;

  // branch bound
  if(branch_bound_set && state.get_no_branches()>branch_bound)
    return true;

  // unwinding limit -- loops
  if(unwind_limit_set && state.get_instruction()->is_backwards_goto())
  {
    for(const auto &loop_info : state.unwinding_map)
      if(loop_info.second>unwind_limit)
        return true;
  }

  // unwinding limit -- recursion
  if(unwind_limit_set && state.get_instruction()->is_function_call())
  {
    for(const auto &rec_info : state.recursion_map)
      if(rec_info.second>unwind_limit)
        return true;
  }

  if(pc->is_assume() &&
     simplify_expr(pc->guard, ns).is_false())
  {
    debug() << "aborting path on assume(false) at "
            << pc->source_location
            << " thread " << state.get_current_thread();

    const irep_idt &c=pc->source_location.get_comment();
    if(!c.empty())
      debug() << ": " << c;

    debug() << eom;

    return true;
  }

  return false;
}

bool path_searcht::is_feasible(statet &state)
{
  status() << "Feasibility check" << eom;

  // take the time
  absolute_timet sat_start_time=current_time();

  satcheckt satcheck;
  bv_pointerst bv_pointers(ns, satcheck);
  
  satcheck.set_message_handler(get_message_handler());
  bv_pointers.set_message_handler(get_message_handler());

  bool result=state.is_feasible(bv_pointers);
  
  sat_time+=current_time()-sat_start_time;
  
  return result;
}

void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
{
  // We increase the L2 renaming to make these non-deterministic.
  // We also prevent propagation of old values.

  ssa_exprt ssa(expr);
  state.rename(ssa, ns, goto_symex_statet::L1);
  const irep_idt &l1_identifier=ssa.get_identifier();

  // rename type to L2
  state.rename(ssa.type(), l1_identifier, ns);
  ssa.update_type();

  // in case of pointers, put something into the value set
  if(ns.follow(expr.type()).id()==ID_pointer)
  {
    exprt failed=
      get_failed_symbol(expr, ns);

    exprt rhs;

    if(failed.is_not_nil())
    {
      address_of_exprt address_of_expr;
      address_of_expr.object()=failed;
      address_of_expr.type()=expr.type();
      rhs=address_of_expr;
    }
    else
      rhs=exprt(ID_invalid);

    state.rename(rhs, ns, goto_symex_statet::L1);
    state.value_set.assign(ssa, rhs, ns, true, false);
  }

  // prevent propagation
  state.propagation.remove(l1_identifier);

  // L2 renaming
  // inlining may yield multiple declarations of the same identifier
  // within the same L1 context
  if(state.level2.current_names.find(l1_identifier)==
     state.level2.current_names.end())
    state.level2.current_names[l1_identifier]=std::make_pair(ssa, 0);
  state.level2.increase_counter(l1_identifier);
  const bool record_events=state.record_events;
  state.record_events=false;
  state.rename(ssa, ns);
  state.record_events=record_events;

  // we hide the declaration of auxiliary variables
  // and if the statement itself is hidden
  bool hidden=
    ns.lookup(expr.get_identifier()).is_auxiliary ||
    state.top().hidden_function ||
    state.source.pc->source_location.get_hide();

  target.decl(
    state.guard.as_expr(),
    ssa,
    state.source,
    hidden?symex_targett::HIDDEN:symex_targett::STATE);

  assert(state.dirty);
  if((*state.dirty)(ssa.get_object_name()) &&
     state.atomic_section_id==0)
    target.shared_write(
      state.guard.as_expr(),
      ssa,
      state.atomic_section_id,
      state.source);
}

void goto_symext::symex_step(
  const goto_functionst &goto_functions,
  statet &state)
{
  #if 0
  std::cout << "\ninstruction type is " << state.source.pc->type << '\n';
  std::cout << "Location: " << state.source.pc->source_location << '\n';
  std::cout << "Guard: " << from_expr(ns, "", state.guard.as_expr()) << '\n';
  std::cout << "Code: " << from_expr(ns, "", state.source.pc->code) << '\n';
  #endif

  assert(!state.threads.empty());
  assert(!state.call_stack().empty());

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

  merge_gotos(state);

  // depth exceeded?
  {
    unsigned max_depth=options.get_unsigned_int_option("depth");
    if(max_depth!=0 && state.depth>max_depth)
      state.guard.add(false_exprt());
    state.depth++;
  }

  // actually do instruction
  switch(instruction.type)
  {
  case SKIP:
    if(!state.guard.is_false())
      target.location(state.guard.as_expr(), state.source);
    state.source.pc++;
    break;

  case END_FUNCTION:
    // do even if state.guard.is_false() to clear out frame created
    // in symex_start_thread
    symex_end_of_function(state);
    state.source.pc++;
    break;

  case LOCATION:
    if(!state.guard.is_false())
      target.location(state.guard.as_expr(), state.source);
    state.source.pc++;
    break;

  case GOTO:
    symex_goto(state);
    break;

  case ASSUME:
    if(!state.guard.is_false())
    {
      exprt tmp=instruction.guard;
      clean_expr(tmp, state, false);
      state.rename(tmp, ns);
      symex_assume(state, tmp);
    }

    state.source.pc++;
    break;

  case ASSERT:
    if(!state.guard.is_false())
    {
      std::string msg=id2string(state.source.pc->source_location.get_comment());
      if(msg=="")
        msg="assertion";
      exprt tmp(instruction.guard);
      clean_expr(tmp, state, false);
      vcc(tmp, msg, state);
    }

    state.source.pc++;
    break;

  case RETURN:
    if(!state.guard.is_false())
      return_assignment(state);

    state.source.pc++;
    break;

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

    state.source.pc++;
    break;

  case FUNCTION_CALL:
    if(!state.guard.is_false())
    {
      code_function_callt deref_code=
        to_code_function_call(instruction.code);

      if(deref_code.lhs().is_not_nil())
        clean_expr(deref_code.lhs(), state, true);
//.........这里部分代码省略.........