From 7f5bb81a887d9256a6f2882fcf89f62b6fce8623 Mon Sep 17 00:00:00 2001 From: Leonid Vasilev Date: Mon, 1 Jul 2024 22:52:51 +0400 Subject: [PATCH] motoko-san: add locations of pre/post conditions to the source mapper --- src/viper/pretty.ml | 6 +- src/viper/trans.ml | 8 +-- test/viper/ok/array-of-tuples.vpr.ok | 16 ++--- test/viper/ok/reverse.vpr.ok | 5 +- test/viper/ok/todo_record.tc.ok | 2 + test/viper/ok/todo_record.vpr.ok | 67 +++++++++---------- test/viper/ok/todo_record.vpr.stderr.ok | 2 + test/viper/ok/todo_tuple.vpr.ok | 87 +++++++++++++------------ 8 files changed, 101 insertions(+), 92 deletions(-) create mode 100644 test/viper/ok/todo_record.tc.ok create mode 100644 test/viper/ok/todo_record.vpr.stderr.ok diff --git a/src/viper/pretty.ml b/src/viper/pretty.ml index f4c0d1164a6..5d86110dc94 100644 --- a/src/viper/pretty.ml +++ b/src/viper/pretty.ml @@ -93,13 +93,15 @@ 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 + marks := exp.at :: !marks; + fprintf ppf "\017@[requires %a@]\019" 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 + marks := exp.at :: !marks; + fprintf ppf "\017@[ensures %a@]\019" pp_exp exp and pp_local ppf (id, typ) = fprintf ppf "@[<2>%s: %a@]" diff --git a/src/viper/trans.ml b/src/viper/trans.ml index abc4c0c8dcd..6f9c7e8f865 100644 --- a/src/viper/trans.ml +++ b/src/viper/trans.ml @@ -407,8 +407,8 @@ and dec_field' ctxt d = 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 pres, stmts' = List.partition_map (function { it = PreconditionS exp; at; _ } -> Left { exp with at } | s -> Right s) (snd stmts.it) in + let posts, stmts' = List.partition_map (function { it = PostconditionS exp; at; _ } -> Left { exp with at } | s -> Right s) stmts' in let arg_preds = local_access_preds ctxt in let ret_preds, ret = rets ctxt t_opt in let pres = arg_preds @ pres in @@ -434,8 +434,8 @@ and dec_field' ctxt d = 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 pres, stmts' = List.partition_map (function { it = PreconditionS exp; at; _ } -> Left { exp with at } | s -> Right s) (snd stmts.it) in + let posts, stmts' = List.partition_map (function { it = PostconditionS exp; at; _ } -> Left { exp with at } | s -> Right s) stmts' in let arg_preds = local_access_preds ctxt in let ret_preds, ret = rets ctxt t_opt in let pres = arg_preds @ pres in diff --git a/test/viper/ok/array-of-tuples.vpr.ok b/test/viper/ok/array-of-tuples.vpr.ok index 40fca261497..fb1c1be8261 100644 --- a/test/viper/ok/array-of-tuples.vpr.ok +++ b/test/viper/ok/array-of-tuples.vpr.ok @@ -60,17 +60,17 @@ method set_nested_mut_arr($Self: Ref, arr: Array) requires $Perm($Self) requires $array_acc(arr, $option$tuple2$option$int$tuple2$bool$bool, - write) + write) ensures $Perm($Self) ensures $array_acc(arr, $option$tuple2$option$int$tuple2$bool$bool, - write) + write) ensures ((($size(arr) >= 2) && (($loc(arr, 0)).$option$tuple2$option$int$tuple2$bool$bool == - old(($loc(arr, 0)).$option$tuple2$option$int$tuple2$bool$bool))) && ( - ($loc(arr, 1)).$option$tuple2$option$int$tuple2$bool$bool == Some( - Tup$2( - Some(42), - Tup$2(true, - true))))) + old(($loc(arr, 0)).$option$tuple2$option$int$tuple2$bool$bool))) && ( + ($loc(arr, 1)).$option$tuple2$option$int$tuple2$bool$bool == Some( + Tup$2( + Some(42), + Tup$2(true, + true))))) { assume ($size(arr) >= 2); ($loc(arr, 1)).$option$tuple2$option$int$tuple2$bool$bool := Some( diff --git a/test/viper/ok/reverse.vpr.ok b/test/viper/ok/reverse.vpr.ok index ecbdf556dd8..e9b398c251d 100644 --- a/test/viper/ok/reverse.vpr.ok +++ b/test/viper/ok/reverse.vpr.ok @@ -51,8 +51,9 @@ method reverseArray$Nat($Self: Ref, a: Array) ensures $array_acc(a, $int, write) ensures ($size(($Self).xarray) == 5) ensures ($size(a) == old($size(a))) - ensures (forall k : Int :: (((0 <= k) && (k < $size(a))) ==> (($loc(a, k)).$int == - old(($loc(a, (($size(a) - 1) - k))).$int)))) + ensures (forall k : Int :: (((0 <= k) && (k < $size(a))) ==> (($loc(a, + k)).$int == + old(($loc(a, (($size(a) - 1) - k))).$int)))) { var b: Array var length: Int var i: Int diff --git a/test/viper/ok/todo_record.tc.ok b/test/viper/ok/todo_record.tc.ok new file mode 100644 index 00000000000..4d98bcfadb3 --- /dev/null +++ b/test/viper/ok/todo_record.tc.ok @@ -0,0 +1,2 @@ +todo_record.mo:109.23-109.28: warning [M0155], operator may trap for inferred type + Nat diff --git a/test/viper/ok/todo_record.vpr.ok b/test/viper/ok/todo_record.vpr.ok index 02b6ebd33ea..054f3380c69 100644 --- a/test/viper/ok/todo_record.vpr.ok +++ b/test/viper/ok/todo_record.vpr.ok @@ -58,17 +58,17 @@ method resize($Self: Ref, n: Int) requires $Perm($Self) requires ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos))) requires (forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> ( - (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id < ($Self).nextId))) + (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id < ($Self).nextId))) ensures $Perm($Self) ensures ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos))) ensures (forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> ( - (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id < ($Self).nextId))) + (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id < ($Self).nextId))) ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == - old(($Self).nextId))) + old(($Self).nextId))) ensures ($size(($Self).todos) >= n) ensures (old($size(($Self).todos)) <= $size(($Self).todos)) ensures (forall i : Int :: (((0 <= i) && (i < old($size(($Self).todos)))) ==> ( - ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) + ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) { var new_array: Array var i: Int if ((n <= $size(($Self).todos))) @@ -111,10 +111,10 @@ method getTodos($Self: Ref) ensures $Perm($Self) ensures $array_acc($Res, $c_ToDo, wildcard) ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == - old(($Self).nextId))) + old(($Self).nextId))) ensures ($size(($Self).todos) == old($size(($Self).todos))) ensures (forall i : Int :: (((0 <= i) && (i < old($size(($Self).todos)))) ==> ( - ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) + ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) ensures $Inv($Self) { var new_array: Array inhale $array_acc(new_array, $c_ToDo, write); @@ -132,26 +132,27 @@ method getTodo($Self: Ref, id: Int) requires $Inv($Self) ensures $Perm($Self) ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == - old(($Self).nextId))) + old(($Self).nextId))) ensures ($size(($Self).todos) == old($size(($Self).todos))) ensures (forall i : Int :: (((0 <= i) && (i < old($size(($Self).todos)))) ==> ( - ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) + ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) ensures ((exists i : Int :: (((0 <= i) && (i < ($Self).num)) && ( - (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id))) ==> - (exists i : Int :: (((0 <= i) && (i < ($Self).num)) && (Some(($loc( + (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id))) ==> + (exists i : Int :: (((0 <= i) && (i < ($Self).num)) && (Some(( + $loc( ($Self).todos, i)).$c_ToDo) == - ($Res).tup$2$0)))) + ($Res).tup$2$0)))) ensures ((($Res).tup$2$0 == None()) == (forall i : Int :: (((0 <= i) && (i < - ($Self).num)) ==> ((($loc( - ($Self).todos, - i)).$c_ToDo).$ToDo$id != id)))) + ($Self).num)) ==> ((($loc( + ($Self).todos, + i)).$c_ToDo).$ToDo$id != id)))) ensures ((($Res).tup$2$0 != None()) ==> ((0 <= ($Res).tup$2$1) && ( - ($Res).tup$2$1 < $size(($Self).todos)))) - ensures ((($Res).tup$2$0 != None()) ==> (($Res).tup$2$0 == Some(( - $loc( - ($Self).todos, - ($Res).tup$2$1)).$c_ToDo))) + ($Res).tup$2$1 < $size(($Self).todos)))) + ensures ((($Res).tup$2$0 != None()) ==> (($Res).tup$2$0 == Some( + ($loc( + ($Self).todos, + ($Res).tup$2$1)).$c_ToDo))) ensures $Inv($Self) { var i: Int var res: Option[ToDo] @@ -200,10 +201,10 @@ method addTodo($Self: Ref, description: Int) ensures (($Self).nextId == (old(($Self).nextId) + 1)) ensures ($Res == old(($Self).nextId)) ensures (($loc(($Self).todos, (($Self).num - 1))).$c_ToDo == $RecordCtor_ToDo(description, - $Res, - TODO())) + $Res, + TODO())) ensures (forall i : Int :: (((0 <= i) && (i < (($Self).num - 1))) ==> ( - ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) + ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) ensures $Inv($Self) { var id: Int id := ($Self).nextId; @@ -225,14 +226,14 @@ method completeTodo($Self: Ref, id: Int) requires $Inv($Self) ensures $Perm($Self) ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == - old(($Self).nextId))) + old(($Self).nextId))) ensures ($size(($Self).todos) == old($size(($Self).todos))) ensures (forall i : Int :: ((((0 <= i) && (i < ($Self).num)) && ( - (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id != id)) ==> ( - ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) + (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id != id)) ==> ( + ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) ensures (forall i : Int :: ((((0 <= i) && (i < ($Self).num)) && ( - (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id)) ==> ( - (($loc(($Self).todos, i)).$c_ToDo).$ToDo$state == DONE()))) + (($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id)) ==> ( + (($loc(($Self).todos, i)).$c_ToDo).$ToDo$state == DONE()))) ensures $Inv($Self) { var i: Int i := 0; @@ -280,10 +281,10 @@ method showTodos($Self: Ref) requires $Inv($Self) ensures $Perm($Self) ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == - old(($Self).nextId))) + old(($Self).nextId))) ensures ($size(($Self).todos) == old($size(($Self).todos))) ensures (forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> ( - ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) + ($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))) ensures $Inv($Self) { var output: Int var i: Int @@ -327,11 +328,11 @@ method clearstate($Self: Ref) ensures (($Self).nextId == old(($Self).nextId)) ensures ($size(($Self).todos) == old($size(($Self).todos))) ensures (forall i : Int :: ((((0 <= i) && (i < old(($Self).num))) && ( - old((($loc(($Self).todos, i)).$c_ToDo).$ToDo$state) == TODO())) ==> - (exists k : Int :: (((0 <= k) && (k < $size(($Self).todos))) && ( - ($loc(($Self).todos, k)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))))) + old((($loc(($Self).todos, i)).$c_ToDo).$ToDo$state) == TODO())) ==> + (exists k : Int :: (((0 <= k) && (k < $size(($Self).todos))) && ( + ($loc(($Self).todos, k)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo)))))) ensures (forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> ( - (($loc(($Self).todos, i)).$c_ToDo).$ToDo$state == TODO()))) + (($loc(($Self).todos, i)).$c_ToDo).$ToDo$state == TODO()))) ensures $Inv($Self) { var new_array: Array var i: Int diff --git a/test/viper/ok/todo_record.vpr.stderr.ok b/test/viper/ok/todo_record.vpr.stderr.ok new file mode 100644 index 00000000000..4d98bcfadb3 --- /dev/null +++ b/test/viper/ok/todo_record.vpr.stderr.ok @@ -0,0 +1,2 @@ +todo_record.mo:109.23-109.28: warning [M0155], operator may trap for inferred type + Nat diff --git a/test/viper/ok/todo_tuple.vpr.ok b/test/viper/ok/todo_tuple.vpr.ok index 75ca3782186..dacdfb1c1ab 100644 --- a/test/viper/ok/todo_tuple.vpr.ok +++ b/test/viper/ok/todo_tuple.vpr.ok @@ -56,14 +56,14 @@ method resize($Self: Ref, n: Int) ensures $Perm($Self) ensures ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos))) ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == - old(($Self).nextId))) + old(($Self).nextId))) ensures ($size(($Self).todos) >= n) ensures (old($size(($Self).todos)) <= $size(($Self).todos)) ensures (forall i : Int :: (((0 <= i) && (i < old($size(($Self).todos)))) ==> ( - ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old(( - $loc( - ($Self).todos, - i)).$tuple3$int$int$c_State)))) + ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old( + ($loc( + ($Self).todos, + i)).$tuple3$int$int$c_State)))) { var new_array: Array var i: Int if ((n <= $size(($Self).todos))) @@ -107,13 +107,13 @@ method getTodos($Self: Ref) ensures $Perm($Self) ensures $array_acc($Res, $tuple3$int$int$c_State, wildcard) ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == - old(($Self).nextId))) + old(($Self).nextId))) ensures ($size(($Self).todos) == old($size(($Self).todos))) ensures (forall i : Int :: (((0 <= i) && (i < old($size(($Self).todos)))) ==> ( - ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old(( - $loc( - ($Self).todos, - i)).$tuple3$int$int$c_State)))) + ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old( + ($loc( + ($Self).todos, + i)).$tuple3$int$int$c_State)))) ensures $Inv($Self) { var new_array: Array inhale $array_acc(new_array, $tuple3$int$int$c_State, write); @@ -131,16 +131,17 @@ method getTodo($Self: Ref, id: Int) requires $Inv($Self) ensures $Perm($Self) ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == - old(($Self).nextId))) + old(($Self).nextId))) ensures ($size(($Self).todos) == old($size(($Self).todos))) ensures (forall i : Int :: (((0 <= i) && (i < old($size(($Self).todos)))) ==> ( - ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old(( - $loc( - ($Self).todos, - i)).$tuple3$int$int$c_State)))) + ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old( + ($loc( + ($Self).todos, + i)).$tuple3$int$int$c_State)))) ensures ((exists i : Int :: (((0 <= i) && (i < ($Self).num)) && ( - (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$0 == id))) ==> - (exists i : Int :: (((0 <= i) && (i < ($Self).num)) && (Some(($loc( + (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$0 == id))) ==> + (exists i : Int :: (((0 <= i) && (i < ($Self).num)) && (Some(( + $loc( ($Self).todos, i)).$tuple3$int$int$c_State) == $Res)))) ensures $Inv($Self) @@ -182,12 +183,12 @@ method addTodo($Self: Ref, description: Int) ensures (($Self).nextId == (old(($Self).nextId) + 1)) ensures ($Res == old(($Self).nextId)) ensures (($loc(($Self).todos, (($Self).num - 1))).$tuple3$int$int$c_State == - Tup$3($Res, description, TODO())) + Tup$3($Res, description, TODO())) ensures (forall i : Int :: (((0 <= i) && ((i + 1) < ($Self).num)) ==> ( - ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old(( - $loc( - ($Self).todos, - i)).$tuple3$int$int$c_State)))) + ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old( + ($loc( + ($Self).todos, + i)).$tuple3$int$int$c_State)))) ensures $Inv($Self) { var id: Int id := ($Self).nextId; @@ -209,18 +210,18 @@ method completeTodo($Self: Ref, id: Int) requires $Inv($Self) ensures $Perm($Self) ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == - old(($Self).nextId))) + old(($Self).nextId))) ensures ($size(($Self).todos) == old($size(($Self).todos))) ensures (forall i : Int :: ((((0 <= i) && (i < ($Self).num)) && ( - (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$0 != id)) ==> ( - ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old(( - $loc( - ($Self).todos, - i)).$tuple3$int$int$c_State)))) + (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$0 != id)) ==> ( + ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old( + ($loc( + ($Self).todos, + i)).$tuple3$int$int$c_State)))) ensures (forall i : Int :: ((((0 <= i) && (i < ($Self).num)) && ( - (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$0 == id)) ==> ( - (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$2 == - DONE()))) + (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$0 == id)) ==> ( + (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$2 == + DONE()))) ensures $Inv($Self) { var i: Int i := 0; @@ -266,13 +267,13 @@ method showTodos($Self: Ref) requires $Inv($Self) ensures $Perm($Self) ensures ((($Self).num == old(($Self).num)) && (($Self).nextId == - old(($Self).nextId))) + old(($Self).nextId))) ensures ($size(($Self).todos) == old($size(($Self).todos))) ensures (forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> ( - ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old(( - $loc( - ($Self).todos, - i)).$tuple3$int$int$c_State)))) + ($loc(($Self).todos, i)).$tuple3$int$int$c_State == old( + ($loc( + ($Self).todos, + i)).$tuple3$int$int$c_State)))) ensures $Inv($Self) { var output: Int var i: Int @@ -314,14 +315,14 @@ method clearCompleted($Self: Ref) ensures (($Self).nextId == old(($Self).nextId)) ensures ($size(($Self).todos) == old($size(($Self).todos))) ensures (forall i : Int :: ((((0 <= i) && (i < old(($Self).num))) && ( - old((($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$2) == - TODO())) ==> (exists k : Int :: (((0 <= k) && (k < $size( - ($Self).todos))) && ( - ($loc(($Self).todos, k)).$tuple3$int$int$c_State == - old(($loc(($Self).todos, i)).$tuple3$int$int$c_State)))))) + old((($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$2) == + TODO())) ==> (exists k : Int :: (((0 <= k) && (k < $size( + ($Self).todos))) && ( + ($loc(($Self).todos, k)).$tuple3$int$int$c_State == + old(($loc(($Self).todos, i)).$tuple3$int$int$c_State)))))) ensures (forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> ( - (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$2 == - TODO()))) + (($loc(($Self).todos, i)).$tuple3$int$int$c_State).tup$3$2 == + TODO()))) ensures $Inv($Self) { var new_array: Array var i: Int