Building PSharp-as-language samples fails on macOS

[fniksic]

I am having issues trying to build PSharp-as-language samples on macOS. Building PSharp itself works without problems by executing:

dotnet build -c Release PSharp.sln

I can then build PSharp-as-framework samples by executing:

cd Samples
dotnet build -c Release Samples.Framework.sln

However, if I try executing

dotnet build -c Release Samples.Language.sln

I get a number of error messages of the following form:

/Users/filip/PSharp/Samples/Language/build.props(3,3): error MSB4019: The imported project "/Users/filip/PSharp/bin/net46/PSharp.vs2017.targets" was not found. Confirm that the path in the <Import> declaration is correct, and that the file exists on disk. [/Users/filip/PSharp/Samples/Language/MultiPaxos/MultiPaxos.csproj]

The csproj files reference the file Samples/Language/build.props, which in turn references a non-existing file bin/net46/PSharp.vs2017.targets. As far as I understand, the file is supposed to be copied from Tools/Compilation/SyntaxRewriter/PSharp.vs2017.targets, and it's purpose is to define a build task that runs PSharpSyntaxRewriter to rewrite PSharp files into C# files. So I tried to manually copy the file. There's a number of smaller changes I had to do as well:

• The file Samples/Language/build.props unconditionally defines net46 as the target framework. I changed this as in Samples/Framework/build.props to target netcoreapp2.1 on macOS.
• The PSharp build process produces PSharpSyntaxRewriter for netstandard2.0, so I copied the PSharp.vs2017.targets to bin/netstandard2.0 and made the corresponding change in Samples/Language/build.props.
• The file PSharp.vs2017.targets references the assembly file PSharpSyntaxRewriter.exe, but the build process produces PSharpSyntaxRewriter.dll on macOS, so I changed the file to reference the DLL.

Unfortunately, the build still doesn't go through. Here's the sample message I get:

/Users/filip/PSharp/bin/netstandard2.0/PSharp.vs2017.targets(4,5): error MSB4062: The "Microsoft.PSharp.Rewriter" task could not be loaded from the assembly /Users/filip/PSharp/bin/netstandard2.0/./PSharpSyntaxRewriter.dll.  Confirm that the <UsingTask> declaration is correct, that the assembly and all its dependencies are available, and that the task contains a public class that implements Microsoft.Build.Framework.ITask. [/Users/filip/PSharp/Samples/Language/MultiPaxos/MultiPaxos.csproj]

I tried to run the syntax rewriter manually just to see if I can rewrite s PSharp file. It turns out this fails as well:

$ mono bin/netstandard2.0/PSharpSyntaxRewriter.dll Samples/Language/PingPong/Server.psharp 
Assembly '/Users/filip/PSharp/bin/netstandard2.0/PSharpSyntaxRewriter.dll' doesn't have an entry point.

I guess there is some problem with the way dependencies are defined in Tools/Compilation/SyntaxRewriter/SyntaxRewriter.csproj. I will continue investigating the issue, but if someone with a better understanding of the build process knows how to quickly make this work, I would appreciate the help.

[akashlal]

I don't think LanguageServices will build on mac because of Roslyn dependencies that are unavailable for .net core. Is that right, @pdeligia?

[pdeligia]

That is correct. Right now, if you want to use P# with .NET core you need to use it as a library, and thus can only use the framework samples.

Basically, the .NET core port of P# is incomplete. The core library and production runtime as well as the testing services are fully supported in .NET core, but the language services, compiler and syntax rewriter (that the language-version samples depend upon) are not fully ported to .NET core yet. If I remember correctly, there were some API incompatibilities (because we are using some libraries that were not supported in .NET core when I worked on the port). There should be workarounds (or perhaps these APIs are now supported), but we have not looked into this lately.

Saying this, we are happy to accept contributions to finish these parts of the .NET core port, but we are also planning to do this (but on low priority for now).

[fniksic]

When you talk about API incompatibilities, are you referring to MSBuildWorkspace, i.e., Roslyn issue 17974?

The funny thing is, a month or two ago I was playing with the language samples, and I am pretty sure I managed to somehow get them to compile and run. I am not sure how that was possible, because indeed now I see LanguageServices depend on MSBuildWorkspace, which is apparently still incompatible with .NET Core.

[fniksic]

