-
Notifications
You must be signed in to change notification settings - Fork 34
ScalaZ3 and Visual Studio 2012 Express for Windows Desktop
z3.lib is needed for access to Z3's C/C++ API. Ages ago, this was provided as a precompiled binary for Windows. It can be rebuilt easily from the source code release for Z3 version 4.1.2 at http://z3.codeplex.com/releases/view/95754. The Visual C++ solution and projects are included: just open the top-level solution z3-prover.sln and select test_capi as your start-up project. I recommend starting with the Release Configuration targetting the x64 platform. The project dependencies are pre-configured. You will also need to open dll.rc in an editor and manually edit the line "#include afxres.h" to read "#include "WinResrc.h"" as described at http://stackoverflow.com/a/17454415/201008.
This step will test your resolve to continue further down the route of using Visual Studio 2012 Express. You will see.
Once you have a z3.lib built for the x64 platform, change the platform to x86 and rebuild in order to support 32-bit Java VMs.
Version control software is available from GitHub. This document is based on the source clonable from https://github.com/epfl-lara/ScalaZ3/tree/2.9.x.
Many of the changes discussed below have been incorporated into the branch located at: https://github.com/vo1stv/ScalaZ3/tree/VS2012Express
The version of Eclipse used during creation of this document was Indigo. Suggested workspace location is in MyDocuments\GitHub. This is the default location beneath which GitHub stores local copies of projects you have cloned.
Suggested project location (within workspace MyDocuments\GitHub) is ScalaZ3. This is the default location where GitHub stores local clones of the ScalaZ3 project. If you have cloned ScalaZ3 as above, Eclipse will configure .\src\main\java, .\src\main\scala and .\src\test as source folders. Set the output class folder to ScalaZ3\target\scala-2.9.x\classes.
Use Eclipse to build the classpath. This will fail with one error:
LibraryChecksum cannot be resolved to a variable Z3Wrapper.java /ScalaZ3/src/main/java/z3 line 27 Java Problem
You can eliminate this by creating a file named LibraryChecksum.java in folder target\java\z3 with the following contents:
package z3;
public class LibraryChecksum {
static String value = "TODO: Specific Library Checksum Here";
}
You need the compiled classfiles and the javah from the JDK for this. On my host, this requires the rather long command name:
"C:\Program Files\Java\jdk1.7.0_21\bin\javah.exe" -classpath .\target\scala-2.9.x\classes;C:\eclipse\configuration\org.eclipse.osgi\bundles\808\1\.cp\lib\scala-library.jar -d target\c\include z3.Z3Wrapper
An alternative to the command line is to set up Eclipse External Tools. This simplifies the command somewhat because variables can be used instead of the hard-coded paths above. To date I have not found a variable that returns the fully qualified path of the scala-library.jar. Consequently this option requires customizing the eclipse variables by adding a user-defined variable (PATH_TO_ECLIPSE_SCALA) that maps to the fully qualified name as copied to the clipboard by eclipse from the package explorer. I was hoping it would be simpler, something like ${pathto:scala-library.jar}.
- Launch Visual Studio 2012 Express
- From the Start Page, choose New Project
- Choose to create a Win32 Project named scalaz3.
- Create the project in the MyDocuments\GitHub\ScalaZ3\projects folder. It's not necessary to create a subfolder for the project, but the IDE will probably create one called scalaz3 regardless.
- Under Application Settings, select the DLL application type. Also check the empty project checkbox.
- Click Finish to create the project.
- Add the files from ScalaZ3: src/c to the project.
- Under additional include directories, add "....\src\c" and "....\target\c\include;" and the path to the include location(s) of the JDK (e.g C:\Program Files (x86)\Java\jdk1.7.0_21\include and C:\Program Files (x86)\Java\jdk1.7.0_21\include\win32) and the path to Z3 (e.g. C:\z3-4.1.2\lib)
- Under Link options, add z3.lib. Also add the path to the Win32 (i.e 32-bit x86 platform) z3.lib library to the Additional Library Directories
- Edit src\c\casts.h to insert the following line after the include statement for jni.h:
#define inline
- Because of the issue discussed at http://stackoverflow.com/questions/6754126/msvc-vs-gcc-variable-declaration-in-function, a few edits are required to the C files to make them compatible with C89 conventions. The number of mods is small: functions Java_z3_Z3Wrapper_substitute and Java_z3_Z3Wrapper_mkTactic. The fix simply requires pre-declaring variables at the beginning of functions instead of mid-way through.
You will probably want to add 32-bit and 64-bit configurations. The DLL configuration must match the version of the Java VM (32-bit or 64-bit) installed. The above instructions will create the 32-bit configuration by default. To copy the settings for 64-bit configuration, run the Configuration Manager from the Project Properties dialog.
To test the DLLs open the ScalaZ3 project (cloned above) in Eclipse. Make sure the Scala perspective is installed and that you have installed ScalaTest, which is available from the same update site where you downloaded Scala (see http://scala-ide.org/download/current.html).
Rather than deal with Windows system paths, the procedure below assumes that you have copied the z3.dll and scalaz3.dll you built above into the lib-bin folder of the ScalaZ3 project. If you followed the procedure above the path to this folder is MyDocuments\GitHub\ScalaZ3\lib-bin.
To run the ScalaTest suite, create a Run Configuration for it from the Run menu. In the "Create, Manage, and Run Configurations" dialog, highlight ScalaTest and click the New Launch Configuration icon. I prefer the ForComprehension as the first test to run. Give the configuration the name: ForComprehension, set the project as ScalaZ3, the type as Suite, and the class as z3.ForComprehension. Finally, on the (x)=Arguments tab of the dialog, set the working directory to ${workspace_loc:ScalaZ3/lib-bin}. Apply the changes and Run.
- A successful launch is self-explanatory.
- If the test fails with something to the effect "Can't run 32-bit DLLs on a 64-bit platform", then you are running a 64-bit JavaVM but have placed DLLs for a 32-bit (x86 Win32) platform. Either change the JavaVM to match the DLLs, or vice versa. Also check that the JRE for the run configuration (see the JRE tab of the "Create, Manage, and Run Configurations" dialog) is also what you expect.
- If the test fails with an error "UnsatisfiedLinkError: Can't load library: lib-bin/scalaz3.dll", then the working directory is wrong or you have a bad version of scalaz3.dll.
- If the test fails with exception "java.lang.UnsatisfiedLinkError: lib-bin\scalaz3.dll: Can't find dependent libraries", then the working directory is wrong or you have a bad version of z3.dll.
An odd thing about the above is that it often works only for the Eclipse session in which you create it. Closing Eclipse and reopening it, then re-running the run configuration will either reset the working location to the default, or set it to ScalaZ3/lib-bin/lib-bin.
This step will test your resolve to continue further down the route of using Eclipse.
There is a workaround for this in the code available at https://github.com/vo1stv/ScalaZ3/tree/VS2012Express. If you choose to use the workaround, reset the working directory for the launch configurations back to the default (as if Eclipse really gives you much of a choice).
An article discussing the procedure for migrating Visual Studio projects to makefiles for use in the Eclipse environment can be found at http://www.ibm.com/developerworks/library/os-ecl-vscdt/index.html?ca=dgr-eclipse-1