[WIP] Symex: report reachability of properties

regression/cbmc/Quantifiers-if/test.desc

@@ -4,9 +4,9 @@ main.c
 ^\*\* Results:$
 ^\[main.assertion.1\] .* failure 1: FAILURE$
 ^\[main.assertion.2\] .* failure 2: FAILURE$
-^\[main.assertion.3\] .* success 1: SUCCESS$
+^\[main.assertion.3\] .* success 1: UNREACHABLE$
 ^\[main.assertion.4\] .* failure 3: FAILURE$
-^\[main.assertion.5\] .* success 2: SUCCESS$
+^\[main.assertion.5\] .* success 2: UNREACHABLE$
 ^\*\* 3 of 5 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$

regression/cbmc/Quantifiers-not/test.desc

@@ -2,10 +2,10 @@ CORE broken-z3-smt-backend
 main.c
 
 ^\*\* Results:$
-^\[main.assertion.1\] .* success 1: SUCCESS$
-^\[main.assertion.2\] .* success 2: SUCCESS$
+^\[main.assertion.1\] .* success 1: UNREACHABLE$
+^\[main.assertion.2\] .* success 2: UNREACHABLE$
 ^\[main.assertion.3\] .* failure 1: FAILURE$
-^\[main.assertion.4\] .* success 3: SUCCESS$
+^\[main.assertion.4\] .* success 3: UNREACHABLE$
 ^\[main.assertion.5\] .* failure 2: FAILURE$
 ^\*\* 2 of 5 failed
 ^VERIFICATION FAILED$

src/goto-checker/bmc_util.cpp

@@ -398,7 +398,8 @@ void run_property_decider(
   property_decider.add_constraint_from_goals(
     [&properties](const irep_idt &property_id) {
       return is_property_to_check(properties.at(property_id).status);
-    });
+    },
+    properties);
 
   auto const sat_solver_start = std::chrono::steady_clock::now();
 

src/goto-checker/goto_symex_property_decider.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "goto_symex_property_decider.h"
 
+#include <util/expr_util.h>
 #include <util/ui_message.h>
 
 #include <solvers/prop/prop.h>
@@ -28,15 +29,30 @@ goto_symex_property_decidert::goto_symex_property_decidert(
     ui_message_handler,
     ui_message_handler.get_ui() == ui_message_handlert::uit::XML_UI);
   solver = solvers.get_solver();
+
+  // TODO: make this configurable
+  cover_goals = true;
 }
 
-exprt goto_symex_property_decidert::goalt::as_expr() const
+exprt goto_symex_property_decidert::goalt::build_condition() const
 {
   exprt::operandst conjuncts;
   conjuncts.reserve(instances.size());
   for(const auto &inst : instances)
     conjuncts.push_back(inst->cond_handle);
-  return conjunction(conjuncts);
+
+  // Our goal is to falsify a property, i.e., we will
+  // add the negation of the property as goal.
+  return boolean_negate(conjunction(conjuncts));
+}
+
+exprt goto_symex_property_decidert::goalt::build_path_condition() const
+{
+  exprt::operandst disjuncts;
+  disjuncts.reserve(instances.size());
+  for(const auto &inst : instances)
+    disjuncts.push_back(inst->guard_handle);
+  return disjunction(disjuncts);
 }
 
 void goto_symex_property_decidert::
@@ -72,15 +88,19 @@ void goto_symex_property_decidert::convert_goals()
 {
   for(auto &goal_pair : goal_map)
   {
-    // Our goal is to falsify a property, i.e., we will
-    // add the negation of the property as goal.
-    goal_pair.second.condition = solver->decision_procedure().handle(
-      not_exprt(goal_pair.second.as_expr()));
+    goal_pair.second.condition =
+      solver->decision_procedure().handle(goal_pair.second.build_condition());
+    if(cover_goals)
+    {
+      goal_pair.second.path_condition = solver->decision_procedure().handle(
+        goal_pair.second.build_path_condition());
+    }
   }
 }
 
 void goto_symex_property_decidert::add_constraint_from_goals(
-  std::function<bool(const irep_idt &)> select_property)
+  std::function<bool(const irep_idt &)> select_property,
+  const propertiest &properties)
 {
   exprt::operandst disjuncts;
 
@@ -91,6 +111,12 @@ void goto_symex_property_decidert::add_constraint_from_goals(
       !goal_pair.second.condition.is_false())
     {
       disjuncts.push_back(goal_pair.second.condition);
+      if(cover_goals)
+      {
+        auto &status = properties.at(goal_pair.first).status;
+        if(status == property_statust::UNKNOWN)
+          disjuncts.push_back(goal_pair.second.path_condition);
+      }
     }
   }
 
