Skip to content

Commit

Permalink
motoko-san: ADT encoding for tuples
Browse files Browse the repository at this point in the history
  • Loading branch information
int-index committed Jun 16, 2024
1 parent 076885a commit 34a6244
Show file tree
Hide file tree
Showing 51 changed files with 244 additions and 479 deletions.
5 changes: 3 additions & 2 deletions src/pipeline/pipeline.ml
Original file line number Diff line number Diff line change
Expand Up @@ -509,8 +509,9 @@ let viper_files' parsefn files : viper_result =
let* () = Typing.check_actors ~viper_mode:true 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 (Viper.Prep.prep_unit u) in
let s = Viper.Pretty.prog_mapped "" v in
let reqs = Viper.Common.init_reqs () in
let* v = Viper.Trans.unit reqs (Viper.Prep.prep_unit u) in
let s = Viper.Pretty.prog_mapped "" reqs v in
Diag.return s

let viper_files files : viper_result =
Expand Down
18 changes: 18 additions & 0 deletions src/viper/common.ml
Original file line number Diff line number Diff line change
Expand Up @@ -8,3 +8,21 @@ let rec map_last ~f = function
| [] -> []
| [ x ] -> [ f x ]
| x :: xs -> x :: map_last ~f xs

let tup_con_name n =
Printf.sprintf "Tup$%d" n

let tup_prj_name n i =
Printf.sprintf "tup$%d$%d" n i

module IntSet = Set.Make(struct
type t = int
let compare = compare
end)

(* Requirements arising from the translated code. In trans.ml we collect those
requirements, in prelude.ml we generate definitons to satisfy them. *)
type reqs = { tuple_arities : IntSet.t ref }

let init_reqs () = { tuple_arities = ref IntSet.empty }

67 changes: 50 additions & 17 deletions src/viper/prelude.ml
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
let prelude : string = {prelude|/* BEGIN PRELUDE */
/* Array encoding */
open Common

let prelude_array_encoding : string = {prelude|/* Array encoding */
domain Array {
function $loc(a: Array, i: Int): Ref
function $size(a: Array): Int
Expand All @@ -10,27 +11,59 @@ 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
function $prj_inv1(r: Ref): Tuple
function $prj_inv2(r: Ref): Int
axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
}
/* Option encoding */
define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x|prelude}

let pp_tup_decl_param ppf i = Format.fprintf ppf "T%d" i
let pp_tup_decl_params ppf = function
| 0 -> ()
| n ->
let comma ppf () = Format.fprintf ppf ",@ " in
Format.fprintf ppf "[%a]"
(Format.pp_print_list pp_tup_decl_param ~pp_sep:comma) (List.init n Fun.id)

let pp_tup_decl_con_field n ppf i =
Format.fprintf ppf "%s : %a"
(tup_prj_name n i)
pp_tup_decl_param i
let pp_tup_decl_con ppf n =
let comma ppf () = Format.fprintf ppf ",@ " in
Format.fprintf ppf "%s@[(%a)@]"
(tup_con_name n)
(Format.pp_print_list ~pp_sep:comma (pp_tup_decl_con_field n)) (List.init n Fun.id)

let pp_tup_decl n =
Format.asprintf "@[<2>adt Tuple$%d@;%a@;@[<v 2>{ %a }@]@]"
n
pp_tup_decl_params n
pp_tup_decl_con n

let prelude_tuple_encoding (tuple_arities : IntSet.t) : string =
String.concat "\n"
("/* Tuple encoding */" ::
List.map pp_tup_decl (IntSet.elements tuple_arities))

let prelude_option_encoding : string = {prelude|/* Option encoding */
adt Option[T] {
None()
Some(some$0: T)
}
/* Typed references */
}|prelude}

let prelude_typed_references : string = {prelude|/* Typed references */
field $int: Int
field $bool: Bool
field $ref: Ref
field $array: Array
field $tuple: Tuple
field $option_int: Option[Int]
field $option_bool: Option[Bool]
field $option_array: Option[Array]
field $option_tuple: Option[Tuple]
/* END PRELUDE */|prelude}
field $option_array: Option[Array]|prelude}

let prelude reqs: string =
String.concat "\n"
[
"/* BEGIN PRELUDE */";
prelude_array_encoding;
prelude_tuple_encoding !(reqs.tuple_arities);
prelude_option_encoding;
prelude_typed_references;
"/* END PRELUDE */"
]
12 changes: 8 additions & 4 deletions src/viper/pretty.ml
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,11 @@ and pp_typ ppf t =
| BoolT -> pr ppf "Bool"
| RefT -> pr ppf "Ref"
| ArrayT -> pr ppf "Array"
| TupleT -> pr ppf "Tuple"
| TupleT [] -> pr ppf "Tuple$0"
| TupleT ts ->
fprintf ppf "@[Tuple$%d[%a]@]"
(List.length ts)
(pp_print_list ~pp_sep:comma pp_typ) ts
| OptionT t -> fprintf ppf "@[Option[%a]@]" pp_typ t
| ConT(con, []) -> fprintf ppf "%s" con.it
| ConT(con, ts) ->
Expand Down Expand Up @@ -253,11 +257,11 @@ and pp_fldacc ppf fldacc =
and pp_loop_inv ppf inv =
fprintf ppf "invariant %a" pp_exp inv

let prog_mapped file p =
let prog_mapped file tuple_arities p =
marks := [];
let b = Buffer.create 16 in
let ppf = Format.formatter_of_buffer b in
Format.fprintf ppf "@[%s@]@.@.@[%a@]" prelude pp_prog p;
Format.fprintf ppf "@[%s@]@.@.@[%a@]" (prelude tuple_arities) pp_prog p;
Format.pp_print_flush ppf ();
let in_file { left; right } =
let left, right = { left with file }, { right with file } in
Expand Down Expand Up @@ -294,4 +298,4 @@ let prog_mapped file p =
List.fold_left tighten None mapping in
Buffer.contents b, lookup

let prog p = fst (prog_mapped "" p)
let prog tuple_arities p = fst (prog_mapped "" tuple_arities p)
2 changes: 1 addition & 1 deletion src/viper/syntax.ml
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ and typ' =
| BoolT
| RefT
| ArrayT
| TupleT
| TupleT of typ list
| OptionT of typ
| ConT of id * typ list

Loading

0 comments on commit 34a6244

Please sign in to comment.