Skeleton and initial support for proof-carrying code.

[cfallin]

This PR adds basic support for "facts" to annotate SSA values and VCode VRegs. The idea is that these facts describe properties of the values -- currently, "in a given range" or "points to valid memory of a given size" -- and by validating a chain of facts along the whole derivation of an accessed memory address, we can verify that the memory access is safe.

This is the start of work on the ideas described in #6090. It is a new approach that subsumes/replaces "VeriWasm": it replaces the post-hoc derive-all-facts analysis approach (which is slow and brittle) with a cooperative approach in which the codegen frontend generates a "proof witness" of sorts, we preserve that, and we check that in the machine code (actually the pre-regalloc VCode, and then we can use the regalloc's symbolic checker to obtain the same guarantee).

Right now, this includes (i) the "fact" data structures, (ii) support for parsing these facts in CLIF and dumping them back out, (iii) propagation of facts from CLIF to VCode, when no optimization is enabled, and (iv) validation of a few basic facts in VCode for the AArch64 backend. Everything else is still TODO and will come in further PRs.

Right now, this is sufficient to take the CLIF

test compile
set enable_pcc=true
target aarch64

function %simple1(i64 vmctx, i32) -> i8 {
block0(v0 ! points_to(0x1_0000_0000): i64, v1 ! max(32, 0xffff_ffff): i32):
    v2 ! max(64, 0xffff_ffff) = uextend.i64 v1
    v3 ! points_to(0x1) = iadd.i64 v0, v2
    v4 = load.i8 safe v3
    return v4
}

where the v0 ! fact syntax annotates v0 with a fact, and validate that the load is in fact safe. The safe memory-flag forces this check; if the points_to range is shrunk, or v1 is changed to an i64 and its max range is increased, this code will fail to compile with

 ERROR cranelift_filetests::concurrent > FAIL: compile
FAIL cranelift/filetests/filetests/pcc/simple.clif: compile

Caused by:
    Proof-carrying-code validation error: MissingFact

The idea is to continue further work along these lines:

• Add support for validating facts produced by aarch64 add, shift, ... instructions -- whatever is used in basic address generation.
• Add support for validating amode usage in x64 as well.
• Propagate facts through the egraph layer so they are preserved during optimization.
• Add a richer points_to language for facts to describe what they point to, so a load of a memory base address (for example) from vmctx yields another value with an attached fact (points to a region of this size...). These are the "memory capabilities" described in Verification of addressing / memory accesses with VeriWasm or similar #6090.
• Emit facts on vmctx and on memory-access sequences generated by cranelift-wasm, and add the safe flag to loads/stores wherever possible. At this point, we should be able to validate single- and multi-memory Wasm modules with static memory configurations.
• Add support for annotations on bounds-check logic. After this, we should be able to validate dynamic memories, and table accesses as well.
• Finally, add a "strong enforcing" mode that disallows all non-safe loads/stores, and add whatever memory-capability info is needed so that, e.g., loads of func pointers, VM state, and everything else from vmctx is covered.

After my initial exploration and ideas in #6090, these ideas were further discussed with @fitzgen, @elliottt, @jameysharp, and others; and a large part of this PR was

Co-authored-by: Nick Fitzgerald fitzgen@gmail.com

[github-actions]

Subscribe to Label Action

cc @peterhuene

This issue or pull request has been labeled: "cranelift", "cranelift:area:aarch64", "cranelift:area:machinst", "cranelift:area:x64", "cranelift:meta", "wasmtime:api"

Thus the following users have been cc'd because of the following labels:

• peterhuene: wasmtime:api

To subscribe or unsubscribe from this label, edit the .github/subscribe-to-label.json configuration file.

Learn more.

[fitzgen]

Very excited for this! r=me with comments, some of which can be deferred to follow up PRs.