From 3b9b25251b40ba7e9003af2a941d92f94122d3cb Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Tue, 9 Mar 2010 21:25:46 +0000
Subject: Boogie: Added resolution and type checking for attributes on "call"
 and "call forall".  Fixed printing of these attributes to print all
 attributes.

---
 Source/Core/AbsyCmd.ssc | 65 +++++++++++++++++++++++++++++++++----------------
 1 file changed, 44 insertions(+), 21 deletions(-)

(limited to 'Source/Core')

diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc
index e65569b0..bf80116c 100644
--- a/Source/Core/AbsyCmd.ssc
+++ b/Source/Core/AbsyCmd.ssc
@@ -862,6 +862,29 @@ namespace Microsoft.Boogie
       return new AssignCmd(tok, lhss, rhss);
     }
 
+    /// <summary>
+    /// This is a helper routine for printing a linked list of attributes.  Each attribute
+    /// is terminated by a space.
+    /// </summary>
+    public static void EmitAttributes(TokenTextWriter! stream, QKeyValue attributes)
+    {
+      for (QKeyValue kv = attributes; kv != null; kv = kv.Next) {
+        kv.Emit(stream);
+        stream.Write(" ");
+      }
+    }
+    public static void ResolveAttributes(QKeyValue attributes, ResolutionContext! rc)
+    {
+      for (QKeyValue kv = attributes; kv != null; kv = kv.Next) {
+        kv.Resolve(rc);
+      }
+    }
+    public static void TypecheckAttributes(QKeyValue attributes, TypecheckingContext! tc)
+    {
+      for (QKeyValue kv = attributes; kv != null; kv = kv.Next) {
+        kv.Typecheck(tc);
+      }
+    }
   }
 
   public class CommentCmd : Cmd // just a convenience for debugging
@@ -1247,8 +1270,11 @@ namespace Microsoft.Boogie
 
   public abstract class CallCommonality : SugaredCmd
   {
-    protected CallCommonality(IToken! tok) {
+    public QKeyValue Attributes;
+      
+    protected CallCommonality(IToken! tok, QKeyValue kv) {
       base(tok);
+      Attributes = kv;
     }
 
     protected enum TempVarKind { Formal, Old, Bound }
@@ -1297,8 +1323,6 @@ namespace Microsoft.Boogie
     // type checking
     public TypeParamInstantiation TypeParameters = null;
 
-    public QKeyValue Attributes;
-    
     // TODO: convert to use generics
     private object errorData;
     public object ErrorData {
@@ -1318,27 +1342,24 @@ namespace Microsoft.Boogie
       this(tok, callee, insList, outsList);
     }
     public CallCmd(IToken! tok, string! callee, List<Expr>! ins, List<IdentifierExpr>! outs)
-      : base(tok)
     {
+      base(tok, null);
       this.callee = callee;
       this.Ins = ins;
       this.Outs = outs;
-      // base(tok);
     }
     public CallCmd(IToken! tok, string! callee, List<Expr>! ins, List<IdentifierExpr>! outs, QKeyValue kv)
-      : base(tok)
     {
+      base(tok, kv);
       this.callee = callee;
       this.Ins = ins;
       this.Outs = outs;
-      this.Attributes = kv;
-      // base(tok);
     }
     
     public override void Emit(TokenTextWriter! stream, int level)
     {
       stream.Write(this, level, "call ");
-      if (this.Attributes != null) this.Attributes.Emit(stream);
+      EmitAttributes(stream, Attributes);
       string sep = "";
       if (Outs.Count > 0) {
           foreach (Expr arg in Outs) {
@@ -1374,6 +1395,7 @@ namespace Microsoft.Boogie
         // already resolved
         return;
       }
+      ResolveAttributes(Attributes, rc);
       Proc = rc.LookUpProcedure(callee) as Procedure;
       if (Proc == null) {
         rc.Error(this, "call to undeclared procedure: {0}", callee);
@@ -1472,6 +1494,8 @@ namespace Microsoft.Boogie
     {
       assume this.Proc != null;  // we assume the CallCmd has been successfully resolved before calling this Typecheck method
 
+      TypecheckAttributes(Attributes, tc);
+
       // typecheck in-parameters
       foreach (Expr e in Ins)
         if (e!=null)
@@ -1756,25 +1780,22 @@ namespace Microsoft.Boogie
     // actual non-wildcard arguments
     public TypeSeq InstantiatedTypes;
 
-    public QKeyValue Attributes;
-	
     public CallForallCmd(IToken! tok, string! callee, List<Expr>! ins)
-      : base(tok)
     {
+      base(tok, null);
       this.callee = callee;
       this.Ins = ins;
     }
     public CallForallCmd(IToken! tok, string! callee, List<Expr>! ins, QKeyValue kv)
-      : base(tok)
     {
+      base(tok, kv);
       this.callee = callee;
       this.Ins = ins;
-      this.Attributes = kv;
     }
     public override void Emit(TokenTextWriter! stream, int level)
     {
       stream.Write(this, level, "call ");
-      if (this.Attributes != null) this.Attributes.Emit(stream);
+      EmitAttributes(stream, Attributes);
       stream.Write("forall ");
       stream.Write(TokenTextWriter.SanitizeIdentifier(callee));
       stream.Write("(");
@@ -1797,6 +1818,7 @@ namespace Microsoft.Boogie
         // already resolved
         return;
       }
+      ResolveAttributes(Attributes, rc);
       Proc = rc.LookUpProcedure(callee) as Procedure;
       if (Proc == null) {
         rc.Error(this, "call to undeclared procedure: {0}", callee);
@@ -1810,6 +1832,7 @@ namespace Microsoft.Boogie
     public override void AddAssignedVariables(VariableSeq! vars) { }
     public override void Typecheck(TypecheckingContext! tc)
     {
+      TypecheckAttributes(Attributes, tc);
       // typecheck in-parameters
       foreach (Expr e in Ins) {
         if (e != null) {
@@ -2072,19 +2095,19 @@ namespace Microsoft.Boogie
     public override void Emit(TokenTextWriter! stream, int level)
     {
       stream.Write(this, level, "assert ");
-      EmitAttributes(stream);
+      EmitAttributes(stream, Attributes);
       this.Expr.Emit(stream);
       stream.WriteLine(";");
     }
-    protected void EmitAttributes(TokenTextWriter! stream)
+    public override void Resolve(ResolutionContext! rc)
     {
-      for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
-        kv.Emit(stream);
-        stream.Write(" ");
-      }
+      ResolveAttributes(Attributes, rc);
+      base.Resolve(rc);
     }
+
     public override void Typecheck(TypecheckingContext! tc)
     {
+      TypecheckAttributes(Attributes, tc);
       Expr.Typecheck(tc);
       assert Expr.Type != null;  // follows from Expr.Typecheck postcondition
       if (!Expr.Type.Unify(Type.Bool)) 
-- 
cgit v1.2.3