Closed spernsteiner closed 8 months ago
is this doing equality saturation? it looks very familiar to the approach egg
takes with egraphs, so i'm curious why something like that wasn't used and why this was done by hand?
It's a little difficult for me to review this for correctness, especially given there are no tests. How can I be most useful to you here as a reviewer? One of my concerns is that it's all hand-made with no reference to a standard equivalence constraint solving algorithm. We do this in a few places and it seems repetitious and error-prone; please tell me if my concerns are overblown.
This branch adds an analysis that computes a set of possible pointee types for each pointer. It includes only the analysis; the analysis results aren't used to drive any rewriting yet. On
algo_md5
, the analysis correctly identifies that the_input
argument toMD5_Update
should actually point tou8
s, that thememset
inli_MD5Transform
operates onu32
s, and that thememset
inMD5_Final
operates on anMD5_CTX
.The next step after this will be to use the analysis results in rewriting. We need to rewrite pointer types to use the inferred pointees (such as changing
_input: &c_void
to_input: &[u8]
), replacememcpy
andmemset
with safe operations, and (optionally) delete casts that are now no-ops (such asinput = _input as *const c_uchar
, onceinput
and_input
are both rewritten to&[u8]
). This may also require some changes to our currentvoid*
cast handling.