diff --git a/settings.gradle.kts b/settings.gradle.kts index 136769ed58..58dca165ee 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -20,6 +20,7 @@ include( "xcfa/xcfa-analysis", "xcfa/xcfa-cli", "xcfa/cat", + "xcfa/algorithmselection", "xta/xta", "xta/xta-analysis", diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaState.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaState.java index 5fb4683987..b354aaa657 100644 --- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaState.java +++ b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaState.java @@ -67,6 +67,11 @@ public boolean isBottom() { return state.isBottom(); } + @Override + public boolean isTop() { + return state.isTop(); + } + @Override public Expr toExpr() { // TODO Should be loc = l and toExpr(state) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/State.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/State.java index 4d1de9c526..3d357e618b 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/State.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/State.java @@ -27,4 +27,6 @@ public interface State { */ boolean isBottom(); + default boolean isTop() { return false; } + } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java index 16221bf33e..b50f60f710 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java @@ -22,6 +22,8 @@ import java.util.Collection; import hu.bme.mit.theta.common.container.Containers; + +import java.util.Objects; import java.util.Optional; import java.util.OptionalInt; import java.util.stream.Stream; @@ -41,6 +43,19 @@ public final class ARG { private int nextId = 0; final PartialOrd partialOrd; + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + ARG arg = (ARG) o; + return initialized == arg.initialized && nextId == arg.nextId && initNodes.equals(arg.initNodes) && partialOrd.equals(arg.partialOrd); + } + + @Override + public int hashCode() { + return Objects.hash(initNodes.stream().map(ArgNode::getState), initialized, nextId, partialOrd); + } + private ARG(final PartialOrd partialOrd) { initNodes = Containers.createSet(); this.partialOrd = partialOrd; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java index 2bddf6f8b0..6bb5ddf59a 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java @@ -20,6 +20,7 @@ import hu.bme.mit.theta.analysis.Prec; import hu.bme.mit.theta.analysis.State; import hu.bme.mit.theta.analysis.algorithm.ARG; +import hu.bme.mit.theta.analysis.algorithm.ArgNode; import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.common.Utils; @@ -27,7 +28,13 @@ import hu.bme.mit.theta.common.logging.Logger.Level; import hu.bme.mit.theta.common.logging.NullLogger; +import java.util.Collection; +import java.util.LinkedHashSet; +import java.util.Objects; +import java.util.Set; import java.util.concurrent.TimeUnit; +import java.util.stream.Collectors; +import java.util.stream.Stream; import static com.google.common.base.Preconditions.checkNotNull; @@ -43,6 +50,10 @@ public final class CegarChecker refiner; private final Logger logger; + // controlled restart + private Set args = new LinkedHashSet<>(); + private P lastPrecision = null; + private CegarChecker(final Abstractor abstractor, final Refiner refiner, final Logger logger) { this.abstractor = checkNotNull(abstractor); this.refiner = checkNotNull(refiner); @@ -59,6 +70,28 @@ public static CegarChecker(abstractor, refiner, logger); } + private class AbstractArg { + private final Collection states; + + + private AbstractArg(final Stream> nodes){ + states = nodes.map(ArgNode::getState).collect(Collectors.toSet()); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + AbstractArg that = (AbstractArg) o; + return states.equals(that.states); + } + + @Override + public int hashCode() { + return Objects.hash(states); + } + } + @Override public SafetyResult check(final P initPrec) { logger.write(Level.INFO, "Configuration: %s%n", this); @@ -80,6 +113,29 @@ public SafetyResult check(final P initPrec) { abstractorTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - abstractorStartTime; logger.write(Level.MAINSTEP, "| Checking abstraction done, result: %s%n", abstractorResult); + AbstractArg abstractArg = new AbstractArg(arg.getNodes()); + if(args.contains(abstractArg) && lastPrecision != null && lastPrecision.equals(prec)) { + System.err.println("Not solvable!"); + throw new RuntimeException("Not solvable!"); + } + args.add(abstractArg); + lastPrecision = prec; + + /*Stream> argNodeStream = arg.getNodes().filter(saArgNode -> !saArgNode.getState().isTop() && saArgNode.isSafe()); + List> collect = arg.getNodes().filter(saArgNode -> !saArgNode.getState().isTop() && saArgNode.isSafe()).collect(Collectors.toList()); + + if(argNodeStream.count() == 0) { + System.err.println("True arg"); + if(lastArgTrue && lastPrecision != null && lastPrecision.equals(prec)) { + System.err.println("Not solvable!"); + throw new RuntimeException("Not solvable!"); + } + lastArgTrue = true; + } else { + lastArgTrue = false; + } + lastPrecision = prec;*/ + if (abstractorResult.isUnsafe()) { logger.write(Level.MAINSTEP, "| Refining abstraction...%n"); final long refinerStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplState.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplState.java index 54887e6985..d14d004790 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplState.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplState.java @@ -124,6 +124,11 @@ public boolean isBottom() { return false; } + @Override + public boolean isTop() { + return val.getDecls().isEmpty(); + } + @Override public String toString() { return Utils.lispStringBuilder(ExplState.class.getSimpleName()).aligned() @@ -183,4 +188,5 @@ private static class BottomLazyHolder { private static class TopLazyHolder { static final ExplState INSTANCE = new NonBottom(ImmutableValuation.empty()); } + } diff --git a/subprojects/common/c-frontend/build.gradle.kts b/subprojects/common/c-frontend/build.gradle.kts index baaffcbfec..29f81f4b8b 100644 --- a/subprojects/common/c-frontend/build.gradle.kts +++ b/subprojects/common/c-frontend/build.gradle.kts @@ -4,4 +4,5 @@ plugins { } dependencies { compile(project(":theta-core")) + compile(project(":theta-algorithmselection")) } \ No newline at end of file diff --git a/subprojects/common/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java b/subprojects/common/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java index 792e839c5e..5e87b6ee63 100644 --- a/subprojects/common/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java +++ b/subprojects/common/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java @@ -33,6 +33,7 @@ import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CArray; import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CPointer; import hu.bme.mit.theta.frontend.transformation.model.types.complex.real.CReal; +import hu.bme.mit.theta.xcfa.algorithmselection.MaxEnumAnalyzer; import org.kframework.mpfr.BigFloat; import org.kframework.mpfr.BinaryMathContext; @@ -245,6 +246,7 @@ public Expr visitRelationalExpression(CParser.RelationalExpressionContext ctx default: throw new IllegalStateException("Unexpected value: " + ctx.signs.get(i).getText()); } + MaxEnumAnalyzer.instance.consume(guard); CComplexType signedInt = CComplexType.getSignedInt(); expr = Ite(guard, signedInt.getUnitValue(), signedInt.getNullValue()); FrontendMetadata.create(expr, "cType", signedInt); @@ -536,7 +538,7 @@ public Expr visitPrimaryExpressionConstant(CParser.PrimaryExpressionConstantC BigFloat bigFloat; if (text.startsWith("0x")) { - throw new UnsupportedOperationException("Hexadeximal FP constants are not yet supported!"); + throw new UnsupportedOperationException("Hexadecimal FP constants are not yet supported!"); } else if (text.startsWith("0b")) { throw new UnsupportedOperationException("Binary FP constants are not yet supported!"); } else { diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvType.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvType.java index 8d5b43c483..bebb09ac45 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvType.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvType.java @@ -58,6 +58,11 @@ public int getSize() { return size; } + public Boolean getSigned() { + checkState(signed!=null); + return signed; + } + @Override public EqExpr Eq(Expr leftOp, Expr rightOp) { return BvEqExpr.of(leftOp, rightOp); diff --git a/subprojects/xcfa/algorithmselection/README.md b/subprojects/xcfa/algorithmselection/README.md new file mode 100644 index 0000000000..12d4261b52 --- /dev/null +++ b/subprojects/xcfa/algorithmselection/README.md @@ -0,0 +1,3 @@ +## Overview + +Cat language \ No newline at end of file diff --git a/subprojects/xcfa/algorithmselection/build.gradle.kts b/subprojects/xcfa/algorithmselection/build.gradle.kts new file mode 100644 index 0000000000..52019ac21a --- /dev/null +++ b/subprojects/xcfa/algorithmselection/build.gradle.kts @@ -0,0 +1,9 @@ +plugins { + id("java-common") + id("antlr-grammar") +} + +dependencies { + compile(project(":theta-common")) + compile(project(":theta-core")) +} diff --git a/subprojects/xcfa/algorithmselection/src/main/antlr/C.g4 b/subprojects/xcfa/algorithmselection/src/main/antlr/C.g4 new file mode 100644 index 0000000000..e704536416 --- /dev/null +++ b/subprojects/xcfa/algorithmselection/src/main/antlr/C.g4 @@ -0,0 +1,949 @@ +/* + [The "BSD licence"] + Copyright (c) 2013 Sam Harwell + All rights reserved. + + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions + are met: + 1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + 2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + 3. The name of the author may not be used to endorse or promote products + derived from this software without specific prior written permission. + + THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR + IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES + OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. + IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, + INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT + NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF + THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +*/ + +/** C 2011 grammar built from the C11 Spec */ +grammar C; + + +primaryExpression + : Identifier # primaryExpressionId + | Constant # primaryExpressionConstant + | StringLiteral+ # primaryExpressionStrings + | '(' expression ')' # primaryExpressionBraceExpression + //| genericSelection # primaryExpressionGenericSelection + | '__extension__'? '(' compoundStatement ')' # primaryExpressionGccExtension + //| '__builtin_va_arg' '(' unaryExpression ',' typeName ')' # primaryExpressionBuiltinVaArg + //| '__builtin_offsetof' '(' typeName ',' unaryExpression ')' # primaryExpressionBuiltinOffsetof + ; + +//genericSelection +// : '_Generic' '(' assignmentExpression ',' genericAssocList ')' +// ; + +//genericAssocList +// : genericAssociation (',' genericAssociation)* +// ; + +//genericAssociation +// : (typeName | 'default') ':' assignmentExpression +// ; + +postfixExpression + : (primaryExpression /*| postfixExpressionExtension*/) + (postfixExpressionBrackets | postfixExpressionBraces | postfixExpressionMemberAccess + | postfixExpressionPtrMemberAccess | postfixExpressionIncrement | postfixExpressionDecrement)* + ; + +//postfixExpressionExtension +// : '__extension__'? '(' typeName ')' '{' initializerList ','? '}' +// ; +postfixExpressionBrackets + : '[' expression ']' + ; +postfixExpressionBraces + : '(' argumentExpressionList? ')' + ; +postfixExpressionMemberAccess + : '.' Identifier + ; +postfixExpressionPtrMemberAccess + : '->' Identifier + ; +postfixExpressionIncrement + : '++' + ; +postfixExpressionDecrement + : '--' + ; + +argumentExpressionList + : assignmentExpression (',' assignmentExpression)* + ; + +unaryExpression + : + (unaryExpressionIncrement | unaryExpressionDecrement /*| unaryExpressionSizeof*/)* + (postfixExpression + | unaryExpressionCast + | unaryExpressionSizeOrAlignOf +// | unaryExpressionAddressof // GCC extension address of label + ) + ; + +unaryExpressionIncrement + : '++' + ; +unaryExpressionDecrement + : '--' + ; +//unaryExpressionSizeof +// : 'sizeof' +// ; +unaryExpressionCast + : unaryOperator castExpression + ; +unaryExpressionSizeOrAlignOf + : ('sizeof' | '_Alignof') '(' typeName ')' + ; +//unaryExpressionAddressof +// : '&&' Identifier +// ; + +unaryOperator + : '&' | '*' | '+' | '-' | '~' | '!' + ; + +castExpression + : '__extension__'? '(' typeName ')' castExpression #castExpressionCast + | unaryExpression #castExpressionUnaryExpression +// | DigitSequence #castExpressionDigitSequence + ; + +multiplicativeExpression + : castExpression (signs+=('*'|'/'|'%') castExpression)* + ; + +additiveExpression + : multiplicativeExpression (signs+=('+'|'-') multiplicativeExpression)* + ; + +shiftExpression + : additiveExpression (signs+=('<<'|'>>') additiveExpression)* + ; + +relationalExpression + : shiftExpression (signs+=('<'|'>'|'<='|'>=') shiftExpression)* + ; + +equalityExpression + : relationalExpression (signs+=('=='| '!=') relationalExpression)* + ; + +andExpression + : equalityExpression ( '&' equalityExpression)* + ; + +exclusiveOrExpression + : andExpression ('^' andExpression)* + ; + +inclusiveOrExpression + : exclusiveOrExpression ('|' exclusiveOrExpression)* + ; + +logicalAndExpression + : inclusiveOrExpression ('&&' inclusiveOrExpression)* + ; + +logicalOrExpression + : logicalAndExpression ( '||' logicalAndExpression)* + ; + +conditionalExpression + : logicalOrExpression ('?' expression ':' conditionalExpression)? + ; + +assignmentExpression + : conditionalExpression #assignmentExpressionConditionalExpression + | unaryExpression assignmentOperator assignmentExpression #assignmentExpressionAssignmentExpression +// | DigitSequence #assignmentExpressionDigitSequence + ; + +assignmentOperator + : '=' | '*=' | '/=' | '%=' | '+=' | '-=' | '<<=' | '>>=' | '&=' | '^=' | '|=' + ; + +expression + : assignmentExpression (',' assignmentExpression)* + ; + +constantExpression + : conditionalExpression + ; + +declaration + : declarationSpecifiers initDeclaratorList? ';' +// | staticAssertDeclaration # declarationStatic + ; + +declarationSpecifiers + : declarationSpecifier+ + ; + +declarationSpecifiers2 + : declarationSpecifier+ + ; + +declarationSpecifier + : storageClassSpecifier + | typeSpecifier + | typeQualifier + | functionSpecifier + | alignmentSpecifier + ; + +initDeclaratorList + : initDeclarator (',' initDeclarator)* + ; + +initDeclarator + : declarator ('=' initializer)? + ; + +storageClassSpecifier + : 'typedef' + | 'extern' + | 'static' + | '_Thread_local' + | 'auto' + | 'register' + ; + +typeSpecifier + : ('void' + | 'char' + | 'short' + | 'int' + | 'long' + | 'signed' + | 'unsigned' + | '_Bool' + | '_Complex' + | '__m128' + | '__m128d' + | '__m128i') # typeSpecifierSimple + | 'float' # typeSpecifierFloat + | 'double' # typeSpecifierDouble + | '__extension__' '(' ('__m128' | '__m128d' | '__m128i') ')' # typeSpecifierExtension + | atomicTypeSpecifier # typeSpecifierAtomic + | structOrUnionSpecifier # typeSpecifierCompound + | enumSpecifier # typeSpecifierEnum + | typedefName # typeSpecifierTypedefName + | '__typeof__' '(' constantExpression ')' # typeSpecifierTypeof + | typeSpecifier pointer # typeSpecifierPointer + ; + +structOrUnionSpecifier + : structOrUnion Identifier? '{' structDeclarationList '}' # compoundDefinition + | structOrUnion Identifier # compoundUsage + ; + +structOrUnion + : 'struct' + | 'union' + ; + +structDeclarationList + : structDeclaration+ + ; + +structDeclaration + : specifierQualifierList structDeclaratorList? ';' +// | staticAssertDeclaration #structDeclarationStatic + ; + +specifierQualifierList + : (typeSpecifier| typeQualifier) specifierQualifierList? + ; + +structDeclaratorList + : structDeclarator (',' structDeclarator)* + ; + +structDeclarator + : declarator #structDeclaratorSimple + | declarator? ':' constantExpression #structDeclaratorConstant + ; + +enumSpecifier + : 'enum' Identifier? '{' enumeratorList ','? '}' #enumDefinition + | 'enum' Identifier #enumUsage + ; + +enumeratorList + : enumerator (',' enumerator)* + ; + +enumerator + : enumerationConstant ('=' constantExpression)? + ; + +enumerationConstant + : Identifier + ; + +atomicTypeSpecifier + : '_Atomic' '(' typeName ')' + ; + +typeQualifier + : 'const' + | 'restrict' + | 'volatile' + | '_Atomic' + ; + +functionSpecifier + : ('inline' + | '_Noreturn' + | '__inline__' // GCC extension + | '__stdcall') + | gccAttributeSpecifier + | '__declspec' '(' Identifier ')' + ; + +alignmentSpecifier + : '_Alignas' '(' (typeName | constantExpression) ')' + ; + +declarator + : pointer? directDeclarator gccDeclaratorExtension* + ; + +directDeclarator + : Identifier # directDeclaratorId + | '(' declarator ')' # directDeclaratorBraces + | directDeclarator '[' typeQualifierList? assignmentExpression? ']' # directDeclaratorArray1 + | directDeclarator '[' 'static' typeQualifierList? assignmentExpression ']' # directDeclaratorArray2 + | directDeclarator '[' typeQualifierList 'static' assignmentExpression ']' # directDeclaratorArray3 + | directDeclarator '[' typeQualifierList? '*' ']' # directDeclaratorArray4 + | directDeclarator '(' parameterTypeList? ')' # directDeclaratorFunctionDecl +// | directDeclarator '(' identifierList? ')' # directDeclaratorFunctionCall + | Identifier ':' DigitSequence # directDeclaratorBitField +// | '(' typeSpecifier? pointer directDeclarator ')' # directDeclaratorFunctionPointer + ; + +gccDeclaratorExtension + : '__asm' '(' StringLiteral+ ')' + | gccAttributeSpecifier + ; + +gccAttributeSpecifier + : '__attribute__' '(' '(' gccAttributeList ')' ')' + ; + +gccAttributeList + : gccAttribute? (',' gccAttribute?)* + ; + +gccAttribute + : ~(',' | '(' | ')') // relaxed def for "identifier or reserved word" + ('(' argumentExpressionList? ')')? + ; + +nestedParenthesesBlock + : ( ~('(' | ')') + | '(' nestedParenthesesBlock ')' + )* + ; + +pointer + : ((stars+='*'|'^') ('__restrict')? typeQualifierList?)+ // ^ - Blocks language extension + ; + +typeQualifierList + : typeQualifier+ + ; + +parameterTypeList + : parameterList (',' ellipses='...')? + ; + +parameterList + : parameterDeclaration (',' parameterDeclaration)* + ; + +parameterDeclaration + : declarationSpecifiers declarator # ordinaryParameterDeclaration + | declarationSpecifiers2 abstractDeclarator? # abstractParameterDeclaration + ; + +//identifierList +// : Identifier (',' Identifier)* +// ; + +typeName + : specifierQualifierList abstractDeclarator? + ; + +abstractDeclarator + : pointer + | pointer? directAbstractDeclarator gccDeclaratorExtension* + ; + +directAbstractDeclarator + : '(' abstractDeclarator ')' gccDeclaratorExtension* + | '[' typeQualifierList? assignmentExpression? ']' + | '[' 'static' typeQualifierList? assignmentExpression ']' + | '[' typeQualifierList 'static' assignmentExpression ']' + | '[' '*' ']' + | '(' parameterTypeList? ')' gccDeclaratorExtension* + | directAbstractDeclarator '[' typeQualifierList? assignmentExpression? ']' + | directAbstractDeclarator '[' 'static' typeQualifierList? assignmentExpression ']' + | directAbstractDeclarator '[' typeQualifierList 'static' assignmentExpression ']' + | directAbstractDeclarator '[' '*' ']' + | directAbstractDeclarator '(' parameterTypeList? ')' gccDeclaratorExtension* + ; + +typedefName + : Identifier + ; + +initializer + : assignmentExpression + | '{' initializerList ','? '}' + ; + +initializerList + : designation? initializers+=initializer (',' designation? initializers+=initializer)* + ; + +designation + : designatorList '=' + ; + +designatorList + : designator+ + ; + +designator + : '[' constantExpression ']' + | '.' Identifier + ; + +//staticAssertDeclaration +// : '_Static_assert' '(' constantExpression ',' StringLiteral+ ')' ';' +// ; + +statement + : labeledStatement + | compoundStatement + | expressionStatement + | selectionStatement + | iterationStatement + | jumpStatement ';' +// | ('__asm' | '__asm__') ('volatile' | '__volatile__') '(' (logicalOrExpression (',' logicalOrExpression)*)? (':' (logicalOrExpression (',' logicalOrExpression)*)?)* ')' ';' + ; + +labeledStatement + : Identifier ':' statement # identifierStatement + | 'case' constantExpression ':' statement # caseStatement + | 'default' ':' statement # defaultStatement + ; + +compoundStatement + : '{' blockItemList? '}' + ; + +blockItemList + : blockItem+ + ; + +blockItem + : statement # bodyStatement + | declaration # bodyDeclaration + ; + +expressionStatement + : expression? ';' + ; + +selectionStatement + : 'if' '(' expression ')' statement ('else' statement)? #ifStatement + | 'switch' '(' expression ')' statement #switchStatement + ; + +iterationStatement + : While '(' expression ')' statement # whileStatement + | Do statement While '(' expression ')' ';' # doWhileStatement + | For '(' forCondition ')' statement # forStatement + ; + +// | 'for' '(' expression? ';' expression? ';' forUpdate? ')' statement +// | For '(' declaration expression? ';' expression? ')' statement + +forCondition + : forInit ';' forTest ';' forIncr + ; + +forInit + : forDeclaration + | expression? + ; + +forTest + : forExpression? + ; + +forIncr + : forExpression? + ; + +forDeclaration + : declarationSpecifiers initDeclaratorList? + ; + +forExpression + : assignmentExpression (',' assignmentExpression)* + ; + +jumpStatement + : 'goto' Identifier # gotoStatement + | 'continue' # continueStatement + | 'break' # breakStatement + | 'return' expression? # returnStatement +// | 'goto' unaryExpression // GCC extension + ; + +compilationUnit + : translationUnit? EOF + ; + +translationUnit + : externalDeclaration+ + ; + +externalDeclaration + : functionDefinition #externalFunctionDefinition + | declaration #globalDeclaration + | ';' #externalNop + ; + +functionDefinition + : declarationSpecifiers declarator /*declarationList?*/ compoundStatement + ; + +//declarationList +// : declaration+ +// ; + +Extension: '__extension__' -> skip; // Hack to make .i files work (SV-COMP) +VoidSizeof: '(void) sizeof' -> skip; // Hack to make .i files work (SV-COMP) +Auto : 'auto'; +Break : 'break'; +Case : 'case'; +Char : 'char'; +Const : 'const'; +Continue : 'continue'; +Default : 'default'; +Do : 'do'; +Double : 'double'; +Else : 'else'; +Enum : 'enum'; +Extern : 'extern'; +Float : 'float'; +For : 'for'; +Goto : 'goto'; +If : 'if'; +Inline : 'inline'; +Int : 'int'; +Long : 'long'; +Register : 'register'; +Restrict : 'restrict'; +Return : 'return'; +Short : 'short'; +Signed : 'signed'; +Sizeof : 'sizeof'; +Static : 'static'; +Struct : 'struct'; +Switch : 'switch'; +Typedef : 'typedef'; +Union : 'union'; +Unsigned : 'unsigned'; +Void : 'void'; +Volatile : 'volatile'; +While : 'while'; + +Alignas : '_Alignas'; +Alignof : '_Alignof'; +Atomic : '_Atomic'; +Bool : '_Bool'; +Complex : '_Complex'; +Generic : '_Generic'; +Imaginary : '_Imaginary'; +Noreturn : '_Noreturn'; +StaticAssert : '_Static_assert'; +ThreadLocal : '_Thread_local'; + +LeftParen : '('; +RightParen : ')'; +LeftBracket : '['; +RightBracket : ']'; +LeftBrace : '{'; +RightBrace : '}'; + +Less : '<'; +LessEqual : '<='; +Greater : '>'; +GreaterEqual : '>='; +LeftShift : '<<'; +RightShift : '>>'; + +Plus : '+'; +PlusPlus : '++'; +Minus : '-'; +MinusMinus : '--'; +Star : '*'; +Div : '/'; +Mod : '%'; + +And : '&'; +Or : '|'; +AndAnd : '&&'; +OrOr : '||'; +Caret : '^'; +Not : '!'; +Tilde : '~'; + +Question : '?'; +Colon : ':'; +Semi : ';'; +Comma : ','; + +Assign : '='; +// '*=' | '/=' | '%=' | '+=' | '-=' | '<<=' | '>>=' | '&=' | '^=' | '|=' +StarAssign : '*='; +DivAssign : '/='; +ModAssign : '%='; +PlusAssign : '+='; +MinusAssign : '-='; +LeftShiftAssign : '<<='; +RightShiftAssign : '>>='; +AndAssign : '&='; +XorAssign : '^='; +OrAssign : '|='; + +Equal : '=='; +NotEqual : '!='; + +Arrow : '->'; +Dot : '.'; +Ellipsis : '...'; + +Identifier + : IdentifierNondigit + ( IdentifierNondigit + | Digit + )* + ; + +fragment +IdentifierNondigit + : Nondigit + | UniversalCharacterName + //| // other implementation-defined characters... + ; + +fragment +Nondigit + : [a-zA-Z_] + ; + +fragment +Digit + : [0-9] + ; + +fragment +UniversalCharacterName + : '\\u' HexQuad + | '\\U' HexQuad HexQuad + ; + +fragment +HexQuad + : HexadecimalDigit HexadecimalDigit HexadecimalDigit HexadecimalDigit + ; + +Constant + : IntegerConstant + | FloatingConstant + //| EnumerationConstant + | CharacterConstant + ; + +fragment +IntegerConstant + : DecimalConstant IntegerSuffix? + | OctalConstant IntegerSuffix? + | HexadecimalConstant IntegerSuffix? + | BinaryConstant + ; + +fragment +BinaryConstant + : '0' [bB] [0-1]+ + ; + +fragment +DecimalConstant + : NonzeroDigit Digit* + ; + +fragment +OctalConstant + : '0' OctalDigit* + ; + +fragment +HexadecimalConstant + : HexadecimalPrefix HexadecimalDigit+ + ; + +fragment +HexadecimalPrefix + : '0' [xX] + ; + +fragment +NonzeroDigit + : [1-9] + ; + +fragment +OctalDigit + : [0-7] + ; + +fragment +HexadecimalDigit + : [0-9a-fA-F] + ; + +fragment +IntegerSuffix + : UnsignedSuffix LongSuffix? + | UnsignedSuffix LongLongSuffix + | LongSuffix UnsignedSuffix? + | LongLongSuffix UnsignedSuffix? + ; + +fragment +UnsignedSuffix + : [uU] + ; + +fragment +LongSuffix + : [lL] + ; + +fragment +LongLongSuffix + : 'll' | 'LL' + ; + +fragment +FloatingConstant + : DecimalFloatingConstant + | HexadecimalFloatingConstant + ; + +fragment +DecimalFloatingConstant + : FractionalConstant ExponentPart? FloatingSuffix? + | DigitSequence ExponentPart FloatingSuffix? + ; + +fragment +HexadecimalFloatingConstant + : HexadecimalPrefix (HexadecimalFractionalConstant | HexadecimalDigitSequence) BinaryExponentPart FloatingSuffix? + ; + +fragment +FractionalConstant + : DigitSequence? '.' DigitSequence + | DigitSequence '.' + ; + +fragment +ExponentPart + : [eE] Sign? DigitSequence + ; + +fragment +Sign + : [+-] + ; + +DigitSequence + : Digit+ + ; + +fragment +HexadecimalFractionalConstant + : HexadecimalDigitSequence? '.' HexadecimalDigitSequence + | HexadecimalDigitSequence '.' + ; + +fragment +BinaryExponentPart + : [pP] Sign? DigitSequence + ; + +fragment +HexadecimalDigitSequence + : HexadecimalDigit+ + ; + +fragment +FloatingSuffix + : [flFL] + ; + +fragment +CharacterConstant + : '\'' CCharSequence '\'' + | 'L\'' CCharSequence '\'' + | 'u\'' CCharSequence '\'' + | 'U\'' CCharSequence '\'' + ; + +fragment +CCharSequence + : CChar+ + ; + +fragment +CChar + : ~['\\\r\n] + | EscapeSequence + ; + +fragment +EscapeSequence + : SimpleEscapeSequence + | OctalEscapeSequence + | HexadecimalEscapeSequence + | UniversalCharacterName + ; + +fragment +SimpleEscapeSequence + : '\\' ['"?abfnrtv\\] + ; + +fragment +OctalEscapeSequence + : '\\' OctalDigit OctalDigit? OctalDigit? + ; + +fragment +HexadecimalEscapeSequence + : '\\x' HexadecimalDigit+ + ; + +StringLiteral + : EncodingPrefix? '"' SCharSequence? '"' + ; + +fragment +EncodingPrefix + : 'u8' + | 'u' + | 'U' + | 'L' + ; + +fragment +SCharSequence + : SChar+ + ; + +fragment +SChar + : ~["\\\r\n] + | EscapeSequence + | '\\\n' // Added line + | '\\\r\n' // Added line + ; + +ComplexDefine + : '#' Whitespace? 'define' ~[#\r\n]* + -> skip + ; + +IncludeDirective + : '#' Whitespace? 'include' Whitespace? (('"' ~[\r\n]* '"') | ('<' ~[\r\n]* '>' )) Whitespace? Newline + -> skip + ; + +// ignore the following asm blocks: +/* + asm + { + mfspr x, 286; + } + */ +AsmBlock + : 'asm' ~'{'* '{' ~'}'* '}' + -> skip + ; + +// ignore the lines generated by c preprocessor +// sample line : '#line 1 "/home/dm/files/dk1.h" 1' +LineAfterPreprocessing + : '#line' Whitespace* ~[\r\n]* + -> skip + ; + +LineDirective + : '#' Whitespace? DecimalConstant Whitespace? StringLiteral ~[\r\n]* + -> skip + ; + +PragmaDirective + : '#' Whitespace? 'pragma' Whitespace ~[\r\n]* + -> skip + ; + +Whitespace + : [ \t]+ + -> skip + ; + +Newline + : ( '\r' '\n'? + | '\n' + ) + -> skip + ; + +BlockComment + : '/*' .*? '*/' + -> skip + ; + +LineComment + : '//' ~[\r\n]* + -> skip + ; + +WORD + : [a-zA-Z_]+ -> skip + ; diff --git a/subprojects/xcfa/algorithmselection/src/main/java/hu/bme/mit/theta/xcfa/algorithmselection/MaxEnumAnalyzer.java b/subprojects/xcfa/algorithmselection/src/main/java/hu/bme/mit/theta/xcfa/algorithmselection/MaxEnumAnalyzer.java new file mode 100644 index 0000000000..8cb010504d --- /dev/null +++ b/subprojects/xcfa/algorithmselection/src/main/java/hu/bme/mit/theta/xcfa/algorithmselection/MaxEnumAnalyzer.java @@ -0,0 +1,110 @@ +package hu.bme.mit.theta.xcfa.algorithmselection; + +import hu.bme.mit.theta.common.Tuple2; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.LitExpr; +import hu.bme.mit.theta.core.type.abstracttype.LeqExpr; +import hu.bme.mit.theta.core.type.abstracttype.LtExpr; +import hu.bme.mit.theta.core.type.anytype.RefExpr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.bvtype.BvLitExpr; +import hu.bme.mit.theta.core.type.bvtype.BvType; +import hu.bme.mit.theta.core.type.inttype.IntLitExpr; +import hu.bme.mit.theta.core.utils.BvUtils; + +import java.math.BigInteger; +import java.util.HashMap; +import java.util.Optional; + +/** + * Estimates the value boundaries of integer C variables to decide on a value for the configuration option maxEnum + */ +public class MaxEnumAnalyzer { + public static final MaxEnumAnalyzer instance = new MaxEnumAnalyzer(); + public static boolean enabled = true; + + HashMap, Tuple2, Optional>> boundaries = new HashMap<>(); // k: variable ref, v: min, max + + public void consume(Expr relationalExpr) { + if(!enabled) { + return; + } + LitExpr constant = null; + RefExpr var = null; + + // check, if it is a constant rel.op var expression or var rel.op constant or neither + if (relationalExpr.getOps().get(0) instanceof LitExpr) { + if (relationalExpr.getOps().get(1) instanceof RefExpr) { + constant = (LitExpr) relationalExpr.getOps().get(0); + var = (RefExpr) relationalExpr.getOps().get(1); + } + } else if (relationalExpr.getOps().get(1) instanceof LitExpr) { + if (relationalExpr.getOps().get(0) instanceof RefExpr) { + constant = (LitExpr) relationalExpr.getOps().get(1); + var = (RefExpr) relationalExpr.getOps().get(0); + } + } + + if(constant == null) return; // neither + + // get boundary value + BigInteger constantValue; + if(constant instanceof BvLitExpr) { // bitvector arithmetic + if( ((BvType) constant.getType()).getSigned() ) { + constantValue = BvUtils.signedBvLitExprToBigInteger((BvLitExpr) constant); + } else { + constantValue = BvUtils.unsignedBvLitExprToBigInteger((BvLitExpr) constant); + } + } else if(constant instanceof IntLitExpr) { // integer arithmetic + constantValue = ((IntLitExpr)constant).getValue(); + } else { + throw new RuntimeException("Type of LitExpr should be either BvType or IntType"); + } + + // add boundaries to hashmap + if(relationalExpr instanceof LtExpr || relationalExpr instanceof LeqExpr) { + if(boundaries.containsKey(var)) { + if(boundaries.get(var).get2().isEmpty() || boundaries.get(var).get2().get().compareTo(constantValue) < 0) { + boundaries.put(var, Tuple2.of(boundaries.get(var).get1(), Optional.of(constantValue))); + } + } else { + boundaries.put(var, Tuple2.of(Optional.empty(), Optional.of(constantValue))); + } + } else { + if(boundaries.containsKey(var)) { + if(boundaries.get(var).get1().isEmpty() || boundaries.get(var).get1().get().compareTo(constantValue) > 0) { + boundaries.put(var, Tuple2.of(Optional.of(constantValue), boundaries.get(var).get2())); + } + } else { + boundaries.put(var, Tuple2.of(Optional.of(constantValue), Optional.empty())); + } + } + } + + public BigInteger estimateMaxEnum() { + if(!enabled) { + throw new RuntimeException("Max enum estimation should not be used as it is disabled currently"); + } + Optional width = boundaries.values().stream().map(objects -> { + if(objects.get2().isEmpty() || objects.get1().isEmpty()) { + return BigInteger.valueOf(1); + } + return objects.get2().get().subtract(objects.get1().get()); + }).max(BigInteger::compareTo); + + boundaries.entrySet().forEach(entry -> { + System.out.println("key: " + entry.getKey()); + if(entry.getValue().get1().isPresent()) { + System.out.println("min: " + entry.getValue().get1().get()); + } else System.out.println("No min"); + if(entry.getValue().get2().isPresent()) { + System.out.println("max: " + entry.getValue().get2().get()); + } else System.out.println("No max"); + }); + + if(width.isPresent() && width.get().compareTo(BigInteger.valueOf(1)) < 0) { + width = Optional.of(BigInteger.valueOf(1)); + } + return width.orElse(BigInteger.valueOf(1)); + } +} diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/stateless/XcfaCli.java b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/stateless/XcfaCli.java index 193db2681e..c262d8d75b 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/stateless/XcfaCli.java +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/stateless/XcfaCli.java @@ -43,6 +43,7 @@ import hu.bme.mit.theta.frontend.transformation.model.statements.CProgram; import hu.bme.mit.theta.frontend.transformation.model.statements.CStatement; import hu.bme.mit.theta.solver.z3.Z3SolverFactory; +import hu.bme.mit.theta.xcfa.algorithmselection.MaxEnumAnalyzer; import hu.bme.mit.theta.xcfa.analysis.XcfaAnalysis; import hu.bme.mit.theta.xcfa.analysis.XcfaTraceToWitness; import hu.bme.mit.theta.xcfa.analysis.weakmemory.bounded.BoundedMultithreadedAnalysis; @@ -105,6 +106,9 @@ public class XcfaCli { @Parameter(names = "--print-cfa", description = "Print CFA and exit.") boolean printcfa; + @Parameter(names = "--estimateMaxEnum", description = "Estimate maxenum automatically; overwrites the value of the --maxenum flag.") + boolean estimateMaxEnum; + @Parameter(names = "--timeout", description = "Seconds until timeout (not precise)") Long timeS = Long.MAX_VALUE; @@ -181,6 +185,11 @@ private void run() { } ArchitectureConfig.arithmetic = arithmeticType; + if(estimateMaxEnum) { + MaxEnumAnalyzer.enabled = true; + } else { + MaxEnumAnalyzer.enabled = false; + } try { if(outputResults) { @@ -234,6 +243,11 @@ private void run() { return; } + if(estimateMaxEnum) { + System.out.println("Estimated maxEnum: " + MaxEnumAnalyzer.instance.estimateMaxEnum().intValue()); + maxEnum = MaxEnumAnalyzer.instance.estimateMaxEnum().intValue(); + } + if(showGui) { new XcfaGui(xcfa); return;