Regional verification settings

[pieter-bos]

For several aspects of verification, I think it is a good idea that we have multiple ways of encoding them. Typically we forbid situations that are bad by proving that they do not occur, such as division by zero, field access on null, etc. This is however a well-defined situation in at least Java. Although inadvisable, you may want to verify e.g. this program:

//@ ensures \result == 5;
static int test() {
    try {
        ((Object)null).toString();
    } catch(Throwable t) {
        return 5;
    }

    return -1;
}

VerCors will reject this program with invocationObjectNull.

We should thus be able to set the way in which invocations on null objects are treated: they should probably be banned by default, but we should be able to change it for this instance.

[pieter-bos]

A tentative list of verification conditions that have multiple encodings:

• invocationObjectNull: banned, and NullPointerException semantics
• arrayNull: banned, and NullPointerException semantics
• arraySize: banned, and NegativeArraySizeException semantics
• arrayBounds: banned, and ArrayIndexOutOfBoundsException semantics
• ? null field access ?: implicitly banned due to permissions, but could have NullPointerException semantics (how?)
• divByZero: banned, and ArithmeticException semantics

Perhaps in the future:

• Casting to wrong type: banned, and ClassCastException semantics
• ArrayStoreException if we make java arrays convariant in vercors
• int: can be TInt (unbounded), or bv32 (precise semantics), or a bounded integer axiomatization (ban overflow)
• float: can be TRational (unbounded, infinitely precise), or Float32 (precise semantics), or a rational range approach (ban under/overflow), or a rational range approach that allows NaN, infinity, etc.

[pieter-bos]

Side tangent for C:

• The integral types char, short, int, long, long long, al potentially signed or unsigned, in principle have variable width
• There are three common data models in use for this: ILP32, LP64 and LLP64 - I propose we restrict ourselves to those and only support choosing one data model per program or verification run. They mean respectively:
  • ints, longs and pointers are 32 bits
  • longs and pointers are 64 bits
  • only long longs and pointers are 64 bits
• It is important that e.g. stdint.h types match the selected option, so we should select -target to be (respectively) i386-, x86_64- and aarch64-unknown-unknown-unknown - this seems to match the data models. They are not affected by the os ("system": linux, windows etc.) as insinuated elsewhere, perhaps this refers to some constellation of defaults.
• It is important that e.g. stdint.h types match the selected option, so we should select appropriate values for -target. They should be an entirely defined target that uses the correct data model, as e.g. x86_64-windows-unknown != x86_64-unknown-unknown. I think these are correct:
  • ILP32 = i386-linux-unknown
  • LP64 = x86_64-linux-unknown
  • LLP64 = x86_64-windows-unknown
• I haven't tested yet whether e.g. nvcc likes these targets and will match the data model

[pieter-bos]

we are guaranteed to use clang, and clang will define __LP64__, __ILP32__ or _WIN64 as appropriate, so perhaps we can do something like:

#ifdef __LP64__
//@ \declare_data_model \lp64;
#elifdef __ILP32__
//@ \declare_data_model \ilp32;
#elifdef _WIN64
//@ \declare_data_model \llp64;
#else
#error :(
#endif

[pieter-bos]

Actually we use -nostdinc so we cannot just use the platform stdint.h