feat: motoko-san contributions by Serokell (#4500)

RFP-6: The second iteration of Motoko-san

High-level outline of new features:
* Support more Motoko syntax: return values, patter matching, 
  polymorphic private functions, loop labels
* Support build-in types: arrays, tuples, option, variants, records
  (immutable), `Nat`, `Text`
* Extend annotation syntax: quantifiers, loop invariants, `Prim.Ret`
  bind for return value, function post-conditions
* Add showcases: `test/viper/{reverse.mo,todo_record.mo}`

For more details see the diff of the `src/viper/README.md`

default.nix

@@ -509,7 +509,7 @@ rec {
       run-deser  = test_subdir "run-deser"  [ deser ];
       perf       = perf_subdir "perf"       [ moc nixpkgs.drun ];
       bench      = perf_subdir "bench"      [ moc nixpkgs.drun ic-wasm ];
-      # viper      = test_subdir "viper"      [ moc nixpkgs.which nixpkgs.openjdk nixpkgs.z3 ];
+      viper      = test_subdir "viper"      [ moc nixpkgs.which nixpkgs.openjdk nixpkgs.z3_4_12 ];
       inherit qc lsp unit candid profiling-graphs coverage;
     }) // { recurseForDerivations = true; };
 
@@ -818,7 +818,7 @@ EOF
           niv
           nix-update
           rlwrap # for `rlwrap moc`
-          openjdk z3 # for viper dev
+          openjdk z3_4_12 # for viper dev
           difftastic
         ] ++ lib.optional stdenv.isDarwin darwin.apple_sdk.frameworks.Security
       ));

src/mo_def/arrange.ml

@@ -116,6 +116,7 @@ module Make (Cfg : Config) = struct
     | 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 (Loop_invariant, e)-> "Loop_invariant" $$ [exp e]
     | AssertE (Concurrency s, e) -> "Concurrency"^s $$ [exp e]
     | AnnotE (e, t)       -> "AnnotE"  $$ [exp e; typ t]
     | OptE e              -> "OptE"    $$ [exp e]

src/mo_def/syntax.ml

@@ -201,7 +201,7 @@ and exp' =
 *)
 
 and assert_kind =
-  | Runtime | Static | Invariant | Precondition | Postcondition | Concurrency of string | Loop_entry | Loop_continue | Loop_exit
+  | Runtime | Static | Invariant | Precondition | Postcondition | Concurrency of string | Loop_entry | Loop_continue | Loop_exit | Loop_invariant
 
 and dec_field = dec_field' Source.phrase
 and dec_field' = {dec : dec; vis : vis; stab: stab option}

src/mo_frontend/assertions.mly

@@ -40,6 +40,8 @@ let is_verification () =
     { is_verification () &&& AssertE(Static, e) @? at $sloc }
   | ASSERT COLON INVARIANT e=exp_nest
     { is_verification () &&& AssertE(Invariant, e) @? at $sloc }
+  | ASSERT COLON LOOP COLON INVARIANT e=exp_nest
+    { is_verification () &&& AssertE(Loop_invariant, e) @? at $sloc }
   | ASSERT COLON FUNC e=exp_nest
     { is_verification () &&& AssertE(Precondition, e) @? at $sloc }
   | ASSERT COLON RETURN e=exp_nest

src/mo_frontend/typing.ml

@@ -56,9 +56,10 @@ type env =
     used_identifiers : S.t ref;
     unused_warnings : unused_warnings ref;
     reported_stable_memory : bool ref;
+    viper_mode : bool;
   }
 
-let env_of_scope msgs scope =
+let env_of_scope ?(viper_mode=false) msgs scope =
   { vals = available scope.Scope.val_env;
     libs = scope.Scope.lib_env;
     typs = scope.Scope.typ_env;
@@ -78,6 +79,7 @@ let env_of_scope msgs scope =
     used_identifiers = ref S.empty;
     unused_warnings = ref [];
     reported_stable_memory = ref false;
+    viper_mode;
   }
 
 let use_identifier env id =
