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

Michelson: annotation fixes to match the spec

Browse Source
This commit is contained in:
Alain Mebsout 2018-05-29 15:06:16 +02:00 committed by Benjamin Canou
parent c63e9b6960
commit 821c6255dc
4 changed files with 44 additions and 54 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
docs/whitedoc/michelson.rst
View File

@ -2265,8 +2265,7 @@ helps users track information in the stack for bare contracts.
For unannotated accesses with ``CAR`` and ``CDR`` to fields that are For unannotated accesses with ``CAR`` and ``CDR`` to fields that are
named will be appended (with an additional ``.`` character) to the pair named will be appended (with an additional ``.`` character) to the pair
variable annotation. If the original pair is not named in the stack, no variable annotation.
variable annotation will be inferred.
:: ::
@ -2281,6 +2280,14 @@ If fields are not named but the pair is still named in the stack then
CDAR CDAR
:: @p (pair 'a (pair 'b 'c)) : 'S -> @p.cdr.car 'b : 'S :: @p (pair 'a (pair 'b 'c)) : 'S -> @p.cdr.car 'b : 'S
If the original pair is not named in the stack, but a field annotation
is present in the pair type the accessed value will be annotated with a
variable annotation corresponding to the field annotation alone.
::
CDAR
:: (pair ('a %foo) (pair %bar ('b %x) ('c %y))) : 'S -> @p.bar.x 'b : 'S
A similar mechanism is used for context dependent instructions: A similar mechanism is used for context dependent instructions:

67
src/proto_alpha/lib_client/michelson_v1_macros.ml
View File

@ -48,16 +48,20 @@ let expand_caddadr original =
ok None ok None
| _ -> ok None | _ -> ok None
let extract_first_field_annot annot = let extract_first_annot annot char =
let rec extract_first_field_annot others = function let rec extract_first_annot others = function
| [] -> None, List.rev others | [] -> None, List.rev others
| a :: rest -> | a :: rest ->
match a.[0] with try
| '%' -> Some a, List.rev_append others rest if a.[0] = char
| _ -> extract_first_field_annot (a :: others) rest then Some a, List.rev_append others rest
| exception Invalid_argument _ -> extract_first_field_annot (a :: others) rest else extract_first_annot (a :: others) rest
with Invalid_argument _ -> extract_first_annot (a :: others) rest
in in
extract_first_field_annot [] annot extract_first_annot [] annot
let extract_first_field_annot annot = extract_first_annot annot '%'
let extract_first_bind_annot annot = extract_first_annot annot '$'
let extract_field_annots annot = let extract_field_annots annot =
List.partition (fun a -> List.partition (fun a ->
@ -121,13 +125,8 @@ let expand_set_caddadr original =
] in ] in
let encoding = [ Prim (loc, "CDR", [], []) ; let encoding = [ Prim (loc, "CDR", [], []) ;
Prim (loc, "SWAP", [], []) ] in Prim (loc, "SWAP", [], []) ] in
let rename = match field_annot with
| None -> []
| Some f -> [ Prim (loc, "RENAME", [],
[ "@" ^ String.sub f 1 (String.length f - 1) ]) ]
in
let pair = [ Prim (loc, "PAIR", [], []) ] in let pair = [ Prim (loc, "PAIR", [], []) ] in
let init = Seq (loc, access_check @ encoding @ rename @ pair) in let init = Seq (loc, access_check @ encoding @ pair) in
ok (Some (parse (len - 3) init)) ok (Some (parse (len - 3) init))
| 'D' -> | 'D' ->
let access_check = match field_annot with let access_check = match field_annot with
@ -137,18 +136,8 @@ let expand_set_caddadr original =
Prim (loc, "DROP", [], []) ; Prim (loc, "DROP", [], []) ;
] in ] in
let encoding = [ Prim (loc, "CAR", [], []) ] in let encoding = [ Prim (loc, "CAR", [], []) ] in
let rename = match field_annot with
| None -> []
| Some f ->
[ Prim (loc, "DIP", [
Seq (loc, [
Prim (loc, "RENAME", [],
[ "@" ^ String.sub f 1 (String.length f - 1) ])
])
], []) ]
in
let pair = [ Prim (loc, "PAIR", [], []) ] in let pair = [ Prim (loc, "PAIR", [], []) ] in
let init = Seq (loc, access_check @ encoding @ rename @ pair) in let init = Seq (loc, access_check @ encoding @ pair) in
ok (Some (parse (len - 3) init)) ok (Some (parse (len - 3) init))
| _ -> assert false | _ -> assert false
else else
@ -170,6 +159,7 @@ let expand_map_caddadr original =
| [] | _ :: _ :: _ -> error (Invalid_arity (str, List.length args, 1)) | [] | _ :: _ :: _ -> error (Invalid_arity (str, List.length args, 1))
end >>? fun code -> end >>? fun code ->
let field_annot, annot = extract_first_field_annot annot in let field_annot, annot = extract_first_field_annot annot in
let bind_annot, annot = extract_first_bind_annot annot in
let rec parse i acc = let rec parse i acc =
if i = 4 then if i = 4 then
acc acc
@ -200,14 +190,14 @@ let expand_map_caddadr original =
Prim (loc, "PAIR", [], annot) ]) in Prim (loc, "PAIR", [], annot) ]) in
parse (i - 1) acc parse (i - 1) acc
| _ -> assert false in | _ -> assert false in
let cr_annot = match field_annot with let cr_annot =
| None -> [] let f = match field_annot with
| Some f -> [ f ] in | None -> []
let rename_op = match field_annot with | Some f -> [ f ] in
| None -> [] let b = match bind_annot with
| Some f -> | None -> []
[ Prim (loc, "RENAME", [], | Some b -> [ "@" ^ String.sub b 1 (String.length b - 1) ] in
[ "@" ^ String.sub f 1 (String.length f - 1) ]) ] in f @ b in
match String.get str (len - 2) with match String.get str (len - 2) with
| 'A' -> | 'A' ->
let init = let init =
@ -215,8 +205,7 @@ let expand_map_caddadr original =
[ Prim (loc, "DUP", [], []) ; [ Prim (loc, "DUP", [], []) ;
Prim (loc, "CDR", [], []) ; Prim (loc, "CDR", [], []) ;
Prim (loc, "DIP", Prim (loc, "DIP",
[ Seq (loc, [ Prim (loc, "CAR", [], cr_annot) ; code ] @ [ Seq (loc, [ Prim (loc, "CAR", [], cr_annot) ; code ]) ], []) ;
rename_op ) ], []) ;
Prim (loc, "SWAP", [], []) ; Prim (loc, "SWAP", [], []) ;
Prim (loc, "PAIR", [], []) ]) in Prim (loc, "PAIR", [], []) ]) in
ok (Some (parse (len - 3) init)) ok (Some (parse (len - 3) init))
@ -225,9 +214,7 @@ let expand_map_caddadr original =
Seq (loc, Seq (loc,
[ Prim (loc, "DUP", [], []) ; [ Prim (loc, "DUP", [], []) ;
Prim (loc, "CDR", [], cr_annot) ; Prim (loc, "CDR", [], cr_annot) ;
code ] @ code ;
rename_op @
[
Prim (loc, "SWAP", [], []) ; Prim (loc, "SWAP", [], []) ;
Prim (loc, "CAR", [], []) ; Prim (loc, "CAR", [], []) ;
Prim (loc, "PAIR", [], []) ]) in Prim (loc, "PAIR", [], []) ]) in
@ -674,7 +661,6 @@ let unexpand_set_caddadr expanded =
Prim (_, "DROP", [], []) ; Prim (_, "DROP", [], []) ;
Prim (_, "CDR", [], []) ; Prim (_, "CDR", [], []) ;
Prim (_, "SWAP", [], []) ; Prim (_, "SWAP", [], []) ;
Prim (_, "RENAME", [], _) ;
Prim (_, "PAIR", [], []) ]) -> Prim (_, "PAIR", [], []) ]) ->
Some (loc, "A" :: acc, field_annot :: annots) Some (loc, "A" :: acc, field_annot :: annots)
| Seq (loc, | Seq (loc,
@ -686,7 +672,6 @@ let unexpand_set_caddadr expanded =
Prim (_, "CDR", [], [ field_annot ]) ; Prim (_, "CDR", [], [ field_annot ]) ;
Prim (_, "DROP", [], []) ; Prim (_, "DROP", [], []) ;
Prim (_, "CAR", [], []) ; Prim (_, "CAR", [], []) ;
Prim (_, "DIP", [ Seq (_, [ Prim (_, "RENAME", [], _) ]) ], []);
Prim (_, "PAIR", [], []) ]) -> Prim (_, "PAIR", [], []) ]) ->
Some (loc, "D" :: acc, field_annot :: annots) Some (loc, "D" :: acc, field_annot :: annots)
| Seq (_, | Seq (_,
@ -734,8 +719,7 @@ let unexpand_map_caddadr expanded =
Prim (_, "DIP", Prim (_, "DIP",
[ Seq (_, [ Seq (_,
[ Prim (_, "CAR", [], [ field_annot ]) ; [ Prim (_, "CAR", [], [ field_annot ]) ;
code ; code ]) ], []) ;
Prim (_, "RENAME", [], _) ]) ], []) ;
Prim (_, "PAIR", [], []) ]) -> Prim (_, "PAIR", [], []) ]) ->
Some (loc, "A" :: acc, field_annot :: annots, code) Some (loc, "A" :: acc, field_annot :: annots, code)
| Seq (loc, | Seq (loc,
@ -750,7 +734,6 @@ let unexpand_map_caddadr expanded =
[ Prim (_, "DUP", [], []) ; [ Prim (_, "DUP", [], []) ;
Prim (_, "CDR", [], [ field_annot ]) ; Prim (_, "CDR", [], [ field_annot ]) ;
code ; code ;
Prim (_, "RENAME", [], _) ;
Prim (_, "SWAP", [], []) ; Prim (_, "SWAP", [], []) ;
Prim (_, "CAR", [], []) ; Prim (_, "CAR", [], []) ;
Prim (_, "PAIR", [], []) ]) -> Prim (_, "PAIR", [], []) ]) ->

