Merge incomplete recursion code

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"

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);
 }

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<unsigned>::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<summary_checker_baset> checker;
     if(!options.get_bool_option("k-induction") &&
        !options.get_bool_option("incremental-bmc"))
-      checker=std::unique_ptr<summary_checker_baset>(
-        new summary_checker_ait(options, heap_analysis));
+    {
+      if(options.get_bool_option("has-recursion"))
+        checker=std::unique_ptr<summary_checker_baset>(
+          new summary_checker_rect(options, heap_analysis));
+      else
+        checker=std::unique_ptr<summary_checker_baset>(
+          new summary_checker_ait(options, heap_analysis));
+
+    }
     if(options.get_bool_option("k-induction") &&
        !options.get_bool_option("incremental-bmc"))
       checker=std::unique_ptr<summary_checker_baset>(
@@ -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"

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:

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 \

src/2ls/summary_checker_base.cpp

@@ -7,6 +7,7 @@ Author: Peter Schrammel
 \*******************************************************************/
 
 #include <iostream>
+#include <fstream>
 
 #include <util/options.h>
 #include <util/i2string.h>
@@ -80,6 +81,7 @@ void summary_checker_baset::SSA_functions(
 
   // properties
   initialize_property_map(goto_model.goto_functions);
+  //CustomSSAOperation(SSA,ns,"");//execute ic3
 }
 
 /*******************************************************************\

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);

src/2ls/summary_checker_rect.cpp

@@ -0,0 +1,134 @@
+/*
+ * 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 <solver/summarizer_fw.h>
+#include <solver/summarizer_fw_term.h>
+#include <solver/summarizer_bw.h>
+#include <solver/summarizer_bw_term.h>
+#include <solver/summarizer_rec_fw.h>
+
+#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);
+
+  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."<<eom;
+      exit(1);
+    }
+
+    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
+
+  if(result==property_checkert::UNKNOWN &&
+       options.get_bool_option("heap-values-refine") &&
+       options.get_bool_option("heap-interval"))
+    {
+      summary_db.clear();
+      options.set_option("heap-interval", false);
+      options.set_option("heap-zones", true);
+    }
+    else
+    {
+      finished=true;
+    }
+  }
+  //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(!termination)
+      summarizer=new summarizer_rec_fwt(
+        options, summary_db, ssa_db, ssa_unwinder, ssa_inliner);
+    else
+    {
+      status()<<"No termination check supported for recursive programs."<<eom;
+      exit(1);
+    }
+  }
+  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;
+}

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 */
+

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 = 

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 \

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()
@@ -120,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)
   {

src/domains/ssa_analyzer.cpp

@@ -63,7 +63,9 @@ 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,
+  const exprt &merge_expr)
 {
   if(SSA.goto_function.body.instructions.empty())
     return;
@@ -73,6 +75,8 @@ void ssa_analyzert::operator()(
 
   solver.new_context();
   solver << SSA.get_enabling_exprs();
+
+  if(recursive) solver<<merge_expr;//add merge expressions to solver
 
   // add precondition (or conjunction of asssertion in backward analysis)
   solver << precondition;
@@ -174,6 +178,15 @@ 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"))
+  {
+    while(strategy_solver->iterate_for_ins(*result)) {}
+    status()<<"------------------------------------------------------------------\n"///////////////////////////
+     "-------------------------------------------------------------------\n"<<eom;///////////////////////////
+  }
 
   // iterate
   while(strategy_solver->iterate(*result)) {}