@@ -1132,7 +1134,7 @@ and infer_exp' f env exp : T.typ =
   if not env.pre then begin
     assert (T.normalize t' <> T.Pre);
     let e = A.infer_effect_exp exp in
-    exp.note <- {note_typ = T.normalize t'; note_eff = e}
+    exp.note <- {note_typ = if env.viper_mode then t' else T.normalize t'; note_eff = e}
   end;
   t'
 
@@ -2561,7 +2563,7 @@ and infer_dec env dec : T.typ =
   let t =
   match dec.it with
   | ExpD exp -> infer_exp env exp
-  | LetD (pat, exp, None) -> 
+  | LetD (pat, exp, None) ->
     (* For developer convenience, ignore top-level actor and module identifiers in unused detection. *)
     (if env.in_prog && (CompUnit.is_actor_def exp || CompUnit.is_module_def exp) then
       match pat.it with
@@ -2940,12 +2942,12 @@ and infer_dec_valdecs env dec : Scope.t =
 
 (* Programs *)
 
-let infer_prog scope pkg_opt async_cap prog : (T.typ * Scope.t) Diag.result =
+let infer_prog ?(viper_mode=false) scope pkg_opt async_cap prog : (T.typ * Scope.t) Diag.result =
   Diag.with_message_store
     (fun msgs ->
       recover_opt
         (fun prog ->
-          let env0 = env_of_scope msgs scope in
+          let env0 = env_of_scope ~viper_mode msgs scope in
           let env = {
              env0 with async = async_cap;
           } in
@@ -2963,12 +2965,12 @@ let is_actor_dec d =
     obj_sort.it = T.Actor
   | _ -> false
 
-let check_actors scope progs : unit Diag.result =
+let check_actors ?(viper_mode=false) scope progs : unit Diag.result =
   Diag.with_message_store
     (fun msgs ->
       recover_opt (fun progs ->
         let prog = (CompUnit.combine_progs progs).it in
-        let env = env_of_scope msgs scope in
+        let env = env_of_scope ~viper_mode msgs scope in
         let rec go ds = function
           | [] -> ()
           | (d::ds') when is_actor_dec d ->

src/mo_frontend/typing.mli

@@ -6,10 +6,10 @@ open Scope
 
 val initial_scope : scope
 
-val infer_prog : scope -> string option -> Async_cap.async_cap -> Syntax.prog -> (typ * scope) Diag.result
+val infer_prog : ?viper_mode:bool -> scope -> string option -> Async_cap.async_cap -> Syntax.prog -> (typ * scope) Diag.result
 
 val check_lib : scope -> string option -> Syntax.lib -> scope Diag.result
-val check_actors : scope -> Syntax.prog list -> unit Diag.result
+val check_actors : ?viper_mode:bool -> scope -> Syntax.prog list -> unit Diag.result
 val check_stab_sig : scope -> Syntax.stab_sig -> (field list) Diag.result
 
 val heartbeat_type : typ

src/mo_types/type.mli

@@ -236,6 +236,8 @@ val glb : typ -> typ -> typ
 
 (* First-order substitution *)
 
+val subst : typ ConEnv.t -> typ -> typ
+
 val close : con list -> typ -> typ
 val close_binds : con list -> bind list -> bind list
 

src/pipeline/pipeline.ml

@@ -180,10 +180,10 @@ let async_cap_of_prog prog =
      else
        Async_cap.initial_cap()
 
-let infer_prog pkg_opt senv async_cap prog : (Type.typ * Scope.scope) Diag.result =
+let infer_prog ?(viper_mode=false) pkg_opt senv async_cap prog : (Type.typ * Scope.scope) Diag.result =
   let filename = prog.Source.note.Syntax.filename in
   phase "Checking" filename;
-  let r = Typing.infer_prog pkg_opt senv async_cap prog in
+  let r = Typing.infer_prog ~viper_mode pkg_opt senv async_cap prog in
   if !Flags.trace && !Flags.verbose then begin
     match r with
     | Ok ((_, scope), _) ->
@@ -198,15 +198,15 @@ let infer_prog pkg_opt senv async_cap prog : (Type.typ * Scope.scope) Diag.resul
   let* () = Definedness.check_prog prog in
   Diag.return t_sscope
 
-let rec check_progs senv progs : Scope.scope Diag.result =
+let rec check_progs ?(viper_mode=false) senv progs : Scope.scope Diag.result =
   match progs with
   | [] -> Diag.return senv
   | prog::progs' ->
     let open Diag.Syntax in
     let async_cap = async_cap_of_prog prog in
-    let* _t, sscope = infer_prog senv None async_cap prog in
+    let* _t, sscope = infer_prog ~viper_mode senv None async_cap prog in
     let senv' = Scope.adjoin senv sscope in
-    check_progs senv' progs'
+    check_progs ~viper_mode senv' progs'
 
 let check_lib senv pkg_opt lib : Scope.scope Diag.result =
   let filename = lib.Source.note.Syntax.filename in
@@ -421,14 +421,14 @@ let chase_imports parsefn senv0 imports : (Syntax.lib list * Scope.scope) Diag.r
   in
   Diag.map (fun () -> (List.rev !libs, !senv)) (go_set None imports)
 
-let load_progs parsefn files senv : load_result =
+let load_progs ?(viper_mode=false) parsefn files senv : load_result =
   let open Diag.Syntax in
   let* parsed = Diag.traverse (parsefn Source.no_region) files in
   let* rs = resolve_progs parsed in
   let progs' = List.map fst rs in
   let libs = List.concat_map snd rs in
   let* libs, senv' = chase_imports parsefn senv libs in
-  let* senv'' = check_progs senv' progs' in
+  let* senv'' = check_progs ~viper_mode senv' progs' in
   Diag.return (libs, progs', senv'')
 
 let load_decl parse_one senv : load_decl_result =
@@ -509,12 +509,13 @@ type viper_result = (string * (Source.region -> Source.region option)) Diag.resu
 
 let viper_files' parsefn files : viper_result =
   let open Diag.Syntax in
-  let* libs, progs, senv = load_progs parsefn files initial_stat_env in
-  let* () = Typing.check_actors senv progs in
+  let* libs, progs, senv = load_progs ~viper_mode:true parsefn files initial_stat_env in
+  let* () = Typing.check_actors ~viper_mode:true senv progs in
   let prog = CompUnit.combine_progs progs in
   let u = CompUnit.comp_unit_of_prog false prog in
-  let* v = Viper.Trans.unit u in
-  let s = Viper.Pretty.prog_mapped "" v in
+  let reqs = Viper.Common.init_reqs () in
+  let* v = Viper.Trans.unit reqs (Viper.Prep.prep_unit u) in
+  let s = Viper.Pretty.prog_mapped "" (Viper.Prelude.prelude reqs) v in
   Diag.return s
 
 let viper_files files : viper_result =

src/pipeline/pipeline.mli

@@ -38,4 +38,4 @@ val compile_files : Flags.compile_mode -> bool -> string list -> compile_result
 (* For use in the IDE server *)
 type load_result =
   (Syntax.lib list * Syntax.prog list * Scope.scope) Diag.result
-val load_progs : parse_fn -> string list -> Scope.scope -> load_result
+val load_progs : ?viper_mode:bool -> parse_fn -> string list -> Scope.scope -> load_result

src/prelude/prim.mo

@@ -500,3 +500,17 @@ func regionStoreBlob(r : Region, offset : Nat64, val :  Blob) : () =
 let call_raw = @call_raw;
 
 func performanceCounter(counter : Nat32) : Nat64 = (prim "performanceCounter" : (Nat32) -> Nat64) counter;
+
+// predicates for motoko-san
+
+func forall<T>(f: T -> Bool): Bool {
+  (prim "forall" : <T>(T -> Bool) -> Bool) <T>(f);
+};
+
+func exists<T>(f: T -> Bool): Bool {
+  (prim "exists" : <T>(T -> Bool) -> Bool) <T>(f);
+};
+
+func Ret<T>(): T {
+  (prim "viperRet" : <T>() -> T) ();
+};