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]

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 8facab51220570ff88f72e71e794bcb336208e47, 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

[ArquintL]

HyperMode extended now uses the SIF plugin. For consistency reasons, it would make sense to move SIFLowGuardTransformer.scala to the plugin such that we do not need to conditionally run Viper plugins based on which HyperMode is selected

[ArquintL]

Does anyone have a clue why the CI does not run check-license-headers and build-test-deploy-container (PR) for this PR?

[jcp19]

I suggest that, from now on, we implement changes to this branch by separate PRs (except to merge with master).

[jcp19]

I suggest that, after #904 is merged and we merge https://github.com/viperproject/silver-sif-extension/pull/3/files, we both review this PR to make sure we are reasonably happy and then merge this.

[jcp19]

This is now failing to build because the sif extension uses different versions of silver/silicon/carbon -.- I will repair this later

[jcp19]

So, I finally updated the submodules. I found the culprit of the failure to be https://github.com/viperproject/silicon/pull/927, and this was fixed in https://github.com/viperproject/silicon/pull/937. Thus, we can now stick to the master branch of the silver-sif-extension. When the CI goes through, we should merge this.

[ArquintL]

The CI is currently failing due to commitment-extended.go and termination-extended-simple01.gobra that crash the SIF translation (due to my "fixes"). While I do have locally a fix, I'm hitting an issue that goto statements are by default unsupported by the SIF plugin, which requires enabling enableExperimentalFeatures

[ArquintL]

This PR is currently blocked by https://github.com/viperproject/silver-sif-extension/pull/9 and https://github.com/viperproject/silver-sif-extension/pull/10

[ArquintL]

Note that this branch currently uses the arquintl-goto-encoding instead of master branch of silver-sif-extension. We could either wait until https://github.com/viperproject/silver-sif-extension/pull/10 is merged or merge now and wait until the silver-sif-extension submodule is updated automatically by update-submodules.yml

[jcp19]

aren't we close to merging https://github.com/viperproject/silver-sif-extension/pull/10 too? From a quick look, it seems that this is also in the final phase of the review, and thus, I would be happy to wait until that is merged.

[jcp19]

LGTM