Skip to content

Commit 4d2aedf

Browse files
authored
feat: speed up check_ir by caching sub, lub and check_typ tests (#5260)
Building CycleOps with check-ir on takes a long time with ir type checking turned on (the default) ``` real 1m31.395s user 1m31.210s sys 0m0.166s ``` Adding some naive caching of subtype, lub and type well-formedness checks speeds this up quite a lot: ``` real 0m25.385s user 0m25.236s sys 0m0.148s ``` With no-check-ir, the time is: ``` real 0m12.299s user 0m12.205s sys 0m0.092s ``` (similar optimizations might improve the source typecheck.ml) Proof: Master: ``` crusso@crusso-Virtual-Machine:~/CycleOps$ time "/home/crusso/clean/motoko/bin/moc" "/home/crusso/CycleOps/canisters/cycleops/main.mo" "-o" "/home/crusso/CycleOps/.dfx/local/canisters/cycleops/cycleops.wasm" "-c" "--debug" "--idl" "--stable-types" "--public-metadata" "candid:service" "--public-metadata" "candid:args" "--actor-idl" "/home/crusso/CycleOps/.dfx/local/canisters/idl/" "--actor-alias" "cycleops" "bkyz2-fmaaa-aaaaa-qaaaq-cai" "--actor-alias" "internet_identity" "qhbym-qaaaa-aaaaa-aaafq-cai" "--actor-alias" "mock-management" "aaaaa-aa" "--actor-alias" "nns-cycles-minting" "rkp4c-7iaaa-aaaaa-aaaca-cai" "--actor-alias" "nns-genesis-token" "renrk-eyaaa-aaaaa-aaada-cai" "--actor-alias" "nns-governance" "rrkah-fqaaa-aaaaa-aaaaq-cai" "--actor-alias" "nns-identity" "rdmx6-jaaaa-aaaaa-aaadq-cai" "--actor-alias" "nns-ledger" "ryjl3-tyaaa-aaaaa-aaaba-cai" "--actor-alias" "nns-lifeline" "rno2w-sqaaa-aaaaa-aaacq-cai" "--actor-alias" "nns-registry" "rwlgt-iiaaa-aaaaa-aaaaa-cai" "--actor-alias" "nns-root" "r7inp-6aaaa-aaaaa-aaabq-cai" "--actor-alias" "nns-sns-wasm" "qaa6y-5yaaa-aaaaa-aaafa-cai" "--package" "account" ".vessel/account/a718d61a8a4086ce13056681567535f975ac0ddf/src" "--package" "account-identifier" ".vessel/account-identifier/d07f70f572fc0d4cfe44333276c92611de3e0d44/src" "--package" "array" ".vessel/array/v0.2.1/src" "--package" "base" ".vessel/base/moc-0.12.1/src" "--package" "base-0.7.3" ".vessel/base-0.7.3/aafcdee0c8328087aeed506e64aa2ff4ed329b47/src" "--package" "btree" ".vessel/btree/v0.3.4/src" "--package" "crypto" ".vessel/crypto/v0.3.1/src" "--package" "encoding" ".vessel/encoding/v0.4.1/src" "--package" "hash" ".vessel/hash/v0.1.1/src" "--package" "hashmap" ".vessel/hashmap/v8.0.0/src" "--package" "io" ".vessel/io/v0.3.2/src" "--package" "matchers" ".vessel/matchers/v1.2.0/src" "--package" "principal" ".vessel/principal/v0.2.6/src" "--package" "rand" ".vessel/rand/v0.2.1/src" "--package" "sha2" ".vessel/sha2/fb2d19d6d29406d3294a3f514d2b87f928f87bbf/src" "--package" "stable-buffer" ".vessel/stable-buffer/v1.3.0/src" "--package" "testing" ".vessel/testing/v0.1.3/src" "--package" "ulid" ".vessel/ulid/v0.1.3/src" "--enhanced-orthogonal-persistence" real 1m29.139s user 1m29.010s sys 0m0.124s ``` This branch: ``` crusso@crusso-Virtual-Machine:~/CycleOps$ time "/home/crusso/clean/motoko/bin/moc" "/home/crusso/CycleOps/canisters/cycleops/main.mo" "-o" "/home/crusso/CycleOps/.dfx/local/canisters/cycleops/cycleops.wasm" "-c" "--debug" "--idl" "--stable-types" "--public-metadata" "candid:service" "--public-metadata" "candid:args" "--actor-idl" "/home/crusso/CycleOps/.dfx/local/canisters/idl/" "--actor-alias" "cycleops" "bkyz2-fmaaa-aaaaa-qaaaq-cai" "--actor-alias" "internet_identity" "qhbym-qaaaa-aaaaa-aaafq-cai" "--actor-alias" "mock-management" "aaaaa-aa" "--actor-alias" "nns-cycles-minting" "rkp4c-7iaaa-aaaaa-aaaca-cai" "--actor-alias" "nns-genesis-token" "renrk-eyaaa-aaaaa-aaada-cai" "--actor-alias" "nns-governance" "rrkah-fqaaa-aaaaa-aaaaq-cai" "--actor-alias" "nns-identity" "rdmx6-jaaaa-aaaaa-aaadq-cai" "--actor-alias" "nns-ledger" "ryjl3-tyaaa-aaaaa-aaaba-cai" "--actor-alias" "nns-lifeline" "rno2w-sqaaa-aaaaa-aaacq-cai" "--actor-alias" "nns-registry" "rwlgt-iiaaa-aaaaa-aaaaa-cai" "--actor-alias" "nns-root" "r7inp-6aaaa-aaaaa-aaabq-cai" "--actor-alias" "nns-sns-wasm" "qaa6y-5yaaa-aaaaa-aaafa-cai" "--package" "account" ".vessel/account/a718d61a8a4086ce13056681567535f975ac0ddf/src" "--package" "account-identifier" ".vessel/account-identifier/d07f70f572fc0d4cfe44333276c92611de3e0d44/src" "--package" "array" ".vessel/array/v0.2.1/src" "--package" "base" ".vessel/base/moc-0.12.1/src" "--package" "base-0.7.3" ".vessel/base-0.7.3/aafcdee0c8328087aeed506e64aa2ff4ed329b47/src" "--package" "btree" ".vessel/btree/v0.3.4/src" "--package" "crypto" ".vessel/crypto/v0.3.1/src" "--package" "encoding" ".vessel/encoding/v0.4.1/src" "--package" "hash" ".vessel/hash/v0.1.1/src" "--package" "hashmap" ".vessel/hashmap/v8.0.0/src" "--package" "io" ".vessel/io/v0.3.2/src" "--package" "matchers" ".vessel/matchers/v1.2.0/src" "--package" "principal" ".vessel/principal/v0.2.6/src" "--package" "rand" ".vessel/rand/v0.2.1/src" "--package" "sha2" ".vessel/sha2/fb2d19d6d29406d3294a3f514d2b87f928f87bbf/src" "--package" "stable-buffer" ".vessel/stable-buffer/v1.3.0/src" "--package" "testing" ".vessel/testing/v0.1.3/src" "--package" "ulid" ".vessel/ulid/v0.1.3/src" "--enhanced-orthogonal-persistence" real 0m24.895s user 0m24.784s sys 0m0.111s ``` This branch (-no-check-ir): ``` crusso@crusso-Virtual-Machine:~/CycleOps$ time "/home/crusso/clean/motoko/bin/moc" "/home/crusso/CycleOps/canisters/cycleops/main.mo" "-o" "/home/crusso/CycleOps/.dfx/local/canisters/cycleops/cycleops.wasm" "-c" "--debug" "--idl" "--stable-types" "--public-metadata" "candid:service" "--public-metadata" "candid:args" "--actor-idl" "/home/crusso/CycleOps/.dfx/local/canisters/idl/" "--actor-alias" "cycleops" "bkyz2-fmaaa-aaaaa-qaaaq-cai" "--actor-alias" "internet_identity" "qhbym-qaaaa-aaaaa-aaafq-cai" "--actor-alias" "mock-management" "aaaaa-aa" "--actor-alias" "nns-cycles-minting" "rkp4c-7iaaa-aaaaa-aaaca-cai" "--actor-alias" "nns-genesis-token" "renrk-eyaaa-aaaaa-aaada-cai" "--actor-alias" "nns-governance" "rrkah-fqaaa-aaaaa-aaaaq-cai" "--actor-alias" "nns-identity" "rdmx6-jaaaa-aaaaa-aaadq-cai" "--actor-alias" "nns-ledger" "ryjl3-tyaaa-aaaaa-aaaba-cai" "--actor-alias" "nns-lifeline" "rno2w-sqaaa-aaaaa-aaacq-cai" "--actor-alias" "nns-registry" "rwlgt-iiaaa-aaaaa-aaaaa-cai" "--actor-alias" "nns-root" "r7inp-6aaaa-aaaaa-aaabq-cai" "--actor-alias" "nns-sns-wasm" "qaa6y-5yaaa-aaaaa-aaafa-cai" "--package" "account" ".vessel/account/a718d61a8a4086ce13056681567535f975ac0ddf/src" "--package" "account-identifier" ".vessel/account-identifier/d07f70f572fc0d4cfe44333276c92611de3e0d44/src" "--package" "array" ".vessel/array/v0.2.1/src" "--package" "base" ".vessel/base/moc-0.12.1/src" "--package" "base-0.7.3" ".vessel/base-0.7.3/aafcdee0c8328087aeed506e64aa2ff4ed329b47/src" "--package" "btree" ".vessel/btree/v0.3.4/src" "--package" "crypto" ".vessel/crypto/v0.3.1/src" "--package" "encoding" ".vessel/encoding/v0.4.1/src" "--package" "hash" ".vessel/hash/v0.1.1/src" "--package" "hashmap" ".vessel/hashmap/v8.0.0/src" "--package" "io" ".vessel/io/v0.3.2/src" "--package" "matchers" ".vessel/matchers/v1.2.0/src" "--package" "principal" ".vessel/principal/v0.2.6/src" "--package" "rand" ".vessel/rand/v0.2.1/src" "--package" "sha2" ".vessel/sha2/fb2d19d6d29406d3294a3f514d2b87f928f87bbf/src" "--package" "stable-buffer" ".vessel/stable-buffer/v1.3.0/src" "--package" "testing" ".vessel/testing/v0.1.3/src" "--package" "ulid" ".vessel/ulid/v0.1.3/src" "-no-check-ir" "--enhanced-orthogonal-persistence" real 0m12.603s user 0m12.500s sys 0m0.102s ```
1 parent f0ffc3b commit 4d2aedf

File tree

2 files changed

+42
-5
lines changed

2 files changed

+42
-5
lines changed

Changelog.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
# Motoko compiler changelog
22

3+
* motoko (`moc`)
4+
5+
* optimization: accelerate IR type checking with caching of sub, lub and check_typ tests (#5260). Reduces need for `-no-check-ir` flag.
6+
37
## 0.14.12 (2025-06-12)
48

59
* motoko (`moc`)

src/ir_def/check_ir.ml

Lines changed: 38 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ module E = Ir_effect
1414

1515
(* TODO: check escape of free mutables via actors *)
1616

17+
18+
1719
(* Helpers *)
1820

1921
let (==>) p q = not p || q
@@ -54,6 +56,9 @@ type con_env = T.ConSet.t
5456

5557
type lvl = TopLvl | NotTopLvl
5658

59+
module Set = Set.Make(T.Ord)
60+
module MapPair = Map.Make(T.OrdPair)
61+
5762
type env =
5863
{ flavor : Ir.flavor;
5964
lvl : lvl;
@@ -64,6 +69,9 @@ type env =
6469
async : T.con option;
6570
seen : con_env ref;
6671
check_run : int;
72+
check_typ_cache : Set.t ref;
73+
sub_cache : bool MapPair.t ref;
74+
lub_cache : T.typ MapPair.t ref;
6775
}
6876

6977
let last_run : int ref = ref 0
@@ -82,8 +90,28 @@ let initial_env flavor : env =
8290
| QueryCap c | AwaitCap c | AsyncCap c | CompositeCap c | CompositeAwaitCap c | SystemCap c -> Some c);
8391
seen = ref T.ConSet.empty;
8492
check_run;
93+
check_typ_cache = ref Set.empty;
94+
sub_cache = ref MapPair.empty;
95+
lub_cache = ref MapPair.empty
8596
}
8697

