Merge pull request #580 from utwente-fmt/silicon-master

Upgrade to viper 21.01, scala 2.13.5, and sbt 1.4.5. Also fix currently present scala and sbt warnings. Finally, add a rewrite rule that transforms multiplications with read into plain "read" terms.

.gitignore

@@ -1,3 +1,4 @@
+# General Java folders
 .metadata/
 .project
 .classpath
@@ -15,13 +16,14 @@ doc/
 tmp
 tmp.*
 vct-tool.jar
-*~
+.bsp/
 
 # Mac specific OS files
 .DS_Store
 
 # Vim swap file
 *.swp
+*~
 
 # Haskell/Cabal rules
 dist

bin/carbon

@@ -5,8 +5,10 @@ BIN=$(dirname $0)
 
 if [[ "$OSTYPE" == "darwin" ]]; then
   Z3="$BIN/../src/main/universal/res/deps/z3/4.8.6/Darwin/x86_64/bin/z3"
+  BOOGIE_EXE="$BIN/../src/main/universal/res/deps/boogie/1.0.0.0-carbon/Darwin/Boogie"
 else
   Z3="$BIN/../src/main/universal/res/deps/z3/4.8.6/Linux/x86_64/bin/z3"
+  BOOGIE_EXE="$BIN/../src/main/universal/res/deps/boogie/1.0.0.0-carbon/Linux/Boogie"
 fi
 
-BOOGIE_EXE="$BIN/../src/main/universal/res/deps/boogie/2.4.1.10503/Boogie.exe" $BIN/run-class viper.carbon.Carbon --z3Exe $Z3 "$@"
+BOOGIE_EXE=$BOOGIE_EXE $BIN/run-class viper.carbon.Carbon --z3Exe $Z3 "$@"

bin/carbon.cmd

@@ -4,4 +4,7 @@ setlocal
 rem %~dp0 is expanded pathname of the current script under NT, i.e. the "bin" directory
 set BIN=%~dp0
 
-call "%BIN%\run-class.cmd" viper.carbon.Carbon %*
+set BOOGIE_EXE=%BIN%\..\src\main\universal\res\deps\boogie\1.0.0.0-carbon\Windows\Boogie.exe
+set Z3="%BIN%\..\src\main\universal\res\deps\z3\4.8.6\Windows NT\intel\bin\z3.exe"
+
+call "%BIN%\run-class.cmd" viper.carbon.Carbon --z3Exe %Z3% %*

bin/run-class

@@ -7,12 +7,9 @@ set -e
 
 BIN=$(dirname $0)
 if [ ! -f "$BIN/.classpath" ] || [ ! -s "$BIN/.classpath" ]; then
-    #    Instruct sbt to export the classpath
-    #    |                               Duplicate stdout to...
-    #    |                               |     grep, filtering _out_ lines starting with "["
-    #    |                               |     |              save that to .classpath
-    #    |                               |     |              |                      display _only_ lines starting with "["
-    sbt "export compile:fullClasspath" | tee >(grep -v "^\\[" > "$BIN/.classpath") | grep "^\\["
+    printf "Extracting classpath from SBT. This might take a moment.\n"
+    sbt --error "Global / printMainClasspath" > "$BIN/.classpath"
+    printf "Classpath extracted\n"
 fi
 
 CLASSPATH=$(cat "$BIN/.classpath")

bin/run-class.cmd

@@ -13,9 +13,7 @@ if not exist "%CPFILE%" (
     echo Extracting classpath from SBT. This might take a moment.
     cd %~dp0..
     rem get classpath from SBT
-    rem |                                extract lines that do NOT start with "[" (using regex)
-    rem |                                |                    save that to .classpath file
-    sbt "export compile:fullClasspath" | findstr /R /V "^\[" > "%CPFILE%"
+    call sbt --error "Global / printMainClasspath" > "%CPFILE%"
     cd %cur%
     echo Classpath extracted
 )

bin/silicon.cmd

@@ -3,5 +3,6 @@ setlocal
 
 rem %~dp0 is expanded pathname of the current script under NT, i.e. the "bin" directory
 set BIN=%~dp0
+set Z3="%BIN%\..\src\main\universal\res\deps\z3\4.8.6\Windows NT\intel\bin\z3.exe"
 
