Hyper Gobra

[jcp19]

Felix's implementation of the technique for checking SIF based on this paper

TODO:

• move extension implementation to https://github.com/viperproject/silver-sif-extension/ to avoid duplicating code and add it as a submodule

[jcp19]

TODO: change

[ArquintL]

It would be nice if we could leave this turned on but ensure that if a program does not make use of any SIF specs that we do not perform the product construction.
If this is not easily possible, we have to think about the hyperMode options as "off" currently results in turning all SIF specs to true, which is potentially dangerous if you are not aware of this. Imho, the default mode should make sure that non-SIF programs are encoded as today (i.e., without product construction) and either handle SIF programs soundly or report an error. However, having a mode that allows you to turn SIF checks off for a SIF program could be useful for debugging but this requires a warning / error that this is potentially unsound

[jcp19]

TODO: drop

[jcp19]

@ArquintL I guess setting this to true should allow us to keep the default for SIF. I will change it once I start working on this pR

[ArquintL]

That's not sufficient. Instead of checking which methods have relational spec and which do not, a first attempt would be to decide this for the entire input program. To keep this on a per-method level, we would first need to address the problem mentioned in the comment above namely that a non-SIF method calling a SIF method (or vice-versa) fails as the number of parameters / arguments does not match.
A similar issue occurs if we would mix methods encoded with optimized SIF encoding (enforcing low control flow) and the more complete SIF encoding as the latter one uses additional parameters (namely the activation variables) and also uses a different ordering for the parameters belonging to the 2nd execution (which is just an implementation detail)

[jcp19]

The current version, together with the changes from #818 which have been merged in scion leads to an exception on this file:

package bugs

// Bug 5.
// Trying to verify this file yields the following error message:
// 
// 		Precondition of call test1(ub) might not hold.
// 		Permission to ub[0] might not suffice.
//
// The reason can be seen in the generated Viper file: The `_termination_proof`
// method for `test0` replaces the permission amount (`write`) with `wildcard`.
// Note: In order for this bug to occur, `test1` needs to return a struct
// (at least not some primitive type), and the functions must be `pure` (and
// thus also annotated with `decreases`).
//
// This problem first occurred while trying to verify `pkg\slayers\path\epic`.

type Struct struct {}

requires acc(&ub[0])
decreases
pure func test1(ub []byte) Struct {
    return Struct{}
}

requires acc(&ub[0])
decreases
pure func test0(ub []byte) bool {
    return Struct{} == test1(ub)
}

Reported by @henriman

[ArquintL]

Regression (just in case we are not aware of it yet): in contrast to 8facab5, termination measures are no longer transformed resulting in crashes of Silicon

[jcp19]

So, the bug related to termination measures has been fixed (gobra no longer immediately crashes with consistency errors for programs that perform termination checking). @henriman

There is currently a seemingly absurd bug where ADT members are not translated to the Viper program. I will debug this one next. After this one, I guess it is a matter of cleaning up the code (sorely needed), reviewing everything, and dropping all copied files from the SIF plugin for Viper

[jcp19]

I'm not sure if this is a good solution because every package that imports sync to use a Mutex will use the new spec for this function, which contains low annotations. Thus, this solution forces us to always enable SIF when verifying concurrent code

[ArquintL]

I've also realized this after looking at the failing testcases ^^
Maybe we should distinguish between imported and non-imported SIF expressions and ignore the former while cause errors for the latter (if SIF is disabled).
What I want to avoid is any confusion as in my program contains SIF expressions but I (e.g. by mistake) configured Gobra not to do a product construction and, thus, I'm thinking I've verified SIF but actually Gobra didn't