-
Notifications
You must be signed in to change notification settings - Fork 11
Customizing Viper IDE
- Both the default settings for VS Code and the default settings for Viper extension are stored in a read-only JSON text file.
-
Customizing the settings is done via modifying the User Settings file, in which some of the settings from the default file could be overwritten. The structure should be the same in both files, but one only needs to mention the parameters which are to be changed (not all of them). For example, here is a fragment of the default settings for the Viper extension. You can see them on the left panel if you go to
File→Preferences→User Settings.
{
...
"viperSettings.viperToolsPath": "$defaultViperToolsPath$",
"viperSettings.nailgunSettings": {
"serverJar": "$viperTools$/nailgun/nailgun.jar",
"clientExecutable": "$viperTools$/nailgun/ng",
"port": "7654",
"timeout": 3000
}
...
}
If one would be to change, say, the prefix for Viper's binary dependencies, one would need to copy the relevant settings into the User Settings file (the tab on the right, called just settings.json). The User Settings could then look like this:
{
"viperSettings.viperToolsPath": "C:\VerificationTools\Viper"
}
Another example: if (in addition to the previous customization) one would also like to change the Nailgun port from the default value of 7654 to, say, 8765, here is what the User Settings would look like:
{
"viperSettings.viperToolsPath": "C:\VerificationTools\Viper",
"viperSettings.nailgunSettings": {
"serverJar": "$viperTools$/nailgun/nailgun.jar",
"clientExecutable": "$viperTools$/nailgun/ng",
"port": "8765",
"timeout": 3000
}
}
In this case, one should copy the entire viperSettings.nailgunSettings settings object from the Default Settings into the User Settings, and then change the relevant fields.
The same technique allows to specify any number of verification back-ends. A verification back-end corresponds to a sequence of actions which take place after the verification command (binding to F5) is executed (by-default, this happens automatically while you change the sources). The action might be simple, e.g., running Silicon on the opened file, but it might include other stages, too. A stage corresponds to any command line tool which one might want to run at any order with other stages which together describe a particular back-end.
The list of back-ends is stored under the key viperSettings.verificationBackends in the settings files. Three back-ends are specified in the Default Settings file:
{
...
"viperSettings.verificationBackends": [
{
"name": "silicon"
...
},
{
"name": "silicon with infer",
...
},
{
"name": "carbon_no_nailgun",
...
}
]
...
}
These three back-ends demonstrate how different things could be achieved via customizing the back-end stages.
The backend named silicon uses Nailgun to call Silicon's main method in viper.silicon.SiliconRunner. It only has one stage, called verify. This is the standard way of using the IDE with Silicon.
In contrast, the backend named silicon with infer has two stages:
{
"name": "silicon with infer",
...
"stages": [
{
"name": "verify",
...
"onVerificationError": "infer"
},
{
"name": "infer",
...
"onSuccess": "verify"
}
]
...
}
...
Note how the stages interaction is encoded via the on[EventName] attributes. This way, infer stage is only called if a verification error happens, and after inference is done we call verify stage again. Of course, the Viper IDE extension makes sure that we don't get an infinite loop between these stages.
Finally, we include the back-end called carbon_no_nailgun in order to demonstrate how the IDE could be used without Nailgun (which is inadvisable):
{
"name": "carbon_no_nailgun",
...
"useNailgun": false,
...
}
...
Finally, there is a third possible location for storing settings, called Workspace Settings. The file is accessible through the menu: File→Preferences→Workspace Settings. These settings are meant to be specific for each project, and in terms of VS Code a project is defined by it's main folder, called Workspace. The structure of this file is exactly the same as the structure of Default Settings and User Settings, but Workspace Settings have top priority.
The following shows how a verification back-end (in this case Silicon) could be extended with an external specification inference tool (available as a JAR file). The back-end called "silicon with infer" could be added to the list of backends ("viperSettings.verificationBackends") in the User Settings.
{
"v": "0.3.8",
"name": "silicon with infer",
"paths": [
"$viperTools$/backends/silicon.jar",
"$viperTools$/backends/infer.jar"
],
"useNailgun": true,
"timeout": 100000,
"stages": [{
"name": "verify",
"isVerification": true,
"mainMethod": "viper.silicon.SiliconRunner",
"customArguments": "--ideMode --ideModeAdvanced --z3Exe $z3Exe$ $fileToVerify$",
"onParsingError": "",
"onTypeCheckingError": "",
"onVerificationError": "infer",
"onSuccess": ""
},
{
"name": "infer",
"isVerification": false,
"mainMethod": "ch.ethz.inf.pm.sample.permissionanalysis.Main",
"customArguments": "$fileToVerify$",
"onParsingError": "",
"onTypeCheckingError": "",
"onVerificationError": "",
"onSuccess": "verify"
}
]
}
-
nailgunSettings: All nailgun related settings
- serverJar: The path to the nailgun server jar.
- clientExecutable: The path to the nailgun client executable
- port: The port used for the communication between nailgun client and server
- timeout: After timeout ms the startup of the nailgun server is expected to have failed and thus aborted
-
verificationBackends: Description of backends
- name: The unique name of this backend
- paths: List of paths locating all used jar files, the files can be addressed directly or via folder, in which case all jar files in the folder are included
- useNailgun: Enable to run the backend through nailgun, speeding up the process by reusing the same Java Virtual Machine
- timeout: After timeout ms the verification is expected to be non terminating and is thus aborted.
-
stages: A list of verification stages
- name: The per backend unique name of this stage
- isVerification: Enable if this stage is describing a verification
- mainMethod: The method to invoke when staring the stage
- customArguments: the commandline arguments for the nailgun client (or java, when useNailgun is disabled)
- onParsingError: The name of the stage to start in case of a parsing error
- onTypeCheckingError: The name of the stage to start in case of a type checking error
- onVerificationError: The name of the stage to start in case of a verification error
- onSuccess: The name of the stage to start in case of a success
-
paths: Used paths
- viperToolsPath: Path to the folder containing all the ViperTools
- z3Executable: The path to the z3 executable
- boogieExecutable: The path to the boogie executable
-
preferences: General user preferences
- autoSave: Enable automatically saving modified viper files
- logLevel: Verbosity of the output, all output is written to the logFile, regardless of the logLevel
- autoVerifyAfterBackendChange: Reverify the open viper file upon backend change.
- showProgress: Display the verification progress in the status bar. Only useful if the backend supports progress reporting.
- viperToolsProvider: An url pointing to the location of the viper tools directory.
-
javaSettings: Java related settings
- customArguments: The arguments used for all java invocations
-
advancedFeatures: Settings concening the advanced features
- enabled: Enable heap visualization, stepwise debugging and execution path visualization
- showSymbolicState: Show the symbolic values in the heap visualization. If disabled, the symbolic values are only shown in the error states.
- simpleMode: Useful for verifying programs. Disable when developing the backend darkGraphs: To get the best visual heap representation, this setting should match with the active theme.
- showOldState: When set, the old state is included in the state visualization
- showPartialExecutionTree: When set, the partial execution tree is included in the state visualization
- compareStates: When set, two states are shown in the state visualization for comparison
- verificationBufferSize: Maximal buffer size for verification in KB