<commit_before>/* Copyright 2009-2018 EPFL, Lausanne */

package stainless
package extraction
package imperative

trait GhostChecker { self: EffectsAnalyzer =>
  import s._

  protected def checkGhost(fd: FunDef)(symbols: Symbols, effects: EffectsAnalysis): Unit = {
    import symbols._
    import effects._

    def isGhostEffect(effect: Effect): Boolean = {
      def rec(tpe: Type, path: Seq[Accessor]): Boolean = (tpe, path) match {
        case (adt: ADTType, FieldAccessor(selector) +: rest) =>
          val field = adt.getField(selector).get
          (field.flags contains Ghost) || rec(field.getType, rest)

        case (ArrayType(base), ArrayAccessor(index) +: rest) =>
          rec(base, rest)

        case _ => false
      }

      (effect.receiver.flags contains Ghost) || rec(effect.receiver.getType, effect.target.path)
    }

    def isGhostExpression(e: Expr): Boolean = e match {
      case v: Variable => v.flags contains Ghost

      case FunInvocation(id, _, args, _) =>
        val fun = lookupFunction(id).map(Outer(_)).getOrElse(effects.local(id))
        (fun.flags contains Ghost) ||
        (fun.params zip args).exists { case (vd, arg) =>
          !(vd.flags contains Ghost) && isGhostExpression(arg)
        }

      case ADT(id, _, args) =>
        (getConstructor(id).fields zip args).exists { case (vd, arg) =>
          !(vd.flags contains Ghost) && isGhostExpression(arg)
        }

      case sel @ ADTSelector(e, id) =>
        isGhostExpression(e) ||
        (sel.constructor.fields.find(_.id == id).get.flags contains Ghost)

      case Let(vd, e, b) => isGhostExpression(b)
      case LetVar(vd, e, b) => isGhostExpression(b)
      case Assignment(_, _) => false
      case FieldAssignment(_, _, _) => false
      case Block(_, e) => isGhostExpression(e)

      case Operator(es, _) => es.exists(isGhostExpression)
    }

    def checkFunction(fun: FunAbstraction, inGhost: Boolean): Unit = {
      if (fun.flags contains Ghost) {
        if (!effects(fun).forall(isGhostEffect))
          throw ImperativeEliminationException(fun, s"Ghost function cannot have effect on non-ghost state")
        new Checker(true).traverse(fun)
      } else {
        if (!inGhost && isGhostExpression(fun.fullBody))
          throw ImperativeEliminationException(fun, s"Non-ghost function cannot return a ghost result")
        new Checker(inGhost).traverse(fun)
      }
    }

    class Checker(inGhost: Boolean) extends TreeTraverser {
      override def traverse(expr: Expr): Unit = expr match {
        case Let(vd, e, b) if (vd.flags contains Ghost) && !effects(e).forall(isGhostEffect) =>
          throw ImperativeEliminationException(expr,
            "Right-hand side of ghost variable must only have effects on ghost fields")

        case Let(vd, e, b) if !(vd.flags contains Ghost) && inGhost =>
          val newVd = vd.copy(flags = vd.flags :+ Ghost)
          traverse(Let(newVd, e, exprOps.replaceFromSymbols(Map(vd -> newVd.toVariable), b)).copiedFrom(expr))

        case Let(vd, e, _) if !(vd.flags contains Ghost) && isGhostExpression(e) =>
          throw ImperativeEliminationException(expr,<commit_msg>Don't perform ghost check on synthetic functions<commit_after>/* Copyright 2009-2018 EPFL, Lausanne */

package stainless
package extraction
package imperative

trait GhostChecker { self: EffectsAnalyzer =>
  import s._

  protected def checkGhost(fd: FunDef)(symbols: Symbols, effects: EffectsAnalysis): Unit = {
    import symbols._
    import effects._

    def isGhostEffect(effect: Effect): Boolean = {
      def rec(tpe: Type, path: Seq[Accessor]): Boolean = (tpe, path) match {
        case (adt: ADTType, FieldAccessor(selector) +: rest) =>
          val field = adt.getField(selector).get
          (field.flags contains Ghost) || rec(field.getType, rest)

        case (ArrayType(base), ArrayAccessor(index) +: rest) =>
          rec(base, rest)

        case _ => false
      }

      (effect.receiver.flags contains Ghost) || rec(effect.receiver.getType, effect.target.path)
    }

    def isGhostExpression(e: Expr): Boolean = e match {
      case v: Variable => v.flags contains Ghost

      case FunInvocation(id, _, args, _) =>
        val fun = lookupFunction(id).map(Outer(_)).getOrElse(effects.local(id))
        (fun.flags contains Ghost) ||
        (fun.params zip args).exists { case (vd, arg) =>
          !(vd.flags contains Ghost) && isGhostExpression(arg)
        }

      case ADT(id, _, args) =>
        (getConstructor(id).fields zip args).exists { case (vd, arg) =>
          !(vd.flags contains Ghost) && isGhostExpression(arg)
        }

      case sel @ ADTSelector(e, id) =>
        isGhostExpression(e) ||
        (sel.constructor.fields.find(_.id == id).get.flags contains Ghost)

      case Let(vd, e, b) => isGhostExpression(b)
      case LetVar(vd, e, b) => isGhostExpression(b)
      case Assignment(_, _) => false
      case FieldAssignment(_, _, _) => false
      case Block(_, e) => isGhostExpression(e)

      case Operator(es, _) => es.exists(isGhostExpression)
    }

    def checkFunction(fun: FunAbstraction, inGhost: Boolean): Unit = {
      if (fun.flags contains Synthetic) {
        () // Synthetic functions should always be fine with respect to ghost flow
      } else if (fun.flags contains Ghost) {
        if (!effects(fun).forall(isGhostEffect))
          throw ImperativeEliminationException(fun, s"Ghost function cannot have effect on non-ghost state")
        new Checker(true).traverse(fun)
      } else {
        if (!inGhost && isGhostExpression(fun.fullBody))
          throw ImperativeEliminationException(fun, s"Non-ghost function cannot return a ghost result")
        new Checker(inGhost).traverse(fun)
      }
    }

    class Checker(inGhost: Boolean) extends TreeTraverser {
      override def traverse(expr: Expr): Unit = expr match {
        case Let(vd, e, b) if (vd.flags contains Ghost) && !effects(e).forall(isGhostEffect) =>
          throw ImperativeEliminationException(expr,
            "Right-hand side of ghost variable must only have effects on ghost fields")

        case Let(vd, e, b) if !(vd.flags contains Ghost) && inGhost =>
          val newVd = vd.copy(flags = vd.flags :+ Ghost)
          traverse(Let(newVd, e, exprOps.replaceFromSymbols(Map(vd -> newVd.toVariable), b)).copiedFrom(expr))

        case Let(vd, e, _) if !(vd.flags contains Ghost) && isGhostExpression(e) =>
          throw ImperativeEliminationException(expr,
{'fraction_non_alphanumeric': 0.121661262930369, 'fraction_numerical': 0.0024702794503628223, 'mean_word_length': 2.95, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 43, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7661353', 'n_tokens_mistral': 1997, 'n_tokens_neox': 1947, 'n_words': 519}