98+
let sub env t1 t2 =
99+
if t1 == t2 then true else
100+
match MapPair.find_opt (t1, t2) !(env.sub_cache) with
101+
| Some b -> b
102+
| None ->
103+
let b = T.sub t1 t2 in
104+
env.sub_cache := MapPair.add (t1, t2) b !(env.sub_cache);
105+
b
106+
107+
let lub env t1 t2 =
108+
if t1 == t2 then t1 else
109+
match MapPair.find_opt (t1, t2) !(env.lub_cache) with
110+
| Some t -> t
111+
| None ->
112+
let t = T.lub t1 t2 in
113+
env.lub_cache := MapPair.add (t1, t2) t !(env.lub_cache);
114+
t
87115

88116
(* More error bookkeeping *)
89117

@@ -125,7 +153,7 @@ let disjoint_union env at fmt env1 env2 =
125153

126154
(* FIX ME: these error reporting functions are eager and will construct unnecessary type strings !*)
127155
let check_sub env at t1 t2 =
128-
if not (T.sub t1 t2) then
156+
if not (sub env t1 t2) then
129157
error env at "subtype violation:\n %s\n %s\n"
130158
(T.string_of_typ_expand t1) (T.string_of_typ_expand t2)
131159

@@ -317,7 +345,7 @@ and check_typ_bounds env (tbs : T.bind list) typs at : unit =
317345
error env at "too few type arguments";
318346
List.iter2
319347
(fun tb typ ->
320-
check env at (T.sub typ (T.open_ typs tb.T.bound))
348+
check env at (sub env typ (T.open_ typs tb.T.bound))
321349
"type argument does not match parameter bound")
322350
tbs typs
323351

