Skip to content
GitLab
Explore
Sign in
Hide whitespace changes
Inline
Side-by-side
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/MatlabParser.g4
0 → 100644
View file @
e574db0d
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
;
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/MatlabParser.java
0 → 100644
View file @
e574db0d
/*
* 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
>();
}
}
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/PVSSimpleParser.g4
0 → 100644
View file @
e574db0d
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')+ ;
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/PVSSimpleParser.java
0 → 100644
View file @
e574db0d
/*
* 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
>();
}
}
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/VariableParser.java
0 → 100644
View file @
e574db0d
/*
* 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
;
}
}
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/VariableParserLexer.g4
0 → 100644
View file @
e574db0d
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;
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/VariableParserParser.g4
0 → 100644
View file @
e574db0d
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;
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/smtlibchecker/CheckerRunner.java
0 → 100644
View file @
e574db0d
/*
* 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
;
}
}
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/smtlibchecker/CheckerRunnerResult.java
0 → 100644
View file @
e574db0d
/*
* 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
();
}
}
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/smtlibchecker/HierarchicalGridSMTLIBGenerator.java
0 → 100644
View file @
e574db0d
/*
* 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
();
}
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/smtlibchecker/SMTLibOutParser.g4
0 → 100644
View file @
e574db0d
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
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/tablularexpression/Cell.java
0 → 100644
View file @
e574db0d
/*
* 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
;
}
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/tablularexpression/HierarchcialGridCheckerGenerator.java
0 → 100644
View file @
e574db0d
/*
* 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
();
}
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/tablularexpression/HierarchcialGridCheckerWalkerGenerator.java
0 → 100644
View file @
e574db0d
/*
* 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
();
}
}
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/tablularexpression/HierarchicalCell.java
0 → 100644
View file @
e574db0d
/*
* 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
>();
}
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/tablularexpression/HierarchicalGrid.java
0 → 100644
View file @
e574db0d
/*
* 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
>();
}
Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/tablularexpression/SubHierarchyFetcher.java
0 → 100644
View file @
e574db0d
/*
* 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
();
}
Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/cvc3generator/HierarchicalGridCVC3GeneratorTest.java
0 → 100644
View file @
e574db0d
/*
* 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
();
}
Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/CVC3GeneratorTest.java
0 → 100644
View file @
e574db0d
/*
* 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
()));
}
}
Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/FixedPointVariableTypeTest.java
0 → 100644
View file @
e574db0d
/*
* 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
)));
}
}
Prev
1
2
3
4
Next