Merge pull request #7268 from diffblue/chc_generalization

CHC solver: generalization

Author: kroening

regression/cprover/loops/assigns1.c

@@ -1,12 +1,11 @@
 int main()
 {
-  int *p;
-  __CPROVER_assume(__CPROVER_r_ok(p));
+  int x = 123;
 
   for(int i = 0; i < 10; i++)
   {
-    // does not assign p
+    // does not assign x
   }
 
-  __CPROVER_assert(__CPROVER_r_ok(p), "property 1"); // passes
+  __CPROVER_assert(x == 123, "property 1"); // passes
 }

regression/cprover/loops/assigns1.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 assigns1.c
 
 ^EXIT=0$

regression/cprover/loops/assigns2.c

@@ -0,0 +1,12 @@
+int main()
+{
+  int x = 123;
+
+  // The loops do not assign x.
+  for(int i = 0; i < 10; i++)
+    ;
+  for(int i = 0; i < 10; i++)
+    ;
+
+  __CPROVER_assert(x == 123, "property 1"); // passes
+}

regression/cprover/loops/assigns2.desc

@@ -0,0 +1,8 @@
+CORE
+assigns2.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+--
+--

src/cprover/Makefile

@@ -12,6 +12,7 @@ SRC = address_taken.cpp \
       flatten_ok_expr.cpp \
       format_hooks.cpp \
       free_symbols.cpp \
+      generalization.cpp \
       help_formatter.cpp \
       inductiveness.cpp \
       instrument_contracts.cpp \

src/cprover/generalization.cpp

