Skip to content
This repository was archived by the owner on Aug 27, 2025. It is now read-only.

Gas charges to use Name.t instead of string #897

Merged
jjcnn merged 1 commit into from
Oct 20, 2020
Merged

Gas charges to use Name.t instead of string #897

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 22 additions & 2 deletions src/base/Cashflow.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,6 +108,25 @@ struct

let add_noinfo_to_builtin (op, rep) = (op, (ECFR.NoInfo, rep))

let rec cf_init_gas_charge gc =
let open TypedSyntax.SGasCharge in
match gc with
| StaticCost i -> CFSyntax.SGasCharge.StaticCost i
| SizeOf v -> CFSyntax.SGasCharge.SizeOf v
| ValueOf v -> CFSyntax.SGasCharge.ValueOf v
| LengthOf v -> CFSyntax.SGasCharge.LengthOf v
| MapSortCost m -> CFSyntax.SGasCharge.MapSortCost m
| SumOf (g1, g2) ->
CFSyntax.SGasCharge.SumOf (cf_init_gas_charge g1, cf_init_gas_charge g2)
| ProdOf (g1, g2) ->
CFSyntax.SGasCharge.ProdOf (cf_init_gas_charge g1, cf_init_gas_charge g2)
| MinOf (g1, g2) ->
CFSyntax.SGasCharge.MinOf (cf_init_gas_charge g1, cf_init_gas_charge g2)
| DivCeil (g1, g2) ->
CFSyntax.SGasCharge.DivCeil
(cf_init_gas_charge g1, cf_init_gas_charge g2)
| LogOf v -> CFSyntax.SGasCharge.LogOf v

let rec cf_init_tag_pattern p =
match p with
| Wildcard -> CFSyntax.Wildcard
Expand All @@ -128,7 +147,8 @@ struct
| Var i -> CFSyntax.Var (add_noinfo_to_ident i)
| Fun (arg, t, body) ->
CFSyntax.Fun (add_noinfo_to_ident arg, t, cf_init_tag_expr body)
| GasExpr (g, body) -> CFSyntax.GasExpr (g, cf_init_tag_expr body)
| GasExpr (g, body) ->
CFSyntax.GasExpr (cf_init_gas_charge g, cf_init_tag_expr body)
| App (f, actuals) ->
CFSyntax.App
(add_noinfo_to_ident f, List.map ~f:add_noinfo_to_ident actuals)
Expand Down Expand Up @@ -200,7 +220,7 @@ struct
match xopt with
| Some x -> CFSyntax.Throw (Some (add_noinfo_to_ident x))
| None -> CFSyntax.Throw None )
| GasStmt g -> CFSyntax.GasStmt g
| GasStmt g -> CFSyntax.GasStmt (cf_init_gas_charge g)
in
(res_s, rep)

Expand Down
67 changes: 64 additions & 3 deletions src/base/Disambiguate.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -128,6 +128,52 @@ module ScillaDisambiguation (SR : Rep) (ER : Rep) = struct
in
recurse t

(**************************************************************)
(* Disambiguating explict gas charges *)
(**************************************************************)

(* No variable bindings in gas charge nodes, so dis_id_helper just wraps
a call to disambiguate_identifier using the appropriate dictionaries. *)

