Skip to content

Commit

Permalink
motoko-san: add locations of pre/post conditions to the source mapper
Browse files Browse the repository at this point in the history
  • Loading branch information
@DK318
DK318 committed Jul 2, 2024
1 parent 1c0f9a9 commit 7f5bb81
Show file tree
Hide file tree
Showing 8 changed files with 101 additions and 92 deletions.
6 changes: 4 additions & 2 deletions src/viper/pretty.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,13 +93,15 @@ and pp_pres ppf exps =
fprintf ppf "@[<v 0>%a@]" (pp_print_list pp_pre) exps

and pp_pre ppf exp =
fprintf ppf "@[<v 2>requires %a@]" pp_exp exp
marks := exp.at :: !marks;
fprintf ppf "\017@[<v 2>requires %a@]\019" pp_exp exp

and pp_posts ppf exps =
fprintf ppf "@[<v 0>%a@]" (pp_print_list pp_post) exps

and pp_post ppf exp =
fprintf ppf "@[<v 2>ensures %a@]" pp_exp exp
marks := exp.at :: !marks;
fprintf ppf "\017@[<v 2>ensures %a@]\019" pp_exp exp

and pp_local ppf (id, typ) =
fprintf ppf "@[<2>%s: %a@]"
Expand Down
8 changes: 4 additions & 4 deletions src/viper/trans.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
16 changes: 8 additions & 8 deletions test/viper/ok/array-of-tuples.vpr.ok
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down
5 changes: 3 additions & 2 deletions test/viper/ok/reverse.vpr.ok
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions test/viper/ok/todo_record.tc.ok
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
todo_record.mo:109.23-109.28: warning [M0155], operator may trap for inferred type
Nat
67 changes: 34 additions & 33 deletions test/viper/ok/todo_record.vpr.ok
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)))
Expand Down Expand Up @@ -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);
Expand All @@ -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]
Expand Down Expand Up @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions test/viper/ok/todo_record.vpr.stderr.ok
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
todo_record.mo:109.23-109.28: warning [M0155], operator may trap for inferred type
Nat
Loading

0 comments on commit 7f5bb81

Please sign in to comment.