LLVM Compatibility

What version of LLVM IR does Vellvm support?

LLVM IR is a rapidly moving target. Vellvm aims to provide parsing support for all of LLVM IR as of at least Clang version 17. However, the Vellvm formal semantics and interpreter may not support all of LLVM IR’s features. See below for more details.

What features of LLVM IR does Vellvm support?

Vellvm covers most features of the core sequential fragment of LLVM IR as per its informal specification in LangRef.

• basic operations on arbitrary bit-width integers
• doubles, floats, structs, arrays, pointers
• casts
• undef and poison
• SSA-structured control-flow-graphs
• global data
• mutually-recursive functions
• some intrinsics (in a user-extensible way)

What about undef?

The Vellvm semantic model currently includes undef as a source of nondeterminism, so the meaning of an LLVM IR program is a set of possible behaviors. The Vellvm executable interpreter currently picks a default value for undef depending on its type.

What about Undefined Behaviors (UB)?

LLVM IR semantics characterize many operations as resulting in unedefined behavior. For instance, storing to an address in a stack frame that has been deallocated yield UB. The Vellvm semantics tries to clarify and define the situations in which UB can occur. The executable with fail with an assertion when it encounters UB. However, the notion of refinement needed to prove the correctness of optimizations allows any behavior to refine UB.

What computation features are not supported?

• full C++-style exceptions via the landing_pad and related instructions
• architecture-specific floating point values
• inlined assembly
• concurrency and concurrency-related instructions
• some semantics-relevant instruction annotations

What about instruction annotations?

Many LLVM IR instructions support various annotations (such as noalias) that are intended to allow the semantics to trigger undefined behavior under certain circumstances. While Vellvm aims to support as many of these as it can, the set of annotations changes often and the intended meaning can sometimes be unclear, so we try to support them in a best effort but sound way. (That is, we won’t rule a behavior as UB unless it actually is—“true” LLVM IR may exhibit more UB than Vellvm semantics.

What about libraries?

Vellvm does not yet provide support for many C standard library functions, but it does support some basics:

• puts
• printf
• malloc

Additionally, any code that can be expressed a an LLVM IR .ll file can be linked into the Vellvm interpreter. See the code in the src/libll folder and information about running tests for an example.

Miscellany

How do I pronounce “Vellvm”?

It is pronounced like the word “vellum”. (Romans wrote the Latin alphabet using the symbol “v” for both “v” and “u”…)