Self-contained Stainless releases

sfiruch commented 3 years ago

For our project, we store the compiler toolchain with its dependencies in the source repository for two reasons:

To have bit-exact, reproducible build results
To let developers work on the project without having to set up additional dependencies

Integrating Stainless into our build environment is difficult for these reasons:

Stainless depends on Java (which means that we have to bundle a lot of "baggage")
Stainless doesn't work on reliably Windows natively

Having prebuilt single-file (or few-file) cross-platform builds of Stainless without external dependencies would be valuable for the above reasons. Additionally, I suspect it would lower the entry barrier for interested new users, especially on Windows.

The most promising avenue towards such releases is GraalVM Native Images (Example). Alternatives include jlink and javapackager (Example) and a number of commercial tools. Bundling the Azul Zulu JVM is allowed by their license.

romac commented 3 years ago

At the moment, Stainless and Inox cannot be compiled to a native executable using GrallVM Native Image because they rely on Java reflection in some places, notably for serialization.

The other alternatives should definitely be looked into!

vkuncak commented 3 years ago

I believe one should be able to bundle with OpenJDK as well. Isabelle proof assistant: https://isabelle.in.tum.de/ is an example of a software system that bundles JDK, an IDE, as well as poly/ML compiler and runtime. It's a nearly 400MB bundle for Windows. I am wondering whether docker would not be a more realistic path. We had this working before.

sfiruch commented 3 years ago

@romac GraalVM appears to support reflection in native images: https://www.graalvm.org/reference-manual/native-image/Reflection/. Maybe we're fine, as long as no code generation is involved?

Bundling the JRE should add less than 50MB to Stainless. Having a 100MB Stainless release would be ok for us. I'm less of a fan of Docker, because that adds another dependency (Docker itself) and it is likely to increase the build time. Further, it requires network access (Docker Hub) or the container image +base images in the repo. These will be bigger, as they have to include the JRE plus a distribution as well.

For these reasons, I had hoped we could find a solution without Docker?

sfiruch commented 3 years ago

I can try to work on a prototype of this. @vkuncak and @romac, would you be interested? Or do you want to go in another direction (i.e. docker)?

vkuncak commented 3 years ago

I think it would be cool if a binary version of stainless existed. Also it would be an interesting data point to know whether you succeeded in compiling such a relatively complex build with GraalVM, whatever the outcome.

sfiruch commented 3 years ago

GraalVM runs Stainless fine.
Native Image can compile Stainless, and I got it so far to show the command line help. This is using https://github.com/scalameta/sbt-native-image
Verification with Stainless didn't work though. I couldn't get it to work, due to INOX serialization, not entirely unexpected.
- First, I had to patch out the string concatenation in https://github.com/epfl-lara/inox/blob/1b17cb4d38dfddf16286e3346929b7a05267c380/src/main/scala/inox/utils/Serialization.scala#L465. This worked.
- Next, https://github.com/epfl-lara/inox/blob/1b17cb4d38dfddf16286e3346929b7a05267c380/src/main/scala/inox/utils/Serialization.scala#L235 failed. I couldn't find a workaround.

Next, I'll try jlink/javapackager, which is lower risk.

vkuncak commented 3 years ago

Thanks for the report! Without caching, you may be able to remove this dependency. I look forward to the outcome of javapackager experiment. They seem to support creating .deb packages as well.

samarion commented 3 years ago

We can probably also change Inox serialization to use a macro instead which wouldn't require reflection.

vkuncak commented 3 years ago

Do we use serialization (on the master branch) for anything except caching? Rust front end might also be using it.

@deiruch: did you try verifying something with --vc-cache=false ? Can you show me the full stack trace of what failed?

samarion commented 3 years ago

Do we use serialization (on the master branch) for anything except caching?

I don't think we use it for anything other than caching.

Rust front end might also be using it.

Indeed, it's also used by the Rust frontend but the macro solution can produce/consume the same format as the reflection variant so it shouldn't affect Rust support.

sfiruch commented 3 years ago

@deiruch: did you try verifying something with --vc-cache=false ? Can you show me the full stack trace of what failed?

