Merge pull request #7488 from qinheping/goto-synthesizer-enumerating

SYNTHESIZER: Enable enumerating mode for checks other than pointer checks

Author: tautschnig

regression/goto-synthesizer/loop_contracts_synthesis_assert_false/main.c

@@ -0,0 +1,17 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+void main()
+{
+  long x = 0;
+  long y;
+  __CPROVER_assume(y > 1);
+
+  while(y > 0)
+  {
+    x = 1;
+    y = y - 1;
+  }
+
+  assert(false);
+}

regression/goto-synthesizer/loop_contracts_synthesis_assert_false/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.assigns.\d+\] .* Check that x is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that y is assignable: SUCCESS$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+--
+--
+Check whether loop invariant are synthesized when there is ASSERT FALSE.

regression/goto-synthesizer/loop_contracts_synthesis_other_assertion/main.c

@@ -0,0 +1,15 @@
+#include <stdlib.h>
+
+void main()
+{
+  long x = 0;
+  long y;
+  __CPROVER_assume(y > 1);
+
+  while(y > 0)
+  {
+    x = 1;
+    y = y - 1;
+  }
+  assert(y == 0);
+}

regression/goto-synthesizer/loop_contracts_synthesis_other_assertion/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.assigns.\d+\] .* Check that x is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that y is assignable: SUCCESS$
+^\[main.assertion.\d+\] .* assertion y \=\=
+^VERIFICATION SUCCESSFUL$
+--
+--
+Check whether loop invariant are synthesized for checks other than
+pointer checks.

src/goto-synthesizer/cegis_verifier.cpp

@@ -588,6 +588,8 @@ optionalt<cext> cegis_verifiert::verify()
   // 3. construct the formatted counterexample from the violated property and
   //    its trace.
 
+  const namespacet ns(goto_model.symbol_table);
+
   // Store the original functions. We will restore them after the verification.
   for(const auto &fun_entry : goto_model.goto_functions.function_map)
   {
@@ -600,11 +602,11 @@ optionalt<cext> cegis_verifiert::verify()
   // Annotate assigns
   annotate_assigns(assigns_map, goto_model);
 
-  // Control verbosity.
-  // We allow non-error output message only when verbosity is set to at least 9.
+  // Control verbosity. We allow non-error output message only when verbosity
+  // is set to larger than messaget::M_DEBUG.
   const unsigned original_verbosity = log.get_message_handler().get_verbosity();
-  if(original_verbosity < 9)
-    log.get_message_handler().set_verbosity(1);
+  if(original_verbosity < messaget::M_DEBUG)
+    log.get_message_handler().set_verbosity(messaget::M_ERROR);
 
   // Apply loop contracts we annotated.
   code_contractst cont(goto_model, log);
@@ -630,7 +632,7 @@ optionalt<cext> cegis_verifiert::verify()
   // Run the checker to get the result.
   const resultt result = (*checker)();
 
-  if(original_verbosity >= 9)
+  if(original_verbosity >= messaget::M_DEBUG)
     checker->report();
 
   // Restore the verbosity.
@@ -652,38 +654,48 @@ optionalt<cext> cegis_verifiert::verify()
   }
 
   properties = checker->get_properties();
-  bool target_violation_found = false;
-  auto target_violation_info = properties.begin()->second;
+  auto target_violation = properties.end();
 
   // Find target violation---the violation we want to fix next.
   // A target violation is an assignable violation or the first violation that
   // is not assignable violation.
-  for(const auto &property : properties)
+  for(auto it_property = properties.begin(); it_property != properties.end();
+      it_property++)
   {
-    if(property.second.status != property_statust::FAIL)
+    if(it_property->second.status != property_statust::FAIL)
       continue;
 
     // assignable violation found
-    if(property.second.description.find("assignable") != std::string::npos)
+    if(it_property->second.description.find("assignable") != std::string::npos)
     {
-      target_violation = property.first;
-      target_violation_info = property.second;
+      target_violation = it_property;
       break;
     }
 
     // Store the violation that we want to fix with synthesized
     // assigns/invariant.
-    if(!target_violation_found)
+    // ignore ASSERT FALSE
+    if(
+      target_violation == properties.end() &&
+      simplify_expr(it_property->second.pc->condition(), ns) != false_exprt())
     {
-      target_violation = property.first;
-      target_violation_info = property.second;
-      target_violation_found = true;
+      target_violation = it_property;
     }
   }
 
