balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Michelson: Add typechecking context

Browse Source
This commit is contained in:
Milo Davis 2017-10-10 20:22:42 +02:00
parent 370112f9b8
commit ecd861ca70
4 changed files with 61 additions and 61 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/client/embedded/alpha/client_proto_programs.ml
View File

@ -296,6 +296,7 @@ let collect_error_locations errs =
| Bad_stack (loc, _, _, _) | Bad_stack (loc, _, _, _)
| Unmatched_branches (loc, _, _) | Unmatched_branches (loc, _, _)
| Transfer_in_lambda loc | Transfer_in_lambda loc
| Transfer_in_dip loc
| Invalid_constant (loc, _, _) | Invalid_constant (loc, _, _)
| Invalid_contract (loc, _) | Invalid_contract (loc, _)
| Comparable_type_expected (loc, _) | Comparable_type_expected (loc, _)
@ -506,6 +507,10 @@ let report_errors cctxt errs =
cctxt.warning cctxt.warning
"%aThe TRANSFER_TOKENS instruction cannot appear in a lambda." "%aThe TRANSFER_TOKENS instruction cannot appear in a lambda."
print_loc loc print_loc loc
| Transfer_in_dip loc ->
cctxt.warning
"%aThe TRANSFER_TOKENS instruction cannot appear within a DIP."
print_loc loc
| Bad_stack_length -> | Bad_stack_length ->
cctxt.warning cctxt.warning
"Bad stack length." "Bad stack length."

17
src/proto/alpha/script_interpreter.ml
View File

