Merge pull request #1252 from utwente-fmt/unsound-auto-value

AutoValue unsoundness, Test Suite runner, Paths with spaces
utwente-fmt · Sep 27, 2024 · 3cb0d92 · 3cb0d92
2 parents cd30c48 + 7c7470d
commit 3cb0d92
Show file tree

Hide file tree

Showing 11 changed files with 134 additions and 41 deletions.
diff --git a/bin/bashComplete b/bin/bashComplete
@@ -1,5 +1,5 @@
 #!/bin/bash
 set -e
-ROOT=$(dirname $(dirname $(readlink -f $0)))
-(cd $ROOT; ./mill -j 0 vercors.main.runScript)
-$ROOT/out/vercors/main/runScript.dest/bashOptions "$@"
+ROOT="$(dirname "$(dirname "$(readlink -f $0)")")"
+(cd "$ROOT"; ./mill -j 0 vercors.main.runScript)
+"$ROOT/out/vercors/main/runScript.dest/bashOptions" "$@"
diff --git a/bin/carbon b/bin/carbon
@@ -1,7 +1,7 @@
 #!/bin/bash
 set -e
-ROOT=$(dirname $(dirname $(readlink -f $0)))
-(cd $ROOT; ./mill -j 0 vercors.main.runScript)
+ROOT="$(dirname "$(dirname "$(readlink -f $0)")")"
+(cd "$ROOT"; ./mill -j 0 vercors.main.runScript)
 
 
 if [[ "$OSTYPE" == "darwin" ]]; then
@@ -12,4 +12,4 @@ else
   BOOGIE_EXE="$ROOT/res/universal/deps/unix/boogie/Boogie"
 fi
 
-BOOGIE_EXE=$BOOGIE_EXE $ROOT/out/vercors/main/runScript.dest/carbon --z3Exe $Z3 "$@"
+BOOGIE_EXE="$BOOGIE_EXE" "$ROOT/out/vercors/main/runScript.dest/carbon" --z3Exe $Z3 "$@"
diff --git a/bin/silicon b/bin/silicon
@@ -1,12 +1,12 @@
 #!/bin/bash
 set -e
-ROOT=$(dirname $(dirname $(readlink -f $0)))
-(cd $ROOT; ./mill -j 0 vercors.main.runScript)
+ROOT="$(dirname "$(dirname "$(readlink -f $0)")")"
+(cd "$ROOT"; ./mill -j 0 vercors.main.runScript)
 
 if [[ "$OSTYPE" == "darwin" ]]; then
   Z3="$ROOT/res/universal/deps/darwin/z3/bin/z3"
 else
   Z3="$ROOT/res/universal/deps/unix/z3/bin/z3"
 fi
 
-$ROOT/out/vercors/main/runScript.dest/silicon --logLevel ERROR --z3Exe $Z3 "$@"
+"$ROOT/out/vercors/main/runScript.dest/silicon" --logLevel ERROR --z3Exe "$Z3" "$@"
diff --git a/bin/testSuite b/bin/testSuite
@@ -0,0 +1,5 @@
+#!/bin/bash
+set -e
+ROOT="$(dirname "$(dirname "$(readlink -f $0)")")"
+(cd "$ROOT"; ./mill -j 0 vercors.allTests.runScript)
+"$ROOT/out/vercors/allTests/runScript.dest/testSuite" -o "$@"
diff --git a/bin/testSuite.cmd b/bin/testSuite.cmd
@@ -0,0 +1,11 @@
+@echo off
+setlocal
+
+set BIN=%~dp0
+set ROOT=%BIN%..
+
+pushd %ROOT%
+call mill vercors.allTests.runScript
+popd
+
+"%ROOT%\out\vercors\allTests\runScript.dest\testSuite" %*
diff --git a/bin/vct b/bin/vct
@@ -1,5 +1,5 @@
 #!/bin/bash
 set -e
