[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
PlusCal call-goto enhancement
Hi, I have found it desirable in PlusCal to be able to issue a call immediately followed by a goto without an intervening label (for example, in certain cases inside a with block). I see no reason why this relaxation of the labeling rules should be invalid (indeed, it is not much different from the call-followed-by-return case).
Attached please find a patch which adds this feature to the PlusCal compiler. Feedback would be appreciated as I'm sure I've missed something. In particular I'm not sure which of the various .tla files in the source tree are kept up-to-date (at least one of them has "Old" in its name); I'd be glad to also modify the relevant modules if I can be pointed in the right direction. I have tested the patch and it seems to work for my purposes.
--- tla/pcal/AST.java.orig 2017-06-23 16:13:54.802549009 -0400
+++ tla/pcal/AST.java 2017-06-23 16:28:15.693400359 -0400
@@ -17,7 +17,7 @@
* However, there are the following classes that do not represent explicit *
* non-terminals of the +CAL grammar. *
* *
-* Uniprocess MultiProcess SingleAssign CallReturn *
+* Uniprocess MultiProcess SingleAssign CallReturn CallGoto *
* *
* Every AST has col and line fields that contain the position of the *
* first character of the corresponding portion of the algorithm text (as *
@@ -100,6 +100,7 @@
public static AST.Call CallObj ;
public static AST.Return ReturnObj ;
public static AST.CallReturn CallReturnObj ;
+ public static AST.CallGoto CallGotoObj ;
public static AST.Goto GotoObj ;
public static AST.Macro MacroObj ;
public static AST.MacroCall MacroCallObj ;
@@ -214,6 +215,7 @@
CallObj = new AST.Call() ;
ReturnObj = new AST.Return() ;
CallReturnObj = new AST.CallReturn() ;
+ CallGotoObj = new AST.CallGoto() ;
GotoObj = new AST.Goto() ;
MacroObj = new AST.Macro() ;
MacroCallObj = new AST.MacroCall() ;
@@ -840,6 +842,24 @@
" to |-> \"" + to + "\"," + NewLine() +
Indent("args |-> ") + VectorToSeqString(args)
+ "]" + NewLine() +
+ EndIndent() +
+ EndIndent() ;
+ }
+ }
+
+ public static class CallGoto extends AST
+ { public String after = "" ;
+ public String to = "" ;
+ public Vector args = null ; // of TLAExpr
+ public CallGoto() { };
+ public String toString()
+ { return
+ Indent(lineCol()) +
+ "[type |-> \"callGoto\"," + NewLine() +
+ " after |-> \"" + after + "\"," + NewLine() +
+ " to |-> \"" + to + "\"," + NewLine() +
+ Indent("args |-> ") + VectorToSeqString(args)
+ + "]" + NewLine() +
EndIndent() +
EndIndent() ;
}
--- tla/pcal/ParseAlgorithm.java.orig 2017-06-23 16:14:11.556184229 -0400
+++ tla/pcal/ParseAlgorithm.java 2017-06-23 17:00:53.313543911 -0400
@@ -49,9 +49,10 @@
* holds the label (the absence of a label represented by *
* a lbl field equal to the empty string ""). The only difference *
* from the simple grammar is that a <Call> followed by an unlabeled *
-* <Return> is converted into a single AST.CallReturn object. This *
-* pass does not produce any AST.If or AST.Either objects, and any *
-* AST.While object it produces has an empty labDo field. *
+* <Return> or <Goto> is converted into a single AST.CallReturn or *
+* AST.CallGoto object, respectively. This pass does not produce any *
+* AST.If or AST.Either objects, and any AST.While object it produces *
+* has an empty labDo field. *
* *
* - It calls the procedure AddLabelsToStmtSeq to check for missing *
* labels and either add them or report an error if it finds one, *
@@ -1077,7 +1078,7 @@
if (nextTok.equals("print")) { return GetPrintS() ; } ;
if (nextTok.equals("assert")) { return GetAssert() ; } ;
if (nextTok.equals("skip")) { return GetSkip() ; } ;
- if (nextTok.equals("call")) { return GetCallOrCallReturn() ; } ;
+ if (nextTok.equals("call")) { return GetCallOrCallReturnOrCallGoto() ; } ;
if (nextTok.equals("return")) { return GetReturn() ; } ;
if (nextTok.equals("goto")) { return GetGoto() ; } ;
if (nextTok.equals("while")) { return GetWhile() ; } ;
@@ -1581,7 +1582,7 @@
return result ;
}
- public static AST GetCallOrCallReturn() throws ParseAlgorithmException
+ public static AST GetCallOrCallReturnOrCallGoto() throws ParseAlgorithmException
/**********************************************************************
* Note: should not complain if it finds a return that is not inside *
* a procedure because it could be in a macro that is called only *
@@ -1601,6 +1602,23 @@
result.setOrigin(new Region(theCall.getOrigin().getBegin(), end)) ;
return result ;
}
+ else if (PeekAtAlgToken(1).equals("goto"))
+ { MustGobbleThis("goto") ;
+ AST.CallGoto result = new AST.CallGoto();
+ result.col = theCall.col ;
+ result.line = theCall.line ;
+ result.to = theCall.to ;
+ result.after = GetAlgToken() ;
+ result.args = theCall.args ;
+ PCalLocation end = new PCalLocation(lastTokLine-1, lastTokCol-1+result.to.length());
+ result.setOrigin(new Region(theCall.getOrigin().getBegin(), end)) ;
+ gotoUsed = true ;
+ if (result.to.equals("Done") || result.to.equals("\"Done\"")) {
+ gotoDoneUsed = true;
+ }
+ GobbleThis(";") ;
+ return result ;
+ }
else
{ return theCall; }
}
@@ -2016,15 +2034,16 @@
* set assignedVbls to the set of variables being assigned *
* by this statement. Should set nextStepNeedsLabel to *
* true and set assignedVbls to a non-empty set iff this is *
- * a call, return, or callReturn. *
+ * a call, return, callReturn, or callGoto. *
************************************************************/
nextStepNeedsLabel = false ;
Vector assignedVbls = new Vector() ;
/************************************************************
- * Set isCallOrReturn true iff this is a call, return, or *
- * callReturn. Will set setsPrcdVbls true iff this is a *
- * return or callReturn or a call of currentProcedure. *
+ * Set isCallOrReturn true iff this is a call, return, *
+ * callReturn, or callGoto. Will set setsPrcdVbls true iff *
+ * this is a return or callReturn or a call of *
+ * currentProcedure. *
************************************************************/
boolean isCallOrReturn = false ;
boolean setsPrcdVbls = false ;
@@ -2037,6 +2056,12 @@
if (obj.to.equals(currentProcedure))
{ setsPrcdVbls = true ; } ;
}
+ else if (stmt.getClass().equals(AST.CallGotoObj.getClass()))
+ { AST.CallGoto obj = (AST.CallGoto) stmt ;
+ isCallOrReturn = true ;
+ if (obj.to.equals(currentProcedure))
+ { setsPrcdVbls = true ; } ;
+ }
else if ( stmt.getClass().equals(AST.ReturnObj.getClass())
|| stmt.getClass().equals(AST.CallReturnObj.getClass())
)
@@ -2489,8 +2514,10 @@
} ;
result = 1 ;
}
- else if (node.getClass().equals(
- AST.GotoObj.getClass())
+ else if ( node.getClass().equals(
+ AST.GotoObj.getClass())
+ || node.getClass().equals(
+ AST.CallGotoObj.getClass())
)
{ result = 1 ;
}
@@ -3156,6 +3183,25 @@
TLAExpr.SeqSubstituteForAll(tstmt.args, args, params) ;
return result;
} ;
+
+ if (stmt.getClass().equals( AST.CallGotoObj.getClass()))
+ { AST.CallGoto tstmt = (AST.CallGoto) stmt ;
+ AST.CallGoto result = new AST.CallGoto() ;
+ result.col = tstmt.col ;
+ result.line = tstmt.line ;
+ result.macroCol = tstmt.macroCol ;
+ result.macroLine = tstmt.macroLine ;
+ result.setOrigin(tstmt.getOrigin()) ;
+ if (macroLine > 0)
+ { result.macroLine = macroLine ;
+ result.macroCol = macroCol ;
+ } ;
+ result.to = tstmt.to ;
+ result.after = tstmt.after ;
+ result.args =
+ TLAExpr.SeqSubstituteForAll(tstmt.args, args, params) ;
+ return result;
+ } ;
if (stmt.getClass().equals( AST.GotoObj.getClass()))
{ AST.Goto tstmt = (AST.Goto) stmt ;
--- tla/pcal/PcalFixIDs.java.orig 2017-06-23 16:40:14.893653972 -0400
+++ tla/pcal/PcalFixIDs.java 2017-06-23 17:02:01.420843279 -0400
@@ -73,6 +73,8 @@
FixReturn((AST.Return) ast, context);
else if (ast.getClass().equals(AST.CallReturnObj.getClass()))
FixCallReturn((AST.CallReturn) ast, context);
+ else if (ast.getClass().equals(AST.CallGotoObj.getClass()))
+ FixCallGoto((AST.CallGoto) ast, context);
else if (ast.getClass().equals(AST.GotoObj.getClass()))
FixGoto((AST.Goto) ast, context);
@@ -393,6 +395,13 @@
ast.to = st.UseThis(PcalSymTab.PROCEDURE, ast.to, context);
for (int i = 0; i < ast.args.size(); i++)
FixExpr((TLAExpr) ast.args.elementAt(i), context);
+ }
+
+ private static void FixCallGoto(AST.CallGoto ast, String context) throws PcalFixIDException {
+ ast.after = st.UseThis(PcalSymTab.PROCEDURE, ast.after, context);
+ ast.to = st.UseThis(PcalSymTab.PROCEDURE, ast.to, context);
+ for (int i = 0; i < ast.args.size(); i++)
+ FixExpr((TLAExpr) ast.args.elementAt(i), context);
}
private static void FixGoto(AST.Goto ast, String context) throws PcalFixIDException {
--- tla/pcal/PcalSymTab.java.orig 2017-06-23 16:40:24.592771372 -0400
+++ tla/pcal/PcalSymTab.java 2017-06-23 16:40:48.519289620 -0400
@@ -484,6 +484,8 @@
ExtractReturn((AST.Return) ast, context, cType);
else if (ast.getClass().equals(AST.CallReturnObj.getClass()))
ExtractCallReturn((AST.CallReturn) ast, context, cType);
+ else if (ast.getClass().equals(AST.CallGotoObj.getClass()))
+ ExtractCallGoto((AST.CallGoto) ast, context, cType);
else if (ast.getClass().equals(AST.GotoObj.getClass()))
ExtractGoto((AST.Goto) ast, context, cType);
@@ -669,6 +671,11 @@
String cType) {
}
+ private void ExtractCallGoto(AST.CallGoto ast,
+ String context,
+ String cType) {
+ }
+
private void ExtractGoto(AST.Goto ast, String context, String cType) {
}
--- tla/pcal/PcalTranslate.java.orig 2017-06-23 16:40:56.730236561 -0400
+++ tla/pcal/PcalTranslate.java 2017-06-23 17:02:49.549535041 -0400
@@ -556,6 +556,10 @@
result1.removeElementAt(result1.size()-1);
result1.addAll(ExplodeCallReturn((AST.CallReturn) last, next));
}
+ else if (last.getClass().equals(AST.CallGotoObj.getClass())) {
+ result1.removeElementAt(result1.size()-1);
+ result1.addAll(ExplodeCallGoto((AST.CallGoto) last, next));
+ }
else if (last.getClass().equals(AST.IfObj.getClass())) {
AST.If If = (AST.If) last;
Vector p1 = CopyAndExplodeLastStmt(If.Then, next);
@@ -1479,4 +1483,18 @@
result.addElement(UpdatePC(peTo.iPC));
return result;
}
+
+ /***********************************************************************
+ * Generate sequence of statements corresponding to call followed by a *
+ * goto. *
+ ***********************************************************************/
+ private static Vector ExplodeCallGoto(AST.CallGoto ast, String next) throws PcalTranslateException {
+ AST.Call call = new AST.Call();
+ call.to = ast.to;
+ call.args = ast.args;
+ call.line = ast.line;
+ call.col = ast.col;
+ call.setOrigin(ast.getOrigin());
+ return ExplodeCall(call, ast.after);
+ }
}