add heap tests ; discover error with SLASH

This commit is contained in:
Galfour 2019-04-30 08:41:06 +00:00
parent 6cb341b162
commit 2674e84199
9 changed files with 120 additions and 45 deletions

View File

@ -30,6 +30,7 @@ module Michelson = struct
let bytes s : michelson = Bytes (0, s) let bytes s : michelson = Bytes (0, s)
let t_unit = prim T_unit 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_pair a b = prim ~children:[a;b] T_pair
let t_lambda a b = prim ~children:[a;b] T_lambda 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_piar = seq [ i_swap ; i_pair ]
let i_push ty code = prim ~children:[ty;code] I_PUSH let i_push ty code = prim ~children:[ty;code] I_PUSH
let i_push_unit = i_push t_unit d_unit 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_none ty = prim ~children:[ty] I_NONE
let i_nil ty = prim ~children:[ty] I_NIL let i_nil ty = prim ~children:[ty] I_NIL
let i_some = prim I_SOME 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_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_if_left a b = prim ~children:[a;b] I_IF_LEFT
let i_failwith = prim I_FAILWITH 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 dip code : michelson = prim ~children:[seq [code]] I_DIP
let i_unpair = seq [i_dup ; i_car ; dip i_cdr] let i_unpair = seq [i_dup ; i_car ; dip i_cdr]

View File

@ -7,5 +7,8 @@ function minus_op (const n : int) : int is
function times_op (const n : int) : int is function times_op (const n : int) : int is
begin skip end with n * 42 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 function int_op (const n : nat) : int is
block { skip } with int(n) block { skip } with int(n)

View File

@ -1,2 +1,6 @@
function main (const p : int ; const s : int) : (list(operation) * int) is type some_type is int
block {skip} with ((nil : operation), p + s)
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)

View File

@ -15,20 +15,75 @@ function pop_switch (const h : heap) : heap is
h[1n] := last ; h[1n] := last ;
} with h } with h
// function largest_child (const h : heap) : nat is function pop_ (const h : heap) : nat is
// block { begin
// const result : heap_element = get_top (h) ; const result : heap_element = get_top (h) ;
// const s : nat = size(h) ; const s : nat = size(h) ;
// var current : heap_element := get_force(s, h) ; var current : heap_element := get_force(s, h) ;
// const i : nat = 1n ; const i : nat = 1n ;
// const left : nat = 2n * i ; const left : nat = 2n * i ;
// const right : nat = left + 1n ; const right : nat = left + 1n ;
// remove 1n from map h ; remove 1n from map h ;
// h[1n] := current ; h[1n] := current ;
// var largest : nat := i ; var largest : nat := i ;
// if (left <= s and heap_element_lt(get_force(s , h) , get_force(left , h))) then if (left <= s and heap_element_lt(get_force(s , h) , get_force(left , h))) then
// largest := left largest := left
// else if (right <= s and heap_element_lt(get_force(s , h) , get_force(right , h))) then else if (right <= s and heap_element_lt(get_force(s , h) , get_force(right , h))) then
// largest := right largest := right
// else skip else skip
// } with largest 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)

View File

@ -316,10 +316,14 @@ module Compiler = struct
("CAR" , simple_unary @@ prim I_CAR) ; ("CAR" , simple_unary @@ prim I_CAR) ;
("CDR" , simple_unary @@ prim I_CDR) ; ("CDR" , simple_unary @@ prim I_CDR) ;
("EQ" , simple_binary @@ seq [prim I_COMPARE ; prim I_EQ]) ; ("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]) ; ("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) ; ("UPDATE" , simple_ternary @@ prim I_UPDATE) ;
("SOME" , simple_unary @@ prim I_SOME) ; ("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) ; ("GET" , simple_binary @@ prim I_GET) ;
("SIZE" , simple_unary @@ prim I_SIZE) ; ("SIZE" , simple_unary @@ prim I_SIZE) ;
("INT" , simple_unary @@ prim I_INT) ; ("INT" , simple_unary @@ prim I_INT) ;

View File

@ -7,3 +7,4 @@ val print_tokens : AST.t -> unit
val print_path : AST.path -> unit val print_path : AST.path -> unit
val print_pattern : AST.pattern -> unit val print_pattern : AST.pattern -> unit
val print_instruction : AST.instruction -> unit

View File

@ -408,10 +408,10 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
let c = c.value in let c = c.value in
let%bind expr = simpl_expression c.test in let%bind expr = simpl_expression c.test in
let%bind match_true = match c.ifso with 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 | ClauseBlock b -> simpl_statements @@ fst b.value.inside in
let%bind match_false = match c.ifnot with 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 | ClauseBlock b -> simpl_statements @@ fst b.value.inside in
ok @@ I_matching (expr, (Match_bool {match_true; match_false})) ok @@ I_matching (expr, (Match_bool {match_true; match_false}))
| Assign a -> ( | Assign a -> (
@ -560,6 +560,11 @@ and simpl_instruction_block : Raw.instruction -> block result = fun t ->
| Block b -> simpl_block b.value | Block b -> simpl_block b.value
and simpl_instruction : Raw.instruction -> instruction result = fun t -> 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 match t with
| Single s -> simpl_single_instruction s | Single s -> simpl_single_instruction s
| Block _ -> simple_fail "no block instruction yet" | Block _ -> simple_fail "no block instruction yet"

View File

@ -96,30 +96,29 @@ let pop_switch () : unit result =
@@ [0 ; 2 ; 7 ; 12] in @@ [0 ; 2 ; 7 ; 12] in
ok () ok ()
(* let pop () : unit result = let pop () : unit result =
* let%bind program = get_program () in let%bind program = get_program () in
* let aux n = let aux n =
* let input = dummy n in let input = dummy n in
* match n, easy_run_typed "pop" program input with (match easy_run_typed "pop" program input with
* | 0, Trace.Ok _ -> simple_fail "unexpected success" | Trace.Ok (output , _) -> (
* | 0, _ -> ok () Format.printf "\nPop output on %d : %a\n" n AST_Typed.PP.annotated_expression output ;
* | _, result -> )
* let%bind result' = result in | Errors errs -> (
* let expected = ez List.( Format.printf "\nPop output on %d : error\n" n) ;
* map (fun i -> if i = 1 then (1, (n, string_of_int n)) else (i, (i, string_of_int i))) Format.printf "Errors : {\n%a}\n%!" errors_pp (List.rev (List.rev_map (fun f -> f ()) errs)) ;
* @@ tl ) ;
* @@ range (n + 1) ok ()
* ) in in
* AST_Typed.assert_value_eq (expected, result') let%bind _ = bind_list
* in @@ List.map aux
* let%bind _ = bind_list @@ [2 ; 7 ; 12] in
* @@ List.map aux (* simple_fail "display" *)
* @@ [0 ; 2 ; 7 ; 12] in ok ()
* ok () *)
let main = "Heap (End to End)", [ let main = "Heap (End to End)", [
test "is_empty" is_empty ; test "is_empty" is_empty ;
test "get_top" get_top ; test "get_top" get_top ;
test "pop_switch" pop_switch ; test "pop_switch" pop_switch ;
(* test "pop" pop ; *) test "pop" pop ;
] ]

View File

@ -103,6 +103,7 @@ let arithmetic () : unit result =
("plus_op", fun n -> (n + 42)) ; ("plus_op", fun n -> (n + 42)) ;
("minus_op", fun n -> (n - 42)) ; ("minus_op", fun n -> (n - 42)) ;
("times_op", fun n -> (n * 42)) ; ("times_op", fun n -> (n * 42)) ;
("div_op", fun n -> (n / 2)) ;
] in ] in
let%bind () = expect_n_pos program "int_op" e_a_nat e_a_int in let%bind () = expect_n_pos program "int_op" e_a_nat e_a_int in
ok () ok ()
@ -393,5 +394,5 @@ let main = "Integration (End to End)", [
test "higher order" higher_order ; test "higher order" higher_order ;
test "basic mligo" basic_mligo ; test "basic mligo" basic_mligo ;
test "counter contract mligo" counter_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 ; *)
] ]