added the ability to annotate calls with attributes

3 files changed, 43 insertions, 6 deletions

diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc
index 41a62515..72ffba95 100644
--- a/Source/Core/AbsyCmd.ssc
+++ b/Source/Core/AbsyCmd.ssc
@@ -1297,6 +1297,8 @@ namespace Microsoft.Boogie
     // type checking

     public TypeParamInstantiation TypeParameters = null;

 

+    public QKeyValue Attributes;

+    

     // TODO: convert to use generics

     private object errorData;

     public object ErrorData {

@@ -1323,6 +1325,16 @@ namespace Microsoft.Boogie
       this.Outs = outs;

       // base(tok);

     }

+    public CallCmd(IToken! tok, string! callee, List<Expr>! ins, List<IdentifierExpr>! outs, QKeyValue kv)

+      : base(tok)

+    {

+      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 ");

@@ -1405,6 +1417,12 @@ namespace Microsoft.Boogie
                  callee, Outs.Count);

         return;

       }

+      if (QKeyValue.FindBoolAttribute(this.Attributes, "async")) {

+        if (Proc.OutParams.Length > 1) {

+          rc.Error(this.tok, "a procedure called asynchronously can have at most one output parameter");

+          return;

+        }

+      } 

       

       // Check that type parameters can be determined using the given

       // actual i/o arguments. This is done already during resolution

@@ -1467,15 +1485,28 @@ namespace Microsoft.Boogie
       ExprSeq! actualIns = new ExprSeq();

       IdentifierExprSeq! actualOuts = new IdentifierExprSeq();

       for (int i = 0; i < Ins.Count; ++i)

+      {

         if (Ins[i] != null) {

           formalInTypes.Add(((!)Proc.InParams[i]).TypedIdent.Type);

           actualIns.Add(Ins[i]);

         }

+      } 

       for (int i = 0; i < Outs.Count; ++i)

+      {

         if (Outs[i] != null) {

           formalOutTypes.Add(((!)Proc.OutParams[i]).TypedIdent.Type);

           actualOuts.Add(Outs[i]);

         }

+      }

+          

+      if (QKeyValue.FindBoolAttribute(this.Attributes, "async") && Outs.Count > 0) {

+        Type returnType = ((!)Outs[0]).ShallowType;

+        if (!returnType.Equals(Type.Int))

+        {

+          tc.Error(this.tok, "the return from an asynchronous call should be an integer");

+          return;

+        }

+      }

       

       // match actuals with formals

       List<Type!>! actualTypeParams;

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index ee9675a5..495b1263 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -909,17 +909,19 @@ CallCmd<out Cmd! c>
 = (. IToken! x; IToken! first; IToken p;

      List<IdentifierExpr>! ids = new List<IdentifierExpr>();

      List<Expr>! es = new List<Expr>();

+     QKeyValue kv = null;

      Expr en;  List<Expr> args;

      c = dummyCmd;

   .)

   "call"                          (. x = token; .)

+  { Attribute<ref kv> }

   ( Ident<out first>

     ( "("

       [ CallForallArg<out en>       (. es.Add(en); .)

         { "," CallForallArg<out en> (. es.Add(en); .)

         }

       ]

-      ")"                         (. c = new CallCmd(x, first.val, es, ids); .)

+      ")"                         (. c = new CallCmd(x, first.val, es, ids, kv); .)

     |

                                   (. ids.Add(new IdentifierExpr(first, first.val)); .)

       [ "," CallOutIdent<out p>  (.

@@ -943,7 +945,7 @@ CallCmd<out Cmd! c>
         { "," CallForallArg<out en> (. es.Add(en); .)

         }

       ]

-      ")"                         (. c = new CallCmd(x, first.val, es, ids); .)

+      ")"                         (. c = new CallCmd(x, first.val, es, ids, kv); .)

     )

   | "forall"

     Ident<out first> "("              (. args = new List<Expr>(); .)

@@ -975,7 +977,7 @@ CallCmd<out Cmd! c>
         { "," CallForallArg<out en> (. es.Add(en); .)

         }

       ]

-      ")"                         (. c = new CallCmd(x, first.val, es, ids); .)

+      ")"                         (. c = new CallCmd(x, first.val, es, ids, kv); .)

   )

   .

 

diff --git a/Source/Core/Parser.ssc b/Source/Core/Parser.ssc
index d02ccb37..9202e204 100644
--- a/Source/Core/Parser.ssc
+++ b/Source/Core/Parser.ssc
@@ -1168,11 +1168,15 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		IToken! x; IToken! first; IToken p;

 		List<IdentifierExpr>! ids = new List<IdentifierExpr>();

 		List<Expr>! es = new List<Expr>();

+		QKeyValue kv = null;

 		Expr en;  List<Expr> args;

 		c = dummyCmd;

 		

 		Expect(50);

 		x = token; 

+		while (t.kind == 25) {

+			Attribute(ref kv);

+		}

 		if (t.kind == 1) {

 			Ident(out first);

 			if (t.kind == 8) {

@@ -1187,7 +1191,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 					}

 				}

 				Expect(9);

-				c = new CallCmd(x, first.val, es, ids); 

+				c = new CallCmd(x, first.val, es, ids, kv); 

 			} else if (t.kind == 11 || t.kind == 49) {

 				ids.Add(new IdentifierExpr(first, first.val)); 

 				if (t.kind == 11) {

@@ -1223,7 +1227,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 					}

 				}

 				Expect(9);

-				c = new CallCmd(x, first.val, es, ids); 

+				c = new CallCmd(x, first.val, es, ids, kv); 

 			} else Error(106);

 		} else if (t.kind == 51) {

 			Get();

@@ -1277,7 +1281,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				}

 			}

 			Expect(9);

-			c = new CallCmd(x, first.val, es, ids); 

+			c = new CallCmd(x, first.val, es, ids, kv); 

 		} else Error(107);

 	}