4 ms·
> In this case, when they say LLVM is verified, they mean that they designed a formal correspondence between the (1) semantics of the LLVM virtual machine langu
by CalChris 10y ago
> In this case, when they say LLVM is verified, they mean that they designed a formal correspondence between the (1) semantics of the LLVM virtual machine language and (2) the actual execution of the underlying CPU (in this case, modeled using actual assembly language).
I don't think that's accurate. Vellvm is verifying transformations of IR rather than executions on any given CPU.
- piemonkey 10y agoYou are right, perhaps my original post was unclear. The goal is to verify the transformation between LLVM and low-level assembly. I embellished slightly by equating the semantics of low-level assembly with CPU executions.
- CalChris 10y agoI'm pretty sure they're talking about IR to IR transformations (e.g. high level IR optimizations) rather than IR to low level assembly transformations (code generator backends). The former is grad school stuff; the latter is hard.