refactor: Extract constant folding into separate file (#4921)

This PR does a refactoring of the code that partially evaluates
expressions--that is, that performs constant folding. It also fixes a
null dereference error along the way.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs

@@ -116,7 +116,7 @@ protected override void PostVisitOneExpression(Expression expr, TypeInferenceChe
         var n = (BigInteger)e.Value;
         var absN = n < 0 ? -n : n;
         // For bitvectors, check that the magnitude fits the width
-        if (e.Type.IsBitVectorType && ModuleResolver.MaxBV(e.Type.AsBitVectorType.Width) < absN) {
+        if (e.Type.IsBitVectorType && ConstantFolder.MaxBv(e.Type.AsBitVectorType.Width) < absN) {
           resolver.ReportError(ResolutionErrors.ErrorId.r_literal_too_large_for_bitvector, e.tok, "literal ({0}) is too large for the bitvector type {1}", absN, e.Type);
         }
         // For bitvectors and ORDINALs, check for a unary minus that, earlier, was mistaken for a negative literal

Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs

@@ -285,7 +285,7 @@ protected override void VisitOneExpr(Expression expr) {
           var n = (BigInteger)e.Value;
           var absN = n < 0 ? -n : n;
           // For bitvectors, check that the magnitude fits the width
-          if (PreTypeResolver.IsBitvectorName(familyDeclName, out var width) && ModuleResolver.MaxBV(width) < absN) {
+          if (PreTypeResolver.IsBitvectorName(familyDeclName, out var width) && ConstantFolder.MaxBv(width) < absN) {
             cus.ReportError(e.tok, "literal ({0}) is too large for the bitvector type {1}", absN, e.PreType);
           }
           // For bitvectors and ORDINALs, check for a unary minus that, earlier, was mistaken for a negative literal

Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/diagnosticsFormats.legacy.dfy.expect

@@ -10,7 +10,7 @@ Dafny program verifier finished with 1 verified, 2 errors
 
 Dafny program verifier finished with 1 verified, 2 errors
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":15,"character":0}}},"severity":2,"message":"module-level const declarations are always non-instance, so the \u0027static\u0027 keyword is not allowed here","source":"Parser","relatedInformation":[]}
-{"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":14,"character":8}}},"severity":4,"message":"newtype byte resolves as {:nativeType \u0022byte\u0022} (Detected Range: 0 .. 256)","source":"Resolver","relatedInformation":[]}
+{"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":14,"character":8}}},"severity":4,"message":"newtype byte resolves as {:nativeType \u0022byte\u0022} (detected range: 0 .. 256)","source":"Resolver","relatedInformation":[]}
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":16,"character":17}}},"severity":1,"message":"Error: result of operation might violate newtype constraint for \u0027byte\u0027","source":"Verifier","relatedInformation":[]}
 {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":19,"character":16}}},"severity":1,"message":"Error: a precondition for this call could not be proved","source":"Verifier","relatedInformation":[{"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":18,"character":35}}},"message":"Related location: this is the precondition that could not be proved"}]}
 

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

@@ -1,23 +1,23 @@
-NativeTypeResolution.dfy(4,8): Info: newtype V resolves as {:nativeType "byte"} (Detected Range: 0 .. 200)
-NativeTypeResolution.dfy(5,29): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type.  Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'
-NativeTypeResolution.dfy(6,35): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type.  Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'
-NativeTypeResolution.dfy(8,42): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type.  Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'
-NativeTypeResolution.dfy(10,50): Info: newtype A resolves as {:nativeType "int"} (Detected Range: 0 .. 256)
-NativeTypeResolution.dfy(11,50): Info: newtype B resolves as {:nativeType "byte"} (Detected Range: 0 .. 256)
-NativeTypeResolution.dfy(12,50): Info: newtype C resolves as {:nativeType "int"} (Detected Range: 0 .. 256)
+NativeTypeResolution.dfy(4,8): Info: newtype V resolves as {:nativeType "byte"} (detected range: 0 .. 200)
+NativeTypeResolution.dfy(5,29): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type.  Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)'
+NativeTypeResolution.dfy(6,35): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type.  Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)'
+NativeTypeResolution.dfy(8,42): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type.  Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)'
+NativeTypeResolution.dfy(10,50): Info: newtype A resolves as {:nativeType "int"} (detected range: 0 .. 256)
+NativeTypeResolution.dfy(11,50): Info: newtype B resolves as {:nativeType "byte"} (detected range: 0 .. 256)
+NativeTypeResolution.dfy(12,50): Info: newtype C resolves as {:nativeType "int"} (detected range: 0 .. 256)
 NativeTypeResolution.dfy(14,35): Error: :nativeType 'reallylong' not known
 NativeTypeResolution.dfy(15,41): Error: :nativeType 'reallylong' not known
 NativeTypeResolution.dfy(17,31): Error: None of the types given in :nativeType arguments is supported by the current compilation target. Try supplying others.
 NativeTypeResolution.dfy(18,40): Error: None of the types given in :nativeType arguments is supported by the current compilation target. Try supplying others.