@@ -141,6 +167,15 @@ void goto_symex_property_decidert::update_properties_status_from_goals(
         status |= property_statust::FAIL;
         updated_properties.insert(goal_pair.first);
       }
+      else if(
+        cover_goals && status == property_statust::UNKNOWN &&
+        solver->decision_procedure()
+          .get(goal_pair.second.path_condition)
+          .is_true())
+      {
+        status = property_statust::NOT_CHECKED;
+        updated_properties.insert(goal_pair.first);
+      }
     }
     break;
   case decision_proceduret::resultt::D_UNSATISFIABLE:
@@ -150,6 +185,14 @@ void goto_symex_property_decidert::update_properties_status_from_goals(
     for(auto &property_pair : properties)
     {
       if(property_pair.second.status == property_statust::UNKNOWN)
+      {
+        if(cover_goals)
+          property_pair.second.status |= property_statust::NOT_REACHABLE;
+        else
+          property_pair.second.status |= property_statust::PASS;
+        updated_properties.insert(property_pair.first);
+      }
+      else if(property_pair.second.status == property_statust::NOT_CHECKED)
       {
         property_pair.second.status |= property_statust::PASS;
         updated_properties.insert(property_pair.first);

src/goto-checker/goto_symex_property_decider.h

@@ -39,7 +39,8 @@ class goto_symex_property_decidert
 
   /// Add disjunction of negated selected properties to the equation
   void add_constraint_from_goals(
-    std::function<bool(const irep_idt &property_id)> select_property);
+    std::function<bool(const irep_idt &property_id)> select_property,
+    const propertiest &properties);
 
   /// Calls solve() on the solver instance
   decision_proceduret::resultt solve();
@@ -67,6 +68,7 @@ class goto_symex_property_decidert
     bool set_pass = true) const;
 protected:
   const optionst &options;
+  bool cover_goals;
   ui_message_handlert &ui_message_handler;
   symex_target_equationt &equation;
   std::unique_ptr<solver_factoryt::solvert> solver;
@@ -76,10 +78,14 @@ class goto_symex_property_decidert
     /// A property holds if all instances of it are true
     std::vector<symex_target_equationt::SSA_stepst::iterator> instances;
 
-    /// The goal variable
+    /// The goal property variable
     exprt condition;
 
-    exprt as_expr() const;
+    /// The goal reachability variable
+    exprt path_condition;
+
+    exprt build_condition() const;
+    exprt build_path_condition() const;
   };
 
   /// Maintains the relation between a property ID and

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -127,7 +127,8 @@ operator()(propertiest &properties)
       property_decider.add_constraint_from_goals(
         [&properties](const irep_idt &property_id) {
           return is_property_to_check(properties.at(property_id).status);
-        });
+        },
+        properties);
 
       log.status()
         << "Running "

src/goto-symex/symex_target_equation.cpp

@@ -522,8 +522,9 @@ void symex_target_equationt::convert_assertions(
       if(step.is_assert() && !step.ignore && !step.converted)
       {
         step.converted = true;
-        decision_procedure.set_to_false(step.cond_expr);
-        step.cond_handle = false_exprt();
+        step.cond_handle = decision_procedure.handle(step.cond_expr);
+        decision_procedure.set_to_true(
+          or_exprt{not_exprt{step.cond_handle}, step.guard_handle});
 
         with_solver_hardness(
           decision_procedure, hardness_register_ssa(step_index, step));
@@ -542,10 +543,10 @@ void symex_target_equationt::convert_assertions(
     UNREACHABLE; // unreachable
   }
 
-  // We do (NOT a1) OR (NOT a2) ...
+  // We do (NOT a1) OR a1.guard OR (NOT a2) OR a2.guard ...
   // where the a's are the assertions
   or_exprt::operandst disjuncts;
-  disjuncts.reserve(number_of_assertions);
+  disjuncts.reserve(2 * number_of_assertions);
 
   exprt assumption=true_exprt();
 
@@ -581,6 +582,7 @@ void symex_target_equationt::convert_assertions(
 
       // store disjunct
       disjuncts.push_back(not_exprt(step.cond_handle));
+      disjuncts.push_back(step.guard_handle);
     }
     else if(step.is_assume())
     {