Commit 2a5d3a27 authored by Alfons Laarman's avatar Alfons Laarman
Browse files

Print errors in lieu of static exceptions

TODO: new for loop construction
parent 88ce17cb
......@@ -28,6 +28,9 @@ import spins.promela.compiler.variable.*;
import spins.promela.compiler.actions.*;
import java.io.*;
import java.util.*;
import static spins.promela.compiler.ltsmin.util.LTSminUtil.*;
import spins.promela.compiler.ltsmin.util.LTSminUtil;
import static spins.promela.compiler.parser.PromelaConstants.*;
public class Promela {
public static final String C_STATE_PROC_COUNTER = "_pc";
......@@ -99,7 +102,7 @@ public class Promela {
public void addPC(Proctype p) {
Variable pc = new Variable(C_TYPE_PROC_COUNTER, C_STATE_PROC_COUNTER, -1, p);
int initial_pc = (p.getNrActive() == 0 && !p.getName().equals("never") ? -1 : 0);
try { pc.setInitExpr(new ConstantExpression(new Token(PromelaConstants.NUMBER, ""+initial_pc), initial_pc));
try { pc.setInitExpr(new ConstantExpression(new Token(NUMBER, ""+initial_pc), initial_pc));
} catch (ParseException e) { assert (false); }
p.addVariable(pc, false);
}
......@@ -132,6 +135,7 @@ TOKEN : { /* Keywords */
| <XS: "xs">
| <OF: "of">
| <EVAL: "eval">
| <FOR: "for">
| <IF: "if">
| <FI: "fi">
| <DO: "do">
......@@ -270,7 +274,7 @@ SKIP : {
String defined = image.toString().trim();
while (0 != Preprocessor.level) {
Preprocessor.level--;
if (PromelaConstants.RPAREN != getNextToken().kind)
if (RPAREN != getNextToken().kind)
throw new AssertionError("Missing closing parenthesis after defined.");
}
// reinitialize input_stream
......@@ -297,7 +301,7 @@ SKIP : {
defined = image.toString().trim();
while (0 != Preprocessor.level) {
Preprocessor.level--;
if (PromelaConstants.RPAREN != getNextToken().kind)
if (RPAREN != getNextToken().kind)
throw new AssertionError("Missing closing parenthesis after defined.");
}
// reinitialize input_stream
......@@ -328,8 +332,8 @@ loop: while (true) {
Token next = getNextToken();
text += next.image;
switch (next.kind) {
case PromelaConstants.LPAREN: level++; break;
case PromelaConstants.RPAREN: level--; if (0 == level) break loop;
case LPAREN: level++; break;
case RPAREN: level--; if (0 == level) break loop;
}
}
text = text.substring(1, text.length()-1); // delete parentheses
......@@ -380,10 +384,10 @@ SKIP : { // Skip whitespace and comments
if (null == b) {
throw new AssertionError("Spurious null in #if");
} else if (true == b.booleanValue()) {
SwitchTo(PromelaConstants.PREPROCESSOR_SKIP); // if was true, ignore else
SwitchTo(PREPROCESSOR_SKIP); // if was true, ignore else
} else {
throw new AssertionError("Spurious false in DEFAULT else");
//SwitchTo(PromelaConstants.DEFAULT); // if was false, parse else
//SwitchTo(DEFAULT); // if was false, parse else
}
}
| "#elif"
......@@ -393,7 +397,7 @@ SKIP : { // Skip whitespace and comments
if (null == b3) {
throw new AssertionError("Spurious null in DEFAULT #elif");
} else if (true == b3.booleanValue()) {
SwitchTo(PromelaConstants.PREPROCESSOR_SKIP); // if was true, ignore else
SwitchTo(PREPROCESSOR_SKIP); // if was true, ignore else
} else {
throw new AssertionError("Unexpected false else in DEFAULT");
}
......@@ -403,7 +407,7 @@ SKIP : { // Skip whitespace and comments
if (null == Preprocessor.ifs.pop()) { // pop last if
throw new AssertionError("Spurious null in #if");
} else {
SwitchTo(PromelaConstants.DEFAULT); // end ITE
SwitchTo(DEFAULT); // end ITE
}
}
| "#line" : PREPROCESSOR_FILE
......@@ -423,13 +427,18 @@ SKIP : { // Skip whitespace and comments
Promela prom = new Promela(parser, is); // start new parser for condition
try {
Expression expr = prom.expr();
int num = expr.getConstantValue();
int num;
try {
num = expr.getConstantValue();
} catch (Exception e) {
throw new ParseException("The template expression '"+ expr +"' is not a constant");
}
if (0 != num) { // true
Preprocessor.ifs.push(true);
SwitchTo(PromelaConstants.DEFAULT); // parse if until else/endif
SwitchTo(DEFAULT); // parse if until else/endif
} else { // false
Preprocessor.ifs.push(false);
SwitchTo(PromelaConstants.PREPROCESSOR_SKIP); // ignore if until else/enfi
SwitchTo(PREPROCESSOR_SKIP); // ignore if until else/enfi
}
} catch (Exception e) {
throw new AssertionError("Failed to parse #if "+ image.toString()+ e);
......@@ -452,10 +461,10 @@ SKIP : { // Skip whitespace and comments
String def = image.toString().trim();
if (null != Preprocessor.defines(def)) { // true
Preprocessor.ifs.push(true);
SwitchTo(PromelaConstants.DEFAULT); // parse if until else/endif
SwitchTo(DEFAULT); // parse if until else/endif
} else { // false
Preprocessor.ifs.push(false);
SwitchTo(PromelaConstants.PREPROCESSOR_SKIP); // ignore if until else/enfi
SwitchTo(PREPROCESSOR_SKIP); // ignore if until else/enfi
}
}
}
......@@ -472,10 +481,10 @@ SKIP : { // Skip whitespace and comments
def = image.toString().trim();
if (null == Preprocessor.defines(def)) { // true
Preprocessor.ifs.push(true);
SwitchTo(PromelaConstants.DEFAULT); // parse if until else/endif
SwitchTo(DEFAULT); // parse if until else/endif
} else { // false
Preprocessor.ifs.push(false);
SwitchTo(PromelaConstants.PREPROCESSOR_SKIP); // ignore if until else/enfi
SwitchTo(PREPROCESSOR_SKIP); // ignore if until else/enfi
}
}
}
......@@ -493,20 +502,20 @@ SKIP : { // Skip whitespace and comments
{
Boolean b2 = Preprocessor.ifs.peek();
if (null == b2) {
SwitchTo(PromelaConstants.PREPROCESSOR_SKIP); // ignore else
SwitchTo(PREPROCESSOR_SKIP); // ignore else
} else if (true == b2.booleanValue()) {
SwitchTo(PromelaConstants.PREPROCESSOR_SKIP); // (elif was true) ignore else
SwitchTo(PREPROCESSOR_SKIP); // (elif was true) ignore else
} else {
SwitchTo(PromelaConstants.DEFAULT);
SwitchTo(DEFAULT);
}
}
| "#elif" : PREPROCESSOR_ELIF_SKIP
| "#endif"
{
if (null == Preprocessor.ifs.pop()) { // pop last if
SwitchTo(PromelaConstants.PREPROCESSOR_SKIP); // keep ignoring input
SwitchTo(PREPROCESSOR_SKIP); // keep ignoring input
} else { // maybe false of true:
SwitchTo(PromelaConstants.DEFAULT); // end ITE
SwitchTo(DEFAULT); // end ITE
}
}
| < ~[] > : PREPROCESSOR_SKIP
......@@ -518,22 +527,27 @@ SKIP : { // Skip whitespace and comments
< "\n"|"\r"|"\r\n" > { // constant expression is read
Boolean b1 = Preprocessor.ifs.peek();
if (null == b1) { // bogus if
SwitchTo(PromelaConstants.PREPROCESSOR_SKIP);
SwitchTo(PREPROCESSOR_SKIP);
} else if (true == b1.booleanValue()) { // another if condition was true already
SwitchTo(PromelaConstants.PREPROCESSOR_SKIP); // parse if until endif
SwitchTo(PREPROCESSOR_SKIP); // parse if until endif
} else { // current if statement has thusfar not been true
Preprocessor.preprocessing.push(null);
InputStream is3 = new ByteArrayInputStream(image.toString().getBytes());
Promela prom2 = new Promela(parser, is3); // start new parser for condition
try {
Expression expr = prom2.expr();
int num = expr.getConstantValue(); // check condition
int num;
try {
num = expr.getConstantValue();
} catch (Exception e) {
throw new ParseException("The template expression '"+ expr +"' is not a constant");
}
if (0 != num) { // true
Preprocessor.ifs.pop();
Preprocessor.ifs.push(true);
SwitchTo(PromelaConstants.DEFAULT); // parse elif until else/endif
SwitchTo(DEFAULT); // parse elif until else/endif
} else { //false
SwitchTo(PromelaConstants.PREPROCESSOR_SKIP); // skip until elif/endif
SwitchTo(PREPROCESSOR_SKIP); // skip until elif/endif
}
} catch (Exception e) {
int line1 = input_stream.getEndLine();
......@@ -663,9 +677,9 @@ SKIP : { // Skip whitespace and comments
image.setLength(image.length() - 1); // remove '}'
// add inline to preprocessor defines
Preprocessor.addDefine(image.toString(), true);
SwitchTo(PromelaConstants.DEFAULT);
SwitchTo(DEFAULT);
} else {
SwitchTo(PromelaConstants.PREPROCESSOR_INLINE_REST);
SwitchTo(PREPROCESSOR_INLINE_REST);
}
}
| < ~[] >
......@@ -794,9 +808,9 @@ SKIP : { // Skip whitespace and comments
"*/" {
Preprocessor.level--;
if (0 == Preprocessor.level) {
SwitchTo(PromelaConstants.DEFAULT);
SwitchTo(DEFAULT);
} else {
SwitchTo(PromelaConstants.IN_COMMENT);
SwitchTo(IN_COMMENT);
}
}
}
......@@ -1054,8 +1068,12 @@ void ch_init(Token as, VariableContainer store, ChannelVariable var): {
store.addVariable(var); }
|
<LBRACK> size=constant() <RBRACK> <OF>
{
ctype = new ChannelType(size.getConstantValue());
{
try {
ctype = new ChannelType(size.getConstantValue());
} catch (Exception e) {
throw new ParseException("The channel size expression '"+ size +"' is not a constant");
}
var.setType(ctype);
}
<LCURLY> type=typename()
......@@ -1107,6 +1125,25 @@ State sequence(State start, State breakNode, boolean inAtomic): {
{ currentProc.addXS((Identifier)expr); }
(<COMMA> expr=varref() { currentProc.addXS((Identifier)expr); })*
(delim() (end=sequence(end, breakNode, inAtomic))?)?
| <FOR> {
ConstantExpression b, e;
}
<LPAREN> expr=varref() <COLON> b=onlyconstant() <DOT><DOT> e=onlyconstant() <RPAREN>
{
end = new State(automaton, inAtomic);
start.newTransition(LTSminUtil.assign((Identifier)expr, b), end);
start1 = end;
}
<LCURLY> end=sequence(end, breakNode, inAtomic) <RCURLY>
{
trans = end.newTransition(new ExprAction(compare(LT, expr, e)), start1);
trans.addAction( incr((Identifier)expr) );
end1 = end;
end = new State(automaton, inAtomic);
end1.newTransition(new ExprAction(compare(GTE, expr, e)), end);
}
(end=sequence(end, breakNode, inAtomic))?
| <IF>
{ end = new State(automaton, inAtomic); }
(option(start, end, breakNode, inAtomic))+
......@@ -1150,7 +1187,7 @@ State sequence(State start, State breakNode, boolean inAtomic): {
| t=<GOTO> id=<IDENTIFIER>
{
String label = id.image +"_"+ Preprocessor.getLevel();
Token tok = new Token(PromelaConstants.IDENTIFIER, label);
Token tok = new Token(IDENTIFIER, label);
tok.beginLine = id.beginLine;
tok.endLine = id.endLine;
tok.beginColumn = id.beginColumn;
......
......@@ -55,147 +55,149 @@ public interface PromelaConstants {
/** RegularExpression Id. */
int EVAL = 22;
/** RegularExpression Id. */
int IF = 23;
int FOR = 23;
/** RegularExpression Id. */
int FI = 24;
int IF = 24;
/** RegularExpression Id. */
int DO = 25;
int FI = 25;
/** RegularExpression Id. */
int OD = 26;
int DO = 26;
/** RegularExpression Id. */
int ATOMIC = 27;
int OD = 27;
/** RegularExpression Id. */
int D_STEP = 28;
int ATOMIC = 28;
/** RegularExpression Id. */
int ELSE = 29;
int D_STEP = 29;
/** RegularExpression Id. */
int BREAK = 30;
int ELSE = 30;
/** RegularExpression Id. */
int GOTO = 31;
int BREAK = 31;
/** RegularExpression Id. */
int PRINT = 32;
int GOTO = 32;
/** RegularExpression Id. */
int ASSERT = 33;
int PRINT = 33;
/** RegularExpression Id. */
int LEN = 34;
int ASSERT = 34;
/** RegularExpression Id. */
int TIMEOUT = 35;
int LEN = 35;
/** RegularExpression Id. */
int NP_ = 36;
int TIMEOUT = 36;
/** RegularExpression Id. */
int ENABLED = 37;
int NP_ = 37;
/** RegularExpression Id. */
int PC_VALUE = 38;
int ENABLED = 38;
/** RegularExpression Id. */
int RUN = 39;
int PC_VALUE = 39;
/** RegularExpression Id. */
int FULL = 40;
int RUN = 40;
/** RegularExpression Id. */
int EMPTY = 41;
int FULL = 41;
/** RegularExpression Id. */
int NFULL = 42;
int EMPTY = 42;
/** RegularExpression Id. */
int NEMPTY = 43;
int NFULL = 43;
/** RegularExpression Id. */
int TRUE = 44;
int NEMPTY = 44;
/** RegularExpression Id. */
int FALSE = 45;
int TRUE = 45;
/** RegularExpression Id. */
int SKIP_ = 46;
int FALSE = 46;
/** RegularExpression Id. */
int UNLESS = 47;
int SKIP_ = 47;
/** RegularExpression Id. */
int VAR_PID = 48;
int UNLESS = 48;
/** RegularExpression Id. */
int VAR_NR_PR = 49;
int VAR_PID = 49;
/** RegularExpression Id. */
int LCURLY = 50;
int VAR_NR_PR = 50;
/** RegularExpression Id. */
int RCURLY = 51;
int LCURLY = 51;
/** RegularExpression Id. */
int ASSIGN = 52;
int RCURLY = 52;
/** RegularExpression Id. */
int LPAREN = 53;
int ASSIGN = 53;
/** RegularExpression Id. */
int RPAREN = 54;
int LPAREN = 54;
/** RegularExpression Id. */
int LBRACK = 55;
int RPAREN = 55;
/** RegularExpression Id. */
int RBRACK = 56;
int LBRACK = 56;
/** RegularExpression Id. */
int OPTION = 57;
int RBRACK = 57;
/** RegularExpression Id. */
int COLON = 58;
int OPTION = 58;
/** RegularExpression Id. */
int SEMICOLON = 59;
int COLON = 59;
/** RegularExpression Id. */
int COMMA = 60;
int SEMICOLON = 60;
/** RegularExpression Id. */
int RARROW = 61;
int COMMA = 61;
/** RegularExpression Id. */
int CH_SEND_SORTED = 62;
int RARROW = 62;
/** RegularExpression Id. */
int CH_READ = 63;
int CH_SEND_SORTED = 63;
/** RegularExpression Id. */
int CH_READ_RAND = 64;
int CH_READ = 64;
/** RegularExpression Id. */
int AT = 65;
int CH_READ_RAND = 65;
/** RegularExpression Id. */
int BNOT = 66;
int AT = 66;
/** RegularExpression Id. */
int LNOT = 67;
int BNOT = 67;
/** RegularExpression Id. */
int MINUS = 68;
int LNOT = 68;
/** RegularExpression Id. */
int TIMES = 69;
int MINUS = 69;
/** RegularExpression Id. */
int DIVIDE = 70;
int TIMES = 70;
/** RegularExpression Id. */
int MODULO = 71;
int DIVIDE = 71;
/** RegularExpression Id. */
int PLUS = 72;
int MODULO = 72;
/** RegularExpression Id. */
int LSHIFT = 73;
int PLUS = 73;
/** RegularExpression Id. */
int RSHIFT = 74;
int LSHIFT = 74;
/** RegularExpression Id. */
int LT = 75;
int RSHIFT = 75;
/** RegularExpression Id. */
int LTE = 76;
int LT = 76;
/** RegularExpression Id. */
int GT = 77;
int LTE = 77;
/** RegularExpression Id. */
int GTE = 78;
int GT = 78;
/** RegularExpression Id. */
int EQ = 79;
int GTE = 79;
/** RegularExpression Id. */
int NEQ = 80;
int EQ = 80;
/** RegularExpression Id. */
int BAND = 81;
int NEQ = 81;
/** RegularExpression Id. */
int XOR = 82;
int BAND = 82;
/** RegularExpression Id. */
int BOR = 83;
int XOR = 83;
/** RegularExpression Id. */
int LAND = 84;
int BOR = 84;
/** RegularExpression Id. */
int LOR = 85;
int LAND = 85;
/** RegularExpression Id. */
int INCR = 86;
int LOR = 86;
/** RegularExpression Id. */
int DECR = 87;
int INCR = 87;
/** RegularExpression Id. */
int DOT = 88;
int DECR = 88;
/** RegularExpression Id. */
int IDENTIFIER = 98;
int DOT = 89;
/** RegularExpression Id. */
int NUMBER = 99;
int IDENTIFIER = 99;
/** RegularExpression Id. */
int DEFINE = 188;
int NUMBER = 100;
/** RegularExpression Id. */
int PARAM = 193;
int DEFINE = 189;
/** RegularExpression Id. */
int STRING = 215;
int PARAM = 194;
/** RegularExpression Id. */
int STRING = 216;
/** Lexical state. */
int DEFAULT = 0;
......@@ -277,6 +279,7 @@ public interface PromelaConstants {
"\"xs\"",
"\"of\"",
"\"eval\"",
"\"for\"",
"\"if\"",
"\"fi\"",
"\"do\"",
......@@ -348,10 +351,10 @@ public interface PromelaConstants {
"\"ndef\"",
"\"(\"",
"\" \"",
"<token of kind 94>",
"<token of kind 95>",
"\"(\"",
"\" \"",
"<token of kind 97>",
"<token of kind 98>",
"<IDENTIFIER>",
"<NUMBER>",
"\" \"",
......@@ -371,63 +374,63 @@ public interface PromelaConstants {
"\"#define\"",
"\"#include\"",
"\"#\"",
"<token of kind 117>",
"<token of kind 118>",
"\"\\\\\\n\"",
"\"\\\\\\r\"",
"\"\\\\\\r\\n\"",
"<token of kind 121>",
"<token of kind 122>",
"<token of kind 123>",
"<token of kind 124>",
"<token of kind 125>",
"<token of kind 126>",
"<token of kind 127>",
"\"#else\"",
"\"#elif\"",
"\"#endif\"",
"<token of kind 130>",
"<token of kind 131>",
"<token of kind 132>",
"\"\\\\\\n\"",
"\"\\\\\\r\"",
"\"\\\\\\r\\n\"",
"<token of kind 135>",
"<token of kind 136>",
"<token of kind 137>",
"\"\\\\\\n\"",
"\"\\\\\\r\"",
"\"\\\\\\r\\n\"",
"<token of kind 140>",
"<token of kind 141>",
"<token of kind 142>",
"\"\\\\\\n\"",
"\"\\\\\\r\"",
"\"\\\\\\r\\n\"",
"<token of kind 145>",
"<token of kind 146>",
"\" \"",
"\"\\t\"",
"\"\\n\"",
"\"\\r\"",
"\"\\r\\n\"",
"<token of kind 151>",
"<token of kind 152>",
"\" \"",
"\"\\t\"",
"\"\\n\"",
"\"\\r\"",
"\"\\r\\n\"",
"\"(\"",
"<token of kind 158>",
"<token of kind 159>",
"\" \"",
"\"\\t\"",
"\"\\n\"",
"\"\\r\"",
"\"\\r\\n\"",
"<token of kind 164>",
"<token of kind 165>",
"\")\"",
"<token of kind 166>",
"<token of kind 167>",
"\" \"",
"\"\\t\"",
"\"\\n\"",
"\"\\r\"",
"\"\\r\\n\"",
"<token of kind 172>",
"<token of kind 173>",
"<token of kind 174>",
"\" \"",
"\"\\t\"",
"\"\\n\"",
......@@ -435,40 +438,40 @@ public interface PromelaConstants {
"\"\\r\\n\"",
"\",\"",
"\")\"",
"<token of kind 181>",
"<token of kind 182>",
"<token of kind 183>",
"\"{\"",
"\"{\"",
"\"}\"",
"<token of kind 186>",
"<token of kind 187>",