From a52e1134aa8b516809f208fb0de55f64fc813e1c Mon Sep 17 00:00:00 2001
From: Shaz Qadeer <shaz.qadeer@gmail.com>
Date: Thu, 15 Oct 2020 10:48:42 -0700
Subject: [PATCH] another bug fix to have the monomorphizer descend into the
 constructors of monomorphic datatype declarations (#301)

---
 Source/Core/Monomorphization.cs     | 11 +++++-
 Test/monomorphize/vector.bpl        | 52 ++++++++++++++++++++++++++++-
 Test/monomorphize/vector.bpl.expect |  2 +-
 3 files changed, 62 insertions(+), 3 deletions(-)

diff --git a/Source/Core/Monomorphization.cs b/Source/Core/Monomorphization.cs
index 1c5cbe733..1f784bef9 100644
--- a/Source/Core/Monomorphization.cs
+++ b/Source/Core/Monomorphization.cs
@@ -641,7 +641,16 @@ public override Expr VisitExpr(Expr node)
     {
       return exprMonomorphizationVisitor.VisitExpr(node);
     }
-    
+
+    public override Declaration VisitTypeCtorDecl(TypeCtorDecl node)
+    {
+      if (node is DatatypeTypeCtorDecl datatypeTypeCtorDecl)
+      {
+        datatypeTypeCtorDecl.Constructors.Iter(constructor => VisitFunction(constructor));
+      }
+      return base.VisitTypeCtorDecl(node);
+    }
+
     private class TypeInstantiationComparer : IEqualityComparer<List<Type>>
     {
       public bool Equals(List<Type> l1, List<Type> l2)
diff --git a/Test/monomorphize/vector.bpl b/Test/monomorphize/vector.bpl
index 13f69d9eb..ee3035a74 100644
--- a/Test/monomorphize/vector.bpl
+++ b/Test/monomorphize/vector.bpl
@@ -37,6 +37,7 @@ function {:inline} Len<T>(v: Vec T): int
 {
   len#Vec(v)
 }
+
 procedure test0()
 {
   var s: Vec int;
@@ -112,7 +113,7 @@ ensures (forall i, j: int :: 0 <= i && i <= j && j < Len(s') ==> Nth(s', i) <= N
 
 procedure sorted_insert(s: Vec int, x: int) returns (s': Vec int)
 requires (forall i, j: int :: 0 <= i && i <= j && j < Len(s) ==> Nth(s, i) <= Nth(s, j));
-ensures (forall i, j: int :: 0 <= i && i <= j && j < Len(s) ==> Nth(s, i) <= Nth(s, j));
+ensures (forall i, j: int :: 0 <= i && i <= j && j < Len(s') ==> Nth(s', i) <= Nth(s', j));
 {
   var pos: int;
   var val: int;
@@ -138,3 +139,52 @@ ensures (forall i, j: int :: 0 <= i && i <= j && j < Len(s) ==> Nth(s, i) <= Nth
   }
   s' := Append(s', val);
 }
+
+type {:datatype} Value;
+function {:constructor} Integer(i: int): Value;
+function {:constructor} Vector(v: Vec Value): Value;
+
+procedure test3(val: Value) returns (val': Value)
+requires is#Vector(val) && Len(v#Vector(val)) == 1 && Nth(v#Vector(val), 0) == Integer(0);
+ensures val == val';
+{
+  var s: Vec Value;
+
+  s := Empty();
+  s := Append(s, Integer(0));
+  val' := Vector(s);
+}
+
+function has_zero(val: Value): (bool)
+{
+  if (is#Integer(val))
+  then val == Integer(0)
+  else (exists i: int :: 0 <= i && i < Len(v#Vector(val)) && has_zero(Nth(v#Vector(val), i)))
+}
+
+procedure traverse(val: Value) returns (b: bool)
+ensures b == has_zero(val);
+{
+  var s: Vec Value;
+  var i: int;
+
+  b := false;
+  if (is#Integer(val)) {
+      b := val == Integer(0);
+      return;
+  }
+  s := v#Vector(val);
+  i := 0;
+  while (i < Len(s))
+  invariant !b;
+  invariant 0 <= i;
+  invariant (forall j: int :: 0 <= j && j < i ==> !has_zero(Nth(s, j)));
+  {
+    call b := traverse(Nth(s, i));
+    if (b) {
+        return;
+    }
+    assert !has_zero(Nth(s, i));
+    i := i + 1;
+  }
+}
diff --git a/Test/monomorphize/vector.bpl.expect b/Test/monomorphize/vector.bpl.expect
index 76a9a2bfb..12041afe1 100644
--- a/Test/monomorphize/vector.bpl.expect
+++ b/Test/monomorphize/vector.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 8 verified, 0 errors
+Boogie program verifier finished with 10 verified, 0 errors