Merge branch 'master' into magic-wand-maps

src/main/scala/viper/silver/ast/utility/Simplifier.scala

@@ -116,10 +116,15 @@ object Simplifier {
         IntLit(left - right)(root.pos, root.info)
       case root @ Mul(IntLit(left), IntLit(right)) =>
         IntLit(left * right)(root.pos, root.info)
-      case root @ Div(IntLit(left), IntLit(right)) if right != bigIntZero =>
+      /* In the general case, Viper uses the SMT division and modulo. Scala's division is not in-sync with SMT division.
+         For nonnegative dividends and divisors, all used division and modulo definitions coincide. So, in order to not
+         not make any assumptions on the SMT division, division and modulo are simplified only if the dividend and divisor
+         are nonnegative. Also see Carbon PR #448.
+       */
+      case root @ Div(IntLit(left), IntLit(right)) if left >= bigIntZero && right > bigIntZero =>
         IntLit(left / right)(root.pos, root.info)
-      case root @ Mod(IntLit(left), IntLit(right)) if right != bigIntZero =>
-        IntLit((right.abs + (left % right)) % right.abs)(root.pos, root.info)
+      case root @ Mod(IntLit(left), IntLit(right)) if left >= bigIntZero && right > bigIntZero =>
+        IntLit(left % right)(root.pos, root.info)
 
       // statement simplifications
       case Seqn(EmptyStmt, _) => EmptyStmt // remove empty Seqn (including unnecessary scopedDecls)

src/main/scala/viper/silver/parser/MacroExpander.scala

@@ -481,6 +481,19 @@ object MacroExpander {
           freeVars += varUse.name
           (varUse, ctx)
         }
+      case (label@PLabel(lbl, lName, invs), ctx) if !ctx.c.boundVars.contains(lName.name) =>
+        if (ctx.c.paramToArgMap.contains(lName.name)) {
+          val replacement = ctx.c.paramToArgMap(lName.name).deepCopyAll
+          val replaced = replacement match {
+            case r: PIdnUseExp => PIdnDef(r.name)(r.pos)
+            case r =>
+              throw MacroException(s"macro expansion cannot substitute expression `${replacement.pretty}` at ${replacement.pos._1} in non-expression position at ${lName.pos._1}.", replacement.pos)
+          }
+          (PLabel(lbl, replaced, invs)(label.pos), ctx.updateContext(ctx.c.copy(paramToArgMap = ctx.c.paramToArgMap.empty)))
+        } else {
+          freeVars += lName.name
+          (label, ctx)
+        }
     }, ReplaceContext())
     (replacer, freeVars)
   }

src/test/resources/all/heap-dependent_triggers/triggerFoldPackage.vpr

@@ -12,7 +12,7 @@ method m1(xs: Set[Ref], y: Ref, zs: Seq[Ref]) {
     assume z in zs
     assume !(z in xs)
     package acc(z.f) --* acc(y.f)
-    //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/000/)
+
     //:: ExpectedOutput(assert.failed:assertion.false)
     assert z != y
 }

src/test/resources/all/issues/silicon/0832.vpr

