Need help to implement an ambiguous grammar (ACSL grammar) [message #1794841] |
Fri, 07 September 2018 14:03 |
|
Hello everybody,
I post a message here, because I'm not able to find how to manage trouble with ambiguous grammar.
I'm implementing a part of the ACSL Grammar (see https://frama-c.com/download/acsl_1.3.pdf). Basically it allows to write annotations in C code.
This grammar provides many rules. My problem comes from Term and Predicat (Pred) definitions which use common symbols. Here an abtract of this grammar:
Grammar of Terms:
literal::= \true | \false | integer | real | string | char
bin-op::= + | - | * | / | % | << | >> | == | != | <= | >= | > | < | && | || | ^^:
term::= literal |
\result |
term bin-op term
| and others possibilities
Grammar of Pred:
rel-op::= == | != | <= | >= | > | < (Yes, these symbols are also available in bin-op)
pred::= \true | \false |
term (rel-op term)+ |
pred && pred | (&& is also available in bin-op)
pred || pred | (|| is also available in bin-op)
and others possibilities.
With the grammar plugins in attachement, the ambiguous bin-on symbols are commented, so the next sentence is valid:
requires \result >= 12 && \result <= 15; (rule RequiresClause)
It is the rule RequiresClause ('requires' pred=PredExpression) where the PredExpression is a PredConjuction (pred1 && pred2) with pred1="\result >= 12" and pred2="\result <= 15".
pred1 and pred2 are identified as the rule Pred_TermComparison (a comparison of 2 Terms with a RelOp (== | != | <= | >= | > | <).
This usecase works fine.
Now, if I uncomment one of the ambiguous bin-op symbol (== | != | <= | >= | && | ...), my sentence is not yet recognized as valid by the framework.
By example, uncommenting <= in the bin-op rule, I assume, the framework interprete the sentence as:
\result >= 12 is now seen as a term
\result >= 15 as a pred (as previously)
so we have as now a conjunction between a term and a pred and it is not valid.
Please, could you indicate me a way to fix my troubles (parameters to add in the mw2e file, generated code to override or whatever).
you will find in attachement:
- the xtext plugins for this grammar
- some snapshot of the ACSL grammar
Here my mwe2 file and my grammar (also in the attached plugins of course):
The mwe2 file
module com.cea.xtext.demo.GenerateAcslDemo
import org.eclipse.xtext.xtext.generator.*
import org.eclipse.xtext.xtext.generator.model.project.*
var rootPath = ".."
Workflow {
//
bean = org.eclipse.emf.mwe.utils.StandaloneSetup {
// platformUri = "${rootPath}"
scanClassPath = true
//load EMF ECORE
uriMap = {
from = "platform:/plugin/org.eclipse.emf.ecore/model/Ecore.ecore"
to = "platform:/resource/org.eclipse.emf.ecore/model/Ecore.ecore"
}
uriMap = {
from = "platform:/plugin/org.eclipse.emf.codegen.ecore/model/GenModel.genmodel"
to = "platform:/resource/org.eclipse.emf.codegen.ecore/model/GenModel.genmodel"
}
uriMap = {
from = "platform:/plugin/org.eclipse.emf.ecore/model/Ecore.genmodel"
to = "platform:/resource/org.eclipse.emf.ecore/model/Ecore.genmodel"
}
registerGeneratedEPackage = "org.eclipse.emf.ecore.EcorePackage"
registerGenModelFile = "platform:/resource/org.eclipse.emf.ecore/model/Ecore.genmodel"
registerGeneratedEPackage = "org.eclipse.emf.codegen.ecore.genmodel.GenModelPackage"
registerGenModelFile = "platform:/resource/org.eclipse.emf.codegen.ecore/model/GenModel.genmodel"//load UML
////Types
uriMap = {
from = "platform:/plugin/org.eclipse.uml2.codegen.ecore/model/GenModel.ecore"
to = "platform:/resource/org.eclipse.uml2.codegen.ecore/model/GenModel.ecore"
}
uriMap = {
from = "platform:/plugin/org.eclipse.uml2.codegen.ecore/model/GenModel.genmodel"
to = "platform:/resource/org.eclipse.uml2.codegen.ecore/model/GenModel.genmodel"
}
uriMap = {
from = "platform:/plugin/org.eclipse.uml2.types/model/Types.ecore"
to = "platform:/resource/org.eclipse.uml2.types/model/Types.ecore"
}
uriMap = {
from = "platform:/plugin/org.eclipse.uml2.types/model/Types.genmodel"
to = "platform:/resource/org.eclipse.uml2.types/model/Types.genmodel"
}
uriMap = {
from = "platform:/plugin/org.eclipse.uml2.uml/model/UML.ecore"
to = "platform:/resource/org.eclipse.uml2.uml/model/UML.ecore"
}
uriMap = {
from = "platform:/plugin/org.eclipse.uml2.uml/model/UML.genmodel"
to = "platform:/resource/org.eclipse.uml2.uml/model/UML.genmodel"
}
//
registerGeneratedEPackage = "org.eclipse.uml2.codegen.ecore.genmodel.GenModelPackage"
registerGenModelFile = "platform:/resource/org.eclipse.uml2.codegen.ecore/model/GenModel.genmodel"
registerGeneratedEPackage = "org.eclipse.uml2.uml.UMLPackage"
registerGenModelFile = "platform:/resource/org.eclipse.uml2.uml/model/UML.genmodel"
}
component = XtextGenerator {
configuration = {
project = StandardProjectConfig {
baseName = "com.cea.xtext.demo"
rootPath = rootPath
runtimeTest = {
enabled = true
}
eclipsePlugin = {
enabled = true
}
eclipsePluginTest = {
enabled = true
}
createEclipseMetaData = true
}
code = {
encoding = "UTF-8"
lineDelimiter = "\n"
fileHeader = "/*\n * generated by Xtext \${version}\n */"
}
}
language = StandardLanguage {
name = "com.cea.xtext.demo.AcslDemo"
fileExtensions = "acslDemo"
fragment = ecore2xtext.Ecore2XtextValueConverterServiceFragment2 auto-inject {}
serializer = {
generateStub = false
}
validator = {
// composedCheck = "org.eclipse.xtext.validation.NamesAreUniqueValidator"
}
parserGenerator = parser.antlr.XtextAntlrGeneratorFragment2 auto-inject {
debugGrammar = true
combinedGrammar = true
options = {
backtrack = true
}
}
fragment = idea.parser.antlr.XtextAntlrIDEAGeneratorFragment auto-inject {
options = {
backtrack = true
}
}
}
}
}
The grammar
grammar com.cea.xtext.demo.AcslDemo with org.eclipse.xtext.common.Terminals
generate acslDemo "http://www.cea.com/xtext/demo/AcslDemo"
import "http://www.eclipse.org/uml2/5.0.0/UML" as uml
import "http://www.eclipse.org/emf/2002/Ecore" as ecore
/**
* the input rule to edit an opaque behavior
*/
OpaqueBehaviorRule:
contract=FunctionContract;
/*
* defined in figure 2.5 page 29
*/
FunctionContract:
{FunctionContract} (requiresClause+=RequiresClause)*
;
/**
* defined in figure 2.5, page 29
*/
RequiresClause:
'requires' pred=PredExpression ';';
//TERMS
TermExpression:
TermBinOpExpression;
TermBinOpExpression returns TermExpression:
TermArrayAccess ({TermBinOpExpression.left=current} op=BinOp right=TermArrayAccess)*
;
TermArrayAccess returns TermExpression:
TermPrimary ({TermArrayAccess.left=current} '[' right=TermPrimary ']')*;
TermPrimary returns TermExpression:
{TermParenthesis} '(' termInParenthesis=TermExpression ')' | Term_UnaryOp | TermNot | {TermOld} '\\old' '('
termInOld=TermExpression ')' | TermAtomic
;
TermNot returns TermExpression:
'!' exp=TermPrimary;
TermAtomic returns TermExpression:
{TermLiteral} lit=Literal | Term_Result | Term_PolyId;
Term_PolyId returns TermExpression:
{Term_PolyId} ident=Ident;
Ident:
id=ID;
/**
* We adapt the pred description defined in Figure 2.2
* to avoid left recursive grammar and others troubles
*/
//Pred:
// expression=PredExpression
//// pred=Pred_Basic secondMember+=(Pred_RightMember)*
//;
//PRED-PRED-PRED-PRED-PRED-PRED-PRED-PRED-PRED-PRED-PRED-PRED-PRED-
PredExpression:
PredImplication;
PredImplication returns PredExpression:
PredEquivalence ({PredImplication.left=current} '==>' right=PredEquivalence)*;
PredEquivalence returns PredExpression:
PredOrExpression ({PredEquivalence.left=current} '<==>' right=PredOrExpression)*;
PredOrExpression returns PredExpression:
PredAndExpression ({PredOrExpression.left=current} '||' right=PredAndExpression)*;
PredAndExpression returns PredExpression:
PredXorExpression ({PredAndExpression.left=current} '&&' right=PredXorExpression)*;
PredXorExpression returns PredExpression:
PredPlusOrMinus ({PredXorExpression.left=current} '^^' right=PredPlusOrMinus)*;
PredPlusOrMinus returns PredExpression:
PredMulOrDiv (({PredPlus.left=current} '+' | {PredMinus.left=current} "-") right=PredMulOrDiv)*;
PredMulOrDiv returns PredExpression:
PredPrimary ({PredMulOrDiv.left=current} op=('*' | '/') right=PredPrimary)*;
PredPrimary returns PredExpression:
Pred_TermComparison |{PredParenthesis} '(' pred=PredExpression ')' | {PredNot} '!' exp=PredPrimary | {PredOld} '\\old' '('
pred=PredExpression ')' | PredAtomic;
////defined in Figure 2.2
enum RelOp:
EQUALS="=="
| NOT_EQUALS="!="
| SUPERIOR_STRICT=">"
| SUPERIOR_OR_EQUALS=">="
| INFERIOR_STRICT="<"
| INFERIOR_OR_EQUALS="<=";
Pred_TermComparison returns PredExpression:
{Pred_TermComparison} left=TermExpression right+=Pred_TermComparisonRight+;
Pred_TermComparisonRight:
op=RelOp right=TermExpression;
PredAtomic returns PredExpression:
Pred_True
| Pred_False;
Pred_True returns PredExpression:
{Pred_True} "\\true";
Pred_False returns PredExpression:
{Pred_False} "\\false";
//END_PRED-END_PRED-END_PRED-END_PRED-END_PRED-END_PRED-END_PRED-END_PRED-END_PRED-END_PRED-END_PRED-END_PRED-END_PRED-END_PRED
//END_TERMS
Literal:
LiteralBoolean
| LiteralInt
| LiteralReal
| LiteralString
| LiteralChar;
LiteralBoolean:
value=("\\true" | "\\false");
LiteralInt:
i=INT;
LiteralString:
s=STRING;
LiteralReal:
r=REAL;
LiteralChar:
c=CHAR;
terminal REAL:
INT '.' INT;
//
terminal CHAR:
('a'..'z' | 'A'..'Z');// | '_' | '0'..'9');
//
//terminal BOOLEAN:
// ('\\true' | '\\false');
//
///**
// * binary operators
// * figure 2.1 page 16 in document acsl_1.13.pdf
// *
// */
enum BinOp:
PLUS="+"
| MINUS="-"
| STAR = "/*"
| SLASH="/"
| PERCENT = "%"
| LEFT_SHIFT = "<<"
| RIGHT_SHIFT = ">>"
// | DOUBLE_EQUALS = "=="
// | NOT_EQUALS = "!="
// | TODO1 = "<=" //TODO
// | TODO2 = ">="//TODO
// | TODO3 = ">"//TODO
// | TODO4 = "<"//TODO
// | BOOLEAN_AND_OPERATION = "&&"
// | BOOLEAN_OR_OPERATION = "||"
// | BOOLEAN_XOR_OPERATION= "^^"
| BITWISE_AND_OPERATION = "&"
| BITWISE_OR_OPERATION = "|"
| BITWISE_XOR_OPERATION = "^"
;
//
///**
// * unary operators
// * figure 2.1 page 16 in document acsl_1.13.pdf
// */
//
enum UnaryOp:
UNARY_PLUS="+"
| UNARY_MINUS="-"
| BOOLEAN_NEGATION="!"
| BITWISE_COMPLEMENTATION="~"
| POINTER_DEFERENCING="*"
| ADRESS_OF_OPERATOR="&";
Term_UnaryOp returns TermExpression:
unaryOperator=UnaryOp referencedTermInUnaryOpTerm=TermExpression;
Term_Result:
{Term_Result} '\\result';
@Override
terminal ID : ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|'0'..'9')* ;// | ('\'' -> '\'') ;
Regards,
--
Vincent LORENZO
|
|
|
|
Re: Need help to implement an ambiguous grammar (ACSL grammar) [message #1794856 is a reply to message #1794844] |
Sat, 08 September 2018 07:14 |
|
you have multiple problems
(1) unusal pattern for unary expressions. ususal pattern is
Term_UnaryOp returns TermExpression: {Term_UnaryOp}op=UnaryOp p=TermPrimary | TermPrimary;
(2) duplicate not (its in unary and a separate one
(3) you have an actually left cycle between the primaries
i recommend you to generate a debug grammar
parserGenerator = {
debugGrammar = true
}
and use antlrworks to inspect
Twitter : @chrdietrich
Blog : https://www.dietrich-it.de
|
|
|
|
Powered by
FUDForum. Page generated in 0.04037 seconds