@@ -326,6 +354,11 @@ and check_inst_bounds env tbs typs at =
326354
List.iter (check_typ env) typs;
327355
check_typ_bounds env tbs typs at
328356

357+
let check_typ env typ =
358+
if Set.mem typ !(env.check_typ_cache) then () else
359+
check_typ env typ;
360+
env.check_typ_cache := Set.add typ !(env.check_typ_cache);
361+
329362
(* Literals *)
330363

331364
open Ir
@@ -968,7 +1001,7 @@ and check_case env t_pat t {it = {pat; exp}; _} =
9681001
let ve = check_pat env pat in
9691002
check_sub env pat.at t_pat pat.note;
9701003
check_exp (adjoin_vals env ve) exp;
971-
check env pat.at (T.sub (typ exp) t) "bad case"
1004+
check env pat.at (sub env (typ exp) t) "bad case"
9721005

9731006
(* Arguments *)
9741007

@@ -1003,7 +1036,7 @@ and gather_pat env const ve0 pat : val_env =
10031036
List.fold_left go ve (pats_of_obj_pat pfs)
10041037
| AltP (pat1, pat2) ->
10051038
let ve1, ve2 = go ve pat1, go ve pat2 in
1006-
let common i1 i2 = { typ = T.lub i1.typ i2.typ; loc_known = i1.loc_known && i2.loc_known; const = i1.const && i2.const } in
1039+
let common i1 i2 = { typ = lub env i1.typ i2.typ; loc_known = i1.loc_known && i2.loc_known; const = i1.const && i2.const } in
10071040
T.Env.merge (fun _ -> Lib.Option.map2 common) ve1 ve2
10081041
| OptP pat1
10091042
| TagP (_, pat1) ->
@@ -1053,7 +1086,7 @@ and check_pat env pat : val_env =
10531086
t <: pat2.note;
10541087
if T.Env.(keys ve1 <> keys ve2) then
10551088
error env pat.at "set of bindings differ for alternative pattern";
1056-
let common i1 i2 = { typ = T.lub i1.typ i2.typ; loc_known = i1.loc_known && i2.loc_known; const = i1.const && i2.const } in
1089+
let common i1 i2 = { typ = lub env i1.typ i2.typ; loc_known = i1.loc_known && i2.loc_known; const = i1.const && i2.const } in
10571090
T.Env.merge (fun _ -> Lib.Option.map2 common) ve1 ve2
10581091

10591092
and check_pats at env pats ve : val_env =

0 commit comments

Comments
 (0)