Major dead code elimination

src/main/scala/leon/Settings.scala

 package leon
 
 // typically these settings can be changed through some command-line switch.
+// TODO this global object needs to die (or at least clean out of its var's)
 object Settings {
   var experimental : Boolean = false
   var showIDs: Boolean = false
@@ -10,7 +11,6 @@ object Settings {
   var runDefaultExtensions: Boolean = true
   var noForallAxioms: Boolean = true
   var unrollingLevel: Int = 0
-  var zeroInlining : Boolean = true
   var useBAPA: Boolean = false
   var impureTestcases: Boolean = false
   var nbTestcases: Int = 1

src/main/scala/leon/verification/Analysis.scala

@@ -220,116 +220,3 @@ class Analysis(val program : Program, val reporter: Reporter) {
     }
   }
 }
-
-object Analysis {
-  private val keepCallWhenInlined: Boolean = true
-
-  private def defineOneInlining(f : FunctionInvocation) : (Expr, Expr) = {
-    val FunctionInvocation(fd, args) = f
-    val newLetIDs = fd.args.map(a => FreshIdentifier("arg_" + a.id.name, true).setType(a.tpe)).toList
-    val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip newLetIDs.map(Variable(_))) : _*)
-    val newBody = replace(substMap, freshenLocals(matchToIfThenElse(fd.body.get)))
-    val newFunctionCall = FunctionInvocation(fd, newLetIDs.map(Variable(_))).setType(f.getType)
-    val callID = FreshIdentifier("call_" + fd.id.name, true).setType(newBody.getType)
-    val callTree = Let(callID, (newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e)), Variable(callID))
-
-    (Equals(newFunctionCall, Variable(callID)), callTree)
-  }
-
-  private def inlineFunctionCall(f : FunctionInvocation) : Expr = {
-    val FunctionInvocation(fd, args) = f
-    val newLetIDs = fd.args.map(a => FreshIdentifier("arg_" + a.id.name, true).setType(a.tpe)).toList
-    val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip newLetIDs.map(Variable(_))) : _*)
-    val newBody = replace(substMap, freshenLocals(matchToIfThenElse(fd.body.get)))
-    simplifyLets((newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e)))
-  }
-
-  def inlineNonRecursiveFunctions(program: Program, expression: Expr) : Expr = {
-    def applyToCall(e: Expr) : Option[Expr] = e match {
-      case f @ FunctionInvocation(fd, args) if fd.hasImplementation && !program.isRecursive(fd) => Some(inlineFunctionCall(f))
-      case _ => None
-    }
-  
-    var change: Boolean = true
-    var toReturn: Expr = expression
-    while(change) {
-      val (t,c) = searchAndReplaceDFSandTrackChanges(applyToCall)(toReturn)
-      change = c
-      toReturn = t
-    }
-    toReturn
-  }
-
-  def unrollRecursiveFunctions(program: Program, expression: Expr, times: Int) : Expr = {
-    def urf1(expression: Expr, times: Int) : Expr = {
-      var newEqs: List[Expr] = Nil
-
-      def applyToCall(e: Expr) : Option[Expr] = e match {
-        case f @ FunctionInvocation(fd, args) if fd.hasImplementation && program.isRecursive(fd) => {
-          val (newEq, bdy) = defineOneInlining(f)
-          newEqs = newEq :: newEqs
-          Some(bdy)
-        }
-        case _ => None
-      }
-
-      var remaining = if(times < 0) 0 else times
-      var change: Boolean = true
-      var toReturn: Expr = expression
-      while(remaining > 0 && change) {
-        val (t,c) = searchAndReplaceDFSandTrackChanges(applyToCall)(toReturn)
-        change = c
-        toReturn = inlineNonRecursiveFunctions(program, t)
-        remaining = remaining - 1
-      }
-      liftLets(Implies(And(newEqs.reverse), toReturn))
-    }
-
-    def urf2(expression: Expr, times: Int) : Expr = {
-      def applyToCall(e: Expr) : Option[Expr] = e match {
-        case f @ FunctionInvocation(fd, args) if fd.hasImplementation && program.isRecursive(fd) => Some(inlineFunctionCall(f))
-        case _ => None
-      }
-
-      var remaining = if(times < 0) 0 else times
-      var change: Boolean = true
-      var toReturn: Expr = expression
-      while(remaining > 0 && change) {
-        val (t,c) = searchAndReplaceDFSandTrackChanges(applyToCall)(toReturn)
-        change = c
-        toReturn = inlineNonRecursiveFunctions(program, t)
-        remaining = remaining - 1
-      }
-      toReturn
-    }
-
-    if(keepCallWhenInlined)
-      urf1(expression, times)
-    else
-      urf2(expression, times)
-  }
-
-  def inlineContracts(expression: Expr) : Expr = {
-    var trueThings: List[Expr] = Nil
-
-    def applyToCall(e: Expr) : Option[Expr] = e match {
-      case f @ FunctionInvocation(fd, args) if fd.hasPostcondition => {
-        val argsAsLet   = fd.args.map(a => FreshIdentifier("parg_" + a.id.name, true).setType(a.tpe)).toList
-        val argsAsLetVars = argsAsLet.map(Variable(_))
-        val resultAsLet = FreshIdentifier("call_" + fd.id.name, true).setType(f.getType)
-        val newFunCall = FunctionInvocation(fd, argsAsLetVars)
-        val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip argsAsLetVars) : _*) + (ResultVariable() -> Variable(resultAsLet))
-        // this thing is full of let variables! We will need to lift the let
-        // defs. later to make sure they capture this
-        val trueFact = replace(substMap, freshenLocals(fd.postcondition.get))
-        val defList: Seq[(Identifier,Expr)] = ((argsAsLet :+ resultAsLet) zip (args :+ newFunCall))
-        trueThings = trueFact :: trueThings
-        // again: these let defs. need eventually to capture the "true thing"
-        Some(defList.foldRight[Expr](Variable(resultAsLet))((iap, e) => Let(iap._1, iap._2, e)))
-      }
-      case _ => None
-    }
-    val result = searchAndReplaceDFS(applyToCall)(expression)
-    liftLets(Implies(And(trueThings.reverse), result))
-  }
-}