@ -568,21 +568,12 @@ let rec interp
(* ---- contract handling ---------------------------------------------------*) (* ---- contract handling ---------------------------------------------------*)
and execute ?log origination orig source ctxt storage script amount arg qta = and execute ?log origination orig source ctxt storage script amount arg qta =
let { Script.storage ; storage_type } = storage in parse_script ctxt storage script
let { Script.code ; arg_type ; ret_type } = script in >>=? fun (Ex_script { code; arg_type; ret_type; storage; storage_type }) ->
(Lwt.return (parse_ty arg_type)) >>=? fun (Ex_ty arg_type) ->
(Lwt.return (parse_ty ret_type)) >>=? fun (Ex_ty ret_type) ->
(Lwt.return (parse_ty storage_type)) >>=? fun (Ex_ty storage_type) ->
let arg_type_full = Pair_t (arg_type, storage_type) in
let ret_type_full = Pair_t (ret_type, storage_type) in
trace
(Ill_typed_contract (code, arg_type, ret_type, storage_type, []))
(parse_lambda ~storage_type ctxt arg_type_full ret_type_full code) >>=? fun lambda ->
parse_data ctxt arg_type arg >>=? fun arg -> parse_data ctxt arg_type arg >>=? fun arg ->
parse_data ctxt storage_type storage >>=? fun storage ->
trace trace
(Runtime_contract_error (source, code, arg_type, ret_type, storage_type)) (Runtime_contract_error (source, script.code, arg_type, ret_type, storage_type))
(interp ?log origination qta orig source amount ctxt lambda (arg, storage)) (interp ?log origination qta orig source amount ctxt code (arg, storage))
>>=? fun (ret, qta, ctxt, origination) -> >>=? fun (ret, qta, ctxt, origination) ->
let ret, storage = ret in let ret, storage = ret in
return (unparse_data storage_type storage, return (unparse_data storage_type storage,

86
src/proto/alpha/script_ir_translator.ml
View File

@ -33,6 +33,7 @@ type error += Bad_return : Script.location * _ stack_ty * _ ty -> error
type error += Bad_stack : Script.location * string * int * _ stack_ty -> error type error += Bad_stack : Script.location * string * int * _ stack_ty -> error
type error += Unmatched_branches : Script.location * _ stack_ty * _ stack_ty -> error type error += Unmatched_branches : Script.location * _ stack_ty * _ stack_ty -> error
type error += Transfer_in_lambda of Script.location type error += Transfer_in_lambda of Script.location
type error += Transfer_in_dip of Script.location
type error += Bad_stack_length type error += Bad_stack_length
type error += Bad_stack_item of int type error += Bad_stack_item of int
@ -51,6 +52,19 @@ type error += Unordered_set_values of Script.location * Script.expr
type error += Duplicate_map_keys of Script.location * Script.expr type error += Duplicate_map_keys of Script.location * Script.expr
type error += Duplicate_set_values of Script.location * Script.expr type error += Duplicate_set_values of Script.location * Script.expr
type ex_comparable_ty = Ex_comparable_ty : 'a comparable_ty -> ex_comparable_ty
type ex_ty = Ex_ty : 'a ty -> ex_ty
type ex_stack_ty = Ex_stack_ty : 'a stack_ty -> ex_stack_ty
type tc_context =
| Lambda : tc_context
| Dip : 'a stack_ty -> tc_context
| Toplevel : { storage_type : 'a ty } -> tc_context
let add_dip ty = function
| Lambda | Toplevel _ -> Dip (Item_t (ty, Empty_t))
| Dip stack -> Dip (Item_t (ty, stack))
(* ---- Error helpers -------------------------------------------------------*) (* ---- Error helpers -------------------------------------------------------*)
let location = function let location = function
@ -369,7 +383,6 @@ let eq
: type t. t -> t -> (t, t) eq tzresult : type t. t -> t -> (t, t) eq tzresult
= fun ta tb -> Ok (Eq (ta, tb)) = fun ta tb -> Ok (Eq (ta, tb))
(* TODO: shall we allow operations to compare nats and ints ? *)
let comparable_ty_eq let comparable_ty_eq
: type ta tb. : type ta tb.
ta comparable_ty -> tb comparable_ty -> ta comparable_ty -> tb comparable_ty ->
@ -480,10 +493,6 @@ let merge_branches
| Failed { descr = descrt }, Typed dbf -> | Failed { descr = descrt }, Typed dbf ->
return (Typed (branch (descrt dbf.aft) dbf)) return (Typed (branch (descrt dbf.aft) dbf))
type ex_comparable_ty = Ex_comparable_ty : 'a comparable_ty -> ex_comparable_ty
type ex_ty = Ex_ty : 'a ty -> ex_ty
type ex_stack_ty = Ex_stack_ty : 'a stack_ty -> ex_stack_ty
let rec parse_comparable_ty : Script.expr -> ex_comparable_ty tzresult = function let rec parse_comparable_ty : Script.expr -> ex_comparable_ty tzresult = function
| Prim (_, "int", [], _) -> ok (Ex_comparable_ty Int_key) | Prim (_, "int", [], _) -> ok (Ex_comparable_ty Int_key)
| Prim (_, "nat", [], _) -> ok (Ex_comparable_ty Nat_key) | Prim (_, "nat", [], _) -> ok (Ex_comparable_ty Nat_key)
@ -714,7 +723,7 @@ let rec parse_data
(* Lambdas *) (* Lambdas *)
| Lambda_t (ta, tr), (Seq _ as script_instr) -> | Lambda_t (ta, tr), (Seq _ as script_instr) ->
traced @@ traced @@
parse_lambda ?type_logger ctxt ta tr script_instr parse_returning Lambda ?type_logger ctxt ta tr script_instr
| Lambda_t _, expr -> | Lambda_t _, expr ->
traced (fail (Invalid_kind (location expr, [ Seq_kind ], kind expr))) traced (fail (Invalid_kind (location expr, [ Seq_kind ], kind expr)))
(* Options *) (* Options *)
@ -793,13 +802,12 @@ and parse_comparable_data
= fun ?type_logger ctxt ty script_data -> = fun ?type_logger ctxt ty script_data ->
parse_data ?type_logger ctxt (ty_of_comparable_ty ty) script_data parse_data ?type_logger ctxt (ty_of_comparable_ty ty) script_data
and parse_lambda and parse_returning
: type arg ret storage. context -> : type arg ret. tc_context -> context ->
?storage_type: storage ty ->
?type_logger: (int * (Script.expr list * Script.expr list) -> unit) -> ?type_logger: (int * (Script.expr list * Script.expr list) -> unit) ->
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 ?type_logger arg ret script_instr -> fun tc_context ctxt ?type_logger arg ret script_instr ->
parse_instr ctxt ?storage_type ?type_logger parse_instr tc_context ctxt ?type_logger
script_instr (Item_t (arg, Empty_t)) >>=? function script_instr (Item_t (arg, Empty_t)) >>=? function
| Typed ({ loc ; aft = (Item_t (ty, Empty_t) as stack_ty) } as descr) -> | Typed ({ loc ; aft = (Item_t (ty, Empty_t) as stack_ty) } as descr) ->
trace trace
@ -812,11 +820,12 @@ and parse_lambda
return (Lam (descr (Item_t (ret, Empty_t)), script_instr) : (arg, ret) lambda) return (Lam (descr (Item_t (ret, Empty_t)), script_instr) : (arg, ret) lambda)
and parse_instr and parse_instr
: type bef storage. context -> : type bef.
?storage_type: storage ty -> tc_context ->
context ->
?type_logger: (int * (Script.expr list * Script.expr list) -> unit) -> ?type_logger: (int * (Script.expr list * Script.expr list) -> unit) ->
Script.expr -> bef stack_ty -> bef judgement tzresult Lwt.t = Script.expr -> bef stack_ty -> bef judgement tzresult Lwt.t =
fun ctxt ?storage_type ?type_logger script_instr stack_ty -> fun tc_context ctxt ?type_logger 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 check loc name n m = let check_item check loc name n m =
trace (Bad_stack (loc, name, m, stack_ty)) @@ trace (Bad_stack (loc, name, m, stack_ty)) @@
@ -861,8 +870,8 @@ and parse_instr
(Item_t (Option_t t, rest) as bef) -> (Item_t (Option_t t, rest) as bef) ->
check_kind [ Seq_kind ] bt >>=? fun () -> check_kind [ Seq_kind ] bt >>=? fun () ->
check_kind [ Seq_kind ] bf >>=? fun () -> check_kind [ Seq_kind ] bf >>=? fun () ->
parse_instr ?storage_type ?type_logger ctxt bt rest >>=? fun btr -> parse_instr ?type_logger tc_context ctxt bt rest >>=? fun btr ->
parse_instr ?storage_type ?type_logger ctxt bf (Item_t (t, rest)) >>=? fun bfr -> parse_instr ?type_logger tc_context ctxt bf (Item_t (t, rest)) >>=? fun bfr ->
let branch ibt ibf = let branch ibt ibf =
{ loc ; instr = If_none (ibt, ibf) ; bef ; aft = ibt.aft ; annot } in { loc ; instr = If_none (ibt, ibf) ; bef ; aft = ibt.aft ; annot } in
merge_branches loc btr bfr { branch } merge_branches loc btr bfr { branch }
@ -889,8 +898,8 @@ and parse_instr
(Item_t (Union_t (tl, tr), rest) as bef) -> (Item_t (Union_t (tl, tr), rest) as bef) ->
check_kind [ Seq_kind ] bt >>=? fun () -> check_kind [ Seq_kind ] bt >>=? fun () ->
check_kind [ Seq_kind ] bf >>=? fun () -> check_kind [ Seq_kind ] bf >>=? fun () ->
parse_instr ?storage_type ?type_logger ctxt bt (Item_t (tl, rest)) >>=? fun btr -> parse_instr ?type_logger tc_context ctxt bt (Item_t (tl, rest)) >>=? fun btr ->
parse_instr ?storage_type ?type_logger ctxt bf (Item_t (tr, rest)) >>=? fun bfr -> parse_instr ?type_logger tc_context ctxt bf (Item_t (tr, rest)) >>=? fun bfr ->
let branch ibt ibf = let branch ibt ibf =
{ loc ; instr = If_left (ibt, ibf) ; bef ; aft = ibt.aft ; annot } in { loc ; instr = If_left (ibt, ibf) ; bef ; aft = ibt.aft ; annot } in
merge_branches loc btr bfr { branch } merge_branches loc btr bfr { branch }
@ -907,8 +916,8 @@ and parse_instr
(Item_t (List_t t, rest) as bef) -> (Item_t (List_t t, rest) as bef) ->
check_kind [ Seq_kind ] bt >>=? fun () -> check_kind [ Seq_kind ] bt >>=? fun () ->
check_kind [ Seq_kind ] bf >>=? fun () -> check_kind [ Seq_kind ] bf >>=? fun () ->
parse_instr ?storage_type ?type_logger ctxt bt (Item_t (t, Item_t (List_t t, rest))) >>=? fun btr -> parse_instr ?type_logger tc_context ctxt bt (Item_t (t, Item_t (List_t t, rest))) >>=? fun btr ->
parse_instr ?storage_type ?type_logger ctxt bf rest >>=? fun bfr -> parse_instr ?type_logger tc_context ctxt bf rest >>=? fun bfr ->
let branch ibt ibf = let branch ibt ibf =
{ loc ; instr = If_cons (ibt, ibf) ; bef ; aft = ibt.aft ; annot } in { loc ; instr = If_cons (ibt, ibf) ; bef ; aft = ibt.aft ; annot } in
merge_branches loc btr bfr { branch } merge_branches loc btr bfr { branch }
@ -1001,10 +1010,10 @@ and parse_instr
return (typed loc annot (Nop, stack)) return (typed loc annot (Nop, stack))
| Seq (_, [ single ], None), | Seq (_, [ single ], None),
stack -> stack ->
parse_instr ?storage_type ?type_logger ctxt single stack parse_instr ?type_logger tc_context ctxt single stack
| Seq (loc, [ single ], (Some _ as annot)), | Seq (loc, [ single ], (Some _ as annot)),
stack -> stack ->
parse_instr ?storage_type ?type_logger ctxt single stack >>=? begin function parse_instr ?type_logger tc_context ctxt single stack >>=? begin function
| Typed ({ aft } as instr) -> | Typed ({ aft } as instr) ->
let nop = { bef = aft ; loc = loc ; aft ; annot = None ; instr = Nop } in let nop = { bef = aft ; loc = loc ; aft ; annot = None ; instr = Nop } in
return (typed loc annot (Seq (instr, nop), aft)) return (typed loc annot (Seq (instr, nop), aft))
@ -1017,11 +1026,11 @@ and parse_instr
end end
| Seq (loc, hd :: tl, annot), | Seq (loc, hd :: tl, annot),
stack -> stack ->
parse_instr ?storage_type ?type_logger ctxt hd stack >>=? begin function parse_instr ?type_logger tc_context ctxt hd stack >>=? begin function
| Failed _ -> | Failed _ ->
fail (Fail_not_in_tail_position loc) fail (Fail_not_in_tail_position loc)
| Typed ({ aft = middle } as ihd) -> | Typed ({ aft = middle } as ihd) ->
parse_instr ?storage_type ?type_logger ctxt (Seq (loc, tl, annot)) middle >>=? function parse_instr ?type_logger tc_context ctxt (Seq (loc, tl, annot)) middle >>=? function
| Failed { descr } -> | Failed { descr } ->
let descr ret = let descr ret =
{ loc ; instr = Seq (ihd, descr ret) ; { loc ; instr = Seq (ihd, descr ret) ;
@ -1034,15 +1043,15 @@ and parse_instr
(Item_t (Bool_t, rest) as bef) -> (Item_t (Bool_t, rest) as bef) ->
check_kind [ Seq_kind ] bt >>=? fun () -> check_kind [ Seq_kind ] bt >>=? fun () ->
check_kind [ Seq_kind ] bf >>=? fun () -> check_kind [ Seq_kind ] bf >>=? fun () ->
parse_instr ?storage_type ?type_logger ctxt bt rest >>=? fun btr -> parse_instr ?type_logger tc_context ctxt bt rest >>=? fun btr ->
parse_instr ?storage_type ?type_logger ctxt bf rest >>=? fun bfr -> parse_instr ?type_logger tc_context ctxt bf rest >>=? fun bfr ->
let branch ibt ibf = let branch ibt ibf =
{ loc ; instr = If (ibt, ibf) ; bef ; aft = ibt.aft ; annot } in { loc ; instr = If (ibt, ibf) ; bef ; aft = ibt.aft ; annot } in
merge_branches loc btr bfr { branch } merge_branches loc btr bfr { branch }
| Prim (loc, "LOOP", [ body ], annot), | Prim (loc, "LOOP", [ body ], annot),
(Item_t (Bool_t, rest) as stack) -> (Item_t (Bool_t, rest) as stack) ->
check_kind [ Seq_kind ] body >>=? fun () -> check_kind [ Seq_kind ] body >>=? fun () ->
parse_instr ?storage_type ?type_logger ctxt body rest >>=? begin function parse_instr ?type_logger tc_context ctxt body rest >>=? begin function
| Typed ibody -> | Typed ibody ->
trace trace
(Unmatched_branches (loc, ibody.aft, stack)) (Unmatched_branches (loc, ibody.aft, stack))
@ -1057,7 +1066,7 @@ and parse_instr
(Lwt.return (parse_ty arg)) >>=? fun (Ex_ty arg) -> (Lwt.return (parse_ty arg)) >>=? fun (Ex_ty arg) ->
(Lwt.return (parse_ty ret)) >>=? fun (Ex_ty ret) -> (Lwt.return (parse_ty ret)) >>=? fun (Ex_ty ret) ->
check_kind [ Seq_kind ] code >>=? fun () -> check_kind [ Seq_kind ] code >>=? fun () ->
parse_lambda ?type_logger ctxt arg ret code >>=? fun lambda -> parse_returning Lambda ?type_logger ctxt arg ret code >>=? fun lambda ->
return (typed loc annot (Lambda lambda, Item_t (Lambda_t (arg, ret), stack))) return (typed loc annot (Lambda lambda, Item_t (Lambda_t (arg, ret), stack)))
| Prim (loc, "EXEC", [], annot), | Prim (loc, "EXEC", [], annot),
Item_t (arg, Item_t (Lambda_t (param, ret), rest)) -> Item_t (arg, Item_t (Lambda_t (param, ret), rest)) ->
@ -1066,7 +1075,7 @@ and parse_instr
| Prim (loc, "DIP", [ code ], annot), | Prim (loc, "DIP", [ code ], annot),
Item_t (v, rest) -> Item_t (v, rest) ->
check_kind [ Seq_kind ] code >>=? fun () -> check_kind [ Seq_kind ] code >>=? fun () ->
parse_instr ?type_logger ctxt code rest >>=? begin function parse_instr ?type_logger (add_dip v tc_context) ctxt code rest >>=? begin function
| Typed descr -> | Typed descr ->
return (typed loc annot (Dip descr, Item_t (v, descr.aft))) return (typed loc annot (Dip descr, Item_t (v, descr.aft)))
| Failed _ -> | Failed _ ->
@ -1258,13 +1267,13 @@ and parse_instr
(Contract_t (cp, cr), Item_t (Contract_t (cp, cr), Item_t
(storage, Empty_t)))) -> (storage, Empty_t)))) ->
check_item_ty p cp loc "TRANSFER_TOKENS" 1 4 >>=? fun (Eq _) -> check_item_ty p cp loc "TRANSFER_TOKENS" 1 4 >>=? fun (Eq _) ->
begin match storage_type with begin match tc_context with
| Some storage_type -> | Dip _ -> fail (Transfer_in_dip loc)
| Lambda -> fail (Transfer_in_lambda loc)
| Toplevel { storage_type } ->
check_item_ty storage storage_type loc "TRANSFER_TOKENS" 3 4 >>=? fun (Eq _) -> check_item_ty storage storage_type loc "TRANSFER_TOKENS" 3 4 >>=? fun (Eq _) ->
return (typed loc annot (Transfer_tokens storage, return (typed loc annot (Transfer_tokens storage,
Item_t (cr, Item_t (storage, Empty_t)))) Item_t (cr, Item_t (storage, Empty_t))))
| None ->
fail (Transfer_in_lambda loc)
end end
| Prim (loc, "CREATE_ACCOUNT", [], annot), | Prim (loc, "CREATE_ACCOUNT", [], annot),
Item_t Item_t
@ -1463,7 +1472,8 @@ let parse_script
(parse_data ?type_logger ctxt storage_type storage) >>=? fun storage -> (parse_data ?type_logger ctxt storage_type storage) >>=? fun storage ->
trace trace
(Ill_typed_contract (code, arg_type, ret_type, storage_type, [])) (Ill_typed_contract (code, arg_type, ret_type, storage_type, []))
(parse_lambda ctxt ~storage_type ?type_logger arg_type_full ret_type_full code) >>=? fun code -> (parse_returning (Toplevel { storage_type }) ctxt ?type_logger arg_type_full ret_type_full code)
>>=? fun code ->
return (Ex_script { code; arg_type; ret_type; storage; storage_type }) return (Ex_script { code; arg_type; ret_type; storage; storage_type })
let type_map_enc = let type_map_enc =
@ -1571,11 +1581,11 @@ let typecheck_code
let arg_type_full = Pair_t (arg_type, storage_type) in let arg_type_full = Pair_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
let result = let result =
parse_lambda ctxt parse_returning
~storage_type (Toplevel { storage_type })
ctxt
~type_logger:(fun x -> failure_type_map := x :: !failure_type_map) ~type_logger:(fun x -> failure_type_map := x :: !failure_type_map)
arg_type_full ret_type_full arg_type_full ret_type_full code in
code in
trace trace
(Ill_typed_contract (code, arg_type, ret_type, storage_type, !failure_type_map)) (Ill_typed_contract (code, arg_type, ret_type, storage_type, !failure_type_map))
result >>=? fun (Lam (descr,_)) -> result >>=? fun (Lam (descr,_)) ->

8
src/proto/alpha/script_ir_translator.mli
View File

@ -38,6 +38,7 @@ type error += Bad_return : Script.location * _ Script_typed_ir.stack_ty * _ Scri
type error += Bad_stack : Script.location * string * int * _ Script_typed_ir.stack_ty -> error type error += Bad_stack : Script.location * string * int * _ Script_typed_ir.stack_ty -> error
type error += Unmatched_branches : Script.location * _ Script_typed_ir.stack_ty * _ Script_typed_ir.stack_ty -> error type error += Unmatched_branches : Script.location * _ Script_typed_ir.stack_ty * _ Script_typed_ir.stack_ty -> error
type error += Transfer_in_lambda of Script.location type error += Transfer_in_lambda of Script.location
type error += Transfer_in_dip of Script.location
type error += Bad_stack_length type error += Bad_stack_length
type error += Bad_stack_item of int type error += Bad_stack_item of int
@ -92,13 +93,6 @@ val parse_ty :
val unparse_ty : val unparse_ty :
'a Script_typed_ir.ty -> Script.expr 'a Script_typed_ir.ty -> Script.expr
val parse_lambda :
context ->
?storage_type:'storage Script_typed_ir.ty ->
?type_logger: (int * (Script.expr list * Script.expr list) -> unit) ->
'arg Script_typed_ir.ty -> 'ret Script_typed_ir.ty -> Script.expr ->
('arg, 'ret) Script_typed_ir.lambda tzresult Lwt.t
val type_map_enc : type_map Data_encoding.encoding val type_map_enc : type_map Data_encoding.encoding
val ex_ty_enc : ex_ty Data_encoding.encoding val ex_ty_enc : ex_ty Data_encoding.encoding