-NativeTypeResolution.dfy(21,22): Error: Dafny's heuristics cannot find a compatible native type.  Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'
-NativeTypeResolution.dfy(22,22): Info: newtype I resolves as {:nativeType "sbyte"} (Detected Range: -2 .. 30)
-NativeTypeResolution.dfy(23,27): Error: Dafny's heuristics cannot find a compatible native type.  Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'
-NativeTypeResolution.dfy(24,27): Info: newtype K resolves as {:nativeType "sbyte"} (Detected Range: -2 .. 30)
+NativeTypeResolution.dfy(21,22): Error: Dafny's heuristics cannot find a compatible native type.  Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)'
+NativeTypeResolution.dfy(22,22): Info: newtype I resolves as {:nativeType "sbyte"} (detected range: -2 .. 30)
+NativeTypeResolution.dfy(23,27): Error: Dafny's heuristics cannot find a compatible native type.  Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)'
+NativeTypeResolution.dfy(24,27): Info: newtype K resolves as {:nativeType "sbyte"} (detected range: -2 .. 30)
 NativeTypeResolution.dfy(29,27): Error: unexpected :nativeType argument
 NativeTypeResolution.dfy(30,21): Error: unexpected :nativeType argument
 NativeTypeResolution.dfy(31,28): Error: :nativeType can only be used on integral types
-NativeTypeResolution.dfy(33,29): Error: Dafny's heuristics failed to confirm 'long' to be a compatible native type.  Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'
-NativeTypeResolution.dfy(34,29): Error: Dafny's heuristics failed to confirm 'long' to be a compatible native type.  Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'
-NativeTypeResolution.dfy(38,8): Info: newtype FF resolves as {:nativeType "sbyte"} (Detected Range: -20 .. 20)
-NativeTypeResolution.dfy(39,29): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type.  Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'
+NativeTypeResolution.dfy(33,29): Error: Dafny's heuristics failed to confirm 'long' to be a compatible native type.  Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)'
+NativeTypeResolution.dfy(34,29): Error: Dafny's heuristics failed to confirm 'long' to be a compatible native type.  Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)'
+NativeTypeResolution.dfy(38,8): Info: newtype FF resolves as {:nativeType "sbyte"} (detected range: -20 .. 20)
+NativeTypeResolution.dfy(39,29): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type.  Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)'
 15 resolution/type errors detected in NativeTypeResolution.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276.dfy.expect

