This project is read-only.

Unable to start the process z3.exe from default location

Jul 14, 2010 at 10:12 PM

There are two issues here that i am facing. One is that i am not getting any potential errors and/or warnings, whereas i expect at least some and the other problem is the installation of z3.exe and understanding the role of ssc.boogie here.

Problem 1.  I previously had version 1.2 of z3 verifier. I was getting plenty of warnings in the projects, where some made sense and were expected and some errors were just unacceptable. I thought i solved the mystery by installing the latest version of z3 ie 2.9. However , now i do not get any warnings errors at all, whereas i do expect at least some over there. Could you please help me with this? It is so consfusing, as i cannot resolve those potential problems without looking at them. Everything seems to pass the verifier right now!  

 

Problem2:  I am 

 building from binaries. but the status of binaries download on page  

  Released: Aug 5 2009

Updated: Aug 5 2009 by mikebarnett

 

Are there any updates after that?? Am i working with the correct version? Do i also need to do/download something separately from boogie.codeplex.com ??

Also, I have  installed the latest version of Z3 in the default place, which is 2.9 as of now. I dont have a copy of the z3 in the SpecSharp folder. However, if i have Z3 installed
 only 
at the default place which is C:\ProgramFiles\MicrosoftResearch... ... it gives me an error at runtime. Probably it is trying to locate z3 at a different location than default one as mentioned. The following is the error.  

