Factor out goto_symex_property_decider

Author: peterschrammel

src/goto-checker/Makefile

@@ -1,6 +1,7 @@
 SRC = bmc_util.cpp \
       counterexample_beautification.cpp \
       incremental_goto_checker.cpp \
+      goto_symex_property_decider.cpp \
       goto_trace_storage.cpp \
       goto_verifier.cpp \
       multi_path_symex_checker.cpp \

src/goto-checker/goto_symex_property_decider.cpp

@@ -0,0 +1,164 @@
+/*******************************************************************\
+
+Module: Property Decider for Goto-Symex
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Property Decider for Goto-Symex
+
+#include "goto_symex_property_decider.h"
+
+goto_symex_property_decidert::goto_symex_property_decidert(
+  const optionst &options,
+  ui_message_handlert &ui_message_handler,
+  symex_target_equationt &equation,
+  const namespacet &ns)
+  : options(options),
+    ui_message_handler(ui_message_handler),
+    equation(equation)
+{
+  solver_factoryt solvers(
+    options,
+    ns,
+    ui_message_handler,
+    ui_message_handler.get_ui() == ui_message_handlert::uit::XML_UI);
+  solver = solvers.get_solver();
+  solver->prop_conv().set_message_handler(ui_message_handler);
+}
+
+exprt goto_symex_property_decidert::goalt::as_expr() const
+{
+  std::vector<exprt> tmp;
+  tmp.reserve(instances.size());
+  for(const auto &inst : instances)
+    tmp.push_back(literal_exprt(inst->cond_literal));
+  return conjunction(tmp);
+}
+
+void goto_symex_property_decidert::
+update_properties_goals_from_symex_target_equation(propertiest &properties)
+{
+  for(symex_target_equationt::SSA_stepst::iterator it =
+    equation.SSA_steps.begin();
+      it != equation.SSA_steps.end();
+      ++it)
+  {
+    if(it->is_assert())
+    {
+      irep_idt property_id = it->get_property_id();
+      CHECK_RETURN(!property_id.empty());
+
+      // consider goal instance if it is in the given properties
+      auto property_pair_it = properties.find(property_id);
+      if(
+        property_pair_it != properties.end() &&
+        is_property_to_check(property_pair_it->second.status))
+      {
+        // it's going to be checked, but we don't know the status yet
+        property_pair_it->second.status |= property_statust::UNKNOWN;
+        goal_map[property_id].instances.push_back(it);
+      }
+    }
+  }
+}
+
+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->prop_conv().convert(goal_pair.second.as_expr());
+  }
+}
+
+void goto_symex_property_decidert::freeze_goal_variables()
+{
+  for(const auto &goal_pair : goal_map)
+  {
+    if(!goal_pair.second.condition.is_constant())
+      solver->prop_conv().set_frozen(goal_pair.second.condition);
+  }
+}
+
+void goto_symex_property_decidert::add_constraint_from_goals(
+  std::function<bool(const irep_idt &)> select_property)
+{
+  exprt::operandst disjuncts;
+
+  for(const auto &goal_pair : goal_map)
+  {
+    if(
+      select_property(goal_pair.first) &&
+      !goal_pair.second.condition.is_false())
+    {
+      disjuncts.push_back(literal_exprt(goal_pair.second.condition));
+    }
+  }
+
+  // this is 'false' if there are no disjuncts
+  solver->prop_conv().set_to_true(disjunction(disjuncts));
+}
+
+decision_proceduret::resultt goto_symex_property_decidert::solve()
+{
+  return solver->prop_conv().dec_solve();
+}
+
+prop_convt &goto_symex_property_decidert::get_solver() const
+{
+  return solver->prop_conv();
+}
+
+symex_target_equationt &goto_symex_property_decidert::get_equation() const
+{
+  return equation;
+}
+
+void goto_symex_property_decidert::update_properties_status_from_goals(
+  propertiest &properties,
+  std::unordered_set<irep_idt> &updated_properties,
+  decision_proceduret::resultt dec_result,
+  bool set_pass) const
+{
+  switch(dec_result)
+  {
+    case decision_proceduret::resultt::D_SATISFIABLE:
+      for(auto &goal_pair : goal_map)
+      {
+        if(solver->prop_conv().l_get(goal_pair.second.condition).is_true())
+        {
+          properties.at(goal_pair.first).status |= property_statust::FAIL;
+          updated_properties.insert(goal_pair.first);
+        }
+      }
+      break;
+    case decision_proceduret::resultt::D_UNSATISFIABLE:
+      if(!set_pass)
+        break;
+
+      for(auto &property_pair : properties)
+      {
+        if(property_pair.second.status == property_statust::UNKNOWN)
+        {
+          property_pair.second.status |= property_statust::PASS;
+          updated_properties.insert(property_pair.first);
+        }
+      }
+      break;
+    case decision_proceduret::resultt::D_ERROR:
+      for(auto &property_pair : properties)
+      {
+        if(property_pair.second.status == property_statust::UNKNOWN)
+        {
+          property_pair.second.status |= property_statust::ERROR;
+          updated_properties.insert(property_pair.first);
+        }
+      }
+      break;
+  }
+}

src/goto-checker/goto_symex_property_decider.h

@@ -0,0 +1,91 @@
+/*******************************************************************\
+
+Module: Property Decider for Goto-Symex
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Property Decider for Goto-Symex
+
+#ifndef CPROVER_GOTO_CHECKER_GOTO_SYMEX_PROPERTY_DECIDER_H
+#define CPROVER_GOTO_CHECKER_GOTO_SYMEX_PROPERTY_DECIDER_H
+
+#include <util/ui_message.h>
+
+#include <goto-symex/symex_target_equation.h>
+
+#include "properties.h"
+#include "solver_factory.h"
+
+/// Provides management of goal variables that encode properties
+class goto_symex_property_decidert
+{
+public:
+  goto_symex_property_decidert(
+    const optionst &options,
+    ui_message_handlert &ui_message_handler,
+    symex_target_equationt &equation,
+    const namespacet &ns);
+
+  /// Get the conditions for the properties from the equation
+  /// and collect all 'instances' of the properties in the `goal_map`
+  void
+  update_properties_goals_from_symex_target_equation(propertiest &properties);
+
+  /// Convert the instances of a property into a goal variable
+  void convert_goals();
+
+  /// Prevent the solver to optimize-away the goal variables
+  /// (necessary for incremental solving)
+  void freeze_goal_variables();
+
+  /// Add disjunction of negated selected properties to the equation
+  void add_constraint_from_goals(
+    std::function<bool(const irep_idt &property_id)> select_property);
+
+  /// Calls solve() on the solver instance
+  decision_proceduret::resultt solve();
+
+  /// Returns the solver instance
+  prop_convt &get_solver() const;
+
+  /// Return the equation associated with this instance
+  symex_target_equationt &get_equation() const;
+
+  /// Update the property status from the truth value of the goal variable
+  /// \param [inout] properties: The status is updated in this data structure
+  /// \param [inout] updated_properties: The set of property IDs of
+  ///   updated properties
+  /// \param dec_result: The result returned by the solver
+  void update_properties_status_from_goals(
+    propertiest &properties,
+    std::unordered_set<irep_idt> &updated_properties,
+    decision_proceduret::resultt dec_result,
+    bool set_pass = true) const;
+
+protected:
+  const optionst &options;
+  ui_message_handlert &ui_message_handler;
+  symex_target_equationt &equation;
+  std::unique_ptr<solver_factoryt::solvert> solver;
+
+  struct goalt
+  {
+    /// A property holds if all instances of it are true
+    std::vector<symex_target_equationt::SSA_stepst::iterator> instances;
+
+    /// The goal variable
+    literalt condition;
+
+    exprt as_expr() const;
+  };
+
+  /// Maintains the relation between a property ID and
+  /// the corresponding goal variable that encodes
+  /// the negation of the conjunction of the instances of the property
+  std::map<irep_idt, goalt> goal_map;
+};
+
+#endif // CPROVER_GOTO_CHECKER_GOTO_SYMEX_PROPERTY_DECIDER_H