Lit-lift more unary operators

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs

@@ -767,31 +767,38 @@ public Boogie.Expr TrExpr(Expression expr) {
           case UnaryOpExpr opExpr: {
               var e = opExpr;
               Boogie.Expr arg = TrExpr(e.E);
+              Boogie.Expr argWithoutLit = BoogieGenerator.GetLit(arg) ?? arg;
+              var wrapInLit = BoogieGenerator.IsLit(arg);
+              Boogie.Expr result;
               switch (e.ResolvedOp) {
                 case UnaryOpExpr.ResolvedOpcode.Lit:
-                  return MaybeLit(arg);
+                  result = arg;
+                  wrapInLit = true;
+                  break;
                 case UnaryOpExpr.ResolvedOpcode.BVNot:
                   var bvWidth = opExpr.Type.NormalizeToAncestorType().AsBitVectorType.Width;
                   var bvType = BoogieGenerator.BplBvType(bvWidth);
-                  Boogie.Expr r = FunctionCall(GetToken(opExpr), "not_bv" + bvWidth, bvType, arg);
-                  if (BoogieGenerator.IsLit(arg)) {
-                    r = MaybeLit(r, bvType);
-                  }
-                  return r;
+                  result = FunctionCall(GetToken(opExpr), "not_bv" + bvWidth, bvType, argWithoutLit);
+                  break;
                 case UnaryOpExpr.ResolvedOpcode.BoolNot:
-                  return Boogie.Expr.Unary(GetToken(opExpr), UnaryOperator.Opcode.Not, arg);
+                  result = Boogie.Expr.Unary(GetToken(opExpr), UnaryOperator.Opcode.Not, argWithoutLit);
+                  break;
                 case UnaryOpExpr.ResolvedOpcode.SeqLength:
                   Contract.Assert(e.E.Type.NormalizeToAncestorType() is SeqType);
-                  return BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.SeqLength, null, arg);
+                  result = BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.SeqLength, null, argWithoutLit);
+                  break;
                 case UnaryOpExpr.ResolvedOpcode.SetCard:
                   Contract.Assert(e.E.Type.NormalizeToAncestorType() is SetType { Finite: true });
-                  return BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.SetCard, null, arg);
+                  result = BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.SetCard, null, argWithoutLit);
+                  break;
                 case UnaryOpExpr.ResolvedOpcode.MultiSetCard:
                   Contract.Assert(e.E.Type.NormalizeToAncestorType() is MultiSetType);
-                  return BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.MultiSetCard, null, arg);
+                  result = BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.MultiSetCard, null, argWithoutLit);
+                  break;
                 case UnaryOpExpr.ResolvedOpcode.MapCard:
                   Contract.Assert(e.E.Type.NormalizeToAncestorType() is MapType { Finite: true });
-                  return BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.MapCard, null, arg);
+                  result = BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.MapCard, null, argWithoutLit);
+                  break;
                 case UnaryOpExpr.ResolvedOpcode.Fresh:
                   var freshLabel = ((FreshExpr)e).AtLabel;
                   var eeType = e.E.Type.NormalizeToAncestorType();
@@ -859,6 +866,8 @@ public Boogie.Expr TrExpr(Expression expr) {
                 default:
                   Contract.Assert(false); throw new cce.UnreachableException();  // unexpected unary expression
               }
+
+              return wrapInLit ? MaybeLit(result, BoogieGenerator.TrType(expr.Type)) : result;
             }
           case ConversionExpr conversionExpr: {
               var e = conversionExpr;

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LitTests.dfy

@@ -0,0 +1,70 @@
+// RUN: %exits-with 4 %verify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module SeqLength {
+  function LengthToIntUp(v: seq<int>): int {
+    if v == [] then
+      0
+    else
+      1 + LengthToIntUp(v[1..])
+  }
+
+  function LengthToIntDown(v: seq<int>): int {
+    if v == [] then
+      0
+    else
+      1 + LengthToIntDown(v[..|v| - 1])
+  }
+
+  method TestUp() {
+    var j := [2, 3, 5, 7, 11, 13, 17, 19];
+    assert LengthToIntUp(j) == 8;
+  }
+
+  method TestDown() {
+    var j := [2, 3, 5, 7, 11, 13, 17, 19];
+    assert LengthToIntDown(j) == 8;
+  }
+
+  function ToInt(v: seq<int>): int
+    decreases |v|
+  {
+    if |v| == 0 then
+      0
+    else
+      10 * ToInt(v[..|v| - 1]) + v[|v| - 1]
+  }
+
+  function ToIntBackward(v: seq<int>): int
+    decreases |v|
+  {
+    if |v| == 0 then
+      0
+    else
+      v[0] + 10 * ToIntBackward(v[1..])
+  }
+
+  method Test() {
+    assert ToIntBackward([1, 2]) == 21;
+    assert ToIntBackward([1, 2, 3, 4, 5]) == 54321;
+
+    assert ToInt([1, 2]) == 12;
+    assert ToInt([1, 2, 3, 4, 5]) == 12345; // error:  verifier runs out of steam :(
+  }
+
+  method ManualProof() {
+    assert ToInt([1, 2, 3, 4, 5]) == 12345 by {
+      var j := [1, 2, 3, 4, 5];
+      calc {
+        ToInt(j);
+        10 * ToInt(j[..4]) + 5;
+        { assert j[..4][..3] == j[..3]; }
+        100 * ToInt(j[..3]) + 45;
+        { assert j[..3][..2] == j[..2]; }
+        1000 * ToInt(j[..2]) + 345;
+        { assert j[..2][..1] == j[..1]; }
+        10_000 * ToInt(j[..1]) + 2345;
+      }
+    }
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LitTests.dfy.expect

@@ -0,0 +1,3 @@
+LitTests.dfy(52,34): Error: assertion might not hold
+
+Dafny program verifier finished with 7 verified, 1 error