From f3de4b34f8866efb6ca416cdcd189e9e26250fe4 Mon Sep 17 00:00:00 2001 From: Sarbojit Das Date: Thu, 13 Sep 2018 13:36:17 +0530 Subject: [PATCH 1/7] modified: src/2ls/2ls_parse_options.cpp modified: src/2ls/2ls_parse_options.h modified: src/2ls/Makefile modified: src/2ls/summary_checker_base.cpp modified: src/2ls/summary_checker_base.h new file: src/2ls/summary_checker_rect.cpp new file: src/2ls/summary_checker_rect.h modified: src/domains/Makefile modified: src/domains/domain.h modified: src/domains/ssa_analyzer.cpp modified: src/domains/ssa_analyzer.h modified: src/domains/strategy_solver_base.h modified: src/domains/strategy_solver_binsearch.h new file: src/domains/template_gen_rec_summary.cpp new file: src/domains/template_gen_rec_summary.h modified: src/domains/template_generator_base.cpp modified: src/domains/template_generator_base.h modified: src/domains/tpolyhedra_domain.cpp modified: src/domains/tpolyhedra_domain.h modified: src/solver/Makefile modified: src/solver/summarizer_fw.cpp modified: src/solver/summarizer_fw.h new file: src/solver/summarizer_rec_fw.cpp new file: src/solver/summarizer_rec_fw.h --- src/2ls/2ls_parse_options.cpp | 24 +- src/2ls/2ls_parse_options.h | 2 +- src/2ls/Makefile | 1 + src/2ls/summary_checker_base.cpp | 560 +++++++++++++++++++++++ src/2ls/summary_checker_base.h | 2 +- src/2ls/summary_checker_rect.cpp | 108 +++++ src/2ls/summary_checker_rect.h | 28 ++ src/domains/Makefile | 1 + src/domains/domain.h | 4 + src/domains/ssa_analyzer.cpp | 24 +- src/domains/ssa_analyzer.h | 9 +- src/domains/strategy_solver_base.h | 2 + src/domains/strategy_solver_binsearch.h | 2 + src/domains/template_gen_rec_summary.cpp | 69 +++ src/domains/template_gen_rec_summary.h | 39 ++ src/domains/template_generator_base.cpp | 6 +- src/domains/template_generator_base.h | 2 +- src/domains/tpolyhedra_domain.cpp | 32 +- src/domains/tpolyhedra_domain.h | 6 +- src/solver/Makefile | 1 + src/solver/summarizer_fw.cpp | 5 +- src/solver/summarizer_fw.h | 2 +- src/solver/summarizer_rec_fw.cpp | 202 ++++++++ src/solver/summarizer_rec_fw.h | 51 +++ 24 files changed, 1162 insertions(+), 20 deletions(-) create mode 100644 src/2ls/summary_checker_rect.cpp create mode 100644 src/2ls/summary_checker_rect.h create mode 100644 src/domains/template_gen_rec_summary.cpp create mode 100644 src/domains/template_gen_rec_summary.h create mode 100755 src/solver/summarizer_rec_fw.cpp create mode 100755 src/solver/summarizer_rec_fw.h diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp index a9e8a3f76..9c69d5c79 100644 --- a/src/2ls/2ls_parse_options.cpp +++ b/src/2ls/2ls_parse_options.cpp @@ -53,6 +53,7 @@ Author: Daniel Kroening, Peter Schrammel #include "summary_checker_bmc.h" #include "summary_checker_kind.h" #include "summary_checker_nonterm.h" +#include "summary_checker_rect.h" #include "show.h" #include "horn_encoding.h" @@ -316,6 +317,13 @@ void twols_parse_optionst::get_command_line_options(optionst &options) if(!cmdline.isset("unwind")) options.set_option("unwind", std::numeric_limits::max()); } + //............................................ + // handle recursive functions + if(cmdline.isset("has-recursion")) + { + options.set_option("has-recursion", true); + } + //............................................. // check for spuriousness of assertion failures if(cmdline.isset("no-spurious-check")) @@ -493,9 +501,9 @@ int twols_parse_optionst::doit() } #if IGNORE_RECURSION - if(recursion_detected) + if(recursion_detected && !cmdline.isset("has-recursion")) { - status() << "Recursion not supported" << eom; + status() << "Recursion not supportedwithout --has-recursion option" << eom; report_unknown(); return 5; } @@ -582,8 +590,15 @@ int twols_parse_optionst::doit() std::unique_ptr checker; if(!options.get_bool_option("k-induction") && !options.get_bool_option("incremental-bmc")) - checker=std::unique_ptr( - new summary_checker_ait(options, heap_analysis)); + { + if(options.get_bool_option("has-recursion")) + checker=std::unique_ptr( + new summary_checker_rect(options, heap_analysis)); + else + checker=std::unique_ptr( + new summary_checker_ait(options, heap_analysis)); + + } if(options.get_bool_option("k-induction") && !options.get_bool_option("incremental-bmc")) checker=std::unique_ptr( @@ -1765,6 +1780,7 @@ void twols_parse_optionst::help() " --termination compute ranking functions to prove termination\n" // NOLINT(*) " --k-induction use k-induction\n" " --incremental-bmc use incremental-bmc\n" + " --has-recursion enable recursive function support" " --preconditions compute preconditions\n" " --sufficient sufficient preconditions (default: necessary)\n" // NOLINT(*) " --havoc havoc loops and function calls\n" diff --git a/src/2ls/2ls_parse_options.h b/src/2ls/2ls_parse_options.h index 2199b95d3..2bdf1dc75 100644 --- a/src/2ls/2ls_parse_options.h +++ b/src/2ls/2ls_parse_options.h @@ -65,7 +65,7 @@ class optionst; "(graphml-witness):(json-cex):" \ "(no-spurious-check)(stop-on-fail)" \ "(competition-mode)(slice)(no-propagation)(independent-properties)" \ - "(no-unwinding-assertions)" + "(no-unwinding-assertions)(has-recursion)" // the last line is for CBMC-regression testing only class twols_parse_optionst: diff --git a/src/2ls/Makefile b/src/2ls/Makefile index 5b9362169..c817b5e84 100644 --- a/src/2ls/Makefile +++ b/src/2ls/Makefile @@ -6,6 +6,7 @@ SRC = 2ls_main.cpp 2ls_parse_options.cpp \ 2ls_languages.cpp \ show.cpp summary_checker_base.cpp \ summary_checker_ai.cpp summary_checker_bmc.cpp \ + summary_checker_rect.cpp \ summary_checker_kind.cpp summary_checker_nonterm.cpp \ cover_goals_ext.cpp horn_encoding.cpp \ preprocessing_util.cpp \ diff --git a/src/2ls/summary_checker_base.cpp b/src/2ls/summary_checker_base.cpp index 63aa43f15..d5305edf2 100644 --- a/src/2ls/summary_checker_base.cpp +++ b/src/2ls/summary_checker_base.cpp @@ -7,6 +7,7 @@ Author: Peter Schrammel \*******************************************************************/ #include +#include #include #include @@ -51,6 +52,564 @@ Function: summary_checker_baset::SSA_functions \*******************************************************************/ +///////////////////////////////////ic3//////////////////////////////// +std::string extract_var(std::string in) +{ + std::string::iterator i; + std::string s=""; + for(i=in.begin();*i!='#';i++) + { + s.append(1,*i); + } + return s; +} + +int is_var(std::vector vars,std::string in) +{ + std::string var; + if(in.at(0)=='$') + return -1; + else + { + std::string::iterator i; + int count=-1,pos=-1; + for(i=in.begin();i!=in.end();i++) + { + if(*i=='#') + { + std::vector::iterator i1; + for(i1=vars.begin();i1!=vars.end();i1++) + { + std::string var1=extract_var(from_expr(*i1)); + count++; + if(var.compare(var1)==0) pos=count; + } + if(pos==-1) return pos; + } + var.append(1,*i); + } + return pos; + } +} +bool construct_cnf(std::vector& P,std::ofstream& out,std::string in,std::vector pre_vars,unsigned loophead)//reads the input formula and construct an cnf object +{ + int flag=0,sign=0,size=0; + std::string::iterator i; + std::string *s=new std::string(),*clause=new std::string(pre_vars.size(),'X'); + for (i=in.begin();i!=in.end();i++) + { + if(*i=='&') + { + std::vector::iterator i1; + if((s->compare("True")==0&&sign==0)||(s->compare("False")==0&&sign==1)) + { + s->clear(); + clause->insert(0,'X',pre_vars.size()); + size=0; + continue; + } + else if((s->compare("False")==0&&sign==0)||(s->compare("True")==0&&sign==1)) + { + if(size==0) + { + P.clear(); + out<<"P is FALSE.\n"; + return false; + } + } + else + { + std::vector::iterator i1; + int pos=0; + *s=*s+"#phi"+std::to_string(loophead); + for(i1=pre_vars.begin();i1!=pre_vars.end();i1++) + { + if(from_expr(*i1).compare(*s)==0) + { + if(sign==0 && clause->at(pos)!='F') (*clause)[pos]='T'; + else if(clause->at(pos)!='T') (*clause)[pos]='F'; + else + { + out<<"Contradiction in I.\n"; + return false; + } + break; + } + pos++; + } + sign=0; + if(pos==pre_vars.size()) return false; + P.push_back(*clause); + s->clear(); + clause=new std::string(pre_vars.size(),'X'); + size=0; + } + } + else if(*i=='|') + { + std::vector::iterator i1; + if((s->compare("True")==0&&sign==0)||(s->compare("False")==0&&sign==1)) + { + while(*i!='&'||i!=in.end()) + { + i++; + } + i--; + clause->insert(0,'X',pre_vars.size()); + size=0; + } + else if((s->compare("False")==0&&sign==0)||(s->compare("True")==0&&sign==1)) + { + + } + else + { + std::vector::iterator i1; + int pos=0; + *s=*s+"#phi"+std::to_string(loophead); + for(i1=pre_vars.begin();i1!=pre_vars.end();i1++) + { + if(from_expr(*i1).compare(*s)==0) + { + if(sign==0 && clause->at(pos)!='F') (*clause)[pos]='T'; + else if(clause->at(pos)!='T') (*clause)[pos]='F'; + else + { + out<<"Contradiction in I.\n"; + return false; + } + break; + } + pos++; + } + sign=0; + if(pos==pre_vars.size()) return false; + } + s->clear(); + } + else if(*i == '(') + { + if(!(s->empty())) + { + out<<"Error in the formula\n"; + return false; + } + if(flag==1) + { + out<<"Parenthesis mismatch\n"; + return false; + } + flag=1; + } + else if(*i == ')') + { + if(flag==0) + { + out<<"Parenthesis mismatch\n"; + return false; + } + flag=0; + } + else if(*i == '~') sign=1; + else + { + s->append(1,*i); + } + } + if(flag!=0){ + out<<"Parenthesis mismatch\n"; + return false; + } + std::vector::iterator i1; + if((s->compare("True")==0&&sign==0)||(s->compare("False")==0&&sign==1)) + { + + } + else if((s->compare("False")==0&&sign==0)||(s->compare("True")==0&&sign==1)) + { + if(size==0) + { + P.clear(); + out<<"P is FALSE.\n"; + return false; + } + } + else + { + std::vector::iterator i1; + int pos=0; + *s=*s+"#phi"+std::to_string(loophead); + for(i1=pre_vars.begin();i1!=pre_vars.end();i1++) + { + if(from_expr(*i1).compare(*s)==0) + { + if(sign==0 && clause->at(pos)!='F') (*clause)[pos]='T'; + else if(clause->at(pos)!='T') (*clause)[pos]='F'; + else + { + out<<"Contradiction in I.\n"; + return false; + } + break; + } + pos++; + } + if(pos==pre_vars.size()) return false; + P.push_back(*clause); + } + if(P.empty()) + { + clause->clear(); + out<<"Property is True.\n"; + P.clear(); + return false; + } + return true; +} + +exprt clause_to_exprt(std::string clause,std::vector vars) +{ + std::vector lits; + unsigned i2; + constant_exprt f("00000000",vars.at(0).type()); + for(i2 = 0;i2 to_exprt_vec(std::vector P,std::vector vars)//adds clauses of the caller cnf to the Solver object +{ + std::vector conjuncts; + std::vector< std::string >::iterator i1; + for(i1 = P.begin();i1 != P.end();i1++) + { + conjuncts.push_back(clause_to_exprt(*i1,vars)); + //std::cout<<"\n"; + } + //std::cout<<"solver::"<> &Frames,int no,std::vector pre_vars,std::vector post_vars,const namespacet &ns,unsigned loophead) +{ + constant_exprt f("00000000",pre_vars.at(0).type()); + incremental_solvert solver(ns),solver1(ns); + solver< conjuncts,disjuncts; + std::vector::iterator iter; + out<<"At frame "<\n"; + int pos=0; + for(iter=pre_vars.begin();iter!=pre_vars.end();iter++) + { + exprt e1=solver.get(*iter); + if(from_expr(ns,"",e1).compare("TRUE")==0) + { + disjuncts.push_back(equal_exprt(*iter,f)); + conjuncts.push_back(equal_exprt(post_vars.at(pos),e1)); + blocked_clause[pos]='F'; + } + else if(from_expr(ns,"",e1).compare("FALSE")==0) + { + disjuncts.push_back(notequal_exprt(*iter,f)); + conjuncts.push_back(equal_exprt(post_vars.at(pos),e1)); + blocked_clause[pos]='T'; + } + pos++; + } + out<<" CTI "<::iterator iter1=Frames.at(i).begin();iter1!=Frames.at(i).end();iter1++) + { + if(subsumes(*iter1,blocked_clause)) subsumes_flag=true; + } + if(!subsumes_flag) Frames.at(i).push_back(blocked_clause); + } + out<<"Blocked clause(Blocked upto frame "< frame1,std::vector frame2) +{ + +}*/ + +bool propagate_clauses(std::ofstream& out,exprt T,std::vector> &Frames,std::vector pre_vars,std::vector post_vars,int framesize,const namespacet &ns) +{ + out<<"Propagation phase |-------------------------------------------->\n\n"; + int i1; + for(i1=0;i1<=framesize;i1++) + { + std::vector Clauses1=Frames.at(i1),Clauses2=Frames.at(i1+1); + unsigned i2,i3; + for(i2=0;i2 P_pre,std::vector P,std::vector pre_vars,std::vector post_vars,unsigned loophead) +{ + incremental_solvert solver(ns); + solver< P_post=to_exprt_vec(P,post_vars); + solver1<> Frames; + Frames.push_back(std::vector(P)); + int iter=0; + out<<"\n=======================IC3 iteration "<=0) + { + incremental_solvert solver2(ns); + solver2<\n\n"; + for(std::vector::iterator i=P_post.begin();i!=P_post.end();i++) + { + if(!(block_recursively(out,I,T,not_exprt(*i),Frames,iter,pre_vars,post_vars,ns,loophead))) + { + return; + } + } + } + else + { + Frames.push_back(std::vector()); + if(propagate_clauses(out,T,Frames,pre_vars,post_vars,iter,ns)) return; + int i=0; + while(i<=iter+1) + { + out<<"Frame"<& pre_vars,std::vector& post_vars,unsigned& loophead,exprt& I,exprt& T) +{ + std::vector conjuncts,conjuncts1; + unsigned loopend=0; + loophead=0; + for(local_SSAt::nodest::const_iterator n_it=SSA.nodes.begin(); + n_it!=SSA.nodes.end(); n_it++) + { + if(n_it->loophead!=SSA.nodes.end()) + { + loophead=n_it->loophead->location->location_number; + loopend=n_it->location->location_number; + break; + } + } + if(loophead==loopend&&loopend==0) + { + out<<"No loop in the program\n"; + return false; + } + for(local_SSAt::nodest::const_iterator n_it=SSA.nodes.begin(); + n_it!=SSA.nodes.end(); n_it++) + { + if(n_it->location->location_number==loophead) + { + exprt loop_exit_cond,temp_exp; + for(local_SSAt::nodet::equalitiest::const_iterator c_it=n_it->equalities.begin(); + c_it!=n_it->equalities.end(); + c_it++) + { + pre_vars.push_back((*c_it).op0()); + loop_exit_cond=temp_exp; + temp_exp=*c_it; + } + pre_vars.pop_back(); + pre_vars.pop_back(); + conjuncts.push_back(loop_exit_cond); + conjuncts.push_back(equal_exprt(temp_exp.op0(),true_exprt())); + } + } + exprt post_vars1[pre_vars.size()]; + for(local_SSAt::nodest::const_iterator n_it=SSA.nodes.begin(); + n_it!=SSA.nodes.end(); n_it++) + { + if(n_it->location->location_numberequalities.begin(); + c_it!=n_it->equalities.end(); + c_it++) + { + conjuncts1.push_back(*c_it); + } + } + else if(n_it->location->location_number==loophead) + { + for(local_SSAt::nodet::equalitiest::const_iterator c_it=n_it->equalities.begin(); + c_it!=n_it->equalities.end(); + c_it++) + { + conjuncts1.push_back(*c_it); + } + local_SSAt::nodet::equalitiest::const_iterator c_it=n_it->equalities.begin(); + conjuncts1.pop_back(); + conjuncts1.pop_back(); + conjuncts1.push_back(equal_exprt(c_it->op1().op0(),false_exprt())); + I=conjunction(conjuncts1); + } + else if(n_it->location->location_number>loophead && n_it->location->location_number<=loopend) + { + for(local_SSAt::nodet::equalitiest::const_iterator c_it=n_it->equalities.begin(); + c_it!=n_it->equalities.end(); + c_it++) + { + int pos=is_var(pre_vars,from_expr(c_it->op0())); + if(pos!=-1) + { + post_vars1[pos]=c_it->op0(); + } + conjuncts.push_back(*c_it); + } + } + } + unsigned j; + for(j=0;j pre_vars,post_vars; + unsigned loophead=0; + exprt I,T; + if(!get_I_and_T(out,SSA,ns,pre_vars,post_vars,loophead,I,T)) return; + out<<"T:= "<>prop; + std::vector P; + if(!construct_cnf(P,out,prop,pre_vars,loophead)) + { + out<<"Error in the given property\n"; + return; + } + std::vector P_pre=to_exprt_vec(P,pre_vars); + out<<"\nP:= "< +#include +#include +#include +#include + +#include "summary_checker_rect.h" + +property_checkert::resultt summary_checker_rect::operator()( + const goto_modelt &goto_model) +{ + const namespacet ns(goto_model.symbol_table); + + SSA_functions(goto_model, ns, heap_analysis); + + ssa_unwinder.init(false, false); + + unsigned unwind=options.get_unsigned_int_option("unwind"); + if(unwind>0) + { + status() << "Unwinding" << messaget::eom; + + ssa_unwinder.init_localunwinders(); + + ssa_unwinder.unwind_all(unwind); + } + + // properties + initialize_property_map(goto_model.goto_functions); + + bool preconditions=options.get_bool_option("preconditions"); + bool termination=options.get_bool_option("termination"); + bool trivial_domain=options.get_bool_option("havoc"); + if(!trivial_domain || termination) + { + // forward analysis + summarize(goto_model, true, termination); + } + /*if(preconditions) + { + report_statistics(); + report_preconditions(); + return property_checkert::UNKNOWN; + } + + if(termination) + { + report_statistics(); + return report_termination(); + } + +#ifdef SHOW_CALLINGCONTEXTS + if(options.get_bool_option("show-calling-contexts")) + return property_checkert::UNKNOWN; +#endif + + property_checkert::resultt result=check_properties(); + report_statistics(); + return result;*/ + return UNKNOWN; +} + +void summary_checker_rect::summarize( + const goto_modelt &goto_model, + bool forward, + bool termination) +{ + summarizer_baset *summarizer=NULL; +#ifdef SHOW_CALLING_CONTEXTS + if(options.get_bool_option("show-calling-contexts")) + summarizer=new summarizer_fw_contextst( + options, summary_db, ssa_db, ssa_unwinder, ssa_inliner); + else // NOLINT(*) +#endif + { + if(forward && !termination) + summarizer=new summarizer_rec_fwt( + options, summary_db, ssa_db, ssa_unwinder, ssa_inliner); + } + assert(summarizer!=NULL); + summarizer->set_message_handler(get_message_handler()); + if(!options.get_bool_option("context-sensitive") && + options.get_bool_option("all-functions")) + summarizer->summarize(); + else + summarizer->summarize(goto_model.goto_functions.entry_point()); + + // statistics + /*solver_instances+=summarizer->get_number_of_solver_instances(); + solver_calls+=summarizer->get_number_of_solver_calls(); + summaries_used+=summarizer->get_number_of_summaries_used(); + termargs_computed+=summarizer->get_number_of_termargs_computed();*/ + + delete summarizer; +} diff --git a/src/2ls/summary_checker_rect.h b/src/2ls/summary_checker_rect.h new file mode 100644 index 000000000..9e70c52e6 --- /dev/null +++ b/src/2ls/summary_checker_rect.h @@ -0,0 +1,28 @@ +/* + * File: summary_checker_rect.h + * Author: sarbojit + * + * Created on 21 March, 2018, 7:13 PM + */ + +#ifndef SUMMARY_CHECKER_RECT_H +#define SUMMARY_CHECKER_RECT_H + +#include "summary_checker_ai.h" + +class summary_checker_rect:public summary_checker_ait +{ +public: + explicit summary_checker_rect(optionst &_options, + const ssa_heap_analysist &heap_analysis): + summary_checker_ait(_options, heap_analysis) + { + } + + virtual resultt operator()(const goto_modelt &); +protected: + void summarize(const goto_modelt &, bool, bool); +}; + +#endif /* SUMMARY_CHECKER_RECT_H */ + diff --git a/src/domains/Makefile b/src/domains/Makefile index e293aee2f..f25ec032b 100644 --- a/src/domains/Makefile +++ b/src/domains/Makefile @@ -9,6 +9,7 @@ SRC = tpolyhedra_domain.cpp equality_domain.cpp domain.cpp \ strategy_solver_enumeration.cpp strategy_solver_binsearch.cpp \ template_generator_base.cpp template_generator_summary.cpp \ template_generator_callingcontext.cpp template_generator_ranking.cpp \ + template_gen_rec_summary.cpp \ strategy_solver_binsearch2.cpp strategy_solver_binsearch3.cpp \ strategy_solver_predabs.cpp strategy_solver_heap.cpp \ strategy_solver_heap_tpolyhedra.cpp \ diff --git a/src/domains/domain.h b/src/domains/domain.h index 5f8fde816..0f54581f3 100644 --- a/src/domains/domain.h +++ b/src/domains/domain.h @@ -65,6 +65,10 @@ class domaint }; virtual void initialize(valuet &value) { value.basic_value=valuet::BOTTOM; } + virtual void initialize_in_templates(valuet &value, + std::map context_bounds= + std::map()) {assert(false);} + // returns true as long as further refinements are possible virtual void reset_refinements() { } diff --git a/src/domains/ssa_analyzer.cpp b/src/domains/ssa_analyzer.cpp index 72ad03b52..9a5460fad 100644 --- a/src/domains/ssa_analyzer.cpp +++ b/src/domains/ssa_analyzer.cpp @@ -63,7 +63,10 @@ void ssa_analyzert::operator()( incremental_solvert &solver, local_SSAt &SSA, const exprt &precondition, - template_generator_baset &template_generator) + template_generator_baset &template_generator, + bool recursive, + std::map context_bounds, + tmpl_rename_mapt templ_maps) { if(SSA.goto_function.body.instructions.empty()) return; @@ -75,7 +78,10 @@ void ssa_analyzert::operator()( solver << SSA.get_enabling_exprs(); // add precondition (or conjunction of asssertion in backward analysis) - solver << precondition; + if(!template_generator.options.get_bool_option("has-recursion") || + !recursive || + !template_generator.options.get_bool_option("context-sensitive")) + solver << precondition; domain=template_generator.domain(); @@ -174,10 +180,24 @@ void ssa_analyzert::operator()( // initialize inv domain->initialize(*result); + // initialize input arguments and input global variables with calling context + if(recursive && + template_generator.options.get_bool_option("context-sensitive")) + domain->initialize_in_templates(*result, context_bounds); // iterate while(strategy_solver->iterate(*result)) {} + /*if(recursive)//iterate for recursive function + { + assert(template_generator.options.get_bool_option("binsearch-solver")); + //while(strategy_solver->iterate_for_recursive(*result,templ_maps, + //template_generator.options.get_bool_option("context-sensitive"))) {} + while(strategy_solver->iterate(*result)) {}//need to change + } + else//iterate for non-recursive function + while(strategy_solver->iterate(*result)) {}*/ + solver.pop_context(); // statistics diff --git a/src/domains/ssa_analyzer.h b/src/domains/ssa_analyzer.h index 5398e883d..50e4ca098 100644 --- a/src/domains/ssa_analyzer.h +++ b/src/domains/ssa_analyzer.h @@ -22,7 +22,8 @@ class ssa_analyzert:public messaget public: typedef strategy_solver_baset::constraintst constraintst; typedef strategy_solver_baset::var_listt var_listt; - + typedef std::vector>> tmpl_rename_mapt; + ssa_analyzert(): result(NULL), solver_instances(0), @@ -40,7 +41,11 @@ class ssa_analyzert:public messaget incremental_solvert &solver, local_SSAt &SSA, const exprt &precondition, - template_generator_baset &template_generator); + template_generator_baset &template_generator, + bool recursive=false, + std::map context_bounds= + std::map(), + tmpl_rename_mapt templ_maps=tmpl_rename_mapt()); void get_result(exprt &result, const domaint::var_sett &vars); diff --git a/src/domains/strategy_solver_base.h b/src/domains/strategy_solver_base.h index 7915b5ef9..bb77bb485 100644 --- a/src/domains/strategy_solver_base.h +++ b/src/domains/strategy_solver_base.h @@ -31,6 +31,8 @@ class strategy_solver_baset:public messaget {} virtual bool iterate(invariantt &inv) { assert(false); } + /*virtual bool iterate_for_recursive( + invariantt &inv, tmpl_rename_mapt templ_maps,bool cntxt_sensitive) {assert(false);}*/ inline unsigned get_number_of_solver_calls() { return solver_calls; } inline unsigned get_number_of_solver_instances() { return solver_instances; } diff --git a/src/domains/strategy_solver_binsearch.h b/src/domains/strategy_solver_binsearch.h index 8bcdf7f4b..325122955 100644 --- a/src/domains/strategy_solver_binsearch.h +++ b/src/domains/strategy_solver_binsearch.h @@ -25,6 +25,8 @@ class strategy_solver_binsearcht:public strategy_solver_baset } virtual bool iterate(invariantt &inv); + /*virtual bool iterate_for_recursive( + invariantt &inv, tmpl_rename_mapt templ_maps,bool cntxt_sensitive);*/ protected: tpolyhedra_domaint &tpolyhedra_domain; diff --git a/src/domains/template_gen_rec_summary.cpp b/src/domains/template_gen_rec_summary.cpp new file mode 100644 index 000000000..74818cc3e --- /dev/null +++ b/src/domains/template_gen_rec_summary.cpp @@ -0,0 +1,69 @@ +/* + * To change this license header, choose License Headers in Project Properties. + * To change this template file, choose Tools | Templates + * and open the template in the editor. + */ + +/* + * File: template_gen_rec_summary.cpp + * Author: sarbojit + * + * Created on 19 March, 2018, 10:19 PM + */ + +#define SHOW_TEMPLATE +#include "tpolyhedra_domain.h" + +#include "template_gen_rec_summary.h" + +void template_gen_rec_summaryt::operator()(const irep_idt &function_name, + unsigned _domain_number, + const local_SSAt &SSA, tmpl_rename_mapt &templ_maps, + bool forward, bool recursive) +{ + domain_number=_domain_number; + handle_special_functions(SSA); // we have to call that to prevent trouble! + + collect_variables_loop(SSA, forward); + + // do not compute summary for entry-point + if(SSA.goto_function.body.instructions.front().function!=ID__start || + options.get_bool_option("preconditions")) + { + collect_variables_inout(SSA, forward); + } + if(recursive) get_renaming_maps(function_name,SSA,templ_maps); + // either use standard templates or user-supplied ones + if(!instantiate_custom_templates(SSA)) + instantiate_standard_domains(SSA,recursive); + +#ifdef SHOW_TEMPLATE_VARIABLES + debug() << "Template variables: " << eom; + domaint::output_var_specs(debug(), var_specs, SSA.ns); debug() << eom; +#endif +#ifdef SHOW_TEMPLATE + debug() << "Template: " << eom; + domain_ptr->output_domain(debug(), SSA.ns); debug() << eom; +#endif +} + +void template_gen_rec_summaryt::get_renaming_maps(const irep_idt &function_name, + local_SSAt SSA,tmpl_rename_mapt &templ_maps) +{ + for(local_SSAt::nodet node:SSA.nodes) + for(function_application_exprt f_call:node.function_calls) + if(function_name==to_symbol_expr(f_call.function()).get_identifier()) + { + std::pair> p(SSA.guard_symbol(node.location), + std::vector(f_call.arguments())); + std::set globals_in,globals_out; + SSA.get_globals(node.location,globals_in); + for(exprt e:globals_in) {p.second.push_back(e);} + SSA.get_globals(node.location,globals_out,false); + for(exprt e:globals_out) {p.second.push_back(e);} + for(domaint::var_spect s:var_specs) {std::cout<>> tmpl_rename_mapt; + explicit template_gen_rec_summaryt( + optionst &_options, + ssa_dbt &_ssa_db, + ssa_local_unwindert &_ssa_local_unwinder): + template_generator_summaryt(_options, _ssa_db, _ssa_local_unwinder) + { + } + virtual void operator()(const irep_idt &function_name, + unsigned _domain_number, + const local_SSAt &SSA, tmpl_rename_mapt &templ_maps, + bool forward=true, bool recursive=false); + + void get_renaming_maps(const irep_idt &function_name,local_SSAt SSA, + tmpl_rename_mapt &templ_maps); +}; + +#endif /* TEMPLATE_GEN_REC_SUMMARY_H */ + diff --git a/src/domains/template_generator_base.cpp b/src/domains/template_generator_base.cpp index f9a56e7bd..788c84d86 100644 --- a/src/domains/template_generator_base.cpp +++ b/src/domains/template_generator_base.cpp @@ -739,7 +739,7 @@ Function: template_generator_baset::instantiate_standard_domains \*******************************************************************/ void template_generator_baset::instantiate_standard_domains( - const local_SSAt &SSA) + const local_SSAt &SSA, bool recursive) { replace_mapt &renaming_map= std_invariants ? aux_renaming_map : post_renaming_map; @@ -762,7 +762,9 @@ void template_generator_baset::instantiate_standard_domains( new tpolyhedra_domaint(domain_number, renaming_map, SSA.ns); filter_template_domain(); static_cast(domain_ptr) - ->add_interval_template(var_specs, SSA.ns); + ->add_interval_template(var_specs, SSA.ns, + options.get_bool_option("context-sensitive") && + recursive); } else if(options.get_bool_option("zones")) { diff --git a/src/domains/template_generator_base.h b/src/domains/template_generator_base.h index 1c42a6c0c..5668166d8 100644 --- a/src/domains/template_generator_base.h +++ b/src/domains/template_generator_base.h @@ -130,7 +130,7 @@ class template_generator_baset:public messaget exprt &expr); virtual void handle_special_functions(const local_SSAt &SSA); - void instantiate_standard_domains(const local_SSAt &SSA); + void instantiate_standard_domains(const local_SSAt &SSA, bool recursive=false); bool instantiate_custom_templates(const local_SSAt &SSA); void rename_aux_post(symbol_exprt &expr) diff --git a/src/domains/tpolyhedra_domain.cpp b/src/domains/tpolyhedra_domain.cpp index dbbecde6e..03fb38b5c 100644 --- a/src/domains/tpolyhedra_domain.cpp +++ b/src/domains/tpolyhedra_domain.cpp @@ -53,6 +53,31 @@ void tpolyhedra_domaint::initialize(valuet &value) } } +void tpolyhedra_domaint::initialize_in_templates(valuet &value, + std::map context_bounds) +{ + templ_valuet &v=static_cast(value); + v.resize(templ.size()); + for(std::size_t row=0; row context_bounds= + std::map()); virtual void join(valuet &value1, const valuet &value2); @@ -124,7 +127,8 @@ class tpolyhedra_domaint:public domaint void add_interval_template( const var_specst &var_specs, - const namespacet &ns); + const namespacet &ns, + bool rec_cntx_sensitive=false); void add_difference_template( const var_specst &var_specs, const namespacet &ns); diff --git a/src/solver/Makefile b/src/solver/Makefile index bd0fe97b7..ada270d7c 100644 --- a/src/solver/Makefile +++ b/src/solver/Makefile @@ -1,6 +1,7 @@ SRC = summarizer_base.cpp summarizer_bw.cpp \ summarizer_bw_term.cpp summarizer_fw_contexts.cpp \ summarizer_fw.cpp summarizer_fw_term.cpp \ + summarizer_rec_fw.cpp \ summary.cpp summary_db.cpp include ../config.inc diff --git a/src/solver/summarizer_fw.cpp b/src/solver/summarizer_fw.cpp index 27f8dd1da..7d3370084 100644 --- a/src/solver/summarizer_fw.cpp +++ b/src/solver/summarizer_fw.cpp @@ -214,8 +214,9 @@ void summarizer_fwt::inline_summaries( 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)) + if(to_symbol_expr(f_it->function()).get_identifier()==function_name || + !check_call_reachable( + function_name, SSA, n_it, f_it, precondition, true)) { continue; } diff --git a/src/solver/summarizer_fw.h b/src/solver/summarizer_fw.h index 6ee541620..a57f4636f 100644 --- a/src/solver/summarizer_fw.h +++ b/src/solver/summarizer_fw.h @@ -39,7 +39,7 @@ class summarizer_fwt:public summarizer_baset const exprt &precondition, bool context_sensitive); - void inline_summaries( + virtual void inline_summaries( const function_namet &function_name, local_SSAt &SSA, const exprt &precondition, diff --git a/src/solver/summarizer_rec_fw.cpp b/src/solver/summarizer_rec_fw.cpp new file mode 100755 index 000000000..200727ed3 --- /dev/null +++ b/src/solver/summarizer_rec_fw.cpp @@ -0,0 +1,202 @@ +/* + * To change this license header, choose License Headers in Project Properties. + * To change this template file, choose Tools | Templates + * and open the template in the editor. + */ + +/* + * File: summarizer_rec_fwt.cpp + * Author: sarbojit + * + * Created on 13 March, 2018, 4:53 PM + */ + +#include +#include +#include +#include "summarizer_rec_fw.h" + +void summarizer_rec_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 + + bool recursive=false; + for(local_SSAt::nodet node:SSA.nodes) + { + for(function_application_exprt f_call:node.function_calls) + if(function_name==to_symbol_expr(f_call.function()).get_identifier()) + recursive=true; + } + if(recursive)//if this_function_is_recursive + { + //inline other non-recursive functions in the same SCC of the call graph + //this makes it self recursive + } + + // recursively compute summaries for non-recursive 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(const auto &node : SSA.nodes) + { + if(!node.empty()) + node.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; + //if(recursive) summary.fw_precondition=true; + summary.fw_precondition=precondition; + + + if(!options.get_bool_option("havoc")) + { + do_summary(function_name, SSA, summary, true_exprt(), context_sensitive,recursive); + } + + #if 0 + 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; + } + #endif + + // store summary in db + //summary_db.put(function_name, summary); + + /*if(!options.get_bool_option("competition-mode")) + { + std::ostringstream out; + out << std::endl << "Summary for function " << function_name << std::endl; + summary_db.get(function_name).output(out, SSA.ns); + status() << out.str() << eom; + }*/ +} + +void summarizer_rec_fwt::do_summary( + const function_namet &function_name, + local_SSAt &SSA, + summaryt &summary, + exprt cond, + bool context_sensitive,bool recursive) +{ + status() << "Computing summary" << eom; + + // solver + incremental_solvert &solver=ssa_db.get_solver(function_name); + solver.set_message_handler(get_message_handler()); + + // analyze + ssa_analyzert analyzer; + analyzer.set_message_handler(get_message_handler()); + + tmpl_rename_mapt templ_maps; + + template_gen_rec_summaryt template_generator( + options, ssa_db, ssa_unwinder.get(function_name)); + template_generator.set_message_handler(get_message_handler()); + template_generator( + function_name,solver.next_domain_number(), SSA, templ_maps, true,recursive); + + exprt::operandst conds; + conds.reserve(5); + conds.push_back(cond); + if(!(recursive && context_sensitive)) conds.push_back(summary.fw_precondition); + conds.push_back(ssa_inliner.get_summaries(SSA)); + +#ifdef REUSE_INVARIANTS + if(summary_db.exists(function_name)) // reuse existing invariants + { + const exprt &old_inv=summary_db.get(function_name).fw_invariant; + exprt inv=ssa_unwinder.get(function_name).rename_invariant(old_inv); + conds.push_back(inv); + +#if 0 + std::ostringstream out; + out << "(original inv)" << from_expr(SSA.ns, "", old_inv) << "\n"; + debug() << out.str() << eom; + out << "(renamed inv)" << from_expr(SSA.ns, "", inv) << "\n"; + debug() << out.str() << eom; +#endif + } +#endif + + cond=conjunction(conds); + + std::map context_bounds; + if(recursive && context_sensitive) + { + context_bounds = get_context_bounds(summary.fw_precondition); + + /*for(std::pair p : context_bounds) + { + debug()< summarizer_rec_fwt::get_context_bounds( + exprt con) +{ + std::map cntxt_bound; + for(exprt op:con.operands()) + { + assert(op.id()==ID_le); + cntxt_bound.insert(std::pair + (op.op0(),to_constant_expr(op.op1()))); + } + return cntxt_bound; +} \ No newline at end of file diff --git a/src/solver/summarizer_rec_fw.h b/src/solver/summarizer_rec_fw.h new file mode 100755 index 000000000..5dd646236 --- /dev/null +++ b/src/solver/summarizer_rec_fw.h @@ -0,0 +1,51 @@ +/* + * To change this license header, choose License Headers in Project Properties. + * To change this template file, choose Tools | Templates + * and open the template in the editor. + */ + +/* + * File: summarizer_rec_fwt.h + * Author: sarbojit + * + * Created on 13 March, 2018, 4:52 PM + */ + +#ifndef SUMMARIZER_REC_FWT_H +#define SUMMARIZER_REC_FWT_H + +#include +#include +#include + +#include +#include +#include +#include + +#include "summarizer_fw.h" + +class summarizer_rec_fwt:public summarizer_fwt { +public: + explicit summarizer_rec_fwt(optionst &_options, + summary_dbt &_summary_db, + ssa_dbt &_ssa_db, + ssa_unwindert &_ssa_unwinder, + ssa_inlinert &_ssa_inliner): + summarizer_fwt( + _options, _summary_db, _ssa_db, _ssa_unwinder, _ssa_inliner) + { + } + typedef std::vector>> tmpl_rename_mapt; +protected: + virtual void compute_summary_rec(const function_namet &, + const exprt &, bool); + + virtual void do_summary(const function_namet &, + local_SSAt &SSA, summaryt &summary, exprt cond, + bool context_sensitive, bool recursive); + std::map get_context_bounds(exprt); +}; + +#endif /* SUMMARIZER_REC_FWT_H */ + From 528b1d11c2a64ad58033ea7e3bc93015bfbafc67 Mon Sep 17 00:00:00 2001 From: Sarbojit Das Date: Fri, 14 Sep 2018 11:36:13 +0530 Subject: [PATCH 2/7] modified: src/2ls/summary_checker_base.cpp --- src/2ls/summary_checker_base.cpp | 558 ------------------------------- 1 file changed, 558 deletions(-) diff --git a/src/2ls/summary_checker_base.cpp b/src/2ls/summary_checker_base.cpp index d5305edf2..548dfbedf 100644 --- a/src/2ls/summary_checker_base.cpp +++ b/src/2ls/summary_checker_base.cpp @@ -52,564 +52,6 @@ Function: summary_checker_baset::SSA_functions \*******************************************************************/ -///////////////////////////////////ic3//////////////////////////////// -std::string extract_var(std::string in) -{ - std::string::iterator i; - std::string s=""; - for(i=in.begin();*i!='#';i++) - { - s.append(1,*i); - } - return s; -} - -int is_var(std::vector vars,std::string in) -{ - std::string var; - if(in.at(0)=='$') - return -1; - else - { - std::string::iterator i; - int count=-1,pos=-1; - for(i=in.begin();i!=in.end();i++) - { - if(*i=='#') - { - std::vector::iterator i1; - for(i1=vars.begin();i1!=vars.end();i1++) - { - std::string var1=extract_var(from_expr(*i1)); - count++; - if(var.compare(var1)==0) pos=count; - } - if(pos==-1) return pos; - } - var.append(1,*i); - } - return pos; - } -} -bool construct_cnf(std::vector& P,std::ofstream& out,std::string in,std::vector pre_vars,unsigned loophead)//reads the input formula and construct an cnf object -{ - int flag=0,sign=0,size=0; - std::string::iterator i; - std::string *s=new std::string(),*clause=new std::string(pre_vars.size(),'X'); - for (i=in.begin();i!=in.end();i++) - { - if(*i=='&') - { - std::vector::iterator i1; - if((s->compare("True")==0&&sign==0)||(s->compare("False")==0&&sign==1)) - { - s->clear(); - clause->insert(0,'X',pre_vars.size()); - size=0; - continue; - } - else if((s->compare("False")==0&&sign==0)||(s->compare("True")==0&&sign==1)) - { - if(size==0) - { - P.clear(); - out<<"P is FALSE.\n"; - return false; - } - } - else - { - std::vector::iterator i1; - int pos=0; - *s=*s+"#phi"+std::to_string(loophead); - for(i1=pre_vars.begin();i1!=pre_vars.end();i1++) - { - if(from_expr(*i1).compare(*s)==0) - { - if(sign==0 && clause->at(pos)!='F') (*clause)[pos]='T'; - else if(clause->at(pos)!='T') (*clause)[pos]='F'; - else - { - out<<"Contradiction in I.\n"; - return false; - } - break; - } - pos++; - } - sign=0; - if(pos==pre_vars.size()) return false; - P.push_back(*clause); - s->clear(); - clause=new std::string(pre_vars.size(),'X'); - size=0; - } - } - else if(*i=='|') - { - std::vector::iterator i1; - if((s->compare("True")==0&&sign==0)||(s->compare("False")==0&&sign==1)) - { - while(*i!='&'||i!=in.end()) - { - i++; - } - i--; - clause->insert(0,'X',pre_vars.size()); - size=0; - } - else if((s->compare("False")==0&&sign==0)||(s->compare("True")==0&&sign==1)) - { - - } - else - { - std::vector::iterator i1; - int pos=0; - *s=*s+"#phi"+std::to_string(loophead); - for(i1=pre_vars.begin();i1!=pre_vars.end();i1++) - { - if(from_expr(*i1).compare(*s)==0) - { - if(sign==0 && clause->at(pos)!='F') (*clause)[pos]='T'; - else if(clause->at(pos)!='T') (*clause)[pos]='F'; - else - { - out<<"Contradiction in I.\n"; - return false; - } - break; - } - pos++; - } - sign=0; - if(pos==pre_vars.size()) return false; - } - s->clear(); - } - else if(*i == '(') - { - if(!(s->empty())) - { - out<<"Error in the formula\n"; - return false; - } - if(flag==1) - { - out<<"Parenthesis mismatch\n"; - return false; - } - flag=1; - } - else if(*i == ')') - { - if(flag==0) - { - out<<"Parenthesis mismatch\n"; - return false; - } - flag=0; - } - else if(*i == '~') sign=1; - else - { - s->append(1,*i); - } - } - if(flag!=0){ - out<<"Parenthesis mismatch\n"; - return false; - } - std::vector::iterator i1; - if((s->compare("True")==0&&sign==0)||(s->compare("False")==0&&sign==1)) - { - - } - else if((s->compare("False")==0&&sign==0)||(s->compare("True")==0&&sign==1)) - { - if(size==0) - { - P.clear(); - out<<"P is FALSE.\n"; - return false; - } - } - else - { - std::vector::iterator i1; - int pos=0; - *s=*s+"#phi"+std::to_string(loophead); - for(i1=pre_vars.begin();i1!=pre_vars.end();i1++) - { - if(from_expr(*i1).compare(*s)==0) - { - if(sign==0 && clause->at(pos)!='F') (*clause)[pos]='T'; - else if(clause->at(pos)!='T') (*clause)[pos]='F'; - else - { - out<<"Contradiction in I.\n"; - return false; - } - break; - } - pos++; - } - if(pos==pre_vars.size()) return false; - P.push_back(*clause); - } - if(P.empty()) - { - clause->clear(); - out<<"Property is True.\n"; - P.clear(); - return false; - } - return true; -} - -exprt clause_to_exprt(std::string clause,std::vector vars) -{ - std::vector lits; - unsigned i2; - constant_exprt f("00000000",vars.at(0).type()); - for(i2 = 0;i2 to_exprt_vec(std::vector P,std::vector vars)//adds clauses of the caller cnf to the Solver object -{ - std::vector conjuncts; - std::vector< std::string >::iterator i1; - for(i1 = P.begin();i1 != P.end();i1++) - { - conjuncts.push_back(clause_to_exprt(*i1,vars)); - //std::cout<<"\n"; - } - //std::cout<<"solver::"<> &Frames,int no,std::vector pre_vars,std::vector post_vars,const namespacet &ns,unsigned loophead) -{ - constant_exprt f("00000000",pre_vars.at(0).type()); - incremental_solvert solver(ns),solver1(ns); - solver< conjuncts,disjuncts; - std::vector::iterator iter; - out<<"At frame "<\n"; - int pos=0; - for(iter=pre_vars.begin();iter!=pre_vars.end();iter++) - { - exprt e1=solver.get(*iter); - if(from_expr(ns,"",e1).compare("TRUE")==0) - { - disjuncts.push_back(equal_exprt(*iter,f)); - conjuncts.push_back(equal_exprt(post_vars.at(pos),e1)); - blocked_clause[pos]='F'; - } - else if(from_expr(ns,"",e1).compare("FALSE")==0) - { - disjuncts.push_back(notequal_exprt(*iter,f)); - conjuncts.push_back(equal_exprt(post_vars.at(pos),e1)); - blocked_clause[pos]='T'; - } - pos++; - } - out<<" CTI "<::iterator iter1=Frames.at(i).begin();iter1!=Frames.at(i).end();iter1++) - { - if(subsumes(*iter1,blocked_clause)) subsumes_flag=true; - } - if(!subsumes_flag) Frames.at(i).push_back(blocked_clause); - } - out<<"Blocked clause(Blocked upto frame "< frame1,std::vector frame2) -{ - -}*/ - -bool propagate_clauses(std::ofstream& out,exprt T,std::vector> &Frames,std::vector pre_vars,std::vector post_vars,int framesize,const namespacet &ns) -{ - out<<"Propagation phase |-------------------------------------------->\n\n"; - int i1; - for(i1=0;i1<=framesize;i1++) - { - std::vector Clauses1=Frames.at(i1),Clauses2=Frames.at(i1+1); - unsigned i2,i3; - for(i2=0;i2 P_pre,std::vector P,std::vector pre_vars,std::vector post_vars,unsigned loophead) -{ - incremental_solvert solver(ns); - solver< P_post=to_exprt_vec(P,post_vars); - solver1<> Frames; - Frames.push_back(std::vector(P)); - int iter=0; - out<<"\n=======================IC3 iteration "<=0) - { - incremental_solvert solver2(ns); - solver2<\n\n"; - for(std::vector::iterator i=P_post.begin();i!=P_post.end();i++) - { - if(!(block_recursively(out,I,T,not_exprt(*i),Frames,iter,pre_vars,post_vars,ns,loophead))) - { - return; - } - } - } - else - { - Frames.push_back(std::vector()); - if(propagate_clauses(out,T,Frames,pre_vars,post_vars,iter,ns)) return; - int i=0; - while(i<=iter+1) - { - out<<"Frame"<& pre_vars,std::vector& post_vars,unsigned& loophead,exprt& I,exprt& T) -{ - std::vector conjuncts,conjuncts1; - unsigned loopend=0; - loophead=0; - for(local_SSAt::nodest::const_iterator n_it=SSA.nodes.begin(); - n_it!=SSA.nodes.end(); n_it++) - { - if(n_it->loophead!=SSA.nodes.end()) - { - loophead=n_it->loophead->location->location_number; - loopend=n_it->location->location_number; - break; - } - } - if(loophead==loopend&&loopend==0) - { - out<<"No loop in the program\n"; - return false; - } - for(local_SSAt::nodest::const_iterator n_it=SSA.nodes.begin(); - n_it!=SSA.nodes.end(); n_it++) - { - if(n_it->location->location_number==loophead) - { - exprt loop_exit_cond,temp_exp; - for(local_SSAt::nodet::equalitiest::const_iterator c_it=n_it->equalities.begin(); - c_it!=n_it->equalities.end(); - c_it++) - { - pre_vars.push_back((*c_it).op0()); - loop_exit_cond=temp_exp; - temp_exp=*c_it; - } - pre_vars.pop_back(); - pre_vars.pop_back(); - conjuncts.push_back(loop_exit_cond); - conjuncts.push_back(equal_exprt(temp_exp.op0(),true_exprt())); - } - } - exprt post_vars1[pre_vars.size()]; - for(local_SSAt::nodest::const_iterator n_it=SSA.nodes.begin(); - n_it!=SSA.nodes.end(); n_it++) - { - if(n_it->location->location_numberequalities.begin(); - c_it!=n_it->equalities.end(); - c_it++) - { - conjuncts1.push_back(*c_it); - } - } - else if(n_it->location->location_number==loophead) - { - for(local_SSAt::nodet::equalitiest::const_iterator c_it=n_it->equalities.begin(); - c_it!=n_it->equalities.end(); - c_it++) - { - conjuncts1.push_back(*c_it); - } - local_SSAt::nodet::equalitiest::const_iterator c_it=n_it->equalities.begin(); - conjuncts1.pop_back(); - conjuncts1.pop_back(); - conjuncts1.push_back(equal_exprt(c_it->op1().op0(),false_exprt())); - I=conjunction(conjuncts1); - } - else if(n_it->location->location_number>loophead && n_it->location->location_number<=loopend) - { - for(local_SSAt::nodet::equalitiest::const_iterator c_it=n_it->equalities.begin(); - c_it!=n_it->equalities.end(); - c_it++) - { - int pos=is_var(pre_vars,from_expr(c_it->op0())); - if(pos!=-1) - { - post_vars1[pos]=c_it->op0(); - } - conjuncts.push_back(*c_it); - } - } - } - unsigned j; - for(j=0;j pre_vars,post_vars; - unsigned loophead=0; - exprt I,T; - if(!get_I_and_T(out,SSA,ns,pre_vars,post_vars,loophead,I,T)) return; - out<<"T:= "<>prop; - std::vector P; - if(!construct_cnf(P,out,prop,pre_vars,loophead)) - { - out<<"Error in the given property\n"; - return; - } - std::vector P_pre=to_exprt_vec(P,pre_vars); - out<<"\nP:= "< Date: Tue, 18 Sep 2018 11:59:00 +0530 Subject: [PATCH 3/7] modified: src/2ls/2ls_parse_options.cpp modified: src/2ls/2ls_parse_options.h modified: src/2ls/Makefile modified: src/2ls/summary_checker_base.cpp modified: src/2ls/summary_checker_base.h new file: src/2ls/summary_checker_rect.cpp new file: src/2ls/summary_checker_rect.h modified: src/domains/Makefile modified: src/domains/domain.h modified: src/domains/ssa_analyzer.cpp modified: src/domains/ssa_analyzer.h modified: src/domains/strategy_solver_base.h modified: src/domains/strategy_solver_binsearch.h new file: src/domains/template_gen_rec_summary.cpp new file: src/domains/template_gen_rec_summary.h modified: src/domains/template_generator_base.cpp modified: src/domains/template_generator_base.h modified: src/domains/tpolyhedra_domain.cpp modified: src/domains/tpolyhedra_domain.h modified: src/solver/Makefile modified: src/solver/summarizer_fw.cpp modified: src/solver/summarizer_fw.h new file: src/solver/summarizer_rec_fw.cpp new file: src/solver/summarizer_rec_fw.h --- src/2ls/2ls_parse_options.cpp | 24 ++- src/2ls/2ls_parse_options.h | 2 +- src/2ls/Makefile | 1 + src/2ls/summary_checker_base.cpp | 2 + src/2ls/summary_checker_base.h | 2 +- src/2ls/summary_checker_rect.cpp | 108 ++++++++++++ src/2ls/summary_checker_rect.h | 28 ++++ src/domains/Makefile | 1 + src/domains/domain.h | 4 + src/domains/ssa_analyzer.cpp | 24 ++- src/domains/ssa_analyzer.h | 9 +- src/domains/strategy_solver_base.h | 2 + src/domains/strategy_solver_binsearch.h | 2 + src/domains/template_gen_rec_summary.cpp | 69 ++++++++ src/domains/template_gen_rec_summary.h | 39 +++++ src/domains/template_generator_base.cpp | 6 +- src/domains/template_generator_base.h | 2 +- src/domains/tpolyhedra_domain.cpp | 32 +++- src/domains/tpolyhedra_domain.h | 6 +- src/solver/Makefile | 1 + src/solver/summarizer_fw.cpp | 5 +- src/solver/summarizer_fw.h | 2 +- src/solver/summarizer_rec_fw.cpp | 202 +++++++++++++++++++++++ src/solver/summarizer_rec_fw.h | 51 ++++++ 24 files changed, 604 insertions(+), 20 deletions(-) create mode 100644 src/2ls/summary_checker_rect.cpp create mode 100644 src/2ls/summary_checker_rect.h create mode 100644 src/domains/template_gen_rec_summary.cpp create mode 100644 src/domains/template_gen_rec_summary.h create mode 100755 src/solver/summarizer_rec_fw.cpp create mode 100755 src/solver/summarizer_rec_fw.h diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp index a9e8a3f76..9c69d5c79 100644 --- a/src/2ls/2ls_parse_options.cpp +++ b/src/2ls/2ls_parse_options.cpp @@ -53,6 +53,7 @@ Author: Daniel Kroening, Peter Schrammel #include "summary_checker_bmc.h" #include "summary_checker_kind.h" #include "summary_checker_nonterm.h" +#include "summary_checker_rect.h" #include "show.h" #include "horn_encoding.h" @@ -316,6 +317,13 @@ void twols_parse_optionst::get_command_line_options(optionst &options) if(!cmdline.isset("unwind")) options.set_option("unwind", std::numeric_limits::max()); } + //............................................ + // handle recursive functions + if(cmdline.isset("has-recursion")) + { + options.set_option("has-recursion", true); + } + //............................................. // check for spuriousness of assertion failures if(cmdline.isset("no-spurious-check")) @@ -493,9 +501,9 @@ int twols_parse_optionst::doit() } #if IGNORE_RECURSION - if(recursion_detected) + if(recursion_detected && !cmdline.isset("has-recursion")) { - status() << "Recursion not supported" << eom; + status() << "Recursion not supportedwithout --has-recursion option" << eom; report_unknown(); return 5; } @@ -582,8 +590,15 @@ int twols_parse_optionst::doit() std::unique_ptr checker; if(!options.get_bool_option("k-induction") && !options.get_bool_option("incremental-bmc")) - checker=std::unique_ptr( - new summary_checker_ait(options, heap_analysis)); + { + if(options.get_bool_option("has-recursion")) + checker=std::unique_ptr( + new summary_checker_rect(options, heap_analysis)); + else + checker=std::unique_ptr( + new summary_checker_ait(options, heap_analysis)); + + } if(options.get_bool_option("k-induction") && !options.get_bool_option("incremental-bmc")) checker=std::unique_ptr( @@ -1765,6 +1780,7 @@ void twols_parse_optionst::help() " --termination compute ranking functions to prove termination\n" // NOLINT(*) " --k-induction use k-induction\n" " --incremental-bmc use incremental-bmc\n" + " --has-recursion enable recursive function support" " --preconditions compute preconditions\n" " --sufficient sufficient preconditions (default: necessary)\n" // NOLINT(*) " --havoc havoc loops and function calls\n" diff --git a/src/2ls/2ls_parse_options.h b/src/2ls/2ls_parse_options.h index 2199b95d3..2bdf1dc75 100644 --- a/src/2ls/2ls_parse_options.h +++ b/src/2ls/2ls_parse_options.h @@ -65,7 +65,7 @@ class optionst; "(graphml-witness):(json-cex):" \ "(no-spurious-check)(stop-on-fail)" \ "(competition-mode)(slice)(no-propagation)(independent-properties)" \ - "(no-unwinding-assertions)" + "(no-unwinding-assertions)(has-recursion)" // the last line is for CBMC-regression testing only class twols_parse_optionst: diff --git a/src/2ls/Makefile b/src/2ls/Makefile index 5b9362169..c817b5e84 100644 --- a/src/2ls/Makefile +++ b/src/2ls/Makefile @@ -6,6 +6,7 @@ SRC = 2ls_main.cpp 2ls_parse_options.cpp \ 2ls_languages.cpp \ show.cpp summary_checker_base.cpp \ summary_checker_ai.cpp summary_checker_bmc.cpp \ + summary_checker_rect.cpp \ summary_checker_kind.cpp summary_checker_nonterm.cpp \ cover_goals_ext.cpp horn_encoding.cpp \ preprocessing_util.cpp \ diff --git a/src/2ls/summary_checker_base.cpp b/src/2ls/summary_checker_base.cpp index 63aa43f15..548dfbedf 100644 --- a/src/2ls/summary_checker_base.cpp +++ b/src/2ls/summary_checker_base.cpp @@ -7,6 +7,7 @@ Author: Peter Schrammel \*******************************************************************/ #include +#include #include #include @@ -80,6 +81,7 @@ void summary_checker_baset::SSA_functions( // properties initialize_property_map(goto_model.goto_functions); + //CustomSSAOperation(SSA,ns,"");//execute ic3 } /*******************************************************************\ diff --git a/src/2ls/summary_checker_base.h b/src/2ls/summary_checker_base.h index 0d65062ce..6475517be 100644 --- a/src/2ls/summary_checker_base.h +++ b/src/2ls/summary_checker_base.h @@ -84,7 +84,7 @@ class summary_checker_baset:public property_checkert const namespacet &ns, const ssa_heap_analysist &heap_analysis); - void summarize( + virtual void summarize( const goto_modelt &, bool forward=true, bool termination=false); diff --git a/src/2ls/summary_checker_rect.cpp b/src/2ls/summary_checker_rect.cpp new file mode 100644 index 000000000..5e69d0d25 --- /dev/null +++ b/src/2ls/summary_checker_rect.cpp @@ -0,0 +1,108 @@ +/* + * To change this license header, choose License Headers in Project Properties. + * To change this template file, choose Tools | Templates + * and open the template in the editor. + */ + +/* + * File: summary_checker_rect.cpp + * Author: sarbojit + * + * Created on 21 March, 2018, 7:13 PM + */ + +#include +#include +#include +#include +#include + +#include "summary_checker_rect.h" + +property_checkert::resultt summary_checker_rect::operator()( + const goto_modelt &goto_model) +{ + const namespacet ns(goto_model.symbol_table); + + SSA_functions(goto_model, ns, heap_analysis); + + ssa_unwinder.init(false, false); + + unsigned unwind=options.get_unsigned_int_option("unwind"); + if(unwind>0) + { + status() << "Unwinding" << messaget::eom; + + ssa_unwinder.init_localunwinders(); + + ssa_unwinder.unwind_all(unwind); + } + + // properties + initialize_property_map(goto_model.goto_functions); + + bool preconditions=options.get_bool_option("preconditions"); + bool termination=options.get_bool_option("termination"); + bool trivial_domain=options.get_bool_option("havoc"); + if(!trivial_domain || termination) + { + // forward analysis + summarize(goto_model, true, termination); + } + /*if(preconditions) + { + report_statistics(); + report_preconditions(); + return property_checkert::UNKNOWN; + } + + if(termination) + { + report_statistics(); + return report_termination(); + } + +#ifdef SHOW_CALLINGCONTEXTS + if(options.get_bool_option("show-calling-contexts")) + return property_checkert::UNKNOWN; +#endif + + property_checkert::resultt result=check_properties(); + report_statistics(); + return result;*/ + return UNKNOWN; +} + +void summary_checker_rect::summarize( + const goto_modelt &goto_model, + bool forward, + bool termination) +{ + summarizer_baset *summarizer=NULL; +#ifdef SHOW_CALLING_CONTEXTS + if(options.get_bool_option("show-calling-contexts")) + summarizer=new summarizer_fw_contextst( + options, summary_db, ssa_db, ssa_unwinder, ssa_inliner); + else // NOLINT(*) +#endif + { + if(forward && !termination) + summarizer=new summarizer_rec_fwt( + options, summary_db, ssa_db, ssa_unwinder, ssa_inliner); + } + assert(summarizer!=NULL); + summarizer->set_message_handler(get_message_handler()); + if(!options.get_bool_option("context-sensitive") && + options.get_bool_option("all-functions")) + summarizer->summarize(); + else + summarizer->summarize(goto_model.goto_functions.entry_point()); + + // statistics + /*solver_instances+=summarizer->get_number_of_solver_instances(); + solver_calls+=summarizer->get_number_of_solver_calls(); + summaries_used+=summarizer->get_number_of_summaries_used(); + termargs_computed+=summarizer->get_number_of_termargs_computed();*/ + + delete summarizer; +} diff --git a/src/2ls/summary_checker_rect.h b/src/2ls/summary_checker_rect.h new file mode 100644 index 000000000..9e70c52e6 --- /dev/null +++ b/src/2ls/summary_checker_rect.h @@ -0,0 +1,28 @@ +/* + * File: summary_checker_rect.h + * Author: sarbojit + * + * Created on 21 March, 2018, 7:13 PM + */ + +#ifndef SUMMARY_CHECKER_RECT_H +#define SUMMARY_CHECKER_RECT_H + +#include "summary_checker_ai.h" + +class summary_checker_rect:public summary_checker_ait +{ +public: + explicit summary_checker_rect(optionst &_options, + const ssa_heap_analysist &heap_analysis): + summary_checker_ait(_options, heap_analysis) + { + } + + virtual resultt operator()(const goto_modelt &); +protected: + void summarize(const goto_modelt &, bool, bool); +}; + +#endif /* SUMMARY_CHECKER_RECT_H */ + diff --git a/src/domains/Makefile b/src/domains/Makefile index e293aee2f..f25ec032b 100644 --- a/src/domains/Makefile +++ b/src/domains/Makefile @@ -9,6 +9,7 @@ SRC = tpolyhedra_domain.cpp equality_domain.cpp domain.cpp \ strategy_solver_enumeration.cpp strategy_solver_binsearch.cpp \ template_generator_base.cpp template_generator_summary.cpp \ template_generator_callingcontext.cpp template_generator_ranking.cpp \ + template_gen_rec_summary.cpp \ strategy_solver_binsearch2.cpp strategy_solver_binsearch3.cpp \ strategy_solver_predabs.cpp strategy_solver_heap.cpp \ strategy_solver_heap_tpolyhedra.cpp \ diff --git a/src/domains/domain.h b/src/domains/domain.h index 5f8fde816..0f54581f3 100644 --- a/src/domains/domain.h +++ b/src/domains/domain.h @@ -65,6 +65,10 @@ class domaint }; virtual void initialize(valuet &value) { value.basic_value=valuet::BOTTOM; } + virtual void initialize_in_templates(valuet &value, + std::map context_bounds= + std::map()) {assert(false);} + // returns true as long as further refinements are possible virtual void reset_refinements() { } diff --git a/src/domains/ssa_analyzer.cpp b/src/domains/ssa_analyzer.cpp index 72ad03b52..9a5460fad 100644 --- a/src/domains/ssa_analyzer.cpp +++ b/src/domains/ssa_analyzer.cpp @@ -63,7 +63,10 @@ void ssa_analyzert::operator()( incremental_solvert &solver, local_SSAt &SSA, const exprt &precondition, - template_generator_baset &template_generator) + template_generator_baset &template_generator, + bool recursive, + std::map context_bounds, + tmpl_rename_mapt templ_maps) { if(SSA.goto_function.body.instructions.empty()) return; @@ -75,7 +78,10 @@ void ssa_analyzert::operator()( solver << SSA.get_enabling_exprs(); // add precondition (or conjunction of asssertion in backward analysis) - solver << precondition; + if(!template_generator.options.get_bool_option("has-recursion") || + !recursive || + !template_generator.options.get_bool_option("context-sensitive")) + solver << precondition; domain=template_generator.domain(); @@ -174,10 +180,24 @@ void ssa_analyzert::operator()( // initialize inv domain->initialize(*result); + // initialize input arguments and input global variables with calling context + if(recursive && + template_generator.options.get_bool_option("context-sensitive")) + domain->initialize_in_templates(*result, context_bounds); // iterate while(strategy_solver->iterate(*result)) {} + /*if(recursive)//iterate for recursive function + { + assert(template_generator.options.get_bool_option("binsearch-solver")); + //while(strategy_solver->iterate_for_recursive(*result,templ_maps, + //template_generator.options.get_bool_option("context-sensitive"))) {} + while(strategy_solver->iterate(*result)) {}//need to change + } + else//iterate for non-recursive function + while(strategy_solver->iterate(*result)) {}*/ + solver.pop_context(); // statistics diff --git a/src/domains/ssa_analyzer.h b/src/domains/ssa_analyzer.h index 5398e883d..50e4ca098 100644 --- a/src/domains/ssa_analyzer.h +++ b/src/domains/ssa_analyzer.h @@ -22,7 +22,8 @@ class ssa_analyzert:public messaget public: typedef strategy_solver_baset::constraintst constraintst; typedef strategy_solver_baset::var_listt var_listt; - + typedef std::vector>> tmpl_rename_mapt; + ssa_analyzert(): result(NULL), solver_instances(0), @@ -40,7 +41,11 @@ class ssa_analyzert:public messaget incremental_solvert &solver, local_SSAt &SSA, const exprt &precondition, - template_generator_baset &template_generator); + template_generator_baset &template_generator, + bool recursive=false, + std::map context_bounds= + std::map(), + tmpl_rename_mapt templ_maps=tmpl_rename_mapt()); void get_result(exprt &result, const domaint::var_sett &vars); diff --git a/src/domains/strategy_solver_base.h b/src/domains/strategy_solver_base.h index 7915b5ef9..bb77bb485 100644 --- a/src/domains/strategy_solver_base.h +++ b/src/domains/strategy_solver_base.h @@ -31,6 +31,8 @@ class strategy_solver_baset:public messaget {} virtual bool iterate(invariantt &inv) { assert(false); } + /*virtual bool iterate_for_recursive( + invariantt &inv, tmpl_rename_mapt templ_maps,bool cntxt_sensitive) {assert(false);}*/ inline unsigned get_number_of_solver_calls() { return solver_calls; } inline unsigned get_number_of_solver_instances() { return solver_instances; } diff --git a/src/domains/strategy_solver_binsearch.h b/src/domains/strategy_solver_binsearch.h index 8bcdf7f4b..325122955 100644 --- a/src/domains/strategy_solver_binsearch.h +++ b/src/domains/strategy_solver_binsearch.h @@ -25,6 +25,8 @@ class strategy_solver_binsearcht:public strategy_solver_baset } virtual bool iterate(invariantt &inv); + /*virtual bool iterate_for_recursive( + invariantt &inv, tmpl_rename_mapt templ_maps,bool cntxt_sensitive);*/ protected: tpolyhedra_domaint &tpolyhedra_domain; diff --git a/src/domains/template_gen_rec_summary.cpp b/src/domains/template_gen_rec_summary.cpp new file mode 100644 index 000000000..74818cc3e --- /dev/null +++ b/src/domains/template_gen_rec_summary.cpp @@ -0,0 +1,69 @@ +/* + * To change this license header, choose License Headers in Project Properties. + * To change this template file, choose Tools | Templates + * and open the template in the editor. + */ + +/* + * File: template_gen_rec_summary.cpp + * Author: sarbojit + * + * Created on 19 March, 2018, 10:19 PM + */ + +#define SHOW_TEMPLATE +#include "tpolyhedra_domain.h" + +#include "template_gen_rec_summary.h" + +void template_gen_rec_summaryt::operator()(const irep_idt &function_name, + unsigned _domain_number, + const local_SSAt &SSA, tmpl_rename_mapt &templ_maps, + bool forward, bool recursive) +{ + domain_number=_domain_number; + handle_special_functions(SSA); // we have to call that to prevent trouble! + + collect_variables_loop(SSA, forward); + + // do not compute summary for entry-point + if(SSA.goto_function.body.instructions.front().function!=ID__start || + options.get_bool_option("preconditions")) + { + collect_variables_inout(SSA, forward); + } + if(recursive) get_renaming_maps(function_name,SSA,templ_maps); + // either use standard templates or user-supplied ones + if(!instantiate_custom_templates(SSA)) + instantiate_standard_domains(SSA,recursive); + +#ifdef SHOW_TEMPLATE_VARIABLES + debug() << "Template variables: " << eom; + domaint::output_var_specs(debug(), var_specs, SSA.ns); debug() << eom; +#endif +#ifdef SHOW_TEMPLATE + debug() << "Template: " << eom; + domain_ptr->output_domain(debug(), SSA.ns); debug() << eom; +#endif +} + +void template_gen_rec_summaryt::get_renaming_maps(const irep_idt &function_name, + local_SSAt SSA,tmpl_rename_mapt &templ_maps) +{ + for(local_SSAt::nodet node:SSA.nodes) + for(function_application_exprt f_call:node.function_calls) + if(function_name==to_symbol_expr(f_call.function()).get_identifier()) + { + std::pair> p(SSA.guard_symbol(node.location), + std::vector(f_call.arguments())); + std::set globals_in,globals_out; + SSA.get_globals(node.location,globals_in); + for(exprt e:globals_in) {p.second.push_back(e);} + SSA.get_globals(node.location,globals_out,false); + for(exprt e:globals_out) {p.second.push_back(e);} + for(domaint::var_spect s:var_specs) {std::cout<>> tmpl_rename_mapt; + explicit template_gen_rec_summaryt( + optionst &_options, + ssa_dbt &_ssa_db, + ssa_local_unwindert &_ssa_local_unwinder): + template_generator_summaryt(_options, _ssa_db, _ssa_local_unwinder) + { + } + virtual void operator()(const irep_idt &function_name, + unsigned _domain_number, + const local_SSAt &SSA, tmpl_rename_mapt &templ_maps, + bool forward=true, bool recursive=false); + + void get_renaming_maps(const irep_idt &function_name,local_SSAt SSA, + tmpl_rename_mapt &templ_maps); +}; + +#endif /* TEMPLATE_GEN_REC_SUMMARY_H */ + diff --git a/src/domains/template_generator_base.cpp b/src/domains/template_generator_base.cpp index f9a56e7bd..788c84d86 100644 --- a/src/domains/template_generator_base.cpp +++ b/src/domains/template_generator_base.cpp @@ -739,7 +739,7 @@ Function: template_generator_baset::instantiate_standard_domains \*******************************************************************/ void template_generator_baset::instantiate_standard_domains( - const local_SSAt &SSA) + const local_SSAt &SSA, bool recursive) { replace_mapt &renaming_map= std_invariants ? aux_renaming_map : post_renaming_map; @@ -762,7 +762,9 @@ void template_generator_baset::instantiate_standard_domains( new tpolyhedra_domaint(domain_number, renaming_map, SSA.ns); filter_template_domain(); static_cast(domain_ptr) - ->add_interval_template(var_specs, SSA.ns); + ->add_interval_template(var_specs, SSA.ns, + options.get_bool_option("context-sensitive") && + recursive); } else if(options.get_bool_option("zones")) { diff --git a/src/domains/template_generator_base.h b/src/domains/template_generator_base.h index 1c42a6c0c..5668166d8 100644 --- a/src/domains/template_generator_base.h +++ b/src/domains/template_generator_base.h @@ -130,7 +130,7 @@ class template_generator_baset:public messaget exprt &expr); virtual void handle_special_functions(const local_SSAt &SSA); - void instantiate_standard_domains(const local_SSAt &SSA); + void instantiate_standard_domains(const local_SSAt &SSA, bool recursive=false); bool instantiate_custom_templates(const local_SSAt &SSA); void rename_aux_post(symbol_exprt &expr) diff --git a/src/domains/tpolyhedra_domain.cpp b/src/domains/tpolyhedra_domain.cpp index dbbecde6e..03fb38b5c 100644 --- a/src/domains/tpolyhedra_domain.cpp +++ b/src/domains/tpolyhedra_domain.cpp @@ -53,6 +53,31 @@ void tpolyhedra_domaint::initialize(valuet &value) } } +void tpolyhedra_domaint::initialize_in_templates(valuet &value, + std::map context_bounds) +{ + templ_valuet &v=static_cast(value); + v.resize(templ.size()); + for(std::size_t row=0; row context_bounds= + std::map()); virtual void join(valuet &value1, const valuet &value2); @@ -124,7 +127,8 @@ class tpolyhedra_domaint:public domaint void add_interval_template( const var_specst &var_specs, - const namespacet &ns); + const namespacet &ns, + bool rec_cntx_sensitive=false); void add_difference_template( const var_specst &var_specs, const namespacet &ns); diff --git a/src/solver/Makefile b/src/solver/Makefile index bd0fe97b7..ada270d7c 100644 --- a/src/solver/Makefile +++ b/src/solver/Makefile @@ -1,6 +1,7 @@ SRC = summarizer_base.cpp summarizer_bw.cpp \ summarizer_bw_term.cpp summarizer_fw_contexts.cpp \ summarizer_fw.cpp summarizer_fw_term.cpp \ + summarizer_rec_fw.cpp \ summary.cpp summary_db.cpp include ../config.inc diff --git a/src/solver/summarizer_fw.cpp b/src/solver/summarizer_fw.cpp index 27f8dd1da..7d3370084 100644 --- a/src/solver/summarizer_fw.cpp +++ b/src/solver/summarizer_fw.cpp @@ -214,8 +214,9 @@ void summarizer_fwt::inline_summaries( 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)) + if(to_symbol_expr(f_it->function()).get_identifier()==function_name || + !check_call_reachable( + function_name, SSA, n_it, f_it, precondition, true)) { continue; } diff --git a/src/solver/summarizer_fw.h b/src/solver/summarizer_fw.h index 6ee541620..a57f4636f 100644 --- a/src/solver/summarizer_fw.h +++ b/src/solver/summarizer_fw.h @@ -39,7 +39,7 @@ class summarizer_fwt:public summarizer_baset const exprt &precondition, bool context_sensitive); - void inline_summaries( + virtual void inline_summaries( const function_namet &function_name, local_SSAt &SSA, const exprt &precondition, diff --git a/src/solver/summarizer_rec_fw.cpp b/src/solver/summarizer_rec_fw.cpp new file mode 100755 index 000000000..e95029eab --- /dev/null +++ b/src/solver/summarizer_rec_fw.cpp @@ -0,0 +1,202 @@ +/* + * To change this license header, choose License Headers in Project Properties. + * To change this template file, choose Tools | Templates + * and open the template in the editor. + */ + +/* + * File: summarizer_rec_fwt.cpp + * Author: sarbojit + * + * Created on 13 March, 2018, 4:53 PM + */ + +#include +#include +#include +#include "summarizer_rec_fw.h" + +void summarizer_rec_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 + + bool recursive=false; + for(local_SSAt::nodet node:SSA.nodes) + { + for(function_application_exprt f_call:node.function_calls) + if(function_name==to_symbol_expr(f_call.function()).get_identifier()) + recursive=true;//function is recursive + } + if(recursive)//if this_function_is_recursive + { + //inline other non-recursive functions in the same SCC of the call graph + //this makes it self recursive + } + + // recursively compute summaries for non-recursive 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(const auto &node : SSA.nodes) + { + if(!node.empty()) + node.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; + //if(recursive) summary.fw_precondition=true; + summary.fw_precondition=precondition; + + + if(!options.get_bool_option("havoc")) + { + do_summary(function_name, SSA, summary, true_exprt(), context_sensitive,recursive); + } + + #if 0 + 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; + } + #endif + + // store summary in db + //summary_db.put(function_name, summary); + + /*if(!options.get_bool_option("competition-mode")) + { + std::ostringstream out; + out << std::endl << "Summary for function " << function_name << std::endl; + summary_db.get(function_name).output(out, SSA.ns); + status() << out.str() << eom; + }*/ +} + +void summarizer_rec_fwt::do_summary( + const function_namet &function_name, + local_SSAt &SSA, + summaryt &summary, + exprt cond, + bool context_sensitive,bool recursive) +{ + status() << "Computing summary" << eom; + + // solver + incremental_solvert &solver=ssa_db.get_solver(function_name); + solver.set_message_handler(get_message_handler()); + + // analyze + ssa_analyzert analyzer; + analyzer.set_message_handler(get_message_handler()); + + tmpl_rename_mapt templ_maps; + + template_gen_rec_summaryt template_generator( + options, ssa_db, ssa_unwinder.get(function_name)); + template_generator.set_message_handler(get_message_handler()); + template_generator( + function_name,solver.next_domain_number(), SSA, templ_maps, true,recursive); + + exprt::operandst conds; + conds.reserve(5); + conds.push_back(cond); + if(!(recursive && context_sensitive)) conds.push_back(summary.fw_precondition); + conds.push_back(ssa_inliner.get_summaries(SSA)); + +#ifdef REUSE_INVARIANTS + if(summary_db.exists(function_name)) // reuse existing invariants + { + const exprt &old_inv=summary_db.get(function_name).fw_invariant; + exprt inv=ssa_unwinder.get(function_name).rename_invariant(old_inv); + conds.push_back(inv); + +#if 0 + std::ostringstream out; + out << "(original inv)" << from_expr(SSA.ns, "", old_inv) << "\n"; + debug() << out.str() << eom; + out << "(renamed inv)" << from_expr(SSA.ns, "", inv) << "\n"; + debug() << out.str() << eom; +#endif + } +#endif + + cond=conjunction(conds); + + std::map context_bounds; + if(recursive && context_sensitive) + { + context_bounds = get_context_bounds(summary.fw_precondition); + + /*for(std::pair p : context_bounds) + { + debug()< summarizer_rec_fwt::get_context_bounds( + exprt con) +{ + std::map cntxt_bound; + for(exprt op:con.operands()) + { + assert(op.id()==ID_le); + cntxt_bound.insert(std::pair + (op.op0(),to_constant_expr(op.op1()))); + } + return cntxt_bound; +} \ No newline at end of file diff --git a/src/solver/summarizer_rec_fw.h b/src/solver/summarizer_rec_fw.h new file mode 100755 index 000000000..5dd646236 --- /dev/null +++ b/src/solver/summarizer_rec_fw.h @@ -0,0 +1,51 @@ +/* + * To change this license header, choose License Headers in Project Properties. + * To change this template file, choose Tools | Templates + * and open the template in the editor. + */ + +/* + * File: summarizer_rec_fwt.h + * Author: sarbojit + * + * Created on 13 March, 2018, 4:52 PM + */ + +#ifndef SUMMARIZER_REC_FWT_H +#define SUMMARIZER_REC_FWT_H + +#include +#include +#include + +#include +#include +#include +#include + +#include "summarizer_fw.h" + +class summarizer_rec_fwt:public summarizer_fwt { +public: + explicit summarizer_rec_fwt(optionst &_options, + summary_dbt &_summary_db, + ssa_dbt &_ssa_db, + ssa_unwindert &_ssa_unwinder, + ssa_inlinert &_ssa_inliner): + summarizer_fwt( + _options, _summary_db, _ssa_db, _ssa_unwinder, _ssa_inliner) + { + } + typedef std::vector>> tmpl_rename_mapt; +protected: + virtual void compute_summary_rec(const function_namet &, + const exprt &, bool); + + virtual void do_summary(const function_namet &, + local_SSAt &SSA, summaryt &summary, exprt cond, + bool context_sensitive, bool recursive); + std::map get_context_bounds(exprt); +}; + +#endif /* SUMMARIZER_REC_FWT_H */ + From 1c5913c438ad7b46f71e92f6c78f8cedfc225ebf Mon Sep 17 00:00:00 2001 From: Sarbojit Das Date: Wed, 21 Nov 2018 16:44:03 +0530 Subject: [PATCH 4/7] modified: src/2ls/summary_checker_rect.cpp modified: src/2ls/summary_checker_rect.h new file: src/config.inc.bak modified: src/domains/domain.h modified: src/domains/ssa_analyzer.cpp modified: src/domains/ssa_analyzer.h modified: src/domains/strategy_solver_base.h modified: src/domains/strategy_solver_binsearch.cpp modified: src/domains/strategy_solver_binsearch.h modified: src/domains/template_gen_rec_summary.cpp modified: src/domains/template_gen_rec_summary.h modified: src/domains/template_generator_base.cpp modified: src/domains/template_generator_base.h modified: src/domains/tpolyhedra_domain.cpp modified: src/domains/tpolyhedra_domain.h modified: src/solver/summarizer_rec_fw.cpp modified: src/solver/summarizer_rec_fw.h modified: src/ssa/local_ssa.cpp --- src/2ls/summary_checker_rect.cpp | 82 ++++--- src/2ls/summary_checker_rect.h | 14 +- src/config.inc.bak | 10 + src/domains/domain.h | 10 +- src/domains/ssa_analyzer.cpp | 27 +-- src/domains/ssa_analyzer.h | 4 +- src/domains/strategy_solver_base.h | 3 +- src/domains/strategy_solver_binsearch.cpp | 275 ++++++++++++++++++++-- src/domains/strategy_solver_binsearch.h | 4 +- src/domains/template_gen_rec_summary.cpp | 209 ++++++++++++++-- src/domains/template_gen_rec_summary.h | 37 +-- src/domains/template_generator_base.cpp | 8 +- src/domains/template_generator_base.h | 2 +- src/domains/tpolyhedra_domain.cpp | 164 ++++++------- src/domains/tpolyhedra_domain.h | 31 ++- src/solver/summarizer_rec_fw.cpp | 208 ++++++++-------- src/solver/summarizer_rec_fw.h | 2 - src/ssa/local_ssa.cpp | 16 +- 18 files changed, 767 insertions(+), 339 deletions(-) create mode 100644 src/config.inc.bak diff --git a/src/2ls/summary_checker_rect.cpp b/src/2ls/summary_checker_rect.cpp index 5e69d0d25..5877a524c 100644 --- a/src/2ls/summary_checker_rect.cpp +++ b/src/2ls/summary_checker_rect.cpp @@ -22,7 +22,7 @@ property_checkert::resultt summary_checker_rect::operator()( const goto_modelt &goto_model) { - const namespacet ns(goto_model.symbol_table); + const namespacet ns(goto_model.symbol_table); SSA_functions(goto_model, ns, heap_analysis); @@ -41,35 +41,56 @@ property_checkert::resultt summary_checker_rect::operator()( // properties initialize_property_map(goto_model.goto_functions); - bool preconditions=options.get_bool_option("preconditions"); - bool termination=options.get_bool_option("termination"); - bool trivial_domain=options.get_bool_option("havoc"); - if(!trivial_domain || termination) - { - // forward analysis - summarize(goto_model, true, termination); - } - /*if(preconditions) - { - report_statistics(); - report_preconditions(); - return property_checkert::UNKNOWN; - } - - if(termination) - { - report_statistics(); - return report_termination(); - } + /*property_checkert::resultt result=property_checkert::UNKNOWN; + bool finished=false; + while(!finished) + {*/ + bool preconditions=options.get_bool_option("preconditions"); + bool termination=options.get_bool_option("termination"); + bool trivial_domain=options.get_bool_option("havoc"); + if(!trivial_domain || termination) + { + // forward analysis + summarize(goto_model, true, termination); + } + if(!trivial_domain && preconditions) + { + status()<<"No backward analysis supported for recursive programs."<set_message_handler(get_message_handler()); @@ -99,10 +123,10 @@ void summary_checker_rect::summarize( summarizer->summarize(goto_model.goto_functions.entry_point()); // statistics - /*solver_instances+=summarizer->get_number_of_solver_instances(); + solver_instances+=summarizer->get_number_of_solver_instances(); solver_calls+=summarizer->get_number_of_solver_calls(); summaries_used+=summarizer->get_number_of_summaries_used(); - termargs_computed+=summarizer->get_number_of_termargs_computed();*/ + termargs_computed+=summarizer->get_number_of_termargs_computed(); delete summarizer; } diff --git a/src/2ls/summary_checker_rect.h b/src/2ls/summary_checker_rect.h index 9e70c52e6..41e0a017b 100644 --- a/src/2ls/summary_checker_rect.h +++ b/src/2ls/summary_checker_rect.h @@ -13,15 +13,15 @@ class summary_checker_rect:public summary_checker_ait { public: - explicit summary_checker_rect(optionst &_options, - const ssa_heap_analysist &heap_analysis): - summary_checker_ait(_options, heap_analysis) - { - } + explicit summary_checker_rect(optionst &_options, + const ssa_heap_analysist &heap_analysis): + summary_checker_ait(_options, heap_analysis) + { + } - virtual resultt operator()(const goto_modelt &); + virtual resultt operator()(const goto_modelt &); protected: - void summarize(const goto_modelt &, bool, bool); + void summarize(const goto_modelt &, bool, bool); }; #endif /* SUMMARY_CHECKER_RECT_H */ diff --git a/src/config.inc.bak b/src/config.inc.bak new file mode 100644 index 000000000..002688fa8 --- /dev/null +++ b/src/config.inc.bak @@ -0,0 +1,10 @@ +CBMC = ~/my-cbmc + +# Variables you may want to override +#CXXFLAGS = -Wall -O0 -g -Werror -Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing -pedantic + +#static compilation +#LINKFLAGS += -static-libgcc -static-libstdc++ + +#2LS switches +TWOLS_FLAGS = diff --git a/src/domains/domain.h b/src/domains/domain.h index 0f54581f3..646148442 100644 --- a/src/domains/domain.h +++ b/src/domains/domain.h @@ -24,11 +24,13 @@ class domaint domaint( unsigned _domain_number, replace_mapt &_renaming_map, - const namespacet &_ns): + const namespacet &_ns, + bool rec=false): domain_number(_domain_number), renaming_map(_renaming_map), ns(_ns) { + recursive=rec; } virtual ~domaint() @@ -65,10 +67,6 @@ class domaint }; virtual void initialize(valuet &value) { value.basic_value=valuet::BOTTOM; } - virtual void initialize_in_templates(valuet &value, - std::map context_bounds= - std::map()) {assert(false);} - // returns true as long as further refinements are possible virtual void reset_refinements() { } @@ -124,6 +122,8 @@ class domaint unsigned domain_number; // serves as id for variables names replace_mapt &renaming_map; const namespacet &ns; + + bool recursive;//sarbojit inline void rename(exprt &expr) { diff --git a/src/domains/ssa_analyzer.cpp b/src/domains/ssa_analyzer.cpp index 9a5460fad..094aee7c1 100644 --- a/src/domains/ssa_analyzer.cpp +++ b/src/domains/ssa_analyzer.cpp @@ -65,8 +65,7 @@ void ssa_analyzert::operator()( const exprt &precondition, template_generator_baset &template_generator, bool recursive, - std::map context_bounds, - tmpl_rename_mapt templ_maps) + const exprt &merge_expr) { if(SSA.goto_function.body.instructions.empty()) return; @@ -76,12 +75,11 @@ void ssa_analyzert::operator()( solver.new_context(); solver << SSA.get_enabling_exprs(); + + if(recursive) solver<initialize(*result); + // initialize input arguments and input global variables with calling context if(recursive && template_generator.options.get_bool_option("context-sensitive")) - domain->initialize_in_templates(*result, context_bounds); + { + //while(strategy_solver->iterate_for_ins(*result)) {} + } + status()<<"------------------------------------------------------------------\n"/////////////////////////// + "-------------------------------------------------------------------\n"<iterate(*result)) {} - /*if(recursive)//iterate for recursive function - { - assert(template_generator.options.get_bool_option("binsearch-solver")); - //while(strategy_solver->iterate_for_recursive(*result,templ_maps, - //template_generator.options.get_bool_option("context-sensitive"))) {} - while(strategy_solver->iterate(*result)) {}//need to change - } - else//iterate for non-recursive function - while(strategy_solver->iterate(*result)) {}*/ - solver.pop_context(); // statistics diff --git a/src/domains/ssa_analyzer.h b/src/domains/ssa_analyzer.h index 50e4ca098..3c6e69f22 100644 --- a/src/domains/ssa_analyzer.h +++ b/src/domains/ssa_analyzer.h @@ -43,9 +43,7 @@ class ssa_analyzert:public messaget const exprt &precondition, template_generator_baset &template_generator, bool recursive=false, - std::map context_bounds= - std::map(), - tmpl_rename_mapt templ_maps=tmpl_rename_mapt()); + const exprt &merge_expr=true_exprt()); void get_result(exprt &result, const domaint::var_sett &vars); diff --git a/src/domains/strategy_solver_base.h b/src/domains/strategy_solver_base.h index bb77bb485..29cd9823a 100644 --- a/src/domains/strategy_solver_base.h +++ b/src/domains/strategy_solver_base.h @@ -31,8 +31,7 @@ class strategy_solver_baset:public messaget {} virtual bool iterate(invariantt &inv) { assert(false); } - /*virtual bool iterate_for_recursive( - invariantt &inv, tmpl_rename_mapt templ_maps,bool cntxt_sensitive) {assert(false);}*/ + virtual bool iterate_for_ins(invariantt &inv) { assert(false); } inline unsigned get_number_of_solver_calls() { return solver_calls; } inline unsigned get_number_of_solver_instances() { return solver_instances; } diff --git a/src/domains/strategy_solver_binsearch.cpp b/src/domains/strategy_solver_binsearch.cpp index 398d66ddd..5c0b7db5c 100644 --- a/src/domains/strategy_solver_binsearch.cpp +++ b/src/domains/strategy_solver_binsearch.cpp @@ -36,10 +36,10 @@ bool strategy_solver_binsearcht::iterate(invariantt &_inv) exprt inv_expr=tpolyhedra_domain.to_pre_constraints(inv); -#if 0 +//#if 0 debug() << "improvement check: " << eom; debug() << "pre-inv: " << from_expr(ns, "", inv_expr) << eom; -#endif +//#endif solver << inv_expr; @@ -49,33 +49,33 @@ bool strategy_solver_binsearcht::iterate(invariantt &_inv) strategy_cond_literals.resize(strategy_cond_exprs.size()); -#if 0 +//#if 0 debug() << "post-inv: "; -#endif +//#endif for(std::size_t i=0; i0 ? " || " : "") << from_expr(ns, "", strategy_cond_exprs[i]); -#endif +//#endif strategy_cond_literals[i]=solver.convert(strategy_cond_exprs[i]); // solver.set_frozen(strategy_cond_literals[i]); strategy_cond_exprs[i]=literal_exprt(strategy_cond_literals[i]); } -#if 0 +//#if 0 debug() << eom; -#endif +//#endif solver << disjunction(strategy_cond_exprs); -#if 0 +//#if 0 debug() << "solve(): "; -#endif +//#endif if(solver()==decision_proceduret::D_SATISFIABLE) // improvement check { -#if 0 +//#if 0 debug() << "SAT" << eom; -#endif +//#endif #if 0 for(std::size_t i=0; i(_inv); + + bool improved=false; + + solver.new_context(); // for improvement check + + exprt inv_expr=tpolyhedra_domain.to_pre_constraints(inv,true); + +//#if 0 + debug() << "improvement check: " << eom; + debug() << "pre-inv: " << from_expr(ns, "", inv_expr) << eom; +//#endif + + solver << inv_expr; + + exprt::operandst strategy_cond_exprs; + tpolyhedra_domain.make_not_post_constraints( + inv, strategy_cond_exprs, strategy_value_exprs,true); + + strategy_cond_literals.resize(strategy_cond_exprs.size()); + +//#if 0 + debug() << "post-inv: "; +//#endif + + for(std::size_t i=0; i0 ? " || " : "") << from_expr(ns, "", strategy_cond_exprs[i]); +//#endif + strategy_cond_literals[i]=solver.convert(strategy_cond_exprs[i]); + // solver.set_frozen(strategy_cond_literals[i]); + strategy_cond_exprs[i]=literal_exprt(strategy_cond_literals[i]); + } +//#if 0 + debug() << eom; +//#endif + + solver << disjunction(strategy_cond_exprs); + +//#if 0 + debug() << "solve(): "; +//#endif + + if(solver()==decision_proceduret::D_SATISFIABLE) // improvement check + { +//#if 0 + debug() << "SAT" << eom; +//#endif + +#if 0 + for(std::size_t i=0; i improve_rows; + improve_rows.insert(row); + + tpolyhedra_domaint::row_valuet upper= + tpolyhedra_domain.get_max_row_value(row); + tpolyhedra_domaint::row_valuet lower= + simplify_const(solver.get(strategy_value_exprs[row])); + + solver.pop_context(); // improvement check + + solver.new_context(); // symbolic value system + + exprt pre_inv_expr= + tpolyhedra_domain.to_symb_pre_constraints(inv, improve_rows, true); + + solver << pre_inv_expr; + + exprt post_inv_expr=tpolyhedra_domain.get_row_symb_post_constraint(row); + + solver << post_inv_expr; + +//#if 0 + debug() << "symbolic value system: " << eom; + debug() << "pre-inv: " << from_expr(ns, "", pre_inv_expr) << eom; + debug() << "post-inv: " << from_expr(ns, "", post_inv_expr) << eom; +//s#endif + + while(tpolyhedra_domain.less_than(lower, upper)) + { + tpolyhedra_domaint::row_valuet middle= + tpolyhedra_domain.between(lower, upper); + if(!tpolyhedra_domain.less_than(lower, middle)) + middle=upper; + + // row_symb_value >= middle + exprt c= + tpolyhedra_domain.get_row_symb_value_constraint(row, middle, true); + +//#if 0 + debug() << "upper: " << from_expr(ns, "", upper) << eom; + debug() << "middle: " << from_expr(ns, "", middle) << eom; + debug() << "lower: " << from_expr(ns, "", lower) << eom; +//#endif + + solver.new_context(); // binary search iteration + +//#if 0 + debug() << "constraint: " << from_expr(ns, "", c) << eom; +//#endif + + solver << c; + + if(solver()==decision_proceduret::D_SATISFIABLE) + { +//#if 0 + debug() << "SAT" << eom; +//#endif + +#if 0 + for(std::size_t i=0; iis_in_conflict(solver.formula[i])) + debug() << "is_in_conflict: " << solver.formula[i] << eom; + else + debug() << "not_in_conflict: " << solver.formula[i] << eom; + } +#endif + + if(!tpolyhedra_domain.less_than(middle, upper)) + middle=lower; + upper=middle; + } + solver.pop_context(); // binary search iteration + } + + debug() << "update value: " << from_expr(ns, "", lower) << eom; + + solver.pop_context(); // symbolic value system + + tpolyhedra_domain.set_row_value(row, lower, inv); + improved=true; + } + else + { +//#if 0 + debug() << "UNSAT" << eom; +//#endif + +#ifdef DEBUG_FORMULA + for(std::size_t i=0; iis_in_conflict(solver.formula[i])) + debug() << "is_in_conflict: " << solver.formula[i] << eom; + else + debug() << "not_in_conflict: " << solver.formula[i] << eom; + } +#endif + + solver.pop_context(); // improvement check + } + + return improved; +} \ No newline at end of file diff --git a/src/domains/strategy_solver_binsearch.h b/src/domains/strategy_solver_binsearch.h index 325122955..e0783cfc2 100644 --- a/src/domains/strategy_solver_binsearch.h +++ b/src/domains/strategy_solver_binsearch.h @@ -25,9 +25,7 @@ class strategy_solver_binsearcht:public strategy_solver_baset } virtual bool iterate(invariantt &inv); - /*virtual bool iterate_for_recursive( - invariantt &inv, tmpl_rename_mapt templ_maps,bool cntxt_sensitive);*/ - + virtual bool iterate_for_ins(invariantt &inv); protected: tpolyhedra_domaint &tpolyhedra_domain; }; diff --git a/src/domains/template_gen_rec_summary.cpp b/src/domains/template_gen_rec_summary.cpp index 74818cc3e..1032bfcaa 100644 --- a/src/domains/template_gen_rec_summary.cpp +++ b/src/domains/template_gen_rec_summary.cpp @@ -18,24 +18,30 @@ void template_gen_rec_summaryt::operator()(const irep_idt &function_name, unsigned _domain_number, - const local_SSAt &SSA, tmpl_rename_mapt &templ_maps, - bool forward, bool recursive) + const local_SSAt &SSA, + exprt &merge_expr, + bool forward) { domain_number=_domain_number; handle_special_functions(SSA); // we have to call that to prevent trouble! collect_variables_loop(SSA, forward); + merge_vars(function_name, SSA, merge_expr); // do not compute summary for entry-point if(SSA.goto_function.body.instructions.front().function!=ID__start || options.get_bool_option("preconditions")) { - collect_variables_inout(SSA, forward); + collect_inout_vars(SSA, forward); + } + + if(options.get_bool_option("context-sensitive")) + { + instantiate_template_for_rec(SSA); } - if(recursive) get_renaming_maps(function_name,SSA,templ_maps); // either use standard templates or user-supplied ones - if(!instantiate_custom_templates(SSA)) - instantiate_standard_domains(SSA,recursive); + else if(!instantiate_custom_templates(SSA)) + instantiate_standard_domains(SSA); #ifdef SHOW_TEMPLATE_VARIABLES debug() << "Template variables: " << eom; @@ -43,27 +49,186 @@ void template_gen_rec_summaryt::operator()(const irep_idt &function_name, #endif #ifdef SHOW_TEMPLATE debug() << "Template: " << eom; - domain_ptr->output_domain(debug(), SSA.ns); debug() << eom; + domain_ptr->output_domain(debug(), SSA.ns); + debug()<<"Where:\n"; + for(const exprt& op:merge_expr.operands()) + { + debug()<<" "< globals_in,globals_out; + exprt guard=SSA.guard_symbol(node.location); + std::vector::iterator e_it=expr_vec.begin(); + if(function_name==to_symbol_expr(f_call.function()).get_identifier()&& + f_call.function().id()==ID_symbol) { - std::pair> p(SSA.guard_symbol(node.location), - std::vector(f_call.arguments())); - std::set globals_in,globals_out; - SSA.get_globals(node.location,globals_in); - for(exprt e:globals_in) {p.second.push_back(e);} + guards_vec.push_back(guard); + if(options.get_bool_option("context-sensitive")) + { + for(const exprt &arg:f_call.arguments())//merging arguments + { + exprt& expr=*e_it; + expr=if_exprt(guard,arg,expr); + e_it++; + } + } + SSA.get_globals(node.location,globals_in,true,false); + for(exprt g_in:globals_in) + { + exprt& expr=*e_it; + expr=if_exprt(guard,g_in,expr); + e_it++; + } SSA.get_globals(node.location,globals_out,false); - for(exprt e:globals_out) {p.second.push_back(e);} - for(domaint::var_spect s:var_specs) {std::cout< exp_vec; + guard_ins=symbol_exprt("guard#ins",bool_typet()); + for(const exprt& var:SSA.params) + { + std::string var_name= + id2string(to_symbol_expr(var).get_identifier()); + irep_idt name(var_name+"#rb"),name1(var_name+"#init"); + symbol_exprt var_rb(name,var.type()),var_init(name1,var.type()); + rb_vars.push_back(var_rb); + init_vars_map[var]=var_init; + exprt rhs=if_exprt(guard_ins,var_rb,var_init); + exp_vec.push_back(equal_exprt(var,rhs)); + } + unsigned size=SSA.params.size()+SSA.globals_in.size(),n=size; + for(unsigned i=0;i::const_iterator v_it=rb_vars.begin(); + local_SSAt::var_sett::const_iterator out=SSA.globals_out.begin(); + for(domaint::var_spect var_spec:var_specs) + { + if(var_spec.kind==domaint::OUT) + { + post_renaming_map[var_spec.var]=*out; + out++; + } + else + { + post_renaming_map[var_spec.var]=*v_it; + post_renaming_map[*v_it]=var_spec.var; + v_it++; + } + } + for(domaint::var_spect var_spec:var_specs) + { + if(var_spec.kind==domaint::OUT) break; + var_spec.pre_guard=and_exprt(first_guard,guard_ins); + var_spec.post_guard=merge_guard; + var_spec.var=post_renaming_map[var_spec.var]; + var_specs_no_out.push_back(var_spec); + } +} + +void template_gen_rec_summaryt::instantiate_template_for_rec(local_SSAt SSA) +{ + replace_mapt &renaming_map= + std_invariants ? aux_renaming_map : post_renaming_map; + domain_ptr= + new tpolyhedra_domaint(domain_number, renaming_map, SSA.ns,true); + filter_template_domain(); + + //IN templates + static_cast(domain_ptr) + ->add_interval_template(var_specs_no_out, SSA.ns, + options.get_bool_option("context-sensitive")); + static_cast(domain_ptr) + ->add_sum_template(var_specs_no_out, SSA.ns, false); + static_cast(domain_ptr) + ->add_difference_template(var_specs_no_out, SSA.ns, false); + //OUT templates + static_cast(domain_ptr) + ->add_sum_template(var_specs, SSA.ns); + static_cast(domain_ptr) + ->add_difference_template(var_specs, SSA.ns); } \ No newline at end of file diff --git a/src/domains/template_gen_rec_summary.h b/src/domains/template_gen_rec_summary.h index f4c46132b..3e845dcf7 100644 --- a/src/domains/template_gen_rec_summary.h +++ b/src/domains/template_gen_rec_summary.h @@ -18,21 +18,30 @@ class template_gen_rec_summaryt:public template_generator_summaryt { public: - typedef std::vector>> tmpl_rename_mapt; - explicit template_gen_rec_summaryt( - optionst &_options, - ssa_dbt &_ssa_db, - ssa_local_unwindert &_ssa_local_unwinder): - template_generator_summaryt(_options, _ssa_db, _ssa_local_unwinder) - { - } - virtual void operator()(const irep_idt &function_name, - unsigned _domain_number, - const local_SSAt &SSA, tmpl_rename_mapt &templ_maps, - bool forward=true, bool recursive=false); + typedef std::vector>> tmpl_rename_mapt; + explicit template_gen_rec_summaryt( + optionst &_options, + ssa_dbt &_ssa_db, + ssa_local_unwindert &_ssa_local_unwinder): + template_generator_summaryt(_options, _ssa_db, _ssa_local_unwinder) + { + } + virtual void operator()(const irep_idt &function_name, + unsigned _domain_number, + const local_SSAt &SSA, + exprt &merge_exprt, + bool forward=true); - void get_renaming_maps(const irep_idt &function_name,local_SSAt SSA, - tmpl_rename_mapt &templ_maps); + void merge_vars(const irep_idt &function_name, + const local_SSAt &SSA, + exprt& merge_expr); + void collect_inout_vars(const local_SSAt &SSA, bool forward); + void instantiate_template_for_rec(local_SSAt SSA); + replace_mapt init_vars_map; + domaint::var_specst var_specs_no_out; + private: + exprt merge_guard,guard_ins; + std::vector in_vars_vec,out_vars_vec,rb_vars; }; #endif /* TEMPLATE_GEN_REC_SUMMARY_H */ diff --git a/src/domains/template_generator_base.cpp b/src/domains/template_generator_base.cpp index 788c84d86..628edeefe 100644 --- a/src/domains/template_generator_base.cpp +++ b/src/domains/template_generator_base.cpp @@ -150,7 +150,7 @@ void template_generator_baset::collect_variables_loop( bool forward) { // used for renaming map - var_listt pre_state_vars, post_state_vars; + //var_listt pre_state_vars, post_state_vars; // add loop variables for(local_SSAt::nodest::const_iterator n_it=SSA.nodes.begin(); @@ -739,7 +739,7 @@ Function: template_generator_baset::instantiate_standard_domains \*******************************************************************/ void template_generator_baset::instantiate_standard_domains( - const local_SSAt &SSA, bool recursive) + const local_SSAt &SSA) { replace_mapt &renaming_map= std_invariants ? aux_renaming_map : post_renaming_map; @@ -762,9 +762,7 @@ void template_generator_baset::instantiate_standard_domains( new tpolyhedra_domaint(domain_number, renaming_map, SSA.ns); filter_template_domain(); static_cast(domain_ptr) - ->add_interval_template(var_specs, SSA.ns, - options.get_bool_option("context-sensitive") && - recursive); + ->add_interval_template(var_specs, SSA.ns); } else if(options.get_bool_option("zones")) { diff --git a/src/domains/template_generator_base.h b/src/domains/template_generator_base.h index 5668166d8..1c42a6c0c 100644 --- a/src/domains/template_generator_base.h +++ b/src/domains/template_generator_base.h @@ -130,7 +130,7 @@ class template_generator_baset:public messaget exprt &expr); virtual void handle_special_functions(const local_SSAt &SSA); - void instantiate_standard_domains(const local_SSAt &SSA, bool recursive=false); + void instantiate_standard_domains(const local_SSAt &SSA); bool instantiate_custom_templates(const local_SSAt &SSA); void rename_aux_post(symbol_exprt &expr) diff --git a/src/domains/tpolyhedra_domain.cpp b/src/domains/tpolyhedra_domain.cpp index 03fb38b5c..6c2d7d080 100644 --- a/src/domains/tpolyhedra_domain.cpp +++ b/src/domains/tpolyhedra_domain.cpp @@ -46,38 +46,13 @@ void tpolyhedra_domaint::initialize(valuet &value) v.resize(templ.size()); for(std::size_t row=0; row context_bounds) -{ - templ_valuet &v=static_cast(value); - v.resize(templ.size()); - for(std::size_t row=0; row loop15 regression binary_relation_exprt(templ_row.expr, ID_le, get_row_symb_value(row))); + //if((templ_row.kind==OUT || templ_row.kind==OUTL) && recursive) + // rename(c); + return c; } /*******************************************************************\ @@ -514,16 +502,17 @@ exprt tpolyhedra_domaint::get_row_symb_pre_constraint( \*******************************************************************/ -exprt tpolyhedra_domaint::get_row_symb_post_constraint(const rowt &row) +exprt tpolyhedra_domaint::get_row_symb_post_constraint(const rowt &row)// { assert(row &symb_rows) + const std::set &symb_rows, + bool no_out) { assert(value.size()==templ.size()); exprt::operandst c; @@ -573,7 +563,7 @@ exprt tpolyhedra_domaint::to_symb_pre_constraints( if(symb_rows.find(row)!=symb_rows.end()) c.push_back(get_row_symb_pre_constraint(row, value[row])); else - c.push_back(get_row_pre_constraint(row, value[row])); + c.push_back(get_row_pre_constraint(row, value[row], no_out)); } return conjunction(c); } @@ -590,7 +580,7 @@ exprt tpolyhedra_domaint::to_symb_pre_constraints( \*******************************************************************/ -exprt tpolyhedra_domaint::to_symb_post_constraints( +/*exprt tpolyhedra_domaint::to_symb_post_constraints( const std::set &symb_rows) { exprt::operandst c; @@ -599,7 +589,7 @@ exprt tpolyhedra_domaint::to_symb_post_constraints( c.push_back(get_row_symb_post_constraint(row)); } return conjunction(c); -} +}*/ /*******************************************************************\ @@ -613,7 +603,7 @@ exprt tpolyhedra_domaint::to_symb_post_constraints( \*******************************************************************/ -exprt tpolyhedra_domaint::get_row_symb_value_constraint( +exprt tpolyhedra_domaint::get_row_symb_value_constraint(// const rowt &row, const row_valuet &row_value, bool geq) @@ -709,7 +699,7 @@ void tpolyhedra_domaint::project_on_vars( templ_row.pre_guard, binary_relation_exprt(templ_row.expr, ID_le, row_v))); } - else + else if(templ_row.kind!=IN)//sarbojit { if(is_row_value_neginf(row_v)) c.push_back(false_exprt()); @@ -873,25 +863,39 @@ void tpolyhedra_domaint::output_domain( for(std::size_t row=0; row " - << std::endl << " "; - break; - case IN: - out << "(IN) "; - out << from_expr(ns, "", templ_row.pre_guard) << "===> " - << std::endl << " "; - break; - case OUT: case OUTL: - out << "(OUT) "; - out << from_expr(ns, "", templ_row.post_guard) << "===> " - << std::endl << " "; - break; - default: assert(false); + if(templ_row.kind==IN) out << "(IN"; + if(templ_row.kind==OUT) out << "(OUT"; + if(templ_row.kind==LOOP) out << "(LOOP"; + out << ") [ " << from_expr(ns, "", templ_row.pre_guard) << " | "; + out << from_expr(ns, "", templ_row.post_guard) << " ]===> "; + out << std::endl << " "; + } + //---sarbojit + else//sarbojit + { + switch(templ_row.kind) + { + case LOOP: + out << "(LOOP) [ " << from_expr(ns, "", templ_row.pre_guard) << " | "; + out << from_expr(ns, "", templ_row.post_guard) << " | "; + out << from_expr(ns, "", templ_row.aux_expr) << " ]===> " + << std::endl << " "; + break; + case IN: + out << "(IN) "; + out << from_expr(ns, "", templ_row.pre_guard) << "===> " + << std::endl << " "; + break; + case OUT: case OUTL: + out << "(OUT) "; + out << from_expr(ns, "", templ_row.post_guard) << "===> " + << std::endl << " "; + break; + default: assert(false); + } } out << "( " << from_expr(ns, "", templ_row.expr) << "<=CONST )" << std::endl; @@ -1070,7 +1074,8 @@ void tpolyhedra_domaint::add_interval_template( void tpolyhedra_domaint::add_difference_template( const var_specst &var_specs, - const namespacet &ns) + const namespacet &ns, + bool no_in) { std::size_t size=var_specs.size()*(var_specs.size()-1); templ.reserve(templ.size()+size); @@ -1085,7 +1090,7 @@ void tpolyhedra_domaint::add_difference_template( for(; v2!=var_specs.end(); ++v2) { kindt k=domaint::merge_kinds(v1->kind, v2->kind); - if(k==IN) + if(k==IN&&no_in) continue; if(k==LOOP && v1->pre_guard!=v2->pre_guard) continue; // TEST: we need better heuristics @@ -1166,7 +1171,8 @@ Function: tpolyhedra_domaint::add_sum_template void tpolyhedra_domaint::add_sum_template( const var_specst &var_specs, - const namespacet &ns) + const namespacet &ns, + bool no_in) { unsigned size=var_specs.size()*(var_specs.size()-1); templ.reserve(templ.size()+size); @@ -1178,7 +1184,7 @@ void tpolyhedra_domaint::add_sum_template( for(; v2!=var_specs.end(); ++v2) { kindt k=domaint::merge_kinds(v1->kind, v2->kind); - if(k==IN) + if(k==IN&&no_in) continue; if(k==LOOP && v1->pre_guard!=v2->pre_guard) continue; // TEST: we need better heuristics @@ -1244,4 +1250,4 @@ void tpolyhedra_domaint::eliminate_sympaths( ? true_exprt() : static_cast(not_exprt(disjunction(paths))); } -} +} \ No newline at end of file diff --git a/src/domains/tpolyhedra_domain.h b/src/domains/tpolyhedra_domain.h index 47fae0825..818dee437 100644 --- a/src/domains/tpolyhedra_domain.h +++ b/src/domains/tpolyhedra_domain.h @@ -43,37 +43,40 @@ class tpolyhedra_domaint:public domaint tpolyhedra_domaint( unsigned _domain_number, replace_mapt &_renaming_map, - const namespacet &_ns): - domaint(_domain_number, _renaming_map, _ns) + const namespacet &_ns, + bool rec=false): + domaint(_domain_number, _renaming_map, _ns, rec) { } // initialize value virtual void initialize(valuet &value); - virtual void initialize_in_templates(valuet &value, - std::map context_bounds= - std::map()); virtual void join(valuet &value1, const valuet &value2); // value -> constraints exprt get_row_constraint(const rowt &row, const row_valuet &row_value); - exprt get_row_pre_constraint(const rowt &row, const row_valuet &row_value); - exprt get_row_post_constraint(const rowt &row, const row_valuet &row_value); + exprt get_row_pre_constraint(const rowt &row, const row_valuet &row_value, + bool no_out=false); + exprt get_row_post_constraint(const rowt &row, const row_valuet &row_value, + bool no_out=false); exprt get_row_pre_constraint(const rowt &row, const templ_valuet &value); - exprt get_row_post_constraint(const rowt &row, const templ_valuet &value); + exprt get_row_post_constraint(const rowt &row, const templ_valuet &value, + bool no_out=false); - exprt to_pre_constraints(const templ_valuet &value); + exprt to_pre_constraints(const templ_valuet &value,bool no_out=false); void make_not_post_constraints( const templ_valuet &value, exprt::operandst &cond_exprs, - exprt::operandst &value_exprs); + exprt::operandst &value_exprs, + bool no_out=false); // value -> symbolic bound constraints (for optimization) exprt to_symb_pre_constraints(const templ_valuet &value); exprt to_symb_pre_constraints( const templ_valuet &value, - const std::set &symb_rows); + const std::set &symb_rows, + bool no_out=false); exprt to_symb_post_constraints(const std::set &symb_rows); exprt get_row_symb_value_constraint( const rowt &row, @@ -131,10 +134,12 @@ class tpolyhedra_domaint:public domaint bool rec_cntx_sensitive=false); void add_difference_template( const var_specst &var_specs, - const namespacet &ns); + const namespacet &ns, + bool no_in=true); void add_sum_template( const var_specst &var_specs, - const namespacet &ns); + const namespacet &ns, + bool no_in=true); void add_quadratic_template( const var_specst &var_specs, const namespacet &ns); diff --git a/src/solver/summarizer_rec_fw.cpp b/src/solver/summarizer_rec_fw.cpp index 200727ed3..4157908b8 100755 --- a/src/solver/summarizer_rec_fw.cpp +++ b/src/solver/summarizer_rec_fw.cpp @@ -21,75 +21,77 @@ void summarizer_rec_fwt::compute_summary_rec( const exprt &precondition, bool context_sensitive) { - local_SSAt &SSA=ssa_db.get(function_name);// TODO: make const + local_SSAt &SSA=ssa_db.get(function_name);// TODO: make const - bool recursive=false; - for(local_SSAt::nodet node:SSA.nodes) - { - for(function_application_exprt f_call:node.function_calls) - if(function_name==to_symbol_expr(f_call.function()).get_identifier()) - recursive=true; - } - if(recursive)//if this_function_is_recursive - { - //inline other non-recursive functions in the same SCC of the call graph - //this makes it self recursive - } - - // recursively compute summaries for non-recursive 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(const auto &node : SSA.nodes) - { - if(!node.empty()) - node.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; - //if(recursive) summary.fw_precondition=true; - summary.fw_precondition=precondition; + bool recursive=false; + for(local_SSAt::nodet node:SSA.nodes) + { + for(function_application_exprt f_call:node.function_calls) + if(function_name==to_symbol_expr(f_call.function()).get_identifier() && + f_call.function().id()==ID_symbol)//No function pointer + recursive=true; + } + if(recursive)//if this_function_is_recursive + { + status()<<"Function "< context_bounds; - if(recursive && context_sensitive) - { - context_bounds = get_context_bounds(summary.fw_precondition); - - /*for(std::pair p : context_bounds) - { - debug()< summarizer_rec_fwt::get_context_bounds( - exprt con) -{ - std::map cntxt_bound; - for(exprt op:con.operands()) - { - assert(op.id()==ID_le); - cntxt_bound.insert(std::pair - (op.op0(),to_constant_expr(op.op1()))); - } - return cntxt_bound; -} \ No newline at end of file diff --git a/src/solver/summarizer_rec_fw.h b/src/solver/summarizer_rec_fw.h index 5dd646236..df335de87 100755 --- a/src/solver/summarizer_rec_fw.h +++ b/src/solver/summarizer_rec_fw.h @@ -36,7 +36,6 @@ class summarizer_rec_fwt:public summarizer_fwt { _options, _summary_db, _ssa_db, _ssa_unwinder, _ssa_inliner) { } - typedef std::vector>> tmpl_rename_mapt; protected: virtual void compute_summary_rec(const function_namet &, const exprt &, bool); @@ -44,7 +43,6 @@ class summarizer_rec_fwt:public summarizer_fwt { virtual void do_summary(const function_namet &, local_SSAt &SSA, summaryt &summary, exprt cond, bool context_sensitive, bool recursive); - std::map get_context_bounds(exprt); }; #endif /* SUMMARIZER_REC_FWT_H */ diff --git a/src/ssa/local_ssa.cpp b/src/ssa/local_ssa.cpp index 6ca775df8..e0d106440 100644 --- a/src/ssa/local_ssa.cpp +++ b/src/ssa/local_ssa.cpp @@ -578,16 +578,12 @@ void local_SSAt::build_function_call(locationt loc) unsigned i=0; for(exprt &a : f.arguments()) { - if(a.is_constant() || - (a.id()==ID_typecast && to_typecast_expr(a).op().is_constant())) - { - const std::string arg_name= - id2string(fname)+"#arg"+i2string(i)+"#"+ - i2string(loc->location_number); - symbol_exprt arg(arg_name, a.type()); - n_it->equalities.push_back(equal_exprt(a, arg)); - a=arg; - } + const std::string arg_name= + id2string(fname)+"#arg"+i2string(i)+"#"+ + i2string(loc->location_number); + symbol_exprt arg(arg_name, a.type()); + n_it->equalities.push_back(equal_exprt(a, arg)); + a=arg; ++i; } From 688cbe3fc86468132dc575c129c2c2e793665d22 Mon Sep 17 00:00:00 2001 From: Sarbojit Das Date: Wed, 21 Nov 2018 16:48:46 +0530 Subject: [PATCH 5/7] modified: src/domains/ssa_analyzer.cpp --- src/domains/ssa_analyzer.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/domains/ssa_analyzer.cpp b/src/domains/ssa_analyzer.cpp index 094aee7c1..9a4035d6a 100644 --- a/src/domains/ssa_analyzer.cpp +++ b/src/domains/ssa_analyzer.cpp @@ -183,7 +183,7 @@ void ssa_analyzert::operator()( if(recursive && template_generator.options.get_bool_option("context-sensitive")) { - //while(strategy_solver->iterate_for_ins(*result)) {} + while(strategy_solver->iterate_for_ins(*result)) {} } status()<<"------------------------------------------------------------------\n"/////////////////////////// From ca2bc04dbc9fab8abc5474efbf8efa1fe98c2751 Mon Sep 17 00:00:00 2001 From: Sarbojit Das Date: Sat, 24 Nov 2018 15:10:27 +0530 Subject: [PATCH 6/7] modified: src/2ls/summary_checker_rect.cpp --- src/2ls/summary_checker_rect.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/2ls/summary_checker_rect.cpp b/src/2ls/summary_checker_rect.cpp index 5877a524c..dd17388de 100644 --- a/src/2ls/summary_checker_rect.cpp +++ b/src/2ls/summary_checker_rect.cpp @@ -111,8 +111,10 @@ void summary_checker_rect::summarize( summarizer=new summarizer_rec_fwt( options, summary_db, ssa_db, ssa_unwinder, ssa_inliner); else + { status()<<"No termination check supported for recursive programs."<set_message_handler(get_message_handler()); From acf531feecc368ecda5a4a87f3d206da713f0d95 Mon Sep 17 00:00:00 2001 From: Sarbojit Das Date: Sat, 24 Nov 2018 15:10:27 +0530 Subject: [PATCH 7/7] modified: src/2ls/summary_checker_rect.cpp modified: src/domains/ssa_analyzer.cpp modified: src/2ls/summary_checker_rect.cpp modified: src/2ls/summary_checker_rect.cpp modified: src/domains/ssa_analyzer.cpp modified: src/domains/template_gen_rec_summary.cpp modified: src/domains/tpolyhedra_domain.cpp --- install.sh | 8 ++++---- regression/interprocedural/contextsensitive2/main.c | 3 +-- src/2ls/summary_checker_rect.cpp | 10 ++++++---- src/domains/ssa_analyzer.cpp | 4 ++-- src/domains/template_gen_rec_summary.cpp | 13 +++++++------ src/domains/tpolyhedra_domain.cpp | 2 +- 6 files changed, 21 insertions(+), 19 deletions(-) diff --git a/install.sh b/install.sh index 299186752..90ee9b78a 100755 --- a/install.sh +++ b/install.sh @@ -14,10 +14,10 @@ CBMC=`pwd` git checkout $CBMC_VERSION if grep '^MINISAT2' src/config.inc > /dev/null then - make -C src minisat2-download > /dev/null + make -C src minisat2-download > /dev/null -j4 elif grep '^GLUCOSE' src/config.inc then - make -C src glucose-download + make -C src glucose-download -j4 else echo "SAT solver not supported" exit 1 @@ -26,7 +26,7 @@ if [ "$COMPILER" != "" ] then make -C src CXX=$COMPILER else - make -C src + make -C src -j4 fi cd ../src @@ -36,7 +36,7 @@ if [ "$COMPILER" != "" ] then make CXX=$COMPILER else - make + make -j4 fi cd .. echo "The executable is src/2ls/2ls" diff --git a/regression/interprocedural/contextsensitive2/main.c b/regression/interprocedural/contextsensitive2/main.c index 70fd27c8b..4a2ef0219 100644 --- a/regression/interprocedural/contextsensitive2/main.c +++ b/regression/interprocedural/contextsensitive2/main.c @@ -20,7 +20,6 @@ void main() int x = 1; int y = do1(x); assert(y==1); - x = -x; - int z = do2(x); + int z = do2(-x); assert(-1<=z && z<=1); } diff --git a/src/2ls/summary_checker_rect.cpp b/src/2ls/summary_checker_rect.cpp index 5877a524c..968bcf171 100644 --- a/src/2ls/summary_checker_rect.cpp +++ b/src/2ls/summary_checker_rect.cpp @@ -41,10 +41,10 @@ property_checkert::resultt summary_checker_rect::operator()( // properties initialize_property_map(goto_model.goto_functions); - /*property_checkert::resultt result=property_checkert::UNKNOWN; + property_checkert::resultt result=property_checkert::UNKNOWN; bool finished=false; while(!finished) - {*/ + { bool preconditions=options.get_bool_option("preconditions"); bool termination=options.get_bool_option("termination"); bool trivial_domain=options.get_bool_option("havoc"); @@ -59,7 +59,7 @@ property_checkert::resultt summary_checker_rect::operator()( exit(1); } - /*if(preconditions) + if(preconditions) { report_statistics(); report_preconditions(); @@ -89,7 +89,7 @@ property_checkert::resultt summary_checker_rect::operator()( { finished=true; } - }*/ + } //return result; return UNKNOWN; } @@ -111,8 +111,10 @@ void summary_checker_rect::summarize( summarizer=new summarizer_rec_fwt( options, summary_db, ssa_db, ssa_unwinder, ssa_inliner); else + { status()<<"No termination check supported for recursive programs."<set_message_handler(get_message_handler()); diff --git a/src/domains/ssa_analyzer.cpp b/src/domains/ssa_analyzer.cpp index 9a4035d6a..2ac046147 100644 --- a/src/domains/ssa_analyzer.cpp +++ b/src/domains/ssa_analyzer.cpp @@ -184,10 +184,10 @@ void ssa_analyzert::operator()( template_generator.options.get_bool_option("context-sensitive")) { while(strategy_solver->iterate_for_ins(*result)) {} + status()<<"------------------------------------------------------------------\n"/////////////////////////// + "-------------------------------------------------------------------\n"<iterate(*result)) {} diff --git a/src/domains/template_gen_rec_summary.cpp b/src/domains/template_gen_rec_summary.cpp index 1032bfcaa..e9233f6f5 100644 --- a/src/domains/template_gen_rec_summary.cpp +++ b/src/domains/template_gen_rec_summary.cpp @@ -69,8 +69,8 @@ void template_gen_rec_summaryt::merge_vars(const irep_idt &function_name, { std::string var_name= id2string(to_symbol_expr(var).get_identifier()); - irep_idt nondet_name(var_name+"_nondet"); - in_vars_vec.push_back(symbol_exprt(dstring(var_name+"_comb"),var.type())); + irep_idt nondet_name(var_name+"#nondet"); + in_vars_vec.push_back(symbol_exprt(dstring(var_name+"#comb"),var.type())); expr_vec.push_back(symbol_exprt(nondet_name,var.type())); } @@ -79,8 +79,8 @@ void template_gen_rec_summaryt::merge_vars(const irep_idt &function_name, { std::string var_name= id2string(to_symbol_expr(var).get_identifier()); - irep_idt nondet_name(var_name+"_nondet"); - in_vars_vec.push_back(symbol_exprt(dstring(var_name+"_comb"),var.type())); + irep_idt nondet_name(var_name+"#nondet"); + in_vars_vec.push_back(symbol_exprt(dstring(var_name+"#comb"),var.type())); expr_vec.push_back(symbol_exprt(nondet_name,var.type())); } @@ -89,8 +89,9 @@ void template_gen_rec_summaryt::merge_vars(const irep_idt &function_name, { std::string var_name= id2string(to_symbol_expr(var).get_identifier()); - irep_idt nondet_name(var_name+"_nondet"); - out_vars_vec.push_back(symbol_exprt(dstring(var_name+"_comb"),var.type())); + var_name=var_name.substr(0,var_name.find_last_of("#")); + irep_idt nondet_name(var_name+"#nondet"); + out_vars_vec.push_back(symbol_exprt(dstring(var_name+"#comb"),var.type())); expr_vec.push_back(symbol_exprt(nondet_name,var.type())); } diff --git a/src/domains/tpolyhedra_domain.cpp b/src/domains/tpolyhedra_domain.cpp index 6c2d7d080..7c99a77a5 100644 --- a/src/domains/tpolyhedra_domain.cpp +++ b/src/domains/tpolyhedra_domain.cpp @@ -699,7 +699,7 @@ void tpolyhedra_domaint::project_on_vars( templ_row.pre_guard, binary_relation_exprt(templ_row.expr, ID_le, row_v))); } - else if(templ_row.kind!=IN)//sarbojit + else //if(templ_row.kind!=IN)//sarbojit { if(is_row_value_neginf(row_v)) c.push_back(false_exprt());