Error 1 Plugin type 'Microsoft.Boogie.BoogiePluginVisitor' threw exception 'Unable to start the process C:\Program Files (x86)\Microsoft Visual Studio 9.0\Common7\IDE\z3.exe: The system cannot find the file specified'.\nStack:    at Microsoft.Boogie.Simplify.ProverProcess..ctor(ProcessStartInfo psi, String proverPath)
   at Microsoft.Boogie.Z3.Z3ProverProcess..ctor(String proverPath, Boolean bvnative, Int32 timeout, Boolean typed)
   at Microsoft.Boogie.Z3.Z3ProcessTheoremProver.CreateProverProcess(String proverPath)
   at Microsoft.Boogie.Simplify.ProcessTheoremProver.FireUpNewProver()
   at Microsoft.Boogie.Simplify.ProcessTheoremProver.ResurrectProver()
   at Microsoft.Boogie.Simplify.ProcessTheoremProver.BeginCheck(String descriptiveName, VCExpr vc, ErrorHandler handler)
   at Microsoft.Boogie.Checker.BeginCheck(String descriptiveName, VCExpr vc, ErrorHandler handler)
   at VC.VCGen.Split.BeginCheck(VerifierCallback callback, Int32 no, Int32 timeout)
   at VC.VCGen.VerifyImplementation(Implementation impl, Program program, VerifierCallback callback)
   at VC.VCGen.VerifyImplementation(Implementation impl, Program program, List`1& errors)
   at Microsoft.Boogie.BoogiePluginVisitor.VerifyBplProgram(TranslatedProgram program, Node programNode, CompilerSite site) in D:\Boogie\2\Source\CompilerPlugin\Plugin.ssc:line 435
   at Microsoft.Boogie.BoogiePluginVisitor.VisitCompilation(Compilation compilation) in D:\Boogie\2\Source\CompilerPlugin\Plugin.ssc:line 275
   at System.Compiler.StandardVisitor.Visit(Node node)
   at Microsoft.SpecSharp.SpecSharpCompilation.RunPlugins(Compilation compilation, ErrorHandler errorHandler) in D:\CCI\Microsoft.SpecSharp\Compiler.cs:line 156 c:\Program Files (x86)\Microsoft Visual Studio 9.0\Common7\IDE\unknown file 1 1 SpecXML
--------------------------------------------------------------------------

So after putting z3.dll and z3.exe at the above location manually
 C:\Program Files (x86)\Microsoft Visual Studio 9.0\Common7\IDE\z3.exe
I do not get any warnings/errors, whereas i do expect at least some logical ones there. I would like to mention here, that i did exactly the same way as instructed on the codeplex page. I do run  registerLKG.cmd and specsharp is recognised by visual studio. But verification does not seem to be correct. It just verifies everything. Please note here that i also had to copy prelude.dll and .exe in the same folder as it gave me same error for that. 

 

Could anyone please help me with the dilemmas stated above?

Jul 16, 2010 at 10:09 PM

Not been able to resolve yet

Just want this post to move up .. still wonder if someone can help here as i am struck.. 

Jul 16, 2010 at 10:57 PM

Here's the scoop.  Let's think of the Spec# release as having 3 components:  the compiler (ssc.exe), the Spec# verifier (SscBoogie.exe), and the Boogie verification engine that underlies SscBoogie.exe.  You get all three from the binary Spec# release.  To make use of the verifier, you also need Z3.exe, which you get separately from http://research.microsoft.com/projects/z3.

In the past, the place to download these 3 components was the Spec# page at http://research.microsoft.com/specsharp.  In fact, I think that release also contained a version of Z3, which was probably Z3 version 1.2 or 1.3.  Since you mention having used that version of Z3, I'm guessing you obtained your Spec# from this site.

Last summer, we released Spec# as open source at http://specsharp.codeplex.com and then also provided a binary release of Spec# there.  That was a slightly newer version, and in particular the Boogie verification engine in that release was newer.  Here, Z3 version 2.x was supported, but Z3 had to be downloaded separately from the Z3 homepage mentioned above.

Since last summer, we have not noticably evolved Spec# itself, nor SscBoogie, but the underlying Boogie engine has evolved.  Boogie is now also available as open source, at http://boogie.codeplex.com (which has a more liberal license than Spec# and Z3).  All changes to Boogie since last summer have gone into that release.  A small but for this discussion relevant change to Boogie has to do with where Boogie looks for Z3.  It always starts by checking in the directory from which Boogie is being executed.  After that, it looks in the file system in the places where Z3 installs itself, which is inside the Program Files folder and depends on the version of Z3.  The way that happens is a bit clunky (but Boogie is open source and you're welcome to implement a better behavior), namely:  it looks for a Z3 version 2.15 (which doesn't yet exist), then version 2.14, and so on down to version 2.0.  The current version of Z3 is 2.9, so if you have it installed (and don't have a Z3.exe in your Boogie binaries directory), then this is the one Boogie will find.  However, a previous version of Boogie started looking in for Z3 version 2.5.  After Z3 version 2.6 was release, we updated Boogie to search more folders, and we have changed that again to start looking for version 2.15.  So, if you have a version of Boogie from some previous time in the last year, it may not find the latest version of Z3.  The fix here is to update to the latest Boogie.

Back to Spec#.  Since SscBoogie rests on Boogie, where it looks for Z3 is subject to which version of Boogie you're using.  If you're building Spec# from source and are synched up to the latest Boogie, your SscBoogie will find the latest Z3.  However, the Spec# binary release has not been updated to include the latest Boogie.  In fact, as you (and others!) have noticed, the so-called Stable binary release of Spec# is from last summer.  We are currently trying to fix this problem by putting out a new binary release of Spec# (including the compiler, SscBoogie, and Boogie).  Regrettably, this has proved much more mind boggling than anyone would have thought, and we're struggling with finding a recipe that will install the correct version of Spec#.

I hope we can figure this out soon.  In the meantime, if you want to give it a shot yourself, try clicking on the so-called Planned releases on the Download tab.  Be warned, however, that you may get into a bad installation state from which you can't run Spec# at all and from which it is difficult to restore even a previously working Spec# version.  When we find a fix, I will post another Reply to this thread.

  Rustan

Jul 21, 2010 at 6:41 AM

We were able to get together a new binary release that, I hope, solves these problems.  Please give the new version a try (and you'll also want to install the latest version of Z3, which is 2.9).

  Rustan

Jul 21, 2010 at 10:18 AM
I have just installed the new binary release. Boogie found Z3 2.9 and they are talking beautifully.
Aug 4, 2010 at 11:16 PM

Hi Rustan, Rosemary,

Thanks a lot for your reply.

I installed the latest version, then registered everything successfully. I already had z3 2.9 version installed on my system.

But when i built my project in SpecSharp, the build fails and throws the following error. 

Error 1 Plugin type 'Microsoft.Boogie.BoogiePluginVisitor' threw exception 'Method not found: 'Microsoft.Boogie.TranslatedProgram Microsoft.Boogie.CilTranslator.TranslateAstToBoogie(System.Compiler.CompilationUnit, System.Compiler.Analyzer, System.Compiler.ErrorHandler)'.'.\nStack:    at Microsoft.Boogie.BoogiePluginVisitor.VisitCompilationUnit(CompilationUnit unit)   at System.Compiler.StandardVisitor.VisitCompilationUnitSnippet(CompilationUnitSnippet snippet) in C:\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 849   at System.Compiler.StandardVisitor.Visit(Node node) in C:\specsharp\SpecSharp\System.Compiler\StandardVisitor.cs:line 167   at Microsoft.SpecSharp.SpecSharpCompilation.RunPlugins(Node node, ErrorHandler errorHandler) in C:\specsharp\SpecSharp\Microsoft.SpecSharp\Compiler.cs:line 150 C:\Users\.... \JobType.ssc 1 1 SpecXML

 

Could you please tell me, if there is any way i could resolve this issue? Do i need to uninstall/reinstall something?

Many Thanks

Ruchi

Aug 4, 2010 at 11:19 PM
Edited Aug 20, 2010 at 8:10 PM

Forgot to mention. 

Thanks a lot Rustan.

Ruchi