s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Code tidy. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11085 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 10 years ago
parent
f78b3437d6
commit
8c26fba334
1 changed files with 137 additions and 112 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 249
      prism/src/prism/Preprocessor.java

249
prism/src/prism/Preprocessor.java
View File

@ -26,35 +26,40 @@
package prism;
import java.io.*;
import java.util.Vector;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.io.IOException;
import java.util.Stack;
import java.util.Vector;
import parser.*;
import parser.ast.*;
import parser.type.*;
import parser.Values;
import parser.ast.Expression;
import parser.ast.ForLoop;
import parser.type.Type;
import parser.type.TypeInt;
public class Preprocessor
{
private final static char DELIMITER = '#';
private final static boolean IGNORE_COMMENTS = true;
// prism
private Prism prism;
// files
private File modelFile;
// preprocessing (PP) stuff
private int numPPExprs;
private String ppExprStrings[];
private String ppExprs[];
private int ppExprLines[];
private String lastString;
// interpreter stuff
private int pc; // program counter
private Stack stack; // control flow stack
private Stack<Object> stack; // control flow stack
private String output; // output string
private boolean outputEnabled; // output enabling flag
private Vector<String> varNames; // variable names
@ -62,11 +67,11 @@ public class Preprocessor
private Vector<Integer> varScopes; // variable scopes
private Values values; // variable values
private int paramCounter; // how many paramaters found so far
private String params[];
// constructor
public Preprocessor(Prism p, File mf)
{
prism = p;
@ -79,74 +84,76 @@ public class Preprocessor
}
// main method: do preprocessing
public String preprocess() throws PrismException
{
// see how many preprocessing expressions there are
countPPExprs();
// and bail out if none
if (numPPExprs == 0) return null;
if (numPPExprs == 0)
return null;
// do preprocessing
storePPExprs();
interpret();
return output;
}
// count the number of preprocessing expressions
private void countPPExprs() throws PrismException
{
BufferedReader in;
String s, s2;
int i, count, lineNum = 0;
numPPExprs = 0;
try {
// open file for reading
in = new BufferedReader(new FileReader(modelFile));
try (BufferedReader in = new BufferedReader(new FileReader(modelFile))) {
// read lines one by one
s = in.readLine(); lineNum++;
s = in.readLine();
lineNum++;
while (s != null) {
// strip any comments
i = (IGNORE_COMMENTS) ? s.indexOf("//") : -1;
s2 = (i != -1) ? s.substring(0, i) : s;
// count delimiters
count = 0; i = -1; while ((i = s2.indexOf(DELIMITER, i+1)) != -1) count++;
if (count % 2 != 0) throw new PrismException("Unterminated preprocessing expression at line " + lineNum);
numPPExprs += (count/2);
count = 0;
i = -1;
while ((i = s2.indexOf(DELIMITER, i + 1)) != -1)
count++;
if (count % 2 != 0)
throw new PrismException("Unterminated preprocessing expression at line " + lineNum);
numPPExprs += (count / 2);
// read next line
s = in.readLine(); lineNum++;
s = in.readLine();
lineNum++;
}
// close file
in.close();
}
catch (IOException e) {
} catch (IOException e) {
throw new PrismException("File I/O error reading from \"" + modelFile + "\"");
}
}
// store the preprocessing expressions and related info
private void storePPExprs() throws PrismException
{
BufferedReader in;
String s, s1, s2, s3, text, ss[];
int i, j, n, count, lineNum = 0;
// allocate arrays
ppExprStrings = new String[numPPExprs];
ppExprs = new String[numPPExprs];
ppExprLines = new int[numPPExprs];
try {
count = 0;
text = "";
// open file for reading
in = new BufferedReader(new FileReader(modelFile));
// read lines one by one
s = in.readLine(); lineNum++;
s = in.readLine();
lineNum++;
while (s != null) {
// split into non-comment(s1)/comment(s2)
i = (IGNORE_COMMENTS) ? s.indexOf("//") : -1;
@ -158,101 +165,105 @@ public class Preprocessor
text += s1;
text += s2;
text += "\n";
}
else {
} else {
// strip off stuff before first and after last delimiter
j = s1.lastIndexOf(DELIMITER);
s3 = s1.substring(i, j+1);
s2 = s1.substring(j+1) + s2;
s3 = s1.substring(i, j + 1);
s2 = s1.substring(j + 1) + s2;
s1 = s1.substring(0, i);
// add trailing space so that split() catches any trailing empty pairs of delimiters
s3 += " ";
// go through delimiters
ss = s3.split(""+DELIMITER);
n = (ss.length-1) / 2;
ss = s3.split("" + DELIMITER);
n = (ss.length - 1) / 2;
// add first part of line to text
// (unless this line contains just one pp expr and white space)
if (!(n == 1 && s1.trim().length() == 0 && s2.trim().length() == 0)) text += s1;
if (!(n == 1 && s1.trim().length() == 0 && s2.trim().length() == 0))
text += s1;
for (i = 0; i < n; i++) {
text += ss[2*i];
text += ss[2 * i];
ppExprStrings[count] = text;
ppExprs[count] = ss[2*i+1];
ppExprs[count] = ss[2 * i + 1];
ppExprLines[count] = lineNum;
count++;
text = "";
}
// add last part of line to text
// (unless this line contains just one pp expr and white space)
if (!(n == 1 && s1.trim().length() == 0 && s2.trim().length() == 0)) text += s2 + "\n";
if (!(n == 1 && s1.trim().length() == 0 && s2.trim().length() == 0))
text += s2 + "\n";
}
// read next line
s = in.readLine(); lineNum++;
s = in.readLine();
lineNum++;
}
lastString = text;
// close file
in.close();
}
catch (IOException e) {
} catch (IOException e) {
throw new PrismException("File I/O error reading from \"" + modelFile + "\"");
}
}
// go through the preprocessing expressions, interpreting them
private void interpret() throws PrismException
{
String s;
// initialise interpreter
output = "";
outputEnabled = true;
pc = 0;
stack = new Stack();
stack = new Stack<Object>();
varNames = new Vector<String>();
varTypes = new Vector<Type>();
varScopes = new Vector<Integer>();
values = new Values();
paramCounter = 0;
// main control flow loop
try{
try {
while (pc < numPPExprs) {
// add text preceding this preprocessing expression to output
if (outputEnabled) output += ppExprStrings[pc];
if (outputEnabled)
output += ppExprStrings[pc];
// process current preprocessing expression
s = ppExprs[pc].trim();
// parameter
if (s.indexOf("param int ") == 0) {
s = s.substring(10).trim(); interpretConstant(s);
}
else if (s.indexOf("const ") == 0) {
s = s.substring(10).trim();
interpretConstant(s);
} else if (s.indexOf("const ") == 0) {
// old notation - backwards compatability
s = s.substring(6).trim(); interpretConstant(s);
s = s.substring(6).trim();
interpretConstant(s);
}
// for loops
else if (s.indexOf("for ") == 0) {
s = s.substring(4).trim(); interpretForLoop(s, "");
}
else if (s.indexOf("& ") == 0) {
s = s.substring(2).trim(); interpretForLoop(s, "&");
}
else if (s.indexOf("| ") == 0) {
s = s.substring(2).trim(); interpretForLoop(s, "|");
}
else if (s.indexOf("* ") == 0) {
s = s.substring(2).trim(); interpretForLoop(s, "*");
}
else if (s.indexOf("+ ") == 0) {
s = s.substring(2).trim(); interpretForLoop(s, "+");
}
else if (s.indexOf(", ") == 0) {
s = s.substring(2).trim(); interpretForLoop(s, ",");
}
else if (s.indexOf("; ") == 0) {
s = s.substring(2).trim(); interpretForLoop(s, ";");
s = s.substring(4).trim();
interpretForLoop(s, "");
} else if (s.indexOf("& ") == 0) {
s = s.substring(2).trim();
interpretForLoop(s, "&");
} else if (s.indexOf("| ") == 0) {
s = s.substring(2).trim();
interpretForLoop(s, "|");
} else if (s.indexOf("* ") == 0) {
s = s.substring(2).trim();
interpretForLoop(s, "*");
} else if (s.indexOf("+ ") == 0) {
s = s.substring(2).trim();
interpretForLoop(s, "+");
} else if (s.indexOf(", ") == 0) {
s = s.substring(2).trim();
interpretForLoop(s, ",");
} else if (s.indexOf("; ") == 0) {
s = s.substring(2).trim();
interpretForLoop(s, ";");
}
// end
else if (s.equals("end")) {
@ -269,9 +280,9 @@ public class Preprocessor
}
}
// add final piece of text to output
if (outputEnabled) output += lastString;
}
catch (PrismException e) {
if (outputEnabled)
output += lastString;
} catch (PrismException e) {
throw new PrismException(e.getMessage() + " (preprocessing expression \"" + ppExprs[pc] + "\" at line " + ppExprLines[pc] + ")");
}
}
@ -281,15 +292,21 @@ public class Preprocessor
int i;
String name;
Expression expr;
// if not currently outputting, just skip this
if (!outputEnabled) { pc++; return; }
if (!outputEnabled) {
pc++;
return;
}
// get constant name - terminated by "=", white space or end of expression
i = s.indexOf('=');
if (i == -1) i = s.indexOf(' ');
if (i == -1) i = s.indexOf('\t');
if (i == -1) i = s.length();
if (i == -1)
i = s.indexOf(' ');
if (i == -1)
i = s.indexOf('\t');
if (i == -1)
i = s.length();
name = s.substring(0, i).trim();
// check name is valid identifier
if (!name.matches("[_a-zA-Z]([_a-zA-Z0-9])*"))
@ -308,7 +325,7 @@ public class Preprocessor
s = s.substring(1).trim();
// parse expression, do some checks
expr = prism.parseSingleExpressionString(s);
expr = (Expression)expr.findAllVars(varNames, varTypes);
expr = (Expression) expr.findAllVars(varNames, varTypes);
expr.typeCheck();
expr.semanticCheck();
}
@ -319,7 +336,7 @@ public class Preprocessor
if (expr != null) {
values.addValue(name, new Integer(expr.evaluateInt(null, values)));
} else {
if (params.length <= paramCounter+1)
if (params.length <= paramCounter + 1)
throw new PrismException("No value provided for undefined preprocessor constant \"" + name + "\"");
values.addValue(name, new Integer(Integer.parseInt(params[++paramCounter])));
}
@ -330,15 +347,19 @@ public class Preprocessor
private void interpretForLoop(String s, String between) throws PrismException
{
ForLoop fl;
// if not currently outputting, just stick a dummy for loop on the stack and move on
if (!outputEnabled) { stack.push("Dummy for loop"); pc++; return; }
if (!outputEnabled) {
stack.push("Dummy for loop");
pc++;
return;
}
// parse for loop, do some checks
fl = prism.parseForLoopString(s);
if (varNames.contains(fl.getLHS()))
throw new PrismException("Duplicated variable/constant \"" + fl.getLHS() + "\"");
fl = (ForLoop)fl.findAllVars(varNames, varTypes);
fl = (ForLoop) fl.findAllVars(varNames, varTypes);
fl.typeCheck();
fl.semanticCheck();
// set up more info and then put on stack
@ -354,7 +375,7 @@ public class Preprocessor
if (fl.getFrom().evaluateInt(null, values) > fl.getTo().evaluateInt(null, values)) {
outputEnabled = false;
}
// move to next statement
pc++;
}
@ -363,23 +384,24 @@ public class Preprocessor
{
int i, j;
ForLoop fl;
// make sure there is something to end
if (stack.empty()) throw new PrismException("Surpus \"end\" statement");
if (stack.empty())
throw new PrismException("Surplus \"end\" statement");
// end of for loop
if (stack.peek() instanceof ForLoop) {
fl = (ForLoop)stack.peek();
fl = (ForLoop) stack.peek();
// remove variables that will become out of scope (except loop counter)
i = stack.size();
j = 0; while (j < varNames.size()) {
j = 0;
while (j < varNames.size()) {
if (varScopes.get(j) >= i && !varNames.get(j).equals(fl.getLHS())) {
varNames.removeElementAt(j);
varTypes.removeElementAt(j);
varScopes.removeElementAt(j);
values.removeValue(j);
}
else {
} else {
j++;
}
}
@ -428,13 +450,13 @@ public class Preprocessor
}
}
}
// if not currently outputting, just pop the stack and move on
else if (stack.peek() instanceof String && !outputEnabled) {
stack.pop();
pc++;
}
else {
throw new PrismException("Preprocessor stack error");
}
@ -443,13 +465,16 @@ public class Preprocessor
private void interpretExpression(String s) throws PrismException
{
Expression expr;
// if not currently outputting, just skip this
if (!outputEnabled) { pc++; return; }
if (!outputEnabled) {
pc++;
return;
}
// parse expression, do some checks
expr = prism.parseSingleExpressionString(s);
expr = (Expression)expr.findAllVars(varNames, varTypes);
expr = (Expression) expr.findAllVars(varNames, varTypes);
expr.typeCheck();
expr.semanticCheck();
// add
@ -460,7 +485,8 @@ public class Preprocessor
public static void main(String[] args)
{
if (args.length < 1) return;
if (args.length < 1)
return;
Prism p = new Prism(new PrismFileLog("stdout"));
try {
Preprocessor pp = new Preprocessor(p, new File(args[0]));
@ -471,8 +497,7 @@ public class Preprocessor
} else {
System.out.print(s);
}
}
catch (PrismException e) {
} catch (PrismException e) {
System.err.println("Error: " + e.getMessage());
}
}

Write Preview
Loading…
Cancel
Save