Experiment: Viper integration

[rvanasa]

VS Code support for dfinity/motoko#3477.

• This implementation uses moc.js (rather than the OCaml LSP) to generate Viper files.
  • This makes it possible for anyone to try the demo without requiring a modified moc or dfx installation.
  • See below for steps to quickly rebuild the extension.
• Activate code translation by adding // @verify at the top of a Motoko file.

Example (Main.mo):

// @viper

actor {
  var claimed = false;
  var count = 0 : Int;

  assert claimed and not (-1 == -1) and (-42 == -42) or true;
  assert count > 0;

  public shared func claim() : async () { };
};

Generated file (Main.vpr):

method __init__($Self: Ref)  
  ensures invariant_7($Self)
  ensures invariant_8($Self)
   { 
     ($Self).claimed := false
     ($Self).count := 0 
   }
field claimed: Bool
field count: Int
define invariant_7(self) (((((self).claimed && (!(-1 == -1))) && (-42 == -42)) || true))
define invariant_8(self) (((self).count > 0))
method claim($Self: Ref) 
  requires invariant_7($Self)
  requires invariant_8($Self)
  ensures invariant_7($Self)
  ensures invariant_8($Self)  { 
                                 
                              }

Recommended editor workflow using split-screen tabs (updates as you type):

Steps to build the extension:

• Ensure motoko and vscode-motoko are in the same parent directory
• Switch to the ryan/viper branch in the Motoko compiler repository
• In your terminal, run cd vscode-motoko and then npm run package (this will rebuild moc.js)
• Right-click the generated /vscode-motoko-*-viper.vsix file and select "Install extension VSIX"

Progress:

• Generate Viper files on code change
• Show Motoko diagnostics from Pipeline.viper_files
• Show Viper diagnostics in Motoko via source map

[ggreif]

A few more materials:

• viper LSP API: https://github.com/viperproject/viper-ide/blob/master/client/src/ViperProtocol.ts
• how to invoke (see dialog below)
• there needs to be setting for the <ViperServerPort:54816> and hostname
• you start the server (in nix-shell) with env Z3_EXE="$(which z3)" java -Xmx2048m -Xss16m -jar $VIPER_SERVER --singleClient --serverMode LSP --port 54816&

On establishing connection

Content-Length: 85

{ "jsonrpc": "2.0", "id": 1, "method": "initialize","params": { "processId": null}}

On Viper program creation/updates

Content-Length: 173

{ "jsonrpc": "2.0", "method": "textDocument/didOpen","params": { "textDocument": { "languageId": "viper","version": 0,"uri": "file:///Users/ggreif/motoko/post-fail.vpr"}}}

Content-Length: 137

{ "jsonrpc": "2.0", "method": "textDocument/didSave","params": { "textDocument": {"uri": "file:///Users/ggreif/motoko/post-fail.vpr"}}}

Asking for verification

Content-Length: 274

{ "jsonrpc": "2.0", "id": 1, "method": "Verify","params":{"uri":"file:/Users/ggreif/motoko/post-fail.vpr","backend":"silicon","customArgs":"--z3Exe /nix/store/3dpbapw0ia9q835pqbf7khdi9rps2rm2-z3-4.8.15/bin/z3 /Users/ggreif/motoko/post-fail.vpr","manuallyTriggered":false}}

Here --z3Exe is not mandatory if the server has been started with Z3_EXE envvar. The to filenames pointing to the same file are unfortunate, but a current wart in the protocol. You can throw in --logLevel OFF for less noise.

You may get a request asking for file endings (GetViperFileEndings), answer that with

Content-Length: 66

{ "jsonrpc": "2.0", "id": 1, "result":{"fileEndings":["*.vpr"]}}

A VerificationNotStarted notification is basically bad news. When you get status reports on the course of the verification that's good news, and "state"=6 is what concludes the report. From there you can fish out the diagnostics. Earlier states might contain auxiliary information about different partial results in the various methods.

You'll see something like this:

{"jsonrpc":"2.0","method":"StateChange","params":{"newState":6,"progress":-1.0,"success":4,"verificationCompleted":1.0,"manuallyTriggered":1.0,"filename":"post-fail.vpr","time":3.346,"verificationNeeded":-1.0,"uri":"file:///Users/ggreif/motoko/post-fail.vpr","error":"","diagnostics":[{"range":{"start":{"line":3,"character":12},"end":{"line":3,"character":17}},"severity":1,"source":"","message":"Postcondition of bar might not hold. Assertion foo() might not hold. ([email protected])"}]}}

[ggreif]

Btw. If you start code from a nix-shell, then you already have a viperserver.jar around, path is in $VIPER_SERVER, so instead of downloading afresh, just check for the env-var.

$ echo $VIPER_SERVER
/nix/store/v202v4jgrc39hjpi7b7613b7qkv5z4lm-viperserver.jar

[ggreif]

You can use $VIPER_SERVER in the first place.

[rvanasa]

Good idea; now using the Nix environment for the stand-in portable build logic.

[rvanasa]

Progress:

• Implemented error reporting in Motoko files from a sandboxed Viper LSP
• Added syntax highlighting for the invariant and implies keywords
• Included a "view in context" button to jump from Motoko errors to the corresponding Viper source location

In this screenshot, the // @viper comment is being used as a default error location. The TS language server is ready to display errors at the correct locations once the lookup function from moc.js is working as expected (dfinity/motoko#3501).

[aterga]

While installing the extension from this branch, I've experienced the following minor hick-ups:

1. Needed to run npm install run-a --dev (maybe repeating npm install would have sufficed)
2. Needed to run src/generated (otherwise, I was getting

'src/moc.js' -> '../vscode-motoko/src/generated/moc.js'
cp: cannot create regular file '../vscode-motoko/src/generated/moc.js': No such file or directory

The rest of the instructions worked out nicely!

PS. I ran npm run package from motoko repo's nix-shell.

[aterga]

Also, one probably needs code --force --install-extension pwd/vscode-motoko-0.5.3-viper.vsix

[crusso]

2. Needed to run src/generated (otherwise, I was getting

An you mean create (not run) src/generated.

[rvanasa]

While installing the extension from this branch, I've experienced the following minor hick-ups:

Fixed; thanks!

[aterga]

Added a few minor suggestions.