Better dce by ordinarymath · Pull Request #297 · polyml/polyml · GitHub

Improves the DCE focusing on handling the case when codeUse = [].

This change also implements 2 optimizations Removes code that is conservatively widening empty use into [UseGeneral] Adds cleanDead which attempts to clean whatever that is not needed keeping only the effectful code needed.

Extract the BeginLoop handling in doClean into a shared cleanBeginLoop called by both doClean and cleanDead.

Uses the same logic in doClean case, lifted out to cleanEval. This requires adding support for UseApply([], args) to cleanLambda

Structural refactor only. Replace the per-scope state that cleanProc captured implicitly through its closure with a context instead.

@dcjm supposing you approve of this changes I don't mind running a full build of HOL building all the examples + CakeML proofs to test this before you merge this change.
@mdesharnais might be interested in doing a similar check for Isabelle.

Another side note @dcjm I suspect the dead argument removal in this pass, RemoveRedundant is potentially buggy.

polyml/mlsource/MLCompiler/CodeTree/CodetreeRemoveRedundant.ML

Lines 347 to 394 in d615dad

    
                               (* Remove unused arguments.  They're unnecessary and may cause problems 
        
                                  later on. *) 
        
                               fun filterUnused [] = ([], []) 
        
                               |   filterUnused(({value, addr, ...}, t) :: args) = 
        
                                   let 
        
                                       val (used, discards) = filterUnused args 
        
                                   in 
        
                                       case Array.sub(locals, addr) of 
        
                                           [] => (* We only need to keep this if it might have a side-effect. *) 
        
                                               (used, NullBinding(cleanCode(value, [UseGeneral])) :: discards) 
        
                                       |   use => (({value=cleanCode(value, use), addr=addr, use=use}, t) :: used, discards) 
        
                                   end 
        
                               val (usedArgs, discards) = filterUnused arguments 
        
                           in 
        
                               if not(null discards) 
        
                               then 
        
                               let 
        
                                   fun splitArgs([], []) = ([], []) 
        
                                   |   splitArgs((arg as (argVal, _)) :: args, ({addr, ...}, _) :: arguments) = 
        
                                       let 
        
                                           val (useArgs, discards) = splitArgs(args, arguments) 
        
                                       in 
        
                                           (* We actually only need to keep this argument if it might have 
        
                                              a side-effect but keep it anyway. *) 
        
                                           case Array.sub(locals, addr) of 
        
                                               [] => (useArgs, NullBinding argVal :: discards) 
        
                                           |   _ => (arg :: useArgs, discards) 
        
                                       end 
        
                                   |   splitArgs _ = raise InternalError "splitArgs" 
        
                                   fun filterLoopArgs(Loop l) = 
        
                                       let 
        
                                           val (useArgs, discards) = splitArgs(l, arguments) 
        
                                       in 
        
                                           SOME(Newenv(discards, Loop useArgs)) 
        
                                       end 
        
                                       (* Don't descend into functions or inner loops. *) 
        
                                   |   filterLoopArgs(instr as Lambda _) = SOME instr 
        
                                   |   filterLoopArgs(instr as BeginLoop _) = SOME instr 
        
                                   |   filterLoopArgs _ = NONE 
        
                                   val newLoop = 
        
                                       BeginLoop {loop = mapCodetree filterLoopArgs cleanBody, arguments = usedArgs} 
        
                               in 
        
                                   SOME(Newenv(discards, newLoop)) 
        
                               end 
        
                               else SOME(BeginLoop {loop = cleanBody, arguments = usedArgs}) 
        
                           end

Consider you have (arg1,arg2,arg3) where all the args are effectful and arg2 is dead.
The effect of arg2 would be executed before arg1. I don't think it's buggy rn because there's isn't any inlining so args for Loops are always locals/ args /closures etc. but could be a potential bug. I haven't tried to fix this potential bug in this PR.

I suspect for the potential bug highlighted above should be done in the optimizer anyway since this doesn't do the detupling of loop args too.

I might get rid of d48249d I tried implementing the TODO i added here and it seems like extending removeRedundant with a more precise liveness analysis is hard and going to be inefficient compared to a additional liveness analysis pass

d48249d is now removed

fun k (a,b) = a + b;
fun f g x = k (let fun r y = y in r (g x handle e => (r 0; raise e)) end);

This raises an internal error

ordinarymath added 4 commits August 4, 2026 21:30

Make cleanCode safe with null codeUse

d5d979b

This change also implements 2 optimizations Removes code that is conservatively widening empty use into [UseGeneral] Adds cleanDead which attempts to clean whatever that is not needed keeping only the effectful code needed.

Optimize BeginLoop case in cleanDead.

72dc030

Extract the BeginLoop handling in doClean into a shared cleanBeginLoop called by both doClean and cleanDead.

Optimize Eval case in cleanDead

8ea1a8b

Uses the same logic in doClean case, lifted out to cleanEval. This requires adding support for UseApply([], args) to cleanLambda

refactor CodetreeRemoveRedundant to use explicit context

eb29200

Structural refactor only. Replace the per-scope state that cleanProc captured implicitly through its closure with a context instead.

Add missing handle case in doClean

0046006

ordinarymath force-pushed the better_dce branch from 6333b81 to 0046006 Compare August 28, 2026 07:41

ordinarymath mentioned this pull request Aug 28, 2026

Better optimiser #300

Draft

ordinarymath marked this pull request as draft August 28, 2026 12:11

Better dce by ordinarymath · Pull Request #297 · polyml/polyml · GitHub

Uh oh!

Better dce - #297

Better dce#297
ordinarymath wants to merge 5 commits into
polyml:masterfrom
ordinarymath:better_dce

ordinarymath commented Aug 4, 2026

Uh oh!

ordinarymath commented Aug 4, 2026

Uh oh!

ordinarymath commented Aug 4, 2026 •
edited
Loading

Uh oh!

Uh oh!

ordinarymath commented Aug 4, 2026

Uh oh!

ordinarymath commented Aug 13, 2026 •
edited
Loading

Uh oh!

Uh oh!

ordinarymath commented Aug 28, 2026

Uh oh!

ordinarymath commented Aug 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Better dce by ordinarymath · Pull Request #297 · polyml/polyml · GitHub

Uh oh!

Better dce - #297

Better dce#297ordinarymath wants to merge 5 commits intopolyml:masterpolyml/polyml:masterfrom ordinarymath:better_dceordinarymath/polyml:better_dceCopy head branch name to clipboard

Conversation

ordinarymath commented Aug 4, 2026

Uh oh!

ordinarymath commented Aug 4, 2026

Uh oh!

ordinarymath commented Aug 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ordinarymath commented Aug 4, 2026

Uh oh!

ordinarymath commented Aug 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ordinarymath commented Aug 28, 2026

Uh oh!

ordinarymath commented Aug 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Better dce#297
ordinarymath wants to merge 5 commits into
polyml:masterfrom
ordinarymath:better_dce

ordinarymath commented Aug 4, 2026 •
edited
Loading

ordinarymath commented Aug 13, 2026 •
edited
Loading