Replace AddAssignedVariables with AddAssignedIdentifiers (#945)

Replace AddAssignedVariables with AddAssignedIdentifiers, because the latter can already be computed before resolution, which is useful for Dafny.
boogie-org · Sep 11, 2024 · 50ef2fb · 50ef2fb
1 parent 16c53d9
commit 50ef2fb
Show file tree

Hide file tree

Showing 16 changed files with 586 additions and 573 deletions.
diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
@@ -229,8 +229,7 @@ private void CheckAsyncToSyncSafety(ActionDecl actionDecl, HashSet<string> refin
               Error(callCmd, "unable to eliminate pending async since a global is modified subsequently");
             }
           }
-          var assignedVariables = new List<Variable>();
-          cmd.AddAssignedVariables(assignedVariables);
+          var assignedVariables = cmd.GetAssignedVariables().ToList();
           if (assignedVariables.OfType<GlobalVariable>().Any())
           {
             modifiedGlobals = true;

diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs
@@ -2042,6 +2042,7 @@ public DatatypeConstructor(Function func)
 
   public class Function : DeclWithFormals
   {
+    public bool AlwaysRevealed;
     public string Comment;
 
     public Expr Body; // Only set if the function is declared with {:inline}
@@ -2121,7 +2122,7 @@ public override void Emit(TokenTextWriter stream, int level)
         stream.WriteLine(this, level, "// " + Comment);
       }
 
-      stream.Write(this, level, "function ");
+      stream.Write(this, level, (AlwaysRevealed ? "revealed " : "") + "function ");
       EmitAttributes(stream);
       if (Body != null && !QKeyValue.FindBoolAttribute(Attributes, "inline"))
       {
@@ -3823,10 +3824,9 @@ public RE()
     {
     }
 
-    public override void AddAssignedVariables(List<Variable> vars)
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars)
     {
-      //Contract.Requires(vars != null);
-      throw new NotImplementedException();
+      throw new NotSupportedException();
     }
   }
 

diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs
@@ -1108,7 +1108,6 @@ void ObjectInvariant()
       Contract.Invariant(cce.NonNullElements(Invariants));
     }
 
-
     public WhileCmd(IToken tok, [Captured] Expr guard, List<PredicateCmd> invariants, List<CallCmd> yields, StmtList body)
       : base(tok)
     {
@@ -1205,10 +1204,8 @@ public override void Emit(TokenTextWriter stream, int level)
       throw new NotImplementedException();
     }
 
-    public override void AddAssignedVariables(List<Variable> vars)
-    {
-      Contract.Requires(vars != null);
-      throw new NotImplementedException();
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
+      throw new NotSupportedException();
     }
   }
 
@@ -1352,14 +1349,22 @@ public Cmd(IToken /*!*/ tok)
     }
 
     public abstract void Emit(TokenTextWriter /*!*/ stream, int level);
-    public abstract void AddAssignedVariables(List<Variable> /*!*/ vars);
+
+    /// <summary>
+    /// Should only be called after resolution
+    /// </summary>
+    public IEnumerable<Variable> GetAssignedVariables() {
+      List<IdentifierExpr> ids = new();
+      AddAssignedIdentifiers(ids);
+      return ids.Select(id => id.Decl);
+    }
+
+    public abstract void AddAssignedIdentifiers(List<IdentifierExpr> /*!*/ vars);
 
     public void CheckAssignments(TypecheckingContext tc)
     {
       Contract.Requires(tc != null);
-      List<Variable> /*!*/
-        vars = new List<Variable>();
-      this.AddAssignedVariables(vars);
+      var /*!*/ vars = GetAssignedVariables().ToList();
       foreach (Variable /*!*/ v in vars)
       {
         Contract.Assert(v != null);
@@ -1527,9 +1532,8 @@ public override void Emit(TokenTextWriter stream, int level)
     public override void Resolve(ResolutionContext rc)
     {
     }
-
-    public override void AddAssignedVariables(List<Variable> vars)
-    {
+
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
     }
 
     public override void Typecheck(TypecheckingContext tc)
@@ -1777,12 +1781,10 @@ public override void Typecheck(TypecheckingContext tc)
       }
     }
 
-    public override void AddAssignedVariables(List<Variable> vars)
-    {
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
       foreach (AssignLhs /*!*/ l in Lhss)
       {
-        Contract.Assert(l != null);
-        vars.Add(l.DeepAssignedVariable);
+        vars.Add(l.DeepAssignedIdentifier);
       }
     }
 
@@ -2307,9 +2309,8 @@ public Expr Rhs
 
     public IEnumerable<IdentifierExpr> UnpackedLhs => lhs.Args.Cast<IdentifierExpr>();
 
-    public override void AddAssignedVariables(List<Variable> vars)
-    {
-      lhs.Args.Cast<IdentifierExpr>().ForEach(arg => vars.Add(arg.Decl));
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
+      lhs.Args.Cast<IdentifierExpr>().ForEach(vars.Add);
     }
 
     public override void Emit(TokenTextWriter stream, int level)
@@ -2423,21 +2424,19 @@ public override void Resolve(ResolutionContext rc)
       rc.PopVarContext();
     }
 
