Merge branch 'master' into trace-ensuring-newspecs

.gitignore

@@ -107,3 +107,8 @@ project/project/
 
 # ripgrep
 .rgignore
+
+# C files
+*.c
+*.h
+*.out

.larabot.conf

@@ -1,6 +1,6 @@
 commands = [
     "sbt -batch -Dparallel=5 test"
-    "sbt -batch -Dparallel=5 \"it:testOnly stainless.GhostRewriteSuite stainless.TypeCheckerLibrarySuite stainless.ScalacExtractionSuite stainless.LibrarySuite stainless.verification.SMTZ3TypeCheckerSuite stainless.verification.SMTZ3VerificationSuite stainless.verification.SMTZ3UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.StrictArithmeticSuite stainless.verification.CodeGenVerificationSuite stainless.verification.SMTCVC4TypeCheckerSuite stainless.verification.SMTCVC4VerificationSuite stainless.verificatoin.SMTCVC4UncheckedSuite stainless.termination.TerminationSuite\""
+    "sbt -batch -Dparallel=5 \"it:testOnly stainless.GhostRewriteSuite stainless.GenCSuite stainless.TypeCheckerLibrarySuite stainless.ScalacExtractionSuite stainless.LibrarySuite stainless.verification.SMTZ3TypeCheckerSuite stainless.verification.SMTZ3VerificationSuite stainless.verification.SMTZ3UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.StrictArithmeticSuite stainless.verification.CodeGenVerificationSuite stainless.verification.SMTCVC4TypeCheckerSuite stainless.verification.SMTCVC4VerificationSuite stainless.verificatoin.SMTCVC4UncheckedSuite stainless.termination.TerminationSuite\""
 ]
 
 nightly {

bin/package-standalone.sh

@@ -29,20 +29,15 @@ LOG="./package-standalone.log"
 
 # -----
 
-RST="\e[0m"
-BLD="\e[1m"
-RED="\e[31m"
-GRN="\e[32m"
-
 function info {
-  echo -e "$1 $RST"
+  echo "$1 $(tput sgr 0)"
 }
 function okay {
-  info "${GRN}    Done."
+  info "$(tput setaf 2)    Done."
   echo -e "-----\n" >> $LOG
 }
 function fail {
-  info "${RED}    Failed. See log ($LOG) for details."
+  info "$(tput setaf 1)   Failed. See log ($LOG) for details."
   exit 1
 }
 
@@ -138,25 +133,25 @@ function package {
 
 echo -e "Starting packaging version $STAINLESS_VERSION on $(date).\n-----\n" | tee -a $LOG
 
-info "${BLD}[] Checking required tools..."
+info "$(tput bold)[] Checking required tools..."
 check_tools
 
-info "${BLD}[] Assembling fat jar..."
+info "$(tput bold)[] Assembling fat jar..."
 if [ -f "$STAINLESS_JAR_PATH" ]; then
   info "  (JAR already exists, skipping sbt assembly step.)" && okay
 else
   $SBT_PACKAGE >> $LOG && okay || fail
 fi
 
-info "${BLD}\n[] Downloading Z3 binaries..."
+info "$(tput bold)[] Downloading Z3 binaries..."
 fetch_z3 "linux" $Z3_LINUX_NAME
 fetch_z3 "mac" $Z3_MAC_NAME
 
-info "${BLD}\n[] Packaging..."
+info "$(tput bold)[] Packaging..."
 package "linux" $SCALAZ3_JAR_LINUX_PATH
 package "mac" $SCALAZ3_JAR_MAC_PATH
 
-info "\n${BLD}[] Cleaning up..."
+info "$(tput bold)[] Cleaning up..."
 rm -r "$TMP_DIR" && okay
 
-info "\n${BLD}Packaging successful."
+info "$(tput bold)Packaging successful."

build.sbt

@@ -233,7 +233,7 @@ val scriptSettings: Seq[Setting[_]] = Seq(
 def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
 
 // lazy val inox = RootProject(file("../inox"))
-lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "22de8d6b6af51fbe09bca2fc26dbdd596de8e3e8")
+lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "7e72d941e748df31b966bbb5726ade447673b199")
 //lazy val dotty = ghProject("git://github.com/lampepfl/dotty.git", "b3194406d8e1a28690faee12257b53f9dcf49506")
 
 // Allow integration test to use facilities from regular tests

core/src/main/scala/stainless/ast/Definitions.scala

@@ -83,6 +83,12 @@ trait Definitions extends inox.ast.Definitions { self: Trees =>
     }
 
     val lookup = new Lookup
+
+    override protected def simplestValue(tpe: Type, seen: Set[Type], allowSolver: Boolean, inLambda: Boolean)
+                                        (implicit sem: symbols.Semantics, ctx: inox.Context): Expr = tpe match {
+      case ArrayType(base) => FiniteArray(Seq(), base)
+      case _ => super.simplestValue(tpe, seen, allowSolver, inLambda)
+    }
   }
 
   implicit class StainlessFunDef(fd: FunDef) {

core/src/main/scala/stainless/ast/ExprOps.scala

@@ -275,7 +275,7 @@ trait ExprOps extends inox.ast.ExprOps { self =>
     withSpec(expr, pred.filterNot(_.body == BooleanLiteral(true)).map(Postcondition).toLeft(PostconditionKind))
 
   final def withMeasure(expr: Expr, measure: Option[Expr]): Expr =
-    withSpec(expr, measure.map(Measure).toLeft(MeasureKind))
+    withSpec(expr, measure.map(expr => Measure(expr).setPos(expr)).toLeft(MeasureKind))
 
   /** Adds a body to a specification
     *

core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala

@@ -233,6 +233,9 @@ trait AntiAliasing
                     val (recCond, recSelect) = select(field.tpe, ClassSelector(AsInstanceOf(expr, fieldClassType).setPos(expr), id).setPos(pos), xs)
                     (and(condition, recCond), recSelect)
 
+                  case (tt: TupleType, TupleFieldAccessor(idx) +: xs) =>
+                    select(tt.bases(idx - 1), TupleSelect(expr, idx).setPos(pos), xs)
+
                   case (ArrayType(base), ArrayAccessor(idx) +: xs) =>
                     select(base, ArraySelect(expr, idx).setPos(pos), xs)
 
@@ -578,6 +581,15 @@ trait AntiAliasing
             else Annotated(ClassSelector(casted, vd.id).copiedFrom(receiver), Seq(Unchecked)).copiedFrom(receiver)
           }).copiedFrom(newValue)
 
+        case TupleFieldAccessor(index) :: fs =>
+          val tt @ TupleType(_) = receiver.getType
+          val r = rec(Annotated(TupleSelect(receiver, index).copiedFrom(newValue), Seq(Unchecked)).copiedFrom(newValue), fs)
+
+          Tuple((1 to tt.dimension).map { i =>
+            if (i == index) r
+            else Annotated(TupleSelect(receiver, i).copiedFrom(receiver), Seq(Unchecked)).copiedFrom(receiver)
+          }).copiedFrom(newValue)
+
         case ArrayAccessor(index) :: fs =>
           val r = rec(Annotated(ArraySelect(receiver, index).copiedFrom(newValue), Seq(Unchecked)).copiedFrom(newValue), fs)
           ArrayUpdated(receiver, index, r).copiedFrom(newValue)

core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala

@@ -179,6 +179,10 @@ trait EffectsAnalyzer extends oo.CachingPhase {
     def asString(implicit ctx: inox.Context) = s"MutableMapAccessor(${index.asString})"
   }
 
+  case class TupleFieldAccessor(index: Int) extends Accessor {
+    def asString(implicit ctx: inox.Context) = s"TupleFieldAccessor($index)"
+  }
+
   case class Path(path: Seq[Accessor]) {
     def :+(elem: Accessor): Path = Path(path :+ elem)
     def +:(elem: Accessor): Path = Path(elem +: path)
@@ -210,6 +214,8 @@ trait EffectsAnalyzer extends oo.CachingPhase {
           rec(xs1, xs2)
         case (ClassFieldAccessor(id1) +: xs1, ClassFieldAccessor(id2) +: xs2) if id1 == id2 =>
           rec(xs1, xs2)
+        case (TupleFieldAccessor(id1) +: xs1, TupleFieldAccessor(id2) +: xs2) if id1 == id2 =>
+          rec(xs1, xs2)
         case (MutableMapAccessor(_) +: xs1, MutableMapAccessor(_) +: xs2) =>
           rec(xs1, xs2)
         case _ => false
@@ -225,6 +231,7 @@ trait EffectsAnalyzer extends oo.CachingPhase {
       else path.map {
         case ADTFieldAccessor(id) => s".${id.asString}"
         case ClassFieldAccessor(id) => s".${id.asString}"
+        case TupleFieldAccessor(idx) => s"._$idx"
         case ArrayAccessor(idx) => s"(${idx.asString})"
         case MutableMapAccessor(idx) => s"(${idx.asString})"
       }.mkString("")
@@ -239,6 +246,9 @@ trait EffectsAnalyzer extends oo.CachingPhase {
       case ADTFieldAccessor(id) +: xs =>
         wrap(ADTSelector(expr, id), xs)
 
+      case TupleFieldAccessor(idx) +: xs =>
+        wrap(TupleSelect(expr, idx), xs)
+
       case ClassFieldAccessor(id) +: xs =>
         def asClassType(tpe: Type): Option[ClassType] = tpe match {
           case ct: ClassType => Some(ct)
@@ -297,6 +307,9 @@ trait EffectsAnalyzer extends oo.CachingPhase {
           val field = syms.classForField(ct, id).flatMap(_.fields.find(_.id == id))
           field.isDefined && rec(field.get.getType, xs)
 
+        case (tt: TupleType, TupleFieldAccessor(idx) +: xs) =>
+          0 < idx && idx <= tt.dimension && rec(tt.bases(idx - 1), xs)
+
         case (ArrayType(base), ArrayAccessor(idx) +: xs) =>
           rec(base, xs)
 
@@ -331,11 +344,14 @@ trait EffectsAnalyzer extends oo.CachingPhase {
     override def toString: String = asString
   }
 
+  // getTargets(expr, Seq()) returns the set of targets such that after `var x = expr`,
+  // the modifications on `x` will result in modifications on these targets
   def getTargets(expr: Expr, path: Seq[Accessor])(implicit symbols: Symbols): Set[Target] = expr match {
     case _ if variablesOf(expr).forall(v => !symbols.isMutableType(v.tpe)) => Set.empty
     case v: Variable => Set(Target(v, None, Path(path)))
     case ADTSelector(e, id) => getTargets(e, ADTFieldAccessor(id) +: path)
     case ClassSelector(e, id) => getTargets(e, ClassFieldAccessor(id) +: path)
+    case TupleSelect(e, idx) => getTargets(e, TupleFieldAccessor(idx) +: path)
     case ArraySelect(a, idx) => getTargets(a, ArrayAccessor(idx) +: path)
     case MutableMapApply(a, idx) => getTargets(a, MutableMapAccessor(idx) +: path)
     case MutableMapDuplicate(m) => getTargets(m, path)
@@ -354,6 +370,13 @@ trait EffectsAnalyzer extends oo.CachingPhase {
         Set.empty
     }
 
+    case Tuple(exprs) => path match {
+      case TupleFieldAccessor(idx) +: rest =>
+        getTargets(exprs(idx - 1), rest)
+      case _ =>
+        Set.empty
+    }
+
     case FiniteArray(elems, _) => path match {
       case ArrayAccessor(bv: BVLiteral) +: rest =>
         val i = bv.toBigInt.toInt
@@ -390,7 +413,8 @@ trait EffectsAnalyzer extends oo.CachingPhase {
       } yield target
 
     case fi: FunctionInvocation if !symbols.isRecursive(fi.id) =>
-      BodyWithSpecs(symbols.simplifyLets(fi.inlined))
+      if (fi.tfd.flags.contains(IsPure)) Set.empty
+      else BodyWithSpecs(symbols.simplifyLets(fi.inlined))
         .bodyOpt
         .map(getTargets(_, path))
         .getOrElse(Set.empty)
@@ -403,6 +427,7 @@ trait EffectsAnalyzer extends oo.CachingPhase {
     case AsInstanceOf(e, _) => getTargets(e, path)
     case Old(_) => Set.empty
     case Snapshot(_) => Set.empty
+    case FreshCopy(_) => Set.empty
 
     case ArrayLength(_) => Set.empty
 

core/src/main/scala/stainless/extraction/imperative/EffectsChecker.scala

@@ -289,8 +289,9 @@ trait EffectsChecker { self: EffectsAnalyzer =>
         case MutableMapDuplicate(IsTyped(_, MutableMapType(from, to))) =>
           !isMutableType(from) && !isMutableType(to)
 
-        // snapshots are fresh
-        case Snapshot(e) => true
+        // snapshots & fresh copies are fresh
+        case Snapshot(_) => true
+        case FreshCopy(_) => true
 
         // For `Let`, it is safe to add `vd` as a fresh binding because we disallow
         // `FieldAssignments` with non-fresh expressions in `check(fd: FunAbstraction)` above.

core/src/main/scala/stainless/extraction/imperative/GhostChecker.scala

@@ -29,6 +29,9 @@ trait GhostChecker { self: EffectsAnalyzer =>
         case (ArrayType(base), ArrayAccessor(index) +: rest) =>
           rec(base, rest)
 
+        case (tt: TupleType, TupleFieldAccessor(index) +: rest) =>
+          rec(tt.bases(index - 1), rest)
+
         case _ => false
       }
 
@@ -44,7 +47,8 @@ trait GhostChecker { self: EffectsAnalyzer =>
       // Measures are also considered ghost, as they are never executed
       case Decreases(_, body) => isGhostExpression(body)
 
-      case Snapshot(e) => true
+      case Snapshot(_) => true
+      case FreshCopy(e) => isGhostExpression(e)
 
       case FunInvocation(id, _, args, _) =>
         val fun = lookupFunction(id).map(Outer(_)).getOrElse(analysis.local(id))

core/src/main/scala/stainless/extraction/imperative/ImperativeCodeElimination.scala

@@ -63,6 +63,7 @@ trait ImperativeCodeElimination
           (UnitLiteral(), scope, rhsFun + (v -> newVd.toVariable))
 
         case Snapshot(e) => toFunction(e)
+        case FreshCopy(e) => toFunction(e)
 
         case ite @ IfExpr(cond, tExpr, eExpr) =>
           val (cRes, cScope, cFun) = toFunction(cond)
@@ -159,7 +160,7 @@ trait ImperativeCodeElimination
           val finalFun = fun ++ lastFun
           (
             replaceFromSymbols(finalFun, lastRes),
-            (body: Expr) => scope(replaceFromSymbols(fun, lastScope(body))),
+            (body: Expr) => scope(replaceFromSymbols(fun, lastScope(body)).setPos(expr)),
             finalFun
           )
 
@@ -361,11 +362,10 @@ trait ImperativeCodeElimination
             val newScope = (body: Expr) => argScope(replaceFromSymbols(argFun, accScope(body)))
             (argVal +: accArgs, newScope, argFun ++ accFun)
           }
-
-          (recons(recArgs), scope, fun)
+          (recons(recArgs).setPos(n), scope, fun)
       }
 
-      (res.copiedFrom(expr), scope, fun)
+      (res.ensurePos(expr.getPos), scope, fun)
     }
 
     def requireRewriting(expr: Expr) = expr match {
@@ -374,6 +374,7 @@ trait ImperativeCodeElimination
       case (e: LetVar) => true
       case (e: Old) => true
       case (e: Snapshot) => true
+      case (e: FreshCopy) => true
       case _ => false
     }
 

core/src/main/scala/stainless/extraction/imperative/ReturnElimination.scala

@@ -134,7 +134,7 @@ trait ReturnElimination
 
           val newPost =
             t.Lambda(
-              Seq(t.ValDef.fresh("_unused", t.UnitType().copiedFrom(wh)).copiedFrom(wh)),
+              Seq(t.ValDef.fresh("_res", t.UnitType().copiedFrom(wh)).copiedFrom(wh)),
               t.and(
                 transformedInv.getOrElse(t.BooleanLiteral(true).copiedFrom(wh)),
                 t.Not(getFunctionalResult(transformedCond).copiedFrom(cond)).copiedFrom(cond),
@@ -411,7 +411,7 @@ trait ReturnElimination
           }
           processBlockExpressions(es :+ last)
 
-        case (_: s.Lambda | _: s.Forall | _: s.Old | _: s.Snapshot | _: s.Choose) =>
+        case (_: s.Lambda | _: s.Forall | _: s.Old | _: s.Snapshot | _: s.FreshCopy | _: s.Choose) =>
           SimpleWhileTransformer.transform(expr)
 
         case _ if exprHasReturn(expr) =>

core/src/main/scala/stainless/extraction/imperative/TransformerWithType.scala

@@ -70,6 +70,9 @@ trait TransformerWithType extends oo.TransformerWithType {
     case s.Snapshot(e) =>
       t.Snapshot(transform(e, tpe)).copiedFrom(expr)
 
+    case s.FreshCopy(e) =>
+      t.FreshCopy(transform(e, tpe)).copiedFrom(expr)
+
     case s.BoolBitwiseAnd(lhs, rhs) =>
       t.BoolBitwiseAnd(transform(lhs, s.BooleanType()), transform(rhs, s.BooleanType())).copiedFrom(expr)
 

core/src/main/scala/stainless/extraction/imperative/Trees.scala

@@ -134,6 +134,11 @@ trait Trees extends oo.Trees with Definitions { self =>
     protected def computeType(implicit s: Symbols): Type = e.getType
   }
 
+  /** copy primitive, like `Snapshot` but usable outside of the ghost context. Mostly to work-around anti-aliasing. */
+  case class FreshCopy(e: Expr) extends Expr with CachingTyped {
+    protected def computeType(implicit s: Symbols): Type = e.getType
+  }
+
   /** $encodingof `a & b` for Boolean; desuggared to { val l = lhs; val r = rhs; l && r } when removing imperative style. */
   case class BoolBitwiseAnd(lhs: Expr, rhs: Expr) extends Expr with CachingTyped {
     protected def computeType(implicit s: Symbols): Type =
@@ -265,6 +270,9 @@ trait Printer extends oo.Printer {
     case Snapshot(e) =>
       p"snapshot($e)"
 
+    case FreshCopy(e) =>
+      p"freshCopy($e)"
+
     case BoolBitwiseAnd(lhs, rhs) => optP {
       p"$lhs & $rhs"
     }
@@ -365,6 +373,9 @@ trait TreeDeconstructor extends oo.TreeDeconstructor {
     case s.Snapshot(e) =>
       (Seq(), Seq(), Seq(e), Seq(), Seq(), (_, _, es, _, _) => t.Snapshot(es.head))
 
+    case s.FreshCopy(e) =>
+      (Seq(), Seq(), Seq(e), Seq(), Seq(), (_, _, es, _, _) => t.FreshCopy(es.head))
+
     case _ => super.deconstruct(e)
   }
 

core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala

@@ -68,14 +68,22 @@ trait FunctionInlining extends CachingPhase with IdentitySorts { self =>
         }
 
         val pre = specced.specs.filter(spec => spec.kind == LetKind || spec.kind == PreconditionKind)
+        val maxPre = pre.count(_.kind == PreconditionKind)
         def addPreconditionAssertions(e: Expr): Expr = {
-          pre.foldRight(e) {
-            case (spec @ LetInSpec(vd, e0), acc) => Let(vd, annotated(e0, Unchecked), acc).setPos(fi)
-            case (spec @ Precondition(cond), acc) =>
+          pre.foldRight((e, maxPre)) {
+            case (spec @ LetInSpec(vd, e0), (acc, i)) => (Let(vd, annotated(e0, Unchecked), acc).setPos(fi), i)
+            case (spec @ Precondition(cond), (acc, i)) =>
+              val num = if (i == 1) "" else s" ($i)"
               // the assertion is not itself marked `Unchecked` (as it needs to be checked)
               // but `cond` should not generate additional VCs and is marked with `Unchecked`
-              Assert(annotated(cond, Unchecked), Some("Inlined precondition of " + tfd.id.asString), acc).copiedFrom(fi)
-          }
+              val condVal = ValDef.fresh("cond", BooleanType()).setPos(fi)
+              (
+                Let(condVal, annotated(cond, Unchecked),
+                  Assert(condVal.toVariable.setPos(fi), Some(s"Inlined precondition$num of " + tfd.id.asString), acc
+                ).copiedFrom(fi)).copiedFrom(fi),
+                i-1
+              )
+          }._1
         }
 
         val post = specced.getSpec(PostconditionKind)
@@ -84,7 +92,11 @@ trait FunctionInlining extends CachingPhase with IdentitySorts { self =>
           // It is thus inlined into an assertion here.
           case Some(Lambda(Seq(vd), post)) if isSynthetic =>
             val err = Some("Inlined postcondition of " + tfd.id.name)
-            Let(vd, e, Assert(annotated(post, Unchecked), err, vd.toVariable.copiedFrom(fi)).copiedFrom(fi)).copiedFrom(fi)
+            val postVal = ValDef.fresh("post", BooleanType()).setPos(fi)
+            Let(vd, e,
+              Let(postVal, annotated(post, Unchecked),
+                Assert(postVal.toVariable.setPos(fi), err, vd.toVariable.copiedFrom(fi)
+            ).copiedFrom(fi)).copiedFrom(fi)).copiedFrom(fi)
           case Some(Lambda(Seq(vd), post)) =>
             Let(vd, e, Assume(annotated(post, Unchecked), vd.toVariable.copiedFrom(fi)).copiedFrom(fi)).copiedFrom(fi)
           case _ => e