The WhyR Type System

WhyR has an internal type system different than that of Why3. It currently has the following types:

• Logical integer
  • This represents an unbounded integernal type.
  • This corresponds to "Int.int" in Why3.
  • This is the type "int" in WAR.
  • Constants can be created with the sexpr "int", like so:

    !{!"int", !"1230"}

  • In WAR, constants are made as in C integers.
  • Note well: In most programming languages, signendness (whether signed or unsigned) is a property of the type; in LLVM, it is a property of the operator. Hence the existence of 'ugt' and 'sgt' instead of just '>' for LLVM integers, for instance!
  • This type's class is LogicTypeInt, and is defined in src/type_int.cpp .
• Logical real
  • This represents an unbounded real type.
  • This corresponds to "real.Real" in Why3. This is the type "real" in WAR.
  • Constants can be created with the sexpr "real", like so:

    !{!"real", !"12.3"}

  • In WAR, constants are made as in C floats.
  • This type's class is LogicTypeReal, and is defined in src/type_real.cpp .
• Logical boolean
  • This represents a boolean type.
  • This corresponds to "Bool.bool" in Why3.
  • This is the type "bool" in WAR.
  • Constants can be created with the sexprs "true" and "false", like so:

    !{!"true"}

  • In WAR, constants are made with the keywords "true" or "false".
  • This type's class is LogicTypeBool, and is defined in src/type_bool.cpp .
• Set
  • This represents a potentially-infinite set of an arbitrary type.
  • The corresponds to "Set.set" in Why3.
  • Sets of pointers have a special theory: "MemorySet". WhyR generates this theory.
  • This is the type "T set", where T is the set type.
  • Constants are created in metadata like so:

    !{!"set", !{!"typeof", i32 0}, i32 1, i32 2, i32 3}

  • Constants are created in WAR like so:

    (set) {1,2,3}

  • This type's class is LogicTypeSet, and is defined in src/type_set.cpp .
• LLVM integer
  • This represents a fixed-size bitvector representing an LLVM integer.
  • This corresponds to the Why3 type "In.in", where n is the size of the integer. WhyR generates this theory.
  • In WAR, this is of type "in".
  • Constants are encoded with LLVM constant directly in metadata, like so:

    i32 1230

  • In WAR, constants are made via casting logical integers:

    (i32)1230

  • This type's class is LogicTypeLLVM, and is defined in src/type_llvm.cpp .
  • Care must be made with casts involving LLVM ints. Truncation in WAR can be done using the casting syntax, but when extending LLVM ints to logical ints (or larger LLVM ints), you need to specify whether the result is sign or zero extended, by using the "sext" and "zext" keywords:

    (i32) (i64) 200
    (i64 zext) (i32) 200
    (int sext) (i64) 200

• LLVM floating
  • This represents a fixed-size floating-point number.
  • This corresponds to the Why3 types "Double.double", "Float.float", etc. WhyR generates this theory.
  • In WAR, this is of type "float", "double", etc.
  • Constants are encoded with LLVM constant directly in metadata, like so:

    double 12.3

  • In WAR, constants are made via casting logical reals:

    (float)12.3

  • This type's class is LogicTypeLLVM, and is defined in src/type_llvm.cpp .
• LLVM arrays
  • This represents a fixed-size array type.
  • This corresponds to the Why3 type "ArrayT_N.at_n", where N is the size and T is the element type. WhyR generates this theory.
  • In WAR, this is of type "t[n]". If n is left out, it will be assumed to be 0.
  • Constants are encoded with LLVM constants directly in metadata, like so:

    [ 4 x i32 ] [ i32 1, i32 2, i32 3, i32 4 ]

  • In WAR, constants are made via curly bracket notation:

    {(i32)1, (i32)2, (i32)3, (i32)4}

  • In WAR, 0-length arrays must be qualified with a type:

    (i32[]){}
    (i32[0]){}

  • This type's class is LogicTypeLLVM, and is defined in src/type_llvm.cpp .
• LLVM structs
  • This represents a structure type.
  • This corresponds to a theory called "Type_name" if the struct is named, and "Struct_types", where types is the list of member types, otherwise. WhyR generates this theory.
  • In WAR, this is of type "struct name" or "struct {a, b, c...}". Packed struct literals look like "struct <{a, b, c...}>".
  • Constants are encoded with LLVM constants directly in metadata, like so:

    {i32,i16,i8} {i32 1, i16 2, i8 3}

  • In WAR, constants are made via curly bracket notation:

    (struct {i32,i16,i8}) struct {(i32)1, (i16)2, (i8)3}

  • This type's class is LogicTypeLLVM, and is defined in src/type_llvm.cpp .
• Type constants
  • This represents another type. This doesn't directly correspond to anything in Why3 or WAR, but exists in the metadata.
  • Type constants can be generated with the sexpr "typeof":

    !{!"typeof", !{!"int", !"0"}}
    !{!"typeof", !{!"true"}}
    !{!"typeof", i32 4}

  • This is useful in quantifiers and lets, where types must be specified:

    !{!"let", !{!{!"x", !{!"typeof", i32 42}, i32 42}}, !{!"local", !"x"}}

  • This type's class is LogicTypeType, and is defined in src/type_type.cpp .
• LLVM vectors
  • This represents a vector type. Vector types are like arrays, but you can do arithmetic on them via SIMD instructions. As such, vectors can only have integer, floating, or pointer elements.
  • This corresponds to the Why3 type "VectorT_N.vt_n", where N is the size and T is the element type. WhyR generates this theory.
  • In WAR, this is of type "vector t[n]".
  • Constants are encoded with LLVM constants directly in metadata, like so:

    < 4 x i32 > < i32 1, i32 2, i32 3, i32 4 >

  • In WAR, constants are made via curly bracket notation with vector qualification:

    (vector) {(i32)1, (i32)2, (i32)3, (i32)4}

  • This type's class is LogicTypeLLVM, and is defined in src/type_llvm.cpp .