@@ -0,0 +1,52 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+method test(x0: Array, x1:Array)
+  requires (forall j: Int :: {arrR(j, x0, 10)} 0 <= j && j < 10 ==> arrR(j, x0, 10))
+  requires arr(x1, 10)
+  requires (forall j: Int :: { aloc(x1, j) }
+    0 <= j && j < 10 ==> (unfolding acc(arr(x1, 10), write/2) in aloc(x1, j).int) == j)
+  requires (forall j: Int :: { aloc(x0, j) }
+    0 <= j && j < 10 ==> (unfolding arrR(j, x0, 10) in aloc(x0, j).int == 3 * j))
+{
+  assert (unfolding arrR(0, x0, 10) in
+            aloc(x0, 0).int == 3 * 0)
+}
+
+predicate arrR(x: Int, a: Array, n: Int) {
+  alen(a) == n && 0 <= x && x < n && acc(aloc(a, x).int, write)
+}
+
+predicate arr(a: Array, n: Int) {
+  alen(a) == n && (forall i: Int :: { aloc(a, i) } 0 <= i && i < alen(a) ==> acc(aloc(a, i).int, write))
+}
+
+field int: Int
+domain Array  {
+
+  function array_loc(a: Array, i: Int): Ref
+  function alen(a: Array): Int
+  function loc_inv_1(loc: Ref): Array
+  function loc_inv_2(loc: Ref): Int
+
+  axiom {
+    (forall a: Array, i: Int ::
+      { array_loc(a, i) }
+      loc_inv_1(array_loc(a, i)) == a && loc_inv_2(array_loc(a, i)) == i)
+  }
+
+  axiom {
+    (forall a: Array :: { alen(a) } alen(a) >= 0)
+  }
+}
+
+function aloc(a: Array, i: Int): Ref
+  requires 0 <= i
+  requires i < alen(a)
+  decreases
+  ensures loc_inv_1(result) == a
+  ensures loc_inv_2(result) == i
+{
+  array_loc(a, i)
+}

src/test/resources/all/issues/silicon/0833.vpr

@@ -0,0 +1,82 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+domain ShStruct2[T0, T1]  {
+
+  function ShStructget1of2(x: ShStruct2[T0, T1]): T1
+
+  function ShStructget0of2(x: ShStruct2[T0, T1]): T0
+
+  function ShStructrev1of2(v1: T1): ShStruct2[T0, T1]
+
+  function ShStructrev0of2(v0: T0): ShStruct2[T0, T1]
+
+  axiom {
+    (forall x: ShStruct2[T0, T1] ::
+      { (ShStructget1of2(x): T1) }
+      (ShStructrev1of2((ShStructget1of2(x): T1)): ShStruct2[T0, T1]) == x)
+  }
+
+  axiom {
+    (forall x: ShStruct2[T0, T1] ::
+      { (ShStructget0of2(x): T0) }
+      (ShStructrev0of2((ShStructget0of2(x): T0)): ShStruct2[T0, T1]) == x)
+  }
+}
+
+field Intint$$$$_E_$$$: Int
+
+// decreases
+function witness_4e2a3fe_F(P0_PI0: Int): ShStruct2[Ref, Ref]
+    ensures witness_rev(result) == P0_PI0
+
+function witness_rev(s: ShStruct2[Ref, Ref]): Int
+
+
+predicate SharedInv_4e2a3fe_F() {
+  (forall i_V0: Int ::
+    { (ShStructget0of2(witness_4e2a3fe_F(i_V0)): Ref) }
+    true && (let fn$$0 == (witness_4e2a3fe_F(i_V0)) in true) ==>
+    acc((ShStructget0of2(witness_4e2a3fe_F(i_V0)): Ref).Intint$$$$_E_$$$, 1 /
+    2)) &&
+  (forall i_V0: Int ::
+    { (ShStructget1of2(witness_4e2a3fe_F(i_V0)): Ref) }
+    true && (let fn$$0 == (witness_4e2a3fe_F(i_V0)) in true) ==>
+    acc((ShStructget1of2(witness_4e2a3fe_F(i_V0)): Ref).Intint$$$$_E_$$$, 1 /
+    2))
+}
+
+method processRequest_4e2a3fe_F(id_V0: Int)
+  requires (let fn$$0 ==
+      (witness_4e2a3fe_F(id_V0)) in
+      acc((ShStructget0of2(fn$$0): Ref).Intint$$$$_E_$$$, 1 / 2) &&
+      acc((ShStructget1of2(fn$$0): Ref).Intint$$$$_E_$$$, 1 / 2) &&
+       true
+      )
+  requires acc(SharedInv_4e2a3fe_F(), write)
+{
+
+  // decl id_V0_CN0: int°°
+  {
+    var id_V0_CN0: Int
+
+
+
+    // init id_V0_CN0
+    inhale id_V0_CN0 == 0
+
+    // id_V0_CN0 = id_V0
+    id_V0_CN0 := id_V0
+
+    // decl
+
+    // unfold acc(SharedInv_4e2a3fe_F())
+    unfold acc(SharedInv_4e2a3fe_F(), write)
+
+    // assert false
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+    label returnLabel
+  }
+}

