Updated README. Changed ADT

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

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

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

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 ->

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))

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" () ()

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"]
 ]

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"]
 ]