+  // All violations are
+  // ASSERT FALSE
+  if(target_violation == properties.end())
+  {
+    restore_functions();
+    return optionalt<cext>();
+  }
+
+  target_violation_id = target_violation->first;
+
   // Decide the violation type from the description of violation
   cext::violation_typet violation_type =
-    extract_violation_type(target_violation_info.description);
+    extract_violation_type(target_violation->second.description);
 
   // Compute the cause loop---the loop for which we synthesize loop contracts,
   // and the counterexample.
@@ -698,15 +710,17 @@ optionalt<cext> cegis_verifiert::verify()
   // although there can be multiple ones.
 
   log.debug() << "Start to compute cause loop ids." << messaget::eom;
+  log.debug() << "Violation description: "
+              << target_violation->second.description << messaget::eom;
 
-  const auto &trace = checker->get_traces()[target_violation];
+  const auto &trace = checker->get_traces()[target_violation->first];
   // Doing assigns-synthesis or invariant-synthesis
   if(violation_type == cext::violation_typet::cex_assignable)
   {
     cext result(violation_type);
     result.cause_loop_ids = get_cause_loop_id_for_assigns(trace);
     result.checked_pointer = static_cast<const exprt &>(
-      target_violation_info.pc->condition().find(ID_checked_assigns));
+      target_violation->second.pc->condition().find(ID_checked_assigns));
     restore_functions();
     return result;
   }
@@ -717,7 +731,7 @@ optionalt<cext> cegis_verifiert::verify()
   // Although there can be multiple cause loop ids. We only synthesize
   // loop invariants for the first cause loop.
   const std::list<loop_idt> cause_loop_ids =
-    get_cause_loop_id(trace, target_violation_info.pc);
+    get_cause_loop_id(trace, target_violation->second.pc);
 
   if(cause_loop_ids.empty())
   {
@@ -741,7 +755,7 @@ optionalt<cext> cegis_verifiert::verify()
     violation_location = get_violation_location(
       cause_loop_ids.front(),
       goto_model.get_goto_function(cause_loop_ids.front().function_id),
-      target_violation_info.pc->location_number);
+      target_violation->second.pc->location_number);
   }
 
   restore_functions();
@@ -753,7 +767,7 @@ optionalt<cext> cegis_verifiert::verify()
       goto_model.goto_functions
         .function_map[cause_loop_ids.front().function_id])
       ->source_location());
-  return_cex.violated_predicate = target_violation_info.pc->condition();
+  return_cex.violated_predicate = target_violation->second.pc->condition();
   return_cex.cause_loop_ids = cause_loop_ids;
   return_cex.violation_location = violation_location;
   return_cex.violation_type = violation_type;
@@ -762,7 +776,7 @@ optionalt<cext> cegis_verifiert::verify()
   if(violation_type == cext::violation_typet::cex_null_pointer)
   {
     return_cex.checked_pointer = get_checked_pointer_from_null_pointer_check(
-      target_violation_info.pc->condition());
+      target_violation->second.pc->condition());
   }
 
   return return_cex;

src/goto-synthesizer/cegis_verifier.h

@@ -117,7 +117,7 @@ class cegis_verifiert
 
   /// Result counterexample.
   propertiest properties;
-  irep_idt target_violation;
+  irep_idt target_violation_id;
 
 protected:
   // Get the options same as using CBMC api without any flag, and

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp

@@ -73,8 +73,8 @@ std::vector<exprt> construct_terminals(const std::set<symbol_exprt> &symbols)
         unary_exprt(ID_loop_entry, e, e.type()), size_type()));
     }
   }
-  result.push_back(from_integer(1, unsigned_int_type()));
-  result.push_back(from_integer(1, unsigned_long_int_type()));
+  result.push_back(from_integer(1, signed_short_int_type()));
+  result.push_back(from_integer(0, signed_short_int_type()));
   return result;
 }
 