-call "%BIN%\run-class.cmd" viper.silicon.SiliconRunner %*
+call "%BIN%\run-class.cmd" viper.silicon.SiliconRunner --z3Exe %Z3% %*

build.sbt

@@ -1,21 +1,23 @@
 import NativePackagerHelper._
 import sys.process._
+import java.io.File.pathSeparator
 import java.nio.file.{Files, Path, Paths}
 import java.net.URL
 import java.util.Comparator
 import sbt.internal._
 
 ThisBuild / turbo := true // en wat is daar het praktisch nut van?
+ThisBuild / scalaVersion := "2.13.5"
 
 enablePlugins(BuildInfoPlugin)
 enablePlugins(JavaAppPackaging)
 enablePlugins(DebianPlugin)
 
 /* To update viper, replace the hash with the commit hash that you want to point to. It's a good idea to ask people to
  re-import the project into their IDE, as the location of the viper projects below will change. */
-val silver_url = uri("git:https://github.com/viperproject/silver.git#v.20.07-release")
-val carbon_url = uri("git:https://github.com/viperproject/carbon.git#v.20.07-release")
-val silicon_url = uri("git:https://github.com/viperproject/silicon.git#v.20.07-release")
+val silver_url = uri("git:https://github.com/viperproject/silver.git#v.21.01-release")
+val carbon_url = uri("git:https://github.com/viperproject/carbon.git#v.21.01-release")
+val silicon_url = uri("git:https://github.com/viperproject/silicon.git#v.21.01-release")
 
 /*
 buildDepdendencies.classpath contains the mapping from project to a list of its dependencies. The viper projects silver,
@@ -48,11 +50,23 @@ lazy val col = (project in file("col")).dependsOn(hre)
 lazy val parsers = (project in file("parsers")).dependsOn(hre, col)
 lazy val viper_api = (project in file("viper")).dependsOn(hre, col, silver_ref, carbon_ref, silicon_ref)
 
-lazy val vercors = (project in file("."))
-  .dependsOn(hre)
-  .dependsOn(col)
-  .dependsOn(viper_api)
-  .dependsOn(parsers)
+// We fix the scalaVersion of all viper components to be silver's scalaVersion, because
+// it seems that in some cases the scalaVersion of the other components is lost.
+// SBT then assumes the version we want for those components is 2.10, and then
+// suddenly it can't find the dependencies anymore! Smart move, sbt.
+// If Viper ever moves to maven central or some other proper dependency mechanism,
+// this can probably be removed.
+scalaVersion in carbon_ref := (scalaVersion in silver_ref).value
+scalaVersion in silicon_ref := (scalaVersion in silver_ref).value
+scalaVersion in ProjectRef(silver_url, "common") := (scalaVersion in silver_ref).value
+scalaVersion in ProjectRef(carbon_url, "common") := (scalaVersion in silver_ref).value
+scalaVersion in ProjectRef(silicon_url, "common") := (scalaVersion in silver_ref).value
+
+lazy val printMainClasspath = taskKey[Unit]("Prints classpath of main vercors executable")
+
+lazy val vercors: Project = (project in file("."))
+  .dependsOn(hre, col, viper_api, parsers)
+  .aggregate(hre, col, viper_api, parsers)
   .settings(
     name := "Vercors",
     organization := "University of Twente",
@@ -68,13 +82,11 @@ lazy val vercors = (project in file("."))
         |PVL. """.stripMargin.replaceAll("\n", ""),
 
     libraryDependencies += "com.google.code.gson" % "gson" % "2.8.0",
-    libraryDependencies += "org.scalactic" %% "scalactic" % "3.0.1",
-    libraryDependencies += "org.scalatest" %% "scalatest" % "3.0.1" % "test",
-    libraryDependencies += "org.scalamock" %% "scalamock-scalatest-support" % "3.4.2" % Test,
+    libraryDependencies += "org.scalactic" %% "scalactic" % "3.1.2",
+    libraryDependencies += "org.scalatest" %% "scalatest" % "3.1.2" % "test",
+    // libraryDependencies += "org.scalamock" %% "scalamock-scalatest-support" % "3.4.2" % Test,
     libraryDependencies += "org.scala-lang.modules" %% "scala-xml" % "1.2.0",
 
-    scalaVersion := "2.12.10",
-
     scalacOptions in ThisBuild += "-deprecation",
     scalacOptions in ThisBuild += "-feature",
     scalacOptions in ThisBuild += "-unchecked",
@@ -83,7 +95,6 @@ lazy val vercors = (project in file("."))
     javacOptions in Compile += "-Xlint:deprecation",
     javacOptions in Compile += "-Xlint:unchecked",
     javacOptions in Compile += "-deprecation",
-    javacOptions in doc := Seq(),
 
     javaOptions in (Compile, run) += "-J-Xss128M",
     /* The run script from universal can accept both JVM arguments and application (VerCors) arguments. They are
@@ -127,4 +138,15 @@ lazy val vercors = (project in file("."))
     // Other projects, e.g., Carbon or Silicon, can then depend on the Sil test artifact, which
     // allows them to access the Sil test suite.
     publishArtifact in(Test, packageBin) := true,
+
+    cleanFiles += baseDirectory.value / "bin" / ".classpath",
   )
+
+Global / printMainClasspath := {
+    val paths = (vercors / Compile / fullClasspath).value
+    val joinedPaths = paths
+        .map(_.data)
+        .mkString(pathSeparator)
+    println(joinedPaths)
+}
+

col/src/main/java/vct/col/ast/expr/Dereference.scala

@@ -15,6 +15,6 @@ case class Dereference(val obj:ASTNode, val field:String) extends ASTNode with V
     case _ => false
   }
 
-  override def debugTreeChildrenFields(): Iterable[String] = Seq("obj")
-  override def debugTreePropertyFields(): Iterable[String] = Seq("field")
+  override def debugTreeChildrenFields: Iterable[String] = Seq("obj")
+  override def debugTreePropertyFields: Iterable[String] = Seq("field")
 }

col/src/main/java/vct/col/ast/expr/FieldAccess.scala

@@ -17,6 +17,6 @@ case class FieldAccess(val classname:ClassName, val `object`:ASTNode, val name:S
   override def accept_simple[T](visitor:ASTVisitor[T]) = visitor.visit(this)
   override def accept_simple[T](map:ASTMapping[T]) = map.map(this)
 
-  override def debugTreeChildrenFields(): Iterable[String] = Seq("object", "value")
-  override def debugTreePropertyFields(): Iterable[String] = Seq("classname", "name")
+  override def debugTreeChildrenFields: Iterable[String] = Seq("object", "value")
+  override def debugTreePropertyFields: Iterable[String] = Seq("classname", "name")
 }

col/src/main/java/vct/col/ast/expr/OperatorExpression.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.expr
 
-import scala.collection.JavaConverters._
+import scala.jdk.CollectionConverters._
 import hre.ast.FileOrigin
 import vct.col.ast.generic.ASTNode
 import vct.col.ast.stmt.composite.Hole
@@ -59,6 +59,6 @@ case class OperatorExpression(val operator:StandardOperator, val args:List[ASTNo
   override def accept_simple[T](m:ASTMapping[T]) = handle_standard(() => m.map(this))
   override def isa(op:StandardOperator) = op == operator
 
-  override def debugTreeChildrenFields(): Iterable[String] = Seq("args")
-  override def debugTreePropertyFields(): Iterable[String] = Seq("operator")
+  override def debugTreeChildrenFields: Iterable[String] = Seq("args")
+  override def debugTreePropertyFields: Iterable[String] = Seq("operator")
 }

col/src/main/java/vct/col/ast/expr/StandardProcedure.scala

@@ -18,6 +18,6 @@ case class StandardProcedure(val operator:StandardOperator) extends ASTNode with
   override def accept_simple[T](v:ASTVisitor[T]) = handle_standard(() => v.visit(this))
   override def accept_simple[T](m:ASTMapping[T]) = handle_standard(() => m.map(this))
 
-  override def debugTreeChildrenFields(): Iterable[String] = Seq()
-  override def debugTreePropertyFields(): Iterable[String] = Seq("operator")
+  override def debugTreeChildrenFields: Iterable[String] = Seq()
+  override def debugTreePropertyFields: Iterable[String] = Seq("operator")
 }

col/src/main/java/vct/col/ast/expr/constant/BooleanValue.scala

@@ -1,5 +1,8 @@
 package vct.col.ast.expr.constant
 
+import scala.annotation.nowarn
+
+@nowarn("msg=.*comparing values of types Any and .* using `equals`.*")
 case class BooleanValue(val value:Boolean) extends Value {
   override def toString() = if (value) "true" else "false"
   override def equals(o:Any) = o.equals(value)

col/src/main/java/vct/col/ast/expr/constant/ConstantExpression.scala

@@ -39,6 +39,6 @@ case class ConstantExpression(val value:Value) extends ASTNode with VisitorHelpe
     case _ => ast.equals(value)
   }
 
-  override def debugTreeChildrenFields(): Iterable[String] = Seq()
-  override def debugTreePropertyFields(): Iterable[String] = Seq("value")
+  override def debugTreeChildrenFields: Iterable[String] = Seq()
+  override def debugTreePropertyFields: Iterable[String] = Seq("value")
 }

col/src/main/java/vct/col/ast/expr/constant/DoubleValue.scala

@@ -1,6 +1,9 @@
 package vct.col.ast.expr.constant
 
+import scala.annotation.nowarn
+
 /** Represents a constant double with value "`value`". */
