Merge pull request #5480 from natasha-jeppu/clause-map

CBMC additional profiling info: Extend solver hardness to track clauses mapped to an instruction

Author: danielsn

regression/solver-hardness/solver-hardness-simple/test.desc

@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^\[main.assertion.\d+\] line \d+ assertion a \+ b \< 10: FAILURE$
 ^VERIFICATION FAILED$
-\"SAT_hardness\":\{(\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+)\}
+\"SAT_hardness\":\{(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+)\}
 --
 ^warning: ignoring

src/solvers/sat/satcheck_minisat2.cpp

@@ -140,8 +140,22 @@ void satcheck_minisat2_baset<T>::lcnf(const bvt &bv)
 
     solver->addClause_(c);
 
+    // To map clauses to lines of program code, track clause indices in the
+    // dimacs cnf output. Dimacs output is generated after processing clauses
+    // to remove duplicates and clauses that are trivially true. Here, a clause
+    // is checked to see if it can be thus eliminated. If not, add the clause
+    // index to list of clauses in solver_hardnesst::register_clause().
+    static size_t cnf_clause_index = 0;
+    bvt cnf;
+    bool clause_removed = process_clause(bv, cnf);
+
+    if(!clause_removed)
+      cnf_clause_index++;
+
     with_solver_hardness(
-      [&bv](solver_hardnesst &hardness) { hardness.register_clause(bv); });
+      [&bv, &cnf, &clause_removed](solver_hardnesst &hardness) {
+        hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
+      });
     clause_counter++;
   }
   catch(const Minisat::OutOfMemoryException &)

src/solvers/solver_hardness.cpp

@@ -26,6 +26,8 @@ operator+=(const solver_hardnesst::sat_hardnesst &other)
   clauses += other.clauses;
   literals += other.literals;
   variables.insert(other.variables.begin(), other.variables.end());
+  clause_set.insert(
+    clause_set.end(), other.clause_set.begin(), other.clause_set.end());
   return *this;
 }
 
@@ -87,14 +89,30 @@ void solver_hardnesst::register_assertion_ssas(
   current_hardness = {};
 }
 
-void solver_hardnesst::register_clause(const bvt &bv)
+void solver_hardnesst::register_clause(
+  const bvt &bv,
+  const bvt &cnf,
+  const size_t cnf_clause_index,
+  bool register_cnf)
 {
   current_hardness.clauses++;
   current_hardness.literals += bv.size();
+
   for(const auto &literal : bv)
   {
     current_hardness.variables.insert(literal.var_no());
   }
+
+  if(register_cnf)
+  {
+#ifdef DEBUG
+    std::cout << cnf_clause_index << ": ";
+    for(const auto &literal : cnf)
+      std::cout << literal.dimacs() << " ";
+    std::cout << "0\n";
+#endif
+    current_hardness.clause_set.push_back(cnf_clause_index);
+  }
 }
 
 void solver_hardnesst::set_outfile(const std::string &file_name)
@@ -151,6 +169,14 @@ void solver_hardnesst::produce_report()
       sat_hardness_json["Variables"] =
         json_numbert{std::to_string(hardness.variables.size())};
 
+      json_arrayt sat_hardness_clause_set_json;
+      for(auto const &clause : hardness.clause_set)
+      {
+        sat_hardness_clause_set_json.push_back(
+          json_numbert{std::to_string(clause)});
+      }
+      sat_hardness_json["ClauseSet"] = sat_hardness_clause_set_json;
+
       hardness_stats_json["SAT_hardness"] = sat_hardness_json;
 
       json_stream_array.push_back(hardness_stats_json);
@@ -183,6 +209,15 @@ void solver_hardnesst::produce_report()
     assertion_hardness_json["Variables"] = json_numbert{
       std::to_string(assertion_stats.sat_hardness.variables.size())};
 
+    json_arrayt assertion_sat_hardness_clause_set_json;
+    for(auto const &clause : assertion_stats.sat_hardness.clause_set)
+    {
+      assertion_sat_hardness_clause_set_json.push_back(
+        json_numbert{std::to_string(clause)});
+    }
+    assertion_hardness_json["ClauseSet"] =
+      assertion_sat_hardness_clause_set_json;
+
     assertion_stats_json["SAT_hardness"] = assertion_hardness_json;
 
     json_stream_array.push_back(assertion_stats_json);

src/solvers/solver_hardness.h

@@ -50,6 +50,7 @@ struct solver_hardnesst
     size_t clauses = 0;
     size_t literals = 0;
     std::unordered_set<size_t> variables = {};
+    std::vector<size_t> clause_set = {};
 
     sat_hardnesst &operator+=(const sat_hardnesst &other);
   };
@@ -105,7 +106,15 @@ struct solver_hardnesst
   /// Called e.g. from the `satcheck_minisat2::lcnf`, this function adds the
   ///   complexity statistics from the last SAT query to the `current_ssa_key`.
   /// \param bv: the clause (vector of literals)
-  void register_clause(const bvt &bv);
+  /// \param cnf: processed clause
+  /// \param cnf_clause_index: index of clause in dimacs output
+  /// \param register_cnf: negation of boolean variable tracking if the clause
+  /// can be eliminated
+  void register_clause(
+    const bvt &bv,
+    const bvt &cnf,
+    const size_t cnf_clause_index,
+    bool register_cnf);
 
   void set_outfile(const std::string &file_name);