-ROOT=$(dirname $(dirname $(readlink -f $0)))
-(cd $ROOT; ./mill -j 0 vercors.main.runScript)
-$ROOT/out/vercors/main/runScript.dest/vercors "$@"
+ROOT="$(dirname "$(dirname "$(readlink -f $0)")")"
+(cd "$ROOT"; ./mill -j 0 vercors.main.runScript)
+"$ROOT/out/vercors/main/runScript.dest/vercors" "$@"
diff --git a/build.sc b/build.sc
@@ -859,6 +859,12 @@ object vercors extends Module {
 
     override def mainClass = T { Some("org.scalatest.tools.Runner") }
 
+    override def runScriptClasses = T {
+      val paths = Seq(col.test.compile(), viperApi.test.compile(), main.test.compile())
+      Map (
+      "testSuite" -> ("org.scalatest.tools.Runner -R " + paths.map(_.classes.path.toString().replace(" ", "\\\\ ")).mkString("\""," ", "\""))
+    ) }
+
     def test(args: String*) = T.command {
       col.test.test(args: _*)
       viperApi.test.test(args: _*)

diff --git a/examples/concepts/autovalue/combination.pvl b/examples/concepts/autovalue/combination.pvl
@@ -0,0 +1,13 @@
+class A {
+    int f;
+}
+
+requires AutoValue(a.f);
+requires Perm(a.f, write);
+void foo(A a) {
+}
+
+void bar() {
+    A a = new A();
+    foo(a);
+}
diff --git a/mill-build/util/src/util/JavaModule.scala b/mill-build/util/src/util/JavaModule.scala
@@ -16,7 +16,7 @@ trait JavaModule extends BaseJavaModule {
 
   def unixClassPathArgumentFile =
     T {
-      val cpString = classPathFileElements().mkString(":")
+      val cpString = classPathFileElements().mkString("\"", ":", "\"")
       val cpArg = "-cp " + cpString
       os.write(T.dest / "classpath", cpArg)
       T.dest / "classpath"
@@ -40,7 +40,7 @@ trait JavaModule extends BaseJavaModule {
 
   def windowsClassPathArgumentFile =
     T {
-      val cpString = classPathFileElements().mkString(";")
+      val cpString = classPathFileElements().mkString("\"", ";", "\"")
       val cpArg = "-cp " + cpString
       os.write(T.dest / "classpath", cpArg)
       T.dest / "classpath"
@@ -57,12 +57,12 @@ trait JavaModule extends BaseJavaModule {
         val header = "@ 2>/dev/null # 2>nul & echo off & goto BOF"
         val unix = Seq(
           ":",
-          s"java ${forkArgs().mkString(" ")} @${unixClassPathArgumentFile()} $mainClass $quote$$@$quote",
+          s"java ${forkArgs().mkString(" ")} $quote@${unixClassPathArgumentFile()}$quote $mainClass $quote$$@$quote",
           "exit",
         )
         val batch = Seq(
           ":BOF",
-          s"java ${forkArgs().mkString(" ")} @${windowsClassPathArgumentFile()} $mainClass %*",
+          s"java ${forkArgs().mkString(" ")} $quote@${windowsClassPathArgumentFile()}$quote $mainClass %*",
           "exit /B %errorlevel%",
         )
         val script =

diff --git a/src/rewrite/vct/rewrite/EncodeAutoValue.scala b/src/rewrite/vct/rewrite/EncodeAutoValue.scala
@@ -38,6 +38,20 @@ case object EncodeAutoValue extends RewriterBuilder {
       )
   }
 
+  case class CombinedAutoValue(autoNode: Node[_], regularNode: Node[_])
+      extends UserError {
+    override def code: String = "combinedAutoValue"
+
+    override def text: String =
+      vct.result.Message.messagesInContext(
+        (
+          regularNode.o,
+          "The AutoValue resource may not be combined with permission resources for what is potentially the same field...",
+        ),
+        (autoNode.o, "The AutoValue resource was here"),
+      )
+  }
+
   private sealed class PreOrPost
 
   private final case class InPrecondition() extends PreOrPost
@@ -55,9 +69,14 @@ case class EncodeAutoValue[Pre <: Generation]() extends Rewriter[Pre] {
 
   import EncodeAutoValue._
 
-  private val conditionContext
-      : ScopedStack[(PreOrPost, mutable.ArrayBuffer[(Expr[Pre], Expr[Post])])] =
-    ScopedStack()
+  private val conditionContext: ScopedStack[
+    (
+        PreOrPost,
+        mutable.ArrayBuffer[(Expr[Pre], Expr[Post])],
+        mutable.HashSet[Location[Post]],
+        mutable.HashSet[Location[Post]],
+    )
+  ] = ScopedStack()
   private val inFunction: ScopedStack[Unit] = ScopedStack()
 
   private lazy val anyRead: Function[Post] = {
@@ -103,14 +122,14 @@ case class EncodeAutoValue[Pre <: Generation]() extends Rewriter[Pre] {
     val postMap = mutable.ArrayBuffer[(Expr[Pre], Expr[Post])]()
     node.rewrite(
       requires =
-        conditionContext.having((InPrecondition(), preMap)) {
-          dispatch(node.requires)
-        },
+        conditionContext.having(
+          (InPrecondition(), preMap, mutable.HashSet(), mutable.HashSet())
+        ) { dispatch(node.requires) },
       ensures = {
         val predicate =
-          conditionContext.having(((InPostcondition(), postMap))) {
-            dispatch(node.ensures)
-          }
+          conditionContext.having(
+            ((InPostcondition(), postMap, mutable.HashSet(), mutable.HashSet()))
+          ) { dispatch(node.ensures) }
         val filtered = preMap.filterNot(pre =>
           postMap.exists(post => {
             Compare.isIsomorphic(pre._1, post._1, matchFreeVariables = true)
@@ -143,7 +162,7 @@ case class EncodeAutoValue[Pre <: Generation]() extends Rewriter[Pre] {
                 (SilverFieldLocation(x.get, field), obj)
             }
           conditionContext.top match {
-            case (InPrecondition(), preMap) =>
+            case (InPrecondition(), preMap, avLocations, locations) =>
               preMap +=
                 ((
                   e,
@@ -155,6 +174,10 @@ case class EncodeAutoValue[Pre <: Generation]() extends Rewriter[Pre] {
                     ),
                   ),
                 ))
+              avLocations += postLoc
+              if (locations.contains(postLoc)) {
+                throw CombinedAutoValue(e, locations.find(_ == postLoc).get)
+              }
               PolarityDependent(
                 onInhale = Perm(
                   postLoc,
@@ -164,8 +187,12 @@ case class EncodeAutoValue[Pre <: Generation]() extends Rewriter[Pre] {
                   !ForPerm(Seq(x), genericLocation, ff) &*
                     !ForPerm(Seq(x), genericLocation, x.get !== obj),
               )
-            case (InPostcondition(), postMap) =>
+            case (InPostcondition(), postMap, avLocations, locations) =>
               postMap += ((e, tt))
+              avLocations += postLoc
+              if (locations.contains(postLoc)) {
+                throw CombinedAutoValue(e, locations.find(_ == postLoc).get)
+              }
               PolarityDependent(
                 onInhale =
                   !ForPerm(Seq(x), genericLocation, ff) &*
@@ -177,6 +204,18 @@ case class EncodeAutoValue[Pre <: Generation]() extends Rewriter[Pre] {
               )
           }
         }
+        case Perm(loc, perm) => {
+          val postLoc = dispatch(loc)
+          conditionContext.top match {
+            case (_, _, avLocations, locations) => {
+              locations += postLoc;
+              if (avLocations.contains(postLoc)) {
+                throw CombinedAutoValue(avLocations.find(_ == postLoc).get, e)
+              }
+              Perm(postLoc, dispatch(perm))
+            }
+          }
+        }
         case Let(binding, value, main) =>
           variables.scope {
             val top = conditionContext.pop()
@@ -185,9 +224,12 @@ case class EncodeAutoValue[Pre <: Generation]() extends Rewriter[Pre] {
               finally { conditionContext.push(top) }
             val mMap = mutable.ArrayBuffer[(Expr[Pre], Expr[Post])]()
             val m =
-              conditionContext.having((conditionContext.top._1, mMap)) {
-                dispatch(main)
-              }
+              conditionContext.having((
+                conditionContext.top._1,
+                mMap,
+                conditionContext.top._3,
+                conditionContext.top._4,
+              )) { dispatch(main) }
             if (mMap.isEmpty) { Let(b, v, m) }
             else {
               mMap.foreach(postM =>
@@ -215,13 +257,19 @@ case class EncodeAutoValue[Pre <: Generation]() extends Rewriter[Pre] {
           val lMap = mutable.ArrayBuffer[(Expr[Pre], Expr[Post])]()
           val rMap = mutable.ArrayBuffer[(Expr[Pre], Expr[Post])]()
           val l =
-            conditionContext.having((conditionContext.top._1, lMap)) {
-              dispatch(left)
-            }
+            conditionContext.having((
+              conditionContext.top._1,
+              lMap,
+              conditionContext.top._3,
+              conditionContext.top._4,
+            )) { dispatch(left) }
           val r =
-            conditionContext.having((conditionContext.top._1, rMap)) {
-              dispatch(right)
-            }
+            conditionContext.having((
+              conditionContext.top._1,
+              rMap,
+              conditionContext.top._3,
+              conditionContext.top._4,
+            )) { dispatch(right) }
           if (lMap.isEmpty && rMap.isEmpty)
             Select(c, l, r)
           else {
@@ -268,9 +316,12 @@ case class EncodeAutoValue[Pre <: Generation]() extends Rewriter[Pre] {
             try { dispatch(left) }
             finally { conditionContext.push(top); }
           val r =
-            conditionContext.having((conditionContext.top._1, rMap)) {
-              dispatch(right)
-            }
+            conditionContext.having((
+              conditionContext.top._1,
+              rMap,
+              conditionContext.top._3,
+              conditionContext.top._4,
+            )) { dispatch(right) }
           if (rMap.nonEmpty) {
             conditionContext.top._1 match {
               case InPrecondition() =>
@@ -299,8 +350,14 @@ case class EncodeAutoValue[Pre <: Generation]() extends Rewriter[Pre] {
           try {
             val lMap = mutable.ArrayBuffer[(Expr[Pre], Expr[Post])]()
             val rMap = mutable.ArrayBuffer[(Expr[Pre], Expr[Post])]()
-            val l = conditionContext.having((top._1, lMap)) { dispatch(left) }
-            val r = conditionContext.having((top._1, rMap)) { dispatch(right) }
+            val l =
+              conditionContext.having((top._1, lMap, top._3, top._4)) {
+                dispatch(left)
+              }
+            val r =
+              conditionContext.having((top._1, rMap, top._3, top._4)) {
+                dispatch(right)
+              }
             top._2.addAll(lMap)
             top._2.addAll(rMap)
             Star(l, r)

diff --git a/test/main/vct/test/integration/examples/AutoValueSpec.scala b/test/main/vct/test/integration/examples/AutoValueSpec.scala
@@ -5,4 +5,5 @@ import vct.test.integration.helper.VercorsSpec
 class AutoValueSpec extends VercorsSpec {
   vercors should verify using silicon example "concepts/autovalue/copy.pvl"
   vercors should verify using silicon example "concepts/autovalue/leak.pvl"
+  vercors should error withCode "combinedAutoValue" example "concepts/autovalue/combination.pvl"
 }