Skip to content
grammar MatlabParser;
/*
Things to fix:
0) lots of warnings. This is because of anonymous function handles; see details in appropriate XXX comment.
if you comment out one line, all of the warnings go away. I believe that even with the warnings,
the grammar is doing the right thing.
1) "clear" statements can accept wildcards as part of IDs, but we can't (due to the way lexing happens)
2) control flow statements require a newline or comma to resolve an ambiguity (but matlab doesn't)
3) vector construction requires comma delimiters because of whitespace madness (but matlab doesn't)
4) matrix transpose doesn't work (again because of lexing, and distinguishing strings from transposes).
5) block comments don't work (and I can't figure out why)
For each case, see the appropriate XXX comment below.
*/
/*options {
output=AST;
}
tokens {
// imaginary nodes for our AST
PROGRAM;
FUNCTION;
FUNCTION_RETURN;
PARAMETER_LIST;
FUNCTION_PARAMETER_LIST;
STATEMENT_LIST;
EXPRESSION;
EXPR_STMT;
NULL_STMT;
ASSIGN;
APPLY;
FIELDACCESS;
DYNFIELDACCESS;
CELLACCESS;
MATRIX;
VECTOR;
CELL;
CLEAR;
LHS;
RHS;
ID_NODE;
PARENS;
}*/
@parser::members{
// This scans backwards in the token stream looking for a hidden newline.
// The newline must occur after the last visible token and before the current token.
// C IMPLEMENTATION
/*
int check_for_hidden_newline( pmatlabParser ctx ) {
pANTLR3_TOKEN_STREAM ts = ctx->pParser->tstream;
int tok_ind = INDEX(); // this is the index of LT(1)
pANTLR3_COMMON_TOKEN cur_tok = LT(1);
ANTLR3_UINT32 cur_tok_chan = cur_tok->getChannel( cur_tok ); // this is the current channel.
int rval = 0;
while ( tok_ind > 0 ) {
tok_ind--;
cur_tok = ts->get( ts, tok_ind );
if ( cur_tok->getChannel( cur_tok ) == cur_tok_chan ) {
// uh-oh. we found a non-hidden token further back in the stream, but no newline in between. fail.
break;
}
if ( cur_tok->getType( cur_tok ) == NL ) {
// found it!
rval = 1;
break;
}
}
return rval;
}
*/
// JAVA IMPLEMENTATION
// Useful for debugging. NOTE: UNCOMMENT THE RELEVANT LINE IN hidden_nl!
boolean check_for_hidden_newline( TokenStream input ) {
int tok_ind = input.index(); // this is the index of LT(1)
Token cur_tok = input.LT(1);
int cur_tok_chan = cur_tok.getChannel(); // this is the current channel.
boolean rval = false;
while ( tok_ind > 0 ) {
tok_ind--;
cur_tok = input.get( tok_ind );
if ( cur_tok.getChannel() == cur_tok_chan ) {
// uh-oh. we found a non-hidden token further back in the stream, but no newline in between. fail.
break;
}
if ( cur_tok.getType() == NL ) {
// found it!
rval = true;
break;
}
}
return rval;
}
} // end of parser::members
//
// ==================================================================
//
// PARSER RULES
//
// we mostly want to ignore whitespace, but every now and then
// it's significant -- as a statement delimiter, as part of
// matrix construction, etc. This checks the hiddent channel for a newline.
hidden_nl
// Java
: ( { check_for_hidden_newline( _input ) }? )
// C
//: ( { check_for_hidden_newline( ctx ) }? )
;
nloc : ( hidden_nl | COMMA ); // mnemonic: newline or comma
nlos : ( hidden_nl | SEMI ); // mnemonic: newline or semicolon
//
// scripts and m-files
//
mfile : function_definition+;
scriptfile: statement_list;
program : func_or_statement_list;
//
// functions and statements
//
function_definition
: FUNCTION function_return? ID parameter_list? nloc
func_or_statement_list
END
;
function_return
: ID EQ
| LSBRACE (ID COMMA?)+? RSBRACE EQ
;
// the contents of a function (or a .m file) are statements and function definitions
func_or_statement: ( function_definition | statement );
func_or_statement_list: func_or_statement*;
// there are times when you can have a list of statements, but not function
// definitions -- for example, inside of an "if" block.
statement_list
: statement*
;
parameter_list
: LPAREN ( ID COMMA? )* RPAREN
;
// Note: there is a functional difference between terminating a statement with a
// newline vs. a semicolon, so we have to remember the appropriate token in the AST.
statement
: lhs EQ rhs nlosoc #ASSIGNMENT
| expression nlosoc #EXPRESSION
| if_statement #IF_STATEMENT
| for_statement #FOR_STATEMENT
| while_statement #WHILE_STATEMENT
| switch_statement #SWITCH_STATEMENT
| try_statement #TRY_STATEMENT
| return_statement #RETURN_STATEMENT
| break_statement #BREAK_STATEMENT
| continue_statement #CONTINUE_STATEMENT
| clear_statement # CLEAR_STATEMENT
| global_statement #GLOBAL_STATEMENT
| persistent_statement #PERSISTENT_STATEMENT
| SEMI # NULL_STMT // a null statement
;
nlosoc : ( hidden_nl | SEMI | COMMA );
lhs: id_plus_indexers;
rhs: expression;
/*
XXX CONTROL FLOW AMBIGUITIES:
The statement
while a (5) end;
is parsed as
while (a(5))
[empty]
end;
and not
while a
(5)
end;
but I can't seem to get a non-ambiguous grammar to do that.
so, I enforce a newline or a comma after the expression to
delimit it from the body of the statements. everywhere you
see a "nloc" below, you shouldn't really need one; this
grammar therefore parses only a subset of "true" matlab.
(Of course, *I* think that reasonable code wouldn't have
such ambiguities, don't you? :) )
Similarly:
The statement
while 1 -5, end;
is parsed as
while (1)
-5,
end;
while the statement
while 1 - 5, end;
is parsed as
while (1-5)
[empty]
end;
NOTE : THIS FEELS A LOT LIKE THE VECTOR AMBIGUITIES BELOW.
Perhaps solving one solves them both, since both are essentially
'space-delimited expressions' ambiguities.
*/
if_statement
: IF expression nloc statement_list elseif_statement* else_statement? END
;
elseif_statement
: ELSEIF expression nloc statement_list
;
else_statement
: ELSE statement_list
;
for_statement
: FOR ID EQ expression nloc statement_list END
;
while_statement
: WHILE expression nloc statement_list END
;
switch_statement
: SWITCH expression nloc case_statement* otherwise_statement? END
;
case_statement
: CASE expression nloc statement_list
;
otherwise_statement
: OTHERWISE nloc statement_list
;
try_statement
: TRY statement_list catch_statement? END
;
catch_statement
: CATCH ID? nlosoc statement_list
;
return_statement
: RETURNS nlosoc
;
break_statement
: BREAK nlosoc
;
continue_statement
: CONTINUE nlosoc
;
global_statement
: GLOBAL (ID COMMA?)+? nlosoc
;
persistent_statement
: PERSISTENT (ID COMMA?)+? nlosoc
;
/*
XXX CLEAR STATEMENT WILDCARDS
How can we fix wildcards in clear statements?
For example, "clear foo* bob" ought to be parsed as
clear (foo*) (bob)
but this is hard since the '*' is lexed as its own
character, and we've discarded the fact that there is
whitespace between '*' and 'bob', but not between
'foo' and '*'. This means we can't tell that it's supposed
to be part of the foo identifier.
Options for solving:
1) parser-context sensitive lexing? (I don't think this is right)
2) poke around in the hidden channel to find out where the whitespace is.
this is probably the best solution, but seems like a pain.
*/
clear_statement
: CLEAR (ID COMMA?)*? nlosoc
;
//
// ===============================
//
// a precedence hierarchy for parsing expressions
// these are groups of operators that have equivalent precedences
g1 : ( NEQ | DOUBLE_EQ | GRTE | GRT | LSTE | LST );
g2 : ( PLUS | MINUS );
g3 : ( LEFTDIV | RIGHTDIV | TIMES | EL_LEFTDIV | EL_RIGHTDIV | EL_TIMES );
g4 : ( EXP | EL_EXP );
/*
XXX MATRIX TRANSPOSE PROBLEM.
The single quote operator is problematic because of things like this:
aa' + foo('some string here')+bb'
Right now, the operator is placed in the correct place in the grammar,
and the grammar checks out just fine, but you get lexing errors if you
try to use it.
*/
postfix_operator
: ( CCT | EL_CCT );
prefix_operator
: ( PLUS | MINUS | NEG );
// the hierarchy is defined from LOWEST to HIGHEST priority.
expression : e0;
e0 : e1;
e1 : e2 (LOG_OR e2)*;
e2 : e3 (LOG_AND e3)*;
e3 : e4 (BIN_OR e4)*;
e4 : e5 (BIN_AND e5)*;
e5 : e6 (g1 e6)*;
e6 : e7 (COLON e7)*;
e7 : e8 (g2 e8)*;
e8 : e9 (g3 e9)*;
e9 : prefix_operator e9 | e10;
e10 : e11 (g4 e11)*; // note: in matlab, exponentiation is left-associative
e11 : unary_expression postfix_operator?;
unary_expression
: base_expression #BASE_EXPRESIION
| LPAREN expression RPAREN # PARENS_EXPRESSION
;
base_expression
: id_plus_indexers
| literal_number
| STRING
| anon_func_handle
| cell
| matrix
;
literal_number
: INT
| FLOAT
;
/*
XXX ANONYMOUS EXPRESSION AMBIGUITIES
This generates a ton of warnings, but it does the right thing.
At least, I think it does.
We want anonymous expressions to be "greedy".
The statement
a+@()x+y
parses as
a+( @()x+y )
and not as
a+ ( @()x ) +y
but I can't seem to make the right behavior explicit. The way that
ANTLR is disabling the alternatives seems to result in the right
behavior, though.
If you comment out the second alternative here, the grammar should
check out perfectly clean.
*/
anon_func_handle
: AT ID
| AT parameter_list (expression)?
;
// this captures things like foo.(bar){3,4}.baz
id_plus_indexers
: ( i1=ID )
( DOT ( i2=ID )
| LPAREN expression RPAREN
| LPAREN fpl1=function_parameter_list? RPAREN
| LBRACE fpl2=function_parameter_list RBRACE
)*
;
// also permits the use of the colon as an "expression"
function_parameter_list
: function_parameter ( COMMA function_parameter )*
;
function_parameter : expression | COLON ;
matrix : LSBRACE vector? ( nlos vector )* RSBRACE;
cell : LBRACE vector? ( nlos vector )* RBRACE;
/*
XXX
I think the rule is the following
1) if a +/- does not have any space to the right, it's interpreted
as a unary op
2) if there's no whitespace to the left of the operator, it's
grouped to the left.
3) if there's whitespace to the right and left, it's treated as
a binary op, and expressions are required on the right and left.
Vectors are pretty crazy. Because you have a list of expressions
that can be separated by nothing but whitespace, all sorts of parsing
ambiguities start happening. Whitespace becomes syntactically
meaningful in strange ways that are not totally context free.
For example,
[ a + b ] is parsed as [ (a+b) ]
[ a+b ] is parsed as [ (a+b) ]
[ a +b ] is parsed as [ (a) (+b) ]
A longer example:
[ 1+ 2+ 3 ] parses to 6
[ 1 + 2+ 3 ] 6
[ 1 +2+ 3 ] 1 5
[ 1+ 2 + 3 ] 6
[ 1 + 2 + 3 ] 6
[ 1 +2 + 3 ] 1 5
[ 1+ 2 +3 ] 3 3
[ 1 + 2 +3 ] 3 3
[ 1 +2 +3 ] 1 2 3
So, the weird thing is that we can't just look for the absence of a
space between '+' and the next character to determine if it's a binary
or unary operator -- we also have to know if there's a space to the
left of it.
This is mostly a problem for prefix operators which can be ambiguous
in this context, but it also shows up in things like cell arrays
of anonymous function expressions.
size( { @()a+b } ) is [ 1 1 ]
size( { @()a +b } ) is [ 1 2 ]
size( { @()a + b } ) is [ 1 1 ]
NOTE : this feels like the control flow ambiguities above,
since both are essentially "whitespace-delimited expression" problems.
*/
// XXX The COMMA should really have a ? after it!!!
// vector : ( expression COMMA? )+;
vector : expression ( COMMA expression )*;
//
// ==================================================================
//
// LEXER RULES
//
//
// language keywords
//
BREAK : 'break';
CASE : 'case';
CATCH : 'catch';
CONTINUE: 'continue';
ELSE : 'else';
ELSEIF : 'elseif';
END : 'end';
FOR : 'for';
FUNCTION: 'function';
GLOBAL : 'global';
IF : 'if';
OTHERWISE: 'otherwise';
PERSISTENT: 'persistent';
RETURNS : 'return'; // not "RETURN" to avoid #define conflicts with readline.h
SWITCH : 'switch';
TRY : 'try';
VARARGIN: 'varargin';
WHILE : 'while';
CLEAR : 'clear';
ENDS : END SEMI? ;
//
// operators and assignments
//
DOUBLE_EQ : '==';
LOG_OR : '||';
LOG_AND : '&&';
LSTE : '<=';
GRTE : '>=';
NEQ : '~=';
EL_TIMES : '.*';
EL_LEFTDIV : './';
EL_RIGHTDIV : '.\\';
EL_EXP : '.^';
EL_CCT : '.\'';
EQ : '=';
BIN_OR : '|';
BIN_AND : '&';
LST : '<';
GRT : '>';
COLON : ':';
PLUS : '+';
MINUS : '-';
NEG : '~';
TIMES : '*';
LEFTDIV : '/';
RIGHTDIV: '\\';
EXP : '^';
CCT : '\'';
//
// Other useful language snippets
//
SEMI : ';';
LPAREN : '(';
RPAREN : ')';
LBRACE : '{';
RBRACE : '}';
LSBRACE : '[';
RSBRACE : ']';
AT : '@';
DOT : '.';
COMMA : ',';
//
// comments
//
NL : '\r'? '\n' -> channel(HIDDEN); // newline
// XXX I can't seem to get block comments to work. The problem is that
// no matter what I do, the linecomment ends up "overriding" the block
// comment, and I get a lex error. I've tried syntactic predicates,
// but they didn't help...
// If I comment out the LINECOMMENT rule, the BLOCKCOMMENT works fine.
// So, since I can only seem to have one or the other, I'm commenting
// out BLOCKCOMMENT for now.
//BLOCKCOMMENT
// : '%{' (options{greedy=false;} : .)* '%}' { $channel = HIDDEN; }
// ;
LINECOMMENT
: '%' .*? NL -> channel(HIDDEN)
;
// I think this is how to use syntactic predicates, but it doesn't seem to work.
//COMMENT
// : ( '%{' ) => '%{' (options{greedy=false;}: .)* '%}' { $channel = HIDDEN; }
// | ( '%' (options{greedy=false;}: .)* NL ) { $channel = HIDDEN; }
// ;
THREEDOTS
: ( '...' NL ) -> channel(HIDDEN)
;
//
// identifiers, strings, numbers, whitespace
//
ID : ('a'..'z'|'A'..'Z') ('a'..'z'|'A'..'Z'|'0'..'9'|'_')* ;
INT : '0'..'9'+ ;
FLOAT
: ('0'..'9')+ '.' ('0'..'9')* EXPONENT?
| '.' ('0'..'9')+ EXPONENT?
| ('0'..'9')+ EXPONENT
;
STRING
: '\'' ( ESC_SEQ | ~('\\'|'\'') )* '\''
;
WS
: ( ' '
| '\t'
) -> skip
;
fragment
EXPONENT
: ('e'|'E') ('+'|'-')? ('0'..'9')+ ;
fragment
HEX_DIGIT
: ('0'..'9'|'a'..'f'|'A'..'F') ;
fragment
ESC_SEQ
: '\\' ('b'|'t'|'n'|'f'|'r'|'\"'|'\''|'\\')
| UNICODE_ESC
| OCTAL_ESC
;
fragment
OCTAL_ESC
: '\\' ('0'..'3') ('0'..'7') ('0'..'7')
| '\\' ('0'..'7') ('0'..'7')
| '\\' ('0'..'7')
;
fragment
UNICODE_ESC
: '\\' 'u' HEX_DIGIT HEX_DIGIT HEX_DIGIT HEX_DIGIT
;
/*
* To change this template, choose Tools | Templates
* and open the template in the editor.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.parsers;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BinaryOperation;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Expression;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionUnaryOperation;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionValue;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionBinaryOperation;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionWithSubExpression;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Literal;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.UnaryOperation;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableCollection;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.G1Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.G2Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.G3Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.G4Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E0Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E1Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E2Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E3Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E4Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E5Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E6Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E7Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E8Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E9Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E10Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.E11Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.Literal_numberContext;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.Id_plus_indexersContext;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParserParser.Prefix_operatorContext;
import java.util.ArrayDeque;
import java.util.Deque;
import java.util.Map;
import org.antlr.v4.runtime.ANTLRInputStream;
import org.antlr.v4.runtime.CommonTokenStream;
import org.antlr.v4.runtime.tree.ParseTree;
import org.antlr.v4.runtime.tree.ParseTreeWalker;
/**
*
* @author matthew
*/
final public class MatlabParser {
private MatlabParser() {
}
public static Expression parseMatlabCode(VariableCollection variableListing, String matlabCode) {
// create a CharStream that reads from standard input
ANTLRInputStream input = new ANTLRInputStream(matlabCode + "\n");
// create a lexer that feeds off of input CharStream
MatlabParserLexer lexer = new MatlabParserLexer(input);
// create a buffer of tokens pulled from the lexer
CommonTokenStream tokens = new CommonTokenStream(lexer);
// create a parser that feeds off the tokens buffer
MatlabParserParser parser = new MatlabParserParser(tokens);
ParseTree tree = parser.expression();
ParseTreeWalker walker = new ParseTreeWalker();
MatlabParserToExpressions listener = new MatlabParserToExpressions(variableListing.getVariablesAndEnumeratedValues());
walker.walk(listener, tree);
return listener.m_rootExpression;
}
private static class MatlabParserToExpressions extends MatlabParserBaseListener implements ExpressionWithSubExpression {
MatlabParserToExpressions(Map<String, Variable> variableListing) {
m_variableParser = variableListing;
m_opStack.addFirst(new ExpressionStackContainer(0, this));
}
private void incrementLevel() {
this.m_level++;
}
private void decrementLevel() {
this.m_level--;
if (!m_hiddenOpStack.isEmpty() && m_hiddenOpStack.peekFirst().level == m_level) {
// We have a hidden op here. The normal methods won't find it, so make use of it!
HiddenOpStackContainer hiddenOp = m_hiddenOpStack.peekFirst();
addExpressionBinaryOperation(new ExpressionBinaryOperation(null, hiddenOp.op, null));
if (--hiddenOp.count == 0) {
m_hiddenOpStack.removeFirst();
}
}
if (!m_opStack.isEmpty() && m_opStack.peekFirst().level > m_level) {
m_opStack.removeFirst();
}
}
private void enqueHiddenOp(BinaryOperation op, int count) {
m_hiddenOpStack.addFirst(new HiddenOpStackContainer(m_level, op, count));
}
private void addExpressionValue(ExpressionValue expressionValue) {
m_opStack.peekFirst().op.setSubExpression(expressionValue);
}
private void addExpressionBinaryOperation(ExpressionBinaryOperation op) {
if (m_rootExpression == null) {
throw new IllegalStateException("It should not be possible to have"
+ "an op where the left hand side is a null expression!");
} else {
if (m_opStack.peekFirst().level >= m_level) { //This current op happens after the root expression op. Pull it up.
op.setLHS((Expression) m_opStack.removeFirst().op);
m_opStack.peekFirst().op.setSubExpression(op);
} else { //This op happens before. Push it down the tree.
op.setLHS(m_opStack.peekFirst().op.getSubExpression());
m_opStack.peekFirst().op.setSubExpression(op);
}
m_opStack.addFirst(new ExpressionStackContainer(m_level, op));
}
}
private void addPrefixUnaryOperation(ExpressionUnaryOperation op) {
/* Unlike Binary operations, unary operations just always insert
* themselves into the operation stack exactly where they appear.
* The whole left hand side handling never happens, since there is no
* left hand side. So just put it in place.
*
* Also, an unary operation is allowed to deal with a null root expression,
* since it doesn't use it!
*/
m_opStack.peekFirst().op.setSubExpression(op);
m_opStack.addFirst(new ExpressionStackContainer(m_level, op));
}
private static BinaryOperation getBinaryOpForSymbol(String text) {
if (text.equals("+")) {
return BinaryOperation.Addition;
} else if (text.equals("-")) {
return BinaryOperation.Minus;
} else if (text.equals("*")) {
return BinaryOperation.Multiplication;
} else if (text.equals("/")) {
return BinaryOperation.Division;
} else if (text.equals("^")) {
return BinaryOperation.Exponentiation;
} else if (text.equals(">")) {
return BinaryOperation.GreaterThen;
} else if (text.equals(">=")) {
return BinaryOperation.GreaterThenEqual;
} else if (text.equals("<")) {
return BinaryOperation.LessThen;
} else if (text.equals("<=")) {
return BinaryOperation.LessThenEqual;
} else if (text.equals("==")) {
return BinaryOperation.Equals;
} else if (text.equals("~=")) {
return BinaryOperation.NotEquals;
} else if (text.equals("&&")) {
return BinaryOperation.BooleanAnd;
} else if (text.equals("||")) {
return BinaryOperation.BooleanOr;
} else {
throw new IllegalArgumentException("No such binary matlab operation defined (" + text + ")!");
}
}
private static UnaryOperation getUnaryOpForSymbol(String text) {
if (text.equals("~")) {
return UnaryOperation.Negation;
} else if (text.equals("-")) {
return UnaryOperation.Minus;
} else {
throw new IllegalArgumentException("No such unary matlab operation defined (" + text + ")!");
}
}
@Override
public Expression getSubExpression() {
return m_rootExpression;
}
@Override
public void setSubExpression(Expression subExpression) {
m_rootExpression = subExpression;
}
@Override
public void enterE0(E0Context ctx) {
incrementLevel();
}
@Override
public void enterE1(E1Context ctx) {
incrementLevel();
if (ctx.LOG_OR().size() > 0) {
enqueHiddenOp(BinaryOperation.BooleanOr, ctx.LOG_OR().size());
}
}
@Override
public void enterE2(E2Context ctx) {
incrementLevel();
if (ctx.LOG_AND().size() > 0) {
enqueHiddenOp(BinaryOperation.BooleanAnd, ctx.LOG_AND().size());
}
}
@Override
public void enterE3(E3Context ctx) {
incrementLevel();
}
@Override
public void enterE4(E4Context ctx) {
incrementLevel();
}
@Override
public void enterE5(E5Context ctx) {
incrementLevel();
}
@Override
public void enterE6(E6Context ctx) {
incrementLevel();
}
@Override
public void enterE7(E7Context ctx) {
incrementLevel();
}
@Override
public void enterE8(E8Context ctx) {
incrementLevel();
}
@Override
public void enterE9(E9Context ctx) {
incrementLevel();
}
@Override
public void enterE10(E10Context ctx) {
incrementLevel();
}
@Override
public void enterE11(E11Context ctx) {
incrementLevel();
}
@Override
public void exitE0(E0Context ctx) {
decrementLevel();
}
@Override
public void exitE1(E1Context ctx) {
decrementLevel();
}
@Override
public void exitE2(E2Context ctx) {
decrementLevel();
}
@Override
public void exitE3(E3Context ctx) {
decrementLevel();
}
@Override
public void exitE4(E4Context ctx) {
decrementLevel();
}
@Override
public void exitE5(E5Context ctx) {
decrementLevel();
}
@Override
public void exitE6(E6Context ctx) {
decrementLevel();
}
@Override
public void exitE7(E7Context ctx) {
decrementLevel();
}
@Override
public void exitE8(E8Context ctx) {
decrementLevel();
}
@Override
public void exitE9(E9Context ctx) {
decrementLevel();
}
@Override
public void exitE10(E10Context ctx) {
decrementLevel();
}
@Override
public void exitE11(E11Context ctx) {
decrementLevel();
}
@Override
public void enterG1(G1Context ctx) {
addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
}
@Override
public void enterG2(G2Context ctx) {
addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
}
@Override
public void enterG3(G3Context ctx) {
addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
}
@Override
public void enterG4(G4Context ctx) {
addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
}
@Override
public void enterPrefix_operator(Prefix_operatorContext ctx) {
addPrefixUnaryOperation(new ExpressionUnaryOperation(getUnaryOpForSymbol(ctx.getText()), null));
}
@Override
public void exitPrefix_operator(Prefix_operatorContext ctx) {
}
@Override
public void enterLiteral_number(Literal_numberContext ctx) {
addExpressionValue(new Literal(ctx.getText()));
}
@Override
public void enterId_plus_indexers(Id_plus_indexersContext ctx) {
addExpressionValue(m_variableParser.get(ctx.getText()));
}
public Expression m_rootExpression;
private int m_level = 0;
private Map<String, Variable> m_variableParser;
private static class ExpressionStackContainer {
public int level;
public ExpressionWithSubExpression op;
public ExpressionStackContainer(int level, ExpressionWithSubExpression op) {
this.level = level;
this.op = op;
}
}
Deque<ExpressionStackContainer> m_opStack = new ArrayDeque<ExpressionStackContainer>();
private static class HiddenOpStackContainer {
public int level, count;
public BinaryOperation op;
public HiddenOpStackContainer(int level, BinaryOperation op, int count) {
this.level = level;
this.op = op;
this.count = count;
}
}
Deque<HiddenOpStackContainer> m_hiddenOpStack = new ArrayDeque<HiddenOpStackContainer>();
}
}
grammar PVSSimpleParser;
/* This is a simple PVS syntax parser. It is designed to be able to parser simple math statements from PVS, instead of
a full blown parser that could be used to re-implement PVS. This file is roughly based on MatlabParser.g4, without all
the extra pieces from it. It is also modified to make the associated pieces in Java simpler. */
//
// ===============================
//
// a precedence hierarchy for parsing expressions
// these are groups of operators that have equivalent precedences
g1: IMPLIES;
g2: LOG_OR;
g3: LOG_AND;
g4: NEG;
g5: ( NEQ | EQ | GRTE | GRT | LSTE | LST );
g6: ( PLUS | MINUS );
g7: ( LEFTDIV | TIMES );
g8: MINUS;
g9: EXPONENTIATION;
// the hierarchy is defined from LOWEST to HIGHEST priority.
expression : e0;
e0 : e1 g1 e0 | e1; // Implies
e1 : e2 g2 e1 | e2; // Logic OR
e2 : e3 g3 e2 | e3; // Logc AND
e3 : g4 e4 | e4; // Logc NOT
e4 : e4 g5 e5 | e5; // Comparison
e5 : e5 g6 e6 | e6; // Addition/Subtraction
e6 : e6 g7 e7 | e7; // Multiplication/Division
e7 : g8 e8 | e8; // Unary Minus
e8 : e8 g9 e9 | e9; // note: in PVS, exponentiation is left-associative
e9 : unary_expression;
unary_expression
: base_expression #BASE_EXPRESIION
| LPAREN expression RPAREN # PARENS_EXPRESSION
;
base_expression
: id
| literal_number
;
literal_number
: INT
| FLOAT
;
id: i1=ID;
//
// operators and assignments
//
IMPLIES : '=>';
LOG_OR : 'OR';
LOG_AND : 'AND';
LSTE : '<=';
GRTE : '>=';
NEQ : '/=';
EQ : '=';
NEG : 'NOT';
LST : '<';
GRT : '>';
PLUS : '+';
MINUS : '-';
TIMES : '*';
LEFTDIV : '/';
EXPONENTIATION: '^';
LPAREN : '(';
RPAREN : ')';
ID : [a-zA-Z][a-zA-Z0-9]*; //Variable identifier. Start with letter, then alpha numerical allowed.
INT : '0'..'9'+ ;
FLOAT
: ('0'..'9')+ '.' ('0'..'9')* EXPONENT?
| '.' ('0'..'9')+ EXPONENT?
| ('0'..'9')+ EXPONENT
;
WS
: ( ' '
| '\t'
| '\n'
) -> skip
;
fragment
EXPONENT
: ('e'|'E') ('+'|'-')? ('0'..'9')+ ;
/*
* To change this template, choose Tools | Templates
* and open the template in the editor.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.parsers;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BinaryOperation;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Expression;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionBinaryOperation;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionUnaryOperation;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionValue;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionWithSubExpression;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Literal;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.UnaryOperation;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableCollection;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E0Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E1Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E2Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E3Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E4Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E5Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E6Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E7Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E8Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E9Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G1Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G2Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G3Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G4Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G5Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G6Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G7Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G8Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G9Context;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.IdContext;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.Literal_numberContext;
import org.antlr.v4.runtime.ANTLRInputStream;
import org.antlr.v4.runtime.CommonTokenStream;
import org.antlr.v4.runtime.tree.ParseTree;
import org.antlr.v4.runtime.tree.ParseTreeWalker;
import java.util.ArrayDeque;
import java.util.Deque;
import java.util.Map;
/**
*
* @author matthew
*/
final public class PVSSimpleParser {
private PVSSimpleParser() {
}
public static Expression parsePVSCode(VariableCollection variableListing, String pvsCode) {
// create a CharStream that reads from standard input
ANTLRInputStream input = new ANTLRInputStream(pvsCode + "\n");
// create a lexer that feeds off of input CharStream
PVSSimpleParserLexer lexer = new PVSSimpleParserLexer(input);
// create a buffer of tokens pulled from the lexer
CommonTokenStream tokens = new CommonTokenStream(lexer);
// create a parser that feeds off the tokens buffer
PVSSimpleParserParser parser = new PVSSimpleParserParser(tokens);
ParseTree tree = parser.expression();
ParseTreeWalker walker = new ParseTreeWalker();
PVSParserToExpressions listener = new PVSParserToExpressions(variableListing.getVariablesAndEnumeratedValues());
walker.walk(listener, tree);
return listener.m_rootExpression;
}
private static class PVSParserToExpressions extends PVSSimpleParserBaseListener implements ExpressionWithSubExpression {
PVSParserToExpressions(Map<String, Variable> variableListing) {
m_variableParser = variableListing;
m_opStack.addFirst(new ExpressionStackContainer(0, this));
}
private void incrementLevel() {
this.m_level++;
}
private void decrementLevel() {
this.m_level--;
if (!m_hiddenOpStack.isEmpty() && m_hiddenOpStack.peekFirst().level == m_level) {
// We have a hidden op here. The normal methods won't find it, so make use of it!
HiddenOpStackContainer hiddenOp = m_hiddenOpStack.peekFirst();
addExpressionBinaryOperation(new ExpressionBinaryOperation(null, hiddenOp.op, null));
if (--hiddenOp.count == 0) {
m_hiddenOpStack.removeFirst();
}
}
if (!m_opStack.isEmpty() && m_opStack.peekFirst().level > m_level) {
m_opStack.removeFirst();
}
}
private void enqueHiddenOp(BinaryOperation op, int count) {
m_hiddenOpStack.addFirst(new HiddenOpStackContainer(m_level, op, count));
}
private void addExpressionValue(ExpressionValue expressionValue) {
m_opStack.peekFirst().op.setSubExpression(expressionValue);
}
private void addExpressionBinaryOperation(ExpressionBinaryOperation op) {
if (m_rootExpression == null) {
throw new IllegalStateException("It should not be possible to have"
+ "an op where the left hand side is a null expression!");
} else {
if (m_opStack.peekFirst().level >= m_level) { //This current op happens after the root expression op. Pull it up.
op.setLHS((Expression) m_opStack.removeFirst().op);
m_opStack.peekFirst().op.setSubExpression(op);
} else { //This op happens before. Push it down the tree.
op.setLHS(m_opStack.peekFirst().op.getSubExpression());
m_opStack.peekFirst().op.setSubExpression(op);
}
m_opStack.addFirst(new ExpressionStackContainer(m_level, op));
}
}
private void addPrefixUnaryOperation(ExpressionUnaryOperation op) {
/* Unlike Binary operations, unary operations just always insert
* themselves into the operation stack exactly where they appear.
* The whole left hand side handling never happens, since there is no
* left hand side. So just put it in place.
*
* Also, an unary operation is allowed to deal with a null root expression,
* since it doesn't use it!
*/
m_opStack.peekFirst().op.setSubExpression(op);
m_opStack.addFirst(new ExpressionStackContainer(m_level, op));
}
private static BinaryOperation getBinaryOpForSymbol(String text) {
if (text.equals("+")) {
return BinaryOperation.Addition;
} else if (text.equals("-")) {
return BinaryOperation.Minus;
} else if (text.equals("*")) {
return BinaryOperation.Multiplication;
} else if (text.equals("/")) {
return BinaryOperation.Division;
} else if (text.equals("^")) {
return BinaryOperation.Exponentiation;
} else if (text.equals(">")) {
return BinaryOperation.GreaterThen;
} else if (text.equals(">=")) {
return BinaryOperation.GreaterThenEqual;
} else if (text.equals("<")) {
return BinaryOperation.LessThen;
} else if (text.equals("<=")) {
return BinaryOperation.LessThenEqual;
} else if (text.equals("=")) {
return BinaryOperation.Equals;
} else if (text.equals("/=")) {
return BinaryOperation.NotEquals;
} else if (text.equals("=>")) {
return BinaryOperation.Implies;
} else if (text.equals("AND")) {
return BinaryOperation.BooleanAnd;
} else if (text.equals("OR")) {
return BinaryOperation.BooleanOr;
} else {
throw new IllegalArgumentException("No such binary PVS operation defined (" + text + ")!");
}
}
@Override
public Expression getSubExpression() {
return m_rootExpression;
}
@Override
public void setSubExpression(Expression subExpression) {
m_rootExpression = subExpression;
}
@Override
public void enterE0(E0Context ctx) {
incrementLevel();
}
@Override
public void enterE1(E1Context ctx) {
incrementLevel();
}
@Override
public void enterE2(E2Context ctx) {
incrementLevel();
}
@Override
public void enterE3(E3Context ctx) {
incrementLevel();
}
@Override
public void enterE4(E4Context ctx) {
incrementLevel();
}
@Override
public void enterE5(E5Context ctx) {
incrementLevel();
}
@Override
public void enterE6(E6Context ctx) {
incrementLevel();
}
@Override
public void enterE7(E7Context ctx) {
incrementLevel();
}
@Override
public void enterE8(E8Context ctx) {
incrementLevel();
}
@Override
public void enterE9(E9Context ctx) {
incrementLevel();
}
@Override
public void exitE0(E0Context ctx) {
decrementLevel();
}
@Override
public void exitE1(E1Context ctx) {
decrementLevel();
}
@Override
public void exitE2(E2Context ctx) {
decrementLevel();
}
@Override
public void exitE3(E3Context ctx) {
decrementLevel();
}
@Override
public void exitE4(E4Context ctx) {
decrementLevel();
}
@Override
public void exitE5(E5Context ctx) {
decrementLevel();
}
@Override
public void exitE6(E6Context ctx) {
decrementLevel();
}
@Override
public void exitE7(E7Context ctx) {
decrementLevel();
}
@Override
public void exitE8(E8Context ctx) {
decrementLevel();
}
@Override
public void exitE9(E9Context ctx) {
decrementLevel();
}
@Override
public void enterG1(G1Context ctx) {
addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
}
@Override
public void enterG2(G2Context ctx) {
addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
}
@Override
public void enterG3(G3Context ctx) {
addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
}
@Override
public void enterG4(G4Context ctx) {
addPrefixUnaryOperation(new ExpressionUnaryOperation(UnaryOperation.Negation, null)); // This is always negation.
}
@Override
public void enterG5(G5Context ctx) {
addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
}
@Override
public void enterG6(G6Context ctx) {
addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
}
@Override
public void enterG7(G7Context ctx) {
addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
}
@Override
public void enterG8(G8Context ctx) {
addPrefixUnaryOperation(new ExpressionUnaryOperation(UnaryOperation.Minus, null)); // This is always minus.
}
@Override
public void enterG9(G9Context ctx) {
addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
}
@Override
public void enterLiteral_number(Literal_numberContext ctx) {
addExpressionValue(new Literal(ctx.getText()));
}
@Override
public void enterId(IdContext ctx) {
addExpressionValue(m_variableParser.get(ctx.getText()));
}
public Expression m_rootExpression;
private int m_level = 0;
private Map<String, Variable> m_variableParser;
private static class ExpressionStackContainer {
public int level;
public ExpressionWithSubExpression op;
public ExpressionStackContainer(int level, ExpressionWithSubExpression op) {
this.level = level;
this.op = op;
}
}
Deque<ExpressionStackContainer> m_opStack = new ArrayDeque<ExpressionStackContainer>();
private static class HiddenOpStackContainer {
public int level, count;
public BinaryOperation op;
public HiddenOpStackContainer(int level, BinaryOperation op, int count) {
this.level = level;
this.op = op;
this.count = count;
}
}
Deque<HiddenOpStackContainer> m_hiddenOpStack = new ArrayDeque<HiddenOpStackContainer>();
}
}
/*
* To change this template, choose Tools | Templates
* and open the template in the editor.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.parsers;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Expression;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.FixedPointVariableType;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.RealVariableType;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableCollection;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParserParser.Bool_typeContext;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParserParser.DefaulttypeContext;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParserParser.Fixed_typeContext;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParserParser.Real_typeContext;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParserParser.VarContext;
import java.util.HashMap;
import java.util.Map;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableType;
import org.antlr.v4.runtime.ANTLRInputStream;
import org.antlr.v4.runtime.CommonTokenStream;
import org.antlr.v4.runtime.misc.NotNull;
import org.antlr.v4.runtime.tree.ParseTree;
import org.antlr.v4.runtime.tree.ParseTreeWalker;
import org.antlr.v4.runtime.tree.TerminalNode;
/**
*
* @author Matthew Dawson
*/
final public class VariableParser {
public VariableCollection parseVariables(String variables) {
// create a CharStream that reads from standard input
ANTLRInputStream input = new ANTLRInputStream(variables) {
@Override
public int LA(int i) {
return Character.toLowerCase(super.LA(i));
}
};
// create a lexer that feeds off of input CharStream
VariableParserLexer lexer = new VariableParserLexer(input);
// create a buffer of tokens pulled from the lexer
CommonTokenStream tokens = new CommonTokenStream(lexer);
// create a parser that feeds off the tokens buffer
VariableParserParser parser = new VariableParserParser(tokens);
ParseTree tree = parser.varlist();
ParseTreeWalker walker = new ParseTreeWalker();
VariablesParserToVariables listener = new VariablesParserToVariables();
walker.walk(listener, tree);
return listener.m_variableCollection;
}
public void addCustomType(String typeName, VariableType type) {
m_customTypes.put(typeName, type);
}
private final Map<String, VariableType> m_customTypes = new HashMap<String, VariableType>();
private class VariablesParserToVariables extends VariableParserParserBaseListener {
private String currentName;
private VariableType currentType;
private limitingExpressionData currentLimitingExpression;
@Override
public void enterVar(VarContext ctx) {
currentName = ctx.ID().getText();
}
@Override
public void enterDefaulttype(DefaulttypeContext ctx) {
currentType = new RealVariableType();
}
@Override
public void enterReal_type(Real_typeContext ctx) {
currentType = new RealVariableType();
}
@Override
public void enterBool_type(Bool_typeContext ctx) {
currentType = new BooleanVariableType();
}
@Override
public void enterUnknown_type(@NotNull VariableParserParser.Unknown_typeContext ctx) {
currentType = m_customTypes.get(ctx.UNKNOWN_TYPE().getText());
if (currentType == null) { // Assume this unknown. For now, pretend a real is wanted.
currentType = new RealVariableType();
}
}
@Override
public void enterSubtype_var(@NotNull VariableParserParser.Subtype_varContext ctx) {
currentLimitingExpression = new limitingExpressionData();
currentLimitingExpression.variableName = ctx.ID().getText();
}
@Override
public void enterPvs_expr(@NotNull VariableParserParser.Pvs_exprContext ctx) {
currentLimitingExpression.expression = ctx.PVS_EXPR().getText();
}
@Override
public void enterFixed_type(Fixed_typeContext ctx) {
boolean signed = (ctx.NAT(0).getText().equals("0"))?false:true;
int digits = Integer.parseInt(ctx.NAT(1).getText());
int fractionPart = 0;
TerminalNode fractionNode;
if ((fractionNode = ctx.NAT(2)) != null) {
fractionPart = Integer.parseInt(fractionNode.getText());
}
currentType = new FixedPointVariableType(signed, digits, fractionPart);
}
@Override
public void exitVar(VarContext ctx) {
m_variables.put(currentName, new Variable(currentName, currentType));
if (currentLimitingExpression != null) {
m_variableLimitingExpressions.put(currentName, currentLimitingExpression);
}
currentName = null;
currentType = null;
currentLimitingExpression = null;
}
@Override
public void exitVarlist(@NotNull VariableParserParser.VarlistContext ctx) {
m_variableCollection = new VariableCollection(m_variables);
for(Map.Entry<String, limitingExpressionData> limitingExpression : m_variableLimitingExpressions.entrySet()) {
String subtypeVar = limitingExpression.getValue().variableName;
String subtypeExpression = limitingExpression.getValue().expression;
if (m_variables.containsKey(limitingExpression.getValue().variableName)) {
throw new IllegalStateException("Reused variable name for subtype declaration!");
}
// Get the variable we are working on, and use it for the variable used in the subtype expression. This
// effectively means the expression can just be emitted into the verification system to limit it.
m_variables.put(subtypeVar, m_variables.get(limitingExpression.getKey()));
m_variables.get(limitingExpression.getKey()).type().setSubtypePredicate(PVSSimpleParser.parsePVSCode(m_variableCollection, subtypeExpression));
// Undo the variables hack, to avoid having unused variables bleed into the verification scripts!
m_variables.remove(subtypeVar);
}
}
private Map<String, Variable> m_variables = new HashMap<String, Variable>();
public VariableCollection m_variableCollection;
private Map<String, limitingExpressionData> m_variableLimitingExpressions = new HashMap<String, limitingExpressionData>();
}
private static class limitingExpressionData {
public String expression;
public String variableName;
}
}
lexer grammar VariableParserLexer;
tokens { ID }
fragment IDRule: [a-zA-Z][a-zA-Z0-9]*; //Variable identifier. Start with letter, then alpha numerical allowed.
REGULAR_ID: IDRule -> type(ID), pushMode(VARIABLE_TYPE);
fragment WS : [ \t\r\n]+; // skip spaces, tabs, newlines
WS1: WS -> skip ;
mode PVS_EXPR_MODE;
PVS_EXPR: ~[\{\}]+ -> popMode;
mode VARIABLE_TYPE;
VAR_SEPARATOR: ',' -> popMode;
COLON: ':';
BOOL_TYPE: 'bool';
REAL_TYPE: 'real';
FIXEDT: 'fixedt' -> pushMode(FIXED_TYPE);
UNKNOWN_TYPE: [a-zA-Z_]+;
OPEN_SUBTYPE: '{' -> pushMode(ID_FETCH);
PVS_EXPR_BEGIN: '|' -> pushMode(PVS_EXPR_MODE);
CLOSE_SUBTYPE: '}';
WS2: WS -> skip;
mode FIXED_TYPE;
NAT_SEPARATOR: ',';
OPEN_BRACKET: '(';
CLOSE_BRACKET: ')' -> popMode;
NAT: [0-9]+;
WS3: WS -> skip;
mode ID_FETCH;
SUBTYPE_ID: IDRule -> type(ID), popMode;
WS4: WS -> skip;
parser grammar VariableParserParser;
options { tokenVocab=VariableParserLexer; }
varlist: var (VAR_SEPARATOR var)*; //Build list of variables
var: ID vartype;
vartype: ':' type_info
| defaulttype;
defaulttype: ;
type_info: simple_type_info
| '{' subtype '}';
subtype: subtype_var '|' pvs_expr;
subtype_var: ID subtype_vartype;
subtype_vartype: ':' simple_type_info
| defaulttype;
pvs_expr: PVS_EXPR;
simple_type_info: bool_type
| real_type
| fixed_type
| unknown_type;
bool_type: BOOL_TYPE;
real_type: 'real';
fixed_type: 'fixedt' '(' NAT NAT_SEPARATOR NAT ')'
| 'fixedt' '(' NAT NAT_SEPARATOR NAT NAT_SEPARATOR NAT ')';
unknown_type: UNKNOWN_TYPE;
/*
* Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.smtlibchecker;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.SMTLIBGenerator;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableCollection;
import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchcialGridCheckerWalkerGenerator;
import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalGrid;
import org.antlr.v4.runtime.ANTLRInputStream;
import org.antlr.v4.runtime.CommonTokenStream;
import org.antlr.v4.runtime.misc.NotNull;
import org.antlr.v4.runtime.tree.ParseTree;
import org.antlr.v4.runtime.tree.ParseTreeWalker;
import java.io.BufferedReader;
import java.io.IOException;
import java.io.InputStreamReader;
import java.io.OutputStreamWriter;
import java.io.Reader;
import java.io.UnsupportedEncodingException;
import java.io.Writer;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
/**
*
* @author Matthew Dawson <matthew@mjdsystems.ca>
*/
final public class CheckerRunner {
public static List<CheckerRunnerResult> RunZ3(HierarchicalGrid grid, VariableCollection vars) {
List<CheckerRunnerResult> ret = new ArrayList<CheckerRunnerResult>();
// Get the queries
HierarchicalGridSMTLIBGenerator queryGenerator = new HierarchicalGridSMTLIBGenerator(vars);
HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, queryGenerator);
// Start Z3
ProcessBuilder pb;
Process p;
try {
pb = new ProcessBuilder("z3", "-smt2", "-in");
p = pb.start();
} catch(IOException ex) {
throw new RuntimeException("Failed to start Z3!", ex);
}
// Input/Output refer to the direction from Z3's pov. So output is Z3's stdout.
BufferedReader z3Output;
Writer z3Input;
try {
// Sigh ... Java has horrible naming conversions here ...
z3Output = new BufferedReader(new InputStreamReader(p.getInputStream(), "ISO-8859-1"));
z3Input = new OutputStreamWriter(p.getOutputStream());
} catch(UnsupportedEncodingException ex) {
throw new RuntimeException("Failed to get ISO-8859-1 charset for talking to Z3!", ex);
}
StringBuilder GetValueRequestBuilder = new StringBuilder();
GetValueRequestBuilder.append("(get-value (");
for(Variable var:vars.getVariables().values()) {
GetValueRequestBuilder.append(var.name()).append(' ');
}
GetValueRequestBuilder.append("))\n");
String GetValueRequestString = GetValueRequestBuilder.toString();
try {
String VarDef = new SMTLIBGenerator().GenerateVariablesDeclaration(vars);
z3Input.write(VarDef);
for(String query : queryGenerator.getFinalQueries()) {
z3Input.write("(push 1)");
z3Input.write(query);
z3Input.write("(check-sat)\n");
z3Input.flush();
String res = z3Output.readLine();
if(res.equals("sat")) { // Failed query. Get a the result.
z3Input.write(GetValueRequestString);
z3Input.flush();
CheckerRunnerResult result = new CheckerRunnerResult();
result.Query = query;
result.SampleValues = parseSMTLIBOutput(z3Output);
ret.add(result);
} else if(res.equals("unknown")) {
// Z3 failed to prove. Throw a failure to check for now.
CheckerRunnerResult result = new CheckerRunnerResult();
result.Query = query;
result.SampleValues = null;
ret.add(result);
} else if(!res.equals("unsat")) {
// Something went wrong
throw new IllegalStateException("Z3 outputed something wrong (" + res + ")!");
}
z3Input.write("(pop 1)\r");
}
} catch(IOException ex) {
throw new RuntimeException("Something bad happened ...", ex);
} finally {
try {
z3Input.write("(exit)\n");
z3Input.flush();
p.destroy();
z3Input.close();
z3Output.close();
} catch(Exception e) {
// Don't care here, so just print it out.
System.out.println(e);
}
}
return ret;
}
private static Map<String, String> parseSMTLIBOutput(Reader reader) throws IOException {
if(reader.markSupported() == false) {
throw new IllegalArgumentException("Reader must support marks!");
}
final Map<String, String> ret = new HashMap<String, String>();
StringBuilder input = new StringBuilder();
int bracketMismatch = 1; // This starts with a (, so we immediately have a a mismatch.
char nextChar = getNextChar(reader);
if (nextChar != '(') { // Should start with a ( for output.
throw new IllegalStateException("Bad input, wanted a ( to start, got " + nextChar);
}
input.append(nextChar);
while(bracketMismatch != 0) {
nextChar = getNextChar(reader);
switch (nextChar) {
case '(':
bracketMismatch++;
break;
case ')':
bracketMismatch--;
break;
}
input.append(nextChar);
}
// Finally, clear the new line, so the output is now clear.
do {
reader.mark(5);
nextChar = getNextChar(reader);
} while(isWhitespace(nextChar) && nextChar != '\n');
if(!isWhitespace(nextChar)) {
reader.reset();
}
ANTLRInputStream antlrInput = new ANTLRInputStream(input.toString());
// create a lexer that feeds off of input CharStream
SMTLibOutParserLexer lexer = new SMTLibOutParserLexer(antlrInput);
// create a buffer of tokens pulled from the lexer
CommonTokenStream tokens = new CommonTokenStream(lexer);
// create a parser that feeds off the tokens buffer
SMTLibOutParserParser parser = new SMTLibOutParserParser(tokens);
ParseTree tree = parser.valuelist();
ParseTreeWalker walker = new ParseTreeWalker();
SMTLibOutParserListener listener = new SMTLibOutParserBaseListener() {
@Override
public void enterValue(@NotNull SMTLibOutParserParser.ValueContext ctx) {
id = ctx.ID().getText();
value = "";
}
@Override
public void enterNegative(@NotNull SMTLibOutParserParser.NegativeContext ctx) {
value = "(- ";
}
@Override
public void exitSingle(@NotNull SMTLibOutParserParser.SingleContext ctx) {
value += ctx.getText();
}
@Override
public void exitFraction(@NotNull SMTLibOutParserParser.FractionContext ctx) {
value += "(" + ctx.RATIONAL(0).getText() + " / " + ctx.RATIONAL(1).getText() + ")";
}
@Override
public void exitNegative(@NotNull SMTLibOutParserParser.NegativeContext ctx) {
value += ')';
}
@Override
public void exitExpr(@NotNull SMTLibOutParserParser.ExprContext ctx) {
ret.put(id, value);
}
String id = "";
String value;
};
walker.walk(listener, tree);
return ret;
}
private static char getNextChar(Reader reader) throws IOException {
char[] c = new char[1];
reader.read(c);
return c[0];
}
private static boolean isWhitespace(char toTest) {
if(toTest == ' ' ||
toTest == '\n' ||
toTest == '\r' ||
toTest == '\t') {
return true;
}
return false;
}
}
/*
* Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.smtlibchecker;
import java.util.Map;
/**
* @author Matthew Dawson <matthew@mjdsystems.ca>
*/
final public class CheckerRunnerResult {
public String Query;
public Map<String, String> SampleValues;
public String GenerateMatlabVariableDeclarations() {
StringBuilder ret = new StringBuilder();
for(Map.Entry<String, String> var: SampleValues.entrySet()) {
ret.
append(var.getKey()).
append(" = ").
append(var.getValue()).
append(";\n");
}
return ret.toString();
}
}
/*
* Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.smtlibchecker;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableCollection;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.MatlabParser;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.SMTLIBGenerator;
import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.Cell;
import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchcialGridCheckerGenerator;
import org.apache.commons.lang3.StringUtils;
import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Deque;
import java.util.List;
import java.util.Map;
/**
*
* @author Matthew Dawson <matthew@mjdsystems.ca>
*/
final public class HierarchicalGridSMTLIBGenerator implements HierarchcialGridCheckerGenerator {
public HierarchicalGridSMTLIBGenerator(VariableCollection variableDefinitions) {
m_variableDefinitions = variableDefinitions;
}
private String generateQueryPrefix() {
if (!m_parentCellsCVC3Code.isEmpty()){
String output = "(and ";
output += StringUtils.join(m_parentCellsCVC3Code, " ") + " ";
return output;
}
return "(and true ";
}
private void outputCells() {
// First is disjoint testing.
m_output += "(push 1)\n";
String query = "(assert ";
query += generateQueryPrefix();
if (m_currentDisjointQueries.isEmpty()) {
query += "false";
} else if (m_currentDisjointQueries.size() == 1) {
query += m_currentDisjointQueries.get(0);
} else {
query += "(or " + StringUtils.join(m_currentDisjointQueries, '\n') + ")";
}
query += "))";
m_queries.add(query);
m_output += query + "\n";
m_output += "(check-sat)\n(pop 1)\n";
// Next is complete.
m_output += "(push 1)\n";
query = "(assert ";
query += generateQueryPrefix();
query += "(not ";
if (m_currentCompleteQueries.isEmpty()) {
query += "true";
} else if (m_currentCompleteQueries.size() == 1) {
query += m_currentCompleteQueries.get(0);
} else {
query += "(or " + StringUtils.join(m_currentCompleteQueries, " ") + ")";
}
query += ")))";
m_queries.add(query);
m_output += query + "\n";
m_output += "(check-sat)\n(pop 1)\n";
m_currentlyRunning = false;
// And finally clear the running list of current queries.
m_currentCompleteQueries.clear();
m_currentDisjointQueries.clear();
}
@Override
public void descendIntoGridFromCell(Cell cell) {
if (m_currentlyRunning) {
outputCells();
}
m_parentCellsCVC3Code.addFirst(MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3Generator, m_booleanType));
m_currentlyRunning = true;
}
@Override
public void ascendFromGrid() {
if (m_currentlyRunning) {
outputCells();
}
m_parentCellsCVC3Code.removeFirst();
}
@Override
public void handleEdgeCell(Cell cell) {
handleLeafCell(cell);
}
@Override
public void handleLeafCell(Cell cell) {
// First get the appropriate CVC3 code from matlab.
String newCellCode = MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3Generator, m_booleanType);
// Next form the disjoint queries and add to the list.
for(String otherCellCode : m_currentCompleteQueries) {
String newDisjointQuery = "(and " + otherCellCode + " " + newCellCode + ")";
m_currentDisjointQueries.add(newDisjointQuery);
}
// Lastly add the cell to the list for the complete query
m_currentCompleteQueries.add(newCellCode);
}
@Override
public String getFinalString() {
if (m_currentlyRunning) {
outputCells();
}
return m_output;
}
public List<String> getFinalQueries() {
if (m_currentlyRunning) {
outputCells();
}
return m_queries;
}
Deque<String> m_parentCellsCVC3Code = new ArrayDeque<String>();
List<String> m_currentDisjointQueries = new ArrayList<String>();
List<String> m_currentCompleteQueries = new ArrayList<String>();
boolean m_currentlyRunning = true;
String m_output = "";
List<String> m_queries = new ArrayList<String>();
// To fix properly.
VariableCollection m_variableDefinitions;
static BooleanVariableType m_booleanType = new BooleanVariableType();
SMTLIBGenerator m_CVC3Generator = new SMTLIBGenerator();
}
grammar SMTLibOutParser;
valuelist: '(' value+ ')'; //Build list of variables
value: '(' ID expr ')';
expr: single |
fraction |
negative;
negative: '(-' fraction ')' |
'(-' single ')';
single: RATIONAL;
fraction: '(/' RATIONAL RATIONAL ')';
ID: [a-zA-Z][a-zA-Z0-9]*; //Variable identifier. Start with letter, then alpha numerical allowed.
RATIONAL: [0-9]+('.'[0-9]+)?;
WS : [ \t\r\n]+ -> skip ; // skip spaces, tabs, newlines
/*
* To change this template, choose Tools | Templates
* and open the template in the editor.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression;
/**
*
* @author Matthew Dawson <matthew@mjdsystems.ca>
*/
public class Cell {
Cell() {}
Cell(String initialContents) {
m_contents = initialContents;
}
public void setContents(String contents) {
m_contents = contents;
}
public String contents() {
return m_contents;
}
private String m_contents;
}
/*
* Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression;
/**
*
* @author Matthew Dawson <matthew@mjdsystems.ca>
*/
public interface HierarchcialGridCheckerGenerator {
void descendIntoGridFromCell(Cell cell);
void ascendFromGrid();
void handleLeafCell(Cell cell);
void handleEdgeCell(Cell cell);
String getFinalString();
}
/*
* Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression;
import java.util.List;
/**
*
* @author Matthew Dawson <matthew@mjdsystems.ca>
*/
public class HierarchcialGridCheckerWalkerGenerator {
private static void HandleGrid(SubHierarchyFetcher grid, HierarchcialGridCheckerGenerator generator) {
List<HierarchicalCell> cells = grid.getSubHiearchy();
for (int i = 0; i < cells.size(); ++i) {
HierarchicalCell cell = cells.get(i);
if (cell.getSubHiearchy().isEmpty()) {
generator.handleLeafCell(cell);
} else {
generator.handleEdgeCell(cell);
}
}
for (int i = 0; i < cells.size(); ++i) {
HierarchicalCell cell = cells.get(i);
if (!cell.getSubHiearchy().isEmpty()) {
generator.descendIntoGridFromCell(cell);
HandleGrid(cell, generator);
generator.ascendFromGrid();
}
}
}
public static String GenerateCheckerFromGrid(HierarchicalGrid grid, HierarchcialGridCheckerGenerator generator) {
HandleGrid(grid, generator);
return generator.getFinalString();
}
}
/*
* To change this template, choose Tools | Templates
* and open the template in the editor.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression;
import java.util.ArrayList;
import java.util.List;
/**
*
* @author Matthew Dawson <matthew@mjdsystems.ca>
*/
public class HierarchicalCell extends Cell implements SubHierarchyFetcher {
public HierarchicalCell() {}
public HierarchicalCell(String initialContents) {
super(initialContents);
}
@Override
public List<HierarchicalCell> getSubHiearchy() {
return m_subHiearchy;
}
private List<HierarchicalCell> m_subHiearchy = new ArrayList<HierarchicalCell>();
}
/*
* To change this template, choose Tools | Templates
* and open the template in the editor.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression;
import java.util.ArrayList;
import java.util.List;
/**
*
* @author Matthew Dawson <matthew@mjdsystems.ca>
*/
public class HierarchicalGrid implements SubHierarchyFetcher {
@Override
public List<HierarchicalCell> getSubHiearchy() {
return m_subHiearchy;
}
private List<HierarchicalCell> m_subHiearchy = new ArrayList<HierarchicalCell>();
}
/*
* Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression;
import java.util.List;
/**
*
* @author Matthew Dawson <matthew@mjdsystems.ca>
*/
public interface SubHierarchyFetcher {
List<HierarchicalCell> getSubHiearchy();
}
/*
* Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.cvc3generator;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParser;
import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalCell;
import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalGrid;
import ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchcialGridCheckerWalkerGenerator;
import java.util.List;
import static org.junit.Assert.*;
import org.junit.Test;
import org.junit.runner.RunWith;
import org.junit.runners.JUnit4;
/**
*
* @author Matthew Dawson <matthew@mjdsystems.ca>
*/
@RunWith(JUnit4.class)
public class HierarchicalGridCVC3GeneratorTest {
// Exercise the cvc3 generator using a table designed in matlab.
@Test
public void exerciseCVC3Generator() {
HierarchicalGrid grid = new HierarchicalGrid();
List<HierarchicalCell> topCells = grid.getSubHiearchy();
topCells.add(new HierarchicalCell("x > 0"));
topCells.add(new HierarchicalCell("x == 0"));
topCells.add(new HierarchicalCell("0 > x"));
List<HierarchicalCell> nextGrid = topCells.get(1).getSubHiearchy();
nextGrid.add(new HierarchicalCell("z > 0"));
nextGrid.add(new HierarchicalCell("z == 0"));
nextGrid.add(new HierarchicalCell("0 > z"));
nextGrid.get(1).getSubHiearchy().add(new HierarchicalCell("z == 0"));
String out = HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, new HierarchicalGridCVC3Generator(variableParser.parseVariables("x,z"), 1));
String expected = "ECHO \"begin1\";\n"+
"PUSH;\n"+
"QUERY (NOT ( (x > 0) AND (x = 0) ) AND\n"+
"NOT ( (x > 0) AND (0 > x) ) AND\n"+
"NOT ( (x = 0) AND (0 > x) ));\n"+
"POP;\n"+
"ECHO \"end1\";\n"+
"ECHO \"begin2\";\n"+
"PUSH;\n"+
"QUERY ((x > 0) OR (x = 0) OR (0 > x));\n"+
"POP;\n"+
"ECHO \"end2\";\n"+
"ECHO \"begin3\";\n"+
"PUSH;\n"+
"QUERY ((x = 0)) => (NOT ( (z > 0) AND (z = 0) ) AND\n"+
"NOT ( (z > 0) AND (0 > z) ) AND\n"+
"NOT ( (z = 0) AND (0 > z) ));\n"+
"POP;\n"+
"ECHO \"end3\";\n"+
"ECHO \"begin4\";\n"+
"PUSH;\n"+
"QUERY ((x = 0)) => ((z > 0) OR (z = 0) OR (0 > z));\n"+
"POP;\n"+
"ECHO \"end4\";\n"+
"ECHO \"begin5\";\n"+
"PUSH;\n"+
"QUERY ((z = 0) AND (x = 0)) => ();\n"+
"POP;\n"+
"ECHO \"end5\";\n"+
"ECHO \"begin6\";\n"+
"PUSH;\n"+
"QUERY ((z = 0) AND (x = 0)) => ((z = 0));\n"+
"POP;\n"+
"ECHO \"end6\";\n";
assertEquals(expected, out);
}
VariableParser variableParser = new VariableParser();
}
/*
* To change this template, choose Tools | Templates
* and open the template in the editor.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
import org.junit.Test;
import org.junit.runner.RunWith;
import org.junit.runners.JUnit4;
import static org.junit.Assert.*;
/**
*
* @author matthew
*/
@RunWith(JUnit4.class)
public class CVC3GeneratorTest {
/**
* Test of addition operation.
*/
@Test
public void testAdditionOpConverstion() {
BinaryOperation op = BinaryOperation.Addition;
assertEquals("+", CVC3Generator.ConvertToOutputOp(op, new RealVariableType()));
assertEquals("BVPLUS(13,", CVC3Generator.ConvertToOutputOp(op, new FixedPointVariableType(true, 13, 5)));
}
/**
* Test of literals containing decimals.
*
* All decimals must be represented as fractions. Ensure that this happens.
*/
@Test
public void testLiteralRationalsAreFractions() {
Literal literal = new Literal("4.56");
assertEquals("(456/100)", literal.getCheckerOutput(new CVC3Generator(), new RealVariableType()));
}
}
/*
* To change this template, choose Tools | Templates
* and open the template in the editor.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
import org.junit.Test;
import static org.junit.Assert.*;
/**
*
* @author matthew
*/
public class FixedPointVariableTypeTest {
/**
* Test of constructor in class FixedPointType.
*/
@Test
public void testConstructor() {
FixedPointVariableType instance = new FixedPointVariableType(true, 19, 9);
assertEquals(true, instance.isSigned());
assertEquals(19, instance.digits());
assertEquals(9, instance.fractionPart());
}
/**
* Test of getCVC3Definition method, of class FixedPointType.
*/
@Test
public void testGetCVC3Definition() {
CVC3Generator generator = new CVC3Generator();
FixedPointVariableType instance = new FixedPointVariableType(true, 16, 8);
assertEquals("BITVECTOR(16)", generator.GenerateVariableType(instance));
}
/**
* Test of canCastToType method, of class FixedPointType.
*/
@Test
public void testCanCastToType() {
FixedPointVariableType instance = new FixedPointVariableType(true, 16, 8);
assertFalse(instance.canCastToType(new RealVariableType()));
}
/**
* Test of equals method, of class FixedPointType.
*/
@Test
public void testEquals() {
FixedPointVariableType instance = new FixedPointVariableType(true, 16, 8);
assertEquals(new FixedPointVariableType(true, 16, 8), instance);
assertFalse(instance.equals(new FixedPointVariableType(false, 16, 8)));
assertFalse(instance.equals(new FixedPointVariableType(true, 15, 8)));
assertFalse(instance.equals(new FixedPointVariableType(true, 16, 7)));
}
}