Add distinction between shared and exclusive global variables (#560)

* Start working on this * Clean-up * Adapt old tests * Better comment * Fix tests * Fix all tests * Add test case * Add test cases * Fix test * Fix test * Fix tests * Fix bug with arrays * feedback from Felix * Undo error in test
viperproject · Nov 3, 2022 · f565a0c · f565a0c
1 parent fda2c1f
commit f565a0c
Show file tree

Hide file tree

Showing 20 changed files with 158 additions and 54 deletions.
diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala
@@ -434,7 +434,8 @@ object Desugar {
       val gvars = decl.left.map(info.regular) map {
         case g: st.GlobalVariable => globalVarD(g)(src)
         case w: st.Wildcard =>
-          val typ = typeD(info.typ(w.decl), Addressability.globalVariable)(src)
+          // wildcards are considered exclusive as they cannot be referenced anywhere else
+          val typ = typeD(info.typ(w.decl), Addressability.wildcard)(src)
           val scope = info.codeRoot(decl).asInstanceOf[PPackage]
           freshGlobalVar(typ, scope, w.context)(src)
         case e => Violation.violation(s"Expected a global variable or wildcard, but instead got $e")
@@ -443,7 +444,12 @@ object Desugar {
       if (decl.right.isEmpty) {
         // assign to all variables its default value:
         val assignsToDefault =
-          gvars.map{ v => singleAss(in.Assignee.Var(v), in.DfltVal(v.typ.withAddressability(Addressability.Exclusive))(src))(src) }
+          gvars.map{
+            case v if v.typ.addressability.isShared =>
+              singleAss(in.Assignee.Var(v), in.DfltVal(v.typ.withAddressability(Addressability.Exclusive))(src))(src)
+            case v =>
+              in.Assume(in.ExprAssertion(in.GhostEqCmp(v, in.DfltVal(v.typ)(src))(src))(src))(src)
+          }
         in.GlobalVarDecl(gvars, assignsToDefault)(src)
       } else if (decl.right.length == 1 && decl.right.length != decl.left.length) {
         // multi-assign mode:
@@ -452,20 +458,29 @@ object Desugar {
           case t: in.Tuple if t.args.length == gvars.length =>
             in.Block(
               decls = Vector(),
-              stmts = gvars.zip(t.args).map{ case (l, r) => singleAss(in.Assignee.Var(l), r)(src) }
+              stmts = gvars.zip(t.args).map{
+                case (l, r) if l.typ.addressability.isShared => singleAss(in.Assignee.Var(l), r)(src)
+                case (l, r) => in.Assume(in.ExprAssertion(in.GhostEqCmp(l,r)(src))(src))(src)
+              }
             )(src)
           case c => violation(s"Expected this case to be unreachable, but found $c instead.")
         })
         in.GlobalVarDecl(gvars, Vector(assigns))(src)
       } else {
         // single-assign mode:
-        val assigns = gvars.zip(exps).map{ case (l, wr) => block(for { r <- wr } yield singleAss(in.Assignee.Var(l), r)(src)) }
+        val assigns = gvars.zip(exps).map{
+          case (l, wr) if l.typ.addressability.isShared =>
+            block(for { r <- wr } yield singleAss(in.Assignee.Var(l), r)(src))
+          case (l, wr) =>
+            block(for { r <- wr } yield in.Assume(in.ExprAssertion(in.GhostEqCmp(l,r)(src))(src))(src))
+        }
         in.GlobalVarDecl(gvars, assigns)(src)
       }
     }
 
     def globalVarD(v: st.GlobalVariable)(src: Meta): in.GlobalVar = {
-      val typ = typeD(v.context.typ(v.id), Addressability.globalVariable)(src)
+      val addr = if (v.addressable) Addressability.Shared else Addressability.Exclusive
+      val typ = typeD(v.context.typ(v.id), addr)(src)
       val proxy = globalVarProxyD(v)
       in.GlobalVar(proxy, typ)(src)
     }
@@ -3468,9 +3483,13 @@ object Desugar {
             postprocessing = Vector(),
             seqn = in.MethodBodySeqn{
               // init all global variables declared in the file (not all declarations in the package!)
-              val initDeclaredGlobs: Vector[in.Initialization] = sortedGlobVarDecls.flatMap(_.left.map(gVar =>
+              val initDeclaredGlobs: Vector[in.Initialization] = sortedGlobVarDecls.flatMap(_.left).filter {
+                // do not initialize Exclusive variables to avoid unsoundnesses with the assumptions.
+                // TODO(another optimization) do not generate initialization code for variables with RHS.
+                _.typ.addressability.isShared
+              }.map{ gVar =>
                 in.Initialization(gVar)(gVar.info)
-              ))
+              }
               // execute the declaration statements for variables in order of declaration, while satisfying the
               // dependency relation
               /**
@@ -3695,7 +3714,6 @@ object Desugar {
     }
 
     def freshGlobalVar(typ: in.Type, scope: PPackage, ctx: ExternalTypeInfo)(info: Source.Parser.Info): in.GlobalVar = {
-      require(typ.addressability == Addressability.globalVariable)
       val name = nm.fresh(scope, ctx)
       val uniqName = nm.global(name, ctx)
       val proxy = in.GlobalVarProxy(name, uniqName)(meta(scope, ctx.getTypeInfo))

diff --git a/src/main/scala/viper/gobra/frontend/info/base/SymbolTable.scala b/src/main/scala/viper/gobra/frontend/info/base/SymbolTable.scala
@@ -110,13 +110,13 @@ object SymbolTable extends Environments[Entity] {
                             expOpt: Option[PExpression],
                             typOpt: Option[PType],
                             ghost: Boolean,
+                            override val addressable: Boolean,
                             isSingleModeDecl: Boolean,
                             context: ExternalTypeInfo
                            ) extends ActualVariable {
     require(expOpt.isDefined || typOpt.isDefined)
     require(0 <= idx && idx < decl.left.length)
     override def rep: PNode = decl
-    override def addressable: Boolean = true
     def id: PDefLikeId = decl.left(idx)
   }
 

diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/Addressability.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/Addressability.scala
@@ -73,7 +73,7 @@ trait Addressability extends BaseProperty { this: TypeInfoImpl =>
         case Some(_: ap.ReceivedMethod | _: ap.MethodExpr | _: ap.ReceivedPredicate | _: ap.PredicateExpr ) => AddrMod.rValue
         case Some(_: ap.NamedType | _: ap.BuiltInType | _: ap.Function | _: ap.Predicate | _: ap.DomainFunction) => AddrMod.rValue
         case Some(_: ap.ImplicitlyReceivedInterfaceMethod | _: ap.ImplicitlyReceivedInterfacePredicate) => AddrMod.rValue
-        case Some(_: ap.GlobalVariable) => AddrMod.globalVariable
+        case Some(g: ap.GlobalVariable) => if (g.symb.addressable) AddrMod.Shared else AddrMod.Exclusive
         case p => Violation.violation(s"Unexpected dot resolve, got $p")
       }
       case _: PLiteral => AddrMod.literal
@@ -126,7 +126,7 @@ trait Addressability extends BaseProperty { this: TypeInfoImpl =>
 
   private lazy val addressableVarAttr: PIdnNode => AddrMod =
     attr[PIdnNode, AddrMod] { n => regular(n) match {
-      case _: GlobalVariable => AddrMod.globalVariable
+      case g: GlobalVariable => if (g.addressable) AddrMod.sharedVariable else AddrMod.exclusiveVariable
       case v: Variable => if (v.addressable) AddrMod.sharedVariable else AddrMod.exclusiveVariable
       case _: Constant => AddrMod.constant
       case _: Wildcard => AddrMod.defaultValue

diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala
@@ -7,6 +7,7 @@
 package viper.gobra.frontend.info.implementation.property
 
 import viper.gobra.ast.frontend._
+import viper.gobra.ast.frontend.{AstPattern => ap}
 import viper.gobra.frontend.info.base.Type._
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.util.TypeBounds.BoundedIntegerKind
@@ -107,6 +108,7 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl =>
   }
 
   lazy val assignable: Property[PExpression] = createBinaryProperty("assignable") {
+    case e if !isMutable(e) => false
     case PIndexedExp(b, _) => underlyingType(exprType(b)) match {
       case _: ArrayT => assignable(b)
       case _: SliceT | _: GhostSliceT => assignable(b)
@@ -302,4 +304,13 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl =>
       case (_, i) => BigInt(i)
     }
   }
+
+  private def isMutable: Property[PExpression] = createBinaryProperty("mutable") { e =>
+    resolve(e) match {
+      case Some(g: ap.GlobalVariable) => g.symb.addressable
+      case Some(i: ap.IndexedExp) => isMutable(i.base)
+      case Some(f: ap.FieldSelection) => isMutable(f.base)
+      case _ => true
+    }
+  }
 }
diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala
@@ -47,9 +47,9 @@ trait NameResolution {
           case decl: PVarDecl if isGlobalVarDeclaration(decl) =>
             val idx = decl.left.zipWithIndex.find(_._1 == id).get._2
             StrictAssignMode(decl.left.size, decl.right.size) match {
-              case AssignMode.Single => GlobalVariable(decl, idx, Some(decl.right(idx)), decl.typ, isGhost, isSingleModeDecl = true, this)
-              case AssignMode.Multi  => GlobalVariable(decl, idx, decl.right.headOption, decl.typ, isGhost, isSingleModeDecl = false,  this)
-              case _ if decl.right.isEmpty => GlobalVariable(decl, idx, None, decl.typ, isGhost, isSingleModeDecl = true, this)
+              case AssignMode.Single => GlobalVariable(decl, idx, Some(decl.right(idx)), decl.typ, isGhost, decl.addressable(idx), isSingleModeDecl = true,  this)
+              case AssignMode.Multi  => GlobalVariable(decl, idx, decl.right.headOption, decl.typ, isGhost, decl.addressable(idx), isSingleModeDecl = false, this)
+              case _ if decl.right.isEmpty => GlobalVariable(decl, idx, None, decl.typ, isGhost, decl.addressable(idx), isSingleModeDecl = true, this)
               case _ => UnknownEntity()
             }
           case decl: PVarDecl =>

diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala
@@ -72,12 +72,12 @@ trait IdTyping extends BaseTyping { this: TypeInfoImpl =>
       })
     })
 
-    case GlobalVariable(_, _, expOpt, typOpt, _, isSingleModeDecl, _) if isSingleModeDecl => unsafeMessage(! {
+    case GlobalVariable(_, _, expOpt, typOpt, _, _, isSingleModeDecl, _) if isSingleModeDecl => unsafeMessage(! {
       typOpt.exists(wellDefAndType.valid) ||
         expOpt.exists(e => wellDefAndExpr.valid(e) && Single.unapply(exprType(e)).nonEmpty)
     })
 
-    case GlobalVariable(_, idx, expOpt, _, _, _, _) =>
+    case GlobalVariable(_, idx, expOpt, _, _, _, _, _) =>
       // in this case, mv must occur in a declaration in AssignMode.Multi
       unsafeMessage(! {
         expOpt.forall{ exp => wellDefAndExpr.valid(exp) &&
@@ -185,13 +185,13 @@ trait IdTyping extends BaseTyping { this: TypeInfoImpl =>
       case t => violation(s"expected tuple but got $t")
     }
 
-    case GlobalVariable(_, _, expOpt, typOpt, _, isSingleModeDecl, context) if isSingleModeDecl => typOpt.map(context.symbType)
+    case GlobalVariable(_, _, expOpt, typOpt, _, _, isSingleModeDecl, context) if isSingleModeDecl => typOpt.map(context.symbType)
       .getOrElse(context.typ(expOpt.get) match {
         case Single(t) => t
         case t => violation(s"expected single Type but got $t")
       })
 
-    case GlobalVariable(_, idx, expOpt, typOpt, _, _, context) => typOpt.map(context.symbType)
+    case GlobalVariable(_, idx, expOpt, typOpt, _, _, _, context) => typOpt.map(context.symbType)
       // in this case, mv must occur in a declaration in AssignMode.Multi
       .getOrElse(context.typ(expOpt.get) match {
         case Assign(InternalTupleT(ts)) if idx < ts.size => ts(idx)

diff --git a/src/main/scala/viper/gobra/theory/Addressability.scala b/src/main/scala/viper/gobra/theory/Addressability.scala
@@ -93,7 +93,7 @@ object Addressability {
 
   val boundVariable: Addressability = rValue
   val constant: Addressability = rValue
-  val globalVariable: Addressability = sharedVariable
+  val wildcard: Addressability = rValue
 
   val dereference: Addressability = pointerBase
   def fieldLookup(receiver: Addressability): Addressability = field(receiver)

diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
@@ -195,12 +195,20 @@ trait TypeEncoding extends Generator {
     * To avoid conflicts with other encodings, an encoding for type T should be defined at:
     * (1) exclusive operations on T, which includes literals and default values
     * (2) shared expression of type T
-    * The default implements exclusive variables and constants with [[variable]] and [[globalVar]], respectively.
-    * Furthermore, the default implements [T(e: T)] -> [e]
+    * The default implements exclusive local variables and constants with [[variable]] and [[Fixpoint::get]], respectively.
+    * Furthermore, the default implements global exclusive variables and conversions as [T(e: T)] -> [e].
     */
   def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = {
     case v: in.GlobalConst if typ(ctx) isDefinedAt v.typ => unit(ctx.fixpoint.get(v)(ctx))
     case (v: in.BodyVar) :: t / Exclusive if typ(ctx).isDefinedAt(t) => unit(variable(ctx)(v).localVar)
+    case (v: in.GlobalVar) :: t / Exclusive if typ(ctx).isDefinedAt(t) =>
+      val (pos, info, errT) = v.vprMeta
+      val typ = ctx.typ(v.typ)
+      val vprExpr = vpr.FuncApp(
+        funcname = v.name.uniqueName,
+        args = Seq.empty
+      )(pos, info, typ, errT)
+      unit(vprExpr)
     case in.Conversion(t2, expr :: t) if typ(ctx).isDefinedAt(t) && typ(ctx).isDefinedAt(t2) => ctx.expression(expr)
   }
 

diff --git a/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultGlobalVarEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultGlobalVarEncoding.scala
@@ -8,12 +8,10 @@ package viper.gobra.translator.encodings.defaults
 
 import org.bitbucket.inkytonik.kiama.==>
 import viper.gobra.ast.{internal => in}
-import viper.gobra.theory.Addressability
 import viper.gobra.translator.context.Context
 import viper.gobra.translator.encodings.combinators.Encoding
 import viper.gobra.translator.util.ViperWriter.MemberLevel.unit
 import viper.gobra.translator.util.ViperWriter.MemberWriter
-import viper.gobra.util.Violation
 import viper.silver.{ast => vpr}
 import viper.silver.plugin.standard.termination
 
@@ -28,13 +26,12 @@ class DefaultGlobalVarEncoding extends Encoding {
       * global variable declarations are encoded as pure functions that return a pointer
       * to the variable.
       *   [ var x T = exp ] ->
-      *     function x(): [ T@ ]
+      *     function x(): [ T ]
       */
     val termMeasure = synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate")
     unit(
       decl.left map { l =>
         val (pos, info, errTrafo) = l.vprMeta
-        Violation.violation(l.typ.addressability == Addressability.Shared, "Expected type with Shared addressability")
         val typ = ctx.typ(l.typ)
         vpr.Function(
           name = l.name.uniqueName,

diff --git a/src/test/resources/regressions/features/globals/globals-disabled-fail01.gobra b/src/test/resources/regressions/features/globals/globals-disabled-fail01.gobra
@@ -25,13 +25,13 @@ import (
 
 
 //:: ExpectedOutput(type_error)
-var A int = 0
+var A@ int = 0
 //:: ExpectedOutput(type_error)
-var B, C = f()
+var B@, C@ = f()
 //:: ExpectedOutput(type_error)
 var _ = g()
 //:: ExpectedOutput(type_error)
-var D struct{}
+var D@ struct{}
 
 decreases
 func f() (int, bool)

diff --git a/src/test/resources/regressions/features/globals/globals-exclusive-simple01.gobra b/src/test/resources/regressions/features/globals/globals-exclusive-simple01.gobra
@@ -0,0 +1,19 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package test
+
+var f@ int = 1
+var g int = test()
+
+func init() {
+	assert g == 1
+	//:: ExpectedOutput(assert_error)
+	assert false
+}
+
+ensures res == 1
+decreases
+func test() (res int) {
+	return 1
+}
diff --git a/src/test/resources/regressions/features/globals/globals-exclusive-type-fail01.gobra b/src/test/resources/regressions/features/globals/globals-exclusive-type-fail01.gobra
@@ -0,0 +1,29 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package pkg
+
+var A int = 0
+var B [3]int
+
+func test1() {
+	// A cannot be assigned to, it is exclusive.
+	//:: ExpectedOutput(type_error)
+	A = 1
+}
+
+func test2() {
+	// Cannot take the address of an exclusive global variable.
+	//:: ExpectedOutput(type_error)
+	assert acc(&A)
+}
+
+func test3() {
+	//:: ExpectedOutput(type_error)
+	assert acc(&B[0])
+}
+
+func test4() {
+	//:: ExpectedOutput(type_error)
+	B[0] = 1
+}
diff --git a/src/test/resources/regressions/features/globals/globals-fail01.gobra b/src/test/resources/regressions/features/globals/globals-fail01.gobra
@@ -5,10 +5,10 @@ package pkg
 
 import "fmt"
 
-var A = 1
+var A@ = 1
 // Code executed during initialization must terminate
 //:: ExpectedOutput(function_termination_error)
-var _, B = f()
+var _, B@ = f()
 
 func f() (int, bool)
 

diff --git a/src/test/resources/regressions/features/globals/globals-simple01.gobra b/src/test/resources/regressions/features/globals/globals-simple01.gobra
@@ -15,10 +15,10 @@ import (
 	"sync"
 )
 
-var A int = 0
-var B, C = f()
+var A@ int = 0
+var B@, C@ = f()
 var _ = g()
-var D struct{}
+var D@ struct{}
 
 decreases
 func f() (int, bool)

diff --git a/src/test/resources/regressions/features/globals/globals-type-fail01.gobra b/src/test/resources/regressions/features/globals/globals-type-fail01.gobra
@@ -7,4 +7,26 @@ package pkg
 //:: ExpectedOutput(type_error)
 var B, C, _ = f()
 
-func f() (int, bool)
+func f() (int, bool)
+
+type T struct {
+	f int
+}
+
+var x *T = &T{}
+
+// This is currently more restrictive than it needs to be but we
+// expect to support this in the future.
+func test1() {
+	// Rejected because x is not mutable, even though it does not need to be
+	// in this case.
+	//:: ExpectedOutput(type_error)
+	x.f = 2
+}
+
+var y T = T{}
+
+func test2() {
+	//:: ExpectedOutput(type_error)
+	y.f = 2
+}