Merge branch 'work-on-script' into 'master'

Tracing interpreter and type checker

Implements:
  * a typechecker that optionally dumps the types of each instruction
  * an interpreter that drops the stack at each execution step

Incidentally:
  * adds some RPCs to pretty print the traces
  * drops floats and imperative structures from the language
  * fixes the typing of `FAIL`
This commit is contained in:
Benjamin Canou 2016-11-17 14:42:40 +01:00 committed by Benjamin Canou
commit 3b071cac46
19 changed files with 1243 additions and 1449 deletions

View File

@ -57,49 +57,47 @@ let parse_program s =
with
| 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 rec do_seq = function
| [] -> assert false
| [ last ] -> Format.fprintf ppf "%a }@]" print_ir last
| fst :: rest -> Format.fprintf ppf "%a ;@ " print_ir fst ; do_seq rest in
| [ last ] -> Format.fprintf ppf "%a }@]" (print_ir locations) last
| fst :: rest -> Format.fprintf ppf "%a ;@ " (print_ir locations) fst ; do_seq rest in
let rec do_args = function
| [] -> assert false
| [ last ] -> Format.fprintf ppf "%a@]" print_ir last
| fst :: rest -> Format.fprintf ppf "%a@," print_ir fst ; do_args rest in
| [ last ] -> Format.fprintf ppf "%a@]" (print_ir locations) last
| 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
| String (_, s) -> Format.fprintf ppf "%S" s
| Int (_, s) -> Format.fprintf ppf "%s" s
| Float (_, s) -> Format.fprintf ppf "%s" s
| Seq (_, [ one ]) -> print_ir ppf one
| Seq (_, [ one ]) -> print_ir locations ppf one
| Seq (_, []) -> Format.fprintf ppf "{}" ;
| Seq (_, seq) ->
Format.fprintf ppf "{ @[<v>" ;
do_seq seq
| Prim (_, "push", [ Prim (_, name, []) ]) ->
Format.fprintf ppf "push %s" name
| Prim (_, name, []) ->
Format.fprintf ppf "%s" name
| 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 ;
| Prim (loc, name, []) ->
Format.fprintf ppf "%s%a" name print_location loc
| Prim (loc, name, seq) ->
Format.fprintf ppf "@[<v 2>%s%a@," name print_location loc;
do_args seq
let print_program ppf c =
let print_program locations ppf c =
Format.fprintf ppf
"@[<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
"@[<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
"@[<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
"@[<v 2>code@,%a@]"
print_ir (c : Script.code).Script.code
(print_ir locations) (c : Script.code).Script.code
let parse_data s =
let lexbuf = Lexing.from_string s in
@ -119,16 +117,65 @@ let parse_data_type s =
with
| exn -> report_parse_error "data_type: " exn lexbuf
let unexpand_macros type_map program =
let open Script in
let rec caddr type_map acc = function
| [] -> Some (List.rev acc)
| Prim (loc, "car" , []) :: rest when List.mem_assoc loc type_map ->
caddr type_map ((loc, "a") :: acc) rest
| Prim (loc, "cdr" , []) :: rest when List.mem_assoc loc type_map ->
caddr type_map ((loc, "d") :: acc) rest
| _ -> None in
let rec unexpand type_map node =
match node with
| Seq (loc, l) ->
begin match caddr type_map [] l with
| None ->
let type_map, l =
List.fold_left
(fun (type_map, acc) e ->
let type_map, e = unexpand type_map e in
type_map, e :: acc)
(type_map, [])
l in
type_map, Seq (loc, List.rev l)
| Some l ->
let locs, steps = List.split l in
let name = "c" ^ String.concat "" steps ^ "r" in
let first, last = List.hd locs, List.hd (List.rev locs) in
let (before, _) = List.assoc first type_map in
let (_, after) = List.assoc last type_map in
let type_map =
List.filter
(fun (loc, _) -> not (List.mem loc locs))
type_map in
let type_map = (loc, (before, after)):: type_map in
type_map, Prim (loc, name, [])
end
| oth -> type_map, oth in
let type_map, code = unexpand type_map program.code in
type_map, { program with code }
module Program = Client_aliases.Alias (struct
type t = Script.code
let encoding = Script.code_encoding
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"
end)
let commands () =
let open Cli_entries in
let show_types = ref false in
let show_types_arg =
"-details",
Arg.Set show_types,
"Show the types of each instruction" in
let trace_stack = ref false in
let trace_stack_arg =
"-trace-stack",
Arg.Set trace_stack,
"Show the stack after each step" in
register_group "programs" "Commands for managing the record of known programs" ;
[
command
@ -162,17 +209,76 @@ let commands () =
Program.to_source program >>= fun source ->
Format.printf "%s\n" source ;
Lwt.return ()) ;
command
~group: "programs"
~desc: "ask the node to run a program"
~args: [ trace_stack_arg ]
(prefixes [ "run" ; "program" ]
@@ Program.source_param
@@ prefixes [ "on" ; "storage" ]
@@ Cli_entries.param ~name:"storage" ~desc:"the untagged storage data" parse_data
@@ prefixes [ "and" ; "input" ]
@@ Cli_entries.param ~name:"storage" ~desc:"the untagged input data" parse_data
@@ stop)
(fun program storage input () ->
let open Data_encoding in
if !trace_stack then
Client_proto_rpcs.Helpers.trace_code (block ()) program (storage, input) >>= function
| Ok (storage, output, trace) ->
Format.printf "@[<v 0>@[<v 2>storage@,%a@]@,@[<v 2>output@,%a@]@,@[<v 2>trace@,%a@]@]@."
(print_ir (fun _ -> false)) storage
(print_ir (fun _ -> false)) output
(Format.pp_print_list
(fun ppf (loc, gas, stack) ->
Format.fprintf ppf
"- @[<v 0>location: %d (remaining gas: %d)@,[ @[<v 0>%a ]@]@]"
loc gas
(Format.pp_print_list (print_ir (fun _ -> false)))
stack))
trace ;
Lwt.return ()
| Error errs ->
pp_print_error Format.err_formatter errs ;
error "error running program"
else
Client_proto_rpcs.Helpers.run_code (block ()) program (storage, input) >>= function
| Ok (storage, output) ->
Format.printf "@[<v 0>@[<v 2>storage@,%a@]@,@[<v 2>output@,%a@]@]@."
(print_ir (fun _ -> false)) storage
(print_ir (fun _ -> false)) output ;
Lwt.return ()
| Error errs ->
pp_print_error Format.err_formatter errs ;
error "error running program") ;
command
~group: "programs"
~desc: "ask the node to typecheck a program"
~args: [ show_types_arg ]
(prefixes [ "typecheck" ; "program" ]
@@ Program.source_param
@@ stop)
(fun program () ->
let open Data_encoding in
Client_proto_rpcs.Helpers.typecheck_code (block ()) program >>= function
| Ok () ->
| Ok type_map ->
let type_map, program = unexpand_macros type_map program in
message "Well typed" ;
if !show_types then begin
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)
(List.sort compare type_map)
end ;
Lwt.return ()
| Error 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_type: string -> Script.expr Lwt.t
val print_program: Format.formatter -> Script.code -> unit
module Program : Client_aliases.Alias with type t = Script.code
val commands: unit -> Cli_entries.command list

View File

@ -127,6 +127,14 @@ module Helpers = struct
let typecheck_code = call_error_service1 Services.Helpers.typecheck_code
let run_code block code (storage, input) =
call_error_service1 Services.Helpers.run_code
block (code, storage, input, None, None)
let trace_code block code (storage, input) =
call_error_service1 Services.Helpers.trace_code
block (code, storage, input, None, None)
let typecheck_tagged_data = call_error_service1 Services.Helpers.typecheck_tagged_data
let typecheck_untagged_data = call_error_service1 Services.Helpers.typecheck_untagged_data

View File

@ -92,7 +92,14 @@ end
module Helpers : sig
val minimal_time:
block -> ?prio:int -> unit -> Time.t tzresult Lwt.t
val typecheck_code: block -> Script.code -> unit tzresult Lwt.t
val run_code: block -> Script.code ->
(Script.expr * Script.expr) ->
(Script.expr * Script.expr) tzresult Lwt.t
val trace_code: block -> Script.code ->
(Script.expr * Script.expr) ->
(Script.expr * Script.expr *
(Script.location * int * Script.expr list) list) 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_untagged_data: block -> Script.expr * Script.expr -> unit tzresult Lwt.t
val hash_data: block -> Script.expr -> string tzresult Lwt.t

View File

@ -73,22 +73,6 @@ let char_for_hexadecimal_code lexbuf i =
in
char_of_int (val1 * 16 + val2)
(* Remove underscores from float literals *)
let remove_underscores s =
let s = Bytes.of_string s in
let l = Bytes.length s in
let rec remove src dst =
if Compare.Int.(src >= l) then
if Compare.Int.(dst >= l) then s else Bytes.sub s 0 dst
else
match Bytes.get s src with
'_' -> remove (src + 1) dst
| c -> Bytes.set s dst c; remove (src + 1) (dst + 1)
in Bytes.to_string (remove 0 0)
(** Lexer state *)
type state = {
@ -234,11 +218,6 @@ let bin_literal =
'0' ['b' 'B'] ['0'-'1'] ['0'-'1' '_']*
let int_literal =
'-' ? ( decimal_literal | hex_literal | oct_literal | bin_literal)
let float_literal =
'-' ?
['0'-'9'] ['0'-'9' '_']*
('.' ['0'-'9' '_']* )?
(['e' 'E'] ['+' '-']? ['0'-'9'] ['0'-'9' '_']*)?
rule indent_tokens st nl = parse
@ -332,9 +311,6 @@ and raw_token st = parse
| int_literal
{ INT (Lexing.lexeme lexbuf) }
| float_literal
{ FLOAT (remove_underscores (Lexing.lexeme lexbuf)) }
| "\""
{ reset_string_buffer st;
let string_start = lexbuf.Lexing.lex_start_p in

View File

@ -9,12 +9,11 @@
%token RPAREN
%token SEMICOLON
%token <string> FLOAT
%token <string> INT
%token <string> PRIM
%token <string> STRING
%left PRIM INT FLOAT LPAREN LBRACE STRING
%left PRIM INT LPAREN LBRACE STRING
%left apply
%start <Script_located_ir.node list> tree
@ -127,7 +126,7 @@ let expand = function
let apply node arg =
match node with
| Prim (loc, n, args) -> Prim (loc, n, args @ [arg])
| Int _ | Float _ | String _ | Seq _ as _node ->
| Int _ | String _ | Seq _ as _node ->
raise (Invalid_application (node_location arg))
let rec apply_seq node = function
@ -166,7 +165,6 @@ line_node:
| LBRACE nodes = nodes RBRACE { Seq (pos $startpos $endpos, nodes) }
| prim = PRIM { Prim (pos $startpos $endpos, prim, []) }
| i = INT { Int (pos $startpos $endpos, i) }
| f = FLOAT { Float (pos $startpos $endpos, f) }
| s = STRING { String (pos $startpos $endpos, s) }
%%

View File

@ -15,14 +15,12 @@ type location =
type node =
| Int of location * string
| Float of location * string
| String of location * string
| Prim of location * string * node list
| Seq of location * node list
let node_location = function
| Int (loc, _)
| Float (loc, _)
| String (loc, _)
| Prim (loc, _, _)
| Seq (loc, _) -> loc
@ -57,8 +55,6 @@ let strip_locations root =
match l with
| Int (_, v) ->
Script.Int (id, v)
| Float (_, v) ->
Script.Float (id, v)
| String (_, v) ->
Script.String (id, v)
| Seq (_, seq) ->

View File

@ -102,8 +102,6 @@ with the following JSON script description.
| { "left": [ /* tagged data */, /* type */ ] }
| { "right": [ /* type */, /* tagged data */ ] }
| { "or": [ /* type */, /* type */, /* untagged data */ ] }
| { "ref": [ /* tagged data */ ] }
| { "ref": [ /* type */, /* untagged data */ ] }
| { "some": [ /* tagged data */ ] }
| { "some": [ /* type */, /* untagged data */ ] }
| { "none": [ /* type */ ] }
@ -135,7 +133,6 @@ with the following JSON script description.
| { "pair": [ /* untagged data */, /* untagged data */ ] }
| { "left": [ /* untagged data */ ] }
| { "right": [ /* untagged data */ ] }
| { "ref": [ /* untagged data */ ] }
| { "some": [ /* untagged data */ ] }
| "none"
| { "list": [ /* untagged data */ ... ] }
@ -161,15 +158,11 @@ with the following JSON script description.
| { "if_cons": [ [ /* instruction */ ... ], [ /* instruction */ ... ] ] }
| { "empty_set": [ /* type */ ] }
| { "empty_map": [ /* comparable type */, /* type */ ] }
| "iter"
| "map"
| "reduce"
| "mem"
| "get"
| "update"
| "ref"
| "deref"
| "set"
| { "if": [ [ /* instruction */ ... ], [ /* instruction */ ... ] ] }
| { "loop": [ [ /* instruction */ ... ] ] }
| { "lambda": [ /* type */, /* type */, [ /* instruction */ ... ] ] }
@ -239,7 +232,6 @@ with the following JSON script description.
| "key"
| "timestamp"
| "signature"
| { "ref": [ /* type */ ] }
| { "option": [ /* type */ ] }
| { "list": [ /* type */ ] }
| { "set": [ /* comparable type */ ] }

View File

@ -32,7 +32,7 @@ I - Type system
The types `T` of values in the stack are written using notations
* `bool`, `string`, `void`, `u?int{8|16|32|64}`, `float`,
* `bool`, `string`, `void`, `u?int{8|16|32|64}`,
the core primitive types,
* `identifier` for a primitive data-type,
* `T identifier` for a parametric data-type with one parameter type `T`,
@ -94,7 +94,6 @@ the form `variable = constant, ...`.
The constants are of one of the following forms.
* integers with their sign and size, e.g. `(Uint8 3)`,
* floats in libc-style notation, e.g. `(Float 4.5e2)`,
* `Void`, the unique value of type `void`
* booleans `True` and `False`,
* string literals, as in `(String "contents")`,
@ -274,7 +273,7 @@ combinators, and also for branching.
IV - Data types
---------------
* `bool`, `string`, `void`, `u?int{8|16|32|64}`, `float`:
* `bool`, `string`, `void`, `u?int{8|16|32|64}`:
The core primitive types.
* `list 'a`:
@ -292,11 +291,8 @@ IV - Data types
A union of two types, a value holding either a value a of type 'a
or a value b of type 'b, that we write (Left a) or (Right b).
* `ref 'a`:
Classical imperative stores, that we note (Ref const).
* `set 'a`, `map 'a 'b`:
Imperative map and sets, optimized in the db.
Immutable map and sets.
V - Operations
@ -507,129 +503,6 @@ Bitwise logical operators are also available on unsigned integers.
:: t : t : 'S -> int64 : 'S where t in uint{8|16|32|64}
### Operations on Floats
The float type uses double precision IEEE754 semantics, including NaN
and infinite values.
* `ADD`
:: float : float : 'S -> float : 'S
> ADD ; C / x : y : S => C / (x + y) : S
* `SUB`
:: float : float : 'S -> float : 'S
> SUB ; C / x : y : S => C / (x - y) : S
* `MUL`
:: float : float : 'S -> float : 'S
> MUL ; C / x : y : S => C / (x * y) : S
* `DIV`
:: float : float : 'S -> float : 'S
> DIV ; C / x : y : S => C / (x / y) : S
* `MOD`
:: float : float : 'S -> float : 'S
> MOD ; C / x : y : S => C / (fmod (x, y)) : S
* `ABS`
:: float : 'S -> float : 'S
> ABS ; C / x : S => C / (abs (x)) : S
* `NEG`
:: float : 'S -> float : 'S
> NEG ; C / x : S => C / (-x) : S
* `FLOOR`
:: float : 'S -> float : 'S
> FLOOR ; C / x : S => C / (floor (x)) : S
* `CEIL`
:: float : 'S -> float : 'S
> CEIL ; C / x : S => C / (ceil (x)) : S
* `INF`
:: 'S -> float : 'S
> INF ; C / S => C / +Inf : S
* `NAN`
:: 'S -> float : 'S
> NAN ; C / S => C / NaN : S
* `ISNAN`
:: float : 'S -> bool : 'S
> ISNAN ; C / NaN : S => C / true : S
> ISNAN ; C / _ : S => C / false : S
* `NANAN`
:: float : 'S -> 'S
> NANAN ; C / NaN : S => [FAIL]
> NANAN ; C / _ : S => C / S
* `CAST float`:
Conversion from integers.
:: t_from : 'S -> float : 'S where t_from in u?int{8|16|32|64}
> CAST float ; C / x : S => C / float (x) : S
* `CAST t_to` where `t_to in u?int{8|16|32|64}`:
Conversion to integers.
:: float : 'S -> t_to : 'S
> CAST t_to ; C / NaN : S => C / t_to (0) : S
> CAST t_to ; C / +/-Inf : S => C / t_to (0) : S
> CAST t_to ; C / x : S => C / t_to (floor (x)) : S
* `CHECKED_CAST float`:
Conversion from integers with overflow checking.
:: t_from : 'S -> float : 'S where t_from in u?int{8|16|32|64}
> CHECKED_CAST float ; C / x : S => [FAIL] on overflow
> CHECKED_CAST float ; C / x : S => C / float (x) : S
* `CHECKED_CAST t_to` where `t_to in u?int{8|16|32|64}`:
Conversion to integers with overflow checking.
:: float : 'S -> t_to : 'S
> CHECKED_CAST t_to ; C / x : S => [FAIL] on overflow or NaN
> CHECKED_CAST t_to ; C / x : S => C / t_to (floor (x)) : S
* `COMPARE`:
IEEE754 comparison
:: float : float : 'S -> int64 : 'S
### Operations on strings
Strings are mostly used for naming things without having to rely on
@ -683,49 +556,10 @@ constants as is, concatenate them and use them as keys.
> CD(\rest)R ; C / S => CDR ; C(\rest)R ; C / S
> CR ; C / S => C / S
### Operations on refs
* `REF`:
Build a ref from its initial contents.
:: 'a : 'S -> ref 'a : 'S
> REF ; C / a : S / M => C / l : S / l = (Ref a), M
* `DEREF`:
Access the contents of a ref.
:: ref 'a : 'S -> 'a : 'S
> DEREF ; C / l : S / l = (Ref a), M => C / a : S / l = (Ref a), M
* `SET`
Update the contents of a ref.
:: 'a : ref 'a : 'S -> 'S
> SET ; C / v :: l : S / l = (Ref _), M => C / S / l = (Ref v), M
* `INCR step`:
Increments a counter.
:: ref 'a : 'S -> 'S
iff step :: 'a, operator ADD defined on 'a
> INCR step ; C / l : S / M => DUP ; DEREF ; PUSH step ; ADD ; Set ; C / S / M
* `DECR step`:
Decrements a counter.
:: ref 'a : 'S -> 'S
iff step :: 'a, operator SUB defined on 'a
> DECR step ; C / l : S / M => DUP ; DEREF ; PUSH step ; SUB ; Set ; C / S / M
### Operations on sets
* `EMPTY_SET 'elt`:
Build a new, empty imperative set for elements of a given type.
Build a new, empty set for elements of a given type.
:: 'S -> set 'elt : 'S
@ -740,12 +574,7 @@ constants as is, concatenate them and use them as keys.
* `UPDATE`:
Inserts or removes an element in a set, replacing a previous value.
:: 'elt : bool : set 'elt : 'S -> 'S
* `ITER`:
Apply an imperative function over all the elements of a set.
:: lambda 'elt void : set 'elt : 'S -> 'S
:: 'elt : bool : set 'elt : 'S -> set 'elt : 'S
* `REDUCE`:
Apply a function on a set passing the result of each
@ -756,7 +585,7 @@ constants as is, concatenate them and use them as keys.
### Operations on maps
* `EMPTY_MAP 'key 'val`:
Build a new, empty imperative map.
Build a new, empty map.
The `'key` type must be comparable (the `COMPARE` primitive must be
defined over it).
@ -777,12 +606,7 @@ constants as is, concatenate them and use them as keys.
* `UPDATE`:
Assign or remove an element in a map.
:: 'key : option 'val : map 'key 'val : 'S -> 'S
* `ITER`:
Apply an imperative function over all the bindings of a map.
:: lambda (pair 'key 'val) void : map 'key 'val : 'S -> 'S
:: 'key : option 'val : map 'key 'val : 'S -> map 'key 'val : 'S
* `MAP`:
Apply a function on a map and return the map of results under
@ -874,11 +698,6 @@ constants as is, concatenate them and use them as keys.
> IF_CONS ; C / (Cons a rest) : S => bt ; C / a : rest : S
> IF_CONS ; C / Nil : S => bf ; C / S
* `ITER`:
Apply a function on a list from left to right.
:: lambda 'a void : list 'a : 'S -> 'S
* `MAP`:
Apply a function on a list from left to right and
return the list of results in the same order.
@ -1111,14 +930,11 @@ parsing policy is described just after.
### Constants
There are three kinds of constants:
There are two kinds of constants:
1. Integers in decimal (no prefix), hexadecimal (0x prefix), octal
(0o prefix) or binary (0b prefix).
2. Floating point IEEE754 doubles in libc-style notation, with a
mandatory period character. (`3` is an `int` but `3.` is a
`float`).
3. Strings with usual escapes `\n`, `\t`, `\b`, `\r`, `\\`, `\"`.
2. Strings with usual escapes `\n`, `\t`, `\b`, `\r`, `\\`, `\"`.
Strings are encoding agnostic sequences of bytes. Non printable
characters can be escaped by 3 digits decimal codes `\ddd` or
2 digit hexadecimal codes `\xHH`.
@ -1258,8 +1074,6 @@ Capitalised.
Int8 1
Float 3.5e12
Compound constants such as lists, in order not to repeat the same
constant constructor for each element, take the type(s) of inner
values as first argument(s), and then the values without their
@ -1320,10 +1134,7 @@ data. For this, the code of the contract is checked to be of the
following type lambda (pair (pair tez 'arg) 'global) -> (pair 'ret
'global) where 'global is the type of the original global store given
on origination. The contract also takes a parameter and an amount, and
returns a value, hence the complete calling convention above. The
global values can be updated either by rewriting the object, or by
putting mutable values in it and performing side effects on them,
allowing both imperative and functional style.
returns a value, hence the complete calling convention above.
### Empty contract
@ -1675,7 +1486,6 @@ X - Full grammar
<tagged data> ::=
| <string constant>
| <float constant>
| Int8 <int constant>
| Int16 <int constant>
| Int32 <int constant>
@ -1694,8 +1504,6 @@ X - Full grammar
| Left <tagged data> <type>
| Right <type> <tagged data>
| Or <type> <type> <untagged data>
| Ref <tagged data>
| Ref <type> <untagged data>
| Some <tagged data>
| Some <type> <untagged data>
| None <type>
@ -1710,7 +1518,6 @@ X - Full grammar
<untagged data> ::=
| <int constant>
| <string constant>
| <float constant>
| <timestamp string constant>
| <signature string constant>
| <key string constant>
@ -1722,7 +1529,6 @@ X - Full grammar
| Pair <untagged data> <untagged data>
| Left <untagged data>
| Right <untagged data>
| Ref <untagged data>
| Some <untagged data>
| None
| List <untagged data> ...
@ -1748,15 +1554,11 @@ X - Full grammar
| IF_CONS { <instruction> ... } { <instruction> ... }
| EMPTY_SET <type>
| EMPTY_MAP <comparable type> <type>
| ITER
| MAP
| REDUCE
| MEM
| GET
| UPDATE
| REF
| DEREF
| SET
| IF { <instruction> ... } { <instruction> ... }
| LOOP { <instruction> ... }
| LAMBDA <type> <type> { <instruction> ... }
@ -1820,13 +1622,11 @@ X - Full grammar
| uint64
| void
| string
| float
| tez
| bool
| key
| timestamp
| signature
| ref <type>
| option <type>
| list <type>
| set <comparable type>
@ -1845,7 +1645,6 @@ X - Full grammar
| uint32
| uint64
| string
| float
| tez
| bool
| key
@ -1880,9 +1679,9 @@ The language is implemented in OCaml as follows:
interpreting the If instruction.
* The input, untyped internal representation is an OCaml ADT with
the only 5 grammar constructions: `String`, `Float`, `Int`, `Seq`
and `Prim`. It is the target language for the parser, since not
all parsable programs are well typed, and thus could simply not be
the only 5 grammar constructions: `String`, `Int`, `Seq` and
`Prim`. It is the target language for the parser, since not all
parsable programs are well typed, and thus could simply not be
constructed using the GADT.
* The typechecker is a simple function that recognizes the abstract
@ -1890,7 +1689,7 @@ The language is implemented in OCaml as follows:
well-typed, corresponding GADT expressions. It is mostly a
checker, not a full inferer, and thus takes some annotations
(basically the inpout and output of the program, of lambdas and of
uninitialized imperative structures). It works by performing a
uninitialized maps and sets). It works by performing a
symbolic evaluation of the program, transforming a symbolic
stack. It only needs one pass over the whole program.

View File

@ -65,308 +65,246 @@ type 'tys stack =
| Item : 'ty * 'rest stack -> ('ty * 'rest) stack
| Empty : end_of_stack stack
let is_nan x = match classify_float x with
| FP_nan -> true
| _ -> false
let eq_comparable
: type a. a comparable_ty -> a -> a -> bool
= fun kind x v -> match kind with
| String_key -> Compare.String.(x = v)
| Bool_key -> Compare.Bool.(x = v)
| Float_key -> Compare.Float.(x = v)
| Tez_key -> Tez.(x = v)
| Key_key -> Ed25519.Public_key_hash.(equal x v)
| Int_key kind -> Script_int.(equal kind x v)
| Timestamp_key -> Timestamp.(x = v)
let rec unparse_stack
: type a. a stack * a stack_ty -> Script.expr list
= function
| Empty, Empty_t -> []
| Item (v, rest), Item_t (ty, rest_ty) ->
unparse_tagged_data ty v :: unparse_stack (rest, rest_ty)
let rec interp
: type p r.
?log: (Script.location * int * Script.expr list) list ref ->
int -> Contract.t -> Contract.t -> Tez.t ->
context -> (p, r) lambda -> p -> (r * int * context) tzresult Lwt.t
= fun qta orig source amount ctxt (Lam (code, _)) arg ->
= fun ?log qta orig source amount ctxt (Lam (code, _)) arg ->
let rec step
: type b a.
int -> context -> (b, a) instr -> b stack ->
int -> context -> (b, a) descr -> b stack ->
(a stack * int * context) tzresult Lwt.t =
fun qta ctxt instr stack ->
fun qta ctxt ({ instr ; loc } as descr) stack ->
if Compare.Int.(qta <= 0) then
fail Quota_exceeded
else match instr, stack with
else
let logged_return ((ret, qta, _) as res) =
match log with
| None -> return res
| Some log ->
log := (descr.loc, qta, unparse_stack (ret, descr.aft)) :: !log ;
return res in
match instr, stack with
(* stack ops *)
| Drop, Item (_, rest) ->
return (rest, qta - 1, ctxt)
logged_return (rest, qta - 1, ctxt)
| Dup, Item (v, rest) ->
return (Item (v, Item (v, rest)), qta - 1, ctxt)
logged_return (Item (v, Item (v, rest)), qta - 1, ctxt)
| Swap, Item (vi, Item (vo, rest)) ->
return (Item (vo, Item (vi, rest)), qta - 1, ctxt)
logged_return (Item (vo, Item (vi, rest)), qta - 1, ctxt)
| Const v, rest ->
return (Item (v, rest), qta - 1, ctxt)
logged_return (Item (v, rest), qta - 1, ctxt)
(* options *)
| Cons_some, Item (v, rest) ->
return (Item (Some v, rest), qta - 1, ctxt)
logged_return (Item (Some v, rest), qta - 1, ctxt)
| Cons_none _, rest ->
return (Item (None, rest), qta - 1, ctxt)
logged_return (Item (None, rest), qta - 1, ctxt)
| If_none (bt, _), Item (None, rest) ->
step qta ctxt bt rest
| If_none (_, bf), Item (Some v, rest) ->
step qta ctxt bf (Item (v, rest))
(* pairs *)
| Cons_pair, Item (a, Item (b, rest)) ->
return (Item ((a, b), rest), qta - 1, ctxt)
logged_return (Item ((a, b), rest), qta - 1, ctxt)
| Car, Item ((a, _), rest) ->
return (Item (a, rest), qta - 1, ctxt)
logged_return (Item (a, rest), qta - 1, ctxt)
| Cdr, Item ((_, b), rest) ->
return (Item (b, rest), qta - 1, ctxt)
logged_return (Item (b, rest), qta - 1, ctxt)
(* unions *)
| Left, Item (v, rest) ->
return (Item (L v, rest), qta - 1, ctxt)
logged_return (Item (L v, rest), qta - 1, ctxt)
| Right, Item (v, rest) ->
return (Item (R v, rest), qta - 1, ctxt)
logged_return (Item (R v, rest), qta - 1, ctxt)
| If_left (bt, _), Item (L v, rest) ->
step qta ctxt bt (Item (v, rest))
| If_left (_, bf), Item (R v, rest) ->
step qta ctxt bf (Item (v, rest))
(* lists *)
| Cons_list, Item (hd, Item (tl, rest)) ->
return (Item (hd :: tl, rest), qta - 1, ctxt)
logged_return (Item (hd :: tl, rest), qta - 1, ctxt)
| Nil, rest ->
return (Item ([], rest), qta - 1, ctxt)
logged_return (Item ([], rest), qta - 1, ctxt)
| If_cons (_, bf), Item ([], rest) ->
step qta ctxt bf rest
| If_cons (bt, _), Item (hd :: tl, rest) ->
step qta ctxt bt (Item (hd, Item (tl, rest)))
| List_iter, Item (lam, Item (l, rest)) ->
fold_left_s (fun ((), qta, ctxt) arg ->
interp qta orig source amount ctxt lam arg)
((), qta, ctxt) l >>=? fun ((), qta, ctxt) ->
return (rest, qta, ctxt)
| List_map, Item (lam, Item (l, rest)) ->
fold_left_s (fun (tail, qta, ctxt) arg ->
interp qta orig source amount ctxt lam arg
interp ?log qta orig source amount ctxt lam arg
>>=? fun (ret, qta, ctxt) ->
return (ret :: tail, qta, ctxt))
([], qta, ctxt) l >>=? fun (res, qta, ctxt) ->
return (Item (res, rest), qta, ctxt)
logged_return (Item (res, rest), qta, ctxt)
| List_reduce, Item (lam, Item (l, Item (init, rest))) ->
fold_left_s
(fun (partial, qta, ctxt) arg ->
interp qta orig source amount ctxt lam (arg, partial)
interp ?log qta orig source amount ctxt lam (arg, partial)
>>=? fun (partial, qta, ctxt) ->
return (partial, qta, ctxt))
(init, qta, ctxt) l >>=? fun (res, qta, ctxt) ->
return (Item (res, rest), qta, ctxt)
logged_return (Item (res, rest), qta, ctxt)
(* sets *)
| Empty_set t, rest ->
return (Item ((ref [], t), rest), qta - 1, ctxt)
| Set_iter, Item (lam, Item ((l, _), rest)) ->
fold_left_s (fun ((), qta, ctxt) arg ->
interp qta orig source amount ctxt lam arg)
((), qta, ctxt) !l >>=? fun ((), qta, ctxt) ->
return (rest, qta, ctxt)
| Set_map t, Item (lam, Item ((l, _), rest)) ->
logged_return (Item (empty_set t, rest), qta - 1, ctxt)
| Set_map t, Item (lam, Item (set, rest)) ->
let items =
List.rev (set_fold (fun e acc -> e :: acc) set []) in
fold_left_s
(fun (tail, qta, ctxt) arg ->
interp qta orig source amount ctxt lam arg >>=?
(fun (res, qta, ctxt) arg ->
interp ?log qta orig source amount ctxt lam arg >>=?
fun (ret, qta, ctxt) ->
return (ret :: tail, qta, ctxt))
([], qta, ctxt) !l >>=? fun (res, qta, ctxt) ->
return (Item ((ref res, t), rest), qta, ctxt)
| Set_reduce, Item (lam, Item ((l, _), Item (init, rest))) ->
return (set_update ret true res, qta, ctxt))
(empty_set t, qta, ctxt) items >>=? fun (res, qta, ctxt) ->
logged_return (Item (res, rest), qta, ctxt)
| Set_reduce, Item (lam, Item (set, Item (init, rest))) ->
let items =
List.rev (set_fold (fun e acc -> e :: acc) set []) in
fold_left_s
(fun (partial, qta, ctxt) arg ->
interp qta orig source amount ctxt lam (arg, partial)
interp ?log qta orig source amount ctxt lam (arg, partial)
>>=? fun (partial, qta, ctxt) ->
return (partial, qta, ctxt))
(init, qta, ctxt) !l >>=? fun (res, qta, ctxt) ->
return (Item (res, rest), qta, ctxt)
| Set_mem, Item (v, Item ((l, kind), rest)) ->
return (Item (List.exists (eq_comparable kind v) !l, rest), qta - 1, ctxt)
| Set_update, Item (v, Item (false, Item ((l, kind), rest))) ->
l := List.filter (fun x -> not (eq_comparable kind x v)) !l ;
return (rest, qta - 1, ctxt)
| Set_update, Item (v, Item (true, Item ((l, kind), rest))) ->
l := v :: List.filter (fun x -> not (eq_comparable kind x v)) !l ;
return (rest, qta - 1, ctxt)
(init, qta, ctxt) items >>=? fun (res, qta, ctxt) ->
logged_return (Item (res, rest), qta, ctxt)
| Set_mem, Item (v, Item (set, rest)) ->
logged_return (Item (set_mem v set, rest), qta - 1, ctxt)
| Set_update, Item (v, Item (presence, Item (set, rest))) ->
logged_return (Item (set_update v presence set, rest), qta - 1, ctxt)
(* maps *)
| Empty_map (t, _), rest ->
return (Item ((ref [], t), rest), qta - 1, ctxt)
| Map_iter, Item (lam, Item ((l, _), rest)) ->
logged_return (Item (empty_map t, rest), qta - 1, ctxt)
| Map_map, Item (lam, Item (map, rest)) ->
let items =
List.rev (map_fold (fun k v acc -> (k, v) :: acc) map []) in
fold_left_s
(fun ((), qta, ctxt) arg -> interp qta orig source amount ctxt lam arg)
((), qta, ctxt) !l >>=? fun ((), qta, ctxt) ->
return (rest, qta, ctxt)
| Map_map, Item (lam, Item ((l, t), rest)) ->
fold_left_s
(fun (tail, qta, ctxt) (k, v) ->
interp qta orig source amount ctxt lam (k, v)
(fun (acc, qta, ctxt) (k, v) ->
interp ?log qta orig source amount ctxt lam (k, v)
>>=? fun (ret, qta, ctxt) ->
return ((k, ret) :: tail, qta, ctxt))
([], qta, ctxt) !l >>=? fun (res, qta, ctxt) ->
return (Item ((ref res, t), rest), qta, ctxt)
| Map_reduce, Item (lam, Item ((l, _), Item (init, rest))) ->
return (map_update k (Some ret) acc, qta, ctxt))
(empty_map (map_key_ty map), qta, ctxt) items >>=? fun (res, qta, ctxt) ->
logged_return (Item (res, rest), qta, ctxt)
| Map_reduce, Item (lam, Item (map, Item (init, rest))) ->
let items =
List.rev (map_fold (fun k v acc -> (k, v) :: acc) map []) in
fold_left_s
(fun (partial, qta, ctxt) arg ->
interp qta orig source amount ctxt lam (arg, partial)
interp ?log qta orig source amount ctxt lam (arg, partial)
>>=? fun (partial, qta, ctxt) ->
return (partial, qta, ctxt))
(init, qta, ctxt) !l >>=? fun (res, qta, ctxt) ->
return (Item (res, rest), qta, ctxt)
| Map_mem, Item (v, Item ((l, kind), rest)) ->
let res = List.exists (fun (k, _) -> eq_comparable kind k v) !l in
return (Item (res, rest), qta - 1, ctxt)
| Map_get, Item (v, Item ((l, kind), rest)) ->
let res =
try Some (snd (List.find (fun (k, _) -> eq_comparable kind k v) !l))
with Not_found -> None in
return (Item (res, rest), qta - 1, ctxt)
| Map_update, Item (vk, Item (None, Item ((l, kind), rest))) ->
l := List.filter (fun (k, _) -> not (eq_comparable kind k vk)) !l ;
return (rest, qta - 1, ctxt)
| Map_update, Item (vk, Item (Some v, Item ((l, kind), rest))) ->
l := (vk, v) :: List.filter (fun (k, _) -> not (eq_comparable kind k vk)) !l ;
return (rest, qta - 1, ctxt)
(* reference cells *)
| Ref, Item (v, rest) ->
return (Item (ref v, rest), qta - 1, ctxt)
| Deref, Item ({ contents = v}, rest) ->
return (Item (v, rest), qta - 1, ctxt)
| Set, Item (r, Item (v, rest)) ->
r := v ;
return (rest, qta - 1, ctxt)
(init, qta, ctxt) items >>=? fun (res, qta, ctxt) ->
logged_return (Item (res, rest), qta, ctxt)
| Map_mem, Item (v, Item (map, rest)) ->
logged_return (Item (map_mem v map, rest), qta - 1, ctxt)
| Map_get, Item (v, Item (map, rest)) ->
logged_return (Item (map_get v map, rest), qta - 1, ctxt)
| Map_update, Item (k, Item (v, Item (map, rest))) ->
logged_return (Item (map_update k v map, rest), qta - 1, ctxt)
(* timestamp operations *)
| Add_period_to_timestamp, Item (p, Item (t, rest)) ->
Lwt.return
(Period.of_seconds (Int64.of_float p) >>? fun p ->
Timestamp.(t +? p) >>? fun res ->
Ok (Item (res, rest), qta - 1, ctxt))
| Add_seconds_to_timestamp (kind, _pos), Item (n, Item (t, rest)) ->
| Add_seconds_to_timestamp kind, Item (n, Item (t, rest)) ->
let n = Script_int.to_int64 kind n in
Lwt.return
(Period.of_seconds n >>? fun p ->
Timestamp.(t +? p) >>? fun res ->
Ok (Item (res, rest), qta - 1, ctxt))
| Add_timestamp_to_period, Item (t, Item (p, rest)) ->
Lwt.return
(Period.of_seconds (Int64.of_float p) >>? fun p ->
Timestamp.(t +? p) >>? fun res ->
Ok (Item (res, rest), qta - 1, ctxt))
| Add_timestamp_to_seconds (kind, _pos), Item (t, Item (n, rest)) ->
Ok (Item (res, rest), qta - 1, ctxt)) >>=? fun res ->
logged_return res
| Add_timestamp_to_seconds kind, Item (t, Item (n, rest)) ->
let n = Script_int.to_int64 kind n in
Lwt.return
(Period.of_seconds n >>? fun p ->
Timestamp.(t +? p) >>? fun res ->
Ok (Item (res, rest), qta - 1, ctxt))
Ok (Item (res, rest), qta - 1, ctxt)) >>=? fun res ->
logged_return res
(* string operations *)
| Concat, Item (x, Item (y, rest)) ->
return (Item (x ^ y, rest), qta - 1, ctxt)
logged_return (Item (x ^ y, rest), qta - 1, ctxt)
(* currency operations *)
| Add_tez, Item (x, Item (y, rest)) ->
Lwt.return Tez.(x +? y) >>=? fun res ->
return (Item (res, rest), qta - 1, ctxt)
logged_return (Item (res, rest), qta - 1, ctxt)
| Sub_tez, Item (x, Item (y, rest)) ->
Lwt.return Tez.(x -? y) >>=? fun res ->
return (Item (res, rest), qta - 1, ctxt)
logged_return (Item (res, rest), qta - 1, ctxt)
| Mul_tez kind, Item (x, Item (y, rest)) ->
Lwt.return Tez.(x *? Script_int.to_int64 kind y) >>=? fun res ->
return (Item (res, rest), qta - 1, ctxt)
logged_return (Item (res, rest), qta - 1, ctxt)
| Mul_tez' kind, Item (y, Item (x, rest)) ->
Lwt.return Tez.(x *? Script_int.to_int64 kind y) >>=? fun res ->
return (Item (res, rest), qta - 1, ctxt)
(* float operations *)
| Floor, Item (x, rest) ->
return (Item (floor x, rest), qta - 1, ctxt)
| Ceil, Item (x, rest) ->
return (Item (ceil x, rest), qta - 1, ctxt)
| Inf, rest ->
return (Item (infinity, rest), qta - 1, ctxt)
| NaN, rest ->
return (Item (nan, rest), qta - 1, ctxt)
| IsNaN, Item (x, rest) ->
return (Item (is_nan x, rest), qta - 1, ctxt)
| NaNaN pos, Item (x, rest) ->
if is_nan x then fail (Reject pos) else return (rest, qta - 1, ctxt)
| Abs_float, Item (x, rest) ->
return (Item (abs_float x, rest), qta - 1, ctxt)
| Neg_float, Item (x, rest) ->
return (Item (0. -. x, rest), qta - 1, ctxt)
| Add_float, Item (x, Item (y, rest)) ->
return (Item (x +. y, rest), qta - 1, ctxt)
| Sub_float, Item (x, Item (y, rest)) ->
return (Item (x -. y, rest), qta - 1, ctxt)
| Mul_float, Item (x, Item (y, rest)) ->
return (Item (x *. y, rest), qta - 1, ctxt)
| Div_float, Item (x, Item (y, rest)) ->
return (Item (x /. y, rest), qta - 1, ctxt)
| Mod_float, Item (x, Item (y, rest)) ->
return (Item (mod_float x y, rest), qta - 1, ctxt)
logged_return (Item (res, rest), qta - 1, ctxt)
(* boolean operations *)
| Or, Item (x, Item (y, rest)) ->
return (Item (x || y, rest), qta - 1, ctxt)
logged_return (Item (x || y, rest), qta - 1, ctxt)
| And, Item (x, Item (y, rest)) ->
return (Item (x && y, rest), qta - 1, ctxt)
logged_return (Item (x && y, rest), qta - 1, ctxt)
| Xor, Item (x, Item (y, rest)) ->
return (Item (not x && y || x && not y, rest), qta - 1, ctxt)
logged_return (Item (not x && y || x && not y, rest), qta - 1, ctxt)
| Not, Item (x, rest) ->
return (Item (not x, rest), qta - 1, ctxt)
logged_return (Item (not x, rest), qta - 1, ctxt)
(* integer operations *)
| Checked_abs_int (kind, pos), Item (x, rest) ->
| Checked_abs_int kind, Item (x, rest) ->
begin match Script_int.checked_abs kind x with
| None -> fail (Overflow pos)
| Some res -> return (Item (res, rest), qta - 1, ctxt)
| None -> fail (Overflow loc)
| Some res -> logged_return (Item (res, rest), qta - 1, ctxt)
end
| Checked_neg_int (kind, pos), Item (x, rest) ->
| Checked_neg_int kind, Item (x, rest) ->
begin match Script_int.checked_neg kind x with
| None -> fail (Overflow pos)
| Some res -> return (Item (res, rest), qta - 1, ctxt)
| None -> fail (Overflow loc)
| Some res -> logged_return (Item (res, rest), qta - 1, ctxt)
end
| Checked_add_int (kind, pos), Item (x, Item (y, rest)) ->
| Checked_add_int kind, Item (x, Item (y, rest)) ->
begin match Script_int.checked_add kind x y with
| None -> fail (Overflow pos)
| Some res -> return (Item (res, rest), qta - 1, ctxt)
| None -> fail (Overflow loc)
| Some res -> logged_return (Item (res, rest), qta - 1, ctxt)
end
| Checked_sub_int (kind, pos), Item (x, Item (y, rest)) ->
| Checked_sub_int kind, Item (x, Item (y, rest)) ->
begin match Script_int.checked_sub kind x y with
| None -> fail (Overflow pos)
| Some res -> return (Item (res, rest), qta - 1, ctxt)
| None -> fail (Overflow loc)
| Some res -> logged_return (Item (res, rest), qta - 1, ctxt)
end
| Checked_mul_int (kind, pos), Item (x, Item (y, rest)) ->
| Checked_mul_int kind, Item (x, Item (y, rest)) ->
begin match Script_int.checked_mul kind x y with
| None -> fail (Overflow pos)
| Some res -> return (Item (res, rest), qta - 1, ctxt)
| None -> fail (Overflow loc)
| Some res -> logged_return (Item (res, rest), qta - 1, ctxt)
end
| Abs_int kind, Item (x, rest) ->
return (Item (Script_int.abs kind x, rest), qta - 1, ctxt)
logged_return (Item (Script_int.abs kind x, rest), qta - 1, ctxt)
| Neg_int kind, Item (x, rest) ->
return (Item (Script_int.neg kind x, rest), qta - 1, ctxt)
logged_return (Item (Script_int.neg kind x, rest), qta - 1, ctxt)
| Add_int kind, Item (x, Item (y, rest)) ->
return (Item (Script_int.add kind x y, rest), qta - 1, ctxt)
logged_return (Item (Script_int.add kind x y, rest), qta - 1, ctxt)
| Sub_int kind, Item (x, Item (y, rest)) ->
return (Item (Script_int.sub kind x y, rest), qta - 1, ctxt)
logged_return (Item (Script_int.sub kind x y, rest), qta - 1, ctxt)
| Mul_int kind, Item (x, Item (y, rest)) ->
return (Item (Script_int.mul kind x y, rest), qta - 1, ctxt)
| Div_int (kind, pos), Item (x, Item (y, rest)) ->
logged_return (Item (Script_int.mul kind x y, rest), qta - 1, ctxt)
| Div_int kind, Item (x, Item (y, rest)) ->
if Compare.Int64.(Script_int.to_int64 kind y = 0L) then
fail (Division_by_zero pos)
fail (Division_by_zero loc)
else
return (Item (Script_int.div kind x y, rest), qta - 1, ctxt)
| Mod_int (kind, pos), Item (x, Item (y, rest)) ->
logged_return (Item (Script_int.div kind x y, rest), qta - 1, ctxt)
| Mod_int kind, Item (x, Item (y, rest)) ->
if Compare.Int64.(Script_int.to_int64 kind y = 0L) then
fail (Division_by_zero pos)
fail (Division_by_zero loc)
else
return (Item (Script_int.rem kind x y, rest), qta - 1, ctxt)
logged_return (Item (Script_int.rem kind x y, rest), qta - 1, ctxt)
| Lsl_int kind, Item (x, Item (y, rest)) ->
return (Item (Script_int.logsl kind x y, rest), qta - 1, ctxt)
logged_return (Item (Script_int.logsl kind x y, rest), qta - 1, ctxt)
| Lsr_int kind, Item (x, Item (y, rest)) ->
return (Item (Script_int.logsr kind x y, rest), qta - 1, ctxt)
logged_return (Item (Script_int.logsr kind x y, rest), qta - 1, ctxt)
| Or_int kind, Item (x, Item (y, rest)) ->
return (Item (Script_int.logor kind x y, rest), qta - 1, ctxt)
logged_return (Item (Script_int.logor kind x y, rest), qta - 1, ctxt)
| And_int kind, Item (x, Item (y, rest)) ->
return (Item (Script_int.logand kind x y, rest), qta - 1, ctxt)
logged_return (Item (Script_int.logand kind x y, rest), qta - 1, ctxt)
| Xor_int kind, Item (x, Item (y, rest)) ->
return (Item (Script_int.logxor kind x y, rest), qta - 1, ctxt)
logged_return (Item (Script_int.logxor kind x y, rest), qta - 1, ctxt)
| Not_int kind, Item (x, rest) ->
return (Item (Script_int.lognot kind x, rest), qta - 1, ctxt)
logged_return (Item (Script_int.lognot kind x, rest), qta - 1, ctxt)
(* control *)
| Seq (hd, tl), stack ->
step qta ctxt hd stack >>=? fun (trans, qta, ctxt) ->
@ -377,93 +315,83 @@ let rec interp
step qta ctxt bf rest
| Loop body, Item (true, rest) ->
step qta ctxt body rest >>=? fun (trans, qta, ctxt) ->
step (qta - 1) ctxt (Loop body) trans
step (qta - 1) ctxt descr trans
| Loop _, Item (false, rest) ->
return (rest, qta, ctxt)
logged_return (rest, qta, ctxt)
| Dip b, Item (ign, rest) ->
step qta ctxt b rest >>=? fun (res, qta, ctxt) ->
return (Item (ign, res), qta, ctxt)
logged_return (Item (ign, res), qta, ctxt)
| Exec, Item (arg, Item (lam, rest)) ->
interp qta orig source amount ctxt lam arg >>=? fun (res, qta, ctxt) ->
return (Item (res, rest), qta - 1, ctxt)
interp ?log qta orig source amount ctxt lam arg >>=? fun (res, qta, ctxt) ->
logged_return (Item (res, rest), qta - 1, ctxt)
| Lambda lam, rest ->
return (Item (lam, rest), qta - 1, ctxt)
| Fail pos, _ ->
fail (Reject pos)
logged_return (Item (lam, rest), qta - 1, ctxt)
| Fail, _ ->
fail (Reject loc)
| Nop, stack ->
return (stack, qta - 1, ctxt)
logged_return (stack, qta - 1, ctxt)
(* comparison *)
| Compare Bool_key, Item (a, Item (b, rest)) ->
let cmpres = Compare.Bool.compare a b in
let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in
return (Item (cmpres, rest), qta - 1, ctxt)
logged_return (Item (cmpres, rest), qta - 1, ctxt)
| Compare String_key, Item (a, Item (b, rest)) ->
let cmpres = Compare.String.compare a b in
let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in
return (Item (cmpres, rest), qta - 1, ctxt)
| Compare Float_key, Item (a, Item (b, rest)) ->
let cmpres = Compare.Float.compare a b in
let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in
return (Item (cmpres, rest), qta - 1, ctxt)
logged_return (Item (cmpres, rest), qta - 1, ctxt)
| Compare Tez_key, Item (a, Item (b, rest)) ->
let cmpres = Tez.compare a b in
let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in
return (Item (cmpres, rest), qta - 1, ctxt)
logged_return (Item (cmpres, rest), qta - 1, ctxt)
| Compare (Int_key kind), Item (a, Item (b, rest)) ->
let cmpres = Script_int.compare kind a b in
return (Item (cmpres, rest), qta - 1, ctxt)
logged_return (Item (cmpres, rest), qta - 1, ctxt)
| Compare Key_key, Item (a, Item (b, rest)) ->
let cmpres = Ed25519.Public_key_hash.compare a b in
let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in
return (Item (cmpres, rest), qta - 1, ctxt)
logged_return (Item (cmpres, rest), qta - 1, ctxt)
| Compare Timestamp_key, Item (a, Item (b, rest)) ->
let cmpres = Timestamp.compare a b in
let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in
return (Item (cmpres, rest), qta - 1, ctxt)
logged_return (Item (cmpres, rest), qta - 1, ctxt)
(* comparators *)
| Eq, Item (cmpres, rest) ->
let cmpres = Script_int.to_int64 Int64 cmpres in
let cmpres = Compare.Int64.(cmpres = 0L) in
return (Item (cmpres, rest), qta - 1, ctxt)
logged_return (Item (cmpres, rest), qta - 1, ctxt)
| Neq, Item (cmpres, rest) ->
let cmpres = Script_int.to_int64 Int64 cmpres in
let cmpres = Compare.Int64.(cmpres <> 0L) in
return (Item (cmpres, rest), qta - 1, ctxt)
logged_return (Item (cmpres, rest), qta - 1, ctxt)
| Lt, Item (cmpres, rest) ->
let cmpres = Script_int.to_int64 Int64 cmpres in
let cmpres = Compare.Int64.(cmpres < 0L) in
return (Item (cmpres, rest), qta - 1, ctxt)
logged_return (Item (cmpres, rest), qta - 1, ctxt)
| Gt, Item (cmpres, rest) ->
let cmpres = Script_int.to_int64 Int64 cmpres in
let cmpres = Compare.Int64.(cmpres > 0L) in
return (Item (cmpres, rest), qta - 1, ctxt)
logged_return (Item (cmpres, rest), qta - 1, ctxt)
| Le, Item (cmpres, rest) ->
let cmpres = Script_int.to_int64 Int64 cmpres in
let cmpres = Compare.Int64.(cmpres <= 0L) in
return (Item (cmpres, rest), qta - 1, ctxt)
logged_return (Item (cmpres, rest), qta - 1, ctxt)
| Ge, Item (cmpres, rest) ->
let cmpres = Script_int.to_int64 Int64 cmpres in
let cmpres = Compare.Int64.(cmpres >= 0L) in
return (Item (cmpres, rest), qta - 1, ctxt)
logged_return (Item (cmpres, rest), qta - 1, ctxt)
(* casts *)
| Checked_int_of_int (_, kt, pos), Item (v, rest) ->
| Checked_int_of_int (_, kt), Item (v, rest) ->
begin match Script_int.checked_cast kt v with
| None -> fail (Overflow pos)
| Some res -> return (Item (res, rest), qta - 1, ctxt)
| None -> fail (Overflow loc)
| Some res -> logged_return (Item (res, rest), qta - 1, ctxt)
end
| Int_of_int (_, kt), Item (v, rest) ->
return (Item (Script_int.cast kt v, rest), qta - 1, ctxt)
| Int_of_float kt, Item (v, rest) ->
let v = Int64.of_float v in
return (Item (Script_int.of_int64 kt v, rest), qta - 1, ctxt)
| Float_of_int kf, Item (v, rest) ->
let v = Int64.to_float (Script_int.to_int64 kf v) in
return (Item (v, rest), qta - 1, ctxt)
logged_return (Item (Script_int.cast kt v, rest), qta - 1, ctxt)
(* protocol *)
| Manager, Item ((_, _, contract), rest) ->
Contract.get_manager ctxt contract >>=? fun manager ->
return (Item (manager, rest), qta - 1, ctxt)
| Transfer_tokens (storage_type, loc),
logged_return (Item (manager, rest), qta - 1, ctxt)
| Transfer_tokens storage_type,
Item (p, Item (amount, Item ((tp, Void_t, destination), Item (sto, Empty)))) -> begin
Contract.unconditional_spend ctxt source amount >>=? fun ctxt ->
Contract.credit ctxt destination amount >>=? fun ctxt ->
@ -491,9 +419,9 @@ let rec interp
| No_script -> assert false
| Script { storage = { storage } } ->
parse_untagged_data ctxt storage_type storage >>=? fun sto ->
return (Item ((), Item (sto, Empty)), qta - 1, ctxt))
logged_return (Item ((), Item (sto, Empty)), qta - 1, ctxt))
end
| Transfer_tokens (storage_type, loc),
| Transfer_tokens storage_type,
Item (p, Item (amount, Item ((tp, tr, destination), Item (sto, Empty)))) -> begin
Contract.unconditional_spend ctxt source amount >>=? fun ctxt ->
Contract.credit ctxt destination amount >>=? fun ctxt ->
@ -514,7 +442,7 @@ let rec interp
| No_script -> assert false
| Script { storage = { storage } } ->
parse_untagged_data ctxt storage_type storage >>=? fun sto ->
return (Item (v, Item (sto, Empty)), qta - 1, ctxt))
logged_return (Item (v, Item (sto, Empty)), qta - 1, ctxt))
end
| Create_account,
Item (manager, Item (delegate, Item (delegatable, Item (credit, rest)))) ->
@ -523,7 +451,7 @@ let rec interp
Contract.originate ctxt
~manager ~delegate ~balance
~script:No_script ~spendable:true ~delegatable >>=? fun (ctxt, contract) ->
return (Item ((Void_t, Void_t, contract), rest), qta - 1, ctxt)
logged_return (Item ((Void_t, Void_t, contract), rest), qta - 1, ctxt)
| Create_contract (g, p, r),
Item (manager, Item (delegate, Item (delegatable, Item (credit,
Item (Lam (_, code), Item (init, rest)))))) ->
@ -543,35 +471,43 @@ let rec interp
~manager ~delegate ~balance
~script:(Script { code ; storage }) ~spendable:true ~delegatable
>>=? fun (ctxt, contract) ->
return (Item ((p, r, contract), rest), qta - 1, ctxt)
logged_return (Item ((p, r, contract), rest), qta - 1, ctxt)
| Balance, rest ->
Contract.get_balance ctxt source >>=? fun balance ->
return (Item (balance, rest), qta - 1, ctxt)
logged_return (Item (balance, rest), qta - 1, ctxt)
| Now, rest ->
Timestamp.get_current ctxt >>=? fun now ->
return (Item (now, rest), qta - 1, ctxt)
logged_return (Item (now, rest), qta - 1, ctxt)
| Check_signature, Item (key, Item ((signature, message), rest)) ->
Public_key.get ctxt key >>=? fun key ->
let message = MBytes.of_string message in
let res = Ed25519.check_signature key signature message in
return (Item (res, rest), qta - 1, ctxt)
logged_return (Item (res, rest), qta - 1, ctxt)
| H ty, Item (v, rest) ->
let hash = Script.hash_expr (unparse_untagged_data ty v) in
return (Item (hash, rest), qta - 1, ctxt)
logged_return (Item (hash, rest), qta - 1, ctxt)
| Steps_to_quota, rest ->
let steps = Script_int.of_int64 Uint32 (Int64.of_int qta) in
return (Item (steps, rest), qta - 1, ctxt)
logged_return (Item (steps, rest), qta - 1, ctxt)
| Source (ta, tb), rest ->
return (Item ((ta, tb, orig), rest), qta - 1, ctxt)
logged_return (Item ((ta, tb, orig), rest), qta - 1, ctxt)
| Amount, rest ->
return (Item (amount, rest), qta - 1, ctxt)
logged_return (Item (amount, rest), qta - 1, ctxt)
in
step qta ctxt code (Item (arg, Empty)) >>=? fun (Item (ret, Empty), qta, ctxt) ->
let stack = (Item (arg, Empty)) in
begin match log with
| None -> ()
| Some log ->
log := (code.loc, qta, unparse_stack (stack, code.bef)) :: !log
end ;
step qta ctxt code stack >>=? fun (Item (ret, Empty), qta, ctxt) ->
return (ret, qta, ctxt)
(* ---- contract handling ---------------------------------------------------*)
and execute orig source ctxt { storage; storage_type } { code; arg_type; ret_type } amount arg qta =
and execute ?log orig source ctxt storage script amount arg qta =
let { Script.storage ; storage_type } = storage in
let { Script.code ; arg_type ; ret_type } = script in
parse_ty arg_type >>=? fun (Ex arg_type) ->
parse_ty ret_type >>=? fun (Ex ret_type) ->
parse_ty storage_type >>=? fun (Ex storage_type) ->
@ -580,8 +516,17 @@ and execute orig source ctxt { storage; storage_type } { code; arg_type; ret_typ
parse_lambda ctxt arg_type_full ret_type_full code >>=? fun lambda ->
parse_untagged_data ctxt arg_type arg >>=? fun arg ->
parse_untagged_data ctxt storage_type storage >>=? fun storage ->
interp qta orig source amount ctxt lambda ((amount, arg), storage) >>=? fun (ret, qta, ctxt) ->
interp ?log qta orig source amount ctxt lambda ((amount, arg), storage)
>>=? fun (ret, qta, ctxt) ->
let ret, storage = ret in
return (unparse_untagged_data storage_type storage,
unparse_untagged_data ret_type ret,
qta, ctxt)
let trace orig source ctxt storage script amount arg qta =
let log = ref [] in
execute ~log orig source ctxt storage script amount arg qta >>=? fun res ->
return (res, List.rev !log)
let execute orig source ctxt storage script amount arg qta =
execute orig source ctxt storage script amount arg qta

View File

@ -21,3 +21,9 @@ val execute: Contract.t -> Contract.t -> Tezos_context.t ->
Script.storage -> Script.code -> Tez.t ->
Script.expr -> int ->
(Script.expr * Script.expr * int * context) tzresult Lwt.t
val trace: Contract.t -> Contract.t -> Tezos_context.t ->
Script.storage -> Script.code -> Tez.t ->
Script.expr -> int ->
((Script.expr * Script.expr * int * context) *
(Script.location * int * Script.expr list) list) tzresult Lwt.t

File diff suppressed because it is too large Load Diff

View File

@ -29,7 +29,6 @@ let location_encoding =
type expr = (* TODO: turn the location into an alpha ? *)
| Int of location * string
| Float of location * string
| String of location * string
| Prim of location * string * expr list
| Seq of location * expr list
@ -38,8 +37,6 @@ let expr_encoding =
let open Data_encoding in
let int_encoding =
obj1 (req "int" string) in
let float_encoding =
obj1 (req "float" string) in
let string_encoding =
obj1 (req "string" string) in
let prim_encoding expr_encoding =
@ -65,25 +62,21 @@ let expr_encoding =
[ case ~tag:0 int_encoding
(function Int (_, v) -> Some v | _ -> None)
(fun v -> Int (-1, v)) ;
case ~tag:1 float_encoding
(function Float (_, v) -> Some v | _ -> None)
(fun v -> Float (-1, v)) ;
case ~tag:2 string_encoding
case ~tag:1 string_encoding
(function String (_, v) -> Some v | _ -> None)
(fun v -> String (-1, v)) ;
case ~tag:3 (prim_encoding expr_encoding)
case ~tag:2 (prim_encoding expr_encoding)
(function
| Prim (_, v, args) -> Some (v, args)
| _ -> None)
(function (prim, args) -> Prim (-1, prim, args)) ;
case ~tag:4 (seq_encoding expr_encoding)
case ~tag:3 (seq_encoding expr_encoding)
(function Seq (_, v) -> Some v | _ -> None)
(fun args -> Seq (-1, args)) ])
let update_locations ir =
let rec update_locations i = function
| Int (_, v) -> (Int (i, v), succ i)
| Float (_, v) -> (Float (i, v), succ i)
| String (_, v) -> (String (i, v), succ i)
| Prim (_, name, args) ->
let (nargs, ni) =
@ -99,7 +92,7 @@ let update_locations ir =
(narg :: nargs, ni))
([], succ i) args in
(Seq (i, List.rev nargs), ni) in
fst (update_locations 0 ir)
fst (update_locations 1 ir)
let expr_encoding =
Data_encoding.conv

View File

@ -14,7 +14,6 @@ type location =
type expr =
| Int of location * string
| Float of location * string
| String of location * string
| Prim of location * string * expr list
| Seq of location * expr list

View File

@ -10,6 +10,35 @@
open Tezos_context
open Script_int
(* ---- Auxiliary types -----------------------------------------------------*)
type 'ty comparable_ty =
| Int_key : ('s, 'l) int_kind -> ('s, 'l) int_val comparable_ty
| String_key : string comparable_ty
| Tez_key : Tez.t comparable_ty
| Bool_key : bool comparable_ty
| Key_key : public_key_hash comparable_ty
| Timestamp_key : Timestamp.t comparable_ty
module type Boxed_set = sig
type elt
module OPS : Set.S with type elt = elt
val boxed : OPS.t
end
type 'elt set = (module Boxed_set with type elt = 'elt)
module type Boxed_map = sig
type key
type value
val key_ty : key comparable_ty
module OPS : Map.S with type key = key
val boxed : value OPS.t
end
type ('key, 'value) map = (module Boxed_map with type key = 'key and type value = 'value)
type ('arg, 'ret, 'storage) script =
{ code : (((Tez.t, 'arg) pair, 'storage) pair, ('ret, 'storage) pair) lambda ;
arg_type : 'arg ty ;
@ -17,8 +46,6 @@ type ('arg, 'ret, 'storage) script =
storage : 'storage ;
storage_type : 'storage ty }
(* ---- Auxiliary types -----------------------------------------------------*)
and ('a, 'b) pair = 'a * 'b
and ('a, 'b) union = L of 'a | R of 'b
@ -26,26 +53,16 @@ and ('a, 'b) union = L of 'a | R of 'b
and end_of_stack = unit
and ('arg, 'ret) lambda =
Lam of ('arg * end_of_stack, 'ret * end_of_stack) instr * Script.expr
Lam of ('arg * end_of_stack, 'ret * end_of_stack) descr * Script.expr
and ('arg, 'ret) typed_contract =
'arg ty * 'ret ty * Contract.t
and 'ty comparable_ty =
| Int_key : ('s, 'l) int_kind -> ('s, 'l) int_val comparable_ty
| String_key : string comparable_ty
| Float_key : float comparable_ty
| Tez_key : Tez.t comparable_ty
| Bool_key : bool comparable_ty
| Key_key : public_key_hash comparable_ty
| Timestamp_key : Timestamp.t comparable_ty
and 'ty ty =
| Void_t : unit ty
| Int_t : ('s, 'l) int_kind -> ('s, 'l) int_val ty
| Signature_t : signature ty
| String_t : string ty
| Float_t : float ty
| Tez_t : Tez.t ty
| Key_t : public_key_hash ty
| Timestamp_t : Timestamp.t ty
@ -54,17 +71,14 @@ and 'ty ty =
| Union_t : 'a ty * 'b ty -> ('a, 'b) union ty
| Lambda_t : 'arg ty * 'ret ty -> ('arg, 'ret) lambda ty
| Option_t : 'v ty -> 'v option ty
| Ref_t : 'v ty -> 'v ref ty
| List_t : 'v ty -> 'v list ty
| Set_t : 'v comparable_ty -> 'v set ty
| Map_t : 'k comparable_ty * 'v ty -> ('k, 'v) map ty
| Contract_t : 'arg ty * 'ret ty -> ('arg, 'ret) typed_contract ty
and 'a set =
'a list ref * 'a comparable_ty (* FIXME: ok, this is bad *)
and ('a, 'b) map =
('a * 'b) list ref * 'a comparable_ty (* FIXME: we'll have to do better *)
and 'ty stack_ty =
| Item_t : 'ty ty * 'rest stack_ty -> ('ty * 'rest) stack_ty
| Empty_t : end_of_stack stack_ty
(* ---- Instructions --------------------------------------------------------*)
@ -97,24 +111,22 @@ and ('bef, 'aft) instr =
('v * 'rest, 'v option * 'rest) instr
| Cons_none : 'a ty ->
('rest, 'a option * 'rest) instr
| If_none : ('bef, 'aft) instr * ('a * 'bef, 'aft) instr ->
| If_none : ('bef, 'aft) descr * ('a * 'bef, 'aft) descr ->
('a option * 'bef, 'aft) instr
(* unions *)
| Left :
('l * 'rest, (('l, 'r) union * 'rest)) instr
| Right :
('r * 'rest, (('l, 'r) union * 'rest)) instr
| If_left : ('l * 'bef, 'aft) instr * ('r * 'bef, 'aft) instr ->
| If_left : ('l * 'bef, 'aft) descr * ('r * 'bef, 'aft) descr ->
(('l, 'r) union * 'bef, 'aft) instr
(* lists *)
| Cons_list :
('a * ('a list * 'rest), ('a list * 'rest)) instr
| Nil :
('rest, ('a list * 'rest)) instr
| If_cons : ('a * ('a list * 'bef), 'aft) instr * ('bef, 'aft) instr ->
| If_cons : ('a * ('a list * 'bef), 'aft) descr * ('bef, 'aft) descr ->
('a list * 'bef, 'aft) instr
| List_iter :
(('param, unit) lambda * ('param list * 'rest), 'rest) instr
| List_map :
(('param, 'ret) lambda * ('param list * 'rest), 'ret list * 'rest) instr
| List_reduce :
@ -123,8 +135,6 @@ and ('bef, 'aft) instr =
(* sets *)
| Empty_set : 'a comparable_ty ->
('rest, 'a set * 'rest) instr
| Set_iter :
(('param, unit) lambda * ('param set * 'rest), 'rest) instr
| Set_map : 'ret comparable_ty ->
(('param, 'ret) lambda * ('param set * 'rest), 'ret set * 'rest) instr
| Set_reduce :
@ -133,12 +143,10 @@ and ('bef, 'aft) instr =
| Set_mem :
('elt * ('elt set * 'rest), bool * 'rest) instr
| Set_update :
('elt * (bool * ('elt set * 'rest)), 'rest) instr
('elt * (bool * ('elt set * 'rest)), 'elt set * 'rest) instr
(* maps *)
| Empty_map : 'a comparable_ty * 'v ty ->
('rest, ('a, 'v) map * 'rest) instr
| Map_iter :
(('a * 'v, unit) lambda * (('a, 'v) map * 'rest), 'rest) instr
| Map_map :
(('a * 'v, 'r) lambda * (('a, 'v) map * 'rest), ('a, 'r) map * 'rest) instr
| Map_reduce :
@ -149,25 +157,14 @@ and ('bef, 'aft) instr =
| Map_get :
('a * (('a, 'v) map * 'rest), 'v option * 'rest) instr
| Map_update :
('a * ('v option * (('a, 'v) map * 'rest)), 'rest) instr
(* reference cells *)
| Ref :
('v * 'rest, 'v ref * 'rest) instr
| Deref :
('v ref * 'rest, 'v * 'rest) instr
| Set :
('v ref * ('v * 'rest), 'rest) instr
('a * ('v option * (('a, 'v) map * 'rest)), ('a, 'v) map * 'rest) instr
(* string operations *)
| Concat :
(string * (string * 'rest), string * 'rest) instr
(* timestamp operations *)
| Add_period_to_timestamp :
(float * (Timestamp.t * 'rest), Timestamp.t * 'rest) instr
| Add_seconds_to_timestamp : (unsigned, 'l) int_kind * Script.location ->
| Add_seconds_to_timestamp : (unsigned, 'l) int_kind ->
((unsigned, 'l) int_val * (Timestamp.t * 'rest), Timestamp.t * 'rest) instr
| Add_timestamp_to_period :
(Timestamp.t * (float * 'rest), Timestamp.t * 'rest) instr
| Add_timestamp_to_seconds : (unsigned, 'l) int_kind * Script.location ->
| Add_timestamp_to_seconds : (unsigned, 'l) int_kind ->
(Timestamp.t * ((unsigned, 'l) int_val * 'rest), Timestamp.t * 'rest) instr
(* currency operations *)
| Add_tez :
@ -178,33 +175,6 @@ and ('bef, 'aft) instr =
(Tez.t * ((unsigned, 'l) int_val * 'rest), Tez.t * 'rest) instr
| Mul_tez' : (unsigned, 'l) int_kind ->
((unsigned, 'l) int_val * (Tez.t * 'rest), Tez.t * 'rest) instr
(* float operations *)
| Neg_float :
(float * 'rest, float * 'rest) instr
| Abs_float :
(float * 'rest, float * 'rest) instr
| Add_float :
(float * (float * 'rest), float * 'rest) instr
| Sub_float :
(float * (float * 'rest), float * 'rest) instr
| Mul_float :
(float * (float * 'rest), float * 'rest) instr
| Div_float :
(float * (float * 'rest), float * 'rest) instr
| Mod_float :
(float * (float * 'rest), float * 'rest) instr
| Floor :
(float * 'rest, float * 'rest) instr
| Ceil :
(float * 'rest, float * 'rest) instr
| Inf :
('rest, float * 'rest) instr
| NaN :
('rest, float * 'rest) instr
| IsNaN :
(float * 'rest, bool * 'rest) instr
| NaNaN : Script.location ->
(float * 'rest, 'rest) instr
(* boolean operations *)
| Or :
(bool * (bool * 'rest), bool * 'rest) instr
@ -215,15 +185,15 @@ and ('bef, 'aft) instr =
| Not :
(bool * 'rest, bool * 'rest) instr
(* integer operations *)
| Checked_neg_int : (signed, 'l) int_kind * Script.location ->
| Checked_neg_int : (signed, 'l) int_kind ->
((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr
| Checked_abs_int : (signed, 'l) int_kind * Script.location ->
| Checked_abs_int : (signed, 'l) int_kind ->
((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr
| Checked_add_int : ('s, 'l) int_kind * Script.location ->
| Checked_add_int : ('s, 'l) int_kind ->
(('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
| Checked_sub_int : ('s, 'l) int_kind * Script.location ->
| Checked_sub_int : ('s, 'l) int_kind ->
(('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
| Checked_mul_int : ('s, 'l) int_kind * Script.location ->
| Checked_mul_int : ('s, 'l) int_kind ->
(('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
| Neg_int : (signed, 'l) int_kind ->
((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr
@ -235,9 +205,9 @@ and ('bef, 'aft) instr =
(('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
| Mul_int : ('s, 'l) int_kind ->
(('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
| Div_int : ('s, 'l) int_kind * Script.location ->
| Div_int : ('s, 'l) int_kind ->
(('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
| Mod_int : ('s, 'l) int_kind * Script.location ->
| Mod_int : ('s, 'l) int_kind ->
(('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
| Lsl_int : (unsigned, 'l) int_kind ->
((unsigned, 'l) int_val * ((unsigned, eight) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr
@ -252,20 +222,20 @@ and ('bef, 'aft) instr =
| Not_int : (unsigned, 'l) int_kind ->
((unsigned, 'l) int_val * 'rest, (unsigned, 'l) int_val * 'rest) instr
(* control *)
| Seq : ('bef, 'trans) instr * ('trans, 'aft) instr ->
| Seq : ('bef, 'trans) descr * ('trans, 'aft) descr ->
('bef, 'aft) instr
| If : ('bef, 'aft) instr * ('bef, 'aft) instr ->
| If : ('bef, 'aft) descr * ('bef, 'aft) descr ->
(bool * 'bef, 'aft) instr
| Loop : ('rest, bool * 'rest) instr ->
| Loop : ('rest, bool * 'rest) descr ->
(bool * 'rest, 'rest) instr
| Dip : ('bef, 'aft) instr ->
| Dip : ('bef, 'aft) descr ->
('top * 'bef, 'top * 'aft) instr
| Exec :
('arg * (('arg, 'ret) lambda * 'rest), 'ret * 'rest) instr
| Lambda : ('arg, 'ret) lambda ->
('rest, ('arg, 'ret) lambda * 'rest) instr
| Fail : Script.location ->
('rest, 'rest) instr
| Fail :
('bef, 'aft) instr
| Nop :
('rest, 'rest) instr
(* comparison *)
@ -287,16 +257,12 @@ and ('bef, 'aft) instr =
(* casts *)
| Int_of_int : ('sf, 'lf) int_kind * ('st, 'lt) int_kind ->
(('sf, 'lf) int_val * 'rest, ('st, 'lt) int_val * 'rest) instr
| Checked_int_of_int : ('sf, 'lf) int_kind * ('st, 'lt) int_kind * Script.location ->
| Checked_int_of_int : ('sf, 'lf) int_kind * ('st, 'lt) int_kind ->
(('sf, 'lf) int_val * 'rest, ('st, 'lt) int_val * 'rest) instr
| Int_of_float : ('st, 'lt) int_kind ->
(float * 'rest, ('st, 'lt) int_val * 'rest) instr
| Float_of_int : ('sf, 'lf) int_kind ->
(('sf, 'lf) int_val * 'rest, float * 'rest) instr
(* protocol *)
| Manager :
(('arg, 'ret) typed_contract * 'rest, public_key_hash * 'rest) instr
| Transfer_tokens : 'sto ty * Script.location ->
| Transfer_tokens : 'sto ty ->
('arg * (Tez.t * (('arg, 'ret) typed_contract * ('sto * end_of_stack))), 'ret * ('sto * end_of_stack)) instr
| Create_account :
(public_key_hash * (public_key_hash option * (bool * (Tez.t * 'rest))),
@ -319,3 +285,9 @@ and ('bef, 'aft) instr =
('rest, ('p, 'r) typed_contract * 'rest) instr
| Amount :
('rest, Tez.t * 'rest) instr
and ('bef, 'aft) descr =
{ loc : Script.location ;
bef : 'bef stack_ty ;
aft : 'aft stack_ty ;
instr : ('bef, 'aft) instr }

View File

@ -1,321 +0,0 @@
(**************************************************************************)
(* *)
(* Copyright (c) 2014 - 2016. *)
(* Dynamic Ledger Solutions, Inc. <contact@tezos.com> *)
(* *)
(* All rights reserved. No warranty, explicit or implicit, provided. *)
(* *)
(**************************************************************************)
open Tezos_context
open Script_int
type ('arg, 'ret, 'storage) script =
{ code : (((Tez.t, 'arg) pair, 'storage) pair, ('ret, 'storage) pair) lambda ;
arg_type : 'arg ty ;
ret_type : 'ret ty ;
storage : 'storage ;
storage_type : 'storage ty }
(* ---- Auxiliary types -----------------------------------------------------*)
and ('a, 'b) pair = 'a * 'b
and ('a, 'b) union = L of 'a | R of 'b
and end_of_stack = unit
and ('arg, 'ret) lambda =
Lam of ('arg * end_of_stack, 'ret * end_of_stack) instr * Script.expr
and ('arg, 'ret) typed_contract =
'arg ty * 'ret ty * Contract.t
and 'ty comparable_ty =
| Int_key : ('s, 'l) int_kind -> ('s, 'l) int_val comparable_ty
| String_key : string comparable_ty
| Float_key : float comparable_ty
| Tez_key : Tez.t comparable_ty
| Bool_key : bool comparable_ty
| Key_key : public_key_hash comparable_ty
| Timestamp_key : Time.t comparable_ty
and 'ty ty =
| Void_t : unit ty
| Int_t : ('s, 'l) int_kind -> ('s, 'l) int_val ty
| Signature_t : signature ty
| String_t : string ty
| Float_t : float ty
| Tez_t : Tez.t ty
| Key_t : public_key_hash ty
| Timestamp_t : Time.t ty
| Bool_t : bool ty
| Pair_t : 'a ty * 'b ty -> ('a, 'b) pair ty
| Union_t : 'a ty * 'b ty -> ('a, 'b) union ty
| Lambda_t : 'arg ty * 'ret ty -> ('arg, 'ret) lambda ty
| Option_t : 'v ty -> 'v option ty
| Ref_t : 'v ty -> 'v ref ty
| List_t : 'v ty -> 'v list ty
| Set_t : 'v comparable_ty -> 'v set ty
| Map_t : 'k comparable_ty * 'v ty -> ('k, 'v) map ty
| Contract_t : 'arg ty * 'ret ty -> ('arg, 'ret) typed_contract ty
and 'a set =
'a list ref * 'a comparable_ty (* FIXME: ok, this is bad *)
and ('a, 'b) map =
('a * 'b) list ref * 'a comparable_ty (* FIXME: we'll have to do better *)
(* ---- Instructions --------------------------------------------------------*)
(* The low-level, typed instructions, as a GADT whose parameters
encode the typing rules. The eft parameter is the typed shape of
the stack before the instruction, the right one the shape
after. Any program whose construction is accepted by OCaml's
type-checker is guaranteed to be type-safe. Overloadings of the
concrete syntax are already resolved in this representation, either
by using different constructors or type witness parameters. *)
and ('bef, 'aft) instr =
(* stack ops *)
| Drop :
(_ * 'rest, 'rest) instr
| Dup :
('top * 'rest, 'top * ('top * 'rest)) instr
| Swap :
('tip * ('top * 'rest), 'top * ('tip * 'rest)) instr
| Const : 'ty ->
('rest, ('ty * 'rest)) instr
(* pairs *)
| Cons_pair :
(('car * ('cdr * 'rest)), (('car, 'cdr) pair * 'rest)) instr
| Car :
(('car, _) pair * 'rest, 'car * 'rest) instr
| Cdr :
((_, 'cdr) pair * 'rest, 'cdr * 'rest) instr
(* options *)
| Cons_some :
('v * 'rest, 'v option * 'rest) instr
| Cons_none : 'a ty ->
('rest, 'a option * 'rest) instr
| If_none : ('bef, 'aft) instr * ('a * 'bef, 'aft) instr ->
('a option * 'bef, 'aft) instr
(* unions *)
| Left :
('l * 'rest, (('l, 'r) union * 'rest)) instr
| Right :
('r * 'rest, (('l, 'r) union * 'rest)) instr
| If_left : ('l * 'bef, 'aft) instr * ('r * 'bef, 'aft) instr ->
(('l, 'r) union * 'bef, 'aft) instr
(* lists *)
| Cons_list :
('a * ('a list * 'rest), ('a list * 'rest)) instr
| Nil :
('rest, ('a list * 'rest)) instr
| If_cons : ('a * ('a list * 'bef), 'aft) instr * ('bef, 'aft) instr ->
('a list * 'bef, 'aft) instr
| List_iter :
(('param, unit) lambda * ('param list * 'rest), 'rest) instr
| List_map :
(('param, 'ret) lambda * ('param list * 'rest), 'ret list * 'rest) instr
| List_reduce :
(('param * 'res, 'res) lambda *
('param list * ('res * 'rest)), 'res * 'rest) instr
(* sets *)
| Empty_set : 'a comparable_ty ->
('rest, 'a set * 'rest) instr
| Set_iter :
(('param, unit) lambda * ('param set * 'rest), 'rest) instr
| Set_map : 'ret comparable_ty ->
(('param, 'ret) lambda * ('param set * 'rest), 'ret set * 'rest) instr
| Set_reduce :
(('param * 'res, 'res) lambda *
('param set * ('res * 'rest)), 'res * 'rest) instr
| Set_mem :
('elt * ('elt set * 'rest), bool * 'rest) instr
| Set_update :
('elt * (bool * ('elt set * 'rest)), 'rest) instr
(* maps *)
| Empty_map : 'a comparable_ty * 'v ty ->
('rest, ('a, 'v) map * 'rest) instr
| Map_iter :
(('a * 'v, unit) lambda * (('a, 'v) map * 'rest), 'rest) instr
| Map_map :
(('a * 'v, 'r) lambda * (('a, 'v) map * 'rest), ('a, 'r) map * 'rest) instr
| Map_reduce :
((('a * 'v) * 'res, 'res) lambda *
(('a, 'v) map * ('res * 'rest)), 'res * 'rest) instr
| Map_mem :
('a * (('a, 'v) map * 'rest), bool * 'rest) instr
| Map_get :
('a * (('a, 'v) map * 'rest), 'v option * 'rest) instr
| Map_update :
('a * ('v option * (('a, 'v) map * 'rest)), 'rest) instr
(* reference cells *)
| Ref :
('v * 'rest, 'v ref * 'rest) instr
| Deref :
('v ref * 'rest, 'v * 'rest) instr
| Set :
('v ref * ('v * 'rest), 'rest) instr
(* string operations *)
| Concat :
(string * (string * 'rest), string * 'rest) instr
(* timestamp operations *)
| Add_period_to_timestamp :
(float * (Time.t * 'rest), Time.t * 'rest) instr
| Add_seconds_to_timestamp : (unsigned, 'l) int_kind * Script.location ->
((unsigned, 'l) int_val * (Time.t * 'rest), Time.t * 'rest) instr
| Add_timestamp_to_period :
(Time.t * (float * 'rest), Time.t * 'rest) instr
| Add_timestamp_to_seconds : (unsigned, 'l) int_kind * Script.location ->
(Time.t * ((unsigned, 'l) int_val * 'rest), Time.t * 'rest) instr
(* currency operations *)
| Add_tez :
(Tez.t * (Tez.t * 'rest), Tez.t * 'rest) instr
| Sub_tez :
(Tez.t * (Tez.t * 'rest), Tez.t * 'rest) instr
| Mul_tez : (unsigned, 'l) int_kind ->
(Tez.t * ((unsigned, 'l) int_val * 'rest), Tez.t * 'rest) instr
| Mul_tez' : (unsigned, 'l) int_kind ->
((unsigned, 'l) int_val * (Tez.t * 'rest), Tez.t * 'rest) instr
(* float operations *)
| Neg_float :
(float * 'rest, float * 'rest) instr
| Abs_float :
(float * 'rest, float * 'rest) instr
| Add_float :
(float * (float * 'rest), float * 'rest) instr
| Sub_float :
(float * (float * 'rest), float * 'rest) instr
| Mul_float :
(float * (float * 'rest), float * 'rest) instr
| Div_float :
(float * (float * 'rest), float * 'rest) instr
| Mod_float :
(float * (float * 'rest), float * 'rest) instr
| Floor :
(float * 'rest, float * 'rest) instr
| Ceil :
(float * 'rest, float * 'rest) instr
| Inf :
('rest, float * 'rest) instr
| NaN :
('rest, float * 'rest) instr
| IsNaN :
(float * 'rest, bool * 'rest) instr
| NaNaN : Script.location ->
(float * 'rest, 'rest) instr
(* boolean operations *)
| Or :
(bool * (bool * 'rest), bool * 'rest) instr
| And :
(bool * (bool * 'rest), bool * 'rest) instr
| Xor :
(bool * (bool * 'rest), bool * 'rest) instr
| Not :
(bool * 'rest, bool * 'rest) instr
(* integer operations *)
| Checked_neg_int : (signed, 'l) int_kind * Script.location ->
((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr
| Checked_abs_int : (signed, 'l) int_kind * Script.location ->
((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr
| Checked_add_int : ('s, 'l) int_kind * Script.location ->
(('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
| Checked_sub_int : ('s, 'l) int_kind * Script.location ->
(('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
| Checked_mul_int : ('s, 'l) int_kind * Script.location ->
(('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
| Neg_int : (signed, 'l) int_kind ->
((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr
| Abs_int : (signed, 'l) int_kind ->
((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr
| Add_int : ('s, 'l) int_kind ->
(('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
| Sub_int : ('s, 'l) int_kind ->
(('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
| Mul_int : ('s, 'l) int_kind ->
(('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
| Div_int : ('s, 'l) int_kind * Script.location ->
(('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
| Mod_int : ('s, 'l) int_kind * Script.location ->
(('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
| Lsl_int : (unsigned, 'l) int_kind ->
((unsigned, 'l) int_val * ((unsigned, eight) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr
| Lsr_int : (unsigned, 'l) int_kind ->
((unsigned, 'l) int_val * ((unsigned, eight) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr
| Or_int : (unsigned, 'l) int_kind ->
((unsigned, 'l) int_val * ((unsigned, 'l) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr
| And_int : (unsigned, 'l) int_kind ->
((unsigned, 'l) int_val * ((unsigned, 'l) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr
| Xor_int : (unsigned, 'l) int_kind ->
((unsigned, 'l) int_val * ((unsigned, 'l) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr
| Not_int : (unsigned, 'l) int_kind ->
((unsigned, 'l) int_val * 'rest, (unsigned, 'l) int_val * 'rest) instr
(* control *)
| Seq : ('bef, 'trans) instr * ('trans, 'aft) instr ->
('bef, 'aft) instr
| If : ('bef, 'aft) instr * ('bef, 'aft) instr ->
(bool * 'bef, 'aft) instr
| Loop : ('rest, bool * 'rest) instr ->
(bool * 'rest, 'rest) instr
| Dip : ('bef, 'aft) instr ->
('top * 'bef, 'top * 'aft) instr
| Exec :
('arg * (('arg, 'ret) lambda * 'rest), 'ret * 'rest) instr
| Lambda : ('arg, 'ret) lambda ->
('rest, ('arg, 'ret) lambda * 'rest) instr
| Fail : Script.location ->
('rest, 'rest) instr
| Nop :
('rest, 'rest) instr
(* comparison *)
| Compare : 'a comparable_ty ->
('a * ('a * 'rest), (signed, sixtyfour) int_val * 'rest) instr
(* comparators *)
| Eq :
((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr
| Neq :
((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr
| Lt :
((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr
| Gt :
((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr
| Le :
((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr
| Ge :
((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr
(* casts *)
| Int_of_int : ('sf, 'lf) int_kind * ('st, 'lt) int_kind ->
(('sf, 'lf) int_val * 'rest, ('st, 'lt) int_val * 'rest) instr
| Checked_int_of_int : ('sf, 'lf) int_kind * ('st, 'lt) int_kind * Script.location ->
(('sf, 'lf) int_val * 'rest, ('st, 'lt) int_val * 'rest) instr
| Int_of_float : ('st, 'lt) int_kind ->
(float * 'rest, ('st, 'lt) int_val * 'rest) instr
| Float_of_int : ('sf, 'lf) int_kind ->
(('sf, 'lf) int_val * 'rest, float * 'rest) instr
(* protocol *)
| Manager :
(('arg, 'ret) typed_contract * 'rest, public_key_hash * 'rest) instr
| Transfer_tokens : 'sto ty * Script.location ->
('arg * (Tez.t * (('arg, 'ret) typed_contract * ('sto * end_of_stack))), 'ret * ('sto * end_of_stack)) instr
| Create_account :
(public_key_hash * (public_key_hash option * (bool * (Tez.t * 'rest))),
(unit, unit) typed_contract * 'rest) instr
| Create_contract : 'g ty * 'p ty * 'r ty ->
(public_key_hash * (public_key_hash option * (bool * (Tez.t *
(((Tez.t * 'p) * 'g, 'r * 'g) lambda * ('g * 'rest))))),
('p, 'r) typed_contract * 'rest) instr
| Now :
('rest, Time.t * 'rest) instr
| Balance :
('rest, Tez.t * 'rest) instr
| Check_signature :
(public_key_hash * ((signature * string) * 'rest), bool * 'rest) instr
| H : 'a ty ->
('a * 'rest, string * 'rest) instr
| Steps_to_quota :
('rest, (unsigned, thirtytwo) int_val * 'rest) instr
| Source : 'p ty * 'r ty ->
('rest, ('p, 'r) typed_contract * 'rest) instr
| Amount :
('rest, Tez.t * 'rest) instr

View File

@ -327,11 +327,45 @@ module Helpers = struct
obj1 (req "timestamp" Timestamp.encoding))
RPC.Path.(custom_root / "helpers" / "minimal_timestamp")
let run_code_input_encoding =
(obj5
(req "script" Script.code_encoding)
(req "storage" Script.expr_encoding)
(req "input" Script.expr_encoding)
(opt "amount" Tez.encoding)
(opt "contract" Contract.encoding))
let run_code custom_root =
RPC.service
~description: "Run a piece of code in the current context"
~input: run_code_input_encoding
~output: (wrap_tzerror
(obj2
(req "storage" Script.expr_encoding)
(req "output" Script.expr_encoding)))
RPC.Path.(custom_root / "helpers" / "run_code")
let trace_code custom_root =
RPC.service
~description: "Run a piece of code in the current context, \
keeping a trace"
~input: run_code_input_encoding
~output: (wrap_tzerror
(obj3
(req "storage" Script.expr_encoding)
(req "output" Script.expr_encoding)
(req "trace"
(list @@ obj3
(req "location" Script.location_encoding)
(req "gas" int31)
(req "stack" (list (Script.expr_encoding)))))))
RPC.Path.(custom_root / "helpers" / "trace_code")
let typecheck_code custom_root =
RPC.service
~description: "Typecheck a piece of code in the current context"
~input: Script.code_encoding
~output: (wrap_tzerror empty)
~output: (wrap_tzerror Script_ir_translator.type_map_enc)
RPC.Path.(custom_root / "helpers" / "typecheck_code")
let typecheck_tagged_data custom_root =

View File

@ -179,6 +179,47 @@ let minimal_timestamp ctxt prio =
let () = register1 Services.Helpers.minimal_timestamp minimal_timestamp
let () =
let run_parameters ctxt (script, storage, input, amount, contract) =
let amount =
match amount with
| Some amount -> amount
| None ->
match Tez.of_cents 100_00L with
| Some tez -> tez
| None -> Tez.zero in
let contract =
match contract with
| Some contract -> contract
| None ->
Contract.default_contract
(List.hd Bootstrap.accounts).Bootstrap.public_key_hash in
let storage : Script.storage =
{ storage ; storage_type = (script : Script.code).storage_type } in
let qta =
Constants.instructions_per_transaction ctxt in
(script, storage, input, amount, contract, qta) in
register1 Services.Helpers.run_code
(fun ctxt parameters ->
let (script, storage, input, amount, contract, qta) =
run_parameters ctxt parameters in
Script_interpreter.execute
contract (* transaction initiator *)
contract (* script owner *)
ctxt storage script amount input
qta >>=? fun (sto, ret, _qta, _ctxt) ->
Error_monad.return (sto, ret)) ;
register1 Services.Helpers.trace_code
(fun ctxt parameters ->
let (script, storage, input, amount, contract, qta) =
run_parameters ctxt parameters in
Script_interpreter.trace
contract (* transaction initiator *)
contract (* script owner *)
ctxt storage script amount input
qta >>=? fun ((sto, ret, _qta, _ctxt), trace) ->
Error_monad.return (sto, ret, trace))
let () =
register1 Services.Helpers.typecheck_code
Script_ir_translator.typecheck_code

View File

@ -109,7 +109,6 @@ module Script : sig
type expr =
| Int of location * string
| Float of location * string
| String of location * string
| Prim of location * string * expr list
| Seq of location * expr list