Monomorphization of polymorphic maps and binders (#669)

* first commit

* moved test to the correct location

* first successful verification of polymorphic lambda

* bug fix

* more bug fixes

* minor cleanup

* refactoring

* fixpoint now detects increase in instantiated declarations

* another bug fix

* added support for type instantiation based on instantiated type constructors

* enabled binder instantiation

* fixed bug

* bug fixes

* added representative Viper subset for monomorphization

* add file with parametric Viper domains

* added Dafny files for monomorphization

* remove system information from Viper monomorphization files

* fixed bugs

* refactored MonomorphicExpr() interface method

* split axiom conjuncts into separate axioms

* some typos and minor cleanup

* added dafny and viper tests (but with /noVerify)

* added some documentation

* some refactoring

* fixed bugs and added documentation

* more documentation

* List -> HashSet for instantiationHints

* added two more tests

Co-authored-by: gauravpartha <[email protected]>

Source/Core/StandardVisitor.cs

@@ -530,6 +530,7 @@ public virtual Implementation VisitImplementation(Implementation node)
       node.Blocks = this.VisitBlockList(node.Blocks);
       node.Proc = this.VisitProcedure(cce.NonNull(node.Proc));
       node = (Implementation) this.VisitDeclWithFormals(node); // do this first or last?
+      VisitAttributes(node);
       return node;
     }
 

Source/ExecutionEngine/CommandLineOptions.cs

@@ -1799,7 +1799,7 @@ status in `/trace` and selecting procedures to verify with
        the original name of an identifier translated into Boogie from
        some other source language.
 
-  ---- On Axioms -------------------------------------------------------------
+  ---- On axioms -------------------------------------------------------------
 
     {:include_dep}
       
@@ -1898,6 +1898,8 @@ after substituting variables with their incarnations at the command.
        bound variables with fresh skolem constants, whenever the quantifier is
        skolemized.
 
+     These attributes are not effective for quantifiers inside the scope of axioms.
+
   ---- Civl ------------------------------------------------------------------
 
      {:yields}
@@ -2002,7 +2004,9 @@ inductive sequentialization. These are exempt from the overall pool of
   Multiple .bpl files supplied on the command line are concatenated into one
   Boogie program.
 
-  /lib           : Include library definitions
+  /lib:<name>    : Include definitions in library <name>. The file <name>.bpl
+                   must be an included resource in Core.dll. Currently, the
+                   following libraries are supported---base, node.
   /proc:<p>      : Only check procedures matched by pattern <p>. This option
                    may be specified multiple times to match multiple patterns.
                    The pattern <p> matches the whole procedure name and may

Source/VCGeneration/Prune/AxiomVisitor.cs

@@ -1,5 +1,4 @@
 using System;
-using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
 
@@ -80,10 +79,10 @@ public override Expr VisitExpr(Expr node) {
         bvc.E1.pos = Expr.Position.Neither;
       } else if (node is BinderExpr bexp) {
         bexp.Body.pos = Expr.Position.Neither;
-      } else if (node is LetExpr l){
+      } else if (node is LetExpr l) {
         l.Body.pos = Expr.Position.Neither;
       } else {
-        if(node is LiteralExpr || node is IdentifierExpr) {
+        if (node is LiteralExpr || node is IdentifierExpr) {
 
         } else {
           Console.WriteLine(node);
@@ -93,7 +92,7 @@ public override Expr VisitExpr(Expr node) {
       return base.VisitExpr(node);
     }
 
-    public override Boogie.Type VisitType(Boogie.Type node)
+    public override Type VisitType(Type node)
     {
       types.Add(node);
       return base.VisitType(node);

Source/VCGeneration/Prune/BlocksVisitor.cs

@@ -21,7 +21,7 @@ public override Expr VisitExpr(Expr node)
       return base.VisitExpr(node);
     }
 
-    public override Boogie.Type VisitType(Boogie.Type node)
+    public override Type VisitType(Type node)
     {
       types.Add(node);
       return base.VisitType(node);

Source/VCGeneration/Prune/DependencyEvaluator.cs

@@ -1,5 +1,4 @@
 using System.Collections.Generic;
-using System.Linq;
 
 namespace Microsoft.Boogie
 {
@@ -10,7 +9,7 @@ public class DependencyEvaluator : ReadOnlyVisitor
     // Most incoming dependents correspond to exactly one function or constant, but some of them are tuples.
     // For example, consider an axiom of the form:
     //                        axiom forall x, y :: {P(x, y), Q(y)} {R(x)} P(x, y) ==> R(x)
-    // The axiom may (only) be triggerd by a declaration/implementation that either mentions
+    // The axiom may (only) be triggered by a declaration/implementation that either mentions
     // both P and Q or mentions function R.
     // Thus, it has two incoming dependents:
     // 1) the tuple (P, Q) and 2) the function R. I store tuples in the variable incomingTuples.

Source/VCGeneration/Prune/FunctionVisitor.cs

@@ -28,7 +28,7 @@ public override Expr VisitExpr(Expr node)
       }
       return base.VisitExpr(node);
     }
-    public override Boogie.Type VisitType(Boogie.Type node)
+    public override Type VisitType(Boogie.Type node)
     {
       types.Add(node);
       return base.VisitType(node);

Source/VCGeneration/Prune/Prune.cs

@@ -1,4 +1,3 @@
-using System;
 using System.Linq;
 using System.Collections.Generic;
 using Microsoft.Boogie.GraphUtil;

Test/monomorphize/Dafny_frame.bpl

@@ -0,0 +1,29 @@
+// RUN: %parallel-boogie /monomorphize "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+type Field T;
+type ref;
+type HeapType = [ref]<alpha>[Field alpha]alpha;
+
+var $Heap: HeapType;
+const unique alloc: Field bool;
+const null: ref;
+
+function {:inline} read<alpha>(H: HeapType, r: ref, f: Field alpha) : alpha
+{
+  H[r][f]
+}
+
+procedure p($r: ref)
+requires $r != null;
+requires $Heap[$r][alloc];
+{
+  var $Frame: <beta>[ref,Field beta]bool;
+  var i: int;
+
+  $Frame := (lambda<alpha> $o: ref, $f: Field alpha ::
+    $o != null && read($Heap, $o, alloc) ==> false);
+
+  assert $Frame[null, alloc];
+  assert !$Frame[$r, alloc];
+}

Test/monomorphize/Dafny_frame.bpl.expect

@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors