Michelson: Propagate and check annotations

This commit is contained in:
Milo Davis 2017-10-18 13:46:16 +02:00 committed by Benjamin Canou
parent b22f02868f
commit c387ed823a
13 changed files with 774 additions and 542 deletions

View File

@ -469,22 +469,26 @@ If `DO-NOT-OVERWRITE' is non-nil, the existing contents of the buffer are mainta
(defun michelson-format-stack-top (bef-ele aft-ele width) (defun michelson-format-stack-top (bef-ele aft-ele width)
(lexical-let* (lexical-let*
((pp-no-trailing-newline (lambda (sexp) ((pp-no-trailing-newline
(let* ((str (pp-to-string sexp)) (lambda (sexp)
(len (length str))) (let* ((str (pp-to-string sexp))
(if (equal "\n" (substring str (- len 1) len)) (len (length str)))
(substring str 0 (- len 1)) (if (equal "\n" (substring str (- len 1) len))
str)))) (substring str 0 (- len 1))
str))))
(bef-strs (if bef-ele (split-string (funcall pp-no-trailing-newline bef-ele) "\n") '(""))) (bef-strs (if bef-ele (split-string (funcall pp-no-trailing-newline bef-ele) "\n") '("")))
(aft-strs (if aft-ele (split-string (funcall pp-no-trailing-newline aft-ele) "\n") '(""))) (aft-strs (if aft-ele (split-string (funcall pp-no-trailing-newline aft-ele) "\n") '("")))
(width width)) (width width))
(letrec ((format-strings (letrec ((format-strings
(lambda (befs afts) (lambda (befs afts)
(if (or befs afts) (if (or befs afts)
(concat (format (format "%%-%ds| %%s\n" (/ width 2)) (let ((aft-stack (if afts (car afts) "")))
(if befs (car befs) "") (concat (format (format "%%-%ds|%s%%s\n"
(if afts (car afts) "")) (/ width 2)
(funcall format-strings (cdr befs) (cdr afts))) (if (equal aft-stack "") "" " "))
(if befs (car befs) "")
aft-stack)
(funcall format-strings (cdr befs) (cdr afts))))
"")))) ""))))
(funcall format-strings bef-strs aft-strs)))) (funcall format-strings bef-strs aft-strs))))

View File

@ -10,17 +10,24 @@
open Micheline open Micheline
let print_expr ppf expr = let print_expr ppf expr =
let print_annot ppf = function
| None -> ()
| Some annot -> Format.fprintf ppf " %s" annot in
let rec print_expr ppf = function let rec print_expr ppf = function
| Int (_, value) -> Format.fprintf ppf "%s" value | Int (_, value) -> Format.fprintf ppf "%s" value
| String (_, value) -> Micheline_printer.print_string ppf value | String (_, value) -> Micheline_printer.print_string ppf value
| Seq (_, items, _) -> | Seq (_, items, annot) ->
Format.fprintf ppf "(seq %a)" Format.fprintf ppf "(seq%a %a)"
print_annot annot
(Format.pp_print_list ~pp_sep:Format.pp_print_space print_expr) (Format.pp_print_list ~pp_sep:Format.pp_print_space print_expr)
items items
| Prim (_, name, [], _) -> | Prim (_, name, [], None) ->
Format.fprintf ppf "%s" name Format.fprintf ppf "%s" name
| Prim (_, name, items, _) -> | Prim (_, name, items, annot) ->
Format.fprintf ppf "(%s %a)" name Format.fprintf ppf "(%s%a%s%a)"
name
print_annot annot
(if items = [] then "" else " ")
(Format.pp_print_list ~pp_sep:Format.pp_print_space print_expr) items in (Format.pp_print_list ~pp_sep:Format.pp_print_space print_expr) items in
let root = root (Michelson_v1_primitives.strings_of_prims expr) in let root = root (Michelson_v1_primitives.strings_of_prims expr) in
Format.fprintf ppf "@[<h>%a@]" print_expr root Format.fprintf ppf "@[<h>%a@]" print_expr root
@ -59,6 +66,8 @@ let print_type_map ppf (parsed, type_map) =
let first_error_location errs = let first_error_location errs =
let rec find = function let rec find = function
| [] -> 0 | [] -> 0
| Inconsistent_type_annotations (loc, _, _) :: _
| Unexpected_annotation loc :: _
| Ill_formed_type (_, _, loc) :: _ | Ill_formed_type (_, _, loc) :: _
| Invalid_arity (loc, _, _, _) :: _ | Invalid_arity (loc, _, _, _) :: _
| Invalid_namespace (loc, _, _, _) :: _ | Invalid_namespace (loc, _, _, _) :: _

View File

@ -12,28 +12,24 @@ open Script_ir_translator
open Script_interpreter open Script_interpreter
open Michelson_v1_printer open Michelson_v1_printer
let print_ty (type t) ppf (ty : t ty) = let print_ty (type t) ppf (annot, (ty : t ty)) =
unparse_ty ty unparse_ty annot ty
|> Micheline.strip_locations |> Micheline.strip_locations
|> Michelson_v1_printer.print_expr ppf |> Michelson_v1_printer.print_expr_unwrapped ppf
let rec print_stack_ty (type t) ?(depth = max_int) ppf (s : t stack_ty) = let rec print_stack_ty (type t) ?(depth = max_int) ppf (s : t stack_ty) =
let print_ty (type t) ppf (ty : t ty) =
unparse_ty ty
|> Micheline.strip_locations
|> Michelson_v1_printer.print_expr_unwrapped ppf in
let rec loop let rec loop
: type t. int -> Format.formatter -> t stack_ty -> unit : type t. int -> Format.formatter -> t stack_ty -> unit
= fun depth ppf -> function = fun depth ppf -> function
| Empty_t -> () | Empty_t -> ()
| _ when depth <= 0 -> | _ when depth <= 0 ->
Format.fprintf ppf "..." Format.fprintf ppf "..."
| Item_t (last, Empty_t) -> | Item_t (last, Empty_t, annot) ->
Format.fprintf ppf "%a" Format.fprintf ppf "%a"
print_ty last print_ty (annot, last)
| Item_t (last, rest) -> | Item_t (last, rest, annot) ->
Format.fprintf ppf "%a :@ %a" Format.fprintf ppf "%a :@ %a"
print_ty last (loop (depth - 1)) rest in print_ty (annot, last) (loop (depth - 1)) rest in
match s with match s with
| Empty_t -> | Empty_t ->
Format.fprintf ppf "[]" Format.fprintf ppf "[]"
@ -59,6 +55,8 @@ let collect_error_locations errs =
| Ill_typed_contract (_, _)) :: _ | Ill_typed_contract (_, _)) :: _
| [] -> acc | [] -> acc
| (Invalid_arity (loc, _, _, _) | (Invalid_arity (loc, _, _, _)
| Inconsistent_type_annotations (loc, _, _)
| Unexpected_annotation loc
| Invalid_namespace (loc, _, _, _) | Invalid_namespace (loc, _, _, _)
| Invalid_primitive (loc, _, _) | Invalid_primitive (loc, _, _)
| Invalid_kind (loc, _, _) | Invalid_kind (loc, _, _)
@ -120,7 +118,7 @@ let report_errors ~details ~show_source ?parsed ppf errs =
| Some s -> Format.fprintf ppf "%s " s) | Some s -> Format.fprintf ppf "%s " s)
name name
print_source (parsed, hilights) print_source (parsed, hilights)
print_ty ty ; print_ty (None, ty) ;
if rest <> [] then Format.fprintf ppf "@," ; if rest <> [] then Format.fprintf ppf "@," ;
print_trace (parsed_locations parsed) rest print_trace (parsed_locations parsed) rest
| Ill_formed_type (_, expr, loc) :: rest -> | Ill_formed_type (_, expr, loc) :: rest ->
@ -256,21 +254,21 @@ let report_errors ~details ~show_source ?parsed ppf errs =
@[<hov 2>and@ %a.@]@]" @[<hov 2>and@ %a.@]@]"
print_loc loc print_loc loc
(Michelson_v1_primitives.string_of_prim name) (Michelson_v1_primitives.string_of_prim name)
print_ty tya print_ty (None, tya)
print_ty tyb print_ty (None, tyb)
| Undefined_unop (loc, name, ty) -> | Undefined_unop (loc, name, ty) ->
Format.fprintf ppf Format.fprintf ppf
"@[<hov 0>@[<hov 2>%aoperator %s is undefined on@ %a@]@]" "@[<hov 0>@[<hov 2>%aoperator %s is undefined on@ %a@]@]"
print_loc loc print_loc loc
(Michelson_v1_primitives.string_of_prim name) (Michelson_v1_primitives.string_of_prim name)
print_ty ty print_ty (None, ty)
| Bad_return (loc, got, exp) -> | Bad_return (loc, got, exp) ->
Format.fprintf ppf Format.fprintf ppf
"@[<v 2>%awrong stack type at end of body:@,\ "@[<v 2>%awrong stack type at end of body:@,\
- @[<v 0>expected return stack type:@ %a,@]@,\ - @[<v 0>expected return stack type:@ %a,@]@,\
- @[<v 0>actual stack type:@ %a.@]@]" - @[<v 0>actual stack type:@ %a.@]@]"
print_loc loc print_loc loc
(fun ppf -> print_stack_ty ppf) (Item_t (exp, Empty_t)) (fun ppf -> print_stack_ty ppf) (Item_t (exp, Empty_t, None))
(fun ppf -> print_stack_ty ppf) got (fun ppf -> print_stack_ty ppf) got
| Bad_stack (loc, name, depth, sty) -> | Bad_stack (loc, name, depth, sty) ->
Format.fprintf ppf Format.fprintf ppf
@ -286,6 +284,24 @@ let report_errors ~details ~show_source ?parsed ppf errs =
print_loc loc print_loc loc
(fun ppf -> print_stack_ty ppf) sta (fun ppf -> print_stack_ty ppf) sta
(fun ppf -> print_stack_ty ppf) stb (fun ppf -> print_stack_ty ppf) stb
| Inconsistent_annotations (annot1, annot2) ->
Format.fprintf ppf
"@[<v 2>The two annotations do not match:@,\
- @[<hov>%s@]@,\
- @[<hov>%s@]"
annot1 annot2
| Inconsistent_type_annotations (loc, ty1, ty2) ->
Format.fprintf ppf
"@[<v 2>%athe two types contain incompatible annotations:@,\
- @[<hov>%a@]@,\
- @[<hov>%a@]"
print_loc loc
print_ty (None, ty1)
print_ty (None, ty2)
| Unexpected_annotation loc ->
Format.fprintf ppf
"@[<v 2>%aunexpected annotation."
print_loc loc
| Transfer_in_lambda loc -> | Transfer_in_lambda loc ->
Format.fprintf ppf Format.fprintf ppf
"%aThe TRANSFER_TOKENS instruction cannot appear in a lambda." "%aThe TRANSFER_TOKENS instruction cannot appear in a lambda."
@ -307,7 +323,7 @@ let report_errors ~details ~show_source ?parsed ppf errs =
@[<hov 2>is invalid for type@ %a.@]@]" @[<hov 2>is invalid for type@ %a.@]@]"
print_loc loc print_loc loc
print_expr got print_expr got
print_ty exp print_ty (None, exp)
| Invalid_contract (loc, contract) -> | Invalid_contract (loc, contract) ->
Format.fprintf ppf Format.fprintf ppf
"%ainvalid contract %a." "%ainvalid contract %a."
@ -316,12 +332,13 @@ let report_errors ~details ~show_source ?parsed ppf errs =
Format.fprintf ppf "%acomparable type expected." Format.fprintf ppf "%acomparable type expected."
print_loc loc ; print_loc loc ;
Format.fprintf ppf "@[<hov 0>@[<hov 2>Type@ %a@]@ is not comparable.@]" Format.fprintf ppf "@[<hov 0>@[<hov 2>Type@ %a@]@ is not comparable.@]"
print_ty ty print_ty (None, ty)
| Inconsistent_types (tya, tyb) -> | Inconsistent_types (tya, tyb) ->
Format.fprintf ppf Format.fprintf ppf
"@[<hov 0>@[<hov 2>Type@ %a@]@ \ "@[<hov 0>@[<hov 2>Type@ %a@]@ \
@[<hov 2>is not compatible with type@ %a.@]@]" @[<hov 2>is not compatible with type@ %a.@]@]"
print_ty tya print_ty tyb print_ty (None, tya)
print_ty (None, tyb)
| Reject _ -> Format.fprintf ppf "Script reached FAIL instruction" | Reject _ -> Format.fprintf ppf "Script reached FAIL instruction"
| Overflow _ -> Format.fprintf ppf "Unexpected arithmetic overflow" | Overflow _ -> Format.fprintf ppf "Unexpected arithmetic overflow"
| err -> | err ->

View File

@ -303,6 +303,21 @@ type provided by the programmer, and checking that the resulting
symbolic stack is consistent with the expected result, also provided symbolic stack is consistent with the expected result, also provided
by the programmer. by the programmer.
### Annotations
All instructions in the language can optionally take an annotation.
Annotations allow you to specify additional information about data
or pair and union types.
At join points in the program
(`IF`, `IF_LEFT`, `IF_CONS`, `IF_NONE`, `LOOP`), annotations must be compatible.
Annotations are compatible if both elements are annotated with the same annotation
or if at least one of the values/types is unannotated.
An instruction that carries an annotation places an annotation on the top item in the stack.
Stack visualization tools like the Michelson's Emacs mode print annotations
as associated with each type.
This is useful as a debugging aid.
### Side note ### Side note
As with most type systems, it is incomplete. There are programs that As with most type systems, it is incomplete. There are programs that

View File

@ -67,7 +67,7 @@ let rec unparse_stack
: type a. a stack * a stack_ty -> Script.expr list : type a. a stack * a stack_ty -> Script.expr list
= function = function
| Empty, Empty_t -> [] | Empty, Empty_t -> []
| Item (v, rest), Item_t (ty, rest_ty) -> | Item (v, rest), Item_t (ty, rest_ty, _) ->
Micheline.strip_locations (unparse_data ty v) :: unparse_stack (rest, rest_ty) Micheline.strip_locations (unparse_data ty v) :: unparse_stack (rest, rest_ty)
let rec interp let rec interp
@ -507,9 +507,9 @@ let rec interp
(init, rest))))))) -> (init, rest))))))) ->
let code = let code =
Micheline.strip_locations Micheline.strip_locations
(Seq (0, [ Prim (0, K_parameter, [ unparse_ty p ], None) ; (Seq (0, [ Prim (0, K_parameter, [ unparse_ty None p ], None) ;
Prim (0, K_return, [ unparse_ty r ], None) ; Prim (0, K_return, [ unparse_ty None r ], None) ;
Prim (0, K_storage, [ unparse_ty g ], None) ; Prim (0, K_storage, [ unparse_ty None g ], None) ;
Prim (0, K_code, [ Micheline.root code ], None) ], None)) in Prim (0, K_code, [ Micheline.root code ], None) ], None)) in
let storage = Micheline.strip_locations (unparse_data g init) in let storage = Micheline.strip_locations (unparse_data g init) in
Contract.spend_from_script ctxt source credit >>=? fun ctxt -> Contract.spend_from_script ctxt source credit >>=? fun ctxt ->

File diff suppressed because it is too large Load Diff

View File

@ -19,10 +19,8 @@ type ex_script = Ex_script : ('a, 'b, 'c) Script_typed_ir.script -> ex_script
(* ---- Error definitions ---------------------------------------------------*) (* ---- Error definitions ---------------------------------------------------*)
(* Auxiliary types for error documentation *) (* Auxiliary types for error documentation *)
type namespace = type namespace = Type_namespace | Constant_namespace | Instr_namespace | Keyword_namespace
Type_namespace | Constant_namespace | Instr_namespace | Keyword_namespace type kind = Int_kind | String_kind | Prim_kind | Seq_kind
type kind =
Int_kind | String_kind | Prim_kind | Seq_kind
type type_map = (int * (Script.expr list * Script.expr list)) list type type_map = (int * (Script.expr list * Script.expr list)) list
(* Structure errors *) (* Structure errors *)
@ -39,6 +37,12 @@ type error += Undefined_unop : Script.location * Script.prim * _ Script_typed_ir
type error += Bad_return : Script.location * _ Script_typed_ir.stack_ty * _ Script_typed_ir.ty -> error type error += Bad_return : Script.location * _ Script_typed_ir.stack_ty * _ Script_typed_ir.ty -> error
type error += Bad_stack : Script.location * Script.prim * int * _ Script_typed_ir.stack_ty -> error type error += Bad_stack : Script.location * Script.prim * 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 += Inconsistent_annotations of string * string
type error += Inconsistent_type_annotations :
Script.location * _ Script_typed_ir.ty * _ Script_typed_ir.ty -> error
type error += Unexpected_annotation of Script.location
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 += Transfer_in_dip of Script.location
type error += Bad_stack_length type error += Bad_stack_length
@ -91,9 +95,9 @@ val unparse_data :
'a Script_typed_ir.ty -> 'a -> Script.node 'a Script_typed_ir.ty -> 'a -> Script.node
val parse_ty : val parse_ty :
Script.node -> ex_ty tzresult Script.node -> (ex_ty * Script_typed_ir.annot) tzresult
val unparse_ty : val unparse_ty :
'a Script_typed_ir.ty -> Script.node string option -> 'a Script_typed_ir.ty -> Script.node
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

View File

@ -59,6 +59,8 @@ and ('arg, 'ret) lambda =
and ('arg, 'ret) typed_contract = and ('arg, 'ret) typed_contract =
'arg ty * 'ret ty * Contract.t 'arg ty * 'ret ty * Contract.t
and annot = string option
and 'ty ty = and 'ty ty =
| Unit_t : unit ty | Unit_t : unit ty
| Int_t : z num ty | Int_t : z num ty
@ -70,8 +72,8 @@ and 'ty ty =
| Key_t : public_key ty | Key_t : public_key ty
| Timestamp_t : Script_timestamp.t ty | Timestamp_t : Script_timestamp.t ty
| Bool_t : bool ty | Bool_t : bool ty
| Pair_t : 'a ty * 'b ty -> ('a, 'b) pair ty | Pair_t : ('a ty * annot) * ('b ty * annot) -> ('a, 'b) pair ty
| Union_t : 'a ty * 'b ty -> ('a, 'b) union ty | Union_t : ('a ty * annot) * ('b ty * annot) -> ('a, 'b) union ty
| Lambda_t : 'arg ty * 'ret ty -> ('arg, 'ret) lambda ty | Lambda_t : 'arg ty * 'ret ty -> ('arg, 'ret) lambda ty
| Option_t : 'v ty -> 'v option ty | Option_t : 'v ty -> 'v option ty
| List_t : 'v ty -> 'v list ty | List_t : 'v ty -> 'v list ty
@ -80,7 +82,7 @@ and 'ty ty =
| Contract_t : 'arg ty * 'ret ty -> ('arg, 'ret) typed_contract ty | Contract_t : 'arg ty * 'ret ty -> ('arg, 'ret) typed_contract ty
and 'ty stack_ty = and 'ty stack_ty =
| Item_t : 'ty ty * 'rest stack_ty -> ('ty * 'rest) stack_ty | Item_t : 'ty ty * 'rest stack_ty * annot -> ('ty * 'rest) stack_ty
| Empty_t : end_of_stack stack_ty | Empty_t : end_of_stack stack_ty
(* ---- Instructions --------------------------------------------------------*) (* ---- Instructions --------------------------------------------------------*)
@ -323,5 +325,4 @@ and ('bef, 'aft) descr =
{ loc : Script.location ; { loc : Script.location ;
bef : 'bef stack_ty ; bef : 'bef stack_ty ;
aft : 'aft stack_ty ; aft : 'aft stack_ty ;
instr : ('bef, 'aft) instr ; instr : ('bef, 'aft) instr }
annot : string option }

View File

@ -1,4 +1,4 @@
parameter (pair bool bool); parameter (pair (bool @first) (bool @second));
return bool; return bool;
storage unit; storage unit;
code {CAR; DUP; CAR; DIP{CDR}; AND; UNIT; SWAP; PAIR}; code { CAR @param; DUP; CAR @first; DIP{CDR @second}; AND; UNIT; SWAP; PAIR };

View File

@ -1,7 +1,7 @@
parameter nat; parameter nat;
return (list nat); return (list nat);
storage unit; storage unit;
code {CAR; NIL nat; SWAP; DUP; PUSH nat 0; CMPNEQ; code { CAR @counter; NIL @acc nat; SWAP; DUP @cmp_num; PUSH nat 0; CMPNEQ;
LOOP {DUP; DIP {SWAP}; CONS; SWAP; PUSH nat 1; SWAP; SUB; LOOP { DUP; DIP {SWAP}; CONS @acc; SWAP; PUSH nat 1; SWAP; SUB @counter;
DUP; DIP{ABS} ; PUSH int 0; CMPNEQ}; DUP; DIP{ABS}; PUSH int 0; CMPNEQ};
CONS; UNIT; SWAP; PAIR}; CONS; UNIT; SWAP; PAIR};

View File

@ -1,5 +1,5 @@
parameter (list string); parameter (list string);
return (list string); return (list string);
storage unit; storage unit;
code{CAR; LAMBDA string string {PUSH string "Hello "; CONCAT}; code{ CAR; LAMBDA string string { PUSH @hello string "Hello "; CONCAT };
MAP; UNIT; SWAP; PAIR}; MAP; UNIT; SWAP; PAIR};

View File

@ -1,4 +1,4 @@
parameter unit; parameter unit;
storage tez; storage tez;
return unit; return unit;
code {DROP; AMOUNT; UNIT; PAIR}; code { DROP; AMOUNT; UNIT; PAIR };

View File

@ -1,16 +1,18 @@
# (pair signed_weather_data actual_level) # (pair signed_weather_data actual_level)
parameter (pair signature nat); parameter (pair (signature @sig) (nat @nat));
# (pair (under_key over_key) (pair weather_service_key (pair rain_level days_in_future))) # (pair (under_key over_key) (pair weather_service_key (pair rain_level days_in_future)))
storage (pair (pair (contract unit unit) (contract unit unit)) (pair nat key)); storage (pair (pair (contract @lt unit unit)
(contract @geq unit unit))
(pair nat key));
return unit; return unit;
code {DUP; DUP; code { DUP; DUP;
CAR; DUP; DIP{CDR; H}; CAR; PAIR; CAR; MAP_CDR{H};
SWAP; CDDDR; CHECK_SIGNATURE; # Check if the data has been correctly signed SWAP; CDDDR; CHECK_SIGNATURE; # Check if the data has been correctly signed
IF {} {FAIL} # If signature is not correct, end the execution ASSERT; # If signature is not correct, end the execution
DUP; DUP; DUP; DIIIP{CDR}; # Place storage type on bottom of stack DUP; DUP; DUP; DIIIP{CDR}; # Place storage type on bottom of stack
DIIP{CDAR}; # Place contracts below numbers DIIP{CDAR}; # Place contracts below numbers
DIP{CADR}; # Get actual rain DIP{CADR}; # Get actual rain
CDDAR; # Get rain threshold CDDAR; # Get rain threshold
CMPLT; IF {CAR} {CDR}; # Select contract to receive tokens CMPLT; IF {CAR @lt; ANNOT @winner} {CDR @geq; ANNOT @winner}; # Select contract to receive tokens
BALANCE; UNIT; TRANSFER_TOKENS; # Setup and execute transfer BALANCE; UNIT; TRANSFER_TOKENS; # Setup and execute transfer
PAIR}; # Save storage PAIR }; # Save storage