avoiding instantiatation for non-constant array index!

tracer-x · Sep 14, 2023 · c4ca337 · c4ca337
1 parent 60c20f9
commit c4ca337
Showing 1 changed file with 15 additions and 2 deletions.
diff --git a/lib/Core/TxTree.cpp b/lib/Core/TxTree.cpp
@@ -3019,9 +3019,9 @@ ref<Expr> TxTreeNode::instantiateWPatSubsumption(ref<Expr> wpInterpolant,
     return wpInterpolant->rebuild(kids);
   }
   case Expr::Sel: {
-    llvm::outs() << "In sel expr\n";
+    // llvm::outs() << "In sel expr\n";
     ref<Expr> kids[2];
-    wpInterpolant->dump();
+    // wpInterpolant->dump();
     if (wpInterpolant->getKid(0)->getKind() == Expr::WPVar) {
       kids[0] = instantiateWPatSubsumption(wpInterpolant->getKid(0), state,
                                            dependency);
@@ -3061,6 +3061,13 @@ ref<Expr> TxTreeNode::instantiateWPatSubsumption(ref<Expr> wpInterpolant,
               ConstantExpr::create(kids[0]->getWidth(), kids[1]->getWidth()),
               ConstantExpr::create(8, kids[1]->getWidth())));
 
+      if (!isa<ConstantExpr>(offset)) {
+        ref<Expr> dummy;
+        klee_warning("instantiateWPatSubsumption: unable to instantiate"
+                     " for non-constant array index!");
+        return dummy;
+      }
+
       assert(isa<ConstantExpr>(offset) &&
              "TxTreeNode::"
              "instantiateWPatSubsumption, offset is "
@@ -3117,6 +3124,12 @@ ref<Expr> TxTreeNode::instantiateWPatSubsumption(ref<Expr> wpInterpolant,
         UDivExpr::create(
             ConstantExpr::create(kids[0]->getWidth(), kids[1]->getWidth()),
             ConstantExpr::create(8, kids[1]->getWidth())));
+    if (!isa<ConstantExpr>(offset)) {
+      ref<Expr> dummy;
+      klee_warning("instantiateWPatSubsumption: unable to instantiate"
+                   " for non-constant array index!");
+      return dummy;
+    }
     assert(isa<ConstantExpr>(offset) && "TxTreeNode::"
                                         "instantiateWPatSubsumption, offset is "
                                         "not a constant value");