8
src/proto_alpha/lib_protocol/src/script_ir_annot.ml
View File

@ -94,10 +94,10 @@ let gen_access_annot
: var_annot option -> ?default:field_annot option -> field_annot option -> var_annot option : var_annot option -> ?default:field_annot option -> field_annot option -> var_annot option
= fun value_annot ?(default=None) field_annot -> = fun value_annot ?(default=None) field_annot ->
match value_annot, field_annot, default with match value_annot, field_annot, default with
| None, None, _ | Some _, None, None -> None | None, None, _ | Some _, None, None | None, Some `Field_annot "", _ -> None
| None, Some `Field_annot f, _ -> | None, Some `Field_annot f, _ ->
Some (`Var_annot f) Some (`Var_annot f)
| Some `Var_annot v, None, Some `Field_annot f -> | Some `Var_annot v, (None | Some `Field_annot ""), Some `Field_annot f ->
Some (`Var_annot (String.concat "." [v; f])) Some (`Var_annot (String.concat "." [v; f]))
| Some `Var_annot v, Some `Field_annot f, _ -> | Some `Var_annot v, Some `Field_annot f, _ ->
Some (`Var_annot (String.concat "." [v; f])) Some (`Var_annot (String.concat "." [v; f]))
@ -106,10 +106,10 @@ let gen_binding_access_annot
: var_annot option -> ?default:binding_annot option -> binding_annot option -> binding_annot option : var_annot option -> ?default:binding_annot option -> binding_annot option -> binding_annot option
= fun value_annot ?(default=None) binding_annot -> = fun value_annot ?(default=None) binding_annot ->
match value_annot, binding_annot, default with match value_annot, binding_annot, default with
| None, None, _ | Some _, None, None -> None | None, None, _ | Some _, None, None | None, Some `Binding_annot "", _ -> None
| None, Some `Binding_annot b, _ -> | None, Some `Binding_annot b, _ ->
Some (`Binding_annot b) Some (`Binding_annot b)
| Some `Var_annot v, None, Some `Binding_annot b -> | Some `Var_annot v, (None | Some `Binding_annot ""), Some `Binding_annot b ->
Some (`Binding_annot (String.concat "." [v; b])) Some (`Binding_annot (String.concat "." [v; b]))
| Some `Var_annot v, Some `Binding_annot b, _ -> | Some `Var_annot v, Some `Binding_annot b, _ ->
Some (`Binding_annot (String.concat "." [v; b])) Some (`Binding_annot (String.concat "." [v; b]))

12
src/proto_alpha/lib_protocol/src/script_ir_translator.ml
View File

@ -1828,10 +1828,10 @@ and parse_instr
| Prim (loc, I_LOOP_LEFT, [ body ], annot), | Prim (loc, I_LOOP_LEFT, [ body ], annot),
(Item_t (Union_t ((tl, l_field), (tr, _), _), rest, union_annot) as stack) -> (Item_t (Union_t ((tl, l_field), (tr, _), _), rest, union_annot) as stack) ->
check_kind [ Seq_kind ] body >>=? fun () -> check_kind [ Seq_kind ] body >>=? fun () ->
fail_unexpected_annot loc annot >>=? fun () -> parse_binding_annot loc annot >>=? fun l_bind_annot ->
parse_var_field_annot loc annot >>=? fun (r_annot, l_annot) -> let l_bind_annot = default_annot l_bind_annot
let l_annot = default_annot (field_to_var_annot l_annot) ~default:(gen_binding_access_annot union_annot (field_to_binding_annot l_field)) in
~default:(gen_access_annot union_annot l_field) in let l_annot = binding_to_var_annot l_bind_annot in
parse_instr ?type_logger tc_context ctxt body parse_instr ?type_logger tc_context ctxt body
(Item_t (tl, rest, l_annot)) >>=? begin fun (judgement, ctxt) -> match judgement with (Item_t (tl, rest, l_annot)) >>=? begin fun (judgement, ctxt) -> match judgement with
| Typed ibody -> | Typed ibody ->
@ -1839,10 +1839,10 @@ and parse_instr
trace unmatched_branches trace unmatched_branches
(Lwt.return (stack_ty_eq 1 ibody.aft stack) >>=? fun Eq -> (Lwt.return (stack_ty_eq 1 ibody.aft stack) >>=? fun Eq ->
Lwt.return (merge_stacks loc ibody.aft stack) >>=? fun _stack -> Lwt.return (merge_stacks loc ibody.aft stack) >>=? fun _stack ->
typed ctxt loc (Loop_left ibody) (Item_t (tr, rest, r_annot))) typed ctxt loc (Loop_left ibody) (Item_t (tr, rest, None)))
| Failed { descr } -> | Failed { descr } ->
let ibody = descr stack in let ibody = descr stack in
typed ctxt loc (Loop_left ibody) (Item_t (tr, rest, r_annot)) typed ctxt loc (Loop_left ibody) (Item_t (tr, rest, None))
end end
| Prim (loc, I_LAMBDA, [ arg ; ret ; code ], annot), | Prim (loc, I_LAMBDA, [ arg ; ret ; code ], annot),
stack -> stack ->