+@nowarn("msg=.*comparing values of types Any and .* using `equals`.*")
 case class DoubleValue(val value:Double) extends Value {
   override def equals(a:Any) = a.equals(value)
   override def toString() = value.toString()

col/src/main/java/vct/col/ast/expr/constant/IntegerValue.scala

@@ -1,6 +1,9 @@
 package vct.col.ast.expr.constant
 
+import scala.annotation.nowarn
+
 /** Represents a constant integer with value "`value`". */
+@nowarn("msg=.*comparing values of types Any and .* using `equals`.*")
 case class IntegerValue(val value:Int) extends Value {
   override def toString() = Integer.toString(value)
   override def equals(o:Any) = o.equals(value)

col/src/main/java/vct/col/ast/expr/constant/LongValue.scala

@@ -1,5 +1,8 @@
 package vct.col.ast.expr.constant
 
+import scala.annotation.nowarn
+
+@nowarn("msg=.*comparing values of types Any and .* using `equals`.*")
 case class LongValue(val value:Long) extends Value {
   override def equals(obj:Any) = obj.equals(this.value)
   override def toString() = value.toString()

col/src/main/java/vct/col/ast/expr/constant/StructValue.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.expr.constant
 
-import scala.collection.JavaConverters._
+import scala.jdk.CollectionConverters._
 import vct.col.ast.`type`.Type
 import vct.col.ast.expr.ExpressionNode
 import vct.col.ast.generic.ASTNode
@@ -30,6 +30,6 @@ case class StructValue(val `type`:Type, val map:Map[String,Integer], val values:
   override def accept_simple[T](v:ASTVisitor[T]) = handle_standard(() => v.visit(this))
   override def accept_simple[T](m:ASTMapping[T]) = handle_standard(() => m.map(this))
 
-  override def debugTreeChildrenFields(): Iterable[String] = Seq("type", "map", "values")
-  override def debugTreePropertyFields(): Iterable[String] = Seq()
+  override def debugTreeChildrenFields: Iterable[String] = Seq("type", "map", "values")
+  override def debugTreePropertyFields: Iterable[String] = Seq()
 }

col/src/main/java/vct/col/ast/generic/ASTList.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.generic
 
-import scala.collection.JavaConverters._
+import scala.jdk.CollectionConverters._
 import scala.collection.mutable.ArrayBuffer
 
 class ASTList extends ASTSequence[ASTList] {
@@ -12,7 +12,7 @@ class ASTList extends ASTSequence[ASTList] {
   }
 
   override def add(item:ASTNode) = add(Option(item))
-  override def iterator = list.toIterator.asJava
+  override def iterator = list.iterator.asJava
   override def get(i:Int) = list.apply(i)
   override def size = list.size
 }

col/src/main/java/vct/col/ast/generic/DebugNode.scala

@@ -3,6 +3,7 @@ package vct.col.ast.generic
 import scala.collection.Iterable
 
 trait DebugNode {
+  // Assumed to be side-effect free, so no parentheses.
   def debugTreeChildrenFields: Iterable[String]
   def debugTreePropertyFields: Iterable[String]
 

col/src/main/java/vct/col/ast/generic/DebugSession.scala

@@ -8,7 +8,7 @@ import hre.lang.System.Output
 import scala.collection.mutable
 import scala.collection.mutable.ArrayBuffer
 
-import scala.collection.JavaConverters._
+import scala.jdk.CollectionConverters._
 
 case class DebugSession() {
   val seen: mutable.HashSet[AnyRef] = mutable.HashSet()

col/src/main/java/vct/col/ast/langspecific/c/CFunctionType.scala

@@ -3,6 +3,7 @@ package vct.col.ast.langspecific.c
 import vct.col.ast.`type`.Type
 import vct.col.ast.stmt.decl.{DeclarationStatement, ProgramUnit}
 import vct.col.ast.util.{ASTMapping, ASTMapping1, ASTVisitor, TypeMapping}
+import scala.jdk.CollectionConverters._
 
 case class ParamSpec(t: Option[Type], name: Option[String]) {
   def asDecl: Option[DeclarationStatement] = (t, name) match {
@@ -30,6 +31,8 @@ case class CFunctionType(params: Seq[ParamSpec], returnType: Type) extends Type
     case _ => false
   }
 
+  def paramsJava: java.util.List[ParamSpec] = params.asJava
+
   override protected def accept_simple[T](map: TypeMapping[T]): T = map.map(this)
   override def accept_simple[T](visitor: ASTVisitor[T]): Unit = visitor.visit(this)
   override def accept_simple[T](map: ASTMapping[T]): T = map.map(this)

col/src/main/java/vct/col/ast/langspecific/c/OpenMP.scala

@@ -4,10 +4,15 @@ import vct.col.ast.generic.ASTNode
 import vct.col.ast.stmt.composite.{BlockStatement, LoopStatement}
 import vct.col.ast.stmt.decl.Contract
 import vct.col.ast.util.{ASTMapping, ASTMapping1, ASTVisitor}
+import scala.jdk.CollectionConverters._
 
 sealed trait OMPOption
-case class OMPPrivate(names: Seq[String]) extends OMPOption
-case class OMPShared(names: Seq[String]) extends OMPOption
+case class OMPPrivate(names: Seq[String]) extends OMPOption {
+  def namesJava: java.util.List[String] = names.asJava
+}
+case class OMPShared(names: Seq[String]) extends OMPOption {
+  def namesJava: java.util.List[String] = names.asJava
+}
 case object OMPNoWait extends OMPOption
 case class OMPSimdLen(len: Int) extends OMPOption
 case class OMPNumThreads(len: Int) extends OMPOption
@@ -37,7 +42,9 @@ sealed abstract class OMPBlock(block: BlockStatement) extends ASTNode {
   override def debugTreePropertyFields: Iterable[String] = Seq()
 }
 
-case class OMPParallel(block: BlockStatement, options: Seq[OMPOption], contract: Contract) extends OMPBlock(block)
+case class OMPParallel(block: BlockStatement, options: Seq[OMPOption], contract: Contract) extends OMPBlock(block) {
+  def optionsJava: java.util.List[OMPOption] = options.asJava
+}
 case class OMPSection(block: BlockStatement) extends OMPBlock(block)
 case class OMPSections(block: BlockStatement) extends OMPBlock(block)
 
@@ -62,6 +69,12 @@ sealed abstract class OMPLoop(val loop: LoopStatement, val options: Seq[OMPOptio
   override def debugTreePropertyFields: Iterable[String] = Seq()
 }
 
-case class OMPFor(override val loop: LoopStatement, override val options: Seq[OMPOption]) extends OMPLoop(loop, options)
-case class OMPParallelFor(override val loop: LoopStatement, override val options: Seq[OMPOption]) extends OMPLoop(loop, options)
-case class OMPForSimd(override val loop: LoopStatement, override val options: Seq[OMPOption]) extends OMPLoop(loop, options)
+case class OMPFor(override val loop: LoopStatement, override val options: Seq[OMPOption]) extends OMPLoop(loop, options) {
+  def optionsJava: java.util.List[OMPOption] = options.asJava
+}
+case class OMPParallelFor(override val loop: LoopStatement, override val options: Seq[OMPOption]) extends OMPLoop(loop, options) {
+  def optionsJava: java.util.List[OMPOption] = options.asJava
+}
+case class OMPForSimd(override val loop: LoopStatement, override val options: Seq[OMPOption]) extends OMPLoop(loop, options) {
+  def optionsJava: java.util.List[OMPOption] = options.asJava
+}