Merge pull request #474 from viperproject/meilers_opaque_functions

Opaque function annotation

src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala

@@ -55,6 +55,11 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
   private val assumeFunctionsAbove: Const = Const(assumeFunctionsAboveName)
   private val specialRefName = Identifier("special_ref")
   private val specialRef = Const(specialRefName)
+
+  /* limitedPostfix is appended to the actual function name to get the name of the limited function.
+   * It must be a string that cannot appear in Viper identifiers to ensure that we can easily check if a given identifier
+   * refers to the limited version of a function or not.
+   */
   private val limitedPostfix = "'"
   private val triggerFuncPostfix = "#trigger"
   private val triggerFuncNoHeapPostfix = "#triggerStateless"
@@ -226,10 +231,21 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
   override def dummyFuncApp(e: Exp): Exp = FuncApp(dummyTriggerName, Seq(e), Bool)
 
   override def translateFuncApp(fa: sil.FuncApp) = {
-    translateFuncApp(fa.funcname, heapModule.currentStateExps ++ (fa.args map translateExp), fa.typ)
+    val forceNonLimited = fa.info.getUniqueInfo[sil.AnnotationInfo] match {
+      case Some(ai) if ai.values.contains("reveal") => true
+      case _ => false
+    }
+    translateFuncApp(fa.funcname, heapModule.currentStateExps ++ (fa.args map translateExp), fa.typ, forceNonLimited)
   }
-  def translateFuncApp(fname : String, args: Seq[Exp], typ: sil.Type) = {
-    FuncApp(Identifier(fname), args, translateType(typ))
+
+  def translateFuncApp(fname : String, args: Seq[Exp], typ: sil.Type, forceNonLimited: Boolean) = {
+    val func = verifier.program.findFunction(fname)
+    val useLimited = !forceNonLimited && (func.info.getUniqueInfo[sil.AnnotationInfo] match {
+      case Some(ai) if ai.values.contains("opaque") => true
+      case _ => false
+    })
+    val ident = if (useLimited) Identifier(fname + limitedPostfix) else Identifier(fname)
+    FuncApp(ident, args, translateType(typ))
   }
 
   private def assumeFunctionsAbove(i: Int): Exp =
@@ -247,7 +263,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
     val height = heights(f.name)
     val heap = heapModule.staticStateContributions(true, true)
     val args = f.formalArgs map translateLocalVarDecl
-    val fapp = translateFuncApp(f.name, (heap ++ args) map (_.l), f.typ)
+    val fapp = translateFuncApp(f.name, (heap ++ args) map (_.l), f.typ, true)
     val precondition : Exp = f.pres.map(p => translateExp(Expressions.asBooleanExp(p).whenExhaling)) match {
       case Seq() => TrueLit()
       case Seq(p) => p
@@ -286,10 +302,15 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
         case _ => None}.flatten
     }
 
+    // Do not use predicate triggers if the function is annotated as opaque
+    val usePredicateTriggers = f.info.getUniqueInfo[sil.AnnotationInfo] match {
+      case Some(ai) if ai.values.contains("opaque") => false
+      case _ => true
+    }
 
     Axiom(Forall(
       stateModule.staticStateContributions() ++ args,
-      Seq(Trigger(Seq(staticGoodState,fapp))) ++ (if (predicateTriggers.isEmpty) Seq()  else Seq(Trigger(Seq(staticGoodState, triggerFuncStatelessApp(f,args map (_.l))) ++ predicateTriggers))),
+      Seq(Trigger(Seq(staticGoodState,fapp))) ++ (if (!usePredicateTriggers || predicateTriggers.isEmpty) Seq()  else Seq(Trigger(Seq(staticGoodState, triggerFuncStatelessApp(f,args map (_.l))) ++ predicateTriggers))),
       (staticGoodState && assumeFunctionsAbove(height)) ==>
         (precondition ==> (fapp === body))
     ))
