Skip to content

Customizing Viper IDE

Jump to bottom
Linard Arquint edited this page Feb 17, 2022 · 4 revisions

Customizing Viper IDE

  1. Both the default settings for VS Code and the default settings for Viper extension are stored in a read-only JSON text file. VS Code distinguishes between User settings and Workspace settings. Workspace settings are very handy if you want to use special settings for the current workspace only because Workspace settings take precedence over User settings.
  2. Customizing the settings is done via File→Preferences→Settings. You can then choose between User and Workspace in the tab bar. Some settings, like Viper's build version, can simply be changed in the UI. More complex settings, like Viper's path settings, redirect you to the underlying JSON text file to directly edit the corresponding JSON objects. Note that you can use auto-completing to populate the default version of a settings entry in case VS Code does not automatically do so. Also note that Viper's more complex settings entries have a v field storing some hash value. It is used by the Viper IDE to detect outdated settings. Simply use the value from the default settings entry.

Viper IDE even 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. Two back-ends are specified in the Default Settings file:

{
    ...
    "viperSettings.verificationBackends": [
        {
            "name": "silicon"
            ...
        },
        {
            "name": "carbon",
            ...
        }
    ]
    ...
}

These two back-ends demonstrate how different things could be achieved via customizing the back-end stages. The backend named silicon uses ViperServer 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.

A back-end can have multiple stages as demonstrated next (note that this is no longer part of the default settings): 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.

Adding custom stages to the verification commands

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"
                                }
                            ]
                        }

List of all viperSettings

Clone this wiki locally