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

package stainless
package extraction
package imperative

import inox._

trait AntiAliasing extends inox.ast.SymbolTransformer with EffectsChecking { self =>
  val trees: Trees
  lazy val s: trees.type = trees
  lazy val t: trees.type = trees
  import trees._

  def transform(syms: Symbols): Symbols = {

    object transformer extends SelfTreeTransformer {
      import syms._

      object effects extends {
        val trees: self.trees.type = self.trees
        val symbols: syms.type = syms
      } with EffectsAnalysis

      //convert a function type with mutable parameters, into a function type
      //that returns the mutable parameters. This makes explicit all possible
      //effects of the function. This should be used for higher order functions
      //declared as parameters.
      def makeFunctionTypeExplicit(tpe: FunctionType): FunctionType = {
        val newReturnTypes = tpe.from.filter(t => effects.isMutableType(t))
        if (newReturnTypes.isEmpty) tpe
        else FunctionType(tpe.from, TupleType(tpe.to +: newReturnTypes))
      }

      // XXX: since LetRec and ApplyLetRec use the fun variable to encode
      //      the type of the corresponding function, we have to make sure to
      //      NOT make that first-class function type explicit!!
      override def transform(e: Expr): Expr = e match {
        case LetRec(fds, body) =>
          LetRec(fds.map { case LocalFunDef(fun, tparams, body) =>
            val FunctionType(from, to) = fun.tpe
            LocalFunDef(
              fun.copy(tpe = FunctionType(from map transform, transform(to))),
              tparams map transform,
              transform(body).asInstanceOf[Lambda]
            )
          }, transform(body)).copiedFrom(e)

        case ApplyLetRec(fun, tparams, tps, args) =>
          val FunctionType(from, to) = fun.tpe
          ApplyLetRec(
            fun.copy(tpe = FunctionType(from map transform, transform(to))),
            tparams map (tp => transform(tp).asInstanceOf[TypeParameter]),
            tps map transform,
            args map transform
          ).copiedFrom(e)

        case _ => super.transform(e)
      }

      override def transform(tpe: Type): Type = tpe match {
        case ft: FunctionType => makeFunctionTypeExplicit(ft)
        case _ => super.transform(tpe)
      }
    }

    val newSyms = syms.transform(transformer)
    import newSyms._

    object effects extends {
      val trees: self.trees.type = self.trees
      val symbols: newSyms.type = newSyms
    } with EffectsAnalysis

    checkEffects(effects)

    type Environment = (Set[ValDef], Map[ValDef, Expr], Map[ValDef, LocalFunDef])
    implicit class EnvWrapper(env: Environment) {
      val (bindings, rewritings, locals) = env
      def withBinding(vd: ValDef): Environment = (bindings + vd, rewritings, locals)
      def withBindings(vds: Iterable[ValDef]): Environment = (bindings ++ vds, rewritings, locals)
      def withRewritings(map: Map[ValDef, Expr]): Environment = (bindings, rewritings ++ map, locals)
      def withLocals(fds: Seq[LocalFunDef]): Environment = (bindings, rewritings, locals ++ fds.map(fd => fd.name -> fd))
    }

    object Environment {
      def empty: Environment = (Set.empty, Map.empty, Map.empty)
    }

    /* Create a new FunDef for a given FunDef in the program.
     * Adapt the signature to express its effects. In case the
     * function has no effect, this will still return the original
     * fundef.
     *
     * Also update FunctionType parameters that need to become explicit
     * about the effect they could perform (returning any mutable type that
     * they receive).
     */
    def updateFunction(fd: FunAbstraction, env: Environment): FunAbstraction = {
      val aliasedParams = effects.getAliasedParams(fd)

      //val newParams = fd.params.map(vd => vd.getType match {
      //  case (ft: FunctionType) => {
      //    val nft = makeFunctionTypeExplicit(ft)
      //    if(ft == nft) vd else ValDef(vd.id.duplicate(tpe = nft))
      //  }
      //  case (cct: CaseClassType) => ccdMap.get(cct.classDef) match {
      //    case Some(ncd) => ValDef(vd.id.duplicate(tpe = ncd.typed))
      //    case None => vd
      //  }
      //  case _ => vd
      //})

      effects.getReturnedExpressions(fd.fullBody).foreach {
        case v: Variable if aliasedParams.contains(v.toVal) =>
          throw FatalError("Cannot return a shared reference to a mutable object")
        case _ => ()
      }

      val newFd = fd.copy(returnType = effects.getReturnType(fd))

      val (specs, body) = exprOps.deconstructSpecs(fd.fullBody)

      if (aliasedParams.isEmpty) {
        val newBody = body.map(makeSideEffectsExplicit(_, fd, env))
        val newFullBody = exprOps.reconstructSpecs(specs, newBody, newFd.returnType)
        if (!newFullBody.getPos.isDefined) newFullBody.setPos(newFd)
        newFd.copy(fullBody = newFullBody)
      } else {
        val freshLocals: Seq[ValDef] = aliasedParams.map(v => v.freshen)
        val freshSubst = aliasedParams.zip(freshLocals).map(p => p._1.toVariable -> p._2.toVariable).toMap

        val newBody = body.map { body =>
          val freshBody = exprOps.replaceFromSymbols(freshSubst, body)
          val explicitBody = makeSideEffectsExplicit(freshBody, fd, env withBindings freshLocals)

          //WARNING: only works if side effects in Tuples are extracted from left to right,
          //         in the ImperativeTransformation phase.
          val finalBody: Expr = Tuple(explicitBody +: freshLocals.map(_.toVariable)).copiedFrom(body)

          freshLocals.zip(aliasedParams).foldLeft(finalBody) {
            (bd, vp) => LetVar(vp._1, vp._2.toVariable, bd).copiedFrom(body)
          }
        }

        val newSpecs = specs.map {
          case exprOps.Postcondition(post @ Lambda(Seq(res), postBody)) =>
            val newRes = ValDef(res.id.freshen, newFd.returnType).copiedFrom(res)
            val newBody = exprOps.replaceSingle(
              aliasedParams.map(vd => (Old(vd.toVariable), vd.toVariable): (Expr, Expr)).toMap ++
              aliasedParams.zipWithIndex.map { case (vd, i) =>
                (vd.toVariable, TupleSelect(newRes.toVariable, i+2).copiedFrom(vd)): (Expr, Expr)
              }.toMap + (res.toVariable -> TupleSelect(newRes.toVariable, 1).copiedFrom(res)),
              postBody
            )

            exprOps.Postcondition(Lambda(Seq(newRes), newBody).copiedFrom(post))

          case spec => spec
        }

        newFd.copy(fullBody = exprOps.reconstructSpecs(newSpecs, newBody, newFd.returnType))
      }
    }

    //We turn all local val of mutable objects into vars and explicit side effects
    //using assignments. We also make sure that no aliasing is being done.
    def makeSideEffectsExplicit(
      body: Expr,
      originalFd: FunAbstraction,
      env: Environment
    ): Expr = {

      object transformer extends inox.transformers.Transformer {
        val trees: self.trees.type = self.trees
        type Env = Environment
        val initEnv: Env = env

        def mapApplication(args: Seq[Expr], nfi: Expr, nfiType: Type, fiEffects: Set[Int], env: Env): Expr = {
          if (fiEffects.nonEmpty) {
            val modifiedArgs: Seq[(Seq[Variable], Expr)] = args.zipWithIndex
              .filter { case (arg, i) => fiEffects.contains(i) }
              .map { arg =>
                val rArg = exprOps.replaceFromSymbols(env.rewritings, arg._1)
                (effects.getReferencedVariables(rArg).filter(v => effects.isMutableType(v.tpe)), rArg)
              }

            val allParams: Seq[Variable] = modifiedArgs.flatMap(_._1)
            val duplicatedParams = allParams.diff(allParams.distinct).distinct
            if (duplicatedParams.nonEmpty)
              throw FatalError("Illegal passing of aliased parameter: " + duplicatedParams.head)

            //TODO: The case f(A(x1,x1,x1)) could probably be handled by forbidding creation at any program point of
            //      case class with multiple refs as it is probably not useful

            val freshRes = ValDef(FreshIdentifier("res"), nfiType)

            val extractResults = Block(
              for (((varsForIndex, expr), index) <- modifiedArgs.zipWithIndex; v <- varsForIndex) yield {
                val resSelect = TupleSelect(freshRes.toVariable, index + 2)
                val newValue = expr match {
                  case cs: ADTSelector =>
                    val (rec, path) = fieldPath(cs)
                    objectUpdateToCopy(rec, path, resSelect)

                  case as: ArraySelect =>
                    val (rec, path) = fieldPath(as)
                    objectUpdateToCopy(rec, path, resSelect)

                  case cc @ ADT(id, tps, es) =>
                    val (_, vd) = (es zip cc.getConstructor.definition.fields).find {
                      case (va: Variable, _) => va == v
                      case _ => false
                    }.get
                    ADTSelector(resSelect, vd.id)
                    //TODO: this only checks for a top level modified id,
                    //      must generalize to any number of nested case classes
                    //      must also handle combination of case class and selectors<commit_msg>Stainless shouldn't complain about passing aliased arguments to pure functions<commit_after>/* Copyright 2009-2018 EPFL, Lausanne */

package stainless
package extraction
package imperative

import inox._

trait AntiAliasing extends inox.ast.SymbolTransformer with EffectsChecking { self =>
  val trees: Trees
  lazy val s: trees.type = trees
  lazy val t: trees.type = trees
  import trees._

  def transform(syms: Symbols): Symbols = {

    object transformer extends SelfTreeTransformer {
      import syms._

      object effects extends {
        val trees: self.trees.type = self.trees
        val symbols: syms.type = syms
      } with EffectsAnalysis

      //convert a function type with mutable parameters, into a function type
      //that returns the mutable parameters. This makes explicit all possible
      //effects of the function. This should be used for higher order functions
      //declared as parameters.
      def makeFunctionTypeExplicit(tpe: FunctionType): FunctionType = {
        val newReturnTypes = tpe.from.filter(t => effects.isMutableType(t))
        if (newReturnTypes.isEmpty) tpe
        else FunctionType(tpe.from, TupleType(tpe.to +: newReturnTypes))
      }

      // XXX: since LetRec and ApplyLetRec use the fun variable to encode
      //      the type of the corresponding function, we have to make sure to
      //      NOT make that first-class function type explicit!!
      override def transform(e: Expr): Expr = e match {
        case LetRec(fds, body) =>
          LetRec(fds.map { case LocalFunDef(fun, tparams, body) =>
            val FunctionType(from, to) = fun.tpe
            LocalFunDef(
              fun.copy(tpe = FunctionType(from map transform, transform(to))),
              tparams map transform,
              transform(body).asInstanceOf[Lambda]
            )
          }, transform(body)).copiedFrom(e)

        case ApplyLetRec(fun, tparams, tps, args) =>
          val FunctionType(from, to) = fun.tpe
          ApplyLetRec(
            fun.copy(tpe = FunctionType(from map transform, transform(to))),
            tparams map (tp => transform(tp).asInstanceOf[TypeParameter]),
            tps map transform,
            args map transform
          ).copiedFrom(e)

        case _ => super.transform(e)
      }

      override def transform(tpe: Type): Type = tpe match {
        case ft: FunctionType => makeFunctionTypeExplicit(ft)
        case _ => super.transform(tpe)
      }
    }

    val newSyms = syms.transform(transformer)
    import newSyms._

    object effects extends {
      val trees: self.trees.type = self.trees
      val symbols: newSyms.type = newSyms
    } with EffectsAnalysis

    checkEffects(effects)

    type Environment = (Set[ValDef], Map[ValDef, Expr], Map[ValDef, LocalFunDef])
    implicit class EnvWrapper(env: Environment) {
      val (bindings, rewritings, locals) = env
      def withBinding(vd: ValDef): Environment = (bindings + vd, rewritings, locals)
      def withBindings(vds: Iterable[ValDef]): Environment = (bindings ++ vds, rewritings, locals)
      def withRewritings(map: Map[ValDef, Expr]): Environment = (bindings, rewritings ++ map, locals)
      def withLocals(fds: Seq[LocalFunDef]): Environment = (bindings, rewritings, locals ++ fds.map(fd => fd.name -> fd))
    }

    object Environment {
      def empty: Environment = (Set.empty, Map.empty, Map.empty)
    }

    /* Create a new FunDef for a given FunDef in the program.
     * Adapt the signature to express its effects. In case the
     * function has no effect, this will still return the original
     * fundef.
     *
     * Also update FunctionType parameters that need to become explicit
     * about the effect they could perform (returning any mutable type that
     * they receive).
     */
    def updateFunction(fd: FunAbstraction, env: Environment): FunAbstraction = {
      val aliasedParams = effects.getAliasedParams(fd)

      //val newParams = fd.params.map(vd => vd.getType match {
      //  case (ft: FunctionType) => {
      //    val nft = makeFunctionTypeExplicit(ft)
      //    if(ft == nft) vd else ValDef(vd.id.duplicate(tpe = nft))
      //  }
      //  case (cct: CaseClassType) => ccdMap.get(cct.classDef) match {
      //    case Some(ncd) => ValDef(vd.id.duplicate(tpe = ncd.typed))
      //    case None => vd
      //  }
      //  case _ => vd
      //})

      effects.getReturnedExpressions(fd.fullBody).foreach {
        case v: Variable if aliasedParams.contains(v.toVal) =>
          throw FatalError("Cannot return a shared reference to a mutable object")
        case _ => ()
      }

      val newFd = fd.copy(returnType = effects.getReturnType(fd))

      val (specs, body) = exprOps.deconstructSpecs(fd.fullBody)

      if (aliasedParams.isEmpty) {
        val newBody = body.map(makeSideEffectsExplicit(_, fd, env))
        val newFullBody = exprOps.reconstructSpecs(specs, newBody, newFd.returnType)
        if (!newFullBody.getPos.isDefined) newFullBody.setPos(newFd)
        newFd.copy(fullBody = newFullBody)
      } else {
        val freshLocals: Seq[ValDef] = aliasedParams.map(v => v.freshen)
        val freshSubst = aliasedParams.zip(freshLocals).map(p => p._1.toVariable -> p._2.toVariable).toMap

        val newBody = body.map { body =>
          val freshBody = exprOps.replaceFromSymbols(freshSubst, body)
          val explicitBody = makeSideEffectsExplicit(freshBody, fd, env withBindings freshLocals)

          //WARNING: only works if side effects in Tuples are extracted from left to right,
          //         in the ImperativeTransformation phase.
          val finalBody: Expr = Tuple(explicitBody +: freshLocals.map(_.toVariable)).copiedFrom(body)

          freshLocals.zip(aliasedParams).foldLeft(finalBody) {
            (bd, vp) => LetVar(vp._1, vp._2.toVariable, bd).copiedFrom(body)
          }
        }

        val newSpecs = specs.map {
          case exprOps.Postcondition(post @ Lambda(Seq(res), postBody)) =>
            val newRes = ValDef(res.id.freshen, newFd.returnType).copiedFrom(res)
            val newBody = exprOps.replaceSingle(
              aliasedParams.map(vd => (Old(vd.toVariable), vd.toVariable): (Expr, Expr)).toMap ++
              aliasedParams.zipWithIndex.map { case (vd, i) =>
                (vd.toVariable, TupleSelect(newRes.toVariable, i+2).copiedFrom(vd)): (Expr, Expr)
              }.toMap + (res.toVariable -> TupleSelect(newRes.toVariable, 1).copiedFrom(res)),
              postBody
            )

            exprOps.Postcondition(Lambda(Seq(newRes), newBody).copiedFrom(post))

          case spec => spec
        }

        newFd.copy(fullBody = exprOps.reconstructSpecs(newSpecs, newBody, newFd.returnType))
      }
    }

    //We turn all local val of mutable objects into vars and explicit side effects
    //using assignments. We also make sure that no aliasing is being done.
    def makeSideEffectsExplicit(
      body: Expr,
      originalFd: FunAbstraction,
      env: Environment
    ): Expr = {

      object transformer extends inox.transformers.Transformer {
        val trees: self.trees.type = self.trees
        type Env = Environment
        val initEnv: Env = env

        def mapApplication(args: Seq[Expr], nfi: Expr, nfiType: Type, fiEffects: Set[Int], env: Env): Expr = {
          if (fiEffects.nonEmpty) {
            val modifiedArgs: Seq[(Seq[Variable], Expr)] = args.zipWithIndex
              .filter { case (arg, i) => fiEffects.contains(i) }
              .map { arg =>
                val rArg = exprOps.replaceFromSymbols(env.rewritings, arg._1)
                (effects.getReferencedVariables(rArg).filter(v => effects.isMutableType(v.tpe)), rArg)
              }

            val allParams: Seq[Variable] = modifiedArgs.flatMap(_._1)
            val duplicatedParams = allParams.diff(allParams.distinct).distinct
            //if (duplicatedParams.nonEmpty)
              //throw MissformedStainlessCode(duplicatedParams.head, "Illegal passing of aliased parameter: " + duplicatedParams.head)

            //TODO: The case f(A(x1,x1,x1)) could probably be handled by forbidding creation at any program point of
            //      case class with multiple refs as it is probably not useful

            val freshRes = ValDef(FreshIdentifier("res"), nfiType)

            val extractResults = Block(
              for (((varsForIndex, expr), index) <- modifiedArgs.zipWithIndex; v <- varsForIndex) yield {
                val resSelect = TupleSelect(freshRes.toVariable, index + 2)
                val newValue = expr match {
                  case cs: ADTSelector =>
                    val (rec, path) = fieldPath(cs)
                    objectUpdateToCopy(rec, path, resSelect)

                  case as: ArraySelect =>
                    val (rec, path) = fieldPath(as)
                    objectUpdateToCopy(rec, path, resSelect)

                  case cc @ ADT(id, tps, es) =>
                    val (_, vd) = (es zip cc.getConstructor.definition.fields).find {
                      case (va: Variable, _) => va == v
                      case _ => false
                    }.get
                    ADTSelector(resSelect, vd.id)
                    //TODO: this only checks for a top level modified id,
                    //      must generalize to any number of nested case classes
                    //      must also handle combination of case class and selectors
{'fraction_non_alphanumeric': 0.09938584779706275, 'fraction_numerical': 0.002136181575433912, 'mean_word_length': 2.31199151043509, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 77, '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': '2405707', 'n_tokens_mistral': 5505, 'n_tokens_neox': 5305, 'n_words': 1487}