src/main/scala/leon/verification/DefaultTactic.scala

@@ -44,41 +44,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
 
           import Analysis._
 
-          if(Settings.zeroInlining) {
-            withPrec
-          } else {
-            if(Settings.experimental) {
-              reporter.info("Raw:")
-              reporter.info(withPrec)
-              reporter.info("Raw, expanded:")
-              reporter.info(expandLets(withPrec))
-            }
-            reporter.info(" - inlining...")
-            val expr0 = inlineNonRecursiveFunctions(program, withPrec)
-            if(Settings.experimental) {
-              reporter.info("Inlined:")
-              reporter.info(expr0)
-              reporter.info("Inlined, expanded:")
-              reporter.info(expandLets(expr0))
-            }
-            reporter.info(" - unrolling...")
-            val expr1 = unrollRecursiveFunctions(program, expr0, Settings.unrollingLevel)
-            if(Settings.experimental) {
-              reporter.info("Unrolled:")
-              reporter.info(expr1)
-              reporter.info("Unrolled, expanded:")
-              reporter.info(expandLets(expr1))
-            }
-            reporter.info(" - inlining contracts...")
-            val expr2 = inlineContracts(expr1)
-            if(Settings.experimental) {
-              reporter.info("Contract'ed:")
-              reporter.info(expr2)
-              reporter.info("Contract'ed, expanded:")
-              reporter.info(expandLets(expr2))
-            }
-            expr2
-          }
+          withPrec
         }
         if(functionDefinition.fromLoop)
           Seq(new VerificationCondition(theExpr, functionDefinition.parent.get, VCKind.InvariantPost, this.asInstanceOf[DefaultTactic]).setPosInfo(functionDefinition))