From 7f656cb31b9434e616859046b9a21fcd04147653 Mon Sep 17 00:00:00 2001 From: Leonid Vasilev Date: Fri, 21 Jun 2024 18:04:04 +0400 Subject: [PATCH] motoko-san: pass the correct context in dec_field' --- src/viper/trans.ml | 34 ++++++++++++++--------------- test/viper/ok/reverse.tc.ok | 8 +++---- test/viper/ok/reverse.vpr.ok | 1 + test/viper/ok/reverse.vpr.stderr.ok | 8 +++---- test/viper/reverse.mo | 2 ++ 5 files changed, 28 insertions(+), 25 deletions(-) diff --git a/src/viper/trans.ml b/src/viper/trans.ml index 7ce9c818047..7f1278eb248 100644 --- a/src/viper/trans.ml +++ b/src/viper/trans.ml @@ -336,7 +336,7 @@ and dec_field' ctxt d = match d.M.dec.it with (* type declarations*) | M.(TypD (typ_id, typ_binds, {note = T.Variant cons;_})) -> - ctxt, None, None, fun _ -> + ctxt, None, None, fun ctxt -> let adt_param tb = id tb.it.M.var in let adt_con con = begin { con_name = !!! Source.no_region con.T.lab; @@ -356,21 +356,21 @@ and dec_field' ctxt d = { ctxt with ids = Env.add f.it (Method, note) ctxt.ids }, None, (* no perm *) None, (* no init *) - fun ctxt' -> + fun ctxt -> let open Either in let self_id = !!! (Source.no_region) "$Self" in let method_args = args p in - let method_args' = List.map (fun (id, t) -> id, tr_typ ctxt' t) method_args in - let ctxt'' = { ctxt' + let method_args' = List.map (fun (id, t) -> id, tr_typ ctxt t) method_args in + let ctxt = { ctxt with self = Some self_id.it; ids = List.fold_left (fun env (id, t) -> Env.add id.it (Local, t) env) ctxt.ids method_args } in - let stmts = stmt ctxt'' e in + 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 - let arg_preds = local_access_preds ctxt'' in - let ret_preds, ret = rets ctxt'' t_opt in + let arg_preds = local_access_preds ctxt in + let ret_preds, ret = rets ctxt t_opt in let pres = arg_preds @ pres in let posts = arg_preds @ ret_preds @ posts in let stmts'' = stmts' @ [!!! Source.no_region (LabelS(!!! (Source.no_region) "$Ret"))] in @@ -383,21 +383,21 @@ and dec_field' ctxt d = { ctxt with ids = Env.add f.it (Method, note) ctxt.ids }, None, (* no perm *) None, (* no init *) - fun ctxt' -> + fun ctxt -> let open Either in let self_id = !!! (Source.no_region) "$Self" in let method_args = args p in - let method_args' = List.map (fun (id, t) -> id, tr_typ ctxt' t) method_args in - let ctxt'' = { ctxt' + let method_args' = List.map (fun (id, t) -> id, tr_typ ctxt t) method_args in + let ctxt = { ctxt with self = Some self_id.it; ids = List.fold_left (fun env (id, t) -> Env.add id.it (Local, t) env) ctxt.ids method_args } in - let stmts = stmt ctxt'' e in + 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 - let arg_preds = local_access_preds ctxt'' in - let ret_preds, ret = rets ctxt'' t_opt in + let arg_preds = local_access_preds ctxt in + let ret_preds, ret = rets ctxt t_opt in let pres = arg_preds @ pres in let posts = arg_preds @ ret_preds @ posts in let stmts'' = stmts' @ [!!! Source.no_region (LabelS(!!! (Source.no_region) "$Ret"))] in @@ -418,16 +418,16 @@ and dec_field' ctxt d = Some (fun ctxt' -> (* init *) let at = span x.at e.at in assign_stmts ctxt' at (LValueFld (fldacc ctxt')) e), - (fun ctxt' -> - (FieldI(id x, tr_typ ctxt' t), + (fun ctxt -> + (FieldI(id x, tr_typ ctxt t), NoInfo)) (* invariants *) | M.(ExpD { it = AssertE (Invariant, e); at; _ }) -> ctxt, None, (* no perm *) None, (* no init *) - fun ctxt' -> - (InvariantI (Printf.sprintf "invariant_%d" at.left.line, exp { ctxt' with self = Some "$Self" } e), NoInfo) + 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) diff --git a/test/viper/ok/reverse.tc.ok b/test/viper/ok/reverse.tc.ok index a7e20456276..4a05ca89693 100644 --- a/test/viper/ok/reverse.tc.ok +++ b/test/viper/ok/reverse.tc.ok @@ -1,7 +1,7 @@ -reverse.mo:32.13-32.23: warning [M0155], operator may trap for inferred type +reverse.mo:34.13-34.23: warning [M0155], operator may trap for inferred type Nat -reverse.mo:37.35-37.47: warning [M0155], operator may trap for inferred type +reverse.mo:39.35-39.47: warning [M0155], operator may trap for inferred type Nat -reverse.mo:37.35-37.51: warning [M0155], operator may trap for inferred type +reverse.mo:39.35-39.51: warning [M0155], operator may trap for inferred type Nat -reverse.mo:26.9-26.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`) +reverse.mo:28.9-28.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`) diff --git a/test/viper/ok/reverse.vpr.ok b/test/viper/ok/reverse.vpr.ok index f58275916ba..7b25da6b406 100644 --- a/test/viper/ok/reverse.vpr.ok +++ b/test/viper/ok/reverse.vpr.ok @@ -47,6 +47,7 @@ method reverseArray$Nat($Self: Ref, a: Array) requires $Perm($Self) requires $array_acc(a, $int, write) + requires ($size(($Self).xarray) == 5) ensures $Perm($Self) ensures $array_acc(a, $int, write) ensures ($size(a) == old($size(a))) diff --git a/test/viper/ok/reverse.vpr.stderr.ok b/test/viper/ok/reverse.vpr.stderr.ok index a7e20456276..4a05ca89693 100644 --- a/test/viper/ok/reverse.vpr.stderr.ok +++ b/test/viper/ok/reverse.vpr.stderr.ok @@ -1,7 +1,7 @@ -reverse.mo:32.13-32.23: warning [M0155], operator may trap for inferred type +reverse.mo:34.13-34.23: warning [M0155], operator may trap for inferred type Nat -reverse.mo:37.35-37.47: warning [M0155], operator may trap for inferred type +reverse.mo:39.35-39.47: warning [M0155], operator may trap for inferred type Nat -reverse.mo:37.35-37.51: warning [M0155], operator may trap for inferred type +reverse.mo:39.35-39.51: warning [M0155], operator may trap for inferred type Nat -reverse.mo:26.9-26.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`) +reverse.mo:28.9-28.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`) diff --git a/test/viper/reverse.mo b/test/viper/reverse.mo index f7c74bdc13f..0c292c2e76f 100644 --- a/test/viper/reverse.mo +++ b/test/viper/reverse.mo @@ -20,6 +20,8 @@ actor Reverse { }; private func reverseArray(a : [var T]) : () { + assert:func xarray.size() == 5; + assert:return a.size() == (old (a.size())); assert:return Prim.forall( func (k : Nat) = (0 <= k and k < a.size()) implies a[k] == (old (a[a.size() - 1 - k])));