fix issues with 'contains' in maps and with trigger generation

viperproject · Sep 21, 2023 · 5cd4b21 · 5cd4b21
1 parent 93798d6
commit 5cd4b21
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 17 deletions.
diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala
@@ -47,6 +47,12 @@ class FinalTypeEncoding(te: TypeEncoding) extends TypeEncoding {
   override def goEqual(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = te.goEqual(ctx) orElse expectedMatch("equal")
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = te.expression(ctx) orElse expectedMatch("expression")
   override def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = te.triggerExpr(ctx) orElse {
+    // use predicate access encoding but then take just the predicate access, i.e. remove `acc` and the permission amount:
+    case in.Accessible.Predicate(op) =>
+      for {
+        v <- ctx.assertion(in.Access(in.Accessible.Predicate(op), in.FullPerm(op.info))(op.info))
+        pap = v.asInstanceOf[vpr.PredicateAccessPredicate]
+      } yield pap.loc
     case e: in.Expr => te.expression(ctx)(e)
   }
   override def assertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = te.assertion(ctx) orElse expectedMatch("assertion")

diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
@@ -234,18 +234,7 @@ trait TypeEncoding extends Generator {
   }
 
   // TODO: doc
-  // TODO: optimize assert2(true, ...)
-  // TODO: key in map, instead of key in domain(map)
-  // TODO: enable consistency checks on triggers when --checkConsistency
-  def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = {
-    // use predicate access encoding but then take just the predicate access, i.e. remove `acc` and the permission amount:
-    case in.Accessible.Predicate(op) =>
-      for {
-        v <- ctx.assertion(in.Access(in.Accessible.Predicate(op), in.FullPerm(op.info))(op.info))
-        pap = v.asInstanceOf[vpr.PredicateAccessPredicate]
-      } yield pap.loc
-    // case e: in.Expr => ctx.expression(e)
-  }
+  def triggerExpr(@unused ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = PartialFunction.empty
 
   /**
     * Encodes assertions.

diff --git a/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala
@@ -24,9 +24,6 @@ import viper.silver.verifier.reasons.AssertionFalse
 import viper.silver.verifier.{ErrorReason, errors => err}
 import viper.silver.{ast => vpr}
 
-// TODO: use macros to make the generated code readable?
-// TODO: remove call to assert2 when the condition is the true lit
-
 /**
   * Encoding for Go maps. Unlike slices, maps are not thread-safe;
   * thus, all concurrent accesses to maps must be synchronized. In particular,
@@ -91,10 +88,16 @@ class MapEncoding extends LeafTypeEncoding {
 
       case l@in.Contains(key, exp :: ctx.Map(keys, values)) =>
         for {
+          mapVpr <- goE(exp)
           keyVpr <- goE(key)
           isComp <- MapEncoding.checkKeyComparability(key)(ctx)
           correspondingMap <- getCorrespondingMap(exp, keys, values)(ctx)
-          containsExp = withSrc(vpr.MapContains(keyVpr, correspondingMap), l)
+          containsExp =
+            withSrc(vpr.CondExp(
+              withSrc(vpr.EqCmp(mapVpr, withSrc(vpr.NullLit(), l)), l),
+              withSrc(vpr.FalseLit(), l),
+              withSrc(vpr.MapContains(keyVpr, correspondingMap), l)
+            ), l)
           checkCompAndContains <- assert(isComp, containsExp, comparabilityErrorT)(ctx)
         } yield checkCompAndContains
 
@@ -124,6 +127,7 @@ class MapEncoding extends LeafTypeEncoding {
     }
   }
 
+  // TODO: doc
   override def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = {
     default(super.triggerExpr(ctx)) {
       case l@in.IndexedExp(m :: ctx.Map(keys, values), idx, _) =>
@@ -137,7 +141,7 @@ class MapEncoding extends LeafTypeEncoding {
         for {
           vKey <- ctx.expression(key)
           correspondingMap <- getCorrespondingMap(m, keys, values)(ctx)
-          contains = withSrc(vpr.MapContains(correspondingMap, vKey), l)
+          contains = withSrc(vpr.MapContains(vKey, correspondingMap), l)
         } yield contains
 
       case l@in.Contains(key, in.MapKeys(m :: ctx.Map(keys, values), _)) =>

diff --git a/src/test/resources/regressions/features/maps/maps-simple1.gobra b/src/test/resources/regressions/features/maps/maps-simple1.gobra
@@ -145,3 +145,11 @@ func test16() {
 requires m != nil ==> acc(m)
 requires forall s string :: { s in domain(m) } s in domain(m) ==> acc(m[s])
 func test17(m map[string]*int) {}
+
+requires m != nil ==> acc(m)
+requires forall s string :: { s in m } s in m ==> acc(m[s])
+func test18(m map[string]*int) {}
+
+requires m != nil ==> acc(m)
+requires forall i int :: { i in range(m) } i in range(m) ==> 0 < i
+func test19(m map[string]int) {}