@@ -1,20 +1,20 @@
-git-issue-276.dfy(7,10): Info: newtype byte resolves as {:nativeType "byte"} (Detected Range: 0 .. 256)
-git-issue-276.dfy(8,10): Info: newtype b0 resolves as {:nativeType "ushort"} (Detected Range: 0 .. 2560)
-git-issue-276.dfy(9,10): Info: newtype b1 resolves as {:nativeType "byte"} (Detected Range: 0 .. 5)
-git-issue-276.dfy(10,10): Info: newtype b2 resolves as {:nativeType "byte"} (Detected Range: 0 .. 10)
-git-issue-276.dfy(11,10): Info: newtype b3 resolves as {:nativeType "byte"} (Detected Range: 0 .. 5)
-git-issue-276.dfy(12,10): Info: newtype b3a resolves as {:nativeType "byte"} (Detected Range: 0 .. 5)
-git-issue-276.dfy(13,10): Info: newtype b4 resolves as {:nativeType "byte"} (Detected Range: 0 .. 7)
-git-issue-276.dfy(14,10): Info: newtype b4a resolves as {:nativeType "byte"} (Detected Range: 0 .. 7)
-git-issue-276.dfy(15,10): Info: newtype b5 resolves as {:nativeType "byte"} (Detected Range: 0 .. 42)
-git-issue-276.dfy(16,10): Info: newtype b6 resolves as {:nativeType "byte"} (Detected Range: 0 .. 20)
-git-issue-276.dfy(17,10): Info: newtype b7 resolves as {:nativeType "byte"} (Detected Range: 0 .. 42)
-git-issue-276.dfy(18,10): Info: newtype b8 resolves as {:nativeType "byte"} (Detected Range: 0 .. 20)
-git-issue-276.dfy(19,10): Info: newtype b9 resolves as {:nativeType "byte"} (Detected Range: 0 .. 42)
-git-issue-276.dfy(20,10): Info: newtype ba resolves as {:nativeType "byte"} (Detected Range: 0 .. 20)
-git-issue-276.dfy(21,10): Info: newtype b3b resolves as {:nativeType "byte"} (Detected Range: 0 .. 6)
-git-issue-276.dfy(22,10): Info: newtype b4b resolves as {:nativeType "byte"} (Detected Range: 0 .. 10)
-git-issue-276.dfy(38,10): Info: newtype cx resolves as {:nativeType "byte"} (Detected Range: 0 .. 4)
+git-issue-276.dfy(7,10): Info: newtype byte resolves as {:nativeType "byte"} (detected range: 0 .. 256)
+git-issue-276.dfy(8,10): Info: newtype b0 resolves as {:nativeType "ushort"} (detected range: 0 .. 2560)
+git-issue-276.dfy(9,10): Info: newtype b1 resolves as {:nativeType "byte"} (detected range: 0 .. 5)
+git-issue-276.dfy(10,10): Info: newtype b2 resolves as {:nativeType "byte"} (detected range: 0 .. 10)
+git-issue-276.dfy(11,10): Info: newtype b3 resolves as {:nativeType "byte"} (detected range: 0 .. 5)
+git-issue-276.dfy(12,10): Info: newtype b3a resolves as {:nativeType "byte"} (detected range: 0 .. 5)
+git-issue-276.dfy(13,10): Info: newtype b4 resolves as {:nativeType "byte"} (detected range: 0 .. 7)
+git-issue-276.dfy(14,10): Info: newtype b4a resolves as {:nativeType "byte"} (detected range: 0 .. 7)
+git-issue-276.dfy(15,10): Info: newtype b5 resolves as {:nativeType "byte"} (detected range: 0 .. 42)
+git-issue-276.dfy(16,10): Info: newtype b6 resolves as {:nativeType "byte"} (detected range: 0 .. 20)
+git-issue-276.dfy(17,10): Info: newtype b7 resolves as {:nativeType "byte"} (detected range: 0 .. 42)
+git-issue-276.dfy(18,10): Info: newtype b8 resolves as {:nativeType "byte"} (detected range: 0 .. 20)
+git-issue-276.dfy(19,10): Info: newtype b9 resolves as {:nativeType "byte"} (detected range: 0 .. 42)
+git-issue-276.dfy(20,10): Info: newtype ba resolves as {:nativeType "byte"} (detected range: 0 .. 20)
+git-issue-276.dfy(21,10): Info: newtype b3b resolves as {:nativeType "byte"} (detected range: 0 .. 6)
+git-issue-276.dfy(22,10): Info: newtype b4b resolves as {:nativeType "byte"} (detected range: 0 .. 10)
+git-issue-276.dfy(38,10): Info: newtype cx resolves as {:nativeType "byte"} (detected range: 0 .. 4)
 git-issue-276.dfy(25,17): Error: result of operation might violate newtype constraint for 'byte'
 git-issue-276.dfy(29,18): Error: result of operation might violate newtype constraint for 'b2'
 git-issue-276.dfy(32,18): Error: result of operation might violate newtype constraint for 'b3'

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276a.dfy

@@ -30,3 +30,48 @@ module Main {
   newtype c3 = x | 0 <= x < "abcde"[6] as int
 }
 