src/test/resources/all/issues/silicon/0842.vpr

@@ -0,0 +1,47 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Ref
+field g: Ref
+
+function one(): Int {1}
+function two(): Int {2}
+
+predicate Q(x: Ref)
+
+predicate P(x: Ref) {
+  forall i: Int :: one() == two() && x.f != null ==> acc(x.g.f)
+}
+
+predicate P2(x: Ref) {
+  forall i: Int :: one() == two() && x.f != null ==> Q(x.g)
+}
+
+method consumeField(x: Ref)
+{
+  exhale forall i: Int :: one() == two() && x.f != null ==> acc(x.g.f)
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert false
+}
+
+method produceField(x: Ref)
+{
+  inhale P(x)
+  unfold P(x)
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert false
+}
+
+method consumePred(x: Ref)
+{
+  fold P2(x)
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert false
+}
+
+method producePred(x: Ref)
+{
+  inhale forall i: Int :: one() == two() && x.f != null ==> Q(x.g)
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert false
+}

src/test/resources/all/issues/silver/0787a.vpr

@@ -0,0 +1,14 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+method main()
+{
+    m(some_name)
+}
+
+define m(label_name)
+{
+    goto label_name
+    label label_name
+}

src/test/resources/all/issues/silver/0787b.vpr

@@ -0,0 +1,14 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+method main()
+{
+    //:: ExpectedOutput(parser.error)
+    m(3)
+}
+
+define m(label_name)
+{
+    label label_name
+}

src/test/resources/wands/new_syntax/QPWands.vpr

@@ -23,7 +23,7 @@ requires acc(y.f) {
     invariant xs == completed ++ toGo
     invariant forall x: Ref :: x in toGo ==> x.f == old[setupComplete](x.f)
     invariant acc(y.f) && y.f == 1
-    //:: UnexpectedOutput(invariant.not.preserved:assertion.false, /silicon/issue/311/)
+
     invariant forall x: Ref :: x in completed ==>
       applying (acc(y.f) --* acc(x.f) && acc(y.f) && y.f == old[lhs](y.f)) in
       x.f == old[setupComplete](x.f) {

src/test/scala/SimplifierTests.scala

@@ -36,18 +36,21 @@ class SimplifierTests extends AnyFunSuite with Matchers {
   test("div") {
     simplify(Div(0, 0)()) should be(Div(0, 0)())
     simplify(Div(8, 2)()) should be(4: IntLit)
+    simplify(Div(-3, 2)()) should be(Div(-3, 2)())
+    simplify(Div(3, 2)()) should be(1: IntLit)
+    simplify(Div(3, -2)()) should be(Div(3, -2)())
   }
 
   test("mod") {
     simplify(Mod(0, 0)()) should be (Mod(0, 0)())
     simplify(Mod(8, 3)()) should be (2: IntLit)
     simplify(Mod(3, 8)()) should be (3: IntLit)
-    simplify(Mod(8, -3)()) should be (2: IntLit)
-    simplify(Mod(3, -8)()) should be (3: IntLit)
-    simplify(Mod(-8, 3)()) should be (1: IntLit)
-    simplify(Mod(-3, 8)()) should be (5: IntLit)
-    simplify(Mod(-8, -3)()) should be (1: IntLit)
-    simplify(Mod(-3, -8)()) should be (5: IntLit)
+    simplify(Mod(8, -3)()) should be (Mod(8, -3)())
+    simplify(Mod(3, -8)()) should be (Mod(3, -8)())
+    simplify(Mod(-8, 3)()) should be (Mod(-8, 3)())
+    simplify(Mod(-3, 8)()) should be (Mod(-3, 8)())
+    simplify(Mod(-8, -3)()) should be (Mod(-8, -3)())
+    simplify(Mod(-3, -8)()) should be (Mod(-3, -8)())
   }
 
   test("equality") {