Annotation Syntax

This section is subject to heavy change as WhyR is refactored and expanded!

Here is a list of example operations in [WAR](The WhyR Annotation Language (WAR)) and their [metadata](WhyR Metadata) counterparts:

WAR	Metadata	Notes
a + b	!{!"add", a, b}	Takes either logical ints, LLVM ints, reals, LLVM floats, or vectors of LLVM ints or floats. Arguments' types much match. Returns the type of the arguments.
a - b	!{!"sub", a, b}	see "add".
a * b	!{!"mul", a, b}	see "add".
a / b	!{!"div", a, b}	div can only be used on logical ints.
a sdiv b	!{!"sdiv", a, b}	sdiv and udiv can only be used on LLVM ints or LLVM int vectors.
a mod b	!{!"mod", a, b}	mod can only be used on logical ints
a rem b	!{!"rem", a, b}	rem can only be used on logical ints
%a	!{!"var", !"a"} or !{!"arg", !"a"}	use "arg" if the variable is a function argument
@a	type of @a @a	This returns the pointer to @a, not @a itself
$a	!{!"local", !"a"}	This is a logic-local variable. Created by quantifiers and let statements.
a ? b : c	!{!"ifte", a, b, c}	"a" must be logic boolean. "b" and "c" must be the same type.
a == b	!{!"eq", a, b}	Types of arguments must agree. Returns logic boolean.
a != b	!{!"neq", a, b}	see "eq".
a < b	!{!"lt", a, b}	can only be used on logical ints
a slt b	!{!"slt", a, b}	This is signed-less-than. Corresponds to "icmp slt a, b". Can only be used on LLVM ints
a ult b	!{!"ult", a, b}	This is unsigned-less-than. Corresponds to "icmp ult a, b". Can only be used on LLVM ints
(bool) a	!{!"bool", a}	"a" must be of type i1
forall int $x, ...; a	!{!"forall", !{!{!"x", !{!"typeof", !{!"int", !"0"}}}, ...}, a}	"exists" works in the same way
let int $x = 0, ...; a	!{!"let", !{!{!"x", !{!"typeof", !{!"int", !"0"}}, !{!"int", !"0"}}, ...}, a}
a & b	!{!"band", a, b}	can only be used on LLVM ints or LLVM int vectors.
!a	!{!"not", a}	Argument must be logical boolean. Performs logical NOT.
~a	!{!"bnot", a}	can only be used on LLVM ints or LLVM int vectors.
-a	!{!"neg", a}	Takes either logical ints, LLVM ints, reals, LLVM floats, or vectors of LLVM ints or floats.
a && b	!{!"and", a, b}	Takes logical booleans and produces a logical boolean.
a ==> b	!{!"->", a, b}	see "and".
a <==> b	!{!"<->", a, b}	see "and".
(i32) a	!{!"trunc", !{!"typeof", i32 0}, a}	"a" must be a logic int or a LLVM int greater then i32
(i32 zext) a	!{!"zext", !{!"typeof", i32 0}, a}	"a" must be a LLVM int smaller then i32
(i32 sext) a	!{!"sext", !{!"typeof", i32 0}, a}	"a" must be a LLVM int smaller then i32
(int zext) a	!{!"zext", !{!"typeof", !{!"int", !"0"}}, a}	"a" must be a LLVM int. Treats "a" as unsigned.
(int sext) a	!{!"sext", !{!"typeof", !{!"int", !"0"}}, a}	"a" must be a LLVM int. Treats "a" as signed.
1.0	!{!"real", !"1.0"}	A real constant.
(double) a	!{!"real.to.float", !{!"typeof", double 0.0}, a}	"a" has to be of real type
(int) a	!{!"real.to.int", a}	"a" has to be of real type
(real) a	!{!"float.to.real", a}	"a" has to be a LLVM floating type (double, float, etc.)
(real) a	!{!"int.to.real", a}	"a" has to be an int
a foeq b	!{!"foeq", a, b}	This is float-ordered-equals. Corresponds to "fcmp oeq a, b". Can only be used on LLVM floats
a fugt b	!{!"fugt", a, b}	This is float-unordered-greater-than. Corresponds to "fcmp ugt a, b". Can only be used on LLVM floats
(i32*) null	i32* null	A null pointer.
*a	!{!"load", a}	"a" has to be a pointer type
{(i32)1, (i32)2, (I32)3}	[ 3 x i32 ] [ i32 1, i32 2, i32 3 ]	An LLVM array constant.
{a, b, c...}	!{!"array", !{!"typeof", a}, a, b, c...}	"a", "b", "c"... have to be of the same LLVM type
(i32[]){}	[ 0 x i32 ] []
(i32[0]){}	[ 0 x i32 ] []
a[i]	!{!"get", a, i}	If "a" is an LLVM array or vector, "i" has to be a logic int. If "a" is a struct, "i" also has to be constant.
a[i = v]	!{!"set", a, i, v}	This is the syntax for functional update. "a" must be an LLVM array, vector, or struct. "i" must be a logical int. "v" must be of "a"'s element type. If "a" is a struct, "i" also has to be constant.
(i32)a	!{!"ptr.to.int", !{!"typeof", i32 0}, a}	"a" must be a pointer.
(i32*)a	!{!"int.to.ptr", !{!"typeof", i32* null}, a}	"a" must be an LLVM int.
(i32*)a	!{!"ptr.to.ptr", !{!"typeof", i32* null}, a}	"a" must be a pointer.
&a[b]	!{!"getelementptr", a, b}	"a" must be a pointer. "b" must be intergernal. This corresponds to the LLVM getelementptr instruction.
&a[b][c]	!{!"getelementptr", a, b, c}	"a" must be a pointer to an array. "b" and "c" must be intergernal. This corresponds to the LLVM getelementptr instruction.
(i32 sext) max	!{!"maxint", !{!"typeof", i32 0}}	has to be an LLVM integer type. Returns the maximum signed integer.
(i32 zext) max	!{!"maxuint", !{!"typeof", i32 0}}	has to be an LLVM integer type. Returns the maximum unsigned integer.
(i32 sext) min	!{!"minint", !{!"typeof", i32 0}}	has to be an LLVM integer type. Returns the smallest signed integer.
blockaddress(@func, %label)	i8* blockaddress(@func, %label)	Returns the block address of a function's labelled block. This version cannot handle forward declarations.
blockaddress(@func, %label)	!{!"blockaddress", !"func", !"label"}	Returns the block address of a function's labelled block. This version handles forward declarations.
result	!{!"result"}	The result of the function. Returns an LLVM type.
(struct name) struct {a, b, c...}	%name {a, b, c...}	"name" has to be the name of a named struct.
(struct name) struct {a, b, c...}	!{!"struct", !{!"typeof", %name zeroinitializer}, a, b, c...}	"name" has to be the name of a named struct.
(struct {t1, t2, t3...}) struct {a, b, c...}	{t1, t2, t3...} {a, b, c...}	Returns a literal struct with the given members.
(struct {t1, t2, t3...}) struct {a, b, c...}	!{!"struct", !{!"typeof", {t1, t2, t3...} zeroinitializer}, a, b, c...}	Returns a literal struct with the given members.
(struct <{t1, t2, t3...}>) struct {a, b, c...}	<{t1, t2, t3...}> <{a, b, c...}>	Returns a literal packed struct with the given members.
(struct <{t1, t2, t3...}>) struct {a, b, c...}	!{!"struct", !{!"typeof", <{t1, t2, t3...}> zeroinitializer}, a, b, c...}	Returns a literal packed struct with the given members.
(vector) {a, b, c...}	<n x t> <a, b, c...>	Creates a "n"-sized vector of type "t".
(vector) {a, b, c...}	!{!"vector", a, b, c...}	Creates a "n"-sized vector of type "t".
(set) {a, b, c...}	!{!"set", !{!"typeof", a}, a, b, c...}	Creates a new set. All elements are of the same type.
a in b	!{!"in", b, a}	"a" must be an element of set "b". Returns a boolean, true if the element is in the set.
a in b	!{!"subset", a, b}	"a" and "b" must be sets. Returns a boolean, true if "a" is a subset of "b".
a..b	!{!"range", a, b}	"a" and "b" must be logical integers. Returns a set with elements >= a and < b.
a offset b	!{!"offset", a, b}	Does basic pointer arithmetic. "a" is a pointer (or set of pointers). "b" is a logic int (or set of logic ints). Returns "a" offset by "b" bits.
old a	!{!"old", a}	Evaluates "a" in a state at the beginning of the function. Has no effect in requires clauses.
fresh before a	!{!"fresh.before", a}	"a" must be a pointer. Returns whether or not "a" was allocated before the current state.
fresh after a	!{!"fresh.after", a}	"a" must be a pointer. Returns whether or not "a" was allocated after the current state.