I made some progress on this. The good news is that the Roslyn daily build from the Roslyn MyGet feed is compatible with .NET core 2.1. So after bumping the Roslyn version and adjusting the dependencies and target frameworks, I can build all components of PSharp, including the compiler and the syntax rewriter. There are some failing unit tests in StaticAnalysis mostly caused by latent bugs that perhaps did not manifest themselves before (like dereferencing null references), but this is a topic for a separate issue report.

What I am facing now are assembly loading issues. Namely, when building the language samples, MSBuild loads PSharpSyntaxRewriter.dll, but doesn't know where to find its dependencies:

/Users/filip/PSharp/bin/netcoreapp2.1/PSharp.vs2017.targets(4,5): error MSB4018: The "Rewriter" task failed unexpectedly. [/Users/filip/PSharp/Samples/Language/PingPong/PingPong.csproj]
/Users/filip/PSharp/bin/netcoreapp2.1/PSharp.vs2017.targets(4,5): error MSB4018: System.IO.FileNotFoundException: Could not load file or assembly 'Microsoft.CodeAnalysis, Version=3.1.0.0, Culture=neutral, PublicKeyToken=31bf3856ad364e35'. The system cannot find the file specified. [/Users/filip/PSharp/Samples/Language/PingPong/PingPong.csproj]
/Users/filip/PSharp/bin/netcoreapp2.1/PSharp.vs2017.targets(4,5): error MSB4018:  [/Users/filip/PSharp/Samples/Language/PingPong/PingPong.csproj]
/Users/filip/PSharp/bin/netcoreapp2.1/PSharp.vs2017.targets(4,5): error MSB4018: File name: 'Microsoft.CodeAnalysis, Version=3.1.0.0, Culture=neutral, PublicKeyToken=31bf3856ad364e35' [/Users/filip/PSharp/Samples/Language/PingPong/PingPong.csproj]
/Users/filip/PSharp/bin/netcoreapp2.1/PSharp.vs2017.targets(4,5): error MSB4018:    at Microsoft.PSharp.SyntaxRewriter.Translate(String text, String& errors, Version csVersion) [/Users/filip/PSharp/Samples/Language/PingPong/PingPong.csproj]
/Users/filip/PSharp/bin/netcoreapp2.1/PSharp.vs2017.targets(4,5): error MSB4018:    at Microsoft.PSharp.Rewriter.Execute() in /Users/filip/PSharp/Tools/Compilation/SyntaxRewriter/Program.cs:line 188 [/Users/filip/PSharp/Samples/Language/PingPong/PingPong.csproj]
/Users/filip/PSharp/bin/netcoreapp2.1/PSharp.vs2017.targets(4,5): error MSB4018:    at Microsoft.Build.BackEnd.TaskExecutionHost.Microsoft.Build.BackEnd.ITaskExecutionHost.Execute() [/Users/filip/PSharp/Samples/Language/PingPong/PingPong.csproj]
/Users/filip/PSharp/bin/netcoreapp2.1/PSharp.vs2017.targets(4,5): error MSB4018:    at Microsoft.Build.BackEnd.TaskBuilder.ExecuteInstantiatedTask(ITaskExecutionHost taskExecutionHost, TaskLoggingContext taskLoggingContext, TaskHost taskHost, ItemBucket bucket, TaskExecutionMode howToExecuteTask) [/Users/filip/PSharp/Samples/Language/PingPong/PingPong.csproj]

The assembly in question is installed as a package for the PSharp solution and all the necessary dependency metadata is stored next to the DLL, but I guess MSBuild doesn't take it into account. So I need to investigate how exactly MSBuild resolves dependencies for build tasks.

[fniksic]

I succeeded in making the language samples work on macOS (and more generally, on .NET Core 2.1, so they should work on Linux as well). More importantly, this means that one can use P# as a language on these systems.

Since the solution depends on the beta version of Roslyn, for now it is a workaround. Check it out in my PSharp fork.

To deal with the assembly loading issue I mentioned in my previous comment, it turns out it is best not to have build tasks with dependencies. So I have switched to using SyntaxRewriterProcess, which I adapted to use the ToolTask API instead of manually spawning the rewriter process.

[pdeligia]

What you describe sounds great @fniksic! Thanks a lot for driving this.

I would be very happy to review and merge your solution, if you would like to open a PR?

Since your solution depends on a beta version of Roslyn, we could use conditional compilation to target that version of Roslyn for .NET Core (and keep the existing version for .NET Framework to not break existing users of the language syntax) until its released. We can then move everything to your solution.