Remove Viper field access from trigger with top-level PointerSubscrip…

…t or DerefPointer * Gives a 12% performance improvement on Silicon for examples/concepts/c/structs.c
utwente-fmt · Jul 25, 2024 · a1773b7 · a1773b7
1 parent 401c3d9
commit a1773b7
Showing 1 changed file with 13 additions and 13 deletions.
diff --git a/src/rewrite/vct/rewrite/adt/ImportPointer.scala b/src/rewrite/vct/rewrite/adt/ImportPointer.scala
@@ -286,25 +286,25 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter)
           Nil,
           Nil,
         )(PanicBlame("ptr_deref requires nothing."))
-      case other => rewriteDefault(other)
+      case other => dispatch(other)
     }
   }
 
   override def postCoerce(e: Expr[Pre]): Expr[Post] = {
     implicit val o: Origin = e.o
     e match {
-//      case f @ Forall(_, triggers, _) =>
-//        f.rewrite(triggers =
-//          triggers.map(_.map(rewriteTopLevelPointerSubscriptInTrigger))
-//        )
-//      case s @ Starall(_, triggers, _) =>
-//        s.rewrite(triggers =
-//          triggers.map(_.map(rewriteTopLevelPointerSubscriptInTrigger))
-//        )
-//      case e @ Exists(_, triggers, _) =>
-//        e.rewrite(triggers =
-//          triggers.map(_.map(rewriteTopLevelPointerSubscriptInTrigger))
-//        )
+      case f @ Forall(_, triggers, _) =>
+        f.rewrite(triggers =
+          triggers.map(_.map(rewriteTopLevelPointerSubscriptInTrigger))
+        )
+      case s @ Starall(_, triggers, _) =>
+        s.rewrite(triggers =
+          triggers.map(_.map(rewriteTopLevelPointerSubscriptInTrigger))
+        )
+      case e @ Exists(_, triggers, _) =>
+        e.rewrite(triggers =
+          triggers.map(_.map(rewriteTopLevelPointerSubscriptInTrigger))
+        )
       case sub @ PointerSubscript(pointer, index) =>
         SilverDeref(
           obj =