experiment: Viper integration

.gitignore

@@ -13,6 +13,9 @@ result*
 
 /samples/**/*.txt
 
+**/*.mo.vpr
+test/viper/tmp
+
 enable-internals
 
 # Editor configuration

Changelog.md

@@ -9,6 +9,10 @@
     rejected, not accepted, to be consistent with the declarations of
     mutable fields and mutable objects.
 
+  * Experimental Viper integration by compiling a very narrow subset of
+    Motoko to the verification intermediate language. See `src/viper/README.md`
+    and the PR for details. (#3477).
+
 ## 0.7.3 (2022-11-01)
 
 * motoko (`moc`)

README.md

@@ -12,6 +12,7 @@ A safe, simple, actor-based programming language for authoring [Internet Compute
 * [Concrete syntax](doc/md/examples/grammar.txt).
 * [Documentation sources](doc/md/).
 * [Base library documentation](doc/md/base/index.md).
+* [_Motoko-san_: a prototypical deductive verifier](src/viper/README.md).
 
 ## Introduction
 

default.nix

@@ -350,6 +350,7 @@ rec {
             patchShebangs .
             ${llvmEnv}
             export ESM=${nixpkgs.sources.esm}
+            export VIPER_SERVER=${viperServer}
             type -p moc && moc --version
             make -C ${dir}
           '';
@@ -490,6 +491,7 @@ rec {
       run-deser  = test_subdir "run-deser"  [ deser ];
       perf       = perf_subdir "perf"       [ moc nixpkgs.drun ];
       bench      = perf_subdir "bench"      [ moc nixpkgs.drun ];
+      viper      = test_subdir "viper"      [ moc nixpkgs.which nixpkgs.openjdk nixpkgs.z3 ];
       inherit qc lsp unit candid profiling-graphs coverage;
     }) // { recurseForDerivations = true; };
 
@@ -750,6 +752,11 @@ rec {
     builtins.attrValues js;
   };
 
+  viperServer = nixpkgs.fetchurl {
+    url = https://github.com/viperproject/viperserver/releases/download/v.22.11-release/viperserver.jar;
+    sha256 = "sha256-debC8ZpbIjgpEeISCISU0EVySJvf+WsUkUaLuJ526wA=";
+  };
+
   shell = stdenv.mkDerivation {
     name = "motoko-shell";
 
@@ -780,6 +787,7 @@ rec {
           nixpkgs.nix-update
           nixpkgs.rlwrap # for `rlwrap moc`
           nixpkgs.difftastic
+          nixpkgs.openjdk nixpkgs.z3 nixpkgs.jq # for viper dev
         ]
       ));
 
@@ -797,6 +805,7 @@ rec {
     LOCALE_ARCHIVE = nixpkgs.lib.optionalString stdenv.isLinux "${nixpkgs.glibcLocales}/lib/locale/locale-archive";
     MOTOKO_BASE = base-src;
     CANDID_TESTS = "${nixpkgs.sources.candid}/test";
+    VIPER_SERVER = "${viperServer}";
 
     # allow building this as a derivation, so that hydra builds and caches
     # the dependencies of shell.

emacs/motoko-mode.el

@@ -72,6 +72,8 @@
                  "var"
                  "while"
                  "prim"
+                 "invariant"
+                 "implies"
                  ))
               ;; Braces introduce blocks; it's nice to make them stand
               ;; out more than ordinary symbols

src/exes/moc.ml

@@ -10,7 +10,7 @@ let usage = "Usage: " ^ name ^ " [option] [file ...]"
 
 (* Argument handling *)
 
-type mode = Default | Check | StableCompatible | Compile | Run | Interact | PrintDeps | Explain
+type mode = Default | Check | StableCompatible | Compile | Run | Interact | PrintDeps | Explain | Viper
 
 let mode = ref Default
 let args = ref []
@@ -42,6 +42,7 @@ let argspec = [
   "-r", Arg.Unit (set_mode Run), " interpret programs";
   "-i", Arg.Unit (set_mode Interact), " run interactive REPL (implies -r)";
   "--check", Arg.Unit (set_mode Check), " type-check only";
+  "--viper", Arg.Unit (set_mode Viper), " emit viper code";
   "--stable-compatible",
     Arg.Tuple [
       Arg.String (fun fp -> Flags.pre_ref := Some fp);
@@ -189,6 +190,9 @@ let process_files files : unit =
     exit_on_none (Pipeline.run_files_and_stdin files)
   | Check ->
     Diag.run (Pipeline.check_files files)
+  | Viper ->
+    let (s, _) = Diag.run (Pipeline.viper_files files) in
+    printf "%s" s
   | StableCompatible ->
     begin
       match (!Flags.pre_ref, !Flags.post_ref) with

src/ir_def/construct.ml

@@ -321,6 +321,7 @@ let notE : Ir.exp -> Ir.exp = fun e ->
   primE (RelPrim (T.bool, Operator.EqOp)) [e; falseE ()]
 let andE : Ir.exp -> Ir.exp -> Ir.exp = fun e1 e2 -> ifE e1 e2 (falseE ()) T.bool
 let orE : Ir.exp -> Ir.exp -> Ir.exp = fun e1 e2 -> ifE e1 (trueE ()) e2 T.bool
+let impliesE : Ir.exp -> Ir.exp -> Ir.exp = fun e1 e2 -> orE (notE e1) e2
 let rec conjE : Ir.exp list -> Ir.exp = function
   | [] -> trueE ()
   | [x] -> x

src/ir_def/construct.mli

@@ -97,6 +97,7 @@ val trueE : unit -> exp
 val notE : exp -> exp
 val andE : exp -> exp -> exp
 val orE : exp -> exp -> exp
+val impliesE : exp -> exp -> exp
 val conjE : exp list -> exp
 
 val declare_idE : id -> typ -> exp -> exp

src/js/common.ml

@@ -62,12 +62,30 @@ let js_run list source =
   let list = Js.to_array list |> Array.to_list |> List.map Js.to_string in
   ignore (Pipeline.run_stdin_from_file list (Js.to_string source))
 
+let js_viper filenames =
+  let result = Pipeline.viper_files (Js.to_array filenames |> Array.to_list |> List.map Js.to_string) in
+  js_result result (fun (viper, lookup) ->
+    let js_viper = Js.string viper in
+    let js_lookup = Js.wrap_callback (fun js_file js_region ->
+      let file = Js.to_string js_file in
+      let viper_region = match js_region |> Js.to_array |> Array.to_list with
+      | [a; b; c; d] ->
+        lookup { left = { file; line = a + 1; column = b }; right = { file; line = c + 1; column = d } }
+      | _ -> None in
+      match viper_region with
+      | Some region ->
+        Js.some (range_of_region region)
+      | None -> Js.null) in
+    Js.some (object%js
+      val viper = js_viper
+      val lookup = js_lookup
+    end))
+
 let js_candid source =
   js_result (Pipeline.generate_idl [Js.to_string source])
     (fun prog ->
       let code = Idllib.Arrange_idl.string_of_prog prog in
-      Js.some (Js.string code)
-    )
+      Js.some (Js.string code))
 
 let js_stable_compatible pre post =
   js_result (Pipeline.stable_compatible (Js.to_string pre) (Js.to_string post)) (fun _ -> Js.null)
@@ -96,8 +114,7 @@ let js_compile_wasm mode source =
         val wasm = code
         val candid = Js.string candid
         val stable = sig_
-      end)
-    )
+      end))
 
 let js_parse_candid s =
   let parse_result = Idllib.Pipeline.parse_string (Js.to_string s) in

src/js/moc_js.ml

@@ -27,6 +27,7 @@ let () =
       method gcFlags option = gc_flags option
       method run list s = Flags.compiled := false; wrap_output (fun _ -> js_run list s)
       method check s = Flags.compiled := false; js_check s
+      method viper filenames = js_viper filenames
       method candid s = Flags.compiled := true; js_candid s
       method stableCompatible pre post = js_stable_compatible pre post
       method compileWasm mode s = Flags.compiled := true; js_compile_wasm mode s

src/lang_utils/error_codes.ml

@@ -184,4 +184,5 @@ let error_codes : (string * string option) list =
     "M0178", None; (* Bases of record extensions must be either objects or modules *)
     "M0179", None; (* Mutable (var) fields from bases must be overwritten explicitly *)
     "M0180", None; (* Shared function has unexpected type parameters *)
+    "M0181", None; (* Verification mode assertions not allowed *)
   ]

src/languageServer/imports.ml

@@ -9,7 +9,10 @@ type import = string * string
 
 let parse_with mode lexbuf parser =
   let tokenizer, _ = Lexer.tokenizer mode lexbuf in
-  Ok (Parsing.parse 0 (parser lexbuf.Lexing.lex_curr_p) tokenizer lexbuf)
+  Ok
+    (Parsing.parse Lexer_lib.mode 0
+       (parser lexbuf.Lexing.lex_curr_p)
+       tokenizer lexbuf)
 
 let parse_string s =
   try

src/lowering/desugar.ml

@@ -201,6 +201,7 @@ and exp' at note = function
   | S.NotE e -> (notE (exp e)).it
   | S.AndE (e1, e2) -> (andE (exp e1) (exp e2)).it
   | S.OrE (e1, e2) -> (orE (exp e1) (exp e2)).it
+  | S.ImpliesE (e1, e2) -> (impliesE (exp e1) (exp e2)).it
   | S.IfE (e1, e2, e3) -> I.IfE (exp e1, exp e2, exp e3)
   | S.SwitchE (e1, cs) -> I.SwitchE (exp e1, cases cs)
   | S.TryE (e1, cs) -> I.TryE (exp e1, cases cs)
@@ -222,7 +223,8 @@ and exp' at note = function
               | T.Async (t, _) -> t
               | _ -> assert false)
   | S.AwaitE e -> I.PrimE (I.AwaitPrim, [exp e])
-  | S.AssertE e -> I.PrimE (I.AssertPrim, [exp e])
+  | S.AssertE (Runtime, e) -> I.PrimE (I.AssertPrim, [exp e])
+  | S.AssertE (_, e) -> (unitE ()).it
   | S.AnnotE (e, _) -> assert false
   | S.ImportE (f, ir) -> raise (Invalid_argument (Printf.sprintf "Import expression found in unit body: %s" f))
   | S.PrimE s -> raise (Invalid_argument ("Unapplied prim " ^ s))

src/mo_def/arrange.ml

@@ -78,6 +78,7 @@ module Make (Cfg : Config) = struct
     | NotE e              -> "NotE"    $$ [exp e]
     | AndE (e1, e2)       -> "AndE"    $$ [exp e1; exp e2]
     | OrE (e1, e2)        -> "OrE"     $$ [exp e1; exp e2]
+    | ImpliesE (e1, e2)   -> "ImpliesE"$$ [exp e1; exp e2]
     | IfE (e1, e2, e3)    -> "IfE"     $$ [exp e1; exp e2; exp e3]
     | SwitchE (e, cs)     -> "SwitchE" $$ [exp e] @ List.map case cs
     | WhileE (e1, e2)     -> "WhileE"  $$ [exp e1; exp e2]
@@ -90,7 +91,15 @@ module Make (Cfg : Config) = struct
     | RetE e              -> "RetE"    $$ [exp e]
     | AsyncE (tb, e)      -> "AsyncE"  $$ [typ_bind tb; exp e]
     | AwaitE e            -> "AwaitE"  $$ [exp e]
-    | AssertE e           -> "AssertE" $$ [exp e]
+    | AssertE (Runtime, e)       -> "AssertE" $$ [exp e]
+    | AssertE (Static, e)        -> "Static_AssertE" $$ [exp e]
+    | AssertE (Invariant, e)     -> "Invariant" $$ [exp e]
+    | AssertE (Precondition, e)  -> "Precondition" $$ [exp e]
+    | AssertE (Postcondition, e) -> "Postcondition" $$ [exp e]
+    | AssertE (Loop_entry, e)    -> "Loop_entry" $$ [exp e]
+    | AssertE (Loop_continue, e) -> "Loop_continue" $$ [exp e]
+    | AssertE (Loop_exit, e)     -> "Loop_exit" $$ [exp e]
+    | AssertE (Concurrency s, e) -> "Concurrency"^s $$ [exp e]
     | AnnotE (e, t)       -> "AnnotE"  $$ [exp e; typ t]
     | OptE e              -> "OptE"    $$ [exp e]
     | DoOptE e            -> "DoOptE"  $$ [exp e]

src/mo_def/syntax.ml

@@ -173,6 +173,7 @@ and exp' =
   | NotE of exp                                (* negation *)
   | AndE of exp * exp                          (* conjunction *)
   | OrE of exp * exp                           (* disjunction *)
+  | ImpliesE of exp * exp                      (* implication *)
   | IfE of exp * exp * exp                     (* conditional *)
   | SwitchE of exp * case list                 (* switch *)
   | WhileE of exp * exp                        (* while-do loop *)
@@ -184,7 +185,7 @@ and exp' =
   | DebugE of exp                              (* debugging *)
   | AsyncE of typ_bind * exp                   (* async *)
   | AwaitE of exp                              (* await *)
-  | AssertE of exp                             (* assertion *)
+  | AssertE of assert_kind * exp               (* assertion *)
   | AnnotE of exp * typ                        (* type annotation *)
   | ImportE of (string * resolved_import ref)  (* import statement *)
   | ThrowE of exp                              (* throw exception *)
@@ -195,6 +196,9 @@ and exp' =
   | AtomE of string                            (* atom *)
 *)
 
+and assert_kind =
+  | Runtime | Static | Invariant | Precondition | Postcondition | Concurrency of string | Loop_entry | Loop_continue | Loop_exit
+
 and dec_field = dec_field' Source.phrase
 and dec_field' = {dec : dec; vis : vis; stab: stab option}
 

src/mo_frontend/assertions.mly

@@ -0,0 +1,49 @@
+%{
+
+let verification_syntax_error at code msg =
+  Diag.add_msg (Option.get !Parser_lib.msg_store)
+    (Diag.error_message at code "verification syntax" msg)
+
+(* Verification mode only *)
+
+let (&&&) cond (action : Mo_def.Syntax.exp) =
+  if not cond then
+    verification_syntax_error
+      action.Source.at
+      "M0181" "verification assertions not permitted in normal mode";
+  action
+
+let is_verification () =
+  match !Parser_lib.mode with
+  | None -> assert false
+  | Some mode -> mode.Lexer_lib.verification
+
+%}
+
+(* Viper-only tokens and productions *)
+
+%token INVARIANT
+%token IMPLIES
+(*
+%nonassoc IMPLIES  (* see parser.mly *)
+*)
+
+%%
+
+%public exp_bin(B) :
+  | e1=exp_bin(B) IMPLIES e2=exp_bin(ob)
+    { ImpliesE(e1, e2) @? at $sloc }
+
+%public exp_nondec(B) :
+  | ASSERT COLON SYSTEM e=exp_nest
+    { is_verification () &&& AssertE(Static, e) @? at $sloc }
+  | ASSERT COLON INVARIANT e=exp_nest
+    { is_verification () &&& AssertE(Invariant, e) @? at $sloc }
+  | ASSERT COLON FUNC e=exp_nest
+    { is_verification () &&& AssertE(Precondition, e) @? at $sloc }
+  | ASSERT COLON RETURN e=exp_nest
+    { is_verification () &&& AssertE(Postcondition, e) @? at $sloc }
+  | ASSERT COLON s=NAT COLON ASYNC e=exp_nest
+    { is_verification () &&& AssertE(Concurrency s, e) @? at $sloc }
+
+%%

src/mo_frontend/definedness.ml

@@ -113,6 +113,7 @@ let rec exp msgs e : f = match e.it with
   | NotE e              -> exp msgs e
   | AndE (e1, e2)       -> exps msgs [e1; e2]
   | OrE (e1, e2)        -> exps msgs [e1; e2]
+  | ImpliesE (e1, e2)   -> exps msgs [e1; e2]
   | IfE (e1, e2, e3)    -> exps msgs [e1; e2; e3]
   | SwitchE (e, cs)     -> exp msgs e ++ cases msgs cs
   | TryE (e, cs)        -> exp msgs e ++ cases msgs cs
@@ -124,7 +125,7 @@ let rec exp msgs e : f = match e.it with
   | DebugE e            -> exp msgs e
   | AsyncE (_, e)    -> exp msgs e
   | AwaitE e            -> exp msgs e
-  | AssertE e           -> exp msgs e
+  | AssertE (_, e)      -> exp msgs e
   | AnnotE (e, t)       -> exp msgs e
   | OptE e              -> exp msgs e
   | DoOptE e            -> exp msgs e

src/mo_frontend/dune

@@ -4,7 +4,8 @@
   (instrumentation (backend bisect_ppx --bisect-silent yes))
 )
 (menhir
-  (modules parser)
+  (modules parser assertions)
+  (merge_into parser)
   (flags --table --inspection -v --strict)
   (infer true)
 )

src/mo_frontend/effect.ml

@@ -49,7 +49,7 @@ let rec infer_effect_exp (exp:Syntax.exp) : T.eff =
   | TagE (_, exp1)
   | DotE (exp1, _)
   | NotE exp1
-  | AssertE exp1
+  | AssertE (_, exp1)
   | LabelE (_, _, exp1)
   | BreakE (_, exp1)
   | RetE exp1
@@ -64,6 +64,7 @@ let rec infer_effect_exp (exp:Syntax.exp) : T.eff =
   | CallE (exp1, _, exp2)
   | AndE (exp1, exp2)
   | OrE (exp1, exp2)
+  | ImpliesE (exp1, exp2)
   | WhileE (exp1, exp2)
   | LoopE (exp1, Some exp2)
   | ForE (_, exp1, exp2) ->

src/mo_frontend/error_reporting.ml

@@ -116,8 +116,10 @@ let terminal2token (type a) (symbol : a terminal) : token =
       | T_ANDOP -> ANDOP
       | T_ANDASSIGN -> ANDASSIGN
       | T_AND -> AND
+      | T_IMPLIES -> IMPLIES
       | T_ADDOP -> ADDOP
       | T_ACTOR -> ACTOR
+      | T_INVARIANT -> INVARIANT
       | T_WRAPADDOP -> WRAPADDOP
       | T_WRAPSUBOP -> WRAPSUBOP
       | T_WRAPMULOP -> WRAPMULOP

src/mo_frontend/lexer_lib.ml

@@ -5,13 +5,16 @@
 *)
 type mode = {
   privileged : bool;
+  verification : bool;
 }
 
 let mode : mode = {
   privileged = Option.is_some (Sys.getenv_opt "MOC_UNLOCK_PRIM");
+  verification = Option.is_some (Sys.getenv_opt "MOC_UNLOCK_VERIFICATION");
 }
 
 let mode_priv : mode = { mode with privileged = true }
+let mode_verification : mode = { mode with verification = true }
 
 
 exception Error of Source.region * string