WhyR Metadata

WhyR takes in an LLVM program enhanced with WhyR annotations. These annotations are stored in the form of LLVM metadata nodes. This page contains the format of IR files used by LLVM.

Function definitions and instructions can be annotated with named metadata nodes. WhyR generates annotations for functions with metadata nodes named whyr.requires and whyr.ensures, and instructions pay attention to whyr.assert and whyr.assume. The contents of these nodes represent a clause in WhyR annotation format. The format accepts either LLVM constants or metadata subnodes, which are parsed in an s-expression like format.

For example, a function can have an ensures clause of the following s-expression:

(eq (result) (add 2 2))

By converting it into the following LLVM IR:

define i32 @function() !whyr.ensures !{!{!"eq", !{!"result"}, !{!"add", i32 2, i32 2}}} {
    %a = add i32 2, 2
    ret i32 %a
}

See src/parser.cpp for a list of s-expressions the WhyR parser currently can accept.

Format Notes

Note that the first enclosing !{} around the argument to !whyr.ensures is necessary; it is a part of LLVM syntax that all named metadata has to be inside a node. For example, this program requires true:

define void @function() !whyr.requires !{!{!"true"}} {
    ret void
}

While this program is a WhyR syntax error, because WhyR is receiving just a string, and not an expression node:

define void @function() !whyr.requires !{!"true"} {
    ret void
}

Asserts/Assumes

Here's a small example of how to add asserts and assumes to LLVM:

define void @function() {
    %a = add i32 2, 2
    ret void, !whyr.assert !{!{!"eq", !{!"var", !"a"}, i32 4}}
}

Assigns

Take a look at the following program:

@a = global i32 0
@b = global i32 0

define void @set_b(i32 %x) {
    store i32 %x, i32* @b
    ret void
}

define void @set_a_b(i32 %x) {
    store i32 %x, i32* @a
    call void(i32) @set_b(i32 %x)
    ret void
}

If you attempt to ensure that (eq (load @a) %x) after the call to @set_a_b like so:

@a = global i32 0
@b = global i32 0

define void @set_b(i32 %x) {
    store i32 %x, i32* @b
    ret void
}

define void @set_a_b(i32 %x) !whyr.ensures !{!{!"eq", !{!"load", i32* @a}, !{!"arg", !"x"}}} {
    store i32 %x, i32* @a
    call void(i32) @set_b(i32 %x)
    ret void
}

The goals generated will not prove. This is because, after the call to @set_b, @a could have been assigned to anything. Why is this so? Because of how WhyR works, it cannot see that @set_b only modifies @b, and assumes it could possibly modify any memory it wanted to.

Assigns clauses allow you to specify the maximal possibly set of memory locations a function is able to change. They are made with the !whyr.assigns tag in the function contract. An assigns clause consists of a number of sets of memory locations. Here's an assigns clause that works for @set_b:

(set (typeof @b) @b)

Which means "a set of pointers, consisting of @b". This looks like this in WhyR metadata:

@a = global i32 0
@b = global i32 0

define void @set_b(i32 %x) !whyr.assigns !{!{!"set", !{!"typeof", i32* @b}, i32* @b}} {
    store i32 %x, i32* @b
    ret void
}

define void @set_a_b(i32 %x) !whyr.ensures !{!{!"eq", !{!"load", i32* @a}, !{!"arg", !"x"}}} {
    store i32 %x, i32* @a
    call void(i32) @set_b(i32 %x)
    ret void
}

The program should now prove.