diff --git a/.gitignore b/.gitignore index c22647c5079..c00c4e5497e 100644 --- a/.gitignore +++ b/.gitignore @@ -13,6 +13,9 @@ result* /samples/**/*.txt +**/*.mo.vpr +test/viper/tmp + enable-internals # Editor configuration diff --git a/Changelog.md b/Changelog.md index 37e07283c25..965c22f6386 100644 --- a/Changelog.md +++ b/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`) diff --git a/README.md b/README.md index d69f93eef71..fa08f18c1f4 100644 --- a/README.md +++ b/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 diff --git a/default.nix b/default.nix index 21e8384ef50..bc1b8fa7f14 100644 --- a/default.nix +++ b/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. diff --git a/emacs/motoko-mode.el b/emacs/motoko-mode.el index 19f25a2cc72..c3fc3412d04 100644 --- a/emacs/motoko-mode.el +++ b/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 diff --git a/src/exes/moc.ml b/src/exes/moc.ml index a1da31ca595..c00e8e95870 100644 --- a/src/exes/moc.ml +++ b/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 diff --git a/src/ir_def/construct.ml b/src/ir_def/construct.ml index e00c444250b..faa91680c22 100644 --- a/src/ir_def/construct.ml +++ b/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 diff --git a/src/ir_def/construct.mli b/src/ir_def/construct.mli index 4692835dc1f..91cfbfc6419 100644 --- a/src/ir_def/construct.mli +++ b/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 diff --git a/src/js/common.ml b/src/js/common.ml index 20e6a776b09..483211c322c 100644 --- a/src/js/common.ml +++ b/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 diff --git a/src/js/moc_js.ml b/src/js/moc_js.ml index 8790c3346b4..0918d52b606 100644 --- a/src/js/moc_js.ml +++ b/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 diff --git a/src/lang_utils/error_codes.ml b/src/lang_utils/error_codes.ml index 458bfb4aa7c..7f6f76df51e 100644 --- a/src/lang_utils/error_codes.ml +++ b/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 *) ] diff --git a/src/languageServer/imports.ml b/src/languageServer/imports.ml index 975fe0e7b53..0c269580990 100644 --- a/src/languageServer/imports.ml +++ b/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 diff --git a/src/lowering/desugar.ml b/src/lowering/desugar.ml index 08e78ffaa1e..177944ed0b2 100644 --- a/src/lowering/desugar.ml +++ b/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)) diff --git a/src/mo_def/arrange.ml b/src/mo_def/arrange.ml index 7654c2553a4..8c4cb9cbfa5 100644 --- a/src/mo_def/arrange.ml +++ b/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] diff --git a/src/mo_def/syntax.ml b/src/mo_def/syntax.ml index 69b445bcdd8..6225664b5fd 100644 --- a/src/mo_def/syntax.ml +++ b/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} diff --git a/src/mo_frontend/assertions.mly b/src/mo_frontend/assertions.mly new file mode 100644 index 00000000000..58311e3cc40 --- /dev/null +++ b/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 } + +%% diff --git a/src/mo_frontend/definedness.ml b/src/mo_frontend/definedness.ml index 6ecdeeb72a1..2328089a5f6 100644 --- a/src/mo_frontend/definedness.ml +++ b/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 diff --git a/src/mo_frontend/dune b/src/mo_frontend/dune index 7ed50b1a97a..fc19593f91e 100644 --- a/src/mo_frontend/dune +++ b/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) ) diff --git a/src/mo_frontend/effect.ml b/src/mo_frontend/effect.ml index d5276bbb705..55c24816d32 100644 --- a/src/mo_frontend/effect.ml +++ b/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) -> diff --git a/src/mo_frontend/error_reporting.ml b/src/mo_frontend/error_reporting.ml index a62aba376e1..0f8afd5b6c4 100644 --- a/src/mo_frontend/error_reporting.ml +++ b/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 diff --git a/src/mo_frontend/lexer_lib.ml b/src/mo_frontend/lexer_lib.ml index 73deaf6c870..4ba54102d06 100644 --- a/src/mo_frontend/lexer_lib.ml +++ b/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 diff --git a/src/mo_frontend/parser.mly b/src/mo_frontend/parser.mly index e4be5f7abf5..4a877a96dab 100644 --- a/src/mo_frontend/parser.mly +++ b/src/mo_frontend/parser.mly @@ -236,6 +236,8 @@ and objblock s dec_fields = %token PRIM %token UNDERSCORE +%nonassoc IMPLIES (* see assertions.mly *) + %nonassoc RETURN_NO_ARG IF_NO_ELSE LOOP_NO_WHILE %nonassoc ELSE WHILE @@ -550,7 +552,7 @@ lit : bl : DISALLOWED { PrimE("dummy") @? at $sloc } -ob : e=exp_obj { e } +%public ob : e=exp_obj { e } exp_obj : | LCURLY efs=seplist(exp_field, semicolon) RCURLY @@ -568,7 +570,6 @@ exp_plain : exp_nullary(B) : | e=B - { e } | e=exp_plain { e } | x=id @@ -625,7 +626,7 @@ exp_un(B) : | FROM_CANDID e=exp_un(ob) { FromCandidE e @? at $sloc } -exp_bin(B) : +%public exp_bin(B) : | e=exp_un(B) { e } | e1=exp_bin(B) op=binop e2=exp_bin(ob) @@ -639,7 +640,7 @@ exp_bin(B) : | e=exp_bin(B) COLON t=typ_nobin { AnnotE(e, t) @? at $sloc } -exp_nondec(B) : +%public exp_nondec(B) : | e=exp_bin(B) { e } | e1=exp_bin(B) ASSIGN e2=exp(ob) @@ -655,7 +656,7 @@ exp_nondec(B) : | AWAIT e=exp_nest { AwaitE(e) @? at $sloc } | ASSERT e=exp_nest - { AssertE(e) @? at $sloc } + { AssertE(Runtime, e) @? at $sloc } | LABEL x=id rt=annot_opt e=exp_nest { let x' = ("continue " ^ x.it) @@ x.at in let unit () = TupT [] @! at $sloc in @@ -717,9 +718,8 @@ exp(B) : | d=dec_var { match d.it with ExpD e -> e | _ -> BlockE([d]) @? at $sloc } -exp_nest : +%public exp_nest : | e=block - { e } | e=exp(bl) { e } diff --git a/src/mo_frontend/parser_lib.ml b/src/mo_frontend/parser_lib.ml index 63c331d1174..3c22db4836b 100644 --- a/src/mo_frontend/parser_lib.ml +++ b/src/mo_frontend/parser_lib.ml @@ -2,5 +2,6 @@ exception Imports of Mo_def.Syntax.dec list (* Temporary hack! *) let msg_store : Diag.msg_store option ref = ref None +let mode : Lexer_lib.mode option ref = ref None let triv_table : Mo_def.Trivia.triv_table ref = ref Mo_def.Trivia.empty_triv_table diff --git a/src/mo_frontend/parsing.ml b/src/mo_frontend/parsing.ml index 112c79c27ed..f5ad803b60e 100644 --- a/src/mo_frontend/parsing.ml +++ b/src/mo_frontend/parsing.ml @@ -70,11 +70,12 @@ let slice_lexeme lexbuf i1 i2 = then "" (* Too rare to care *) else Bytes.sub_string lexbuf.lex_buffer offset len -let parse error_detail checkpoint lexer lexbuf = +let parse mode error_detail checkpoint lexer lexbuf = Diag.with_message_store (fun m -> try (* Temporary hack! *) Parser_lib.msg_store := Some m; + Parser_lib.mode := Some mode; Some (E.entry checkpoint lexer) with E.Error ((start, end_), explanations) -> let at = diff --git a/src/mo_frontend/parsing.mli b/src/mo_frontend/parsing.mli index 8b0a16296f8..1d04d9fd880 100644 --- a/src/mo_frontend/parsing.mli +++ b/src/mo_frontend/parsing.mli @@ -8,7 +8,8 @@ type error_detail = int (* TODO: make this a datatype! *) exception Error of string * Lexing.position * Lexing.position -val parse : error_detail -> +val parse : Lexer_lib.mode -> + error_detail -> 'a Parser.MenhirInterpreter.checkpoint -> Parser.MenhirInterpreter.supplier -> Lexing.lexbuf -> diff --git a/src/mo_frontend/printers.ml b/src/mo_frontend/printers.ml index 12e16596ba0..f8bb52ed9d3 100644 --- a/src/mo_frontend/printers.ml +++ b/src/mo_frontend/printers.ml @@ -131,8 +131,10 @@ let string_of_symbol = function | X (T T_ANDOP) -> binop "&" | X (T T_ANDASSIGN) -> binassign "&=" | X (T T_AND) -> "and" + | X (T T_IMPLIES) -> "implies" | X (T T_ADDOP) -> unop "+" | X (T T_ACTOR) -> "actor" + | X (T T_INVARIANT) -> "invariant" (* non-terminals *) | X (N N_bl) -> "" | X (N N_case) -> "" diff --git a/src/mo_frontend/source_lexer.mll b/src/mo_frontend/source_lexer.mll index 317c9014d0a..479bcf53ce6 100644 --- a/src/mo_frontend/source_lexer.mll +++ b/src/mo_frontend/source_lexer.mll @@ -213,6 +213,8 @@ rule token mode = parse | "if" { IF } | "ignore" { IGNORE } | "in" { IN } + | "invariant" as s { if mode.verification then INVARIANT else ID s } + | "implies" as s { if mode.verification then IMPLIES else ID s } | "import" { IMPORT } | "module" { MODULE } | "not" { NOT } diff --git a/src/mo_frontend/source_token.ml b/src/mo_frontend/source_token.ml index ae4ee7942f6..ffb647e68e1 100644 --- a/src/mo_frontend/source_token.ml +++ b/src/mo_frontend/source_token.ml @@ -55,6 +55,7 @@ type token = | BANG | AND | OR + | IMPLIES | NOT | IMPORT | MODULE @@ -114,6 +115,7 @@ type token = | TEXT of string | PRIM | UNDERSCORE + | INVARIANT (* Trivia *) | LINEFEED of line_feed | SINGLESPACE @@ -177,6 +179,7 @@ let to_parser_token : | BANG -> Ok Parser.BANG | AND -> Ok Parser.AND | OR -> Ok Parser.OR + | IMPLIES -> Ok Parser.IMPLIES | NOT -> Ok Parser.NOT | IMPORT -> Ok Parser.IMPORT | MODULE -> Ok Parser.MODULE @@ -236,6 +239,7 @@ let to_parser_token : | TEXT s -> Ok (Parser.TEXT s) | PRIM -> Ok Parser.PRIM | UNDERSCORE -> Ok Parser.UNDERSCORE + | INVARIANT -> Ok Parser.INVARIANT (*Trivia *) | SINGLESPACE -> Error (Space 1) | SPACE n -> Error (Space n) @@ -361,6 +365,8 @@ let string_of_parser_token = function | Parser.TEXT _ -> "TEXT of string" | Parser.PRIM -> "PRIM" | Parser.UNDERSCORE -> "UNDERSCORE" + | Parser.INVARIANT -> "INVARIANT" + | Parser.IMPLIES -> "IMPLIES" let is_lineless_trivia : token -> void trivia option = function | SINGLESPACE -> Some (Space 1) diff --git a/src/mo_frontend/static.ml b/src/mo_frontend/static.ml index 255b23a687a..8d8b54b9b5d 100644 --- a/src/mo_frontend/static.ml +++ b/src/mo_frontend/static.ml @@ -86,6 +86,7 @@ let rec exp m e = match e.it with | ThrowE _ | TryE _ | BangE _ + | ImpliesE _ -> err m e.at and dec_fields m dfs = List.iter (fun df -> dec m df.it.dec) dfs diff --git a/src/mo_frontend/traversals.ml b/src/mo_frontend/traversals.ml index 62564713e8d..86ba96bd143 100644 --- a/src/mo_frontend/traversals.ml +++ b/src/mo_frontend/traversals.ml @@ -15,7 +15,7 @@ let rec over_exp (f : exp -> exp) (exp : exp) : exp = match exp.it with | TagE (x, exp1) -> f { exp with it = TagE (x, over_exp f exp1) } | DotE (exp1, x) -> f { exp with it = DotE (over_exp f exp1, x) } | NotE exp1 -> f { exp with it = NotE (over_exp f exp1) } - | AssertE exp1 -> f { exp with it = AssertE (over_exp f exp1) } + | AssertE (how, exp1) -> f { exp with it = AssertE (how, over_exp f exp1) } | LabelE (x, y, exp1) -> f { exp with it = LabelE (x, y, over_exp f exp1) } | BreakE (x, exp1) -> f { exp with it = BreakE (x, over_exp f exp1) } | RetE exp1 -> f { exp with it = RetE (over_exp f exp1) } @@ -37,6 +37,8 @@ let rec over_exp (f : exp -> exp) (exp : exp) : exp = match exp.it with f { exp with it = AndE (over_exp f exp1, over_exp f exp2) } | OrE (exp1, exp2) -> f { exp with it = OrE (over_exp f exp1, over_exp f exp2) } + | ImpliesE (exp1, exp2) -> + f { exp with it = ImpliesE (over_exp f exp1, over_exp f exp2) } | WhileE (exp1, exp2) -> f { exp with it = WhileE (over_exp f exp1, over_exp f exp2) } | LoopE (exp1, exp2_opt) -> diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index fbbc5fafe25..b15b8c7bcb7 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -754,7 +754,7 @@ let rec is_explicit_exp e = | BreakE _ | RetE _ | ThrowE _ -> false | VarE _ - | RelE _ | NotE _ | AndE _ | OrE _ | ShowE _ | ToCandidE _ | FromCandidE _ + | RelE _ | NotE _ | AndE _ | OrE _ | ImpliesE _ | ShowE _ | ToCandidE _ | FromCandidE _ | AssignE _ | IgnoreE _ | AssertE _ | DebugE _ | WhileE _ | ForE _ | AnnotE _ | ImportE _ -> @@ -1245,6 +1245,7 @@ and infer_exp'' env exp : T.typ = let t1, ve1 = infer_pat_exhaustive (if T.is_shared_sort sort then local_error else warn) env' pat in let ve2 = T.Env.adjoin ve ve1 in let ts2 = List.map (check_typ env') ts2 in + typ.note <- T.seq ts2; (* HACK *) let codom = T.codom c (fun () -> T.Con(List.hd cs,[])) ts2 in if not env.pre then begin let env'' = @@ -1302,6 +1303,12 @@ and infer_exp'' env exp : T.typ = check_exp_strong env T.bool exp2 end; T.bool + | ImpliesE (exp1, exp2) -> + if not env.pre then begin + check_exp_strong env T.bool exp1; + check_exp_strong env T.bool exp2 + end; + T.bool | IfE (exp1, exp2, exp3) -> if not env.pre then check_exp_strong env T.bool exp1; let t2 = infer_exp env exp2 in @@ -1438,7 +1445,7 @@ and infer_exp'' env exp : T.typ = "expected async type, but expression has type%a" display_typ_expand t1 ) - | AssertE exp1 -> + | AssertE (_, exp1) -> if not env.pre then check_exp_strong env T.bool exp1; T.unit | AnnotE (exp1, typ) -> diff --git a/src/mo_interpreter/interpret.ml b/src/mo_interpreter/interpret.ml index 41e180b237b..c3130ed7367 100644 --- a/src/mo_interpreter/interpret.ml +++ b/src/mo_interpreter/interpret.ml @@ -567,6 +567,12 @@ and interpret_exp_mut env exp (k : V.value V.cont) = then k v1 else interpret_exp env exp2 k ) + | ImpliesE (exp1, exp2) -> + interpret_exp env exp1 (fun v1 -> + interpret_exp env exp2 (fun v2 -> + k V.(Bool (as_bool v1 <= as_bool v2)) + ) + ) | IfE (exp1, exp2, exp3) -> interpret_exp env exp1 (fun v1 -> if V.as_bool v1 @@ -641,12 +647,13 @@ and interpret_exp_mut env exp (k : V.value V.cont) = | AwaitE exp1 -> interpret_exp env exp1 (fun v1 -> await env exp.at (V.as_async v1) k) - | AssertE exp1 -> + | AssertE (Runtime, exp1) -> interpret_exp env exp1 (fun v -> if V.as_bool v then k V.unit else trap exp.at "assertion failure" ) + | AssertE (_, exp1) -> k V.unit | AnnotE (exp1, _typ) -> interpret_exp env exp1 k | IgnoreE exp1 -> diff --git a/src/pipeline/dune b/src/pipeline/dune index c4ae822f552..a756a57222a 100644 --- a/src/pipeline/dune +++ b/src/pipeline/dune @@ -18,6 +18,7 @@ ir_passes codegen rts + viper ) (inline_tests) (preprocess (per_module ((pps ppx_inline_test) resolve_import_test))) diff --git a/src/pipeline/pipeline.ml b/src/pipeline/pipeline.ml index 0f0e057da2b..eaeabf1b0ec 100644 --- a/src/pipeline/pipeline.ml +++ b/src/pipeline/pipeline.ml @@ -96,7 +96,7 @@ let generic_parse_with mode lexer parser name : _ Diag.result = let* mk_syntax = try Parser_lib.triv_table := triv_table; - Parsing.parse (!Flags.error_detail) (parser lexer.Lexing.lex_curr_p) tokenizer lexer + Parsing.parse mode (!Flags.error_detail) (parser lexer.Lexing.lex_curr_p) tokenizer lexer with Lexer.Error (at, msg) -> Diag.error at"M0002" "syntax" msg in let phrase = mk_syntax name in @@ -132,6 +132,7 @@ let parse_file' mode at filename : (Syntax.prog * rel_path) Diag.result = ) let parse_file = parse_file' Lexer.mode +let parse_verification_file = parse_file' Lexer.mode_verification (* Import file name resolution *) @@ -236,7 +237,7 @@ let internals, initial_stat_env = let parse_stab_sig s name = let open Diag.Syntax in - let mode = {Lexer.privileged = false} in + let mode = Lexer.{privileged = false; verification = false} in let lexer = Lexing.from_string s in let parse = Parser.Incremental.parse_stab_sig in let* sig_ = generic_parse_with mode lexer parse name in @@ -246,7 +247,7 @@ let parse_stab_sig_from_file filename : Syntax.stab_sig Diag.result = let ic = Stdlib.open_in filename in Diag.finally (fun () -> close_in ic) ( let open Diag.Syntax in - let mode = {Lexer.privileged = false} in + let mode = Lexer.{privileged = false; verification = false} in let lexer = Lexing.from_channel ic in let parse = Parser.Incremental.parse_stab_sig in let* sig_ = generic_parse_with mode lexer parse filename in @@ -483,6 +484,23 @@ let check_files' parsefn files : check_result = let check_files files : check_result = check_files' parse_file files +(* Generate Viper *) + +type viper_result = (string * (Source.region -> Source.region option)) Diag.result + +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 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 + Diag.return s + +let viper_files files : viper_result = + viper_files' parse_verification_file files + (* Generate IDL *) let generate_idl files : Idllib.Syntax.prog Diag.result = diff --git a/src/pipeline/pipeline.mli b/src/pipeline/pipeline.mli index a814e2c5583..c3b4f024e64 100644 --- a/src/pipeline/pipeline.mli +++ b/src/pipeline/pipeline.mli @@ -15,6 +15,8 @@ val print_deps: string -> unit val check_files : string list -> unit Diag.result val check_files' : parse_fn -> string list -> unit Diag.result +val viper_files : string list -> (string * (Source.region -> Source.region option)) Diag.result + val stable_compatible : string -> string -> unit Diag.result val generate_idl : string list -> Idllib.Syntax.prog Diag.result diff --git a/src/viper/README.md b/src/viper/README.md new file mode 100644 index 00000000000..a013f081873 --- /dev/null +++ b/src/viper/README.md @@ -0,0 +1,255 @@ +_Motoko-san_ +============ + +> Disclaimer — this is an _early prototype_; in particular: +> * This project comes with no guarantees whatsoever. +> * The [currently supported subset of Motoko](#Subset) is insufficient for most real-world applications. +> * DFINITY currently has no plans to continue the development of _Motoko-san_. + + +_Motoko-san_ is a prototype code-level verifier for Motoko. The project started at the DFINITY Foundation as a way to demonstrate that Motoko (and the Internet Computer in general) are well-suited for developing formally verified Web3 software. + +-------------------------------------------------------------------------------- +**Jump to:** + +**[Introduction](#Introduction) —** + [Overview](#Overview) + | [Formal specification](#FormalSpecs) + | [Static vs. dynamic assertions](#statVsDyn) + | [Testing vs. formal verification](#testsVsVerif) + | [Precondition of public functions](#publicFuncPreconds) + | [Examples](#Examples) + +**[Contributing](#Contrib) —** + [Building](#Building) + | [Running](#Running) + | [Testing](#Testing) + | [File structure](#Struct) + +**[Currently supported features](#Subset)** + +**[Further information](#Further)** + +-------------------------------------------------------------------------------- + + +Introduction +------------ + + +**Overview** + + +The verifier is implemented as a `moc` compiler feature. When `moc --viper $FILE` is invoked, the Motoko source code from `$FILE` is first translated into the Viper intermediate verification language (currently emitted into stdout) and then compiled. The generated Viper program can be submitted to the Viper tool. If the generated Viper program verifies, this implies that the Motoko source code respects the _formal code specification_, e.g., canister invariants, and that Viper established the corresponding formal proof of correctness. + +**Formal code specification** + + +Formal code specifications are written as part of the Motoko source code. These specifications are _static_, i.e., they do not affect the canister's runtime behavior. If a Motoko canister is compiled with `moc --viper`, it may contain static code specifications defined via the following keywords (`exp : Type` below denotes an expression of type `Type`): + +* `assert:invariant (exp : Bool);` — actor-level invariant; must be ensured right after canister initialization and after every _atomic block_ execution. May appear only at the level of actor members. +* `assert:1:async (exp : Bool);` — an `await async { ... }` block may include this as the first statement; the intention is two-fold: + * at most _one_ instance of this code block can be pending execution. + * specify that the property `exp` is _intended_ to hold when this block execution begins. + * require that the tool actually _checks_ whether this assumption holds (given this actor's entire source code) +* `assert:system (exp : Bool);` — a _static assertion_ that asks the verifier to prove that the property `exp` holds. Useful while designing code-level canister specifications. + +Note: the above syntax is provisional. It has been used so far to avoid introducing breaking changes to the Motoko grammar. In the future, _Motoko-san_ may switch to bespoke syntax for code specifications. + +**Static vs. dynamic assertions** + + +The expression `assert ` (which is already available in Motoko proper) means a _dynamic assertion_, i.e., a runtime check of the Boolean condition ``. Note, however, that adding an `assert ` expression (for some Boolean expression ``) affects the static verification of the canister. Concretely, the verifier will _take for granted_ that `` holds after this statement (since any execution violating this assumption would trap). + +**Testing vs. formal verification** + + +Dynamic assertions can also be used for testing. Of course, the downside of testing is that if is typically not feasible to test against _all_ possible scenarios; the untested scenarios can be exploited by an attacker. In contrast, formal verification relies on statically known information to _prove the absence of attacks_. + +**Precondition of public functions** + + +In particular, dynamic assertions are very useful for specifying _preconditions_ of an actor's public functions (i.e., functions exposed in the Candid API configuration). Since such functions can be invoked by anyone; the identity of the caller is statically unknown. It is thus necessary to check all of the assumptions at runtime, by writing `assert `(here, `` denotes some `Bool` expression representing a function's precondition). Conversely, writing `assert:system ` at the top of a public function will never verify because _Motoko-san_ has zero knowledge about the caller. + +**Examples** + + +To get a better idea about how code-level specifications help formalize what a Motoko canister is intended to do, please refer to the examples in `moc/test/viper`. + +Contributing to _Motoko-san_ +---------------------------- + + +**Building the Motoko compiler** + + +1. Clone https://github.com/dfinity/motoko + ```bash + cd motoko + ``` +4. Install Nix: + ```bash + curl -L https://nixos.org/nix/install | sh + ``` +5. Obtain Nix cache (this speeds up the following steps): + ```bash + nix-env -iA cachix -f https://cachix.org/api/v1/install + cachix use ic-hs-test + ``` +6. Enter Nix shell (the first run of this command may take a while): + ```bash + nix-shell + ``` +7. Finally, build the Motoko compiler runtime and the compiler itself: + ```bash + [nix-shell:motoko]$ make -C rts + [nix-shell:motoko]$ make -C src + ``` + + +**Running _Motoko-san_** + + +```bash +[nix-shell:motoko] moc -viper input.mo > output.vpr +``` + +You may then verify the `output.vpr` file using [Viper](https://viper.ethz.ch/). Soon, there will be an interactive IDE integration for VS Code, s.t. the outputs do not need to be verified by manually invoking Viper. + +**Testing _Motoko-san_** + + +After modifying the code and recompiling `moc`, don't forget to test the changes by running +```bash +[nix-shell:motoko]$ make -C test/viper +``` + +Each test case consists of a (formally specified) Motoko source file, say, `$TEST` (e.g., `invariant.mo`) and the expected test results, represented via a triplet of files: +* `test/viper/ok/$TEST.vpr.ok` — what the Motoko compiler is expected to generate; this should be a Viper program. +* `test/viper/ok/$TEST.silicon.ok` — verification errors reported by the Viper tool. For example: + ``` + [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@7.13--7.24) + ``` + Note: Silicon is the name of one of the backends supported by Viper. +* `test/viper/ok/$TEST.silicon.ret.ok` — the return code from running Viper on this input. For example: + ``` + Return code 1 + ``` + +**File structure** + + +The implementation of _Motoko-san_ consists of the following source files: + +* `src/viper/syntax.ml` — the Viper AST implementation. +* `src/viper/pretty.ml` — the Viper pretty printer. Used for serializing Viper AST into text. +* `src/viper/trans.ml` — the Motoko-to-Viper translation. Implements the logic of _Motoko-san_. + + +Currently supported language features +------------------------------------- + + +_Motoko-san_ is an early prototype. The tool supports only a modest subset of [_Motoko proper_](https://internetcomputer.org/docs/current/developer-docs/build/cdks/motoko-dfinity/about-this-guide), which is not sufficient for most real-world applications. However, we hope that _Motoko-san_ will enable the community to build more sophisticated Motoko code-level verifiers, simply by extending this prototype. In particular, the tool enables verifying _reentrancy safety_ in simple (asynchronous) smart contracts (e.g., `test/viper/claim.mo`). + +Below, we summarize the language features that _Motoko-san_ currently supports. For each feature, we try to estimate the complexity of its natural generalization. For that purpose, we use the terms _trivial_ (e.g., extending code by analogy), _simple_ (we already know how to do it), _hard_ (more discussions would be needed to figure out the exact approach or feasible level of generality). + +* **Literal actor declarations** — The only supported top-level entity is an actor literal: + + `actor ClaimReward { ... }` and `actor { ... }` + + Extending to actor classes and modules is _simple_. + +* **Primitive types** — Only integer and Boolean types are supported (including literals of these types): + + * `Bool`: `not`, `or`, `and`, `implies` (short circuiting semantics) + + * `Int`: `+`, `/`, `*`, `-`, `%` + + * Relations: `==`, `!=`, `<`, `>`, `>=`, `<=` + + Supporting `Text`, `Nat`, `Int32`, tuples, record, and variants is _simple_. + + Supporting `Option` types is _trivial_. + + Supporting `async` types is _hard_. + + Supporting `Float`, function types, co-inductive, mutually recursive, and sub-typing is _hard_. + + Supporting container types and generic types, e.g., arrays (`[var T]`) and `HashMap`, is _hard_. + +* **Declarations** + + * **Actor fields** + * Mutable: `var x = ...` + * Immutable: `let y = ...` + * Fields may _not_ be initialized via block expressions: `let z = { ... };` + + * **Public functions** — Only functions of `async ()` type with no arguments are supported: + + `public func claim() : async () = { ... };` + + Supporting function arguments and return values is _simple_. + + * **Private functions** — Currently not supported (extension is _simple_). + + * **Local declarations** — Only local variable declarations with trivial left-hand side are supported: + + `var x = ...;` and `let y = ...;` + + Supporting pattern matching declarations (e.g., `let (a, b) = ...;`) is _simple_. + +* **Statements** + + * `()`-typed block statements and sequential composition: + + `{ var x = 0 : Int; x := x + 1; }` + + Supporting `let y = do { let y = 1 : Int; y + y };` is _simple_. + + * Runtime assertions: `assert i <= MAX;` + + * Assignments (to local variables and actor fields): `x := x + 1` + + * `if-[else]` statements + + Supporting pattern-matching is conceptually _simple_. + + * `while` loops (loop invariants are not currently supported) + + Supporting `for` loops is _simple_. + + Supporting `break` and `continue` is _simple_. + + * `await async { ... }` — Asynchronous code blocks that are immediately awaited on. + + Supporting general `await`s and `async`s is _hard_. + + Supporting async function calls is _simple_. + +* **Static code specifications** — Note that the syntax is provisional: + + * `assert:invariant` — Canister-level invariants + + * `assert:1:async` — Async constraints (at block entry) + + Extending to support, e.g., `assert:`_`N`_`:async` constraints (for _`N`_ > 1) is _simple_. + + Extending to support async constraints at block exit is _trivial_. + + * `assert:func` — Function preconditions + + * `assert:return` — Function postconditions + + * `assert:system` — Compile-time assertions + + **Loop invariants** — Extension is _simple_. + + **Pure functions** — The tool could be easily extended with a keyword, e.g., `@pure`, to specify functions that are verifier to be side-effect free; such functions could be used inside other code specifications, e.g., `assert:invariant is_okay()` for some `@pure func is_okay() : Bool`. This feature requires private functions. + +Further information +------------------- + + +If you have questions, please contact the Motoko compiler developers. You may do that, e.g., by filing a ticket via https://github.com/dfinity/motoko/issues/new +(please add `viper` into the labels). diff --git a/src/viper/dune b/src/viper/dune new file mode 100644 index 00000000000..e983e120de7 --- /dev/null +++ b/src/viper/dune @@ -0,0 +1,6 @@ +(library + (name viper) + + (libraries lib wasm num lang_utils mo_def mo_types mo_values) + (instrumentation (backend bisect_ppx --bisect-silent yes)) +) diff --git a/src/viper/pretty.ml b/src/viper/pretty.ml new file mode 100644 index 00000000000..f1bdfcd2c0a --- /dev/null +++ b/src/viper/pretty.ml @@ -0,0 +1,231 @@ +open Source +open Syntax + +open Format + +let marks = ref [] + +let pr = pp_print_string + +let comma ppf () = fprintf ppf ",@ " + +let semi ppf () = fprintf ppf ";@ " + +let pp_info ppf NoInfo = () + +let rec pp_prog ppf p = + match p.it with + | is -> + fprintf ppf "@[%a@]" + (pp_print_list pp_item) is + +and pp_item ppf i = + match i.it with + | FieldI (id, typ) -> + fprintf ppf "@[<2>field %s:@ %a@]" + id.it + pp_typ typ + | MethodI (id, locals, rets, pres, posts, bo) -> + marks := i.at :: !marks; + fprintf ppf "\017@[method %s%a@; %a@; %a@; %a@; %a@]\019" + id.it + pp_locals locals + pp_returns rets + pp_pres pres + pp_posts posts + pp_block_opt bo + | InvariantI (inv_name, e) -> (* TODO: srcloc mapping *) + fprintf ppf "@[<2>define %s($Self) (%a)@]" inv_name pp_exp e + +and pp_block_opt ppf = function + | None -> () + | Some seqn -> + pp_seqn ppf seqn + +and pp_seqn ppf seqn = + let (ds, ss) = seqn.it in + fprintf ppf "@[{ %a@ %a @;<0 -2>}@]" + (pp_print_list pp_decl) ds + (pp_print_list pp_stmt) ss + +and pp_decl ppf decl = + let (id, typ) = decl.it in + fprintf ppf "@[var %s: %a@]" + id.it + pp_typ typ + +and pp_pres ppf exps = + fprintf ppf "@[%a@]" (pp_print_list pp_pre) exps + +and pp_pre ppf exp = + fprintf ppf "@[requires %a@]" pp_exp exp + +and pp_posts ppf exps = + fprintf ppf "@[%a@]" (pp_print_list pp_post) exps + +and pp_post ppf exp = + fprintf ppf "@[ensures %a@]" pp_exp exp + +and pp_local ppf (id, typ) = + fprintf ppf "@[<2>%s: %a@]" + id.it + pp_typ typ + +and pp_locals ppf pars = + fprintf ppf "@[<1>(%a)@]" + (pp_print_list ~pp_sep:comma (pp_local)) pars + +and pp_returns ppf pars = + match pars with + | [] -> () + | _ -> + fprintf ppf "@[<1> returns (%a)@]" + (pp_print_list ~pp_sep:comma (pp_local)) pars + +and pp_typ ppf t = + match t.it with + | IntT -> pr ppf "Int" + | BoolT -> pr ppf "Bool" + | RefT -> pr ppf "Ref" + +and pp_exp ppf exp = + match exp.it with + | LocalVar (id, _) -> + fprintf ppf "%s" id.it + | FldAcc fldacc -> + pp_fldacc ppf fldacc + | MacroCall (m, e) -> + fprintf ppf "@[%s(%a)@]" m pp_exp e + | NotE e -> + fprintf ppf "@[(!%a)@]" pp_exp e + | MinusE e -> + fprintf ppf "@[(-%a)@]" pp_exp e + | NullLitE -> + fprintf ppf "null" + | BoolLitE b -> + fprintf ppf "%s" (if b then "true" else "false") + | IntLitE i -> + fprintf ppf "%s" String.(of_seq (Seq.filter (fun c -> c <> '_') (to_seq (Mo_values.Numerics.Int.to_string i)))) + | AddE (e1, e2) | SubE (e1, e2) | MulE (e1, e2) | DivE (e1, e2) | ModE (e1, e2) + | EqCmpE (e1, e2) | NeCmpE (e1, e2) | GtCmpE (e1, e2) | GeCmpE (e1, e2) | LtCmpE (e1, e2) | LeCmpE (e1, e2) + | Implies (e1, e2) | OrE (e1, e2) | AndE (e1, e2) -> + let op = match exp.it with + | AddE _ -> "+" | SubE _ -> "-" + | MulE _ -> "*" | DivE _ -> "/" | ModE _ -> "%" + | EqCmpE _ -> "==" | NeCmpE _ -> "!=" + | GtCmpE _ -> ">" | GeCmpE _ -> ">=" + | LtCmpE _ -> "<" | LeCmpE _ -> "<=" + | Implies _ -> "==>" | OrE _ -> "||" | AndE _ -> "&&" + | _ -> failwith "not a binary operator" in + fprintf ppf "(%a %s %a)" pp_exp e1 op pp_exp e2 + | PermE p -> pp_perm ppf p + | AccE (fldacc, perm) -> fprintf ppf "@[acc(%a,%a)@]" pp_fldacc fldacc pp_exp perm + | _ -> fprintf ppf "@[// pretty printer not implemented for node at %s@]" (string_of_region exp.at) + +and pp_perm ppf perm = + match perm.it with + | NoP -> fprintf ppf "none" + | FullP -> fprintf ppf "write" + | WildcardP -> fprintf ppf "wildcard" + | FractionalP (a, b) -> fprintf ppf "@[(%a/%a)@]" pp_exp a pp_exp b + +and pp_stmt ppf stmt = + marks := stmt.at :: !marks; + fprintf ppf "\017%a\019" + pp_stmt' stmt.it + +and pp_stmt' ppf = function + | SeqnS seqn -> pp_seqn ppf seqn + | IfS (exp1, s1, { it = ([],[]); _ }) -> + fprintf ppf "@[if (%a)@ %a@]" + pp_exp exp1 + pp_seqn s1 + | IfS (exp1, s1, s2) -> + fprintf ppf "@[if (%a)@ %aelse@ %a@]" + pp_exp exp1 + pp_seqn s1 + pp_seqn s2 + | WhileS (exp, _, s) -> (* TODO: Invariant *) + fprintf ppf "@[while (%a) {@ %a}@]" + pp_exp exp + pp_seqn s + | VarAssignS (id, exp) -> + fprintf ppf "@[%s := %a@]" + id.it + pp_exp exp + | FieldAssignS (fldacc, exp) -> + fprintf ppf "@[%a := %a@]" + pp_fldacc fldacc + pp_exp exp + | InhaleS exp -> + fprintf ppf "@[inhale %a@]" + pp_exp exp + | ExhaleS exp -> + fprintf ppf "@[exhale %a@]" + pp_exp exp + | AssumeS exp -> + fprintf ppf "@[assume %a@]" + pp_exp exp + | AssertS exp -> + fprintf ppf "@[assert %a@]" + pp_exp exp + | PreconditionS exp -> + fprintf ppf "@[/*requires %a*/@]" + pp_exp exp + | PostconditionS exp -> + fprintf ppf "@[/*ensures %a*/@]" + pp_exp exp + | ConcurrencyS (max, exp, _) -> + fprintf ppf "@[/*concurrency max %s, cond: s %a*/@]" + max + pp_exp exp + | MethodCallS (_, _, _) + | LabelS (_, _) -> failwith "MethodCallS or LabelS?" + +and pp_fldacc ppf fldacc = + match fldacc with + | (exp1, id) -> + fprintf ppf "@[(%a).%s@]" pp_exp exp1 id.it + +let prog_mapped file p = + marks := []; + let b = Buffer.create 16 in + let ppf = Format.formatter_of_buffer b in + Format.fprintf ppf "@[%a@]" pp_prog p; + Format.pp_print_flush ppf (); + let in_file { left; right } = + let left, right = { left with file }, { right with file } in + { left ; right } in + let marks = ref (List.rev_map (fun loc -> loc, in_file loc) !marks, [], []) in + let pos = ref 0 in + let push line column = match !marks with + | (mot, vip) :: clos, ope, don -> marks := clos, (mot, { vip with left = { vip.left with line; column } }) :: ope, don + | _ -> assert false in + let pop line column = match !marks with + | clos, (mot, vip) :: ope, don -> marks := clos, ope, (mot, { vip with right = { vip.right with line; column } }) :: don + | _ -> assert false in + let line = ref 1 in + let examine = function + | '\n' -> line := !line + 1; pos := 0; '\n'; + | '\017' -> push !line !pos; '\017' + | '\019' -> pop !line !pos; '\017' + | a -> pos := !pos + 1; a in + let clean = function + | '\017' -> false + | _ -> true in + let b = Buffer.(of_seq Seq.(filter clean (map examine (to_seq b)))) in + let _, _, mapping = !marks in + let inside { left; right } other = + left.file = other.left.file && + right.file = other.right.file && + (other.left.line, other.left.column) <= (left.line, left.column) && + (right.line, right.column) <= (other.right.line, other.right.column) in + let lookup (r : Source.region) = + let tighten prev (mot, vip) = + if inside r vip + then Some mot + else prev in + List.fold_left tighten None mapping in + Buffer.contents b, lookup + +let prog p = fst (prog_mapped "" p) diff --git a/src/viper/syntax.ml b/src/viper/syntax.ml new file mode 100644 index 00000000000..334b61dcde9 --- /dev/null +++ b/src/viper/syntax.ml @@ -0,0 +1,91 @@ +type info = NoInfo + +type id = (string, info) Source.annotated_phrase + +type prog = (item list, info) Source.annotated_phrase + +and item = (item', info) Source.annotated_phrase +and item' = + (* | import path *) + | FieldI of id * typ + | MethodI of id * par list * par list * exp list * exp list * seqn option + | InvariantI of string * exp + +and par = id * typ + +and seqn = (decl list * stmt list, info) Source.annotated_phrase + +and decl = (id * typ, info) Source.annotated_phrase + +and exp = (exp', info) Source.annotated_phrase + +and exp' = + | LocalVar of id * typ + | Result of typ + | BoolLitE of bool + | NullLitE + | IntLitE of Mo_values.Numerics.Int.t + | AddE of exp * exp + | SubE of exp * exp + | MulE of exp * exp + | DivE of exp * exp + | ModE of exp * exp + | LtCmpE of exp * exp + | LeCmpE of exp * exp + | GtCmpE of exp * exp + | GeCmpE of exp * exp + | EqCmpE of exp * exp + | NeCmpE of exp * exp + | MinusE of exp + | NotE of exp + | AndE of exp * exp + | OrE of exp * exp + | Implies of exp * exp + | FldAcc of fldacc + | PermE of perm (* perm_amount *) + | AccE of fldacc * exp (* acc((rcvr: exp).field, (exp: perm_amount)) *) + | MacroCall of string * exp + +and perm = (perm', info) Source.annotated_phrase + +and perm' = + | NoP (* 0 / 1 *) + | FullP (* 1 / 1 *) + | WildcardP (* 1 / N for some N *) + | FractionalP of exp * exp (* (a: exp) / (b: exp) *) + +and invariants = exp list + +and stmt = (stmt', info) Source.annotated_phrase + +and tmpl = (tmpl', info) Source.annotated_phrase +and tmpl' = (Mo_def.Syntax.exp -> exp) -> exp + +and fldacc = exp * id + +and stmt' = + | MethodCallS of id * exp list * id list + | ExhaleS of exp + | InhaleS of exp + | AssertS of exp + | AssumeS of exp + | SeqnS of seqn + | VarAssignS of id * exp + | FieldAssignS of fldacc * exp + | IfS of exp * seqn * seqn + | WhileS of exp * invariants * seqn + | LabelS of id * invariants + (* TODO: these are temporary helper terms that should not appear in the final translation + we should avoid introducing them in the first place if possible, so they can be removed *) + | PreconditionS of exp + | PostconditionS of exp + | ConcurrencyS of string * exp * tmpl + + +and typ = (typ', info) Source.annotated_phrase + +and typ' = + | IntT + | BoolT + | RefT + diff --git a/src/viper/trans.ml b/src/viper/trans.ml new file mode 100644 index 00000000000..4cdd44839a2 --- /dev/null +++ b/src/viper/trans.ml @@ -0,0 +1,458 @@ +open Source + +open Syntax + +module T = Mo_types.Type +module M = Mo_def.Syntax +module Arrange = Mo_def.Arrange + +module Stamps = Env.Make(String) + +(* symbol generation *) + +let stamps : int Stamps.t ref = ref Stamps.empty + +let reset_stamps () = stamps := Stamps.empty + +let fresh_stamp name = + let n = Lib.Option.get (Stamps.find_opt name !stamps) 0 in + stamps := Stamps.add name (n + 1) !stamps; + n + +let fresh_id name = + let n = fresh_stamp name in + if n = 0 then + name + else Printf.sprintf "%s_%i" name (fresh_stamp name) + +(* helpers for constructing annotated syntax *) + +let (!!!) at it = { it; at; note = NoInfo} + +let intLitE at i = + !!! at (IntLitE (Mo_values.Numerics.Int.of_int i)) + +let accE at fldacc = + !!! at + (AccE( + fldacc, + !!! at (PermE (!!! at FullP)))) + +let conjoin es at = + match es with + | [] -> !!! at (BoolLitE true) + | e0::es0 -> + List.fold_left + (fun e1 -> fun e2 -> + !!! at (AndE(e1, e2))) + e0 + es0 + +let rec adjoin ctxt e = function + | [] -> e + | f :: fs -> f ctxt (adjoin ctxt e fs) + + +(* exception for reporting unsupported Motoko syntax *) +exception Unsupported of Source.region * string + +let unsupported at sexp = + raise (Unsupported (at, (Wasm.Sexpr.to_string 80 sexp))) + +type sort = Field | Local | Method + +module Env = T.Env + +type ctxt = + { self : string option; + ids : sort T.Env.t; + ghost_items : (ctxt -> item) list ref; + ghost_inits : (ctxt -> stmt) list ref; + ghost_perms : (ctxt -> Source.region -> exp) list ref; + ghost_conc : (ctxt -> exp -> exp) list ref; + } + +let self ctxt at = + match ctxt.self with + | Some id -> !!! at (LocalVar (!!! at id,!!! at RefT)) + | _ -> failwith "no self" + +let rec extract_invariants : item list -> (par -> invariants -> invariants) = function + | [] -> fun _ x -> x + | { it = InvariantI (s, e); at; _ } :: p -> + fun self es -> + !!! at (MacroCall(s, !!! at (LocalVar (fst self, snd self)))) + :: extract_invariants p self es + | _ :: p -> extract_invariants p + +let rec extract_concurrency (seq : seqn) : stmt' list * seqn = + let open List in + let extr (concs, stmts) s : stmt' list * stmt list = + match s.it with + | ConcurrencyS _ -> s.it :: concs, stmts + | SeqnS seq -> + let concs', seq = extract_concurrency seq in + rev_append concs' concs, { s with it = SeqnS seq } :: stmts + | WhileS (e, inv, seq) -> + let concs', seq = extract_concurrency seq in + rev_append concs' concs, { s with it = WhileS (e, inv, seq) } :: stmts + | IfS (e, the, els) -> + let the_concs, the = extract_concurrency the in + let els_concs, els = extract_concurrency els in + rev_append els_concs (rev_append the_concs concs), { s with it = IfS (e, the, els) } :: stmts + | _ -> concs, s :: stmts in + + let stmts = snd seq.it in + let conc, stmts = List.fold_left extr ([], []) stmts in + rev conc, { seq with it = fst seq.it, rev stmts } + +let rec unit (u : M.comp_unit) : prog Diag.result = + Diag.( + reset_stamps(); + try return (unit' u) with + | Unsupported (at, desc) -> error at "0" "viper" ("translation to viper failed:\n"^desc) + | _ -> error u.it.M.body.at "1" "viper" "translation to viper failed" + ) + +and unit' (u : M.comp_unit) : prog = + let { M.imports; M.body } = u.it in + match body.it with + | M.ActorU(id_opt, decs) -> + let ctxt = { self = None; ids = Env.empty; ghost_items = ref []; ghost_inits = ref []; ghost_perms = ref []; ghost_conc = ref [] } in + let ctxt', inits, mk_is = dec_fields ctxt decs in + let is' = List.map (fun mk_i -> mk_i ctxt') mk_is in + (* given is', compute ghost_is *) + let ghost_is = List.map (fun mk_i -> mk_i ctxt') !(ctxt.ghost_items) in + let init_id = !!! (Source.no_region) "__init__" in + let self_id = !!! (Source.no_region) "$Self" in + let self_typ = !!! (self_id.at) RefT in + let ctxt'' = { ctxt' with self = Some self_id.it } in + let perms = List.map (fun (id, _) -> fun (at : region) -> + (accE at (self ctxt'' at, id))) inits in + let ghost_perms = List.map (fun mk_p -> mk_p ctxt'') !(ctxt.ghost_perms) in + let perm = + fun (at : region) -> + List.fold_left + (fun pexp -> fun p_fn -> + !!! at (AndE(pexp, p_fn at))) + (!!! at (BoolLitE true)) + (perms @ ghost_perms) + in + (* Add initializer *) + let init_list = List.map (fun (id, init) -> + !!! { left = id.at.left; right = init.at.right } + (FieldAssignS((self ctxt'' init.at, id), exp ctxt'' init))) + inits in + let init_list = init_list @ List.map (fun mk_s -> mk_s ctxt'') !(ctxt.ghost_inits) in + let init_body = + !!! (body.at) ([], init_list)(* ATG: Is this the correct position? *) + in + let init_m = + !!! (body.at) (MethodI(init_id, [self_id, self_typ], [], [], [], Some init_body)) + in + let is'' = init_m :: is' in + (* Add permissions *) + let is''' = List.map (fun {it; at; note: info} -> ( + match it with + | MethodI (id, ins, outs, pres, posts, body) -> + !!! at + (MethodI (id, ins, outs, + !!! at (MacroCall("$Perm", self ctxt'' at))::pres, + !!! at (MacroCall("$Perm", self ctxt'' at))::posts, + body)) + | _ -> {it; at; note})) is'' in + (* Add functional invariants *) + let invs = extract_invariants is''' (self_id, self_typ) [] in + let is4 = List.map (fun {it; at; note: info} -> + match it with + | MethodI (id, ins, outs, pres, posts, body) -> + !!! at + (MethodI(id, ins, outs, + (if id.it = init_id.it + then pres + else pres @ [!!! at (MacroCall("$Inv", self ctxt'' at))]), + posts @ [!!! at (MacroCall("$Inv", self ctxt'' at))], + body)) + | _ -> {it; at; note}) is''' in + let perm_def = !!! (body.at) (InvariantI("$Perm", perm body.at)) in + let inv_def = !!! (body.at) (InvariantI("$Inv", adjoin ctxt'' (conjoin invs body.at) !(ctxt.ghost_conc))) in + let is = ghost_is @ (perm_def :: inv_def :: is4) in + !!! (body.at) is + | _ -> assert false + +and dec_fields (ctxt : ctxt) (ds : M.dec_field list) = + match ds with + | [] -> + (ctxt, [], []) + | d :: ds -> + let ctxt, init, mk_i = dec_field ctxt d in + let ctxt, inits, mk_is = dec_fields ctxt ds in + (ctxt, (match init with Some i -> i::inits | _ -> inits), mk_i::mk_is) + +and dec_field ctxt d = + let ctxt, init, mk_i = dec_field' ctxt d.it in + (ctxt, + init, + fun ctxt' -> + let (i, info) = mk_i ctxt' in + !!! (d.at) i) + +and dec_field' ctxt d = + match d.M.dec.it with + | M.VarD (x, e) -> + { ctxt with ids = Env.add x.it Field ctxt.ids }, + Some (id x, e), + fun ctxt' -> + (FieldI(id x, tr_typ e.note.M.note_typ), + NoInfo) + | M.(LetD ({it=VarP f;_}, + {it=FuncE(x, sp, tp, p, t_opt, sugar, + {it = AsyncE (_, e); _} );_})) -> (* ignore async *) + { ctxt with ids = Env.add f.it Method ctxt.ids }, + None, + fun ctxt' -> + let open Either in + let self_id = !!! (Source.no_region) "$Self" in + let ctxt'' = { ctxt' with self = Some self_id.it } + in (* TODO: add args (and rets?) *) + let stmts = stmt ctxt'' e in + let _, stmts = extract_concurrency stmts in + let pres, stmts' = List.partition_map (function { it = PreconditionS exp; _ } -> Left exp | s -> Right s) (snd stmts.it) in + let posts, stmts' = List.partition_map (function { it = PostconditionS exp; _ } -> Left exp | s -> Right s) stmts' in + (MethodI(id f, (self_id, !!! Source.no_region RefT)::args p, rets t_opt, pres, posts, Some { stmts with it = fst stmts.it, stmts' } ), + NoInfo) + | M.(ExpD { it = AssertE (Invariant, e); at; _ }) -> + ctxt, + None, + fun ctxt' -> + (InvariantI (Printf.sprintf "invariant_%d" at.left.line, exp { ctxt' with self = Some "$Self" } e), NoInfo) + | _ -> + unsupported d.M.dec.at (Arrange.dec d.M.dec) + +and args p = match p.it with + | M.TupP ps -> + List.map + (fun p -> + match p.it with + | M.VarP x -> + (id x, tr_typ p.note) + | _ -> unsupported p.at (Arrange.pat p)) + ps + | _ -> unsupported p.at (Arrange.pat p) + +and block ctxt at ds = + let ctxt, mk_ss = decs ctxt ds in + !!! at (mk_ss ctxt) + +and decs ctxt ds = + match ds with + | [] -> (ctxt, fun ctxt' -> ([],[])) + | d::ds' -> + let (ctxt1, mk_s) = dec ctxt d in + let (ctxt2, mk_ss) = decs ctxt1 ds' in + (ctxt2, + fun ctxt' -> + let (l, s) = mk_s ctxt' in + let (ls, ss) = mk_ss ctxt' in + (l @ ls, s @ ss)) + +and dec ctxt d = + let (!!) p = !!! (d.at) p in + match d.it with + | M.VarD (x, e) -> + (* TODO: translate e? *) + { ctxt with ids = Env.add x.it Local ctxt.ids }, + fun ctxt' -> + ([ !!(id x, tr_typ e.note.M.note_typ) ], + [ !!(VarAssignS (id x, exp ctxt' e)) ]) + | M.(LetD ({it=VarP x;_}, e)) -> + { ctxt with ids = Env.add x.it Local ctxt.ids }, + fun ctxt' -> + ([ !!(id x, tr_typ e.note.M.note_typ) ], + [ !!(VarAssignS (id x, exp ctxt' e)) ]) + | M.(ExpD e) -> (* TODO: restrict to e of unit type? *) + (ctxt, + fun ctxt' -> + let s = stmt ctxt' e in + s.it) + | _ -> + unsupported d.at (Arrange.dec d) + +and stmt ctxt (s : M.exp) : seqn = + let (!!) p = !!! (s.at) p in + match s.it with + | M.TupE [] -> + block ctxt s.at [] + | M.BlockE ds -> + block ctxt s.at ds + | M.IfE(e, s1, s2) -> + !!([], + [ !!(IfS(exp ctxt e, stmt ctxt s1, stmt ctxt s2))]) + | M.(AwaitE({ it = AsyncE (_, e); at; _ })) -> (* gross hack *) + let id = fresh_id "$message_async" in + let (!!) p = !!! (s.at) p in + let (!@) p = !!! at p in + ctxt.ghost_items := + (fun ctxt -> + !!(FieldI (!!id, !!IntT))) :: + !(ctxt.ghost_items); + let mk_s = fun ctxt -> + !!! at + (FieldAssignS ( + (self ctxt s.at, !!id), + intLitE (s.at) 0)) + in + ctxt.ghost_inits := mk_s :: !(ctxt.ghost_inits); + let mk_p = fun ctxt at -> + accE at (self ctxt at, !!! at id) + in + ctxt.ghost_perms := mk_p :: !(ctxt.ghost_perms); + let stmts = stmt ctxt e in + (* assume that each `async {...}` has an assertion *) + let conc, _ = extract_concurrency stmts in + let mk_c = match conc with + | [] -> + fun _ x -> x + | ConcurrencyS ("1", _, cond) :: _ -> + let (!?) p = !!! (cond.at) p in + let zero, one = intLitE Source.no_region 0, intLitE Source.no_region 1 in + fun ctxt x -> + let ghost_fld () = !?(FldAcc (self ctxt cond.at, !?id)) in + let between = !?(AndE (!?(LeCmpE (zero, ghost_fld ())), !?(LeCmpE (ghost_fld (), one)))) in + let is_one = !?(EqCmpE (ghost_fld (), one)) in + !?(AndE (x, !?(AndE (between, !?(Implies (is_one, cond.it (exp ctxt))))))) + | _ -> unsupported e.at (Arrange.exp e) in + ctxt.ghost_conc := mk_c :: !(ctxt.ghost_conc); + !!([], + [ !!(FieldAssignS( + (self ctxt Source.no_region, !!id), + (!!(AddE(!!(FldAcc (self ctxt (s.at), !!id)), + intLitE Source.no_region 1))))); + !@(ExhaleS (!@(AndE(!@(MacroCall("$Perm", self ctxt at)), + !@(MacroCall("$Inv", self ctxt at)))))); + !@(SeqnS ( + !@([], + [ + !@(InhaleS (!@(AndE(!@(MacroCall("$Perm", self ctxt at)), + !@(AndE(!@(MacroCall("$Inv", self ctxt at)), + !@(GtCmpE(!@(FldAcc (self ctxt at, !@id)), + intLitE Source.no_region 0)))))))); + !@(FieldAssignS( + (self ctxt at, !@id), + (!@(SubE(!@(FldAcc (self ctxt at, !@id)), + intLitE at 1))))); + !!! (e.at) (SeqnS stmts); + !@(ExhaleS (!@(AndE(!@(MacroCall("$Perm", self ctxt at)), + !@(MacroCall("$Inv", self ctxt at)))))) ]))); + !!(InhaleS (!!(AndE(!!(MacroCall("$Perm", self ctxt at)), + !!(MacroCall("$Inv", self ctxt at)))))); + ]) + | M.WhileE(e, s1) -> + !!([], + [ !!(WhileS(exp ctxt e, [], stmt ctxt s1)) ]) (* TODO: Invariant *) + | M.(AssignE({it = VarE x; _}, e2)) -> + begin match Env.find x.it ctxt.ids with + | Local -> + let loc = !!! (x.at) (x.it) in + !!([], + [ !!(VarAssignS(loc, exp ctxt e2)) ]) + | Field -> + let fld = (self ctxt x.at, id x) in + !!([], + [ !!(FieldAssignS(fld, exp ctxt e2)) ]) + | _ -> + unsupported s.at (Arrange.exp s) + end + | M.AssertE (M.Precondition, e) -> + !!( [], + [ !!(PreconditionS (exp ctxt e)) ]) + | M.AssertE (M.Postcondition, e) -> + !!([], + [ !!(PostconditionS (exp ctxt e)) ]) + | M.AssertE (M.Concurrency n, e) -> + !!([], + [ !!(ConcurrencyS (n, exp ctxt e, !! ((|>) e))) ]) + | M.AssertE (M.Static, e) -> + !!([], + [ !!(AssertS (exp ctxt e)) ]) + | M.AssertE (M.Runtime, e) -> + !!([], + [ !!(AssumeS (exp ctxt e)) ]) + | _ -> + unsupported s.at (Arrange.exp s) + +and exp ctxt e = + let open Mo_values.Operator in + let (!!) p = !!! (e.at) p in + match e.it with + | M.VarE x -> + begin + match Env.find x.it ctxt.ids with + | Local -> + !!(LocalVar (id x, tr_typ e.note.M.note_typ)) + | Field -> + !!(FldAcc (self ctxt x.at, id x)) + | _ -> + unsupported e.at (Arrange.exp e) + end + | M.AnnotE(a, b) -> + exp ctxt a + | M.LitE r -> + begin match !r with + | M.BoolLit b -> + !!(BoolLitE b) + | M.IntLit i -> + !!(IntLitE i) + | _ -> + unsupported e.at (Arrange.exp e) + end + | M.NotE e -> + !!(NotE (exp ctxt e)) + | M.RelE (ot, e1, op, e2) -> + let e1, e2 = exp ctxt e1, exp ctxt e2 in + !!(match op with + | EqOp -> EqCmpE (e1, e2) + | NeqOp -> NeCmpE (e1, e2) + | GtOp -> GtCmpE (e1, e2) + | GeOp -> GeCmpE (e1, e2) + | LtOp -> LtCmpE (e1, e2) + | LeOp -> LeCmpE (e1, e2)) + | M.BinE (ot, e1, op, e2) -> + let e1, e2 = exp ctxt e1, exp ctxt e2 in + !!(match op with + | AddOp -> AddE (e1, e2) + | SubOp -> SubE (e1, e2) + | MulOp -> MulE (e1, e2) + | DivOp -> DivE (e1, e2) + | ModOp -> ModE (e1, e2) + | _ -> unsupported e.at (Arrange.exp e)) + | M.OrE (e1, e2) -> + !!(OrE (exp ctxt e1, exp ctxt e2)) + | M.AndE (e1, e2) -> + !!(AndE (exp ctxt e1, exp ctxt e2)) + | M.ImpliesE (e1, e2) -> + !!(Implies (exp ctxt e1, exp ctxt e2)) + | _ -> + unsupported e.at (Arrange.exp e) + +and rets t_opt = + match t_opt with + | None -> [] + | Some t -> + (match T.normalize t.note with + | T.Tup [] -> [] + | T.Async (_, _) -> [] + | _ -> unsupported t.at (Arrange.typ t) + ) + +and id id = { it = id.it; at = id.at; note = NoInfo } + +and tr_typ typ = + { it = tr_typ' typ; + at = Source.no_region; + note = NoInfo } +and tr_typ' typ = + match T.normalize typ with + | T.Prim T.Int -> IntT + | T.Prim T.Bool -> BoolT + | _ -> unsupported Source.no_region (Mo_types.Arrange_type.typ (T.normalize typ)) diff --git a/test/fail/ok/syntax2.tc.ok b/test/fail/ok/syntax2.tc.ok index 5b9912ffea4..eb3081e794b 100644 --- a/test/fail/ok/syntax2.tc.ok +++ b/test/fail/ok/syntax2.tc.ok @@ -7,6 +7,7 @@ syntax2.mo:2.1-2.4: syntax error [M0001], unexpected token 'let', expected one o ; seplist(,) or + implies . : diff --git a/test/fail/ok/syntax3.tc.ok b/test/fail/ok/syntax3.tc.ok index 70e7c6fb8d9..028eebd7729 100644 --- a/test/fail/ok/syntax3.tc.ok +++ b/test/fail/ok/syntax3.tc.ok @@ -6,6 +6,7 @@ syntax3.mo:1.3-1.4: syntax error [M0001], unexpected token ';', expected one of or + implies . , seplist(,,) diff --git a/test/fail/ok/syntax5.tc.ok b/test/fail/ok/syntax5.tc.ok index 62e5fef4e4d..95550080467 100644 --- a/test/fail/ok/syntax5.tc.ok +++ b/test/fail/ok/syntax5.tc.ok @@ -6,6 +6,7 @@ syntax5.mo:3.1: syntax error [M0001], unexpected end of input, expected one of t or + implies . , seplist(,,) diff --git a/test/fail/ok/verification-asserts.tc.ok b/test/fail/ok/verification-asserts.tc.ok new file mode 100644 index 00000000000..49ea928a86e --- /dev/null +++ b/test/fail/ok/verification-asserts.tc.ok @@ -0,0 +1,10 @@ +verification-asserts.mo:1.1-1.19: verification syntax error [M0181], verification assertions not permitted in normal mode +verification-asserts.mo:2.1-2.20: verification syntax error [M0181], verification assertions not permitted in normal mode +verification-asserts.mo:3.1-3.17: verification syntax error [M0181], verification assertions not permitted in normal mode +verification-asserts.mo:4.1-4.19: verification syntax error [M0181], verification assertions not permitted in normal mode +verification-asserts.mo:7.8-7.17: syntax error [M0001], unexpected token 'invariant', expected one of token or sequence: + system + return + invariant + func + : async diff --git a/test/fail/ok/verification-asserts.tc.ret.ok b/test/fail/ok/verification-asserts.tc.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/fail/ok/verification-asserts.tc.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/fail/ok/verification-implies.tc.ok b/test/fail/ok/verification-implies.tc.ok new file mode 100644 index 00000000000..c28341b61ad --- /dev/null +++ b/test/fail/ok/verification-implies.tc.ok @@ -0,0 +1,4 @@ +verification-implies.mo:2.1-2.5: type error [M0097], expected function type, but expression produces type + Bool +verification-implies.mo:2.5-2.6: info, this looks like an unintended function call, perhaps a missing ';'? +verification-implies.mo:2.6-2.13: type error [M0057], unbound variable implies diff --git a/test/fail/ok/verification-implies.tc.ret.ok b/test/fail/ok/verification-implies.tc.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/fail/ok/verification-implies.tc.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/fail/verification-asserts.mo b/test/fail/verification-asserts.mo new file mode 100644 index 00000000000..6be7d479170 --- /dev/null +++ b/test/fail/verification-asserts.mo @@ -0,0 +1,7 @@ +assert:system true; +assert:1:async true; +assert:func true; +assert:return true; + +// `invariant` is a keyword in verification mode only +assert:invariant true; diff --git a/test/fail/verification-implies.mo b/test/fail/verification-implies.mo new file mode 100644 index 00000000000..51652748434 --- /dev/null +++ b/test/fail/verification-implies.mo @@ -0,0 +1,2 @@ +// `implies` is a keyword in verification mode only +true implies true; diff --git a/test/repl/ok/viper.stdout.ok b/test/repl/ok/viper.stdout.ok new file mode 100644 index 00000000000..7a1aaf1d945 --- /dev/null +++ b/test/repl/ok/viper.stdout.ok @@ -0,0 +1,43 @@ +field $message_async: Int +define $Perm($Self) ((((true && acc(($Self).claimed,write)) && acc(($Self).count,write)) && + acc(($Self).$message_async,write))) +define $Inv($Self) (((invariant_7($Self) && invariant_8($Self)) && (((0 <= + ($Self).$message_async) && (($Self).$message_async <= 1)) && ((($Self).$message_async == 1) ==> ( + ($Self).claimed && (($Self).count == 0)))))) +method __init__($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + ($Self).claimed := false + ($Self).count := 0 + ($Self).$message_async := 0 + } +field claimed: Bool +field count: Int +define invariant_7($Self) (((($Self).count == 0) || (($Self).count == 1))) +define invariant_8($Self) (((!($Self).claimed) ==> (($Self).count == 0))) +method claim($Self: Ref) + + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + if ((!($Self).claimed)) + { + ($Self).claimed := true + ($Self).$message_async := (($Self).$message_async + 1) + exhale ($Perm($Self) && $Inv($Self)) + { + inhale ($Perm($Self) && ($Inv($Self) && (($Self).$message_async > 0))) + ($Self).$message_async := (($Self).$message_async - 1) + { + ($Self).count := (($Self).count + 1) + } + exhale ($Perm($Self) && $Inv($Self)) + } + inhale ($Perm($Self) && $Inv($Self)) + } + } diff --git a/test/repl/viper.sh b/test/repl/viper.sh new file mode 100755 index 00000000000..7b2c11c9213 --- /dev/null +++ b/test/repl/viper.sh @@ -0,0 +1,27 @@ +#!/usr/bin/env bash + +# Tests that `moc` can output Viper code +(cat <<__END__ +actor { + + var claimed = false; + + var count = 0 : Int; + + assert:invariant count == 0 or count == 1; + assert:invariant not claimed implies count == 0; + + public shared func claim() : async () { + if (not claimed) { + claimed := true; + + await async { + assert:1:async (claimed and count == 0); + count += 1; + }; + }; + }; + +} +__END__ +) | moc --viper /dev/stdin diff --git a/test/run.sh b/test/run.sh index 7035aa7b453..19c36265d53 100755 --- a/test/run.sh +++ b/test/run.sh @@ -13,6 +13,7 @@ # -i: Only check mo to idl generation # -p: Produce perf statistics # only compiles and runs drun, writes stats to $PERF_OUT +# -v: Translate to Viper # function realpath() { @@ -24,6 +25,7 @@ ACCEPT=no DTESTS=no IDL=no PERF=no +VIPER=no WASMTIME_OPTIONS="--disable-cache" WRAP_drun=$(realpath $(dirname $0)/drun-wrapper.sh) WRAP_ic_ref_run=$(realpath $(dirname $0)/ic-ref-run-wrapper.sh) @@ -35,7 +37,7 @@ ECHO=echo # Always do GC in tests, unless it's disabled in `EXTRA_MOC_ARGS` EXTRA_MOC_ARGS="--force-gc $EXTRA_MOC_ARGS" -while getopts "adpstir" o; do +while getopts "adpstirv" o; do case "${o}" in a) ACCEPT=yes @@ -55,6 +57,9 @@ while getopts "adpstir" o; do i) IDL=yes ;; + v) + VIPER=yes + ;; esac done @@ -93,7 +98,9 @@ function normalize () { # Normalize instruction locations on traps, added by ic-ref ad6ea9e sed -e 's/region:0x[0-9a-fA-F]\+-0x[0-9a-fA-F]\+/region:0xXXX-0xXXX/g' | # Delete everything after Oom - sed -e '/RTS error: Cannot grow memory/q' \ + sed -e '/RTS error: Cannot grow memory/q' | + # Delete Viper meta-output + sed -e '/^Silicon /d' \ > $1.norm mv $1.norm $1 fi @@ -264,6 +271,20 @@ do then run didc didc --check $out/$base.did fi + elif [ $VIPER = 'yes' ] + then + run vpr $moc_with_flags --viper $base.mo -o $out/$base.vpr + vpr_succeeded=$? + + normalize $out/$base.vpr + diff_files="$diff_files $base.vpr" + + if [ "$vpr_succeeded" -eq 0 ] + then + run silicon java -Xmx2048m -Xss16m -cp $VIPER_SERVER \ + viper.silicon.SiliconRunner --logLevel OFF --z3Exe $(which z3) \ + $out/$base.vpr + fi else if [ "$SKIP_RUNNING" != yes -a "$PERF" != yes ] then diff --git a/test/viper/Makefile b/test/viper/Makefile new file mode 100644 index 00000000000..9a04148d1e1 --- /dev/null +++ b/test/viper/Makefile @@ -0,0 +1,13 @@ +RUNFLAGS = -v +export MOC_UNLOCK_VERIFICATION = viper + +all: + ../run.sh $(RUNFLAGS) *.mo + +accept: + ../run.sh $(RUNFLAGS) -a *.mo + +clean: + rm -rf _out + +include ../*.mk diff --git a/test/viper/assertions.mo b/test/viper/assertions.mo new file mode 100644 index 00000000000..7ad5c4a28e8 --- /dev/null +++ b/test/viper/assertions.mo @@ -0,0 +1,26 @@ +// @verify + +// This example should demonstrate all static assertions that are currently +// supported. + +actor { + + var u = false; + var v = 0 : Int; + + assert:invariant u; // canister invariant + + public shared func claim() : async () { + assert:func v >= 0; // function precondition + + assert:system u implies v > 0; // static assertion + assert u implies v > 0; // dynamic assertion + + await async { + assert:1:async true; // concurrency constraints + }; + + assert:return v >= 0; // function postcondition + }; + +} diff --git a/test/viper/async.mo b/test/viper/async.mo new file mode 100644 index 00000000000..c3f18d7d643 --- /dev/null +++ b/test/viper/async.mo @@ -0,0 +1,29 @@ +// @verify + +actor { + + var flag = false; + + public shared func claim() : async () { + flag := true; + flag := false; + await async { + assert:1:async not flag; + flag := true; + flag := false; + flag := flag + }; + if flag { + await async { + assert:1:async flag; + flag := false + } + } else { + await async { + assert:1:async flag; + flag := false + } + } + } + +} diff --git a/test/viper/claim-broken.mo b/test/viper/claim-broken.mo new file mode 100644 index 00000000000..7074a4fc32e --- /dev/null +++ b/test/viper/claim-broken.mo @@ -0,0 +1,22 @@ +// @verify + +actor { + + var claimed = false; + + var count = 0 : Int; + + assert:invariant not claimed implies count == 0; + assert:invariant count == 0 or count == 1; + + public shared func claim() : async () { + if (not claimed) { + await async { + assert:1:async (claimed and count == 0); + claimed := true; + count += 1; + }; + }; + }; + +} diff --git a/test/viper/claim-simple.mo b/test/viper/claim-simple.mo new file mode 100644 index 00000000000..d36c7f09ffb --- /dev/null +++ b/test/viper/claim-simple.mo @@ -0,0 +1,16 @@ +// @verify + +actor { + + var claimed = false; + + var count = 0 : Int; + + public shared func claim() : async () { + if (not claimed) { + claimed := true; + count += 1; + }; + }; + +} diff --git a/test/viper/claim.mo b/test/viper/claim.mo new file mode 100644 index 00000000000..e3e08b52d6d --- /dev/null +++ b/test/viper/claim.mo @@ -0,0 +1,23 @@ +// @verify + +actor { + + var claimed = false; + + var count = 0 : Int; + + assert:invariant count == 0 or count == 1; + assert:invariant not claimed implies count == 0; + + public shared func claim() : async () { + if (not claimed) { + claimed := true; + + await async { + assert:1:async (claimed and count == 0); + count += 1; + }; + }; + }; + +} diff --git a/test/viper/invariant.mo b/test/viper/invariant.mo new file mode 100644 index 00000000000..37e1d946ff5 --- /dev/null +++ b/test/viper/invariant.mo @@ -0,0 +1,26 @@ +// @verify + +actor { + + var claimed = false; + + var count = 0 : Int; + + assert:invariant claimed and not (-1 == -1) and (-42 == -42) or true; + assert:invariant count > 0; + assert:invariant not claimed implies count == 0; + + public shared func claim() : async () { + assert:func count >= 0; + assert claimed implies count > 0; + assert:return count >= 0; + }; + + public shared func loops(/*j : Int*/) : async () { + var i : Int = 0; + while (i > 0) { + i += 1 + } + } + +} diff --git a/test/viper/ok/assertions.silicon.ok b/test/viper/ok/assertions.silicon.ok new file mode 100644 index 00000000000..202af03d0c2 --- /dev/null +++ b/test/viper/ok/assertions.silicon.ok @@ -0,0 +1,2 @@ + [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@10.13--10.24) + [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@28.15--28.44) diff --git a/test/viper/ok/assertions.silicon.ret.ok b/test/viper/ok/assertions.silicon.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/viper/ok/assertions.silicon.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/viper/ok/assertions.vpr.ok b/test/viper/ok/assertions.vpr.ok new file mode 100644 index 00000000000..c834272478d --- /dev/null +++ b/test/viper/ok/assertions.vpr.ok @@ -0,0 +1,41 @@ +field $message_async: Int +define $Perm($Self) ((((true && acc(($Self).u,write)) && acc(($Self).v,write)) && + acc(($Self).$message_async,write))) +define $Inv($Self) ((invariant_11($Self) && (((0 <= ($Self).$message_async) && ( + ($Self).$message_async <= 1)) && ((($Self).$message_async == 1) ==> true)))) +method __init__($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + ($Self).u := false + ($Self).v := 0 + ($Self).$message_async := 0 + } +field u: Bool +field v: Int +define invariant_11($Self) (($Self).u) +method claim($Self: Ref) + + requires $Perm($Self) + requires (($Self).v >= 0) + requires $Inv($Self) + ensures $Perm($Self) + ensures (($Self).v >= 0) + ensures $Inv($Self) + { + assert (($Self).u ==> (($Self).v > 0)) + assume (($Self).u ==> (($Self).v > 0)) + ($Self).$message_async := (($Self).$message_async + 1) + exhale ($Perm($Self) && $Inv($Self)) + { + inhale ($Perm($Self) && ($Inv($Self) && (($Self).$message_async > 0))) + ($Self).$message_async := (($Self).$message_async - 1) + { + + } + exhale ($Perm($Self) && $Inv($Self)) + } + inhale ($Perm($Self) && $Inv($Self)) + } diff --git a/test/viper/ok/async.silicon.ok b/test/viper/ok/async.silicon.ok new file mode 100644 index 00000000000..4cd9741c5a2 --- /dev/null +++ b/test/viper/ok/async.silicon.ok @@ -0,0 +1 @@ + [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@33.15--33.42) diff --git a/test/viper/ok/async.silicon.ret.ok b/test/viper/ok/async.silicon.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/viper/ok/async.silicon.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/viper/ok/async.vpr.ok b/test/viper/ok/async.vpr.ok new file mode 100644 index 00000000000..b0a40dca425 --- /dev/null +++ b/test/viper/ok/async.vpr.ok @@ -0,0 +1,72 @@ +field $message_async_4: Int +field $message_async_2: Int +field $message_async: Int +define $Perm($Self) (((((true && acc(($Self).flag,write)) && acc(($Self).$message_async_4,write)) && + acc(($Self).$message_async_2,write)) && acc(($Self).$message_async,write))) +define $Inv($Self) ((((true && (((0 <= ($Self).$message_async) && (($Self).$message_async <= 1)) && (( + ($Self).$message_async == 1) ==> (!($Self).flag)))) && (((0 <= ($Self).$message_async_2) && ( + ($Self).$message_async_2 <= 1)) && ((($Self).$message_async_2 == 1) ==> + ($Self).flag))) && (((0 <= ($Self).$message_async_4) && (($Self).$message_async_4 <= 1)) && (( + ($Self).$message_async_4 == 1) ==> ($Self).flag)))) +method __init__($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + ($Self).flag := false + ($Self).$message_async_4 := 0 + ($Self).$message_async_2 := 0 + ($Self).$message_async := 0 + } +field flag: Bool +method claim($Self: Ref) + + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + ($Self).flag := true + ($Self).flag := false + ($Self).$message_async := (($Self).$message_async + 1) + exhale ($Perm($Self) && $Inv($Self)) + { + inhale ($Perm($Self) && ($Inv($Self) && (($Self).$message_async > 0))) + ($Self).$message_async := (($Self).$message_async - 1) + { + ($Self).flag := true + ($Self).flag := false + ($Self).flag := ($Self).flag + } + exhale ($Perm($Self) && $Inv($Self)) + } + inhale ($Perm($Self) && $Inv($Self)) + if (($Self).flag) + { + ($Self).$message_async_4 := (($Self).$message_async_4 + 1) + exhale ($Perm($Self) && $Inv($Self)) + { + inhale ($Perm($Self) && ($Inv($Self) && (($Self).$message_async_4 > 0))) + ($Self).$message_async_4 := (($Self).$message_async_4 - 1) + { + ($Self).flag := false + } + exhale ($Perm($Self) && $Inv($Self)) + } + inhale ($Perm($Self) && $Inv($Self)) + }else + { + ($Self).$message_async_2 := (($Self).$message_async_2 + 1) + exhale ($Perm($Self) && $Inv($Self)) + { + inhale ($Perm($Self) && ($Inv($Self) && (($Self).$message_async_2 > 0))) + ($Self).$message_async_2 := (($Self).$message_async_2 - 1) + { + ($Self).flag := false + } + exhale ($Perm($Self) && $Inv($Self)) + } + inhale ($Perm($Self) && $Inv($Self)) + } + } diff --git a/test/viper/ok/claim-broken.silicon.ok b/test/viper/ok/claim-broken.silicon.ok new file mode 100644 index 00000000000..2738a3acfa7 --- /dev/null +++ b/test/viper/ok/claim-broken.silicon.ok @@ -0,0 +1 @@ + [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@31.20--31.47) diff --git a/test/viper/ok/claim-broken.silicon.ret.ok b/test/viper/ok/claim-broken.silicon.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/viper/ok/claim-broken.silicon.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/viper/ok/claim-broken.vpr.ok b/test/viper/ok/claim-broken.vpr.ok new file mode 100644 index 00000000000..f2061664183 --- /dev/null +++ b/test/viper/ok/claim-broken.vpr.ok @@ -0,0 +1,43 @@ +field $message_async: Int +define $Perm($Self) ((((true && acc(($Self).claimed,write)) && acc(($Self).count,write)) && + acc(($Self).$message_async,write))) +define $Inv($Self) (((invariant_9($Self) && invariant_10($Self)) && (((0 <= + ($Self).$message_async) && (($Self).$message_async <= 1)) && ((($Self).$message_async == 1) ==> ( + ($Self).claimed && (($Self).count == 0)))))) +method __init__($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + ($Self).claimed := false + ($Self).count := 0 + ($Self).$message_async := 0 + } +field claimed: Bool +field count: Int +define invariant_9($Self) (((!($Self).claimed) ==> (($Self).count == 0))) +define invariant_10($Self) (((($Self).count == 0) || (($Self).count == 1))) +method claim($Self: Ref) + + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + if ((!($Self).claimed)) + { + ($Self).$message_async := (($Self).$message_async + 1) + exhale ($Perm($Self) && $Inv($Self)) + { + inhale ($Perm($Self) && ($Inv($Self) && (($Self).$message_async > 0))) + ($Self).$message_async := (($Self).$message_async - 1) + { + ($Self).claimed := true + ($Self).count := (($Self).count + 1) + } + exhale ($Perm($Self) && $Inv($Self)) + } + inhale ($Perm($Self) && $Inv($Self)) + } + } diff --git a/test/viper/ok/claim-simple.silicon.ok b/test/viper/ok/claim-simple.silicon.ok new file mode 100644 index 00000000000..c704b94e8c8 --- /dev/null +++ b/test/viper/ok/claim-simple.silicon.ok @@ -0,0 +1 @@ +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (claim-simple.vpr@2.1) diff --git a/test/viper/ok/claim-simple.vpr.ok b/test/viper/ok/claim-simple.vpr.ok new file mode 100644 index 00000000000..50d2875b529 --- /dev/null +++ b/test/viper/ok/claim-simple.vpr.ok @@ -0,0 +1,26 @@ +define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write))) +define $Inv($Self) (true) +method __init__($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + ($Self).claimed := false + ($Self).count := 0 + } +field claimed: Bool +field count: Int +method claim($Self: Ref) + + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + if ((!($Self).claimed)) + { + ($Self).claimed := true + ($Self).count := (($Self).count + 1) + } + } diff --git a/test/viper/ok/claim.vpr.ok b/test/viper/ok/claim.vpr.ok new file mode 100644 index 00000000000..593ce616846 --- /dev/null +++ b/test/viper/ok/claim.vpr.ok @@ -0,0 +1,43 @@ +field $message_async: Int +define $Perm($Self) ((((true && acc(($Self).claimed,write)) && acc(($Self).count,write)) && + acc(($Self).$message_async,write))) +define $Inv($Self) (((invariant_9($Self) && invariant_10($Self)) && (((0 <= + ($Self).$message_async) && (($Self).$message_async <= 1)) && ((($Self).$message_async == 1) ==> ( + ($Self).claimed && (($Self).count == 0)))))) +method __init__($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + ($Self).claimed := false + ($Self).count := 0 + ($Self).$message_async := 0 + } +field claimed: Bool +field count: Int +define invariant_9($Self) (((($Self).count == 0) || (($Self).count == 1))) +define invariant_10($Self) (((!($Self).claimed) ==> (($Self).count == 0))) +method claim($Self: Ref) + + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + if ((!($Self).claimed)) + { + ($Self).claimed := true + ($Self).$message_async := (($Self).$message_async + 1) + exhale ($Perm($Self) && $Inv($Self)) + { + inhale ($Perm($Self) && ($Inv($Self) && (($Self).$message_async > 0))) + ($Self).$message_async := (($Self).$message_async - 1) + { + ($Self).count := (($Self).count + 1) + } + exhale ($Perm($Self) && $Inv($Self)) + } + inhale ($Perm($Self) && $Inv($Self)) + } + } diff --git a/test/viper/ok/invariant.silicon.ok b/test/viper/ok/invariant.silicon.ok new file mode 100644 index 00000000000..94a1ad16eff --- /dev/null +++ b/test/viper/ok/invariant.silicon.ok @@ -0,0 +1 @@ + [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@7.13--7.24) diff --git a/test/viper/ok/invariant.silicon.ret.ok b/test/viper/ok/invariant.silicon.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/viper/ok/invariant.silicon.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/viper/ok/invariant.vpr.ok b/test/viper/ok/invariant.vpr.ok new file mode 100644 index 00000000000..06b14fe0dea --- /dev/null +++ b/test/viper/ok/invariant.vpr.ok @@ -0,0 +1,40 @@ +define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write))) +define $Inv($Self) (((invariant_9($Self) && invariant_10($Self)) && invariant_11($Self))) +method __init__($Self: Ref) + + requires $Perm($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { + ($Self).claimed := false + ($Self).count := 0 + } +field claimed: Bool +field count: Int +define invariant_9($Self) ((((($Self).claimed && (!(-1 == -1))) && (-42 == -42)) || true)) +define invariant_10($Self) ((($Self).count > 0)) +define invariant_11($Self) (((!($Self).claimed) ==> (($Self).count == 0))) +method claim($Self: Ref) + + requires $Perm($Self) + requires (($Self).count >= 0) + requires $Inv($Self) + ensures $Perm($Self) + ensures (($Self).count >= 0) + ensures $Inv($Self) + { + assume (($Self).claimed ==> (($Self).count > 0)) + } +method loops($Self: Ref) + + requires $Perm($Self) + requires $Inv($Self) + ensures $Perm($Self) + ensures $Inv($Self) + { var i: Int + i := 0 + while ((i > 0)) { + { + i := (i + 1) + }} + } diff --git a/test/viper/ok/unsupported.vpr.ok b/test/viper/ok/unsupported.vpr.ok new file mode 100644 index 00000000000..30d4be4428b --- /dev/null +++ b/test/viper/ok/unsupported.vpr.ok @@ -0,0 +1,3 @@ +unsupported.mo:5.3-5.13: viper error [0], translation to viper failed: +(LetD (VarP x) (LitE (TextLit ))) + diff --git a/test/viper/ok/unsupported.vpr.ret.ok b/test/viper/ok/unsupported.vpr.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/viper/ok/unsupported.vpr.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/viper/unsupported.mo b/test/viper/unsupported.mo new file mode 100644 index 00000000000..1dcec99779f --- /dev/null +++ b/test/viper/unsupported.mo @@ -0,0 +1,7 @@ +// @verify + +actor { + + let x = ""; // strings aren't supported + +}