自学教程：C++ true_exprt函数代码示例

void local_SSAt::build_transfer(locationt loc){  if(loc->is_assign())  {    const code_assignt &code_assign=to_code_assign(loc->code);    exprt deref_lhs=dereference(code_assign.lhs(), loc);    exprt deref_rhs=dereference(code_assign.rhs(), loc);    assign_rec(deref_lhs, deref_rhs, true_exprt(), loc);  }  else if(loc->is_function_call())  {    const code_function_callt &code_function_call=      to_code_function_call(loc->code);          const exprt &lhs=code_function_call.lhs();          if(lhs.is_not_nil())    {      exprt deref_lhs=dereference(lhs, loc);          // generate a symbol for rhs      irep_idt identifier="ssa::return_value"+i2string(loc->location_number);      symbol_exprt rhs(identifier, code_function_call.lhs().type());            assign_rec(deref_lhs, rhs, true_exprt(), loc);    }  }}

/// //_all_rows ( pre_guard==> (row_value=> row_expr) )exprt predabs_domaint::to_pre_constraints(valuet &_value){  assert(*e_it<templ.size());  const template_rowt &templ_row=templ[*e_it];  kindt k=templ_row.kind;  if(k==OUT || k==OUTL)    return true_exprt();  return implies_exprt(true_exprt(), templ[*e_it].expr);}

exprt interval_domaint::make_expression(const symbol_exprt &src) const{  if(is_int(src.type()))  {    int_mapt::const_iterator i_it=int_map.find(src.get_identifier());    if(i_it==int_map.end()) return true_exprt();    const integer_intervalt &interval=i_it->second;    if(interval.is_top()) return true_exprt();    if(interval.is_bottom()) return false_exprt();    exprt::operandst conjuncts;    if(interval.upper_set)     {      exprt tmp=from_integer(interval.upper, src.type());      conjuncts.push_back(binary_relation_exprt(src, ID_le, tmp));    }    if(interval.lower_set)     {      exprt tmp=from_integer(interval.lower, src.type());      conjuncts.push_back(binary_relation_exprt(tmp, ID_le, src));    }      return conjunction(conjuncts);  }  else if(is_float(src.type()))  {    float_mapt::const_iterator i_it=float_map.find(src.get_identifier());    if(i_it==float_map.end()) return true_exprt();    const ieee_float_intervalt &interval=i_it->second;    if(interval.is_top()) return true_exprt();    if(interval.is_bottom()) return false_exprt();    exprt::operandst conjuncts;    if(interval.upper_set)     {      exprt tmp=interval.upper.to_expr();      conjuncts.push_back(binary_relation_exprt(src, ID_le, tmp));    }    if(interval.lower_set)     {      exprt tmp=interval.lower.to_expr();      conjuncts.push_back(binary_relation_exprt(tmp, ID_le, src));    }      return conjunction(conjuncts);  }  else    return true_exprt();}

void all_paths_enumeratort::extend_path(patht &path,    goto_programt::targett t,    int succ) {  goto_programt::targett next;  goto_programt::targetst succs;  exprt guard = true_exprt();  goto_program.get_successors(t, succs);  for (goto_programt::targetst::iterator it = succs.begin();       it != succs.end();       ++it) {    if (succ == 0) {      next = *it;      break;    }    succ--;  }  if (t->is_goto()) {    guard = not_exprt(t->guard);    for (goto_programt::targetst::iterator it = t->targets.begin();         it != t->targets.end();         ++it) {      if (next == *it) {        guard = t->guard;        break;      }    }  }  path.push_back(path_nodet(next, guard));}

exprt functionst::arguments_equal(const exprt::operandst &o1,                                  const exprt::operandst &o2){  assert(o1.size()==o2.size());  if(o1.empty())    return true_exprt();  and_exprt and_expr;  and_exprt::operandst &conjuncts=and_expr.operands();  conjuncts.resize(o1.size());  for(std::size_t i=0; i<o1.size(); i++)  {    exprt lhs=o1[i];    exprt rhs=o2[i];    if(lhs.type()!=rhs.type())      rhs.make_typecast(lhs.type());    conjuncts[i]=equal_exprt(lhs, rhs);  }  return and_expr;}

/* * Insert a looping path (usually an accelerator) into a goto-program, * beginning at loop_header and jumping back to loop_header via back_jump. * Stores the locations at which the looping path was added in inserted_path. * * THIS DESTROYS looping_path!! */void acceleratet::insert_looping_path(  goto_programt::targett &loop_header,  goto_programt::targett &back_jump,  goto_programt &looping_path,  patht &inserted_path){  goto_programt::targett loop_body=loop_header;  ++loop_body;  goto_programt::targett jump=program.insert_before(loop_body);  jump->make_goto();  jump->guard=side_effect_expr_nondett(bool_typet());  jump->targets.push_back(loop_body);  program.destructive_insert(loop_body, looping_path);  jump=program.insert_before(loop_body);  jump->make_goto();  jump->guard=true_exprt();  jump->targets.push_back(back_jump);  for(goto_programt::targett t=loop_header;      t!=loop_body;      ++t)  {    inserted_path.push_back(path_nodet(t));  }  inserted_path.push_back(path_nodet(back_jump));}

void acceleratet::set_dirty_vars(path_acceleratort &accelerator){  for(std::set<exprt>::iterator it=accelerator.dirty_vars.begin();      it!=accelerator.dirty_vars.end();      ++it)  {    expr_mapt::iterator jt=dirty_vars_map.find(*it);    exprt dirty_var;    if(jt==dirty_vars_map.end())    {      scratch_programt scratch(symbol_table);      symbolt new_sym=utils.fresh_symbol("accelerate::dirty", bool_typet());      dirty_var=new_sym.symbol_expr();      dirty_vars_map[*it]=dirty_var;    }    else    {      dirty_var=jt->second;    }#ifdef DEBUG    std::cout << "Setting dirty flag " << expr2c(dirty_var, ns)      << " for " << expr2c(*it, ns) << '/n';#endif    accelerator.pure_accelerator.add_instruction(ASSIGN)->code =      code_assignt(dirty_var, true_exprt());  }}

void equality_domaint::make_not_post_constraints(  valuet &_value,  exprt::operandst &cond_exprs){  assert(*e_it<templ.size());  cond_exprs.resize(1);  if(check_dis)  {    cond_exprs[0]=get_post_not_disequ_constraint(*e_it);    return;  }  const template_rowt &templ_row=templ[*e_it];  if(templ_row.kind==IN)  {    cond_exprs[0]=true_exprt();    return;  }  const var_pairt &vv=templ_row.var_pair;  exprt c=    and_exprt(      templ_row.aux_expr,      not_exprt(        implies_exprt(          templ_row.post_guard,          equal_exprt(vv.first, vv.second))));  rename(c);  cond_exprs[0]=c;}

void summarizer_fwt::inline_summaries(const function_namet &function_name, 				   local_SSAt &SSA, const exprt &precondition,				   bool context_sensitive){  for(local_SSAt::nodest::const_iterator n_it = SSA.nodes.begin();      n_it != SSA.nodes.end(); n_it++)  {    for(local_SSAt::nodet::function_callst::const_iterator f_it = 	  n_it->function_calls.begin();        f_it != n_it->function_calls.end(); f_it++)    {      assert(f_it->function().id()==ID_symbol); //no function pointers      if(!check_call_reachable(function_name,SSA,n_it,f_it,precondition,true))       {	continue;      }      if(!check_precondition(function_name,SSA,n_it,f_it,			     precondition,context_sensitive))      {	exprt precondition_call = true_exprt();	if(context_sensitive) 	  precondition_call = compute_calling_context(	    function_name,SSA,n_it,f_it,precondition,true);	irep_idt fname = to_symbol_expr(f_it->function()).get_identifier();	status() << "Recursively summarizing function " << fname << eom;	compute_summary_rec(fname,precondition_call,context_sensitive);	summaries_used++;      }    }  }}

const exprt predabs_domaint::initialize_solver(  const local_SSAt &SSA,  const exprt &precondition,  template_generator_baset &template_generator){  get_row_set(todo_preds);  return true_exprt();}

const exprt equality_domaint::initialize_solver(  const local_SSAt &SSA,  const exprt &precondition,  template_generator_baset &template_generator){  get_index_set(todo_equs);  return true_exprt();}

exprt equality_domaint::to_pre_constraints(valuet &_value){  if(check_dis)    return get_pre_disequ_constraint(*e_it);  assert(*e_it<templ.size());  const template_rowt &templ_row=templ[*e_it];  if(templ_row.kind==OUT || templ_row.kind==OUTL)    return true_exprt();  const var_pairt &vv=templ_row.var_pair;  return implies_exprt(templ_row.pre_guard, equal_exprt(vv.first, vv.second));}

void summarizer_fw_termt::inline_summaries(  const function_namet &function_name,  local_SSAt &SSA, exprt precondition,  bool context_sensitive,  threevalt &calls_terminate,  bool &has_function_calls){  for(local_SSAt::nodest::iterator n_it=SSA.nodes.begin();      n_it!=SSA.nodes.end(); n_it++)  {    for(local_SSAt::nodet::function_callst::iterator f_it=          n_it->function_calls.begin();        f_it!=n_it->function_calls.end(); f_it++)    {      assert(f_it->function().id()==ID_symbol); // no function pointers      exprt::operandst c;      c.push_back(precondition);      get_assertions(SSA, c); // assertions as assumptions      precondition=conjunction(c);      if(!options.get_bool_option("competition-mode") &&         !check_call_reachable(           function_name, SSA, n_it, f_it, precondition, true))        continue;      has_function_calls=true;      irep_idt fname=to_symbol_expr(f_it->function()).get_identifier();      if(!check_precondition(           function_name, SSA, n_it, f_it, precondition, context_sensitive))      {        exprt precondition_call=true_exprt();        if(context_sensitive)          precondition_call=compute_calling_context(            function_name, SSA, n_it, f_it, precondition, true);        status() << "Recursively summarizing function " << fname << eom;        compute_summary_rec(fname, precondition_call, context_sensitive);        summaries_used++;      }      // get information about callee termination      if(summary_db.exists(fname) && summary_db.get(fname).terminates!=YES)      {        // cannot propagate NO        // because call reachability might be over-approximating        calls_terminate=UNKNOWN;        break;      }    }  }}

exprt ranking_synthesis_seneschalt::instantiate(void){  exprt path = body.body_relation;  if(!write_input_file(path))    return nil_exprt();  // make sure nothing is saved  rank_relation = false_exprt();  return true_exprt();}

exprt conjunction(const exprt::operandst &op){  if(op.empty())    return true_exprt();  else if(op.size()==1)    return op.front();  else  {    and_exprt result;    result.operands()=op;    return result;  }}

void summarizer_bwt::summarize(const function_namet &function_name){  status() << "/nBackward analysis..." << eom;  exprt postcondition = true_exprt(); //initial calling context  status() << "/nSummarizing function " << function_name << eom;  if(summary_db.exists(function_name))   {    compute_summary_rec(function_name,postcondition,true);  }  else status() << "Skipping function " << function_name << eom;}

void summarizer_fwt::compute_summary_rec(const function_namet &function_name,				      const exprt &precondition,				      bool context_sensitive){  local_SSAt &SSA = ssa_db.get(function_name); //TODO: make const    // recursively compute summaries for function calls  inline_summaries(function_name,SSA,precondition,context_sensitive);   status() << "Analyzing function "  << function_name << eom;#if 0  {    std::ostringstream out;    out << "Function body for " << function_name <<       " to be analyzed: " << std::endl;    for(local_SSAt::nodest::iterator n = SSA.nodes.begin();         n!=SSA.nodes.end(); n++)    {      if(!n->empty()) n->output(out,SSA.ns);    }    out << "(enable) " << from_expr(SSA.ns, "", SSA.get_enabling_exprs()) 	<< "/n";    debug() << out.str() << eom;  }#endif  // create summary  summaryt summary;  summary.params = SSA.params;  summary.globals_in = SSA.globals_in;  summary.globals_out = SSA.globals_out;  summary.fw_precondition = precondition;  if(!options.get_bool_option("havoc"))  {    do_summary(function_name,SSA,summary,true_exprt(),context_sensitive);  }  if(!options.get_bool_option("competition-mode"))  {    std::ostringstream out;    out << std::endl << "Summary for function " << function_name << std::endl;    summary.output(out,SSA.ns);       status() << out.str() << eom;  }  // store summary in db  summary_db.put(function_name,summary);}

void heap_tpolyhedra_domaint::project_on_vars(  domaint::valuet &value,  const domaint::var_sett &vars,  exprt &result){  heap_tpolyhedra_valuet &v=static_cast<heap_tpolyhedra_valuet &>(value);  exprt heap_result;  heap_domain.project_on_vars(v.heap_value, vars, heap_result);  exprt tpolyhedra_result;  polyhedra_domain.project_on_vars(v.tpolyhedra_value, vars, tpolyhedra_result);  result=heap_result;  if(tpolyhedra_result!=true_exprt())    result=and_exprt(result, tpolyhedra_result);}

exprt flow_insensitive_abstract_domain_baset::get_guard(  locationt from,  locationt to) const{  if(!from->is_goto())    return true_exprt();  locationt next=from;  next++;  if(next==to)  {    exprt tmp(from->guard);    tmp.make_not();    return tmp;  }  return from->guard;}

exprt equality_domaint::make_permanent(valuet &value){  equality_domaint::equ_valuet &inv=    static_cast<equality_domaint::equ_valuet &>(value);  if(unsatisfiable)  {    if(!check_dis)    {      set_equal(*e_it, inv);      // due to transitivity, we have to recheck equalities      //   that did not hold      todo_equs.insert(todo_disequs.begin(), todo_disequs.end());      todo_disequs.clear();    }    return to_pre_constraints(value);  }  return true_exprt();}

exprt guardt::as_expr(guard_listt::const_iterator it) const{  if(it==guard_list.end())    return true_exprt();  else if(it==--guard_list.end())    return guard_list.back();  exprt dest;  dest=exprt(ID_and, typet(ID_bool));  dest.reserve_operands(guard_list.size());  for(; it!=guard_list.end(); it++)  {    if(!it->is_boolean())      throw "guard is expected to be Boolean";    dest.copy_to_operands(*it);  }  return dest;}