+module Regression {
+  newtype GoodUint32 = i: int | 0 <= i <
+    if "abcrimini"[2 + 1 - 1] == 'c' then
+      0x1_0000_0000 + 1 - 1
+    else
+      3
+
+  // Regression test: The following once crashed, because it had expected
+  // the SeqSelect index to really be a folded integer
+  newtype NotUint32 = i: int | 0 <= i <
+    if "abcrimini"[2 + 1 - 1 + k] == 'c' then
+      0x1_0000_0000 + 1 - 1
+    else
+      3
+
+  const k: int
+}
+
+module MoreTests {
+  const bv: bv19 := 203
+
+  newtype EmptyFitsIntoUint8 = i: int |
+    -0x8000_0000 <= i < if !true then 128 else -0x1_0000_0000 // empty range
+    witness *
+
+  newtype int8 = i: int |
+    -128 <= i < if !true then -200 else 128
+
+  newtype AnotherInt8 = i: int |
+    -128 <= i < if true ==> bv == 203 then 128 else -200
+
+  newtype Int16 = i: int |
+    -128 <= i < if true ==> bv == 204 then 128 else 1234
+}
+
+module NotJustInequalityConstraints {
+  newtype Just7 = x: int | 0 <= x < 256 && x == 7 witness 7 // 7..8
+  newtype Just8 = x: int | x == 8 && x == 8 witness 8 // 8..9
+  newtype Also8 = x: int | 8 == x && x < 10 && x < 100 && -2 <= x witness 8 // 8..9
+  newtype Small = x: int | x < 10 && x < 100 && -2 <= x witness 8 // -2..10
+  newtype Only8ButDoesNotDetectCompleteRange = x: int | x == 8 && true witness 8 // 8..9
+  newtype Empty = x: int | 8 == x == 7 && 0 <= x < 256 witness * // empty
+  newtype Byte = x: int | x in {2, 3, 5} witness 3
+  newtype ByteWithKnownRange = x: int | x in {2, 3, 5} && 2 <= x <= 5 witness 3 // 2..6
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276a.dfy.expect

@@ -1,6 +1,18 @@
-git-issue-276a.dfy(23,10): Info: newtype c0 resolves as {:nativeType "byte"} (Detected Range: 0 .. 100)
-git-issue-276a.dfy(27,10): Info: newtype c1 resolves as {:nativeType "byte"} (Detected Range: 0 .. 100)
-git-issue-276a.dfy(28,10): Info: newtype c2 resolves as {:nativeType "byte"} (Detected Range: 0 .. 50)
+git-issue-276a.dfy(23,10): Info: newtype c0 resolves as {:nativeType "byte"} (detected range: 0 .. 100)
+git-issue-276a.dfy(27,10): Info: newtype c1 resolves as {:nativeType "byte"} (detected range: 0 .. 100)
+git-issue-276a.dfy(28,10): Info: newtype c2 resolves as {:nativeType "byte"} (detected range: 0 .. 50)
+git-issue-276a.dfy(34,10): Info: newtype GoodUint32 resolves as {:nativeType "uint"} (detected range: 0 .. 4294967296)
+git-issue-276a.dfy(54,10): Info: newtype EmptyFitsIntoUint8 resolves as {:nativeType "byte"} (detected range: empty)
+git-issue-276a.dfy(58,10): Info: newtype int8 resolves as {:nativeType "sbyte"} (detected range: -128 .. 128)
+git-issue-276a.dfy(61,10): Info: newtype AnotherInt8 resolves as {:nativeType "sbyte"} (detected range: -128 .. 128)
+git-issue-276a.dfy(64,10): Info: newtype Int16 resolves as {:nativeType "short"} (detected range: -128 .. 1234)
+git-issue-276a.dfy(69,10): Info: newtype Just7 resolves as {:nativeType "byte"} (detected range: 7 .. 8)
+git-issue-276a.dfy(70,10): Info: newtype Just8 resolves as {:nativeType "byte"} (detected range: 8 .. 9)
+git-issue-276a.dfy(71,10): Info: newtype Also8 resolves as {:nativeType "byte"} (detected range: 8 .. 9)
+git-issue-276a.dfy(72,10): Info: newtype Small resolves as {:nativeType "sbyte"} (detected range: -2 .. 10)
+git-issue-276a.dfy(73,10): Info: newtype Only8ButDoesNotDetectCompleteRange resolves as {:nativeType "byte"} (detected range: 8 .. 9)
+git-issue-276a.dfy(74,10): Info: newtype Empty resolves as {:nativeType "byte"} (detected range: empty)
+git-issue-276a.dfy(76,10): Info: newtype ByteWithKnownRange resolves as {:nativeType "byte"} (detected range: 2 .. 6)
 git-issue-276a.dfy(5,10): Error: cannot find witness that shows type is inhabited (only tried 0); try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
 git-issue-276a.dfy(5,26): Related location
 git-issue-276a.dfy(5,29): Error: possible division by zero
@@ -37,5 +49,6 @@ git-issue-276a.dfy(21,40): Error: shift amount must be non-negative
 git-issue-276a.dfy(30,10): Error: cannot find witness that shows type is inhabited (only tried 0); try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
 git-issue-276a.dfy(30,26): Related location
 git-issue-276a.dfy(30,35): Error: index out of range
+git-issue-276a.dfy(43,18): Error: index out of range
 
-Dafny program verifier finished with 4 verified, 27 errors
+Dafny program verifier finished with 15 verified, 28 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276b.dfy.expect

@@ -1,12 +1,12 @@
-git-issue-276b.dfy(6,10): Info: newtype b0 resolves as {:nativeType "byte"} (Detected Range: 0 .. 30)
-git-issue-276b.dfy(7,10): Info: newtype b1 resolves as {:nativeType "byte"} (Detected Range: 0 .. 40)
-git-issue-276b.dfy(8,10): Info: newtype b2 resolves as {:nativeType "byte"} (Detected Range: 0 .. 40)
-git-issue-276b.dfy(9,10): Info: newtype b3 resolves as {:nativeType "byte"} (Detected Range: 0 .. 30)
-git-issue-276b.dfy(10,10): Info: newtype b4 resolves as {:nativeType "byte"} (Detected Range: 0 .. 40)
-git-issue-276b.dfy(11,10): Info: newtype b5 resolves as {:nativeType "byte"} (Detected Range: 0 .. 30)
-git-issue-276b.dfy(12,10): Info: newtype b6 resolves as {:nativeType "byte"} (Detected Range: 0 .. 40)
-git-issue-276b.dfy(13,10): Info: newtype b7 resolves as {:nativeType "byte"} (Detected Range: 0 .. 40)
-git-issue-276b.dfy(14,10): Info: newtype b8 resolves as {:nativeType "byte"} (Detected Range: 0 .. 30)
-git-issue-276b.dfy(15,10): Info: newtype b9 resolves as {:nativeType "byte"} (Detected Range: 0 .. 30)
+git-issue-276b.dfy(6,10): Info: newtype b0 resolves as {:nativeType "byte"} (detected range: 0 .. 30)
+git-issue-276b.dfy(7,10): Info: newtype b1 resolves as {:nativeType "byte"} (detected range: 0 .. 40)
+git-issue-276b.dfy(8,10): Info: newtype b2 resolves as {:nativeType "byte"} (detected range: 0 .. 40)
+git-issue-276b.dfy(9,10): Info: newtype b3 resolves as {:nativeType "byte"} (detected range: 0 .. 30)
+git-issue-276b.dfy(10,10): Info: newtype b4 resolves as {:nativeType "byte"} (detected range: 0 .. 40)
+git-issue-276b.dfy(11,10): Info: newtype b5 resolves as {:nativeType "byte"} (detected range: 0 .. 30)
+git-issue-276b.dfy(12,10): Info: newtype b6 resolves as {:nativeType "byte"} (detected range: 0 .. 40)
+git-issue-276b.dfy(13,10): Info: newtype b7 resolves as {:nativeType "byte"} (detected range: 0 .. 40)
+git-issue-276b.dfy(14,10): Info: newtype b8 resolves as {:nativeType "byte"} (detected range: 0 .. 30)
+git-issue-276b.dfy(15,10): Info: newtype b9 resolves as {:nativeType "byte"} (detected range: 0 .. 30)
 
 Dafny program verifier finished with 10 verified, 0 errors