@@ -302,10 +323,16 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
    */
   private def transformFuncAppsToLimitedOrTriggerForm(exp: Exp, heightToSkip : Int = -1, triggerForm: Boolean = false): Exp = {
     def transformer: PartialFunction[Exp, Option[Exp]] = {
-      case FuncApp(recf, recargs, t) if recf.namespace == fpNamespace && (heightToSkip == -1 || heights(recf.name) <= heightToSkip) =>
+      case FuncApp(recf, recargs, t) if recf.namespace == fpNamespace &&
+        // recf might refer to a limited function already if the function was marked as opaque.
+        // In that case, we have to drop the limited postfix, since heights contains only the original function names.
+        // We assume that any name that ends with limitedPostfix refers to a limited function (see limitedPostfix above).
+        (heightToSkip == -1 || heights(if (recf.name.endsWith(limitedPostfix)) recf.name.dropRight(limitedPostfix.length) else recf.name) <= heightToSkip) =>
+
+        val baseName = if (recf.name.endsWith(limitedPostfix)) recf.name.dropRight(limitedPostfix.length) else recf.name
         // change all function applications to use the limited form, and still go through all arguments
         if (triggerForm)
-          {val func = verifier.program.findFunction(recf.name)
+          {val func = verifier.program.findFunction(baseName)
             // This was an attempt to make triggering functions heap-independent.
             // But the problem is that, for soundness such a function cannot be equated with/substituted for
             // the original function application, and if nested inside further structure in a trigger, the
@@ -319,9 +346,9 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
             val frameExp : Exp = {
               getFunctionFrame(func, recargs)._1 // the declarations will be taken care of when the function is translated
             }
-            Some(FuncApp(Identifier(func.name + framePostfix), Seq(frameExp) ++ (recargs.tail /* drop Heap argument */ map (_.transform(transformer))), t))
+            Some(FuncApp(Identifier(baseName + framePostfix), Seq(frameExp) ++ (recargs.tail /* drop Heap argument */ map (_.transform(transformer))), t))
 
-          } else Some(FuncApp(Identifier(recf.name + limitedPostfix), recargs map (_.transform(transformer)), t))
+          } else Some(FuncApp(Identifier(baseName + limitedPostfix), recargs map (_.transform(transformer)), t))
 
       case Forall(vs,ts,e,tvs,w) => Some(Forall(vs,ts,e.transform(transformer),tvs,w)) // avoid recursing into the triggers of nested foralls (which will typically get translated via another call to this anyway)
       case Exists(vs,ts,e,w) => Some(Exists(vs,ts,e.transform(transformer),w)) // avoid recursing into the triggers of nested exists (which will typically get translated via another call to this anyway)
@@ -334,7 +361,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
     val height = heights(f.name)
     val heap = heapModule.staticStateContributions(true, true)
     val args = f.formalArgs map translateLocalVarDecl
-    val fapp = translateFuncApp(f.name, (heap ++ args) map (_.l), f.typ)
+    val fapp = translateFuncApp(f.name, (heap ++ args) map (_.l), f.typ, true)
     val precondition : Exp = f.pres.map(p => translateExp(Expressions.asBooleanExp(p).whenExhaling)) match {
       case Seq() => TrueLit()
       case Seq(p) => p
@@ -387,7 +414,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
     val func = Func(name, LocalVarDecl(Identifier("frame"), frameType) ++ realArgs, typ)
     val funcFrameInfo = getFunctionFrame(f, args map (_.l))
     val funcApp = FuncApp(name, funcFrameInfo._1 ++ (realArgs map (_.l)), typ)
-    val funcApp2 = translateFuncApp(f.name, args map (_.l), f.typ)
+    val funcApp2 = translateFuncApp(f.name, args map (_.l), f.typ, true)
     val outerUnfoldings : Seq[Unfolding] = Functions.recursiveCallsAndSurroundingUnfoldings(f).map((pair) => pair._2.headOption).flatten
 
     //only include predicate accesses that do not refer to bound variables