extends CLI to support more complete SIF encoding supporting non-low …

…control flow

src/main/scala/viper/gobra/frontend/Config.scala

@@ -92,6 +92,8 @@ object MCE {
 
 object Hyper {
   sealed trait Mode
+  /** uses more complete encoding that does not enforce low guards for control flow */
+  object EnabledExtended extends Mode
   object Enabled extends Mode
   object Disabled extends Mode
   object NoMajor extends Mode
@@ -255,6 +257,8 @@ case class Config(
     } else {
       TypeBounds(Int = TypeBounds.IntWith64Bit, UInt = TypeBounds.UIntWith64Bit)
     }
+
+  val hyperModeOrDefault: Hyper.Mode = hyperMode.getOrElse(ConfigDefaults.DefaultHyperMode)
 }
 
 object Config {
@@ -794,12 +798,13 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
 
   val hyperMode: ScallopOption[Hyper.Mode] = choice(
     name = "hyperMode",
-    choices = Seq("on", "off", "noMajor"),
-    descr = "Specifies whether hyper properties should be verified (on), not verified (off), or whether the major checks should be skipped (noMajor).",
+    choices = Seq("on", "extended", "off", "noMajor"),
+    descr = "Specifies whether hyper properties should be verified while enforcing low control flow (on), with support for non-low control flow (extended), not verified (off), or whether the major checks should be skipped (noMajor).",
     default = None,
     noshort = true
   ).map {
     case "on" => Hyper.Enabled
+    case "extended" => Hyper.EnabledExtended
     case "off" => Hyper.Disabled
     case "noMajor" => Hyper.NoMajor
   }

src/main/scala/viper/gobra/translator/Translator.scala

@@ -9,11 +9,11 @@ package viper.gobra.translator
 
 import viper.gobra.ast.internal.Program
 import viper.gobra.backend.BackendVerifier
-import viper.gobra.frontend.{Config, PackageInfo}
+import viper.gobra.frontend.{Config, Hyper, PackageInfo}
 import viper.gobra.reporting.{ConsistencyError, GeneratedViperMessage, TransformerFailureMessage, VerifierError}
 import viper.gobra.translator.context.DfltTranslatorConfig
 import viper.gobra.translator.encodings.programs.ProgramsImpl
-import viper.gobra.translator.transformers.hyper.SIFLowGuardTransformerImpl
+import viper.gobra.translator.transformers.hyper.{SIFLowGuardTransformerImpl, SIFTransformer}
 import viper.gobra.translator.transformers.{AssumeTransformer, TerminationTransformer, ViperTransformer}
 import viper.gobra.util.Violation
 import viper.silver.ast.{AbstractSourcePosition, SourcePosition}
@@ -37,10 +37,13 @@ object Translator {
     val programTranslator = new ProgramsImpl()
     val task = programTranslator.translate(program)(translationConfig)
 
+    val sifTransformer =
+      if (config.hyperModeOrDefault == Hyper.EnabledExtended) new SIFTransformer
+      else new SIFLowGuardTransformerImpl(config)
     val transformers: Seq[ViperTransformer] = Seq(
       new AssumeTransformer,
       new TerminationTransformer,
-      new SIFLowGuardTransformerImpl(config),
+      sifTransformer,
     )
 
     val transformedTask = transformers.foldLeft[Either[Vector[VerifierError], BackendVerifier.Task]](Right(task)) {

src/test/resources/regressions/features/hyper_properties/commitment-extended.go

@@ -0,0 +1,40 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// ##(--hyperMode extended)
+
+package commitment
+
+// @ requires low(hash)
+// @ ensures  res ==> low(value)
+func verify(hash int, value int) (res bool) {
+    res = (hash == computeHash(value))
+    return
+}
+
+// @ requires low(hash)
+// @ ensures  res ==> low(value)
+func verifyWithBranching(hash int, value int) (res bool) {
+    // the following if statement succeeds because we enabled the extended
+    // SIF encoding that allows branching on non-low conditions
+    if hash != computeHash(value) {
+        return false
+    }
+    return true
+}
+
+// the following postcondition specifies that the Go function `computeHash` behaves like the
+// pure (mathematical) function `hashFn` for which we assume injectivity (see domain below)
+// @ ensures res == hashFn(input)
+func computeHash(input int) (res int)
+
+/* @
+type HashFunction domain {
+    func hashFn(int) int
+    func invFn(int) int
+
+    axiom { // hashFn is injective
+        forall v int :: { hashFn(v) } invFn(hashFn(v)) == v
+    }
+}
+@ */

src/test/resources/regressions/features/hyper_properties/commitment.go

@@ -38,4 +38,4 @@ type HashFunction domain {
         forall v int :: { hashFn(v) } invFn(hashFn(v)) == v
     }
 }
-@ */
+@ */