Attempts to fix the lost dependencies during monomoprhization.

The fix is a draft and not optimal, for instance it sometimes adds dependencies that were not part of the `uses` clauses of some functions.
boogie-org · Aug 3, 2023 · 41d2e86 · 41d2e86
1 parent 0b1e684
commit 41d2e86
Show file tree

Hide file tree

Showing 2 changed files with 45 additions and 1 deletion.
diff --git a/Source/Core/Monomorphization.cs b/Source/Core/Monomorphization.cs
@@ -343,7 +343,7 @@ abstract class BinderExprMonomorphizer
      */
 
     protected MonomorphizationVisitor monomorphizationVisitor;
-    protected Dictionary<List<Type>, Expr> instanceExprs;
+    public Dictionary<List<Type>, Expr> instanceExprs { get; }
 
     public BinderExprMonomorphizer(MonomorphizationVisitor monomorphizationVisitor)
     {
@@ -615,6 +615,23 @@ class PolymorphicMapAndBinderSubstituter : VarDeclOnceStandardVisitor
     // be applied.
     private List<Axiom> splitAxioms;
 
+    private Dictionary<Expr, List<Type>> binderExprToTypes = null;
+    public List<Type> lookupTypeForBinderExpr(Expr binderExpr)
+    {
+      if (binderExprToTypes == null)
+      {
+        binderExprToTypes = new Dictionary<Expr, List<Type>>();
+        foreach (var binderMonomorphizer in binderExprMonomorphizers.Values)
+        {
+          foreach ((var types, var expr) in binderMonomorphizer.instanceExprs)
+          {
+            binderExprToTypes.TryAdd(expr, types);
+          }
+        }
+      }
+      return binderExprToTypes.TryGetValue(binderExpr, out var res) ? res : new List<Type>();
+    }
+
     public PolymorphicMapAndBinderSubstituter(MonomorphizationVisitor monomorphizationVisitor)
     {
       this.monomorphizationVisitor = monomorphizationVisitor;
@@ -647,6 +664,10 @@ public override Axiom VisitAxiom(Axiom node)
           stack.Push(nAryExpr.Args[0]);
           stack.Push(nAryExpr.Args[1]);
         }
+        else if (expr == axiom.Expr)
+        {
+          splitAxioms.Add(axiom);
+        }
         else
         {
           splitAxioms.Add(new Axiom(Token.NoToken, expr));
@@ -1379,6 +1400,28 @@ public static MonomorphizationVisitor Initialize(CoreOptions options, Program pr
           polymorphicMapInfo.CreateDatatypeTypeCtorDecl(polymorphicMapAndBinderSubstituter)).ToList();
       var splitAxioms = polymorphicMapAndBinderSubstituter.Substitute(program);
       program.RemoveTopLevelDeclarations(decl => decl is Axiom);
+      foreach (var axiom in splitAxioms)
+      {
+        if (axiom.FunctionDependencies != null)
+        {
+          var functionDependenciesCopy = new List<Function>(axiom.FunctionDependencies);
+          foreach (var function in functionDependenciesCopy)
+          {
+            if (monomorphizationVisitor.functionInstantiations.TryGetValue(function, out var instFuncsMap))
+            {
+              var types = polymorphicMapAndBinderSubstituter.lookupTypeForBinderExpr(axiom.Expr);
+              if (types.Any() && instFuncsMap.ContainsKey(types))
+              {
+                var newFunction = instFuncsMap[types];
+                if (!newFunction.DefinitionAxioms.Contains(axiom))
+                {
+                  newFunction.AddOtherDefinitionAxiom(axiom);
+                }
+              }
+            }
+          }
+        }
+      }
       program.AddTopLevelDeclarations(splitAxioms);
       program.AddTopLevelDeclarations(polymorphicMapDatatypeCtorDecls);
       Contract.Assert(MonomorphismChecker.IsMonomorphic(program));

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -412,6 +412,7 @@ public PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName,
       }
       else if (Options.TypeEncodingMethod == CoreOptions.TypeEncoding.Monomorphic)
       {
+        DependencyCollector.Collect(Options, program);
         var monomorphizableStatus = Monomorphizer.Monomorphize(Options, program);
         if (monomorphizableStatus == MonomorphizableStatus.Monomorphizable)
         {