From f9771ae979176284f701da427d97831c0bfc2629 Mon Sep 17 00:00:00 2001 From: Vladislav Zavialov Date: Sun, 2 Jun 2024 21:11:26 +0200 Subject: [PATCH] motoko-san: mock the Array module --- src/viper/prelude.ml | 1 + src/viper/trans.ml | 59 ++++++++++++++++++++++--- test/run.sh | 4 ++ test/viper/ok/array.silicon.ok | 2 +- test/viper/ok/array.vpr.ok | 1 + test/viper/ok/assertions.silicon.ok | 4 +- test/viper/ok/assertions.vpr.ok | 1 + test/viper/ok/async.silicon.ok | 2 +- test/viper/ok/async.vpr.ok | 1 + test/viper/ok/claim-broken.silicon.ok | 2 +- test/viper/ok/claim-broken.vpr.ok | 1 + test/viper/ok/claim-reward-naive.vpr.ok | 1 + test/viper/ok/claim-simple.silicon.ok | 2 +- test/viper/ok/claim-simple.vpr.ok | 1 + test/viper/ok/claim.vpr.ok | 1 + test/viper/ok/counter.silicon.ok | 2 +- test/viper/ok/counter.vpr.ok | 1 + test/viper/ok/invariant.silicon.ok | 2 +- test/viper/ok/invariant.vpr.ok | 1 + test/viper/ok/lits.silicon.ok | 4 +- test/viper/ok/lits.vpr.ok | 1 + test/viper/ok/loop-invariant.silicon.ok | 4 +- test/viper/ok/loop-invariant.vpr.ok | 1 + test/viper/ok/method-call.silicon.ok | 2 +- test/viper/ok/method-call.vpr.ok | 1 + test/viper/ok/nats.silicon.ok | 2 +- test/viper/ok/nats.vpr.ok | 1 + test/viper/ok/odd-even.silicon.ok | 4 +- test/viper/ok/odd-even.vpr.ok | 1 + test/viper/ok/option.silicon.ok | 2 +- test/viper/ok/option.vpr.ok | 1 + test/viper/ok/polymono.silicon.ok | 4 +- test/viper/ok/polymono.vpr.ok | 1 + test/viper/ok/private.vpr.ok | 1 + test/viper/ok/reverse.silicon.ok | 2 +- test/viper/ok/reverse.tc.ok | 8 ++-- test/viper/ok/reverse.vpr.ok | 10 ++--- test/viper/ok/reverse.vpr.stderr.ok | 8 ++-- test/viper/ok/simple-funs.silicon.ok | 4 +- test/viper/ok/simple-funs.vpr.ok | 1 + test/viper/ok/tuple.silicon.ok | 2 +- test/viper/ok/tuple.vpr.ok | 1 + test/viper/ok/variants.silicon.ok | 4 +- test/viper/ok/variants.vpr.ok | 1 + test/viper/pkg/base/Array.mo | 5 +++ test/viper/reverse.mo | 3 +- 46 files changed, 123 insertions(+), 45 deletions(-) create mode 100644 test/viper/pkg/base/Array.mo diff --git a/src/viper/prelude.ml b/src/viper/prelude.ml index 99f038b56a9..21a1f378dfc 100644 --- a/src/viper/prelude.ml +++ b/src/viper/prelude.ml @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/src/viper/trans.ml b/src/viper/trans.ml index bf87e3fcf86..26e498ae57e 100644 --- a/src/viper/trans.ml +++ b/src/viper/trans.ml @@ -95,10 +95,16 @@ let lvalue_str (lval : lvalue) : string = | LValueUninitVar x -> x.it | LValueFld fld -> (snd fld).it +type imported_module = + | IM_Prim (* mo:⛔ *) + | IM_base_Array (* mo:base/Array *) + module Env = T.Env +module Imports = Map.Make(String) type ctxt = { self : string option; + imports : imported_module Imports.t; ids : (sort * T.t) T.Env.t; ghost_items : (ctxt -> item) list ref; ghost_inits : (ctxt -> seqn') list ref; @@ -178,7 +184,15 @@ 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 = { + self = None; + imports = tr_imports imports; + ids = Env.empty; + ghost_items = ref []; + ghost_inits = ref []; + ghost_perms = ref []; + ghost_conc = ref [] + } in let ctxt', perms, 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 *) @@ -250,6 +264,20 @@ and unit' (u : M.comp_unit) : prog = !!! (body.at) is | _ -> assert false +and tr_imports (imps : M.import list) : imported_module Imports.t = + List.fold_left + (fun acc imp -> + let k, v = tr_import imp in + Imports.add k v acc) + Imports.empty + imps + +and tr_import (imp : M.import) : (string * imported_module) = + match imp.it with + | ({it=M.VarP s;_}, "mo:⛔", _) -> (s.it, IM_Prim) + | ({it=M.VarP s;_}, "mo:base/Array", _) -> (s.it, IM_base_Array) + | (p, _, _) -> unsupported p.at (Arrange.pat p) + and dec_fields (ctxt : ctxt) (ds : M.dec_field list) = match ds with | [] -> @@ -271,7 +299,7 @@ and dec_field ctxt d = and static_invariants at lhs e = match e.it with | M.AnnotE (e, _) -> static_invariants at lhs e - | M.ArrayE (_, es) -> [array_size_inv at lhs (List.length es)] + | M.ArrayE (_, es) -> [array_size_inv at lhs (intLitE at (List.length es))] | _ -> [] and dec_field' ctxt d = @@ -643,6 +671,20 @@ and assign_stmts ctxt at (lval : lvalue) (e : M.exp) : seqn' = match e with | M.({it=TupE [];_}) -> [], [] | M.({it=AnnotE (e, _);_}) -> assign_stmts ctxt at lval e + | M.({it=CallE ({it=M.DotE ({it=M.VarE(m);_}, {it="init";_});_}, _inst, args);_}) + when Imports.find_opt (m.it) ctxt.imports = Some(IM_base_Array) + -> + begin match args with + | M.({it=TupE([e1;e2]); _}) -> + fld_via_tmp_var lval t (fun x -> + let lhs = !!(LocalVar (x, tr_typ t)) in + [], [ !!(AssertS !!(GeCmpE (exp ctxt e1, intLitE at 0))) + ; !!(InhaleS (array_acc at lhs (array_elem_t t))) + ; !!(InhaleS (array_size_inv at lhs (exp ctxt e1))) + ; !!(InhaleS (array_init_const at lhs (array_elem_t t) (exp ctxt e2))) ] + ) + | _ -> unsupported args.at (Arrange.exp args) + end | M.({it = CallE({it = VarE m; _}, inst, args); _}) -> fld_via_tmp_var lval t (fun x -> let self_var = self ctxt m.at in @@ -759,7 +801,10 @@ and exp ctxt e = !!(match e.it with | M.TupE es -> CallE (tag.it, List.map (exp ctxt) es) | _ -> CallE (tag.it, [exp ctxt e])) - | M.CallE ({ it = M.DotE (_, { it = "forall" | "exists" as predicate_name; _ }); _ }, _inst, { it = M.FuncE (_, _, _, pattern, _, _, e); note; _ }) -> + | M.CallE ({ it = M.DotE ({it=M.VarE(m);_}, {it=predicate_name;_}); _ }, _inst, { it = M.FuncE (_, _, _, pattern, _, _, e); note; _ }) + when Imports.find_opt (m.it) ctxt.imports = Some(IM_Prim) + && (predicate_name = "forall" || predicate_name = "exists") + -> let binders = extract_binders pattern in let typs = match M.(note.note_typ) with @@ -845,7 +890,7 @@ and typed_field t = | _ -> unsupported Source.no_region (Mo_types.Arrange_type.typ t) and array_size_inv at lhs n = - !!! at (EqCmpE (sizeE at lhs, intLitE at n)) + !!! at (EqCmpE (sizeE at lhs, n)) and array_acc at lhs t = match T.normalize t with @@ -865,11 +910,15 @@ and array_alloc at ctxt lhs t es : stmt list = | T.Mut _ -> [] | _ -> [ExhaleS (array_acc at lhs t); InhaleS (array_acc at lhs t)])in let stmts = [ InhaleS (array_acc at lhs (T.Mut t)) - ; InhaleS (array_size_inv at lhs (List.length es))] + ; InhaleS (array_size_inv at lhs (intLitE at (List.length es)))] @ init_array @ reset_perm in List.map (!!) stmts +and array_init_const at lhs t x = + let (!!) p = !!! at p in + !! (CallE ("$array_init", [lhs; !!(FldE (typed_field t)); x])) + and array_loc ctxt at e1 e2 t = locE at (exp ctxt e1) (exp ctxt e2) (typed_field t) diff --git a/test/run.sh b/test/run.sh index 142d3a912df..5563608e987 100755 --- a/test/run.sh +++ b/test/run.sh @@ -314,6 +314,10 @@ do else TEST_MOC_ARGS=$EXTRA_MOC_ARGS fi + if [ $VIPER = 'yes' ] + then + TEST_MOC_ARGS="$TEST_MOC_ARGS --package base pkg/base" + fi moc_with_flags="env $moc_extra_env moc $moc_extra_flags $TEST_MOC_ARGS" # Typecheck diff --git a/test/viper/ok/array.silicon.ok b/test/viper/ok/array.silicon.ok index dc4206b8f7d..2e8e44da203 100644 --- a/test/viper/ok/array.silicon.ok +++ b/test/viper/ok/array.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (array.vpr@46.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (array.vpr@47.1) diff --git a/test/viper/ok/array.vpr.ok b/test/viper/ok/array.vpr.ok index 896ea80fbb2..acc6da601cb 100644 --- a/test/viper/ok/array.vpr.ok +++ b/test/viper/ok/array.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/assertions.silicon.ok b/test/viper/ok/assertions.silicon.ok index 1c0878ce6a6..731aff3f2da 100644 --- a/test/viper/ok/assertions.silicon.ok +++ b/test/viper/ok/assertions.silicon.ok @@ -1,2 +1,2 @@ - [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@46.13--46.24) - [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@64.15--64.44) + [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@47.13--47.24) + [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@65.15--65.44) diff --git a/test/viper/ok/assertions.vpr.ok b/test/viper/ok/assertions.vpr.ok index 6a7b6e32dd7..0714d2ffab1 100644 --- a/test/viper/ok/assertions.vpr.ok +++ b/test/viper/ok/assertions.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/async.silicon.ok b/test/viper/ok/async.silicon.ok index 71cd3dc5691..f343396fd9c 100644 --- a/test/viper/ok/async.silicon.ok +++ b/test/viper/ok/async.silicon.ok @@ -1 +1 @@ - [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@69.15--69.42) + [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@70.15--70.42) diff --git a/test/viper/ok/async.vpr.ok b/test/viper/ok/async.vpr.ok index d37cd8572fe..e260d2ecce8 100644 --- a/test/viper/ok/async.vpr.ok +++ b/test/viper/ok/async.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/claim-broken.silicon.ok b/test/viper/ok/claim-broken.silicon.ok index 63db8799253..728650f59e5 100644 --- a/test/viper/ok/claim-broken.silicon.ok +++ b/test/viper/ok/claim-broken.silicon.ok @@ -1 +1 @@ - [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@67.20--67.47) + [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@68.20--68.47) diff --git a/test/viper/ok/claim-broken.vpr.ok b/test/viper/ok/claim-broken.vpr.ok index b0d7564b48d..f4f71780802 100644 --- a/test/viper/ok/claim-broken.vpr.ok +++ b/test/viper/ok/claim-broken.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/claim-reward-naive.vpr.ok b/test/viper/ok/claim-reward-naive.vpr.ok index af0d648480e..2beffb31026 100644 --- a/test/viper/ok/claim-reward-naive.vpr.ok +++ b/test/viper/ok/claim-reward-naive.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/claim-simple.silicon.ok b/test/viper/ok/claim-simple.silicon.ok index de2d22407eb..3a23be0094a 100644 --- a/test/viper/ok/claim-simple.silicon.ok +++ b/test/viper/ok/claim-simple.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (claim-simple.vpr@38.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (claim-simple.vpr@39.1) diff --git a/test/viper/ok/claim-simple.vpr.ok b/test/viper/ok/claim-simple.vpr.ok index 808b33b356e..bee8ebcba75 100644 --- a/test/viper/ok/claim-simple.vpr.ok +++ b/test/viper/ok/claim-simple.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/claim.vpr.ok b/test/viper/ok/claim.vpr.ok index f8679a31150..c6f00ec1647 100644 --- a/test/viper/ok/claim.vpr.ok +++ b/test/viper/ok/claim.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/counter.silicon.ok b/test/viper/ok/counter.silicon.ok index bd240ee0e3d..68b65438d5c 100644 --- a/test/viper/ok/counter.silicon.ok +++ b/test/viper/ok/counter.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (counter.vpr@38.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (counter.vpr@39.1) diff --git a/test/viper/ok/counter.vpr.ok b/test/viper/ok/counter.vpr.ok index 4a7b83bf366..28342694529 100644 --- a/test/viper/ok/counter.vpr.ok +++ b/test/viper/ok/counter.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/invariant.silicon.ok b/test/viper/ok/invariant.silicon.ok index 7638af33db4..c9d2e06097f 100644 --- a/test/viper/ok/invariant.silicon.ok +++ b/test/viper/ok/invariant.silicon.ok @@ -1 +1 @@ - [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@43.13--43.24) + [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@44.13--44.24) diff --git a/test/viper/ok/invariant.vpr.ok b/test/viper/ok/invariant.vpr.ok index 1a5769b06a0..3ff3b243551 100644 --- a/test/viper/ok/invariant.vpr.ok +++ b/test/viper/ok/invariant.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/lits.silicon.ok b/test/viper/ok/lits.silicon.ok index b9e8db2fdb7..7c120307087 100644 --- a/test/viper/ok/lits.silicon.ok +++ b/test/viper/ok/lits.silicon.ok @@ -1,2 +1,2 @@ -Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (lits.vpr@37.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (lits.vpr@38.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (lits.vpr@38.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (lits.vpr@39.1) diff --git a/test/viper/ok/lits.vpr.ok b/test/viper/ok/lits.vpr.ok index 8b8226ef80a..bf4d6883fde 100644 --- a/test/viper/ok/lits.vpr.ok +++ b/test/viper/ok/lits.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/loop-invariant.silicon.ok b/test/viper/ok/loop-invariant.silicon.ok index 3dba2b49c20..5af1d32b9da 100644 --- a/test/viper/ok/loop-invariant.silicon.ok +++ b/test/viper/ok/loop-invariant.silicon.ok @@ -1,2 +1,2 @@ -Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (loop-invariant.vpr@37.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (loop-invariant.vpr@38.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (loop-invariant.vpr@38.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (loop-invariant.vpr@39.1) diff --git a/test/viper/ok/loop-invariant.vpr.ok b/test/viper/ok/loop-invariant.vpr.ok index 2cd1e593141..948c5c20e80 100644 --- a/test/viper/ok/loop-invariant.vpr.ok +++ b/test/viper/ok/loop-invariant.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/method-call.silicon.ok b/test/viper/ok/method-call.silicon.ok index 7d42acbf433..7d73cab3c31 100644 --- a/test/viper/ok/method-call.silicon.ok +++ b/test/viper/ok/method-call.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (method-call.vpr@38.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (method-call.vpr@39.1) diff --git a/test/viper/ok/method-call.vpr.ok b/test/viper/ok/method-call.vpr.ok index a321d1a1a45..62903bdda37 100644 --- a/test/viper/ok/method-call.vpr.ok +++ b/test/viper/ok/method-call.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/nats.silicon.ok b/test/viper/ok/nats.silicon.ok index ab81ca6c18c..6ca52ee0c9a 100644 --- a/test/viper/ok/nats.silicon.ok +++ b/test/viper/ok/nats.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (nats.vpr@38.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (nats.vpr@39.1) diff --git a/test/viper/ok/nats.vpr.ok b/test/viper/ok/nats.vpr.ok index 42ad155e097..a93b86c7048 100644 --- a/test/viper/ok/nats.vpr.ok +++ b/test/viper/ok/nats.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/odd-even.silicon.ok b/test/viper/ok/odd-even.silicon.ok index 4e3284c5706..9409ad1be32 100644 --- a/test/viper/ok/odd-even.silicon.ok +++ b/test/viper/ok/odd-even.silicon.ok @@ -1,2 +1,2 @@ -Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (odd-even.vpr@37.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (odd-even.vpr@38.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (odd-even.vpr@38.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (odd-even.vpr@39.1) diff --git a/test/viper/ok/odd-even.vpr.ok b/test/viper/ok/odd-even.vpr.ok index 785704f2e87..81339b1e185 100644 --- a/test/viper/ok/odd-even.vpr.ok +++ b/test/viper/ok/odd-even.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/option.silicon.ok b/test/viper/ok/option.silicon.ok index a75b26b9765..df52524a5b3 100644 --- a/test/viper/ok/option.silicon.ok +++ b/test/viper/ok/option.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (option.vpr@38.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (option.vpr@39.1) diff --git a/test/viper/ok/option.vpr.ok b/test/viper/ok/option.vpr.ok index db4d5728c93..bc2dd0275ac 100644 --- a/test/viper/ok/option.vpr.ok +++ b/test/viper/ok/option.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/polymono.silicon.ok b/test/viper/ok/polymono.silicon.ok index 824ad659969..32f5c8b91a8 100644 --- a/test/viper/ok/polymono.silicon.ok +++ b/test/viper/ok/polymono.silicon.ok @@ -1,2 +1,2 @@ -Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (polymono.vpr@37.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (polymono.vpr@38.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (polymono.vpr@38.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (polymono.vpr@39.1) diff --git a/test/viper/ok/polymono.vpr.ok b/test/viper/ok/polymono.vpr.ok index f8f7c025cda..01c5b7a6e92 100644 --- a/test/viper/ok/polymono.vpr.ok +++ b/test/viper/ok/polymono.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/private.vpr.ok b/test/viper/ok/private.vpr.ok index 76a62e08c36..ffd04688657 100644 --- a/test/viper/ok/private.vpr.ok +++ b/test/viper/ok/private.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/reverse.silicon.ok b/test/viper/ok/reverse.silicon.ok index df06cca5ed2..ab11e2bcfb1 100644 --- a/test/viper/ok/reverse.silicon.ok +++ b/test/viper/ok/reverse.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (reverse.vpr@41.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (reverse.vpr@42.1) diff --git a/test/viper/ok/reverse.tc.ok b/test/viper/ok/reverse.tc.ok index 6919d61a7d0..a7e20456276 100644 --- a/test/viper/ok/reverse.tc.ok +++ b/test/viper/ok/reverse.tc.ok @@ -1,7 +1,7 @@ -reverse.mo:31.13-31.23: warning [M0155], operator may trap for inferred type +reverse.mo:32.13-32.23: warning [M0155], operator may trap for inferred type Nat -reverse.mo:36.35-36.47: warning [M0155], operator may trap for inferred type +reverse.mo:37.35-37.47: warning [M0155], operator may trap for inferred type Nat -reverse.mo:36.35-36.51: warning [M0155], operator may trap for inferred type +reverse.mo:37.35-37.51: warning [M0155], operator may trap for inferred type Nat -reverse.mo:25.9-25.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`) +reverse.mo:26.9-26.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 6dda372fee1..4ea3b33245e 100644 --- a/test/viper/ok/reverse.vpr.ok +++ b/test/viper/ok/reverse.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref @@ -115,13 +116,10 @@ method copy_xarray($Self: Ref) var t: Array var i: Int length := $size(($Self).xarray); + assert (length >= 0); inhale $array_acc(t, $int, write); - inhale ($size(t) == 5); - ($loc(t, 0)).$int := 0; - ($loc(t, 1)).$int := 0; - ($loc(t, 2)).$int := 0; - ($loc(t, 3)).$int := 0; - ($loc(t, 4)).$int := 0; + inhale ($size(t) == length); + inhale $array_init(t, $int, 0); i := 0; while ((i < length)) invariant $array_acc(t, $int, write) diff --git a/test/viper/ok/reverse.vpr.stderr.ok b/test/viper/ok/reverse.vpr.stderr.ok index 6919d61a7d0..a7e20456276 100644 --- a/test/viper/ok/reverse.vpr.stderr.ok +++ b/test/viper/ok/reverse.vpr.stderr.ok @@ -1,7 +1,7 @@ -reverse.mo:31.13-31.23: warning [M0155], operator may trap for inferred type +reverse.mo:32.13-32.23: warning [M0155], operator may trap for inferred type Nat -reverse.mo:36.35-36.47: warning [M0155], operator may trap for inferred type +reverse.mo:37.35-37.47: warning [M0155], operator may trap for inferred type Nat -reverse.mo:36.35-36.51: warning [M0155], operator may trap for inferred type +reverse.mo:37.35-37.51: warning [M0155], operator may trap for inferred type Nat -reverse.mo:25.9-25.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`) +reverse.mo:26.9-26.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`) diff --git a/test/viper/ok/simple-funs.silicon.ok b/test/viper/ok/simple-funs.silicon.ok index 3b186feb918..4b109ba9fe8 100644 --- a/test/viper/ok/simple-funs.silicon.ok +++ b/test/viper/ok/simple-funs.silicon.ok @@ -1,2 +1,2 @@ -Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (simple-funs.vpr@37.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (simple-funs.vpr@38.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (simple-funs.vpr@38.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (simple-funs.vpr@39.1) diff --git a/test/viper/ok/simple-funs.vpr.ok b/test/viper/ok/simple-funs.vpr.ok index 2cfd17e7002..a761a933c37 100644 --- a/test/viper/ok/simple-funs.vpr.ok +++ b/test/viper/ok/simple-funs.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/tuple.silicon.ok b/test/viper/ok/tuple.silicon.ok index cf1fccc4738..9914bdacfd7 100644 --- a/test/viper/ok/tuple.silicon.ok +++ b/test/viper/ok/tuple.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (tuple.vpr@42.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (tuple.vpr@43.1) diff --git a/test/viper/ok/tuple.vpr.ok b/test/viper/ok/tuple.vpr.ok index d857252c085..f1742ca96aa 100644 --- a/test/viper/ok/tuple.vpr.ok +++ b/test/viper/ok/tuple.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/ok/variants.silicon.ok b/test/viper/ok/variants.silicon.ok index d2588c5c13f..a383ee1a1b6 100644 --- a/test/viper/ok/variants.silicon.ok +++ b/test/viper/ok/variants.silicon.ok @@ -1,2 +1,2 @@ -Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (variants.vpr@37.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (variants.vpr@38.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (variants.vpr@38.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (variants.vpr@39.1) diff --git a/test/viper/ok/variants.vpr.ok b/test/viper/ok/variants.vpr.ok index 6037c04a5d8..6cc6e4dc0a5 100644 --- a/test/viper/ok/variants.vpr.ok +++ b/test/viper/ok/variants.vpr.ok @@ -10,6 +10,7 @@ domain Array { } define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p) define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x /* Tuple encoding */ domain Tuple { function $prj(a: Tuple, i: Int): Ref diff --git a/test/viper/pkg/base/Array.mo b/test/viper/pkg/base/Array.mo new file mode 100644 index 00000000000..da7b728012c --- /dev/null +++ b/test/viper/pkg/base/Array.mo @@ -0,0 +1,5 @@ +import Prim "mo:⛔"; + +module { + public func init(size : Nat, initValue : X) : [var X] = Prim.Array_init(size, initValue); +} diff --git a/test/viper/reverse.mo b/test/viper/reverse.mo index 12306cb3d57..f7c74bdc13f 100644 --- a/test/viper/reverse.mo +++ b/test/viper/reverse.mo @@ -1,3 +1,4 @@ +import Array "mo:base/Array"; import Prim "mo:⛔"; // @verify @@ -7,7 +8,7 @@ actor Reverse { private func copy_xarray(): [var Nat] { assert:return (var:return).size() == xarray.size(); let length = xarray.size(); - let t = [var 0, 0, 0, 0, 0]; + let t = Array.init(length, 0); var i = 0; while (i < length) { assert:loop:invariant (i >= 0);