@@ -100,13 +100,13 @@ void enumerative_loop_contracts_synthesizert::init_candidates()
       // we only synthesize invariants and assigns for unannotated loops
       if(loop_end->condition().find(ID_C_spec_loop_invariant).is_nil())
       {
-        // Store the loop guard.
-        exprt guard =
-          get_loop_head(
-            loop_end->loop_number,
-            goto_model.goto_functions.function_map[function_p.first])
-            ->condition();
-        neg_guards[new_id] = guard;
+        // Store the loop guard if exists.
+        auto loop_head = get_loop_head(
+          loop_end->loop_number,
+          goto_model.goto_functions.function_map[function_p.first]);
+
+        if(loop_head->has_condition())
+          neg_guards[new_id] = loop_head->condition();
 
         // Initialize invariant clauses as `true`.
         in_invariant_clause_map[new_id] = true_exprt();
@@ -120,6 +120,7 @@ void enumerative_loop_contracts_synthesizert::init_candidates()
       }
     }
   }
+  log.debug() << "Finished candidates initialization." << messaget::eom;
 }
 
 void enumerative_loop_contracts_synthesizert::synthesize_assigns(
@@ -303,12 +304,17 @@ exprt enumerative_loop_contracts_synthesizert::synthesize_strengthening_clause(
     // generate candidate and verify
     for(auto strengthening_candidate : start_bool_ph.enumerate(size_bound))
     {
+      log.progress() << "Verifying candidate: "
+                     << format(strengthening_candidate) << messaget::eom;
       seen_terms++;
       invariant_mapt new_in_clauses = invariant_mapt(in_invariant_clause_map);
       new_in_clauses[cause_loop_id] =
         and_exprt(new_in_clauses[cause_loop_id], strengthening_candidate);
+      invariant_mapt new_pos_clauses = invariant_mapt(pos_invariant_clause_map);
+      new_pos_clauses[cause_loop_id] =
+        and_exprt(new_pos_clauses[cause_loop_id], strengthening_candidate);
       const auto &combined_invariant = combine_in_and_post_invariant_clauses(
-        new_in_clauses, pos_invariant_clause_map, neg_guards);
+        new_in_clauses, new_pos_clauses, neg_guards);
 
       // The verifier we use to check current invariant candidates.
       cegis_verifiert verifier(
@@ -323,7 +329,9 @@ exprt enumerative_loop_contracts_synthesizert::synthesize_strengthening_clause(
         (verifier.properties.at(violation_id).status !=
            property_statust::FAIL &&
          return_cex->violation_type !=
-           cext::violation_typet::cex_not_hold_upon_entry))
+           cext::violation_typet::cex_not_hold_upon_entry &&
+         return_cex->violation_type !=
+           cext::violation_typet::cex_not_preserved))
       {
         return strengthening_candidate;
       }
@@ -351,6 +359,7 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all()
   // Set of symbols we used to enumerate strengthening clauses.
   std::vector<exprt> terminal_symbols;
 
+  log.debug() << "Start the first synthesis iteration." << messaget::eom;
   auto return_cex = verifier.verify();
 
   while(return_cex.has_value())
@@ -370,20 +379,26 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all()
         synthesize_same_object_predicate(return_cex->checked_pointer);
       break;
 
+    case cext::violation_typet::cex_assignable:
+      synthesize_assigns(
+        return_cex->checked_pointer, return_cex->cause_loop_ids);
+      break;
+
+    case cext::violation_typet::cex_other:
+      // Update the dependent symbols.
+      dependent_symbols = compute_dependent_symbols(
+        return_cex->cause_loop_ids.front(),
+        new_invariant_clause,
+        return_cex->live_variables);
     case cext::violation_typet::cex_not_preserved:
       terminal_symbols = construct_terminals(dependent_symbols);
       new_invariant_clause = synthesize_strengthening_clause(
         terminal_symbols,
         return_cex->cause_loop_ids.front(),
-        verifier.target_violation);
+        verifier.target_violation_id);
       break;
 
-    case cext::violation_typet::cex_assignable:
-      synthesize_assigns(
-        return_cex->checked_pointer, return_cex->cause_loop_ids);
-      break;
     case cext::violation_typet::cex_not_hold_upon_entry:
-    case cext::violation_typet::cex_other:
       INVARIANT(false, "unsupported violation type");
       break;
     }