search

metamath / metamath-exe

Metamath program - source code for the Metamath executable
GNU General Public License v2.0
77 stars 25 forks source link

shrink live ranges: typeProof, cleanWrkProof #128

Closed digama0 closed 1 year ago

digama0 commented 1 year ago

I'm going to try to make a series of PRs like this which moves allocation/initialization of variables to just before first use and deallocation to just after last use, toward #17 "Move variable declarations from top of function to first use".

david-a-wheeler commented 1 year ago

I haven't reviewed the details, but the general principle sounds great. Historically C only allowed variable declaration at the beginning of a scope (open curly brace), which encouraged "early" allocation.

It might be helpful to compile this with address sanitizer (-fsanitize=address) and run a bunch of tests. (I recommend enabling -O2 for performance and -fno-omit-frame-pointer so the error reports are understandable). That is much slower & takes more memory, so you don't want to do it in "production", but it can detect a lot of problems.

digama0 commented 1 year ago

That sounds like a good idea for the CI. The whole process is still less than a minute so we can definitely afford to run it with more instrumentation.