Fix OOB access (#3383)

In theory_engine.cpp, we were calling `theoryOf()` with
`THEORY_SAT_SOLVER` as the theory id. However, `THEORY_SAT_SOLVER` is
defined as `THEORY_LAST` and thus out-of-bounds of the `d_theoryTable`
defined in theory_engine.h (which is of size `THEORY_LAST`. This commit
adds an assertion that detects the out-of-bound access and introduces a
method to turn a theory id into a string which correctly handles
`THEORY_SAT_SOLVER`.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ac3c63d55e7b7f091ce0cdfab205e5f775ce42ff..2782badcb161a93cbb989c2315ab152fd3531ad9 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -105,6 +105,28 @@ inline Node flattenAnd(Node n){
   return NodeManager::currentNM()->mkNode(kind::AND, out);
 }
 
+/**
+ * Compute the string for a given theory id. In this module, we use
+ * THEORY_SAT_SOLVER as an id, which is not a normal id but maps to
+ * THEORY_LAST. Thus, we need our own string conversion here.
+ *
+ * @param id The theory id
+ * @return The string corresponding to the theory id
+ */
+std::string getTheoryString(theory::TheoryId id)
+{
+  if (id == theory::THEORY_SAT_SOLVER)
+  {
+    return "THEORY_SAT_SOLVER";
+  }
+  else
+  {
+    std::stringstream ss;
+    ss << id;
+    return ss.str();
+  }
+}
+
 theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma,
                                                              ProofRule rule,
                                                              bool removable,
@@ -2065,8 +2087,9 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
     // See if it was sent to the theory by another theory
     PropagationMap::const_iterator find = d_propagationMap.find(toExplain);
     if (find != d_propagationMap.end()) {
-      Debug("theory::explain") << "\tTerm was propagated by another theory (theory = "
-                               << theoryOf((*find).second.theory)->getId() << ")" << std::endl;
+      Debug("theory::explain")
+          << "\tTerm was propagated by another theory (theory = "
+          << getTheoryString((*find).second.theory) << ")" << std::endl;
       // There is some propagation, check if its a timely one
       if ((*find).second.timestamp < toExplain.timestamp) {
         Debug("theory::explain") << "\tRelevant timetsamp, pushing "

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 587d3693ce80c316798ce5c0eff384c062da2d25..e88d3323a86c898504eed57b2bc34edb9e0dd11f 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -797,6 +797,7 @@ public:
    * @returns the theory
    */
   inline theory::Theory* theoryOf(theory::TheoryId theoryId) const {
+    Assert(theoryId < theory::THEORY_LAST);
     return d_theoryTable[theoryId];
   }