diff --git a/README.md b/README.md index 4347a30..90bb2bc 100644 --- a/README.md +++ b/README.md @@ -5,6 +5,9 @@ An intermediate representation of Michelson smart contracts designed to ease static analysis of smart contracts. +You can read more about it on +[this paper](https://drops.dagstuhl.de/opus/volltexte/2020/13417/pdf/OASIcs-FMBC-2020-4.pdf). + ## Install instructions ### Using dune @@ -17,11 +20,11 @@ dune install ``` ### Using opam + ```bash opam install https://github.com/joaosreis/tezla.git ``` - --- Developed under the [FRESCO](https://release.di.ubi.pt/projects/fresco.html) project diff --git a/src/lib/adt/adt.ml b/src/lib/adt/adt.ml index 3420bd8..c465c8e 100644 --- a/src/lib/adt/adt.ml +++ b/src/lib/adt/adt.ml @@ -121,11 +121,7 @@ and expr_t = | E_unlift_or_right of var | E_hd of var | E_tl of var - | E_size_list of var - | E_size_set of var - | E_size_map of var - | E_size_string of var - | E_size_bytes of var + | E_size of var | E_isnat of var | E_int_of_nat of var | E_chain_id @@ -307,7 +303,39 @@ module Expr = Make_common (struct | E_append (v_1, v_2) -> [%string "append(%{v_1#Var}, %{v_2#Var})"] | E_special_empty_list _ -> "{ }" | E_special_empty_map _ -> "{ }" - | _ -> (*TODO: *) assert false + | E_total_voting_power -> "TOTAL_VOTING_POWER" + | E_self_address -> "SELF_address" + | E_level -> "LEVEL" + | E_size v -> [%string "SIZE %{v#Var}"] + | E_create_account_operation (v_1, v_2, v_3, v_4) -> + [%string + "CREATE_ACCOUNT_operation %{v_1#Var} %{v_2#Var} %{v_3#Var} %{v_4#Var}"] + | E_create_account_address (v_1, v_2, v_3, v_4) -> + [%string + "CREATE_ACCOUNT_address %{v_1#Var} %{v_2#Var} %{v_3#Var} %{v_4#Var}"] + | E_voting_power v -> [%string "VOTING_POWER %{v#Var}"] + | E_keccak v -> [%string "KECCAK %{v#Var}"] + | E_sha3 v -> [%string "SHA3 %{v#Var}"] + | E_pairing_check v -> [%string "PAIRING_CHECK %{v#Var}"] + | E_sapling_verify_update (v_1, v_2) -> + [%string "SApling_verify_update %{v_1#Var} %{v_2#Var}"] + | E_sapling_empty_state n -> [%string "SAPLING_EMPTY_STATE %{n#Bigint}"] + | E_ticket (v_1, v_2) -> [%string "TICKET %{v_1#Var} %{v_2#Var}"] + | E_read_ticket_pair v -> [%string "READ_TICKET_pair %{v#Var}"] + | E_read_ticket_ticket v -> [%string "READ_TICKET_ticket %{v#Var}"] + | E_split_ticket (v_1, v_2) -> + [%string "SPLIT_TICKET %{v_1#Var} %{v_2#Var}"] + | E_join_ticket v -> [%string "JOIN_TICKET %{v#Var}"] + | E_open_chest (v_1, v_2, v_3) -> + [%string "OPEN_CHEST %{v_1#Var} %{v_2#Var} %{v_3#Var}"] + | E_get_and_update_val (v_1, v_2, v_3) -> + [%string "GET_AND_UPDATE_val %{v_1#Var} %{v_2#Var} %{v_3#Var}"] + | E_get_and_update_map (v_1, v_2, v_3) -> + [%string "GET_AND_UPDATE_map %{v_1#Var} %{v_2#Var} %{v_3#Var}"] + | E_dup_n (n, v) -> [%string "DUP %{n#Bigint} %{v#Var}"] + | E_get_n (n, v) -> [%string "GET_N %{n#Bigint} %{v#Var}"] + | E_update_n (n, v_1, v_2) -> + [%string "UPDATE_N %{n#Bigint} %{v_1#Var} %{v_2#Var}"] end) module Stmt = struct diff --git a/src/lib/adt/adt.mli b/src/lib/adt/adt.mli index ca865f4..6a11f22 100644 --- a/src/lib/adt/adt.mli +++ b/src/lib/adt/adt.mli @@ -87,11 +87,7 @@ and expr_t = | E_unlift_or_right of var | E_hd of var | E_tl of var - | E_size_list of var - | E_size_set of var - | E_size_map of var - | E_size_string of var - | E_size_bytes of var + | E_size of var | E_isnat of var | E_int_of_nat of var | E_chain_id diff --git a/src/lib/converter/converter.ml b/src/lib/converter/converter.ml index b091243..6fb6d79 100644 --- a/src/lib/converter/converter.ml +++ b/src/lib/converter/converter.ml @@ -409,27 +409,27 @@ and inst_to_stmt counter env i = (s, env') | I_size_list -> let v, env' = pop env in - let e = Tezla_adt.E_size_list v in + let e = Tezla_adt.E_size v in let v', assign = create_assign_annot_1 e in (assign, push v' env') | I_size_set -> let v, env' = pop env in - let e = Tezla_adt.E_size_set v in + let e = Tezla_adt.E_size v in let v', assign = create_assign_annot_1 e in (assign, push v' env') | I_size_map -> let v, env' = pop env in - let e = Tezla_adt.E_size_map v in + let e = Tezla_adt.E_size v in let v', assign = create_assign_annot_1 e in (assign, push v' env') | I_size_string -> let v, env' = pop env in - let e = Tezla_adt.E_size_string v in + let e = Tezla_adt.E_size v in let v', assign = create_assign_annot_1 e in (assign, push v' env') | I_size_bytes -> let v, env' = pop env in - let e = Tezla_adt.E_size_bytes v in + let e = Tezla_adt.E_size v in let v', assign = create_assign_annot_1 e in (assign, push v' env') | I_empty_set t -> diff --git a/src/lib/converter/typer.ml b/src/lib/converter/typer.ml index 6b72e45..ce6d513 100644 --- a/src/lib/converter/typer.ml +++ b/src/lib/converter/typer.ml @@ -118,11 +118,7 @@ let type_expr e = | Map (k, v) -> ct (Pair (k, v)) | _ -> assert false) | E_tl v -> force v.var_type - | E_size_bytes _ -> ct Nat - | E_size_string _ -> ct Nat - | E_size_list _ -> ct Nat - | E_size_set _ -> ct Nat - | E_size_map _ -> ct Nat + | E_size _ -> ct Nat | E_isnat _ -> ct (Option (ct Nat)) | E_int_of_nat _ -> ct Int | E_lambda (t_1, t_2, _, _) -> ct (Lambda (convert_typ t_1, convert_typ t_2)) diff --git a/src/test/test.ml b/src/test/test.ml index bb6dd6e..4f38b4b 100644 --- a/src/test/test.ml +++ b/src/test/test.ml @@ -5,10 +5,9 @@ let () = let files = Sys_unix.readdir dir in let open Alcotest in let create_test filename = - let open Edo_parser.Parser in let convert_f () = - let adt = parse_file (dir ^ filename) in - let adt = convert (dir ^ filename) adt in + let adt = Edo_parser.Parser.parse_file (dir ^ filename) in + let adt = Edo_parser.Parser.convert (dir ^ filename) adt in let adt = Edo_adt.Typer.type_program adt in let _ = Tezla.Converter.convert_program (ref (-1)) adt in check pass "Ok" () () diff --git a/tezla.opam b/tezla.opam index 1ca1662..a6a6b1f 100644 --- a/tezla.opam +++ b/tezla.opam @@ -36,6 +36,6 @@ build: [ ] dev-repo: "git+https://github.com/joaosreis/tezla.git" pin-depends: [ - ["michelson-adt.dev" "git+https://github.com/releaselab/michelson-adt.git"] - ["michelson-parser.dev" "git+https://github.com/releaselab/michelson-parser.git"] + ["michelson-adt.dev" "git+https://github.com/joaosreis/michelson-adt.git"] + ["michelson-parser.dev" "git+https://github.com/joaosreis/michelson-parser.git"] ] diff --git a/tezla.opam.template b/tezla.opam.template index f5707fd..a8e6daf 100644 --- a/tezla.opam.template +++ b/tezla.opam.template @@ -1,4 +1,4 @@ pin-depends: [ - ["michelson-adt.dev" "git+https://github.com/releaselab/michelson-adt.git"] - ["michelson-parser.dev" "git+https://github.com/releaselab/michelson-parser.git"] + ["michelson-adt.dev" "git+https://github.com/joaosreis/michelson-adt.git"] + ["michelson-parser.dev" "git+https://github.com/joaosreis/michelson-parser.git"] ]