The initialization of Stainless fails with this stacktrace, with or without --vc-cache=false:

[ Debug  ] com.oracle.svm.core.jdk.UnsupportedFeatureError: Unsupported constructor java.lang.invoke.MemberName.<init>(Class, String, MethodType, byte) is reachable: All methods from java.lang.invoke should have been replaced during image building.
[ Debug  ]      at com.oracle.svm.core.util.VMError.unsupportedFeature(VMError.java:86)
[ Debug  ]      at java.lang.invoke.MemberName.<init>(MemberName.java:812)
[ Debug  ]      at java.lang.invoke.MethodHandles$Lookup.resolveOrFail(MethodHandles.java:2030)
[ Debug  ]      at java.lang.invoke.MethodHandles$Lookup.findVirtual(MethodHandles.java:1194)
[ Debug  ]      at scala.reflect.internal.util.AlmostFinalValue$AlmostFinalCallSite.<clinit>(AlmostFinalValue.java:64)
[ Debug  ]      at com.oracle.svm.core.classinitialization.ClassInitializationInfo.invokeClassInitializer(ClassInitializationInfo.java:351)
[ Debug  ]      at com.oracle.svm.core.classinitialization.ClassInitializationInfo.initialize(ClassInitializationInfo.java:271)
[ Debug  ]      at scala.reflect.internal.util.AlmostFinalValue.<init>(AlmostFinalValue.java:38)
[ Debug  ]      at scala.reflect.internal.util.StatisticsStatics$1.<init>(StatisticsStatics.java:25)
[ Debug  ]      at scala.reflect.internal.util.StatisticsStatics.<clinit>(StatisticsStatics.java:25)
[ Debug  ]      at com.oracle.svm.core.classinitialization.ClassInitializationInfo.invokeClassInitializer(ClassInitializationInfo.java:351)
[ Debug  ]      at com.oracle.svm.core.classinitialization.ClassInitializationInfo.initialize(ClassInitializationInfo.java:271)
[ Debug  ]      at scala.reflect.internal.Symbols$TypeSymbol.<init>(Symbols.scala:3212)
[ Debug  ]      at scala.reflect.internal.Symbols$ClassSymbol.<init>(Symbols.scala:3268)
[ Debug  ]      at scala.reflect.internal.Symbols$ModuleClassSymbol.<init>(Symbols.scala:3436)
[ Debug  ]      at scala.reflect.internal.Symbols$PackageClassSymbol.<init>(Symbols.scala:3485)
[ Debug  ]      at scala.reflect.internal.Mirrors$Roots$RootClass.<init>(Mirrors.scala:307)
[ Debug  ]      at scala.reflect.runtime.JavaMirrors$JavaMirror$$anon$2.<init>(JavaMirrors.scala:80)
[ Debug  ]      at scala.reflect.runtime.JavaMirrors$JavaMirror.RootClass$lzycompute(JavaMirrors.scala:80)
[ Debug  ]      at scala.reflect.runtime.JavaMirrors$JavaMirror.RootClass(JavaMirrors.scala:80)
[ Debug  ]      at scala.reflect.internal.Mirrors$Roots$EmptyPackageClass.<init>(Mirrors.scala:331)
[ Debug  ]      at scala.reflect.runtime.JavaMirrors$JavaMirror$$anon$4.<init>(JavaMirrors.scala:82)
[ Debug  ]      at scala.reflect.runtime.JavaMirrors$JavaMirror.EmptyPackageClass$lzycompute(JavaMirrors.scala:82)
[ Debug  ]      at scala.reflect.runtime.JavaMirrors$JavaMirror.EmptyPackageClass(JavaMirrors.scala:82)
[ Debug  ]      at scala.reflect.runtime.JavaMirrors$JavaMirror.EmptyPackageClass(JavaMirrors.scala:68)
[ Debug  ]      at scala.reflect.internal.Mirrors$RootsBase.init(Mirrors.scala:251)
[ Debug  ]      at scala.reflect.runtime.JavaMirrors.createMirror(JavaMirrors.scala:46)
[ Debug  ]      at scala.reflect.runtime.JavaMirrors.rootMirror(JavaMirrors.scala:53)
[ Debug  ]      at scala.reflect.runtime.JavaMirrors.rootMirror$(JavaMirrors.scala:53)
[ Debug  ]      at scala.reflect.runtime.JavaUniverse.rootMirror$lzycompute(JavaUniverse.scala:30)
[ Debug  ]      at scala.reflect.runtime.JavaUniverse.rootMirror(JavaUniverse.scala:30)
[ Debug  ]      at scala.reflect.runtime.JavaUniverse.rootMirror(JavaUniverse.scala:30)
[ Debug  ]      at scala.reflect.internal.Definitions$DefinitionsClass.ObjectClass$lzycompute(Definitions.scala:295)
[ Debug  ]      at scala.reflect.internal.Definitions$DefinitionsClass.ObjectClass(Definitions.scala:295)
[ Debug  ]      at scala.reflect.internal.Definitions$DefinitionsClass.init(Definitions.scala:1480)
[ Debug  ]      at scala.reflect.runtime.JavaUniverse.init(JavaUniverse.scala:154)
[ Debug  ]      at scala.reflect.runtime.JavaUniverse.<init>(JavaUniverse.scala:93)
[ Debug  ]      at scala.reflect.runtime.package$.universe$lzycompute(package.scala:29)
[ Debug  ]      at scala.reflect.runtime.package$.universe(package.scala:29)
[ Debug  ]      at inox.utils.InoxSerializer$ClassSerializer.<init>(Serialization.scala:235)
[ Debug  ]      at inox.utils.InoxSerializer.classSerializer(Serialization.scala:293)
[ Debug  ]      at inox.utils.InoxSerializer.classSerializers(Serialization.scala:555)
[ Debug  ]      at stainless.utils.StainlessSerializer.classSerializers(Serialization.scala:27)
[ Debug  ]      at stainless.utils.XLangSerializer.classSerializers(Serialization.scala:104)
[ Debug  ]      at inox.utils.InoxSerializer.<init>(Serialization.scala:541)
[ Debug  ]      at stainless.utils.StainlessSerializer.<init>(Serialization.scala:16)
[ Debug  ]      at stainless.utils.XLangSerializer.<init>(Serialization.scala:93)
[ Debug  ]      at stainless.utils.Serializer$.apply(Serialization.scala:207)
[ Debug  ]      at stainless.frontend.SplitCallBack.<init>(SplitCallBack.scala:122)
[ Debug  ]      at stainless.frontend.package$.getCallBack(package.scala:74)
[ Debug  ]      at stainless.frontend.package$.build(package.scala:40)
[ Debug  ]      at stainless.MainHelpers.newCompiler$1(MainHelpers.scala:174)
[ Debug  ]      at stainless.MainHelpers.main(MainHelpers.scala:175)
[ Debug  ]      at stainless.MainHelpers.main$(MainHelpers.scala:152)
[ Debug  ]      at stainless.Main$.main(Main.scala:3)
[ Debug  ]      at stainless.Main.main(Main.scala)

