From 2674e8419913aec6c7254d8080b858018ff4dc78 Mon Sep 17 00:00:00 2001 From: Galfour Date: Tue, 30 Apr 2019 08:41:06 +0000 Subject: [PATCH] add heap tests ; discover error with SLASH --- src/lib_utils/x_tezos_micheline.ml | 5 +- src/ligo/contracts/arithmetic.ligo | 3 + src/ligo/contracts/counter.ligo | 8 ++- src/ligo/contracts/heap.ligo | 89 ++++++++++++++++++++----- src/ligo/operators/operators.ml | 6 +- src/ligo/parser/pascaligo/ParserLog.mli | 1 + src/ligo/simplify/pascaligo.ml | 9 ++- src/ligo/test/heap_tests.ml | 41 ++++++------ src/ligo/test/integration_tests.ml | 3 +- 9 files changed, 120 insertions(+), 45 deletions(-) diff --git a/src/lib_utils/x_tezos_micheline.ml b/src/lib_utils/x_tezos_micheline.ml index 1f2656c03..b84abc1e0 100644 --- a/src/lib_utils/x_tezos_micheline.ml +++ b/src/lib_utils/x_tezos_micheline.ml @@ -30,6 +30,7 @@ module Michelson = struct let bytes s : michelson = Bytes (0, s) let t_unit = prim T_unit + let t_string = prim T_string let t_pair a b = prim ~children:[a;b] T_pair let t_lambda a b = prim ~children:[a;b] T_lambda @@ -44,6 +45,7 @@ module Michelson = struct let i_piar = seq [ i_swap ; i_pair ] let i_push ty code = prim ~children:[ty;code] I_PUSH let i_push_unit = i_push t_unit d_unit + let i_push_string str = i_push t_string (string str) let i_none ty = prim ~children:[ty] I_NONE let i_nil ty = prim ~children:[ty] I_NIL let i_some = prim I_SOME @@ -56,7 +58,8 @@ module Michelson = struct let i_if_none a b = prim ~children:[a;b] I_IF_NONE let i_if_left a b = prim ~children:[a;b] I_IF_LEFT let i_failwith = prim I_FAILWITH - let i_assert_some = i_if_none (seq [i_failwith]) (seq []) + let i_assert_some = i_if_none (seq [i_push_string "ASSERT_SOME" ; i_failwith]) (seq []) + let i_assert_some_msg msg = i_if_none (seq [msg ; i_failwith]) (seq []) let dip code : michelson = prim ~children:[seq [code]] I_DIP let i_unpair = seq [i_dup ; i_car ; dip i_cdr] diff --git a/src/ligo/contracts/arithmetic.ligo b/src/ligo/contracts/arithmetic.ligo index 56e270120..668a8c619 100644 --- a/src/ligo/contracts/arithmetic.ligo +++ b/src/ligo/contracts/arithmetic.ligo @@ -7,5 +7,8 @@ function minus_op (const n : int) : int is function times_op (const n : int) : int is begin skip end with n * 42 +function div_op (const n : int) : int is + begin skip end with n / 2 + function int_op (const n : nat) : int is block { skip } with int(n) diff --git a/src/ligo/contracts/counter.ligo b/src/ligo/contracts/counter.ligo index 1241242c5..5c525436b 100644 --- a/src/ligo/contracts/counter.ligo +++ b/src/ligo/contracts/counter.ligo @@ -1,2 +1,6 @@ -function main (const p : int ; const s : int) : (list(operation) * int) is - block {skip} with ((nil : operation), p + s) +type some_type is int + +function main (const p : int ; const s : some_type) : (list(operation) * int) is + block { skip } // skip is a do nothing instruction, needed for empty blocks + with ((nil : operation), p + s) + diff --git a/src/ligo/contracts/heap.ligo b/src/ligo/contracts/heap.ligo index 20f7dcf97..44abd2f0a 100644 --- a/src/ligo/contracts/heap.ligo +++ b/src/ligo/contracts/heap.ligo @@ -15,20 +15,75 @@ function pop_switch (const h : heap) : heap is h[1n] := last ; } with h -// function largest_child (const h : heap) : nat is -// block { -// const result : heap_element = get_top (h) ; -// const s : nat = size(h) ; -// var current : heap_element := get_force(s, h) ; -// const i : nat = 1n ; -// const left : nat = 2n * i ; -// const right : nat = left + 1n ; -// remove 1n from map h ; -// h[1n] := current ; -// var largest : nat := i ; -// if (left <= s and heap_element_lt(get_force(s , h) , get_force(left , h))) then -// largest := left -// else if (right <= s and heap_element_lt(get_force(s , h) , get_force(right , h))) then -// largest := right -// else skip -// } with largest +function pop_ (const h : heap) : nat is + begin + const result : heap_element = get_top (h) ; + const s : nat = size(h) ; + var current : heap_element := get_force(s, h) ; + const i : nat = 1n ; + const left : nat = 2n * i ; + const right : nat = left + 1n ; + remove 1n from map h ; + h[1n] := current ; + var largest : nat := i ; + if (left <= s and heap_element_lt(get_force(s , h) , get_force(left , h))) then + largest := left + else if (right <= s and heap_element_lt(get_force(s , h) , get_force(right , h))) then + largest := right + else skip + end with largest + +function insert (const h : heap ; const e : heap_element) : heap is + begin + var i : nat := size(h) + 1n ; + h[i] := e ; + var largest : nat := i ; + while (largest =/= i) block { + largest := i ; + const parent : nat = i / 2n ; + if (parent >= 1n) then block { + if (heap_element_lt(get_force(parent , h) , get_force(i , h))) then block { + largest := parent ; + const tmp : heap_element = get_force(i , h) ; + h[i] := get_force(parent , h) ; + h[parent] := tmp ; + } else skip + } else skip + } + end with h + +function pop (const h : heap) : (heap * heap_element * nat) is + begin + const result : heap_element = get_top (h) ; + var s : nat := size(h) ; + const last : heap_element = get_force(s, h) ; + remove s from map h ; + h[1n] := last ; + s := size(h) ; + var i : nat := 0n ; + var largest : nat := 1n ; + var left : nat := 0n ; + var right : nat := 0n ; + var c : nat := 0n ; + while (largest =/= i) block { + c := c + 1n ; + i := largest ; + left := 2n * i ; + right := left + 1n ; + if (left <= s) then begin + if (heap_element_lt(get_force(left , h) , get_force(i , h))) then begin + largest := left ; + const tmp : heap_element = get_force(i , h) ; + h[i] := get_force(left , h) ; + h[left] := tmp ; + end else skip ; + end else if (right <= s) then begin + if (heap_element_lt(get_force(right , h) , get_force(i , h))) then begin + largest := right ; + const tmp : heap_element = get_force(i , h) ; + h[i] := get_force(right , h) ; + h[left] := tmp ; + end else skip ; + end else skip ; + } + end with (h , result , c) diff --git a/src/ligo/operators/operators.ml b/src/ligo/operators/operators.ml index 57ca170f6..1a3257038 100644 --- a/src/ligo/operators/operators.ml +++ b/src/ligo/operators/operators.ml @@ -316,10 +316,14 @@ module Compiler = struct ("CAR" , simple_unary @@ prim I_CAR) ; ("CDR" , simple_unary @@ prim I_CDR) ; ("EQ" , simple_binary @@ seq [prim I_COMPARE ; prim I_EQ]) ; + ("NEQ" , simple_binary @@ seq [prim I_COMPARE ; prim I_NEQ]) ; ("LT" , simple_binary @@ seq [prim I_COMPARE ; prim I_LT]) ; + ("LE" , simple_binary @@ seq [prim I_COMPARE ; prim I_LE]) ; + ("GT" , simple_binary @@ seq [prim I_COMPARE ; prim I_GT]) ; + ("GE" , simple_binary @@ seq [prim I_COMPARE ; prim I_GE]) ; ("UPDATE" , simple_ternary @@ prim I_UPDATE) ; ("SOME" , simple_unary @@ prim I_SOME) ; - ("GET_FORCE" , simple_binary @@ seq [prim I_GET ; i_assert_some]) ; + ("GET_FORCE" , simple_binary @@ seq [prim I_GET ; i_assert_some_msg (i_push_string "GET_FORCE")]) ; ("GET" , simple_binary @@ prim I_GET) ; ("SIZE" , simple_unary @@ prim I_SIZE) ; ("INT" , simple_unary @@ prim I_INT) ; diff --git a/src/ligo/parser/pascaligo/ParserLog.mli b/src/ligo/parser/pascaligo/ParserLog.mli index 637a15438..a0db900a2 100644 --- a/src/ligo/parser/pascaligo/ParserLog.mli +++ b/src/ligo/parser/pascaligo/ParserLog.mli @@ -7,3 +7,4 @@ val print_tokens : AST.t -> unit val print_path : AST.path -> unit val print_pattern : AST.pattern -> unit +val print_instruction : AST.instruction -> unit diff --git a/src/ligo/simplify/pascaligo.ml b/src/ligo/simplify/pascaligo.ml index e1125d894..f25592c0a 100644 --- a/src/ligo/simplify/pascaligo.ml +++ b/src/ligo/simplify/pascaligo.ml @@ -408,10 +408,10 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t -> let c = c.value in let%bind expr = simpl_expression c.test in let%bind match_true = match c.ifso with - | ClauseInstr i -> let%bind i = simpl_instruction i in ok [i] + | ClauseInstr i -> simpl_instruction_block i | ClauseBlock b -> simpl_statements @@ fst b.value.inside in let%bind match_false = match c.ifnot with - | ClauseInstr i -> let%bind i = simpl_instruction i in ok [i] + | ClauseInstr i -> simpl_instruction_block i | ClauseBlock b -> simpl_statements @@ fst b.value.inside in ok @@ I_matching (expr, (Match_bool {match_true; match_false})) | Assign a -> ( @@ -560,6 +560,11 @@ and simpl_instruction_block : Raw.instruction -> block result = fun t -> | Block b -> simpl_block b.value and simpl_instruction : Raw.instruction -> instruction result = fun t -> + let main_error = + let title () = "simplifiying instruction" in + let content () = Format.asprintf "%a" PP_helpers.(printer Parser.Pascaligo.ParserLog.print_instruction) t in + error title content in + trace main_error @@ match t with | Single s -> simpl_single_instruction s | Block _ -> simple_fail "no block instruction yet" diff --git a/src/ligo/test/heap_tests.ml b/src/ligo/test/heap_tests.ml index df1db2c79..2e6b6fb24 100644 --- a/src/ligo/test/heap_tests.ml +++ b/src/ligo/test/heap_tests.ml @@ -96,30 +96,29 @@ let pop_switch () : unit result = @@ [0 ; 2 ; 7 ; 12] in ok () -(* let pop () : unit result = - * let%bind program = get_program () in - * let aux n = - * let input = dummy n in - * match n, easy_run_typed "pop" program input with - * | 0, Trace.Ok _ -> simple_fail "unexpected success" - * | 0, _ -> ok () - * | _, result -> - * let%bind result' = result in - * let expected = ez List.( - * map (fun i -> if i = 1 then (1, (n, string_of_int n)) else (i, (i, string_of_int i))) - * @@ tl - * @@ range (n + 1) - * ) in - * AST_Typed.assert_value_eq (expected, result') - * in - * let%bind _ = bind_list - * @@ List.map aux - * @@ [0 ; 2 ; 7 ; 12] in - * ok () *) +let pop () : unit result = + let%bind program = get_program () in + let aux n = + let input = dummy n in + (match easy_run_typed "pop" program input with + | Trace.Ok (output , _) -> ( + Format.printf "\nPop output on %d : %a\n" n AST_Typed.PP.annotated_expression output ; + ) + | Errors errs -> ( + Format.printf "\nPop output on %d : error\n" n) ; + Format.printf "Errors : {\n%a}\n%!" errors_pp (List.rev (List.rev_map (fun f -> f ()) errs)) ; + ) ; + ok () + in + let%bind _ = bind_list + @@ List.map aux + @@ [2 ; 7 ; 12] in + (* simple_fail "display" *) + ok () let main = "Heap (End to End)", [ test "is_empty" is_empty ; test "get_top" get_top ; test "pop_switch" pop_switch ; - (* test "pop" pop ; *) + test "pop" pop ; ] diff --git a/src/ligo/test/integration_tests.ml b/src/ligo/test/integration_tests.ml index 32dcf41aa..db4d1d575 100644 --- a/src/ligo/test/integration_tests.ml +++ b/src/ligo/test/integration_tests.ml @@ -103,6 +103,7 @@ let arithmetic () : unit result = ("plus_op", fun n -> (n + 42)) ; ("minus_op", fun n -> (n - 42)) ; ("times_op", fun n -> (n * 42)) ; + ("div_op", fun n -> (n / 2)) ; ] in let%bind () = expect_n_pos program "int_op" e_a_nat e_a_int in ok () @@ -393,5 +394,5 @@ let main = "Integration (End to End)", [ test "higher order" higher_order ; test "basic mligo" basic_mligo ; test "counter contract mligo" counter_mligo ; - test "guess the hash mligo" guess_the_hash_mligo ; + (* test "guess the hash mligo" guess_the_hash_mligo ; *) ]