Why3 Output Format

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

This page details the public interface that WhyR generates in its Why3 output.

LLVM Integers

The model used in for LLVM integers in WhyR is interchangeable. However, the theories used for the model must have the following public interface, split up into the following theories:

• IT
• type it
• constant size : int
• constant max_int : int
• constant two_power_size : int
• constant undef : it
• function to_uint it :int
• function to_int it :int
• function of_int int :it
• function add it it :it
  • Same for sub, mul, sdiv, srem, udiv, urem; as corresponding to LLVM instructions
• predicate ule it it
  • Same for sle, ugt, etc.; as corresponding to LLVM icmp instructions
• function bw_and it it :it
  • same for bw_or and bw_xor
• function bw_not it :it
• function lsl it int :it
  • Same for lsr and asr

LLVM Floats

The model used in for LLVM floatsin WhyR is interchangeable. However, the theories used for the model must have the following public interface, split up into the following theories:

• Float
• type float
• constant size : int
• constant min : real
• constant max : real
• constant max_representable_integer : int
• function to_real Rounding.mode float :real
• function of_real Rounding.mode real :float
• predicate is_finite float
• predicate is_infinite float
• predicate is_NaN float
• function fadd Rounding.mode float float :float
  • Same for fsub, fmul, fdiv, frem; as corresponding to LLVM instructions
• predicate oeq float float
  • Same for ogt, ord, ugt, etc.; as corresponding to LLVM fcmp instructions

For LLVM's double type, replace Float with Double and float with double.

LLVM Arrays

The theories used for the model for LLVM arrays must have the following public interface, split up into the following theories:

• ArrayT_n
• type at_n
• constant elem_num : int
• constant size : int
• constant elem_size : int
• function ([]) at_n int :t
• function ([=]) atn int t :atn

LLVM Pointers and the Memory Model

The memory model used in WhyR is interchangeable. However, the theories used for the model must have the following public interface, split up into the following theories:

• State
• type state
• constant blank_state : state
• TP
• type tp
• constant null: tp
• constant elem_size : int
• constant size : int
• function load state tp :t
• function store state tp t :state
• function offset_pointer tp int :tp
• function to_ptrint tp :i64
• function of_ptrint i64 :tp
• Pointer
• predicate separated ap int bp int
• function cast ap :bp
• predicate valid_read state ap int
• predicate valid_write state ap int
• Alloc
• function alloc state int :(state, tp)
• predicate allocated_before state tp
• predicate allocated_after state tp
• MemorySet
• type mem_set t
• constant empty : mem_set t
• function add tp (mem_set t) :(mem_set t)
• predicate mem tp (mem_set t)
• function havoc state (mem_set t) :state
• function offset_memset (mem_set t) (set int) :(mem_set t)

'default' Memory Model

This memory model is current the default model for WhyR.

A state is a collection of blocks of memory, called mem_spaces, each separate from one another. It is keyed by base_ids, which are integers.

a pointer 'a has a base and an offset. Only pointers from the same base can be non-separated.

loading from a pointer calls load_mem, which knows what was last stored in it at the specified offset. A store will call store_mem, which will update the area, returning a new state.

alloc lets you allocate new blocks of memory. It returns a pointer to offset 0 of a new block, and also the new state. Base IDs increment after a call to alloc, so two allocated blocks are never returned as the same.

'dummy' Memory Model

This memory model only declares the function required above; it defines nothing.

LLVM Vectors

The theories used for the model for LLVM vectors must have the following public interface, split up into the following theories:

• VectorT_n
• type vt_n
• constant elem_num : int
• constant size : int
• constant elem_size : int
• function ([]) at_n int :t
• function ([=]) atn int t :atn

In addition, the theory VectorT_n has different interface depending on the vector's element type.

• Integer
• add, sub, etc. like the version for LLVM floats, but vectors.
• lsl, lsr, etc. like the version for LLVM floats, but vectors.
• Floating
• fadd, fsub, etc. like the version for LLVM floats, but vectors.
• Pointer
• None (yet).

Functions

All functions must have the following public interface:

• constant entry_state : state
• constant exit_state : state
• constant ret_val : result
• The tpye is the function's return type. Only include if the function returns something.
• predicate execute
• predicate function_requires
• predicate function_ensures