romac commented 3 years ago

What happens if you disable the cache altogether in SplitCallBack, with --vc-cache=false to avoid loading VerificationCache?

(Cannot test it myself at the moment, sorry about that)

diff --git a/core/src/main/scala/stainless/frontend/SplitCallBack.scala b/core/src/main/scala/stainless/frontend/SplitCallBack.scala
index ba669f2e..6d5897ce 100644
--- a/core/src/main/scala/stainless/frontend/SplitCallBack.scala
+++ b/core/src/main/scala/stainless/frontend/SplitCallBack.scala
@@ -119,12 +119,12 @@ class SplitCallBack(components: Seq[Component])(override implicit val context: i
   /** Current set of symbols */
   private var symbols = xt.NoSymbols

-  private val serializer = utils.Serializer(xt)
-  import serializer._
+  // private val serializer = utils.Serializer(xt)
+  // import serializer._

   private val canonization = utils.XlangCanonization(xt)

-  private val cache = new ConcurrentCache[SerializationResult, Future[Report]]
+  // private val cache = new ConcurrentCache[SerializationResult, Future[Report]]

   /******************* Internal Helpers ***********************************************************/

@@ -161,9 +161,11 @@ class SplitCallBack(components: Seq[Component])(override implicit val context: i
     val preSyms = xt.NoSymbols.withClasses(clsDeps).withFunctions(funDeps ++ funs).withTypeDefs(typeDeps)
     val funSyms = Recovery.recover(preSyms)

-    val cf = serialize(funs)(funSyms)
+    // val cf = serialize(funs)(funSyms)
+    // val futureReport = cache.getOrElseUpdate(cf, processFunctionsSymbols(ids, funSyms))
+
+    val futureReport = processFunctionsSymbols(ids, funSyms)

-    val futureReport = cache.getOrElseUpdate(cf, processFunctionsSymbols(ids, funSyms))
     this.synchronized { tasks += futureReport }
   }

@@ -198,9 +200,9 @@ class SplitCallBack(components: Seq[Component])(override implicit val context: i
     Future.sequence(componentReports).map(Report)
   }

-  private def serialize(fds: Set[xt.FunDef])(implicit syms: xt.Symbols): SerializationResult = {
-    serializer.serialize(canonization(syms, fds.toSeq.map(_.id).sorted))
-  }
+  // private def serialize(fds: Set[xt.FunDef])(implicit syms: xt.Symbols): SerializationResult = {
+  //   serializer.serialize(canonization(syms, fds.toSeq.map(_.id).sorted))
+  // }

   private def reportError(pos: inox.utils.Position, msg: String, syms: xt.Symbols): Unit = {
     reporter.error(pos, msg)

romac commented 3 years ago

Before that, you might actually want to try with both --vc-cache=false and --batched, as the BatchedCallBack does not seem to use an internal serialized cache.

romac commented 3 years ago

@deiruch I have given it a try myself and managed to get native image (not a fallback one which still depends on the JDK) without touching the source code, by using the following configuration in the stainless-scalac target:

    Compile / mainClass := Some("stainless.Main"),
    nativeImageVersion := "21.0.0",
    nativeImageOptions := Seq(
      "--no-fallback", // disallow fallback on JDK-dependent image
      "--verbose",
      "--install-exit-handlers",
      "--trace-object-instantiation=sun.awt.dnd.SunDropTargetContextPeer",
      "--trace-object-instantiation=java.awt.color.ICC_ColorSpace",
      "--initialize-at-build-time",
      "--initialize-at-run-time=scala.tools.nsc.profile.RealProfiler$,scala.tools.nsc.profile.ExtendedThreadMxBean,scala.tools.nsc.classpath.FileBasedCache$,sun.awt.dnd,sun.java2d.SurfaceData,apple.security.KeychainStore,z3.Z3Wrapper,z3.scala.package$,com.microsoft.z3.Native",
      "-H:+ReportExceptionStackTraces",
      "--report-unsupported-elements-at-runtime"
    ),

Unfortunately, the native image fails at runtime because of a releaseFence call:

❯ ./frontends/scalac/target/native-image/stainless-scalac --help
[ Error  ] Stainless terminated with an error.
[ Error  ] Debug output is available in the file `stainless-stack-trace.txt`, you may report your issue on https://github.com/epfl-lara/stainless/issues
[ Error  ] You may use --debug=stack to have the stack trace displayed in the output.

❯ cat stainless-stack-trace.txt
java.lang.NoSuchMethodError: java.lang.invoke.VarHandle.releaseFence()
    at java.lang.invoke.MethodHandleNatives.resolve(MethodHandleNatives.java:230)
    at java.lang.invoke.MethodHandle.invokeBasic(MethodHandle.java:75)
    at java.lang.invoke.MethodHandle.invokeBasic(MethodHandle.java:0)
    at java.lang.invoke.LambdaForm$MH/893354869.invoke_MT(LambdaForm$MH)
    at scala.collection.immutable.VM.releaseFence(VM.java:25)
    at scala.collection.immutable.HashMap$HashMapBuilder.result(HashMap.scala:1162)
    at scala.collection.immutable.Map$MapBuilderImpl.result(Map.scala:608)
    at scala.collection.immutable.Map$MapBuilderImpl.result(Map.scala:594)
    at scala.collection.TraversableOnce.toMap(TraversableOnce.scala:373)
    at scala.collection.TraversableOnce.toMap$(TraversableOnce.scala:370)
    at scala.collection.AbstractTraversable.toMap(Traversable.scala:108)
    at stainless.Configuration$.parse(Configuration.scala:77)
    at stainless.Configuration$.$anonfun$parseDefault$1(Configuration.scala:62)
    at scala.Option.map(Option.scala:230)
    at stainless.Configuration$.parseDefault(Configuration.scala:61)
    at stainless.Configuration$.get(Configuration.scala:55)
    at stainless.MainHelpers.getConfigOptions(MainHelpers.scala:120)
    at stainless.MainHelpers.getConfigOptions$(MainHelpers.scala:119)
    at stainless.Main$.getConfigOptions(Main.scala:3)
    at stainless.MainHelpers.processOptions(MainHelpers.scala:135)
    at stainless.MainHelpers.processOptions$(MainHelpers.scala:133)
    at stainless.Main$.processOptions(Main.scala:3)
    at inox.MainHelpers.parseArguments(Main.scala:162)
    at inox.MainHelpers.parseArguments$(Main.scala:144)
    at stainless.Main$.parseArguments(Main.scala:3)
    at inox.MainHelpers.setup(Main.scala:195)
    at inox.MainHelpers.setup$(Main.scala:191)
    at stainless.Main$.setup(Main.scala:3)
    at stainless.MainHelpers.main(MainHelpers.scala:154)
    at stainless.MainHelpers.main$(MainHelpers.scala:152)
    at stainless.Main$.main(Main.scala:3)
    at stainless.Main.main(Main.scala)

I was under the impression that sbt-native-image included a fix for this specific behavior, but it either does not seem to work or this is another kind of problem. I unfortunately don't have time to investigate further at the moment.

vkuncak commented 3 years ago

@deiruch : thanks a lot for checking! It looked close... I am still somewhat surprised by your need to do this for the purpose of a dev tool. I'm sure that are plenty of projects that use Java tools and have at least as strong desire to have reproducible builds. Why stop at JVM; you could be trying to store Windows VM image in a git repo?

vkuncak commented 3 years ago

Thanks to @romac for giving it another try. It sounds like you know of this issue; any pointers? Presumably not every code runs into this; would there be a way to adjust our code base so that this is not triggered; would we need to eliminate some concurrent behavior or some libraries that make use of it?

romac commented 3 years ago

The fix I refer to in the comment above is https://github.com/scala/bug/issues/11634#issuecomment-683285019.

At this time, I unfortunately don't really know how to proceed further. I would suggest opening an issue on the sbt-native-image repository describing the problem above.

sfiruch commented 3 years ago

@deiruch : thanks a lot for checking! It looked close... I am still somewhat surprised by your need to do this for the purpose of a dev tool. I'm sure that are plenty of projects that use Java tools and have at least as strong desire to have reproducible builds. Why stop at JVM; you could be trying to store Windows VM image in a git repo?

You are right of course, there are limits to how far we're willing to go and what is feasible. Our developer baseline is Windows + Visual Studio 2019. We bundle anything else that's required for a build. Currently, the build does not have a dependency on a JVM. We'd like to keep it that way, as every external dependency has to be installed/updated/configured by every developer working with the codebase.

sfiruch commented 3 years ago

I've given up on Graal NativeImage. While I got around the problems reported above and others, I ran into a hard block with the Scala compiler. It appears that NativeImage has some ways to go to support complex reflection scenarios.

Packing it with JPackage works without too much fuss. We will use the resulting package in our project.

@vkuncak is right, there are probably a lot of unnecessary dependencies in the fat jar. For example, I've seen PDF libraries, multiple TrueType fonts, another copy of libz3.so and language dictionaries (for Burmese, for example).

epfl-lara / stainless

Self-contained Stainless releases #922