-    public override void AddAssignedVariables(List<Variable> vars)
-    {
-      //Contract.Requires(vars != null);
-      List<Variable> vs = new List<Variable>();
-      foreach (Cmd cmd in this.Cmds)
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
+      var vs = new List<IdentifierExpr>();
+      foreach (Cmd cmd in Cmds)
       {
         Contract.Assert(cmd != null);
-        cmd.AddAssignedVariables(vs);
+        cmd.AddAssignedIdentifiers(vs);
       }
 
       var localsSet = new HashSet<Variable>(this.Locals);
-      foreach (Variable v in vs)
+      foreach (var v in vs)
       {
-        Contract.Assert(v != null);
-        if (!localsSet.Contains(v))
+        Debug.Assert(v.Decl != null);
+        if (!localsSet.Contains(v.Decl))
         {
           vars.Add(v);
         }
@@ -2773,11 +2772,10 @@ public override void Typecheck(TypecheckingContext tc)
       }
     }
 
-    public override void AddAssignedVariables(List<Variable> vars)
-    {
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
       foreach (CallCmd callCmd in CallCmds)
       {
-        callCmd.AddAssignedVariables(vars);
+        callCmd.AddAssignedIdentifiers(vars);
       }
     }
 
@@ -2860,6 +2858,7 @@ void ObjectInvariant()
       Contract.Invariant(Expr != null);
     }
 
+
     public PredicateCmd(IToken /*!*/ tok, Expr /*!*/ expr)
       : base(tok)
     {
@@ -2900,8 +2899,7 @@ public override void Resolve(ResolutionContext rc)
       }
     }
 
-    public override void AddAssignedVariables(List<Variable> vars)
-    {
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
     }
   }
 
@@ -3335,8 +3333,7 @@ public override Absy StdDispatch(StandardVisitor visitor)
 
   public class HavocCmd : Cmd
   {
-    private List<IdentifierExpr> /*!*/
-      _vars;
+    private List<IdentifierExpr> /*!*/ _vars;
 
     public List<IdentifierExpr> /*!*/ Vars
     {
@@ -3384,13 +3381,11 @@ public override void Resolve(ResolutionContext rc)
       }
     }
 
-    public override void AddAssignedVariables(List<Variable> vars)
-    {
-      //Contract.Requires(vars != null);
+    public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
       foreach (IdentifierExpr /*!*/ e in this.Vars)
       {
         Contract.Assert(e != null);
-        vars.Add(e.Decl);
+        vars.Add(e);
       }
     }
 

diff --git a/Source/Core/AST/CallCmd.cs b/Source/Core/AST/CallCmd.cs
@@ -540,8 +540,8 @@ private void TypecheckCallCmdInActionDecl(TypecheckingContext tc)
     }
   }
 
-  public override void AddAssignedVariables(List<Variable> vars)
-  {
+  public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
+    
     if (this.IsAsync)
     {
       return;
@@ -551,20 +551,20 @@ public override void AddAssignedVariables(List<Variable> vars)
     {
       if (e != null)
       {
-        vars.Add(e.Decl);
+        vars.Add(e);
       }
     }
 
     Contract.Assume(this.Proc != null);
     foreach (IdentifierExpr /*!*/ e in this.Proc.Modifies)
     {
       Contract.Assert(e != null);
-      vars.Add(e.Decl);
+      vars.Add(e);
     }
 
     if (AssignedAssumptionVariable != null)
     {
-      vars.Add(AssignedAssumptionVariable);
+      vars.Add(new IdentifierExpr(tok, AssignedAssumptionVariable));
     }
   }
 

diff --git a/Source/Core/AST/ChangeScope.cs b/Source/Core/AST/ChangeScope.cs
@@ -28,7 +28,7 @@ public override void Emit(TokenTextWriter stream, int level) {
     stream.WriteLine(";");
   }
 
-  public override void AddAssignedVariables(List<Variable> vars) {
+  public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
   }
 
   public override Absy StdDispatch(StandardVisitor visitor) {

diff --git a/Source/Core/AST/HideRevealCmd.cs b/Source/Core/AST/HideRevealCmd.cs
@@ -44,8 +44,7 @@ public override void Emit(TokenTextWriter stream, int level)
     stream.WriteLine(";");
   }
 
-  public override void AddAssignedVariables(List<Variable> vars)
-  {
+  public override void AddAssignedIdentifiers(List<IdentifierExpr> vars) {
   }
 
   public override Absy StdDispatch(StandardVisitor visitor)

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
@@ -459,7 +459,10 @@ Function<.out List<Declaration>/*!*/ ds.>
      Expr definition = null;
      Expr/*!*/ tmp;
      Axiom ax;
+     bool revealed = false;
   .)
+  [ "revealed"                         (. revealed = true; .) 
+  ]
   "function" { Attribute<ref kv> } Ident<out z>
   [ TypeParams<out typeParamTok, out typeParams> ]
   "("
@@ -483,6 +486,7 @@ Function<.out List<Declaration>/*!*/ ds.>
     }
     Function/*!*/ func = new Function(z, z.val, typeParams, arguments,
                                       new Formal(retTyd.tok, retTyd, false, argKv), null, kv);
+    func.AlwaysRevealed = revealed;
     foreach(var axiom in axioms) {
         ds.Add(axiom);
         func.OtherDefinitionAxioms.Add(axiom);