let disambiguate_gas_charge dis_id_helper gc =
let rec recurser gc =
let open PreDisSyntax.SGasCharge in
match gc with
| StaticCost i -> pure @@ PostDisSyntax.SGasCharge.StaticCost i
| SizeOf v ->
let%bind dis_v = dis_id_helper v in
pure @@ PostDisSyntax.SGasCharge.SizeOf dis_v
| ValueOf v ->
let%bind dis_v = dis_id_helper v in
pure @@ PostDisSyntax.SGasCharge.ValueOf dis_v
| LengthOf v ->
let%bind dis_v = dis_id_helper v in
pure @@ PostDisSyntax.SGasCharge.LengthOf dis_v
| MapSortCost m ->
let%bind dis_m = dis_id_helper m in
pure @@ PostDisSyntax.SGasCharge.MapSortCost dis_m
| SumOf (g1, g2) ->
let%bind dis_g1 = recurser g1 in
let%bind dis_g2 = recurser g2 in
pure @@ PostDisSyntax.SGasCharge.SumOf (dis_g1, dis_g2)
| ProdOf (g1, g2) ->
let%bind dis_g1 = recurser g1 in
let%bind dis_g2 = recurser g2 in
pure @@ PostDisSyntax.SGasCharge.ProdOf (dis_g1, dis_g2)
| MinOf (g1, g2) ->
let%bind dis_g1 = recurser g1 in
let%bind dis_g2 = recurser g2 in
pure @@ PostDisSyntax.SGasCharge.MinOf (dis_g1, dis_g2)
| DivCeil (g1, g2) ->
let%bind dis_g1 = recurser g1 in
let%bind dis_g2 = recurser g2 in
pure @@ PostDisSyntax.SGasCharge.DivCeil (dis_g1, dis_g2)
| LogOf v ->
let%bind dis_v = dis_id_helper v in
pure @@ PostDisSyntax.SGasCharge.LogOf dis_v
in
recurser gc

(**************************************************************)
(* Disambiguate expressions *)
(**************************************************************)
Expand Down Expand Up @@ -226,6 +272,9 @@ module ScillaDisambiguation (SR : Rep) (ER : Rep) = struct
recurser p

let disambiguate_exp (dicts : name_dicts) erep =
let disambiguate_name_helper simp_var_dict nm =
disambiguate_name dicts.ns_dict simp_var_dict nm
in
let disambiguate_identifier_helper simp_var_dict id =
disambiguate_identifier dicts.ns_dict simp_var_dict id
in
Expand Down Expand Up @@ -336,8 +385,11 @@ module ScillaDisambiguation (SR : Rep) (ER : Rep) = struct
let%bind dis_body = recurser body_simp_var_dict body in
pure @@ PostDisSyntax.Fixpoint (dis_f, dis_t, dis_body)
| GasExpr (g, e) ->
let%bind e' = recurser simp_var_dict e in
pure @@ PostDisSyntax.GasExpr (g, e')
let%bind dis_g =
disambiguate_gas_charge (disambiguate_name_helper simp_var_dict) g
in
let%bind dis_e = recurser simp_var_dict e in
pure @@ PostDisSyntax.GasExpr (dis_g, dis_e)
in
pure @@ (new_e, rep)
in
Expand All @@ -348,6 +400,9 @@ module ScillaDisambiguation (SR : Rep) (ER : Rep) = struct
(**************************************************************)

let rec disambiguate_stmts (dicts : name_dicts) stmts =
let disambiguate_name_helper simp_var_dict nm =
disambiguate_name dicts.ns_dict simp_var_dict nm
in
let disambiguate_identifier_helper simp_var_dict id =
disambiguate_identifier dicts.ns_dict simp_var_dict id
in
Expand Down Expand Up @@ -464,7 +519,13 @@ module ScillaDisambiguation (SR : Rep) (ER : Rep) = struct
~f:(disambiguate_identifier_helper simp_var_dict_acc)
in
pure @@ (PostDisSyntax.Throw dis_xopt, simp_var_dict_acc)
| GasStmt g -> pure @@ (PostDisSyntax.GasStmt g, simp_var_dict_acc)
| GasStmt g ->
let%bind dis_g =
disambiguate_gas_charge
(disambiguate_name_helper simp_var_dict_acc)
g
in
pure @@ (PostDisSyntax.GasStmt dis_g, simp_var_dict_acc)
in
pure @@ (new_simp_var_dict, (dis_s, rep) :: dis_stmts_acc_rev)
in
Expand Down
Loading