Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

mini_c: add additional renames to avoid name collision #12

Merged
merged 2 commits into from
Dec 10, 2024
Merged

mini_c: add additional renames to avoid name collision #12

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
79aa24f
mini_c: alpha renaming after any inlining pass
EduardoRFS Dec 6, 2024
ce4b45c
mini_c: add tests for nested concat arithmetic
EduardoRFS Dec 6, 2024
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
6 changes: 3 additions & 3 deletions src/bin/expect_tests/contract_tests.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1159,7 +1159,7 @@ File "../../test/contracts/negative/create_contract_toplevel.mligo", line 5, cha
^^^^^^^^
10 | in

Not all free variables could be inlined in Tezos.create_contract usage: gen#430. |}];
Not all free variables could be inlined in Tezos.create_contract usage: gen#474. |}];
run_ligo_good [ "compile"; "contract"; contract "create_contract_var.mligo" ];
[%expect
{|
Expand Down Expand Up @@ -1251,7 +1251,7 @@ Not all free variables could be inlined in Tezos.create_contract usage: gen#430.
^^^^^^^^^^
15 | ([toto.0], store)

Not all free variables could be inlined in Tezos.create_contract usage: gen#431. |}];
Not all free variables could be inlined in Tezos.create_contract usage: gen#475. |}];
run_ligo_bad [ "compile"; "contract"; bad_contract "create_contract_no_inline.mligo" ];
[%expect
{|
Expand Down Expand Up @@ -1314,7 +1314,7 @@ Not all free variables could be inlined in Tezos.create_contract usage: gen#430.
^^^^^^^
15 | let toto : operation list = [op] in

Not all free variables could be inlined in Tezos.create_contract usage: foo#445. |}];
Not all free variables could be inlined in Tezos.create_contract usage: foo#489. |}];
run_ligo_good [ "compile"; "contract"; contract "create_contract.mligo" ];
[%expect
{|
Expand Down
152 changes: 0 additions & 152 deletions src/passes/15-self_mini_c/inline.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,158 +3,6 @@ open Mini_c
open Helpers
module Ligo_pair = Simple_utils.Ligo_pair

(* Reference implementation:
https://www.cs.cornell.edu/courses/cs3110/2019sp/textbook/interp/lambda-subst/main.ml

...but, it has at least one bug: in subst,
`let new_body = replace e' y fresh in ...` should be:
`let new_body = replace e' fresh y in ...`,
due to the arg order choice for replace.

Below, this bug is fixed by adopting the other order choice for
replace (as well as subst). *)

let replace_var : var_name -> var_name -> var_name -> var_name =
fun v x y -> if Value_var.equal v x then y else v


(* replace in `e` the variable `x` with `y`.

It would be fine -- better? -- to only replace the _free_ x.
*)
let rec replace : expression -> var_name -> var_name -> expression =
fun e x y ->
let replace e = replace e x y in
let return content = { e with content } in
let replace_var v = replace_var v x y in
match e.content with
| E_literal _ -> e
| E_closure { binder; body } ->
let body = replace body in
let binder = replace_var binder in
return @@ E_closure { binder; body }
| E_rec { func = { binder; body }; rec_binder } ->
let body = replace body in
let binder = replace_var binder in
let rec_binder = replace_var rec_binder in
return @@ E_rec { func = { binder; body }; rec_binder }
| E_constant c ->
let args = List.map ~f:replace c.arguments in
return @@ E_constant { cons_name = c.cons_name; arguments = args }
| E_application (f, x) ->
let f, x = Ligo_pair.map ~f:replace (f, x) in
return @@ E_application (f, x)
| E_variable z ->
let z = replace_var z in
return @@ E_variable z
| E_iterator (name, ((v, tv), body), expr) ->
let body = replace body in
let expr = replace expr in
let v = replace_var v in
return @@ E_iterator (name, ((v, tv), body), expr)
| E_fold (((v, tv), body), collection, initial) ->
let body = replace body in
let collection = replace collection in
let initial = replace initial in
let v = replace_var v in
return @@ E_fold (((v, tv), body), collection, initial)
| E_fold_right (((v, tv), body), (collection, elem_tv), initial) ->
let body = replace body in
let collection = replace collection in
let initial = replace initial in
let v = replace_var v in
return @@ E_fold_right (((v, tv), body), (collection, elem_tv), initial)
| E_if_bool (c, bt, bf) ->
let c = replace c in
let bt = replace bt in
let bf = replace bf in
return @@ E_if_bool (c, bt, bf)
| E_if_none (c, bt, ((v, tv), bf)) ->
let c = replace c in
let bt = replace bt in
let bf = replace bf in
let v = replace_var v in
return @@ E_if_none (c, bt, ((v, tv), bf))
| E_if_cons (c, bf, (((v1, tv1), (v2, tv2)), bt)) ->
let c = replace c in
let bf = replace bf in
let v1 = replace_var v1 in
let v2 = replace_var v2 in
let bt = replace bt in
return @@ E_if_cons (c, bf, (((v1, tv1), (v2, tv2)), bt))
| E_if_left (c, ((v1, tv1), bt), ((v2, tv2), bf)) ->
let c = replace c in
let bf = replace bf in
let v1 = replace_var v1 in
let v2 = replace_var v2 in
let bt = replace bt in
return @@ E_if_left (c, ((v1, tv1), bt), ((v2, tv2), bf))
| E_let_in (e1, inline, ((v, tv), e2)) ->
let v = replace_var v in
let e1 = replace e1 in
let e2 = replace e2 in
return @@ E_let_in (e1, inline, ((v, tv), e2))
| E_tuple exprs ->
let exprs = List.map ~f:replace exprs in
return @@ E_tuple exprs
| E_let_tuple (expr, (vtvs, body)) ->
let expr = replace expr in
let vtvs = List.map ~f:(fun (v, tv) -> replace_var v, tv) vtvs in
let body = replace body in
return @@ E_let_tuple (expr, (vtvs, body))
| E_proj (expr, i, n) ->
let expr = replace expr in
return @@ E_proj (expr, i, n)
| E_update (expr, i, update, n) ->
let expr = replace expr in
let update = replace update in
return @@ E_update (expr, i, update, n)
| E_raw_michelson code -> return @@ E_raw_michelson code
| E_inline_michelson (code, args') ->
let args' = List.map ~f:replace args' in
return @@ E_inline_michelson (code, args')
| E_global_constant (hash, args) ->
let args = List.map ~f:replace args in
return @@ E_global_constant (hash, args)
| E_create_contract (p, s, ((x, t), code), args) ->
let args = List.map ~f:replace args in
let x = replace_var x in
let code = replace code in
return @@ E_create_contract (p, s, ((x, t), code), args)
(* Mutable stuff. We treat immutable and mutable variables
identically because they share the context (e.g. a mutable
variables might need to be renamed for capture-avoidance during
substitution of an immutable variable.) *)
| E_let_mut_in (e1, ((v, tv), e2)) ->
let v = replace_var v in
let e1 = replace e1 in
let e2 = replace e2 in
return @@ E_let_mut_in (e1, ((v, tv), e2))
| E_deref v ->
let v = replace_var v in
return @@ E_deref v
| E_assign (v, e) ->
let v = replace_var v in
let e = replace e in
return @@ E_assign (v, e)
| E_for (start, final, incr, ((x, a), body)) ->
let start = replace start in
let final = replace final in
let incr = replace incr in
let x = replace_var x in
let body = replace body in
return @@ E_for (start, final, incr, ((x, a), body))
| E_for_each (coll, coll_type, (xs, body)) ->
let coll = replace coll in
let xs = List.map ~f:(fun (x, a) -> replace_var x, a) xs in
let body = replace body in
return @@ E_for_each (coll, coll_type, (xs, body))
| E_while (cond, body) ->
let cond = replace cond in
let body = replace body in
return @@ E_while (cond, body)


(** Set with free variables. *)
module Fvs = Set.Make (Value_var)

Expand Down
163 changes: 163 additions & 0 deletions src/passes/15-self_mini_c/rename.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,163 @@
open Mini_c
open Ligo_prim
module Var_map = Map.Make (Value_var)

(** Global alpha renaming *)

(**
The main goal is to ensures that every binder has a unique name globally.

The main advantage is that a transformation such
as moving a let will never capture a variable.

let x = (let y = M in N) in K ↦ let y = M; let x = N in K
*)
let rec rename ~substs expr =
let self expr = rename ~substs expr in
let with_binder ~substs v =
let v' = Value_var.fresh_like v in
v', Map.update substs v ~f:(fun _ -> v')
in
let self_with_binder v ~body =
let v, substs = with_binder ~substs v in
let body = rename ~substs body in
v, body
in
let self_with_binder_pair (v1, v2) ~body =
let v1, substs = with_binder ~substs v1 in
let v2, substs = with_binder ~substs v2 in
let body = rename ~substs body in
(v1, v2), body
in
let self_with_binders vs ~body =
let rev_vs, substs =
List.fold_left vs ~init:([], substs) ~f:(fun (rev_vs, substs) (v, vt) ->
let v, substs = with_binder ~substs v in
let rev_vs = (v, vt) :: rev_vs in
rev_vs, substs)
in
let body = rename ~substs body in
List.rev rev_vs, body
in
let solve_variable v =
match Map.find substs v with
| Some v' -> v'
| None ->
(* TODO: why does this happen? *)
v
in
let return_expr content = { expr with content } in
match expr.content with
(* Here actual substitutions are created. *)
| E_let_in (expr, inline, ((v, tv), body)) ->
let expr = self expr in
let v, body = self_with_binder v ~body in
return_expr @@ E_let_in (expr, inline, ((v, tv), body))
| E_let_mut_in (expr, ((v, tv), body)) ->
let expr = self expr in
let v, body = self_with_binder v ~body in
return_expr @@ E_let_mut_in (expr, ((v, tv), body))
(* Variables and dereferencing. *)
| E_variable v ->
let v = solve_variable v in
return_expr @@ E_variable v
| E_deref v ->
let v = solve_variable v in
return_expr @@ E_deref v
(* Other stuff. *)
| E_closure { binder; body } ->
let binder, body = self_with_binder binder ~body in
return_expr @@ E_closure { binder; body }
| E_rec { func = { binder; body }; rec_binder } ->
let (binder, rec_binder), body = self_with_binder_pair (binder, rec_binder) ~body in
return_expr @@ E_rec { func = { binder; body }; rec_binder }
| E_tuple exprs ->
let exprs = List.map ~f:self exprs in
return_expr @@ E_tuple exprs
| E_let_tuple (expr, (vtvs, body)) ->
let expr = self expr in
let vtvs, body = self_with_binders vtvs ~body in
return_expr @@ E_let_tuple (expr, (vtvs, body))
| E_proj (expr, i, n) ->
let expr = self expr in
return_expr @@ E_proj (expr, i, n)
| E_update (expr, i, update, n) ->
let expr = self expr in
let update = self update in
return_expr @@ E_update (expr, i, update, n)
| E_iterator (s, ((name, tv), body), collection) ->
let collection = self collection in
let name, body = self_with_binder name ~body in
return_expr @@ E_iterator (s, ((name, tv), body), collection)
| E_fold (((name, tv), body), collection, init) ->
let collection = self collection in
let init = self init in
let name, body = self_with_binder name ~body in
return_expr @@ E_fold (((name, tv), body), collection, init)
| E_fold_right (((name, tv), body), (collection, elem_tv), init) ->
let collection = self collection in
let init = self init in
let name, body = self_with_binder name ~body in
return_expr @@ E_fold_right (((name, tv), body), (collection, elem_tv), init)
| E_if_none (c, n, ((name, tv), s)) ->
let c = self c in
let n = self n in
let name, s = self_with_binder name ~body:s in
return_expr @@ E_if_none (c, n, ((name, tv), s))
| E_if_cons (c, n, (((hd, hdtv), (tl, tltv)), cons)) ->
let c = self c in
let n = self n in
let (hd, tl), cons = self_with_binder_pair (hd, tl) ~body:cons in
return_expr @@ E_if_cons (c, n, (((hd, hdtv), (tl, tltv)), cons))
| E_if_left (c, ((name_l, tvl), l), ((name_r, tvr), r)) ->
let c = self c in
let name_l, l = self_with_binder name_l ~body:l in
let name_r, r = self_with_binder name_r ~body:r in
return_expr @@ E_if_left (c, ((name_l, tvl), l), ((name_r, tvr), r))
| E_raw_michelson code -> return_expr @@ E_raw_michelson code
| E_inline_michelson (code, args) ->
let args' = List.map ~f:self args in
return_expr @@ E_inline_michelson (code, args')
| E_literal _ -> expr
| E_constant { cons_name; arguments } ->
let arguments = List.map ~f:self arguments in
return_expr @@ E_constant { cons_name; arguments }
| E_application (farg1, farg2) ->
let farg1 = self farg1 in
let farg2 = self farg2 in
return_expr @@ E_application (farg1, farg2)
| E_if_bool (cab1, cab2, cab3) ->
let cab1 = self cab1 in
let cab2 = self cab2 in
let cab3 = self cab3 in
return_expr @@ E_if_bool (cab1, cab2, cab3)
| E_global_constant (hash, args) ->
let args = List.map ~f:self args in
return_expr @@ E_global_constant (hash, args)
| E_create_contract (p, s, ((x, t), code), args) ->
let args = List.map ~f:self args in
let x, code = self_with_binder x ~body:code in
return_expr @@ E_create_contract (p, s, ((x, t), code), args)
(* Mutable stuff. We allow substituting mutable variables which
aren't mutated because it was easy. Hmm. *)
| E_assign (v, e) ->
let v = solve_variable v in
let e = self e in
return_expr @@ E_assign (v, e)
| E_for (start, final, incr, ((x, a), body)) ->
let start = self start in
let final = self final in
let incr = self incr in
let x, body = self_with_binder x ~body in
return_expr @@ E_for (start, final, incr, ((x, a), body))
| E_for_each (coll, coll_type, (xs, body)) ->
let coll = self coll in
let xs, body = self_with_binders xs ~body in
return_expr @@ E_for_each (coll, coll_type, (xs, body))
| E_while (cond, body) ->
let cond = self cond in
let body = self body in
return_expr @@ E_while (cond, body)


let rename expr = rename ~substs:Var_map.empty expr
14 changes: 3 additions & 11 deletions src/passes/15-self_mini_c/self_mini_c.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -150,39 +150,30 @@ let beta : bool ref -> expression -> expression =
(* (let x = (let y = e1 in e2) in e3) ↦ (let y = e1 in let x = e2 in e3) *)
| E_let_in ({ content = E_let_in (e1, inline2, ((y, b), e2)); _ }, inline1, ((x, a), e3))
->
let y' = Value_var.fresh_like y in
let e2 = Inline.replace e2 y y' in
changed := true;
{ e with
content =
E_let_in
( e1
, inline2
, ((y', b), { e with content = E_let_in (e2, inline1, ((x, a), e3)) }) )
, ((y, b), { e with content = E_let_in (e2, inline1, ((x, a), e3)) }) )
}
(* note: E_let_tuple/E_let_in and E_let_in/E_let_tuple conversions
not implemented yet because they don't seem important (?) *)
(* (let x = e1 in e2)@e3 ↦ let x = e1 in e2@e3 (if e1 or e3 is pure) *)
| E_application ({ content = E_let_in (e1, inline, ((x, a), e2)); _ }, e3) ->
if is_pure e1 || is_pure e3
then (
let x' = Value_var.fresh_like x in
let e2 = Inline.replace e2 x x' in
changed := true;
{ e with
content =
E_let_in (e1, inline, ((x', a), { e with content = E_application (e2, e3) }))
E_let_in (e1, inline, ((x, a), { e with content = E_application (e2, e3) }))
})
else e
(* (let (x, y, ...) = e1 in e2)@e3 ↦ let (x, y, ...) = e1 in e2@e3 (if e1 or e3 is pure) *)
| E_application ({ content = E_let_tuple (e1, (vars, e2)); _ }, e3) ->
if is_pure e1 || is_pure e3
then (
let vars = List.map ~f:(fun (x, a) -> x, Value_var.fresh_like x, a) vars in
let e2 =
List.fold_left vars ~init:e2 ~f:(fun e2 (x, x', _a) -> Inline.replace e2 x x')
in
let vars = List.map ~f:(fun (_x, x', a) -> x', a) vars in
changed := true;
{ e with
content = E_let_tuple (e1, (vars, { e with content = E_application (e2, e3) }))
Expand Down Expand Up @@ -295,6 +286,7 @@ let rec all_expression ~raise (options : Compiler_options.t) : expression -> exp
else (
let changed = ref false in
let e = inline_lets changed e in
let e = Rename.rename e in
let e = betas changed e in
let e = etas changed e in
let e = not_comparable ~raise e in
Expand Down
Loading