@@ -0,0 +1,143 @@
+/*******************************************************************\
+
+Module: Generalization
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+/// \file
+/// Generalization
+
+#include "generalization.h"
+
+#include <util/format_expr.h>
+
+#include "console.h"
+#include "solver.h"
+
+#include <iostream>
+#include <map>
+
+class frequency_mapt
+{
+public:
+  explicit frequency_mapt(const exprt &expr)
+  {
+    setup_rec(expr);
+  }
+
+  void operator()(const exprt &expr)
+  {
+    count_rec(expr);
+  }
+
+  using counterst = std::map<exprt, std::size_t>;
+
+  // return frequencies, highest to lowest
+  std::vector<counterst::const_iterator> frequencies() const
+  {
+    std::vector<counterst::const_iterator> result;
+    for(auto it = counters.begin(); it != counters.end(); it++)
+      result.push_back(it);
+    std::sort(
+      result.begin(),
+      result.end(),
+      [](counterst::const_iterator a, counterst::const_iterator b) -> bool {
+        return a->second >= b->second;
+      });
+    return result;
+  }
+
+protected:
+  counterst counters;
+
+  void count_rec(const exprt &expr)
+  {
+    if(expr.id() == ID_or)
+    {
+      for(auto &op : expr.operands())
+        count_rec(op);
+    }
+    else
+    {
+      auto it = counters.find(expr);
+      if(it != counters.end())
+        it->second++;
+    }
+  }
+
+  void setup_rec(const exprt &expr)
+  {
+    if(expr.id() == ID_or)
+    {
+      for(auto &op : expr.operands())
+        setup_rec(op);
+    }
+    else
+      counters.emplace(expr, 0);
+  }
+};
+
+void generalization(
+  std::vector<framet> &frames,
+  const workt &dropped,
+  const propertyt &property,
+  const solver_optionst &solver_options)
+{
+  // Look at the frame where we've given up
+  auto &frame = frames[dropped.frame.index];
+
+  if(solver_options.verbose)
+  {
+    for(auto &invariant : frame.invariants)
+    {
+      std::cout << consolet::green << "GI " << format(invariant)
+                << consolet::reset << '\n';
+    }
+  }
+
+  // We generalize by dropping disjuncts.
+  // Look at the frequencies of the disjuncts in the proof obligation
+  // among the candidate invariant and the previous obligations.
+  frequency_mapt frequency_map(dropped.invariant);
+
+  for(auto &i : frame.invariants)
+    frequency_map(i);
+
+  for(auto &o : frame.obligations)
+    frequency_map(o);
+
+  const auto frequencies = frequency_map.frequencies();
+
+  if(solver_options.verbose)
+  {
+    for(auto entry : frequencies)
+    {
+      std::cout << "Freq " << entry->second << " " << format(entry->first)
+                << "\n";
+    }
+  }
+
+  // form disjunction of top ones
+  exprt::operandst disjuncts;
+  for(auto entry : frequencies)
+  {
+    if(entry->second == frequencies.front()->second)
+      disjuncts.push_back(entry->first);
+  }
+
+  // Does this actually strengthen the formula?
+  if(disjuncts.size() < frequencies.size())
+  {
+    auto new_invariant = disjunction(disjuncts);
+    frame.add_invariant(new_invariant);
+    if(solver_options.verbose)
+      std::cout << consolet::yellow << "NI " << format(new_invariant)
+                << consolet::reset << '\n';
+  }
+  else
+  {
+    // no, give up
+  }
+}

src/cprover/generalization.h

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module: Generalization
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+/// \file
+/// Generalization
+
+#ifndef CPROVER_CPROVER_GENERALIZATION_H
+#define CPROVER_CPROVER_GENERALIZATION_H
+
+#include "solver_types.h"
+
+class solver_optionst;
+
+void generalization(
+  std::vector<framet> &frames,
+  const workt &dropped,
+  const propertyt &,
+  const solver_optionst &);
+
+#endif // CPROVER_CPROVER_GENERALIZATION_H

src/cprover/inductiveness.cpp

@@ -31,6 +31,7 @@ Author: Daniel Kroening, dkr@amazon.com
 bool is_subsumed(
   const std::unordered_set<exprt, irep_hash> &a1,
   const std::unordered_set<exprt, irep_hash> &a2,
+  const std::unordered_set<exprt, irep_hash> &a3,
   const exprt &b,
   const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
   bool verbose,
@@ -64,6 +65,9 @@ bool is_subsumed(
   for(auto &a_conjunct : a2)
     axioms << a_conjunct;
 
+  for(auto &a_conjunct : a3)
+    axioms << a_conjunct;
+
   axioms.set_to_false(b);
 
   // instantiate our axioms
@@ -136,14 +140,21 @@ inductiveness_resultt inductiveness_check(
 
       if(solver_options.verbose)
       {
-        // print the current invariants in the frame
+        // print the current invariants and obligations in the frame
         for(const auto &invariant : f.invariants)
         {
           std::cout << consolet::faint << consolet::blue;
           std::cout << 'I' << std::setw(2) << frame_ref.index << ' ';
           std::cout << format(invariant);
           std::cout << consolet::reset << '\n';
         }
+        for(const auto &obligation : f.obligations)
+        {
+          std::cout << consolet::faint << consolet::blue;
+          std::cout << 'O' << std::setw(2) << frame_ref.index << ' ';
+          std::cout << format(obligation);
+          std::cout << consolet::reset << '\n';
+        }
       }
 
       if(solver_options.verbose)
@@ -158,6 +169,7 @@ inductiveness_resultt inductiveness_check(
       }
       else if(is_subsumed(
                 f.invariants_set,
+                f.obligations_set,
                 f.auxiliaries_set,
                 invariant,
                 address_taken,
@@ -182,7 +194,7 @@ inductiveness_resultt inductiveness_check(
           std::cout << format(invariant) << '\n';
 
         // store in frame
-        frames[frame_ref.index].add_invariant(invariant);
+        frames[frame_ref.index].add_obligation(invariant);
 
         // add to queue
         auto new_path = path;
@@ -191,14 +203,21 @@ inductiveness_resultt inductiveness_check(
       }
     };
 
-  // stick non-true frames into the queue
+  // stick invariants into the queue
   for(std::size_t frame_index = 0; frame_index < frames.size(); frame_index++)
   {
     frame_reft frame_ref(frame_index);
     for(auto &cond : frames[frame_index].invariants)
       queue.emplace_back(frame_ref, cond, workt::patht{frame_ref});
   }
 
+  // clean up the obligations
+  for(auto &frame : frames)
+  {
+    frame.obligations.clear();
+    frame.obligations_set.clear();
+  }
+
   while(!queue.empty())
   {
     auto work = queue.back();
@@ -218,16 +237,17 @@ inductiveness_resultt inductiveness_check(
     if(counterexample_found)
     {
       property.trace = counterexample_found.value();
-      return inductiveness_resultt::BASE_CASE_FAIL;
+      return inductiveness_resultt::base_case_fail(std::move(work));
     }
 
     propagate(
       frames, work, address_taken, solver_options.verbose, ns, propagator);
+
+    // did we drop anything?
+    if(!dropped.empty())
+      return inductiveness_resultt::step_case_fail(std::move(dropped.front()));
   }
 
-  // did we drop anything?
-  if(dropped.empty())
-    return inductiveness_resultt::INDUCTIVE;
-  else
-    return inductiveness_resultt::STEP_CASE_FAIL;
+  // done, saturated
+  return inductiveness_resultt::inductive();
 }

src/cprover/inductiveness.h

@@ -16,11 +16,41 @@ Author: Daniel Kroening, dkr@amazon.com
 
 class solver_optionst;
 
-enum inductiveness_resultt
+class inductiveness_resultt
 {
-  INDUCTIVE,
-  BASE_CASE_FAIL,
-  STEP_CASE_FAIL
+public:
+  enum outcomet
+  {
+    INDUCTIVE,
+    BASE_CASE_FAIL,
+    STEP_CASE_FAIL
+  } outcome;
+
+  static inductiveness_resultt inductive()
+  {
+    return inductiveness_resultt(INDUCTIVE);
+  }
+
+  static inductiveness_resultt base_case_fail(workt refuted)
+  {
+    auto result = inductiveness_resultt(BASE_CASE_FAIL);
+    result.work = std::move(refuted);
+    return result;
+  }
+
+  static inductiveness_resultt step_case_fail(workt dropped)
+  {
+    auto result = inductiveness_resultt(STEP_CASE_FAIL);
+    result.work = std::move(dropped);
+    return result;
+  }
+
+  optionalt<workt> work;
+
+private:
+  explicit inductiveness_resultt(outcomet __outcome) : outcome(__outcome)
+  {
+  }
 };
 
 inductiveness_resultt inductiveness_check(

src/cprover/propagate.cpp

@@ -75,7 +75,8 @@ void propagate(
       auto &state = to_symbol_expr(function_application.function());
       auto cond1 = to_and_expr(implication.lhs).op1();
       auto cond2 = implies_exprt(cond1, simplified2);
-      propagator(state, cond2, work.path);
+      auto simplified = simplify_expr(cond2, ns);
+      propagator(state, simplified, work.path);
     }
   }
 }