Proto: tracing script translator.

This commit is contained in:
Benjamin Canou 2016-11-10 16:25:31 +01:00
parent 0f91192769
commit 1e2911dd94
6 changed files with 692 additions and 599 deletions

View File

@ -56,48 +56,47 @@ let parse_program s =
with with
| exn -> report_parse_error "program: " exn lexbuf | exn -> report_parse_error "program: " exn lexbuf
let rec print_ir ppf node = let rec print_ir locations ppf node =
let open Script in let open Script in
let rec do_seq = function let rec do_seq = function
| [] -> assert false | [] -> assert false
| [ last ] -> Format.fprintf ppf "%a }@]" print_ir last | [ last ] -> Format.fprintf ppf "%a }@]" (print_ir locations) last
| fst :: rest -> Format.fprintf ppf "%a ;@ " print_ir fst ; do_seq rest in | fst :: rest -> Format.fprintf ppf "%a ;@ " (print_ir locations) fst ; do_seq rest in
let rec do_args = function let rec do_args = function
| [] -> assert false | [] -> assert false
| [ last ] -> Format.fprintf ppf "%a@]" print_ir last | [ last ] -> Format.fprintf ppf "%a@]" (print_ir locations) last
| fst :: rest -> Format.fprintf ppf "%a@," print_ir fst ; do_args rest in | fst :: rest -> Format.fprintf ppf "%a@," (print_ir locations) fst ; do_args rest in
let print_location ppf loc =
if locations loc then begin
Format.fprintf ppf " /* %d */" loc
end in
match node with match node with
| String (_, s) -> Format.fprintf ppf "%S" s | String (_, s) -> Format.fprintf ppf "%S" s
| Int (_, s) -> Format.fprintf ppf "%s" s | Int (_, s) -> Format.fprintf ppf "%s" s
| Seq (_, [ one ]) -> print_ir ppf one | Seq (_, [ one ]) -> print_ir locations ppf one
| Seq (_, []) -> Format.fprintf ppf "{}" ; | Seq (_, []) -> Format.fprintf ppf "{}" ;
| Seq (_, seq) -> | Seq (_, seq) ->
Format.fprintf ppf "{ @[<v>" ; Format.fprintf ppf "{ @[<v>" ;
do_seq seq do_seq seq
| Prim (_, "push", [ Prim (_, name, []) ]) -> | Prim (loc, name, []) ->
Format.fprintf ppf "push %s" name Format.fprintf ppf "%s%a" name print_location loc
| Prim (_, name, []) -> | Prim (loc, name, seq) ->
Format.fprintf ppf "%s" name Format.fprintf ppf "@[<v 2>%s%a@," name print_location loc;
| Prim (_, "push", [ Prim (_, name, seq) ]) ->
Format.fprintf ppf "push @[<v 2>%s@," name ;
do_args seq
| Prim (_, name, seq) ->
Format.fprintf ppf "@[<v 2>%s@," name ;
do_args seq do_args seq
let print_program ppf c = let print_program locations ppf c =
Format.fprintf ppf Format.fprintf ppf
"@[<v 2>storage@,%a@]@." "@[<v 2>storage@,%a@]@."
print_ir (c : Script.code).Script.storage_type ; (print_ir (fun _ -> false)) (c : Script.code).Script.storage_type ;
Format.fprintf ppf Format.fprintf ppf
"@[<v 2>parameter@,%a@]@." "@[<v 2>parameter@,%a@]@."
print_ir (c : Script.code).Script.arg_type ; (print_ir (fun _ -> false)) (c : Script.code).Script.arg_type ;
Format.fprintf ppf Format.fprintf ppf
"@[<v 2>return@,%a@]@." "@[<v 2>return@,%a@]@."
print_ir (c : Script.code).Script.ret_type ; (print_ir (fun _ -> false)) (c : Script.code).Script.ret_type ;
Format.fprintf ppf Format.fprintf ppf
"@[<v 2>code@,%a@]" "@[<v 2>code@,%a@]"
print_ir (c : Script.code).Script.code (print_ir locations) (c : Script.code).Script.code
let parse_data s = let parse_data s =
let lexbuf = Lexing.from_string s in let lexbuf = Lexing.from_string s in
@ -121,7 +120,7 @@ module Program = Client_aliases.Alias (struct
type t = Script.code type t = Script.code
let encoding = Script.code_encoding let encoding = Script.code_encoding
let of_source s = parse_program s let of_source s = parse_program s
let to_source p = Lwt.return (Format.asprintf "%a" print_program p) let to_source p = Lwt.return (Format.asprintf "%a" (print_program (fun _ -> false)) p)
let name = "program" let name = "program"
end) end)
@ -169,8 +168,22 @@ let commands () =
(fun program () -> (fun program () ->
let open Data_encoding in let open Data_encoding in
Client_proto_rpcs.Helpers.typecheck_code (block ()) program >>= function Client_proto_rpcs.Helpers.typecheck_code (block ()) program >>= function
| Ok () -> | Ok type_map ->
message "Well typed" ; message "Well typed" ;
print_program
(fun l -> List.mem_assoc l type_map)
Format.std_formatter program ;
Format.printf "@." ;
List.iter
(fun (loc, (before, after)) ->
Format.printf
"%3d@[<v 0> : [ @[<v 0>%a ]@]@,-> [ @[<v 0>%a ]@]@]@."
loc
(Format.pp_print_list (print_ir (fun _ -> false)))
before
(Format.pp_print_list (print_ir (fun _ -> false)))
after)
type_map ;
Lwt.return () Lwt.return ()
| Error errs -> | Error errs ->
pp_print_error Format.err_formatter errs ; pp_print_error Format.err_formatter errs ;

View File

@ -11,8 +11,6 @@ val parse_program: string -> Script.code Lwt.t
val parse_data: string -> Script.expr Lwt.t val parse_data: string -> Script.expr Lwt.t
val parse_data_type: string -> Script.expr Lwt.t val parse_data_type: string -> Script.expr Lwt.t
val print_program: Format.formatter -> Script.code -> unit
module Program : Client_aliases.Alias with type t = Script.code module Program : Client_aliases.Alias with type t = Script.code
val commands: unit -> Cli_entries.command list val commands: unit -> Cli_entries.command list

View File

@ -92,7 +92,7 @@ end
module Helpers : sig module Helpers : sig
val minimal_time: val minimal_time:
block -> ?prio:int -> unit -> Time.t tzresult Lwt.t block -> ?prio:int -> unit -> Time.t tzresult Lwt.t
val typecheck_code: block -> Script.code -> unit tzresult Lwt.t val typecheck_code: block -> Script.code -> Script_ir_translator.type_map tzresult Lwt.t
val typecheck_tagged_data: block -> Script.expr -> unit tzresult Lwt.t val typecheck_tagged_data: block -> Script.expr -> unit tzresult Lwt.t
val typecheck_untagged_data: block -> Script.expr * Script.expr -> unit tzresult Lwt.t val typecheck_untagged_data: block -> Script.expr * Script.expr -> unit tzresult Lwt.t
val hash_data: block -> Script.expr -> string tzresult Lwt.t val hash_data: block -> Script.expr -> string tzresult Lwt.t

View File

@ -684,11 +684,12 @@ and parse_untagged_comparable_data
and parse_lambda and parse_lambda
: type arg ret storage. context -> : type arg ret storage. context ->
?log: (int -> (stack_ty_val * stack_ty_val) -> unit) ->
?storage_type: storage ty -> ?storage_type: storage ty ->
arg ty -> ret ty -> Script.expr -> (arg, ret) lambda tzresult Lwt.t = arg ty -> ret ty -> Script.expr -> (arg, ret) lambda tzresult Lwt.t =
fun ctxt ?storage_type arg ret script_instr -> fun ctxt ?log ?storage_type arg ret script_instr ->
let loc = location script_instr in let loc = location script_instr in
parse_instr ctxt ?storage_type script_instr (Item_t (arg, Empty_t)) >>=? function parse_instr ctxt ?log ?storage_type script_instr (Item_t (arg, Empty_t)) >>=? function
| Typed (instr, (Item_t (ty, Empty_t) as stack_ty)) -> | Typed (instr, (Item_t (ty, Empty_t) as stack_ty)) ->
trace trace
(Bad_return (loc, Stack_ty stack_ty, Ty ret)) (Bad_return (loc, Stack_ty stack_ty, Ty ret))
@ -701,13 +702,14 @@ and parse_lambda
and parse_instr and parse_instr
: type bef storage. context -> : type bef storage. context ->
?log: (int -> (stack_ty_val * stack_ty_val) -> unit) ->
?storage_type: storage ty -> ?storage_type: storage ty ->
Script.expr -> bef stack_ty -> bef judgement tzresult Lwt.t = Script.expr -> bef stack_ty -> bef judgement tzresult Lwt.t =
fun ctxt ?storage_type script_instr stack_ty -> fun ctxt ?log ?storage_type script_instr stack_ty ->
let return : bef judgement -> bef judgement tzresult Lwt.t = return in let return : bef judgement -> bef judgement tzresult Lwt.t = return in
let check_item_ty got exp pos n = let check_item_ty got exp pos n =
ty_eq got exp |> record_trace (Bad_stack_item (pos, n)) |> Lwt.return in ty_eq got exp |> record_trace (Bad_stack_item (pos, n)) |> Lwt.return in
match script_instr, stack_ty with begin match script_instr, stack_ty with
(* stack ops *) (* stack ops *)
| Prim (_, "drop", []), | Prim (_, "drop", []),
Item_t (_, rest) -> Item_t (_, rest) ->
@ -734,8 +736,8 @@ and parse_instr
Item_t (Option_t t, rest) -> Item_t (Option_t t, rest) ->
expect_sequence_parameter loc Instr "if_none" 0 bt >>=? fun () -> expect_sequence_parameter loc Instr "if_none" 0 bt >>=? fun () ->
expect_sequence_parameter loc Instr "if_none" 1 bf >>=? fun () -> expect_sequence_parameter loc Instr "if_none" 1 bf >>=? fun () ->
parse_instr ?storage_type ctxt bt rest >>=? fun btr -> parse_instr ?log ?storage_type ctxt bt rest >>=? fun btr ->
parse_instr ?storage_type ctxt bf (Item_t (t, rest)) >>=? fun bfr -> parse_instr ?log ?storage_type ctxt bf (Item_t (t, rest)) >>=? fun bfr ->
let branch ibt ibf = If_none (ibt, ibf) in let branch ibt ibf = If_none (ibt, ibf) in
merge_branches loc btr bfr { branch } merge_branches loc btr bfr { branch }
(* pairs *) (* pairs *)
@ -761,8 +763,8 @@ and parse_instr
Item_t (Union_t (tl, tr), rest) -> Item_t (Union_t (tl, tr), rest) ->
expect_sequence_parameter loc Instr "if_left" 0 bt >>=? fun () -> expect_sequence_parameter loc Instr "if_left" 0 bt >>=? fun () ->
expect_sequence_parameter loc Instr "if_left" 1 bf >>=? fun () -> expect_sequence_parameter loc Instr "if_left" 1 bf >>=? fun () ->
parse_instr ?storage_type ctxt bt (Item_t (tl, rest)) >>=? fun btr -> parse_instr ?log ?storage_type ctxt bt (Item_t (tl, rest)) >>=? fun btr ->
parse_instr ?storage_type ctxt bf (Item_t (tr, rest)) >>=? fun bfr -> parse_instr ?log ?storage_type ctxt bf (Item_t (tr, rest)) >>=? fun bfr ->
let branch ibt ibf = If_left (ibt, ibf) in let branch ibt ibf = If_left (ibt, ibf) in
merge_branches loc btr bfr { branch } merge_branches loc btr bfr { branch }
(* lists *) (* lists *)
@ -780,8 +782,8 @@ and parse_instr
Item_t (List_t t, rest) -> Item_t (List_t t, rest) ->
expect_sequence_parameter loc Instr "if_cons" 0 bt >>=? fun () -> expect_sequence_parameter loc Instr "if_cons" 0 bt >>=? fun () ->
expect_sequence_parameter loc Instr "if_cons" 1 bf >>=? fun () -> expect_sequence_parameter loc Instr "if_cons" 1 bf >>=? fun () ->
parse_instr ?storage_type ctxt bt (Item_t (t, Item_t (List_t t, rest))) >>=? fun btr -> parse_instr ?log ?storage_type ctxt bt (Item_t (t, Item_t (List_t t, rest))) >>=? fun btr ->
parse_instr ?storage_type ctxt bf rest >>=? fun bfr -> parse_instr ?log ?storage_type ctxt bf rest >>=? fun bfr ->
let branch ibt ibf = If_cons (ibt, ibf) in let branch ibt ibf = If_cons (ibt, ibf) in
merge_branches loc btr bfr { branch } merge_branches loc btr bfr { branch }
| Prim (loc, "iter", []), | Prim (loc, "iter", []),
@ -893,14 +895,14 @@ and parse_instr
return (Typed (Nop, stack)) return (Typed (Nop, stack))
| Seq (_, [ single ]), | Seq (_, [ single ]),
stack -> stack ->
parse_instr ?storage_type ctxt single stack parse_instr ?log ?storage_type ctxt single stack
| Seq (loc, hd :: tl), | Seq (loc, hd :: tl),
stack -> stack ->
parse_instr ?storage_type ctxt hd stack >>=? begin function parse_instr ?log ?storage_type ctxt hd stack >>=? begin function
| Failed _ -> | Failed _ ->
fail (Fail_not_in_tail_position loc) fail (Fail_not_in_tail_position loc)
| Typed (ihd, trans) -> | Typed (ihd, trans) ->
parse_instr ?storage_type ctxt (Seq (loc, tl)) trans >>=? function parse_instr ?log ?storage_type ctxt (Seq (loc, tl)) trans >>=? function
| Failed { instr } -> | Failed { instr } ->
let instr ret = Seq (ihd, instr ret) in let instr ret = Seq (ihd, instr ret) in
return (Failed { instr }) return (Failed { instr })
@ -911,14 +913,14 @@ and parse_instr
Item_t (Bool_t, rest) -> Item_t (Bool_t, rest) ->
expect_sequence_parameter loc Instr "if" 0 bt >>=? fun () -> expect_sequence_parameter loc Instr "if" 0 bt >>=? fun () ->
expect_sequence_parameter loc Instr "if" 1 bf >>=? fun () -> expect_sequence_parameter loc Instr "if" 1 bf >>=? fun () ->
parse_instr ?storage_type ctxt bt rest >>=? fun btr -> parse_instr ?log ?storage_type ctxt bt rest >>=? fun btr ->
parse_instr ?storage_type ctxt bf rest >>=? fun bfr -> parse_instr ?log ?storage_type ctxt bf rest >>=? fun bfr ->
let branch ibt ibf = If (ibt, ibf) in let branch ibt ibf = If (ibt, ibf) in
merge_branches loc btr bfr { branch } merge_branches loc btr bfr { branch }
| Prim (loc, "loop", [ body ]), | Prim (loc, "loop", [ body ]),
(Item_t (Bool_t, rest) as stack) -> (Item_t (Bool_t, rest) as stack) ->
expect_sequence_parameter loc Instr "loop" 0 body >>=? fun () -> expect_sequence_parameter loc Instr "loop" 0 body >>=? fun () ->
parse_instr ?storage_type ctxt body rest >>=? begin function parse_instr ?log ?storage_type ctxt body rest >>=? begin function
| Typed (ibody, aftbody) -> | Typed (ibody, aftbody) ->
trace trace
(Unmatched_branches (loc, Stack_ty aftbody, Stack_ty stack)) (Unmatched_branches (loc, Stack_ty aftbody, Stack_ty stack))
@ -933,7 +935,7 @@ and parse_instr
parse_ty arg >>=? fun (Ex arg) -> parse_ty arg >>=? fun (Ex arg) ->
parse_ty ret >>=? fun (Ex ret) -> parse_ty ret >>=? fun (Ex ret) ->
expect_sequence_parameter loc Instr "lambda" 2 code >>=? fun () -> expect_sequence_parameter loc Instr "lambda" 2 code >>=? fun () ->
parse_lambda ctxt arg ret code >>=? fun lambda -> parse_lambda ctxt ?log arg ret code >>=? fun lambda ->
return (Typed (Lambda lambda, Item_t (Lambda_t (arg, ret), stack))) return (Typed (Lambda lambda, Item_t (Lambda_t (arg, ret), stack)))
| Prim (loc, "exec", []), | Prim (loc, "exec", []),
Item_t (arg, Item_t (Lambda_t (param, ret), rest)) -> Item_t (arg, Item_t (Lambda_t (param, ret), rest)) ->
@ -942,7 +944,7 @@ and parse_instr
| Prim (loc, "dip", [ code ]), | Prim (loc, "dip", [ code ]),
Item_t (v, rest) -> Item_t (v, rest) ->
expect_sequence_parameter loc Instr "dip" 0 code >>=? fun () -> expect_sequence_parameter loc Instr "dip" 0 code >>=? fun () ->
parse_instr ctxt code rest >>=? begin function parse_instr ?log ctxt code rest >>=? begin function
| Typed (instr, aft_rest) -> | Typed (instr, aft_rest) ->
return (Typed (Dip instr, Item_t (v, aft_rest))) return (Typed (Dip instr, Item_t (v, aft_rest)))
| Failed _ -> | Failed _ ->
@ -958,7 +960,9 @@ and parse_instr
(* timestamp operations *) (* timestamp operations *)
| Prim (loc, "add", []), | Prim (loc, "add", []),
Item_t (Timestamp_t, Item_t (Int_t kind, rest)) -> Item_t (Timestamp_t, Item_t (Int_t kind, rest)) ->
trace (Bad_stack_item (loc, 2)) (Lwt.return (unsigned_int_kind kind)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 2))
(Lwt.return (unsigned_int_kind kind)) >>=? fun (Eq _) ->
return (Typed (Add_timestamp_to_seconds (kind, loc), Item_t (Timestamp_t, rest))) return (Typed (Add_timestamp_to_seconds (kind, loc), Item_t (Timestamp_t, rest)))
| Prim (loc, "add", []), | Prim (loc, "add", []),
Item_t (Int_t kind, Item_t (Timestamp_t, rest)) -> Item_t (Int_t kind, Item_t (Timestamp_t, rest)) ->
@ -979,7 +983,9 @@ and parse_instr
return (Typed (Sub_tez, Item_t (Tez_t, rest))) return (Typed (Sub_tez, Item_t (Tez_t, rest)))
| Prim (loc, "mul", []), | Prim (loc, "mul", []),
Item_t (Tez_t, Item_t (Int_t kind, rest)) -> Item_t (Tez_t, Item_t (Int_t kind, rest)) ->
trace (Bad_stack_item (loc, 2)) (Lwt.return (unsigned_int_kind kind)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 2))
(Lwt.return (unsigned_int_kind kind)) >>=? fun (Eq _) ->
return (Typed (Mul_tez kind, Item_t (Tez_t, rest))) return (Typed (Mul_tez kind, Item_t (Tez_t, rest)))
| Prim (loc, "mul", []), | Prim (loc, "mul", []),
Item_t (Int_t kind, Item_t (Tez_t, rest)) -> Item_t (Int_t kind, Item_t (Tez_t, rest)) ->
@ -1003,83 +1009,127 @@ and parse_instr
(* integer operations *) (* integer operations *)
| Prim (loc, "checked_abs", []), | Prim (loc, "checked_abs", []),
Item_t (Int_t k, rest) -> Item_t (Int_t k, rest) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (signed_int_kind k)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 1))
(Lwt.return (signed_int_kind k)) >>=? fun (Eq _) ->
return (Typed (Checked_abs_int (k, loc), Item_t (Int_t k, rest))) return (Typed (Checked_abs_int (k, loc), Item_t (Int_t k, rest)))
| Prim (loc, "checked_neg", []), | Prim (loc, "checked_neg", []),
Item_t (Int_t k, rest) -> Item_t (Int_t k, rest) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (signed_int_kind k)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 1))
(Lwt.return (signed_int_kind k)) >>=? fun (Eq _) ->
return (Typed (Checked_neg_int (k, loc), Item_t (Int_t k, rest))) return (Typed (Checked_neg_int (k, loc), Item_t (Int_t k, rest)))
| Prim (loc, "checked_add", []), | Prim (loc, "checked_add", []),
Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 1))
(Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
return (Typed (Checked_add_int (kl, loc), Item_t (Int_t kl, rest))) return (Typed (Checked_add_int (kl, loc), Item_t (Int_t kl, rest)))
| Prim (loc, "checked_sub", []), | Prim (loc, "checked_sub", []),
Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 1))
(Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
return (Typed (Checked_sub_int (kl, loc), Item_t (Int_t kl, rest))) return (Typed (Checked_sub_int (kl, loc), Item_t (Int_t kl, rest)))
| Prim (loc, "checked_mul", []), | Prim (loc, "checked_mul", []),
Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 1))
(Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
return (Typed (Checked_mul_int (kl, loc), Item_t (Int_t kl, rest))) return (Typed (Checked_mul_int (kl, loc), Item_t (Int_t kl, rest)))
| Prim (loc, "abs", []), | Prim (loc, "abs", []),
Item_t (Int_t k, rest) -> Item_t (Int_t k, rest) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (signed_int_kind k)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 1))
(Lwt.return (signed_int_kind k)) >>=? fun (Eq _) ->
return (Typed (Abs_int k, Item_t (Int_t k, rest))) return (Typed (Abs_int k, Item_t (Int_t k, rest)))
| Prim (loc, "neg", []), | Prim (loc, "neg", []),
Item_t (Int_t k, rest) -> Item_t (Int_t k, rest) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (signed_int_kind k)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 1))
(Lwt.return (signed_int_kind k)) >>=? fun (Eq _) ->
return (Typed (Neg_int k, Item_t (Int_t k, rest))) return (Typed (Neg_int k, Item_t (Int_t k, rest)))
| Prim (loc, "add", []), | Prim (loc, "add", []),
Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 1))
(Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
return (Typed (Add_int kl, Item_t (Int_t kl, rest))) return (Typed (Add_int kl, Item_t (Int_t kl, rest)))
| Prim (loc, "sub", []), | Prim (loc, "sub", []),
Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 1))
(Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
return (Typed (Sub_int kl, Item_t (Int_t kl, rest))) return (Typed (Sub_int kl, Item_t (Int_t kl, rest)))
| Prim (loc, "mul", []), | Prim (loc, "mul", []),
Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 1))
(Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
return (Typed (Mul_int kl, Item_t (Int_t kl, rest))) return (Typed (Mul_int kl, Item_t (Int_t kl, rest)))
| Prim (loc, "div", []), | Prim (loc, "div", []),
Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 1))
(Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
return (Typed (Div_int (kl, loc), Item_t (Int_t kl, rest))) return (Typed (Div_int (kl, loc), Item_t (Int_t kl, rest)))
| Prim (loc, "mod", []), | Prim (loc, "mod", []),
Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 1))
(Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
return (Typed (Mod_int (kl, loc), Item_t (Int_t kl, rest))) return (Typed (Mod_int (kl, loc), Item_t (Int_t kl, rest)))
| Prim (loc, "lsl", []), | Prim (loc, "lsl", []),
Item_t (Int_t k, Item_t (Int_t Uint8, rest)) -> Item_t (Int_t k, Item_t (Int_t Uint8, rest)) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (unsigned_int_kind k)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 1))
(Lwt.return (unsigned_int_kind k)) >>=? fun (Eq _) ->
return (Typed (Lsl_int k, Item_t (Int_t k, rest))) return (Typed (Lsl_int k, Item_t (Int_t k, rest)))
| Prim (loc, "lsr", []), | Prim (loc, "lsr", []),
Item_t (Int_t k, Item_t (Int_t Uint8, rest)) -> Item_t (Int_t k, Item_t (Int_t Uint8, rest)) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (unsigned_int_kind k)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 1))
(Lwt.return (unsigned_int_kind k)) >>=? fun (Eq _) ->
return (Typed (Lsr_int k, Item_t (Int_t k, rest))) return (Typed (Lsr_int k, Item_t (Int_t k, rest)))
| Prim (loc, "or", []), | Prim (loc, "or", []),
Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (unsigned_int_kind kl)) >>=? fun (Eq _) -> trace
trace (Bad_stack_item (loc, 2)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) -> (Bad_stack_item (loc, 1))
(Lwt.return (unsigned_int_kind kl)) >>=? fun (Eq _) ->
trace
(Bad_stack_item (loc, 2))
(Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
return (Typed (Or_int kl, Item_t (Int_t kl, rest))) return (Typed (Or_int kl, Item_t (Int_t kl, rest)))
| Prim (loc, "and", []), | Prim (loc, "and", []),
Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (unsigned_int_kind kl)) >>=? fun (Eq _) -> trace
trace (Bad_stack_item (loc, 2)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) -> (Bad_stack_item (loc, 1))
(Lwt.return (unsigned_int_kind kl)) >>=? fun (Eq _) ->
trace
(Bad_stack_item (loc, 2))
(Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
return (Typed (And_int kl, Item_t (Int_t kl, rest))) return (Typed (And_int kl, Item_t (Int_t kl, rest)))
| Prim (loc, "xor", []), | Prim (loc, "xor", []),
Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (unsigned_int_kind kl)) >>=? fun (Eq _) -> trace
trace (Bad_stack_item (loc, 2)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) -> (Bad_stack_item (loc, 1))
(Lwt.return (unsigned_int_kind kl)) >>=? fun (Eq _) ->
trace
(Bad_stack_item (loc, 2))
(Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
return (Typed (Xor_int kl, Item_t (Int_t kl, rest))) return (Typed (Xor_int kl, Item_t (Int_t kl, rest)))
| Prim (loc, "not", []), | Prim (loc, "not", []),
Item_t (Int_t k, rest) -> Item_t (Int_t k, rest) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (unsigned_int_kind k)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 1))
(Lwt.return (unsigned_int_kind k)) >>=? fun (Eq _) ->
return (Typed (Not_int k, Item_t (Int_t k, rest))) return (Typed (Not_int k, Item_t (Int_t k, rest)))
(* comparison *) (* comparison *)
| Prim (loc, "compare", []), | Prim (loc, "compare", []),
Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) -> trace
(Bad_stack_item (loc, 1))
(Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
return (Typed (Compare (Int_key kl), Item_t (Int_t Int64, rest))) return (Typed (Compare (Int_key kl), Item_t (Int_t Int64, rest)))
| Prim (_, "compare", []), | Prim (_, "compare", []),
Item_t (Bool_t, Item_t (Bool_t, rest)) -> Item_t (Bool_t, Item_t (Bool_t, rest)) ->
@ -1121,7 +1171,8 @@ and parse_instr
parse_ty t >>=? fun (Ex ty) -> begin match ty, stack with parse_ty t >>=? fun (Ex ty) -> begin match ty, stack with
| Int_t kt, | Int_t kt,
Item_t (Int_t kf, rest) -> Item_t (Int_t kf, rest) ->
return (Typed (Checked_int_of_int (kf, kt, loc), Item_t (Int_t kt, rest))) return (Typed (Checked_int_of_int (kf, kt, loc),
Item_t (Int_t kt, rest)))
| ty, Item_t (ty', _) -> | ty, Item_t (ty', _) ->
fail (Undefined_cast (loc, Ty ty', Ty ty)) fail (Undefined_cast (loc, Ty ty', Ty ty))
| _, Empty_t -> | _, Empty_t ->
@ -1131,7 +1182,8 @@ and parse_instr
stack -> stack ->
parse_ty t >>=? fun (Ex ty) -> begin match ty, stack with parse_ty t >>=? fun (Ex ty) -> begin match ty, stack with
| Int_t kt, Item_t (Int_t kf, rest) -> | Int_t kt, Item_t (Int_t kf, rest) ->
return (Typed (Int_of_int (kf, kt), Item_t (Int_t kt, rest))) return (Typed (Int_of_int (kf, kt),
Item_t (Int_t kt, rest)))
| ty, Item_t (ty', _) -> | ty, Item_t (ty', _) ->
fail (Undefined_cast (loc, Ty ty', Ty ty)) fail (Undefined_cast (loc, Ty ty', Ty ty))
| _, Empty_t -> | _, Empty_t ->
@ -1150,7 +1202,8 @@ and parse_instr
begin match storage_type with begin match storage_type with
| Some storage_type -> | Some storage_type ->
check_item_ty storage storage_type loc 3 >>=? fun (Eq _) -> check_item_ty storage storage_type loc 3 >>=? fun (Eq _) ->
return (Typed (Transfer_tokens (storage, loc), Item_t (cr, Item_t (storage, Empty_t)))) return (Typed (Transfer_tokens (storage, loc),
Item_t (cr, Item_t (storage, Empty_t))))
| None -> | None ->
fail (Transfer_in_lambda loc) fail (Transfer_in_lambda loc)
end end
@ -1160,7 +1213,8 @@ and parse_instr
(Option_t Key_t, Item_t (Option_t Key_t, Item_t
(Bool_t, Item_t (Bool_t, Item_t
(Tez_t, rest)))) -> (Tez_t, rest)))) ->
return (Typed (Create_account, Item_t (Contract_t (Void_t, Void_t), rest))) return (Typed (Create_account,
Item_t (Contract_t (Void_t, Void_t), rest)))
| Prim (loc, "create_contract", []), | Prim (loc, "create_contract", []),
Item_t Item_t
(Key_t, Item_t (Key_t, Item_t
@ -1225,7 +1279,8 @@ and parse_instr
| "empty_map" | "if" | "source" | "empty_map" | "if" | "source"
as name), ([] | [ _ ] | _ :: _ :: _ :: _ as l)), _ -> as name), ([] | [ _ ] | _ :: _ :: _ :: _ as l)), _ ->
fail (Invalid_arity (loc, Instr, name, 2, List.length l)) fail (Invalid_arity (loc, Instr, name, 2, List.length l))
| Prim (loc, "lambda", ([] | [ _ ] | [ _; _ ] | _ :: _ :: _ :: _ :: _ as l)), _ -> | Prim (loc, "lambda", ([] | [ _ ] | [ _; _ ]
| _ :: _ :: _ :: _ :: _ as l)), _ ->
fail (Invalid_arity (loc, Instr, "lambda", 3, List.length l)) fail (Invalid_arity (loc, Instr, "lambda", 3, List.length l))
(* Stack errors *) (* Stack errors *)
| Prim (loc, ("add" | "sub" | "mul" | "div" | "mod" | Prim (loc, ("add" | "sub" | "mul" | "div" | "mod"
@ -1273,6 +1328,13 @@ and parse_instr
fail @@ Invalid_primitive (loc, Instr, prim) fail @@ Invalid_primitive (loc, Instr, prim)
| (Int (loc, _) | String (loc, _)), _ -> | (Int (loc, _) | String (loc, _)), _ ->
fail @@ Invalid_expression_kind loc fail @@ Invalid_expression_kind loc
end >>=? fun judgement ->
begin match judgement, script_instr, log with
| Typed (_, after_ty), Prim (loc, _, _), Some log ->
log loc (Stack_ty stack_ty, Stack_ty after_ty)
| _ -> ()
end ;
return judgement
and parse_contract and parse_contract
: type arg ret. context -> arg ty -> ret ty -> Script.location -> Contract.t -> : type arg ret. context -> arg ty -> ret ty -> Script.location -> Contract.t ->
@ -1522,16 +1584,36 @@ let parse_script
parse_lambda ctxt ~storage_type arg_type_full ret_type_full code >>=? fun code -> parse_lambda ctxt ~storage_type arg_type_full ret_type_full code >>=? fun code ->
return (Ex { code; arg_type; ret_type; storage; storage_type }) return (Ex { code; arg_type; ret_type; storage; storage_type })
type type_map =
(int * (Script.expr list * Script.expr list)) list
let type_map_enc =
let open Data_encoding in
list
(tup2
int31
(tup2
(list Script.expr_encoding)
(list Script.expr_encoding)))
let typecheck_code let typecheck_code
: context -> Script.code -> unit tzresult Lwt.t : context -> Script.code -> type_map tzresult Lwt.t
= fun ctxt { code; arg_type; ret_type; storage_type } -> = fun ctxt { code; arg_type; ret_type; storage_type } ->
parse_ty arg_type >>=? fun (Ex arg_type) -> parse_ty arg_type >>=? fun (Ex arg_type) ->
parse_ty ret_type >>=? fun (Ex ret_type) -> parse_ty ret_type >>=? fun (Ex ret_type) ->
parse_ty storage_type >>=? fun (Ex storage_type) -> parse_ty storage_type >>=? fun (Ex storage_type) ->
let arg_type_full = Pair_t (Pair_t (Tez_t, arg_type), storage_type) in let arg_type_full = Pair_t (Pair_t (Tez_t, arg_type), storage_type) in
let ret_type_full = Pair_t (ret_type, storage_type) in let ret_type_full = Pair_t (ret_type, storage_type) in
parse_lambda ctxt ~storage_type arg_type_full ret_type_full code >>=? fun _ -> let result = ref [] in
return () let log loc (Stack_ty before, Stack_ty after) =
let rec unparse_stack
: type a. a stack_ty -> Script.expr list
= function
| Empty_t -> []
| Item_t (ty, rest) -> unparse_ty ty :: unparse_stack rest in
result := (loc, (unparse_stack before, unparse_stack after)) :: !result in
parse_lambda ctxt ~log ~storage_type arg_type_full ret_type_full code >>=? fun _ ->
return !result
let typecheck_tagged_data let typecheck_tagged_data
: context -> Script.expr -> unit tzresult Lwt.t : context -> Script.expr -> unit tzresult Lwt.t

View File

@ -92,7 +92,7 @@ let update_locations ir =
(narg :: nargs, ni)) (narg :: nargs, ni))
([], succ i) args in ([], succ i) args in
(Seq (i, List.rev nargs), ni) in (Seq (i, List.rev nargs), ni) in
fst (update_locations 0 ir) fst (update_locations 1 ir)
let expr_encoding = let expr_encoding =
Data_encoding.conv Data_encoding.conv

View File

@ -331,7 +331,7 @@ module Helpers = struct
RPC.service RPC.service
~description: "Typecheck a piece of code in the current context" ~description: "Typecheck a piece of code in the current context"
~input: Script.code_encoding ~input: Script.code_encoding
~output: (wrap_tzerror empty) ~output: (wrap_tzerror Script_ir_translator.type_map_enc)
RPC.Path.(custom_root / "helpers" / "typecheck_code") RPC.Path.(custom_root / "helpers" / "typecheck_code")
let typecheck_tagged_data custom_root = let typecheck_tagged_data custom_root =