Ignore false assertion during loop invariant synthesis

Author: qinheping

regression/goto-synthesizer/loop_contracts_synthesis_assert_false/main.c

@@ -0,0 +1,17 @@
+#include <stdlib.h>
+#include <stdbool.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.

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)
   {
@@ -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,17 +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_info.description
-              << 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;
   }
@@ -719,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())
   {
@@ -743,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();
@@ -755,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;
@@ -764,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

@@ -379,7 +379,7 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all()
       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: