Big_map support

Add big_map case in the uncompiler which takes the original big_map and apply the returned diff

Add input_to_value option which compiles input expressions to mini_c.values
This commit is contained in:
Lesenechal Remi 2019-09-13 20:30:09 +02:00
parent 304184bcd3
commit b653996aae
7 changed files with 140 additions and 67 deletions

View File

@ -6,19 +6,19 @@ open Protocol
open Script_typed_ir
open Script_ir_translator
let rec translate_value (Ex_typed_value (ty, value)) : value result =
let rec translate_value ?bm_opt (Ex_typed_value (ty, value)) : value result =
match (ty, value) with
| Pair_t ((a_ty, _, _), (b_ty, _, _), _), (a, b) -> (
let%bind a = translate_value @@ Ex_typed_value(a_ty, a) in
let%bind b = translate_value @@ Ex_typed_value(b_ty, b) in
let%bind a = translate_value ?bm_opt @@ Ex_typed_value(a_ty, a) in
let%bind b = translate_value ?bm_opt @@ Ex_typed_value(b_ty, b) in
ok @@ D_pair(a, b)
)
| Union_t ((a_ty, _), _, _), L a -> (
let%bind a = translate_value @@ Ex_typed_value(a_ty, a) in
let%bind a = translate_value ?bm_opt @@ Ex_typed_value(a_ty, a) in
ok @@ D_left a
)
| Union_t (_, (b_ty, _), _), R b -> (
let%bind b = translate_value @@ Ex_typed_value(b_ty, b) in
let%bind b = translate_value ?bm_opt @@ Ex_typed_value(b_ty, b) in
ok @@ D_right b
)
| (Int_t _), n ->
@ -71,6 +71,28 @@ let rec translate_value (Ex_typed_value (ty, value)) : value result =
bind_map_list aux lst
in
ok @@ D_map lst'
| (Big_map_t (k_cty, v_ty, _)), m ->
let k_ty = Script_ir_translator.ty_of_comparable_ty k_cty in
let lst =
let aux k v acc = (k, v) :: acc in
let lst = Script_ir_translator.map_fold aux m.diff [] in
List.rev lst in
let%bind original_big_map =
match bm_opt with
| Some (D_big_map l) -> ok @@ l
| _ -> fail @@ simple_error "Do not have access to the original big_map" in
let%bind lst' =
let aux orig (k, v) =
let%bind k' = translate_value (Ex_typed_value (k_ty, k)) in
let orig_rem = List.remove_assoc k' orig in
match v with
| Some vadd ->
let%bind v' = translate_value (Ex_typed_value (v_ty, vadd)) in
if (List.mem_assoc k' orig) then ok @@ (k', v')::orig_rem
else ok @@ (k', v')::orig
| None -> ok orig_rem in
bind_fold_list aux original_big_map lst in
ok @@ D_big_map lst'
| (List_t (ty, _)), lst ->
let%bind lst' =
let aux = fun t -> translate_value (Ex_typed_value (ty, t)) in

View File

@ -1,4 +1,3 @@
// type storage_ is big_map(int, int)
type storage_ is big_map(int, int) * unit
function main(const p : unit; const s : storage_) : list(operation) * storage_ is
@ -10,15 +9,6 @@ function main(const p : unit; const s : storage_) : list(operation) * storage_ i
}
with ((nil: list(operation)), s)
// type foobar is map(int, int)
// const fb : foobar = map
// 23 -> 0 ;
// 42 -> 0 ;
// end
function set_ (var n : int ; var m : storage_) : storage_ is block {
var tmp : big_map(int,int) := m.0 ;
tmp[23] := n ;
@ -31,10 +21,6 @@ function rm (var m : storage_) : storage_ is block {
m.0 := tmp;
} with m
// not supported
// function size_ (const m : storage_) : nat is
// block {skip} with (size(m.0))
function gf (const m : storage_) : int is begin skip end with get_force(23, m.0)
function get (const m : storage_) : option(int) is
@ -42,7 +28,9 @@ function get (const m : storage_) : option(int) is
skip
end with m.0[42]
// const bm : storage_ = map
// the following is not supported (negative test cases):
// const bm : storage_ = big_map
// 144 -> 23 ;
// 51 -> 23 ;
// 42 -> 23 ;
@ -50,7 +38,15 @@ function get (const m : storage_) : option(int) is
// 421 -> 23 ;
// end
// not supported
// type foobar is big_map(int, int)
// const fb : foobar = big_map
// 23 -> 0 ;
// 42 -> 0 ;
// end
// function size_ (const m : storage_) : nat is
// block {skip} with (size(m.0))
// function iter_op (const m : storage_) : int is
// var r : int := 0 ;
// function aggregate (const i : int ; const j : int) : unit is block { r := r + i + j } with unit ;

View File

@ -23,7 +23,7 @@ let run_aux ?options (program:compiled_program) (input_michelson:Michelson.t) :
Memory_proto_alpha.interpret ?options descr (Item(input, Empty)) in
ok (Ex_typed_value (output_ty, output))
let run_entry ?(debug_michelson = false) ?options (entry:anon_function) ty (input:value) : value result =
let run_entry ?(debug_michelson = false) ?options ?bm_opt (entry:anon_function) ty (input:value) : value result =
let%bind compiled =
let error =
let title () = "compile entry" in
@ -51,5 +51,5 @@ let run_entry ?(debug_michelson = false) ?options (entry:anon_function) ty (inpu
Format.printf "Compiled Output: %a\n" Michelson.pp michelson_value ;
ok ()
) ;
let%bind (result : value) = Compiler.Uncompiler.translate_value ex_ty_value in
let%bind (result : value) = Compiler.Uncompiler.translate_value ?bm_opt ex_ty_value in
ok result

View File

@ -1,7 +1,7 @@
open Trace
let run_simplityped
?options
?input_to_value ?options
?(debug_mini_c = false) ?(debug_michelson = false)
(program : Ast_typed.program) (entry : string)
(input : Ast_simplified.expression) : Ast_simplified.expression result =
@ -13,7 +13,7 @@ let run_simplityped
in
Typer.type_expression env input in
let%bind typed_result =
Run_typed.run_typed ?options ~debug_mini_c ~debug_michelson entry program typed_input in
Run_typed.run_typed ?input_to_value ?options ~debug_mini_c ~debug_michelson entry program typed_input in
let%bind annotated_result = Typer.untype_expression typed_result in
ok annotated_result

View File

@ -30,8 +30,84 @@ let evaluate_typed
Transpiler.untranspile result typed_main.type_annotation in
ok typed_result
(* returns a big_map if any *)
let rec fetch_big_map (v: Mini_c.value) : Mini_c.value option =
match v with
| D_pair (l , r) ->
begin
match (fetch_big_map l) with
| Some _ as s -> s
| None -> fetch_big_map r
end
| D_big_map _ as bm -> Some bm
| _ -> let () = Printf.printf "lal\n" in None
(* try to convert expression to a literal *)
let rec exp_to_value (exp: Mini_c.expression) : Mini_c.value result =
let open! Mini_c in
match exp.content with
| E_literal v -> ok @@ v
| E_constant ("map" , lst) ->
let aux el =
let%bind l = exp_to_value el in
match l with
| D_pair (a , b) -> ok @@ (a , b)
| _ -> fail @@ simple_error "??" in
let%bind lstl = bind_map_list aux lst in
ok @@ D_map lstl
| E_constant ("big_map" , lst) ->
let aux el =
let%bind l = exp_to_value el in
match l with
| D_pair (a , b) -> ok @@ (a , b)
| _ -> fail @@ simple_error "??" in
let%bind lstl = bind_map_list aux lst in
ok @@ D_big_map lstl
| E_constant ("PAIR" , fst::snd::[]) ->
let%bind fstl = exp_to_value fst in
let%bind sndl = exp_to_value snd in
ok @@ D_pair (fstl , sndl)
| E_constant ("UPDATE", _) ->
let rec handle_prev upd =
match upd.content with
| E_constant ("UPDATE" , [k;v;prev]) ->
begin
match v.content with
| E_constant ("SOME" , [i]) ->
let%bind kl = exp_to_value k in
let%bind il = exp_to_value i in
let%bind prevl = handle_prev prev in
ok @@ (kl,il)::prevl
| E_constant ("NONE" , []) ->
let%bind prevl = handle_prev prev in
ok @@ prevl
| _ -> failwith "UPDATE second parameter is not an option"
end
| E_make_empty_map _ ->
ok @@ []
| _ -> failwith "impossible"
in
begin
match exp.type_value with
| T_big_map _ ->
let%bind kvl = handle_prev exp in
ok @@ D_big_map kvl
| T_map _ ->
let%bind kvl = handle_prev exp in
ok @@ D_map kvl
| _ -> failwith "UPDATE with a non-map type_value"
end
| _ ->
fail @@ simple_error "Can not convert expression to literal"
let convert_to_literals (e:Ast_typed.annotated_expression) : Mini_c.value result =
let open Transpiler in
let%bind exp = translate_annotated_expression e in (*Mini_c.expression*)
let%bind value = exp_to_value exp in
ok @@ value
let run_typed
?(debug_mini_c = false) ?(debug_michelson = false) ?options (entry:string)
?(input_to_value = false) ?(debug_mini_c = false) ?(debug_michelson = false) ?options (entry:string)
(program:Ast_typed.program) (input:Ast_typed.annotated_expression) : Ast_typed.annotated_expression result =
let%bind () =
let open Ast_typed in
@ -49,7 +125,9 @@ let run_typed
Format.(printf "Mini_c : %a\n%!" Mini_c.PP.function_ mini_c_main)
) ;
let%bind mini_c_value = transpile_value input in
let%bind mini_c_value = if input_to_value then
convert_to_literals input else transpile_value input in
let bm_opt = if input_to_value then fetch_big_map mini_c_value else None in
let%bind mini_c_result =
let error =
@ -59,7 +137,7 @@ let run_typed
in
error title content in
trace error @@
Run_mini_c.run_entry ~debug_michelson ?options mini_c_main ty mini_c_value in
Run_mini_c.run_entry ~debug_michelson ?options ?bm_opt mini_c_main ty mini_c_value in
let%bind typed_result =
let%bind main_result_type =
let%bind typed_main = Ast_typed.get_functional_entry program entry in

View File

@ -402,16 +402,7 @@ let big_map () : unit result =
let%bind () =
let make_input = fun n -> ez [(23, n) ; (42, 4)] in
let make_expected = e_int in
expect_eq_n program "gf" make_input make_expected
in
(* let%bind () =
let make_input = fun n -> ez List.(map (fun x -> (x, x)) @@ range n) in
let make_expected = e_nat in
expect_eq_n_strict_pos_small program "size_" make_input make_expected
in
let%bind () =
let expected = ez [(23, 0) ; (42, 0)] in
expect_eq_evaluate program "fb" expected
expect_eq_n ?input_to_value:(Some true) program "gf" make_input make_expected
in
let%bind () =
let make_input = fun n ->
@ -419,32 +410,18 @@ let big_map () : unit result =
e_tuple [(e_int n) ; m]
in
let make_expected = fun n -> ez [(23 , n) ; (42 , 0)] in
expect_eq_n_pos_small program "set_" make_input make_expected
expect_eq_n_pos_small ?input_to_value:(Some true) program "set_" make_input make_expected
in
let%bind () =
let make_input = fun n -> ez [(23, n) ; (42, 4)] in
let make_expected = fun _ -> e_some @@ e_int 4 in
expect_eq_n program "get" make_input make_expected
in
let%bind () =
let expected = ez @@ List.map (fun x -> (x, 23)) [144 ; 51 ; 42 ; 120 ; 421] in
expect_eq_evaluate program "bm" expected
expect_eq_n ?input_to_value:(Some true) program "get" make_input make_expected
in
let%bind () =
let input = ez [(23, 23) ; (42, 42)] in
let expected = ez [23, 23] in
expect_eq program "rm" input expected
in *)
(* let%bind () =
let input = ez [(1 , 10) ; (2 , 20) ; (3 , 30) ] in
let expected = e_int 66 in
expect_eq program "iter_op" input expected
expect_eq ?input_to_value:(Some true) program "rm" input expected
in
let%bind () =
let input = ez [(1 , 10) ; (2 , 20) ; (3 , 30) ] in
let expected = ez [(1 , 11) ; (2 , 21) ; (3 , 31) ] in
expect_eq program "map_op" input expected
in *)
ok ()
let list () : unit result =

View File

@ -31,14 +31,14 @@ let test_suite name lst = Test_suite (name , lst)
open Ast_simplified.Combinators
let expect ?options program entry_point input expecter =
let expect ?input_to_value ?options program entry_point input expecter =
let%bind result =
let run_error =
let title () = "expect run" in
let content () = Format.asprintf "Entry_point: %s" entry_point in
error title content in
trace run_error @@
Ligo.Run.run_simplityped ~debug_michelson:true ?options program entry_point input in
Ligo.Run.run_simplityped ?input_to_value ~debug_michelson:true ?options program entry_point input in
expecter result
let expect_fail ?options program entry_point input =
@ -52,7 +52,7 @@ let expect_fail ?options program entry_point input =
@@ Ligo.Run.run_simplityped ~debug_michelson:true ?options program entry_point input
let expect_eq ?options program entry_point input expected =
let expect_eq ?input_to_value ?options program entry_point input expected =
let expecter = fun result ->
let expect_error =
let title () = "expect result" in
@ -62,7 +62,7 @@ let expect_eq ?options program entry_point input expected =
error title content in
trace expect_error @@
Ast_simplified.Misc.assert_value_eq (expected , result) in
expect ?options program entry_point input expecter
expect ?input_to_value ?options program entry_point input expecter
let expect_evaluate program entry_point expecter =
let error =
@ -89,23 +89,23 @@ let expect_n_aux ?options lst program entry_point make_input make_expecter =
let%bind _ = bind_map_list aux lst in
ok ()
let expect_eq_n_aux ?options lst program entry_point make_input make_expected =
let expect_eq_n_aux ?input_to_value ?options lst program entry_point make_input make_expected =
let aux n =
let input = make_input n in
let expected = make_expected n in
trace (simple_error ("expect_eq_n " ^ (string_of_int n))) @@
let result = expect_eq ?options program entry_point input expected in
let result = expect_eq ?input_to_value ?options program entry_point input expected in
result
in
let%bind _ = bind_map_list_seq aux lst in
ok ()
let expect_eq_n ?options = expect_eq_n_aux ?options [0 ; 1 ; 2 ; 42 ; 163 ; -1]
let expect_eq_n_pos ?options = expect_eq_n_aux ?options [0 ; 1 ; 2 ; 42 ; 163]
let expect_eq_n_strict_pos ?options = expect_eq_n_aux ?options [2 ; 42 ; 163]
let expect_eq_n_pos_small ?options = expect_eq_n_aux ?options [0 ; 1 ; 2 ; 10]
let expect_eq_n_strict_pos_small ?options = expect_eq_n_aux ?options [1 ; 2 ; 10]
let expect_eq_n_pos_mid = expect_eq_n_aux [0 ; 1 ; 2 ; 10 ; 33]
let expect_eq_n ?input_to_value ?options = expect_eq_n_aux ?input_to_value ?options [0 ; 1 ; 2 ; 42 ; 163 ; -1]
let expect_eq_n_pos ?input_to_value ?options = expect_eq_n_aux ?input_to_value ?options [0 ; 1 ; 2 ; 42 ; 163]
let expect_eq_n_strict_pos ?input_to_value ?options = expect_eq_n_aux ?input_to_value ?options [2 ; 42 ; 163]
let expect_eq_n_pos_small ?input_to_value ?options = expect_eq_n_aux ?input_to_value ?options [0 ; 1 ; 2 ; 10]
let expect_eq_n_strict_pos_small ?input_to_value ?options = expect_eq_n_aux ?input_to_value ?options [1 ; 2 ; 10]
let expect_eq_n_pos_mid ?input_to_value = expect_eq_n_aux ?input_to_value [0 ; 1 ; 2 ; 10 ; 33]
let expect_n_pos_small ?options = expect_n_aux ?options [0 ; 2 ; 10]
let expect_n_strict_pos_small ?options = expect_n_aux ?options [2 ; 10]